类型理论:类型类型

Question

我读过很多关于类型、高级类型等有趣的东西。默认情况下，Haskell支持两种类型：

• 简单类型：*
• 类型构造函数：* → *

最新的GHC语言扩展ConstraintKinds增加了一种新的类型：

• 类型参数约束：Constraint

另外，在阅读了这个邮寄名单之后，可以清楚地看到另一种类型的存在，但是GHC不支持它(但是这种支持是在.NET中实现的)：

• 未装箱类型：#

我已经了解了多态种类，我想我理解这个想法。此外，Haskell支持显式的量化。

所以我的问题是：

• 还有其他类型的吗？
• 还有其他与语言有关的功能吗？
• subkinding是什么意思？它在哪里实现/有用？
• 在kinds之上是否有一个类型系统，就像kinds是types之上的一个类型系统一样？(只是感兴趣)

Answer 1

是的，还有其他种类的。页面中间类型描述了在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)

这将允许类型检查器在其接受的内容上具有更多的区分性，并使类型级别的编程更具表现力。

Answer 2

就像类型按种类分类一样，种类也按种类分类。

Ω超级程序设计语言有一个在任何级别上都可以定义用户类型的系统。(它的wiki是这样说的。我认为它指的是上面的种类和级别，但我不确定。)

Answer 3

有人建议将类型提升到类别级别，将值提升到类型级别。但我不知道这是否已经实施(或者它是否会达到“黄金时段”)

考虑以下代码：

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是另一种，生活在与*相同的水平上。

以下是布伦特·约尔盖的演讲

GHC中的类型化类型级函数编程