类型理论：类型种类

Question

我读到了很多关于类型种类、高阶类型等有趣的内容。Haskell默认支持两种种类：

• 简单类型：*
• 类型构造器：* → *

最新的GHC语言扩展ConstraintKinds添加了一个新的种类：

• 类型参数约束：Constraint

另外，在阅读这个邮件列表之后，可以明确另一种种类可能存在，但它在GHC中不被支持（但在.NET中实现了这种支持）：

• 非装箱类型：#

我学习了多态种类，并且我认为我理解了这个想法。此外，Haskell还支持显式种类量化。

所以我的问题是：

• 是否存在其他种类类型？
• 是否存在其他与种类相关的语言特性？
• 子种类(subkinding)是什么意思？它在哪里实现/有用？
• 是否存在基于种类(kinds)的类型系统，就像种类(kinds)是基于类型(types)的类型系统一样？（只是出于兴趣）

- controlflow

Answer 1

是的，还有其他类型存在。页面Intermediate Types描述了GHC中使用的其他种类（包括非装箱类型和一些更复杂的种类）。Ωmega语言将高阶类型推到了最大的逻辑扩展，允许用户定义种类（和排序和更高级别的类型）。这个页面提出了一个GHC种类系统扩展，它将允许在Haskell中定义用户可定义的种类，并且提供了为什么它们很有用的很好的例子。

假设您想要一个具有列表长度类型级注释的列表类型，就像这样：

data Zero
data Succ n

data List :: * -> * -> * where
  Nil   :: List a Zero
  Cons  :: a -> List a n -> List a (Succ n)

目的是让最后一个类型参数只能是 Zero 或者 Succ n，其中 n 再次只能是 Zero 或者 Succ n。简而言之，您需要引入一个名为 Nat 的新类别，它仅包含两种类型： Zero 和 Succ n。然后，List 数据类型可以表达最后一个参数不是 *，而是 Nat 的形式，例如：

data List :: * -> Nat -> * where
  Nil   :: List a Zero
  Cons  :: a -> List a n -> List a (Succ n)

这将使类型检查器在接受内容方面更加具有区分性，同时使类型级别的编程更加表达力。

- John L

Answer 2

有人提议将类型提升到种类级别，将值提升到类型级别。但我不知道这是否已经实现了（或者它是否会达到“主流时间”）。

考虑以下代码：

data Z
data S a 

data Vec (a :: *) (b :: *) where
  VNil  :: Vec Z a 
  VCons :: a -> Vec l a -> Vec (S l) a 

这是一个向量，其维数编码在类型中。我们使用Z和S来生成自然数。这很好，但当生成Vec时，我们无法进行“类型检查”，以确保我们使用了正确的类型（我们可能会意外地切换长度和内容类型），并且我们还需要生成类型S和Z，如果我们已经定义了自然数，则这是不方便的：

data Nat = Z | S Nat

使用这个提议，你可以写出下面这样的代码：

data Nat = Z | S Nat

data Vec (a :: Nat) (b :: *) where                                              
  VNil  :: Vec Z a
  VCons :: a -> Vec l a -> Vec (S l) a

这将把Nat提升到类型的层次，如果需要，也可以将S和Z提升到类型的层次。因此，Nat是另一种类型，并且与*生活在同一个层次上。

这是Brent Yorgey的演示文稿。 Typed type-level functional programming in GHC

- raichoo

---

更新：ghc 7.4.1通过PolyKinds和DataKinds扩展支持此功能。 - raichoo

Answer 3

类别有种类，种类有分类。

Ωmega编程语言拥有一个在任何级别上用户可定义的种类系统。(这是它的维基页面说的，我认为它指的是种类和以上级别，但我不确定。)

- missingfaktor