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, UndecidableInst…

Accepted Answer

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)
```

Binding name in type signature using DataKind

Solution

Problem