为什么名称形成一种而不仅仅是一种类型？

Question

前段时间在Haskell扩展中的一个（找不到链接）和recently in Ur我发现名称（例如，记录字段）形成一个Kind。有人可以解释为什么Type抽象对他们来说不够吗？

Answer 1

答案很简单：因为它们可以出现在类型中。因此，他们必须在类型级别上生活（否则你需要依赖类型）。而且因为他们生活在类型层面，所以他们被归类。

Answer 2

记录系统定义值，类型和（可能）种类的规则。使用什么规则取决于正在设计的类型系统，以及设计者希望达到的目标。

E.g.在Haskell，唱片公司有：

• 值（存取函数）
• 这些值有类型（例如Record -> Int）
• 这些类型有多种（*）

其他记录系统可以使用类型或种类系统用于不同的目的。

通过将标签放置在单独的种类中，类型检查器可以特别对待它们，并具有特殊的规则。自动镜头，或与记录构造（总体可能）做的证明不是真正的通用功能。

在Haskell中使用类系统的一个例子是使用“unboxed types”。这些都是有类型：

• 不同的运行时表示常规值
• 不同的结合形式（例如不能在堆上分配）

为了保持拆箱类型与使用常规混合类型，它们被赋予不同的种类，它允许编译器跟踪它们的分离。

因此，有关于唱片的名字没有什么神奇的，这意味着你必须使用一个不同的来表示它们 - 它只是一个选择一种语言设计者可以 - 在一个依赖性类型的语言，如乌尔或Twelf，这可以是一个有用的区别。