In Conor’s keynote talk at ICFP 2012, he uses a generic list like thing in Agda, which generalizes over regular lists, length indexed lists, and even more complicated things. It is done by indexing the data structure with relations of kind (A -> A -> *) rather than just a value. With the help of GHC’s newest super hot datatype promotion and kind polymorphism this already type checks!!! (I checked this in GHC 7.4.1 but it should work in GHC 7.6.x as well.)

{-# LANGUAGE KindSignatures, GADTs, DataKinds, PolyKinds #-}

– list like thing in Conor’s talk into Haskell!

data List x i j where
Nil  :: List x i i
Cons :: x i j -> List x j k -> List x i k

append :: List x i j -> List x j k -> List x i k
append Nil         ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

– instantiating to a length indexed list

data Nat = Z | S Nat

data VecR a i j where MkVecR :: a -> VecR a (’S i) i

type Vec a n = List (VecR a) n ‘Z

vNil :: Vec a 'Z;
vNil = Nil

vCons :: a -> Vec a n -> Vec a (’S n)
vCons = Cons . MkVecR

– instantiating to a plain list

data R a i j where MkR :: a -> R a ’() ’()

type PlainList a = List (R a) ’() ’()

nil :: PlainList a
nil = Nil

cons :: a -> PlainList a -> PlainList a
cons = Cons . MkR

You can go on and define Inst datatype for instructions. However, in GHC 7.4.1, you cannot write the compile function that compiles expressions to instructions because Haskell does not have stratified universes. GHC 7.4.1 will give you an error that says BOX is not *. I heard that *:* will be added go GHC at one point, so, it may work in more recent versions.

{-# LANGUAGE KindSignatures, GADTs, DataKinds, PolyKinds #-}
{-# LANGUAGE TypeOperators #-}

data Ty = I | B

data Val t where
IV :: Int -> Val I
BV :: Bool -> Val B

plusV :: Val I -> Val I -> Val I
plusV (IV n) (IV m) = IV (n + m)

ifV :: Val B -> Val t -> Val t -> Val t
ifV (BV b) v1 v2 = if b then v1 else v2

data Expr t where
VAL :: Val t -> Expr t
PLUS :: Expr I -> Expr I -> Expr I
IF :: Expr B -> Expr t -> Expr t -> Expr t

eval :: Expr t -> Val t
eval (VAL v) = v
eval (PLUS e1 e2) = plusV (eval e1) (eval e2)
eval (IF e e1 e2) = ifV (eval e) (eval e1) (eval e2)

data Inst :: [Ty] -> [Ty] -> * where
PUSH  :: Val t -> Inst ts (t ’: ts)
ADD   :: Inst ('I ’: 'I ’: ts) ('I ’: ts)
IFPOP :: GList Inst ts ts’ -> GList Inst ts ts’ -> Inst ('B ’: ts) ts’

compile :: Expr t -> GList Inst ts (t ’: ts)
compile (VAL v) = undefined – Cons (PUSH v) Nil
– I am stuck here
{- GListLike.hs:32:19:
-     Couldn’t match kind BOX’ against *’
-     Kind incompatibility when matching types:
-       k0 :: BOX
-       [Ty] :: *
-     In the return type of a call of `Cons’
-     In the expression: Cons (PUSH v) Nil
-}

It turns out that this Conor’s example is a very nice example that highlights the differences between GHC’s datatype promotion and the Nax language approach (or System Fi, which I posted earlier). I’ll try to explain the difference in the IFL 2012 post-proceeding, but in a nutshell, System Fi needs neither *:* (which causes logical inconsistency) nor stratified universes to express Conor’s example of the stack-shape indexed compiler. (Or, we may say that Fi typing context split into two parts somehow encode certain uses of stratified universes) Anyway, I see no problem of writing that code in Nax.

However, we do not have polymorphism at kind level in System Fi, so we cannot express GList, but only specific instances of GList instantiated to some specific x. I do have some rough thoughts that HM-style polymorphism at kind level won’t cause logical inconsistencies, but haven’t worked out the details.