haskell - 使用 DataKind 在类型签名中绑定(bind)名称

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

我的另一个怀疑是我无法绑定(bind)多态类型，但我对此进行了测试:

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)