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-wi...) 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
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe