Most part of Conor's talk at ICFP, until just before the last stage
where he heavily uses true value dependency for compiler correctness all
the code seemed to be able to translate into Haskell with the new hot
DataKinds and PolyKinds extension.
I tried it in GHC 7.4.1 and it was possible to do it, but I got stuck
and I had to make the generic list structure mono-kinded with kind
signatures rather not use the PolyKinds extension.
I wonder if this is just a but of GHC 7.4.1's implementation of
PolyKinds, or a limitation of the DataKind design.
I attached a literate Haskell script with this message that illustrates
this problem.
Thanks in advance for any comments including whether it runs in later
versions or still has problems, and discussions about the DataKinds and
PolyKinds extension.
Ki Yung
I ran into problems when I tryed doing some of
the Conor's talk at ICFP 2012 in Haskell with
DataKinds and PolyKinds extension, using GHC 7.4.1.
I am wondering whether this is a bug in GHC 7.4.1
(maybe fixed in GHC 7.6.x? haven't tried since
I haven't installed 7.6.x yet), or a limitation of
datatype promotion itself. The problem happens when
I try to use promoted list datatype.
Here is a code that illustrates this problem:
> {-# LANGUAGE GADTs, DataKinds, PolyKinds, KindSignatures #-}
>
> data GList x i j where
> GNil :: GList x i i
> GCons :: x i j -> GList x j k
> -> GList x i k
>
>
> append :: GList x i j -> GList x j k
> -> GList x i k
> append GNil ys = ys
> append ( GCons x xs) ys =
> GCons x (append xs ys)
Instantiating to a plain regular list works
> data Elem a i j where
> MkElem :: a -> Elem a () ()
>
> type List' a = GList (Elem a) () ()
>
> nil' = GNil {-"~"-} :: List' a
>
> cons' :: a -> List' a -> List' a
> cons' = GCons . MkElem
Instantiating to a length indexed list works
> data Nat = Z | S Nat
>
> data ElemV a i j where
> MkElemV :: a -> ElemV a (S n) n
>
> type Vec a n = GList (ElemV a) n Z
>
> vNil = GNil {-"~"-} :: Vec a Z
>
> vCons :: a -> Vec a n -> Vec a (S n)
> vCons = GCons . MkElemV
Good, then let's do some more things with DataKinds.
Promoting Bool works as well as Nat.
> data RelB :: Bool -> Bool -> * where
> MkRelB :: RelB b b
>
> l1 = GCons MkRelB GNil
But, I have some problems with promoting [Bool] !!!
> data RelBL :: [Bool] -> [Bool] -> * where
> MkRelBL :: RelBL bs bs
I can only with mono-kinded list structure.
Below is a momomorphization of GList.
> data MyList (x :: [Bool] -> [Bool] -> *) i j where
> MyNil :: MyList x i i
> MyCons :: x i j -> MyList x j k
> -> MyList x i k
>
> l3 = MyCons MkRelBL MyNil
However when I try to do this with the poly-kinded GList,
I get a kind error. Is this a bug of GHC 7.4.1 or is this
a limitation of DataKind extension?
> l4 = GCons MkRelBL GNil
tmp.lhs:74:22:
Couldn't match kind `BOX' against `*'
Kind incompatibility when matching types:
k0 :: BOX
[Bool] :: *
In the second argument of `GCons', namely `GNil'
In the expression: GCons MkRelBL GNil
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
