haskell - 为什么名称形成一种而不只是一种类型？

Question

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

Answer 1

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

例如在 Haskell 中，唱片公司是：

• 值（访问器函数）
• 这些值具有类型（例如Record -> Int）
• 这些类型有种类 ( *)

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

通过将标签放在单独的种类中，类型检查器可以对它们进行特殊处理，例如自动镜头的特殊规则，或与记录构造（可能是整体）有关的证明，而不是通用功能。

在 Haskell 中使用种类系统的一个例子是使用“未装箱类型”。这些类型具有：

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

为了防止未装箱的类型与常规类型混合，它们被赋予了不同的kind，这允许编译器跟踪它们的分离。

因此，唱片标签名称没有什么神奇之处，这意味着您必须使用不同的类型来表示它们——这只是语言设计者可以做出的选择——并且使用依赖类型的语言，例如 Ur 或 Twelf，可以是一个有用的区别。

Answer 2

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