Deep fmap with GADTs and type families.
Dan Doel
dan.doel at gmail.com
Thu Mar 5 22:07:39 EST 2009
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:
--- snip ---
newtype FuntorD f = F { fdmap :: forall a b. (a -> b) -> f a -> f b }
deepFDMap :: FunctorD f -> Nat n -> (a -> b) -> Nest n f a -> Nest n f b
deepFDMap d Z f = fdmap d f
deepFDMap d (S n) f = fdmap d (deepFDMap d n f)
--- snip ---
This works, but to my surprise "deepFMap = deepFDMap (F fmap)" gives the exact
same error as above. Bringing my situation to #haskell, two solutions were
found:
--- snip ---
deepFMap :: forall n f a b. Functor f =>
Nat n -> (a -> b) -> Nest n f a -> Nest n f b
deepFMap = deepFDMap (F fmap :: FunctorD f)
data Proxy (f :: * -> *) = Proxy
deepFMap' :: Functor f =>
Proxy f -> Nat n -> (a -> b) -> Nest n f a -> Nest n f b
deepFMap' _ Z f = fmap f
deepFMap' p (S n) f = fmap (deepFMap p n f)
--- snip ---
But we've so far not been able to find a way of merely annotating the original
into working. So, I was wondering if any of the more knowledgeable folks here
could illuminate what's going wrong here, and whether I should expect my
original code to work or not.
Thanks in advance.
-- Dan
More information about the Glasgow-haskell-users
mailing list