haskell - 种类有什么用吗？

Question

在 Haskell 中，种类(类型的类型)允许一些有用的东西，例如类型构造函数。我的问题是，同时拥有各种种类(类型的类型的类型)是否有任何好处，或者他们能做的事情是否只有种类和类型才能轻松完成？

Answer 1

Ωmega一路向上。基本上就是claimed无限类型层次结构与适当的 GADT 一起与依赖类型一样强大。

此外，当尝试使用 DataKinds、PolyKinds 等内容时，我有时会因为类型构造函数未提升为类型构造函数或提升为类型构造函数而受到某种限制。种类不能受到限制(即没有种类类)。 Ωmega 似乎解决了很多这些限制——不幸的是，正如通常的情况一样，代价是成为一种更加学术的语言。但我仍然发现它比“真正的”依赖类型语言(如 Agda 和 Coq)更容易阅读(尽管至少 Agda does have 也是一种无限的层次结构)。也许这是因为 Ωmega 更适合 Haskell 思维方式。