Binding name in type signature using DataKind

Question

So, I finally found a task where I could make use of the new DataKinds extension (using ghc 7.4.1). Here's the Vec I'm using:

data Nat = Z | S Nat deriving (Eq, Show)

data Vec :: Nat -> * -> * where
    Nil :: Vec Z a
    Cons :: a -> Vec n a -> Vec (S n) a

Now, for convenience I wanted to implement fromList. Basically no problem with simple recursion/fold -- but I can't figure out how to give it the correct type. For reference, this is the Agda version:

fromList : ∀ {a} {A : Set a} → (xs : List A) → Vec A (List.length xs)

My Haskell approach, using the syntax I saw here:

fromList :: (ls :: [a]) -> Vec (length ls) a
fromList [] = Nil 
fromList (x:xs) = Cons x (fromList xs)

This gives me a parse error on input 'a'. Is the syntax I found even correct, or have they changed it? I also added some more extensions which are in the code in the link, which didn't help either (currently I have GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, UndecidableInstances).

My other suspicion was that I just can't bind polymorphic types, but my test for this:

bla :: (n :: Nat) -> a -> Vec (S n) a
bla = undefined

failed, too, with Kind mis-match Expected kind 'ArgKind', but 'n' has kind 'Nat' (don't really know what that means).

Could anyone help me with a working version of fromList and also clarify the other issues? Unfortunately, DataKinds isn't documented very well yet and seems to assume that everybody using it has profound type theory knowledge.

Answer 1

Haskell, unlike Agda, does not have dependent types, so there is no way to do exactly what you want. Types cannot be parameterized by value, since Haskell enforces a phase distinction between runtime and compile time. The way DataKinds works conceptually is actually really simple: data types are promoted to kinds (types of types) and data constructors are promoted to types.

 fromList :: (ls :: [a]) -> Vec (length ls) a

has a couple of problems: (ls :: [a]) does not really make sense (at least when you are only faking dependent types with promotion), and length is a type variable instead of a type function. What you want to say is

 fromList :: [a] -> Vec ??? a

where ??? is the length of the list. The problem is that you have no way of getting the length of the list at compile time... so we might try

 fromList :: [a] -> Vec len a

but this is wrong, since it says that fromList can return a list of any length. Instead what we want to say is

 fromList :: exists len. [a] -> Vec len a

but Haskell does not support this. Instead

 data VecAnyLength a where
     VecAnyLength :: Vec len a -> VecAnyLength a 

 cons a (VecAnyLength v) = VecAnyLength (Cons a v)

 fromList :: [a] -> VecAnyLength a
 fromList []     = VecAnyLength Nil
 fromList (x:xs) = cons x (fromList xs)

you can actually use a VecAnyLength by pattern matching, and thus getting a (locally) psuedo-dependently typed value.

similarly,

bla :: (n :: Nat) -> a -> Vec (S n) a

does not work because Haskell functions can only take arguments of kind *. Instead you might try

data HNat :: Nat -> * where
   Zero :: HNat Z
   Succ :: HNat n -> HNat (S n)

bla :: HNat n -> a -> Ven (S n) a

which is even definable

bla Zero a     = Cons a Nil
bla (Succ n) a = Cons a (bla n a)