Binding name in type signature using DataKind
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)
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.