OCaml中的多态性 - ad hoc,参数,包含/子类型

Question

我在理解不同类型的多态性时遇到了问题,特别是在OCaml方面.我知道多态性允许OCaml中的多个类型表示为'a,但我不明白不同类型的多态是什么.
如果有人可以用相对较低级别的语言给我一个解释,那就太棒了!ad hoc,参数,包含/子类型

Answer 1

这是一个近似值.

Ad-hoc多态通常是指能够声明具有不同类型的相同名称(通常是函数),例如+ : int -> int -> int,+ : float -> float -> float在SML中.这些是不同的功能,它们可以以完全不同的方式起作用,但编译器或解释器根据上下文选择适当的功能.我想不出OCaml中任何ad-hoc多态性的例子.然而,它在C++和Java中很常见.

参数多态是指单个函数可以使用任何类型的参数,因为它不会试图查看该参数的结构.例如,cons : 'a -> 'a list -> 'a list能够将v任何类型的值添加到相同类型的值列表中,因为它cons与结构(布局)的v内容或它支持的操作无关.在C术语中,cons不需要"取消引用"指针,或者对v特定于实际类型的操作执行任何操作v.请注意,与ad-hoc多态性不同,cons 具有对所有类型采取相同的行动.因此,参数和特殊多态性在某种程度上是彼此自然的"对立面".参数多态性是OCaml中绝大多数多态性实例的原因.

子类型多态性是指您可以使用类型的t值,其中type u是值.这可能是因为类型t支持所有类型的操作u,或者因为t结构可以在u预期的地方使用.这方面的例子将继承(也许总线可用于任何车辆都可以),或多态性变异(可以使用'A | 'B那里'A | 'B | 'C的预期).

编辑每条评论

但请注意,必须在OCaml中明确请求子类型.例如,如果你有一个函数f : u -> int,并且你想将它应用于v : twhere t子类型u,你必须写f (v :> u).该(v :> u)语法是一种类型的强制.

OCaml还支持行多态,行多态是一种带约束的参数多态.如果f是f : #u -> int(对于对象类型)或f : [< u] -> int(对于多态变体),#u/ [< u]syntax表示类型变量,类似于'a,但只能用相应的"子类型"替换u(在限制意义上它们可以支持更多字段/ less构造函数,分别).然后,你可以f v没有强制.对于涉及多态变体和对象的许多表达式,OCaml会自动推断使用行多态的类型,但如果要创建签名,则必须显式编写类型.

行多态性有更多用法和注意事项.我忽略了实际的行变量和附加语法,只描述了看似有限量化的东西(如Java泛型).关于行多态性,其名称和/或形式主义的更详细和准确的讨论可能最好地保存用于单独的问题.

Answer 2

我其实并不认为这种问题特别适合Stack Overflow的优势。有很多关于类型的书。事实上，我建议阅读Pierce 的《类型和编程语言》，我发现这本书非常有启发性且令人愉快。

作为一个快速回答（主要基于我从皮尔斯那里记得的内容:-），这是我对这些术语的看法。

参数多态性是指其中包含自由变量的类型，其中变量可以被任何类型替换。该函数List.length具有这样的类型，因为它可以找到任何列表的长度（无论元素的类型是什么）。

# List.length;;
- : 'a list -> int = <fun>

OCaml 的奇妙之处之一是它不仅支持这样的类型，还可以推断它们。给定函数定义，OCaml 会推断该函数最通用的参数多态类型。

子类型是类型之间的关系。如果T的所有实例也是 U 的实例（但不一定反之亦然），则类型T是类型U的子类型。OCaml 支持子类型化，即它允许程序将类型T的值视为其超类型U的值。然而，程序员必须明确要求这一点。

# type ab = [ `A | `B ];;
type ab = [ `A | `B ]
# type abc = [`A | `B | `C ];;
type abc = [ `A | `B | `C ]
# let x : ab = `A;;
val x : ab = `A
# let y : abc = x;;
Error: This expression has type ab but an expression was expected
of type abc. The first variant type does not allow tag(s) `C
# let y : abc = (x :> abc);;
val y : abc = `A

在此示例中，类型 typeab是 type 的子类型abc，并且x具有 type ab。您可以将x其用作 type 的值abc，但必须使用:>类型运算符显式转换。

临时多态性是指程序员针对特定情况定义的多态性，而不是从基本原理派生的多态性。（或者至少这就是我的意思，也许其他人以不同的方式使用这个术语。）一个可能的例子是 OO 继承层次结构，其中对象状态的实际类型不需要以任何方式相关，只要方法之间有适当的关系。

关于临时多态性（恕我直言）的关键观察是，它的工作取决于程序员。因此，它并不总是有效。这里的其他类型的多态性，基于基本原理，实际上不会失败。当使用复杂的系统时，这是一种令人欣慰的感觉。