Type functions and ambiguity
Simon PeytonJones
simonpj at microsoft.com
Mon Mar 9 11:56:14 EDT 2009
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 asyetunknown 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: glasgowhaskellusersbounces at haskell.org [mailto:glasgowhaskellusers
 bounces at haskell.org] On Behalf Of Dan Doel
 Sent: 06 March 2009 03:08
 To: glasgowhaskellusers 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 nonworking 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...
More information about the Glasgowhaskellusers
mailing list