使用 DataKind 在类型签名中绑定名称

所以，我终于找到了一个可以利用新功能的任务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 http://haskell.1045720.n5.nabble.com/Data-Kinds-and-superfluous-in-my-opinion-constraints-contexts-td5689436.html:

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尚未得到很好的记录，并且似乎假设每个使用它的人都具有深厚的类型理论知识。

Haskell 与 Agda 不同，它没有依赖类型，因此无法完全满足您的需求。类型不能按值参数化，因为 Haskell 强制执行运行时和编译时之间的阶段区别。道路DataKinds从概念上讲，工作实际上非常简单：数据类型是promoted到种类（类型的类型）并且数据构造函数被提升为类型。

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

有几个问题：(ls :: [a])并没有真正意义（至少当你只是通过提升来伪造依赖类型时），并且length是类型变量而不是类型函数。你想说的是

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

where ???是列表的长度。问题是你无法在编译时获取列表的长度......所以我们可以尝试

 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)