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

[Andres Löh]

Hi.

You cannot partially apply a type family, as you try in

>> type family P (a :: *) (m :: Nat) (l :: Nat) :: * where
>>   P a m l = Vec a (Plus l m)

and then

>>     p :: Proxy (P a m)
>>     p = Proxy

(The error message for this is not very good.)

There are ways to work around this, for example with Richard's
singletons library:

> import Data.Proxy
> import Data.Singletons
> import Data.Singletons.Prelude

> gfold :: Proxy (p :: TyFun Nat * -> *)
>       -> (forall l . Proxy l -> a -> p $ l -> p $ S l)
>       -> p $ Z -> Vec a k -> p $ k
> gfold _ f z Nil       = z
> gfold p f z (x :> (xs :: Vec a l)) = f (Proxy :: Proxy l) x (gfold p f z xs)

> data P (a :: *) (m :: Nat) (f :: TyFun Nat *) :: *
> type instance Apply (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 (Proxy :: Proxy (P a m)) (const (:>)) ys xs

Rest as before.

Cheers,
  Andres