scala - 类型论 : type kinds

Question

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

简单类型:*

类型构造函数:* → *

最新 GHC 语言扩展 ConstraintKinds添加了一种新类型:

类型参数约束:Constraint

同样在阅读后this mailing list很明显，可能存在另一种类型，但 GHC 不支持(但这种支持在 .NET 中实现):

未装箱类型:#

我了解了 polymorphic kinds我想我理解这个想法。 Haskell 还支持显式类型量化。

所以我的问题是:

是否存在任何其他类型的种类？

还有其他与种类相关的语言功能吗？

subkinding 是什么意思意思是？它在哪里实现/有用？

kinds 之上是否有类型系统？ ，如 kinds是 types 之上的类型系统? (只是感兴趣)

Answer 1

是的，还有其他种类。页面Intermediate Types描述了 GHC 中使用的其他类型(包括未装箱类型和一些更复杂的类型)。 Ωmega 语言将更高种类的类型扩展到最大的逻辑扩展，允许用户定义种类(和排序，以及更高)。 This page为 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)

这将允许类型检查器在其接受的内容方面更具辨别力，并使类型级编程更具表现力。