Type functions and ambiguity

[Simon Peyton-Jones]

Dan's example fails thus:

|   Map.hs:25:19:
|     Couldn't match expected type `Nest n1 f b'
|            against inferred type `Nest n1 f1 b'
|     In the expression: fmap (deepFMap n f)
|     In the definition of `deepFMap':
|         deepFMap (S n) f = fmap (deepFMap n f)
|
| for reasons I don't really understand. So I tried the following:

For what it's worth, here's why. Suppose we have

        type family N a :: *

        f :: forall a. N a -> Int
        f = <blah>

        g :: forall b. N b -> Int
        g x = 1 + f x

The defn of 'g' fails with a very similar error to the one above.  Here's why.  We instantiate the occurrence of 'f' with an as-yet-unknown type 'alpha', so at the call site 'f' has type
        N alpha -> Int
Now, we know from g's type sig that x :: N b.  Since f is applies to x, we must have
        N alpha ~ N b

Does that imply that (alpha ~ b)?   Alas no!  If t1=t2 then (N t1 = N t2), of course, but *not* vice versa.  For example, suppose that

        type instance N [c] = N c

Now we could solve the above with (alpha ~ [b]), or (alpha ~ [[b]]).

You may say
a) There is no such instance.  Well, but you can see it pushes the search for a (unique) solution into new territory.

b) It doesn't matter which solution the compiler chooses: any will do.  True in this case, but false if f :: forall a. (Num a) => N a -> Int.  Now it matters which instance is chosen.


This kind of example encapsulates the biggest single difficulty with using type families in practice.  What is worse is that THERE IS NO WORKAROUND.  You *ought* to be able to add an annotation to guide the type checker.  Currently you can't.  The most obvious solution would be to allow the programmer to specify the types at which a polymorphic function is called, like this:

        g :: forall b. N b -> Int
        g x = 1 + f {b} x

The {b} says that f takes a type argument 'b', which should be used to instantiate its polymorphic type variable 'a'.   Being able to do this would be useful in other circumstances (eg impredicative polymorphism). The issue is really the syntax, and the order of type variables in an implicit forall.

Anyway I hope this helps clarify the issue.

Simon



| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
| bounces at haskell.org] On Behalf Of Dan Doel
| Sent: 06 March 2009 03:08
| To: glasgow-haskell-users at haskell.org
| Subject: Deep fmap with GADTs and type families.
|
| Greetings,
|
| Someone on comp.lang.functional was asking how to map through arbitrary
| nestings of lists, so I thought I'd demonstrate how his non-working ML
| function could actually be typed in GHC, like so:
|
| --- snip ---
|
| {-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls,
|     Rank2Types, ScopedTypeVariables #-}
|
| data Z
| data S n
|
| data Nat n where
|   Z :: Nat Z
|   S :: Nat n -> Nat (S n)
|
| type family Nest n (f :: * -> *) a :: *
|
| type instance Nest Z     f a = f a
| type instance Nest (S n) f a = f (Nest n f a)
|
| deepMap :: Nat n -> (a -> b) -> Nest n [] a -> Nest n [] b
| deepMap Z     f = map f
| deepMap (S n) f = map (deepMap n f)
|
| --- snip ---
|
| This works. However, the straight forward generalisation doesn't:
|
| --- snip ---
|
| deepFMap :: Functor f => Nat n -> (a -> b) -> Nest n f a -> Nest n f b
| deepFMap Z     f = fmap f
| deepFMap (S n) f = fmap (deepFMap n f)
|
| --- snip ---
|
| This fails with a couple errors like:
|
|   Map.hs:25:19:
|     Couldn't match expected type `Nest n1 f b'
|            against inferred type `Nest n1 f1 b'
|     In the expression: fmap (deepFMap n f)
|     In the definition of `deepFMap':
|         deepFMap (S n) f = fmap (deepFMap n f)
|
| for reasons I don't really understand. So I tried the following:
|
...rest snipped...