具有类型约束的类型称为什么?

具有这种特定类型约束的类型称为 “合格类型” ,而特性本身有时是“限定多态性”。我相信这个术语最初是由 Mark Jones' ESOP '92 paper 。

限定类型不应与“有界多态性”这一更主流的概念混淆,Java等语言中的泛型就是基于这一概念。有界多态性本质上是参数多态性与分型的(相当复杂的)组合,而限定类型在没有分型的情况下也能共存。

“合格类型”。参见Mark P.Jones。 合格类型:理论与实践 .剑桥大学出版社,剑桥,1994年。

大量相关 matches on Google 。

我不是类型论专家,但经过一点研究,这就是我所发现的(这可能有帮助,也可能没有帮助,但我无法将其纳入评论中)。

A Gentle Introduction to Haskell: Classes 调用 Num a 部分类型的上下文:

类型a必须是类Eq的实例的约束是 因此,Eq a不是一个类型表达式,而是 表示对类型的约束,称为 上下文 。

所以我想你可以说“有上下文的类型”,或者正如你提到的“约束类型”。

另一个需要注意的地方是Haskell首先描述(我相信)类型类的地方: How to make ad-hoc polymorphism less ad-hoc [附言]。

类型类似乎与中出现的问题密切相关 面向对象编程,类型的有界量化,以及 抽象数据类型[CW85,MP85,Rey85]。有些连接是 概述如下,但需要做更多的工作来支持这些 关系充分。

这篇论文写于1988年,所以我不确定这些关系现在是否被完全理解,但 Bounded quantification 没有提到哈斯克尔,所以我不确定这是完全一样的事情。(再说一遍,不是一个类型理论家——只是一个喜欢哈斯克尔的人)

此外,关于类型 square :: Num a => a -> a 上面写着:

内容如下:“ square 具有类型 a -> a ,每 a 使得 一 归属 到课堂 Num (即,使得 (+) , (*) 、和否定定义在 一 )。”

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

这就是我的全部。就我个人而言,我认为“受约束的类型”或“被约束到类的类型”很好。

这个 Num a => 部分确实被称为约束;你可以把它读成“如果 Num a 是真的,那么。。。”

通常情况下,约束和量词是一起讨论的。任何受约束的类型都可以转换为等效类型,其中约束仅显示在内部 forall 或 exists 量词。因此,你不会像听到“受约束的参数多态性”那样经常听到“受限制的类型”( forall a. C => T ),“受约束的存在类型”( exists a. C => T ),或“受限多态性”(这两种量词)。

一个相关的术语是“有界多态”。有界多态通常意味着约束多态,其中约束是子类型或超类型约束。然而,这一区别并没有得到严格遵守。在Java或Scala等具有子类型的语言中,您经常会听到任何类型的约束被称为“绑定”

你可以称之为 有界多态型 (参见 wikipedia )。