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)

Answer 2

You can use some typeclass magic here (see HList for more):

{-# LANGUAGE GADTs, KindSignatures, DataKinds, FlexibleInstances
  , NoMonomorphismRestriction, FlexibleContexts #-}

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

instance Show (Vec Z a) where
  show Nil = "."

instance (Show a, Show (Vec m a)) => Show (Vec (S m) a) where
  show (Cons x xs) = show x ++ " " ++ show xs

class FromList m where
  fromList :: [a] -> Vec m a

instance FromList Z where
  fromList [] = Nil

instance FromList n => FromList (S n) where
  fromList (x:xs) = Cons x $ fromList xs

t5 = fromList [1, 2, 3, 4, 5]

but this not realy solve the problem:

> :t t5
t5 :: (Num a, FromList m) => Vec m a

Lists are formed at runtime, their length is not known at compile time, so the compiler can't infer the type for t5, it must be specified explicitly:

*Main> t5

<interactive>:99:1:
    Ambiguous type variable `m0' in the constraint:
      (FromList m0) arising from a use of `t5'
    Probable fix: add a type signature that fixes these type variable(s)
    In the expression: t5
    In an equation for `it': it = t5
*Main> t5 :: Vec 'Z Int
*** Exception: /tmp/d.hs:20:3-19: Non-exhaustive patterns in function fromList

*Main> t5 :: Vec ('S ('S ('S 'Z))) Int
1 2 3 *** Exception: /tmp/d.hs:20:3-19: Non-exhaustive patterns in function fromList

*Main> t5 :: Vec ('S ('S ('S ('S ('S 'Z))))) Int
1 2 3 4 5 .
*Main> t5 :: Vec ('S ('S ('S ('S ('S ('S ('S 'Z))))))) Int
1 2 3 4 5 *** Exception: /tmp/d.hs:23:3-40: Non-exhaustive patterns in function fromList

Languages ​​with dependent types have maps from terms to types, types can be formed dynamically at runtime too, so this problem does not exist.

Answer 3

On top of the previous answers :

• value level, from [a] to exist n. Vec n a

• value to typed value, from [a] to Vec 5 a, where you have to provide a specific n.

A variant of the 1st transform, goes like

reify :: [a] -> (forall (n::Nat). Proxy n -> Vec n a -> w) -> w
reify [] k = k (Proxy @ 'Z) Nil
reify (x:xs) k = reify xs (\(_ :: Proxy n) v -> k (Proxy @ ('S n)) (Cons x v))

It still goes from a value [a] to a typed value Vec n a in which n is (statically) quantified. This is similar to the VecAnyLength approach, without introducing an actual datatype to perform quantification.

The proxy here is to explicit the n as a Nat. it can be removed from the code and n left silent, appearing only in the type Vec n a, and not provided to the values constructed, as it is in Proxy @ ('S n).