Имя привязки в подписи типа с использованием DataKind

Haskell, в отличие от Agda, не имеет зависимых типов, поэтому нет возможности сделать именно то, что вы хотите. Типы нельзя параметризовать по значению, так как Haskell применяет фазовое различие между временем выполнения и временем компиляции. Концептуально DataKinds работает на самом деле очень просто: типы данных повышаются до видов (типов типов), а конструкторы данных повышаются до типов.

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

имеет пару проблем: (ls :: [a]) на самом деле не имеет смысла (по крайней мере, когда вы только подделываете зависимые типы с продвижением), а length — это переменная типа, а не функция типа. То, что вы хотите сказать, это

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

где ??? — длина списка. Проблема в том, что у вас нет возможности получить длину списка во время компиляции... поэтому мы можем попробовать

 fromList :: [a] -> Vec len a

но это неправильно, так как там написано, что fromList может возвращать список любой длины. Вместо этого мы хотим сказать

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

но Haskell не поддерживает это. Вместо

 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)

вы можете фактически использовать VecAnyLength путем сопоставления с образцом и, таким образом, получить (локально) псевдозависимое типизированное значение.

по аналогии,

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

не работает, потому что функции Haskell могут принимать аргументы только вида *. Вместо этого вы можете попробовать

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

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

что даже можно определить

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

Здесь вы можете использовать магию классов типов (дополнительную информацию см. в HList):

{-# 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]

но это не решает проблему:

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

Списки формируются во время выполнения, их длина неизвестна во время компиляции, поэтому компилятор не может вывести тип для t5, его нужно указать явно:

*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

Языки с зависимыми типами имеют карты из терминов в типы, типы могут формироваться динамически и во время выполнения, так что этой проблемы не существует.

В дополнение к предыдущим ответам:

• уровень стоимости, от [a] до exist n. Vec n a

• значение в типизированное значение, от [a] до Vec 5 a, где вы должны указать конкретное n.

Вариант 1-го преобразования выглядит так

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

Он по-прежнему переходит от значения [a] к типизированному значению Vec n a, в котором n определяется (статически) количественно. Это похоже на подход VecAnyLength, но без введения фактического типа данных для выполнения количественного определения.

Здесь proxy указывает на n как на Nat. его можно удалить из кода и оставить n безмолвным, появляющимся только в типе Vec n a и не предоставляемым для сконструированных значений, как в Proxy @ ('S n).