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

Question

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

Answer 1

记录系统定义值,类型和(可能)种类的规则.使用的规则取决于所设计的类型系统以及设计者希望实现的目标.

例如,在Haskell中,记录标签是:

• 值(访问者函数)
• 那些值有类型(例如Record -> Int)
• 那些类型有种类(*)

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

通过将标签单独放置,类型检查器可以对它们进行特殊处理,例如自动镜头的特殊规则,或者与记录构造(可能是整体)的证据不符合通用功能.

在Haskell中使用种类系统的一个例子是使用"未装箱的类型".这些类型具有:

• 不同的运行时表示形式到常规值
• 不同的绑定形式(例如,不能在堆上分配)

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

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

Answer 2

答案很简单:因为它们可以出现在类型中.因此,他们必须生活在类型级别(否则您将需要依赖类型).而且因为他们生活在类型级别,他们被分类.