RankNTypes: apply the same function to pairs of different types

Question

I was trying to define this function to regroup three lists of pairs:

{-# LANGUAGE RankNTypes #-}

mapAndZip3 :: (forall x. x -> f x) -> [a] -> [b] -> [c] 
                                   -> [(f a, f b, f c)]
mapAndZip3 f la lb lc = zipWith3 (\a b c -> (f a, f b, f c)) la lb lc


main = do
    let x = mapAndZip3 (fst) [(1,"fruit"), (2,"martini")] 
                             [("chips","fish"),("rice","steak")]
                             [(5,"cake"),(4,"pudding")]
    print x -- was expecting [(1,"chips",5), (2,"rice",4)]

At first I didn't include the RankNTypes or the forall, but then after seing this, namely the liftTup definition, I thought that it should be enough.

But clearly, it wasn't, as I still get an error:

mapAndZip3.hs:8:25:
Couldn't match type `x' with `(f0 x, b0)'
  `x' is a rigid type variable bound by
      a type expected by the context: x -> f0 x at mapAndZip3.hs:8:13
Expected type: x -> f0 x
  Actual type: (f0 x, b0) -> f0 x
In the first argument of `mapAndZip3', namely `(fst)'

I clearly have a limited understanding of the forall keyword, but from what I understood it should, in this case, allow for f to accept any type. What I don't understand is: once within a given context, and used once, does the definition gets 'fixed' for the remaining context?

It doesn't seem so, because if I replace "chips" and "rice" with Ints, the compiler still complains, so I guess I'm assuming something wrong (of course, if I remove the type annotation of mapAndZip3 in this latter case, everything works out because the signature gets simplified to mapAndZip3 :: (a -> t) -> [a] -> [a] -> [a] -> [(t, t, t)], but this is not what I want).

I also found this question, but can't really make if this is the same problem or not, since the function I am trying to apply is not id, but fst or snd, functions that actually return different types (a -> b).

Answer 1

The problem is that fst doesn't have the required type

(forall x. x -> f x)

The type of fst is

fst :: (a, b) -> a

and a is not of the form f (a,b). The f there is a variable that must be instantiated with a type constructor, something like [], Maybe, Either Bool. f can't stand for any "type function" like Λ (a,b) -> a, it must be a type constructor.

It works if we provide it a function of the required type (sorry, stupid example):

{-# LANGUAGE RankNTypes #-}

mapAndZip3 :: (forall x. x -> f x) -> [a] -> [b] -> [c]
                                   -> [(f a, f b, f c)]
mapAndZip3 f la lb lc = zipWith3 (\a b c -> (f a, f b, f c)) la lb lc

fst0 x = (True,x)

main = do
    let x = mapAndZip3 (fst0) [(1 :: Int,"fruit"), (2,"martini")]
                             [("chips","fish"),("rice","steak")]
                             [(5 :: Int,"cake"),(4,"pudding")]
    print x

since here fst0 has the type a -> ((,) Bool) a, which has the form x -> f x.

Answer 2

The problem in your signature is the f. Let's expand it a bit:

mapAndZip3 :: forall (a :: *) (b :: *) (c :: *) (f :: *->*)
           =>  (forall x. x -> f x) -> [a] -> [b] -> [c] 
                               -> [(f a, f b, f c)]

f is here supposed to be "any type-level function", in your instantiation it would be type f (a,b) = a. But Haskell doesn't allow you to abstract over type-level functions, only over type constructors, like Maybe or IO. So mapAndZip3 Just would actually be possible, but fst doesn't construct but deconstruct a tuple type.

Type-level functions don't even really exist in Haskell98, they are only possible since TypeFamilies. The problem is basically that Haskell's kind language is untyped¹, yet type level functions are required to be total functions². But then, you can't really define any nontrivial function (i.e., one other than id or type constructors) that's defined on all types. Type-level fst certainly isn't total, it works only on tuple types.

So to work with such functions you explicitly need to specify their context in some other way. With TypeFamilies it could work like this:

class TypeFunctionDomain d where
  type TypeFunction d :: *

instance TypeFunctionDomain (a,b) where
  type TypeFunction (a,b) = a

mapAndZip3 :: (forall x. TypeFunctionDomain x => x -> TypeFunction x)
          -> [a] -> [b] -> [c] 
                   -> [(TypeFunction a, TypeFunction b, TypeFunction c)]

However, this isn't really what you want: it would not be possible to define in the same scope also a TypeFunctionDomain instance corrsponding to snd, meaning that mapAndZip3 effectively wouldn't be polymorphic at all, but only work with a single function.

These problems can only be solved properly in dependently typed languages such as Agda, where kinds really are just types of types and you can define type-level functions just as well as value-level functions. But this comes as something of a price: all functions need to be total functions! This isn't really a bad thing, but it means these languages generally aren't really Turing-complete (which would require the possibility of infinite looping/recursion; that is however ⟂ with respect to full result evaluation).

---

¹ Things have changed a bit with the advent of kind polymorphism etc..

² That's unlike in e.g. C++, which allows – albeit with very horrible syntax – duck-typed type-level functions, through templates. That can be quite a nice feature, but one of the consequences is that you often get completely unreadable error messages (with even less relation to the real problem than GHC's worst "Possible fix" hints...) when trying to instantiate a template with a type argument outside the implicit domain.