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-boun...@haskell.org [mailto:glasgow-haskell-users-
| boun...@haskell.org] On Behalf Of Dan Doel
| Sent: 06 March 2009 03:08
| To: glasgow-haskell-users@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...
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
