[Haskell-cafe] Dependently typed fold in GHC/Haskell

[Christiaan Baaij]

Dear Cafe,

I'm trying to convert the following Idris code, which compiles:

> gfold : {p : Nat -> Type} 
>         -> ((l : Nat) -> a -> p l -> p (S l))
>         -> p 0 -> Vect k a -> p k
> gfold _ z Nil             = z
> gfold f z ((::) {n} x xs) = f n x (gfold f z xs)
> 
> gconcat : {m : Nat} -> Vect n a -> Vect m a -> Vect (n + m) a
> gconcat {m} xs ys = gfold {p} f ys xs
>   where
>     p : Nat -> Type
>     p l = Vect (l + m) a
> 
>     f : (l : Nat) -> a -> Vect (l + m) a -> Vect (S (l + m)) a
>     f _ x r = x :: r

To Haskell + various GHC extensions, which gives me type errors:

> {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators, RankNTypes,
>              ScopedTypeVariables, TypeFamilies #-}
> 
> import Data.Proxy
> 
> data Nat = Z | S Nat
> 
> type family Plus (x :: Nat) (y :: Nat) :: Nat where
>   Plus Z     y = y
>   Plus (S n) y = S (Plus n y)
> 
> data Vec :: * -> Nat -> * where
>   Nil  :: Vec a Z
>   (:>) :: a -> Vec a n -> Vec a (S n)
> 
> gfold :: Proxy (p :: Nat -> *) 
>       -> (forall l . Proxy l -> a -> p l -> p (S l))
>       -> p Z -> Vec a k -> p k
> gfold Proxy f z Nil       = z
> gfold Proxy f z (x :> xs) = f Proxy x (gfold Proxy f z xs)
> 
> type family P (a :: *) (m :: Nat) (l :: Nat) :: * where
>   P a m l = Vec a (Plus l m)
> 
> gconcat :: forall n m a . Vec a n -> Vec a m -> Vec a (Plus n m)
> gconcat xs ys = gfold p f ys xs
>   where
>     p :: Proxy (P a m)
>     p = Proxy
> 
>     f :: forall (l :: Nat) . Proxy l -> a -> Vec a (Plus l m)
>       -> Vec a (S (Plus l m))
>     f _ x r = x :> r

I get the following errors:

> VecTest.hs:25:25:
>     Couldn't match type ‘l’ with ‘Plus l m’
>       ‘l’ is a rigid type variable bound by
>           a type expected by the context:
>             Proxy l -> a -> Vec a l -> Vec a ('S l)
>           at VecTest.hs:25:17
>     Expected type: Proxy l -> a -> Vec a l -> Vec a ('S l)
>       Actual type: Proxy l
>                    -> a -> Vec a (Plus l m) -> Vec a ('S (Plus l m))
>     Relevant bindings include
>       p :: Proxy (P a m) (bound at VecTest.hs:28:5)
>       f :: forall (l :: Nat).
>            Proxy l -> a -> Vec a (Plus l m) -> Vec a ('S (Plus l m))
>         (bound at VecTest.hs:32:5)
>       ys :: Vec a m (bound at VecTest.hs:25:12)
>       gconcat :: Vec a n -> Vec a m -> Vec a (Plus n m)
>         (bound at VecTest.hs:25:1)
>     In the second argument of ‘gfold’, namely ‘f’
>     In the expression: gfold p f ys xs
> 
> VecTest.hs:25:27:
>     Couldn't match type ‘m’ with ‘'Z’
>       ‘m’ is a rigid type variable bound by
>           the type signature for
>             gconcat :: Vec a n -> Vec a m -> Vec a (Plus n m)
>           at VecTest.hs:24:21
>     Expected type: Vec a 'Z
>       Actual type: Vec a m
>     Relevant bindings include
>       p :: Proxy (P a m) (bound at VecTest.hs:28:5)
>       f :: forall (l :: Nat).
>            Proxy l -> a -> Vec a (Plus l m) -> Vec a ('S (Plus l m))
>         (bound at VecTest.hs:32:5)
>       ys :: Vec a m (bound at VecTest.hs:25:12)
>       gconcat :: Vec a n -> Vec a m -> Vec a (Plus n m)
>         (bound at VecTest.hs:25:1)
>     In the third argument of ‘gfold’, namely ‘ys’
>     In the expression: gfold p f ys xs

Is this kind of type-level programming just not yet possible in GHC?
Or am I simply doing it wrong?

Cheers,

Christiaan