java - 参数多态性与 Ad-hoc 多态性

Question

我想了解参数多态性(例如 Java/Scala/C++ 语言中的泛型类/函数的多态性)与 Haskell 类型系统中的“临时”多态性之间的主要区别。我熟悉第一种语言，但我从未使用过 Haskell。

更确切地说:

类型推断算法如何，例如Java 中的类型推断与 Haskell 中的类型推断有何不同？

请举一个例子，说明可以用 Java/Scala 编写但不能用 Haskell 编写的内容(根据这些平台的模块化特性)，反之亦然。

提前致谢。

Answer 1

根据 TAPL ，第 23.2 节:

Parametric polymorphism (...), allows a single piece of code to be typed “generically,” using variables in place of actual types, and then instantiated with particular types as needed. Parametric definitions are uniform: all of their instances behave the same. (...)

Ad-hoc polymorphism, by contrast, allows a polymorphic value to exhibit different behaviors when “viewed” at different types. The most common example of ad-hoc polymorphism is overloading, which associates a single function symbol with many implementations; the compiler (or the runtime system, depending on whether overloading resolution is static or dynamic) chooses an appropriate implementation for each application of the function, based on the types of the arguments.

因此，如果您考虑历史的连续阶段，非通用官方 Java(又名 pre- J2SE 5.0，2004 年 9 月之前)具有临时多态性 - 因此您可以 overload a method - 但不是参数多态性，所以你不能 write a generic method .之后你当然可以两者都做。

相比之下，从一开始 in 1990 , Haskell 是参数多态的，这意味着你可以写:

swap :: (A; B) -> (B; A)
swap (x; y) = (y; x)

其中 A 和 B 是类型变量，可以实例化为所有类型，无需假设。

但是没有预先存在的构造提供临时多态性，它旨在让您编写适用于多种类型的函数，但不是所有类型。类型类是作为实现这一目标的一种方式来实现的。

它们让您描述一个类(类似于 Java 接口(interface)的东西)，给出要为泛型类型实现的函数的类型签名。然后你可以注册一些(希望是几个)与这个类匹配的实例。同时，您可以编写一个通用方法，例如:

between :: (Ord a)  a -> a -> a -> Bool
between x y z = x ≤ y ^ y ≤ z

哪里Ord是定义函数的类 (_ ≤ _) .使用时，(between "abc" "d" "ghi")静态解析为字符串(而不是例如整数)选择正确的实例 - 正是在(Java的)方法重载的那一刻。

你可以用 bounded wildcards 在 Java 中做类似的事情.但是 Haskell 和 Java 在这方面的主要区别在于，只有 Haskell 可以自动传递字典 : 在两种语言中，给出 Ord T 的两个实例，说 b0和 b1 ，您可以构建一个函数 f将这些作为参数并生成对类型 (b0, b1) 的实例，比如说，使用字典顺序。现在说你得到了 (("hello", 2), ((3, "hi"), 5)) .在 Java 中，您必须记住 string 的实例。和 int ，并传递正确的实例(由 f 的四个应用程序组成!)以应用 between到那个对象。 Haskell 可以申请 compositionality ，并找出如何在仅给出地面实例和 f 的情况下构建正确的实例。构造函数(当然，这扩展到其他构造函数)。

现在，就类型推断而言(这可能应该是一个不同的问题)，对于两种语言来说，它都是不完整的，因为您总是可以编写 未注释 编译器将无法确定其类型的程序。

对于 Haskell，这是因为它有 impredicative (a.k.a. first-class) 多态性，类型推断是不可判定的。请注意，在这一点上，Java 仅限于一阶多态(Scala 对此进行了扩展)。

对于Java，这是因为它支持contravariant subtyping .

但这些语言的主要区别在于 类型推断适用的程序语句范围 在实践中，在 重视正确性 类型推断结果。

对于 Haskell，推理适用于所有“非高度多态性”术语，并根据已发布的知名算法扩展认真努力返回合理的结果:

在其核心，Haskell 的推理基于 Hindley-Milner ，一旦推断应用程序的类型，它就会为您提供完整的结果，类型变量(例如上面示例中的 A 和 B)只能用非多态类型实例化(我正在简化，但是这本质上是您可以在例如 Ocaml 中找到的 ML 风格的多态性。)。

最近的 GHC 将确保可能需要类型注释 only for a let-binding or λ-abstraction that has a non-Damas-Milner type .

Haskell 试图在其最毛茸茸的扩展(例如 GADTs )中与这个可推断的核心保持相对接近。无论如何，提议的扩展几乎总是出现在一篇论文中，并证明了扩展类型推断的正确性。

对于 Java，类型推断无论如何都适用于更有限的方式:

Prior to the release of Java 5, there was no type inference in Java. According to the Java language culture, the type of every variable, method, and dynamically allocated object must be explicitly declared by the programmer. When generics (classes and methods parameterized by type) were introduced in Java 5, the language retained this requirement for variables, methods, and allocations. But the introduction of polymorphic methods (parameterized by type) dictated that either (i) the programmer provide the method type arguments at every polymorphic method call site or (ii) the language support the inference of method type arguments. To avoid creating an additional clerical burden for programmers, the designers of Java 5 elected to perform type inference to determine the type arguments for polymorphic method calls. (source, emphasis mine)

inference algorithm本质上是 that of GJ ，但带有 somewhat kludgy添加通配符作为事后的想法(请注意，我并没有及时了解 J2SE 6.0 中可能进行的更正)。方法上的巨大概念差异在于 Java 的推理是局部的，从某种意义上说，表达式的推断类型仅取决于从类型系统生成的约束及其子表达式的类型，而不取决于上下文。

请注意，有关不完整且有时不正确的类型推断的派对路线相对宽松。根据 the spec :

Note also that type inference does not affect soundness in any way. If the types inferred are nonsensical, the invocation will yield a type error. The type inference algorithm should be viewed as a heuristic, designed to perfdorm well in practice. If it fails to infer the desired result, explicit type paramneters may be used instead.