代码之家  ›  专栏  ›  技术社区  ›  Laurence Gonsalves

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

  •  9
  • Laurence Gonsalves  · 技术社区  · 12 年前

    例如 Num a => a

    我以为它们只是被称为“受限类型”,但谷歌搜索并没有发现这个词的很多用法,所以我很想知道它们是否有其他名字。

    5 回复  |  直到 12 年前
        1
  •  8
  •   Andreas Rossberg    12 年前

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

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

        2
  •  6
  •   Stefan Holdermans    12 年前

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

    大量相关 matches on Google

        3
  •  6
  •   Adam Wagner    12 年前

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

    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 (即,使得 (+) , (*) 、和否定定义在 )。”

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

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

        4
  •  6
  •   Heatsink    12 年前

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

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

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

        5
  •  1
  •   phipsgabler    12 年前

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