[Haskell-cafe] Dependently typed fold in GHC/Haskell
Richard Eisenberg
eir at cis.upenn.edu
Wed Nov 19 14:59:51 UTC 2014
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
>
More information about the Haskell-Cafe
mailing list