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

19 Nov 2014


      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

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

Christiaan Baaij