Связывание имени в сигнатуре типа с использованием DataKind

Question

Итак, я, наконец, нашел задачу, где я мог бы использовать расширение DataKinds (используя ghc 7.4.1). Вот Vec я использую:

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 

Теперь, для удобства я хотел реализовать fromList. В принципе нет проблем с простой рекурсией/сгибом - но я не могу понять, как дать ему правильный тип. Для справки, это версия Agda:

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

Мой Haskell подход, используя синтаксис я видел here:

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

Это дает мне parse error on input 'a'. Является ли синтаксис, который я нашел, даже правильно, или они изменили его? Я также добавил несколько расширений, которые находятся в коде в ссылке, что тоже не помогло (в настоящее время у меня есть GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, UndecidableInstances).

Моя другая подозрение в том, что я просто не могу связать полиморфные типы, но мой тест для этого:

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

не удалось, тоже с Kind mis-match Expected kind 'ArgKind', but 'n' has kind 'Nat' (на самом деле не знаю, что это значит).

Может ли кто-нибудь помочь мне с рабочей версией fromList, а также прояснить другие вопросы? К сожалению, DataKinds еще не задокументирован очень хорошо, и, похоже, предполагается, что все, кто использует его, обладают глубокими знаниями теории типов.

Answer 1

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) 

Answer 2

Вы можете использовать некоторые класса типов магии здесь (см 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 

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