有类型约束的类型被称为什么？

Question

例如，Num a => a。

我认为它们只是被称为“受限类型”，但Google搜索并没有找到许多使用该术语的内容，因此我很想知道它们是否有其他名称。

- Laurence Gonsalves

---

我不太了解 Haskell，但您是在说可枚举类型吗？ - Simon Forsberg

@SimonAndréForsberg 不是的。你为什么会想到枚举类型？他在谈论 Java 中的 <T extends Foobar> 这样的类型约束。 - sepp2k

@sepp2k 我理解为“带有类型约束的类型”是指“只允许具有特定值之一的类型”。感谢您提供Java示例，那是我喜欢的编程语言 ;) - Simon Forsberg

我认为“haskell”标签足以表明我谈论的是Haskell而不是Java。 :-) - Laurence Gonsalves

@LaurenceGonsalves 这不准确。Java中的泛型 确实 像Haskell中的多态。如果你有一个带有 <T extends Number> 的泛型Java方法，并且它的返回类型是 T，那么该方法可以返回每种类型的Number，而不仅仅是某种类型的Number（你可以通过调用 myMethod<Integer> 或 myMethod<Float> 来明确要求某种类型的Number）。当然，除非它还接受至少一个类型为T的参数，否则不可能定义任何有用的方法（指不仅仅是返回null的方法）。 - sepp2k

Answer 1

具有此类限制的类型称为“合格类型”，而该特性有时称为“合格多态”。我相信这个术语最初是由马克·琼斯（Mark Jones）在他的ESOP '92论文中介绍的。

不应将合格类型与更主流的“有界多态”概念混淆，在像Java这样的语言中，它是泛型的基础。有界多态本质上是参数化多态和子类型的（相当复杂的）组合，而合格类型可以在没有子类型的情况下正常工作。

- Andreas Rossberg

Answer 2

我虽然不是类型理论专家，但经过一些研究，这就是我找到的内容（可能有帮助，也可能没有，但我无法在评论中输入这么多）。 Haskell简明教程：类称Num a部分为该类型的上下文：

约束类型a必须是类Eq的一个实例，即写作Eq a。因此，Eq a不是一种类型表达式，而是对类型的限制，并称为上下文。

所以我想你可以说“一个具有上下文的类型”，或者像你提到的“受限类型”。

还有一个地方可以查看类型类最早被描述的地方（我相信）是Haskell：如何让自适应多态性更不那么自适应 [postscript]。

类型类似乎与面向对象编程中出现的问题、类型的有界量化以及抽象数据类型[CW85，MP85，Rey85]密切相关。下面概述了其中一些联系，但需要进行更多的工作，以充分理解这些关系。

这篇论文是在1988年写的，所以我不确定这些关系是否现在已经完全理解了，但维基百科页面有界量化没有提到Haskell，所以我不确定它是否完全相同。（再次声明，我不是类型理论专家，只是喜欢Haskell的人）

另外，关于类型square :: Num a => a -> a，它说：

这被读作“square的类型为a -> a，对于每个a，使得a属于类Num（即在a上定义了(+)、(*)和negate）。”

你可以说该类型“属于一个类”。

这就是我找到的所有内容。个人认为，“受限类型”或“限制为某一类的类型”都可以。

- Adam Wagner

---

关于面向对象编程(OOP)和有界量化的关系：https://dev59.com/c3E85IYBdhLWcg3wkkjK - Heatsink

Answer 3

Num a =>部分被称为约束条件，可以理解为“如果Num a为真，则...”。通常情况下，约束条件和量词是一起讨论的。任何有约束条件的类型都可以转换为一个等效的类型，其中约束条件只出现在forall或exists量词的内部。因此，你不会经常听到“有约束条件的类型”，而是会经常听到“有约束参数多态性”（forall a. C => T）、“有约束存在类型”（exists a. C => T）或“有约束多态性”（这两种量词）。相关术语是“有界多态性”。有界多态性通常指约束多态性，其中约束是子类型或超类型约束。但是，在具有子类型的语言（如Java或Scala）中，这种区别并没有严格遵循。你经常会听到任何类型的约束都被称为“边界”。

- Heatsink

---

当我询问ghci 5 的类型时，它会显示 5 :: (Num t) => t。你是说这实际上是一个 forall 还是 exists？如果是这样，那么是哪一个？ - Laurence Gonsalves

@LaurenceGonsalves 那个类型是forall t。 （Num t）=> t。 类型中的自由变量隐式地量化为forall。 没有“exists”关键字; 存在类型仅与数据构造函数结合使用。 - Heatsink

Answer 4

"合格类型"。参见Mark P. Jones的合格类型：理论与实践。剑桥大学出版社，1994年。

在谷歌上有许多相关的匹配结果。

- Stefan Holdermans

Answer 5

你可以称之为“有界多态类型”（参见wikipedia）。

- phipsgabler

---

该页面上的“仅限于特定类型的子类型范围内的普遍或存在量词”这一短语让我感到怀疑。尽管 Haskell 类型类似乎与 Java 中的接口非常相似，但我认为它们提供的内容并不构成“子类型”。如果它们是子类型，那么这意味着类型系统违反了 LSP。例如，Monad 的 >>= 方法和 Eq 的 == 方法都有使用其实例中“更具体”的参数的方法。 - Laurence Gonsalves

我同意，Haskell确实没有子类型（这个术语实际上是用来描述子类型的）。不过，如果你将其视为字面意义上的“有界量化”，它看起来对我来说很相似：forall a. a<:T => ...只是量词中一种谓词，类似于 forall a. N(a) => …（在这里是在谓词逻辑中思考）。也许更好的表达应该是“类约束的多态类型”。但在这里，我认为简单的“约束类型”更为简单明了。 - phipsgabler