Deep fmap with GADTs and type families.

5 Mar 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

Deep fmap with GADTs and type families.

Dan Doel