我读了很多关于类型类型、高级类型等的有趣的东西。默认情况下，Haskell支持两种类型:
- 简单类型:
* - 类型构造器:
* → *
最新的GHC语言扩展constrainttypes增加了一个新的类型:
- 类型参数约束:
Constraint
同样，在阅读了这个邮件列表之后，很清楚可能存在另一种类型的kind，但它不被GHC支持(但这种支持在。net中实现了):
- 未装箱类型:
#
我学过多态种类，我想我理解这个想法。Haskell还支持显式类型的量化。
我的问题是:
- 还有其他种类吗?
- 是否有其他类型相关的语言功能?
-
subkinding代表什么?它在哪里实现/有用? - 是否有一个类型系统在
kinds之上，像kinds是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)
这将允许类型检查器在它接受的内容上更有区别，并使类型级编程更具表现力。
正如类型被分类为种类，种类被分类为排序。
Ωmega编程语言有一种系统，在任何级别都有用户可定义的类型。(维基百科也是这么说的。我认为它指的是以上的分类和级别，但我不确定。
有人建议将类型提升到类型级别，将值提升到类型级别。但我不知道这是否已经实现(或者是否会达到"黄金时间")
考虑以下代码:
data Z
data S a
data Vec (a :: *) (b :: *) where
VNil :: Vec Z a
VCons :: a -> Vec l a -> Vec (S l) a
这是一个Vector，它的维数编码在该类型中。我们用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的演讲
GHC中的类型化类型级函数式编程