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

[Richard Eisenberg]

You were really close, but there was a big leap that you would have to take before this would work. The fundamental problem is that you tried to use the `P` type family only partially applied. GHC does not allow partially-applied type functions. It is a bug in GHC 7.8.3 that no clear error is reported when you try to do so -- it is better in previous and later versions. (Specifically, I'm looking at the use of `P` in the type signature for `p` within `gconcat`.)

I don't like this restriction, so co-author Jan Stolarek and I devised a workaround. The preliminary idea is explained in a blog post (http://typesandkinds.wordpress.com/2013/04/01/defunctionalization-for-the-win/) and the more developed idea in a paper (http://www.cis.upenn.edu/~eir/papers/2014/promotion/promotion.pdf). In short, we get around the restriction by using empty datatypes to represent type functions, and then we "apply" these datatypes using a `@@` open type family. The whole shebang is implemented in the `singletons` library.

So, I edited your code to allow unsaturated calls to `P` (that's the `genDefunSymbols` line, below) and fixed the kinds in `gfold` to allow for partially-applied type families (which, in my workaround, have a different kind than normal type families).

Then, I had to add a little more type-variable tracking in `gfold` to remove ambiguity. The binding and use of `n` appears in the Idris code, too. By using `proxy` instead of `Proxy`, I tell GHC that the proxy types should be the same. Idris doesn't need to know this because Idris uses higher-order unification, which is sometimes permitted to make guesses. GHC never makes guesses, so it needs a bit more information.

In any case, here you go:

> {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators, RankNTypes,
>             ScopedTypeVariables, TypeFamilies, TemplateHaskell #-}
> 
> import Data.Proxy
> import Data.Singletons.TH         ( genDefunSymbols )
> import Data.Singletons.Prelude    ( type (@@), TyFun )
> 
> 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 :: TyFun Nat * -> *) 
>      -> (forall l . Proxy l -> a -> p @@ l -> p @@ (S l))
>      -> p @@ Z -> Vec a k -> p @@ k
> gfold Proxy _ z Nil                    = z
> gfold proxy f z (x :> (xs :: Vec a n))
>   = f (Proxy :: Proxy n) x (gfold proxy f z xs)
> 
> type family P (a :: *) (m :: Nat) (l :: Nat) :: * where
>  P a m l = Vec a (Plus l m)
> 
> $(genDefunSymbols [''P])
> 
> 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 (PSym2 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
> 


You'll need singletons-1.0 or later.

That was fun! Thanks!

Richard

On Nov 19, 2014, at 7:40 AM, Christiaan Baaij <christiaan.baaij at gmail.com> wrote:

> 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 mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>