我正在查看https://wiki.haskell.org/GHC/Kinds我发现了这个：
data Nat = Zero | Succ Nat
data Vector :: * -> Nat -> * where
VNil :: Vector a Zero
VCons :: a -> Vector a n -> Vector a (Succ n)
我尝试查看whereHaskell 中的作用，但找不到有关它的信息data。我知道什么是种类。不带参数的构造函数具有 kind *，而带一个参数的构造函数具有 kind * -> *，它是构造函数的“类型”。我认为它定义了一种Vector存在* -> Nat -> *，这意味着可以接受任何东西，一个自然数并返回一个Vector？
更重要的是：为什么有人会用这个东西？
语法data ... where ...是GADT语法。（您正在查看的 wiki 也有一个关于 GADT 的页面，从您正在阅读的页面链接）
GADT 语法通过语言扩展启用GADTs。它为您提供了标准数据声明语法的替代方案，其中不是列出数据构造函数，就好像它们应用于其字段的类型一样（从而隐式定义构造函数的整体类型），而是为每个构造函数。
例如，标准Maybe类型在传统语法中是这样定义的：
-- Maybe type constructor takes an argument a;\n-- all data constructors implicitly return Maybe a\ndata Maybe a\n = Just a -- Just data constructor takes an argument **of type** a, not a itself\n | Nothing -- Nothing data constructor takes no arguments\nGADT 语法如下：
\n-- Maybe type constructor takes an argument a\ndata Maybe a where\n Just :: a -> Maybe a -- Just takes an argument of type a to return a Maybe a\n Nothing :: Maybe a -- Nothing is simply of type Maybe a\n这种语法更加冗长。在复杂的情况下，它可以说更清晰，因为我们用普通类型表达式语法显式地编写构造函数的类型，而不是用奇怪的专用语法来定义它们，在这种语法中，我们将术语级数据构造函数伪应用到它们的类型论据。
\n但更重要的是，GADT 语法1为原始语法无法表达的新功能打开了大门。这就是你的例子中发生的情况。
\n主要的新功能来自对每个构造函数的返回类型的控制。如果我们想尝试Vector使用传统的数据语法进行定义，我们将不得不这样做：
data Vector a n\n = VNil\n | VCons a (Vector a n)\n该n参数应该表示向量在类型级别的元素数量。这个想法是这样的，我们可以做一些事情，比如将两个向量压缩在一起，并让编译器强制这两个向量具有相同的长度，而不是像Data.List.zip它简单地放弃并在另一个列表运行时默默地丢弃一个列表中的任何剩余元素之类的事情出元素。
但我们上面写的不能做到这一点。VNil始终返回类型为 的值Vector a n，并且它没有任何类型n( 或a) 的字段，因此 any可以与任何类型参数一起VNil使用；不会说明向量的大小！类似地，有一个包含 a 的字段，但当我们希望它指示大小比尾向量的大小大一时，最终也会构造一个类型为 的值，其中参数相同尺寸。nnVConsVector a nVector a nn
GADT 语法允许我们解决这些问题：
\n{-# LANGUAGE GADTs #-}\n\ndata Vector a n where\n VNil :: Vector a Zero\n VCons :: a -> Vector a n -> Vector a (Succ n)\n现在我们可以明确地说VNil构造函数是一个大小为 的向量Zero；它不像Nothing :: Maybe a该类型变量中总是多态的。（当然，我们的VNil类型变量仍然是多态的a，因为没有元素意味着我们不应该限制元素类型）。并VCons使用 ana和 aVector a n来生成Vector a (Succ n)2；特别是一个比其内部向量“大一项”的向量。
但我们错过了一步，这一步实际上是定义性的Zero，而且Succ是任何地方的。做到这一点的方法很简单：
data Nat = Zero | Succ Nat\n这表示：自然数2要么是Zero，要么是Succ其他 的Nat。我们可以重复模式匹配 a Nat，最终会命中3Zero；如果我们想将其转换为“正常”数字，我们会这样做并计算Succ构造函数。
但这只给了我们Zero和Succ作为数据构造者。我们想在我们的和类型中使用它们。为此，我们需要另一个扩展：. 它只允许使用任何声明来定义（类型级别）类型构造函数及其关联的（术语级别）数据构造函数，并定义（种类级别）“种类构造函数”及其关联的类型构造函数（在Turn 不包含术语级别的任何值；它们纯粹用于类型操作）。VNilVConsDataKindsdata
请注意，您正在查看的 wiki 页面似乎描述了一个尚未实现的语言扩展Kinds，称为 ，它显然与现在的相同DataKinds。因此，该 wiki 页面非常旧，因此您可能应该忽略它。如果您正在寻找有关一般类型（而不是DataKinds特定的扩展）的阅读材料，您可能需要继续搜索。
但是使用DataKinds我们可以做到这一点（实际上现在可以编译）：
{-# LANGUAGE GADTs, DataKinds #-}\n\ndata Nat = Zero | Succ Nat\n\ndata Vector a n where\n VNil :: Vector a Zero\n VCons :: a -> Vector a n -> Vector a (Succ n)\n这里我们正常定义Nat（在类型级别）和Zero& （在术语级别）。但是在我们使用andSucc的定义中，是在类型级别。这足以让 GHC 推断出该类型必须是类型（因为它与该类型的类型构造函数一起使用）。但我们还可以使用另一个扩展，并且更明确地了解类型构造函数的类型，如下所示：VectorZeroSuccVector a nnNatKindSignaturesVector
{-# LANGUAGE GADTs, DataKinds, KindSignatures #-}\n\ndata Nat = Zero | Succ Nat\n\ndata Vector :: * -> Nat -> * where -- this line is where the difference is\n VNil :: Vector a Zero\n VCons :: a -> Vector a n -> Vector a (Succ n)\n在我们只是说data Vector a n并相信编译器和读者从下面的用法中找出必须a是种类的*（它被用作VCons构造函数中实际值的类型）并且n是种类的Nat（因为该位置在Vector类型构造函数中由类型级别填充Zero，并且Succ n在构造函数中）。现在我们可以通过 ; 明确地向编译器和读者提供更多信息data Vector :: * -> Nat -> *。Vector接受一个 kind 的类型参数*，另一个 kind 的类型参数Nat，并产生一个 kind 的类型*（这意味着它是一个实际上可以在术语级别具有值的类型）。
DataKinds标记 likeZero是指术语级别Zero（属于 type Nat，属于 kind *）还是类型级别Zero（属于 kind ）可能会有点令人困惑Nat。大多数时候，编译器可以完美地分辨哪个是哪个，因为它可以很好地跟踪给定的表达式是术语表达式还是类型表达式。但DataKinds给你一种更明确的方式；如果您在类型构造函数前面加上单引号（例如\'Zero），那么它明确意味着数据构造函数提升到类型级别。有些人认为始终使用这种显式标记是一种很好的风格。4
这几乎就是您的示例中发生的所有事情。
\n至于它的用途......在最基本的层面上，它允许您执行诸如跟踪列表5的长度之类的操作，然后让编译器强制多个列表具有相同的大小（或具有相同的大小）有一些特定的其他关系，例如更大，或更小，或两倍大等）。人们将这种功能用于大量我无法在一篇文章中总结的事情（不仅仅是事情的大小；有无数种方法可以在类型级别使用DataKinds和GADTs反映信息，以便编译器可以为您强制执行）；这有点像问“函数有什么用”。但这里有几个示例函数，它们使用类型级别长度做一些有趣的事情：
vzipWith :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n\nvzipWith _ VNil VNil = VNil\nvzipWith f (a `VCons` as) (b `VCons` bs)\n = f a b `VCons` vzipWith f as bs\n正如我之前提到的，强制向量的 zip 具有相同的长度。保证您不会出现错误，因为一个列表意外变短并且您只是忽略了另一个列表的元素，相反编译器会抱怨。这是vzipWithGHCI 的工作内容：
\xce\xbb vzipWith replicate (1 `VCons` (2 `VCons` VNil)) (\'a\' `VCons` (\'b\' `VCons` VNil))\nVCons "a" (VCons "bb" VNil)\nit :: Vector [Char] (\'Succ (\'Succ \'Zero))\n通过更多的工作，我们可以定义如何添加类型级别Nat（使用更多扩展，我不会在这里详细解释）。然后我们可以附加向量，同时跟踪组合长度：
type Plus :: Nat -> Nat -> Nat\ntype family Plus n m\n where Zero `Plus` n = n\n Succ n `Plus` m = Succ (n `Plus` m)\n\nvappend :: Vector a n -> Vector a m -> Vector a (n `Plus` m)\nvappend VNil ys = ys\nvappend (x `VCons` xs) ys = x `VCons` vappend xs ys\n而在工作中：
\n\xce\xbb vappend (1 `VCons` (2 `VCons` VNil)) (3 `VCons` (4 `VCons` (5 `VCons` VNil)))\nVCons 1 (VCons 2 (VCons 3 (VCons 4 (VCons 5 VNil))))\nit ::\n Num a => Vector a (\'Succ (\'Succ (\'Succ (\'Succ (\'Succ \'Zero)))))\n如果你想在 GHCI 中使用它，请将所有这些放入一个文件中并加载它：
\n{-# LANGUAGE DataKinds, GADTs, KindSignatures, StandaloneDeriving, TypeFamilies, TypeOperators, StandaloneKindSignatures #-}\n\ndata Nat = Zero | Succ Nat\n\ndata Vector :: * -> Nat -> * where\n VNil :: Vector a \'Zero\n VCons :: a -> Vector a n -> Vector a (\'Succ n)\n\nderiving instance Show a => Show (Vector a n)\n\n\nvzipWith :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n\nvzipWith _ VNil VNil = VNil\nvzipWith f (a `VCons` as) (b `VCons` bs)\n = f a b `VCons` vzipWith f as bs\n\n\ntype Plus :: Nat -> Nat -> Nat\ntype family Plus n m\n where Zero `Plus` n = n\n Succ n `Plus` m = Succ (n `Plus` m)\n\n\nvappend :: Vector a n -> Vector a m -> Vector a (n `Plus` m)\nvappend VNil ys = ys\nvappend (x `VCons` xs) ys = x `VCons` vappend xs ys\n在这里，我还添加了另一个扩展StandaloneDeriving，以便我们可以派生 的一个Show实例Vector，这样您就可以在解释器中进行操作，看看会得到什么。
1事实上，有一个扩展只GADTSyntax支持新语法，但不允许您定义任何在旧语法中无法定义的类型。据我所知，几乎没有人使用这个扩展；GADT 受到好评，任何愿意学习新语法的人都只会在学习 GADT 的背景下这样做，因此，如果他们喜欢新语法并希望在任何地方使用它，他们可能只是在任何地方启用它。GADTs
2 “Succ”是“继任者”的缩写。从第一原理定义自然数的标准方法是假设存在第一个自然数（零），并且对于任何自然数都有一个不同的自然数的后继（并且不是任何其他数字的后继） 。这是一种奇特的方式，表示您可以从零开始，然后从那里开始计数，直到您想要的为止。但是自然数的这种归纳结构恰好很好地映射到 Haskell 的类型逻辑中，使得使用以这种方式定义的数字在类型级别上对事物进行计数变得非常容易，这就是这里使用它的原因。
\n3除非它是无限的，这意味着我们“计算成功次数”的尝试将永远不会终止，这是 Haskell 中产生 Bottom/undefined 的另一种方式。
\n4在某些情况下，为了消除歧义，这种“tick”语法是必要的。例如，DataKinds我们可以拥有类型的类型级别列表，例如[Bool, Char, Maybe Integer]，因为我们可以将列表提升为在类型级别而不是术语级别进行操作。 [Bool, Char, Maybe Integer]是 kind 的类型级列表[*]（ kind 的事物列表*，即类型列表）。当我们考虑诸如 之类的事情时，问题就出现了[Bool]。这绝对是一个类型表达式，但它是应用于列表类型构造Bool函数（即布尔值列表的术语类型），还是单例类型列表（即列表数据构造函数:和[]，提升到类型级别），其单一值恰好是类型Bool？一个是善良*，另一个是善良[*]。没有办法通过观察来判断程序员的意图，因此DataKinds我们优先考虑 pre-DataKinds 解释；[Bool]绝对是布尔值列表的类型。我们可以使用勾号来显式选择其他解释：\'[Bool]是类型的单例列表。
5类型反映列表长度的列表传统上称为向量，以区别于类型不反映长度的普通列表。也许这并不理想，因为还有其他一些东西也被称为“向量”，以区别于普通列表。但这是既定的术语。
\n| 归档时间： |
|
| 查看次数： |
177 次 |
| 最近记录： |