参数多态性 vs Ad-hoc 多态性

2022-01-24 00:00:00 type-inference types polymorphism java haskell

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

更准确地说:

  1. 类型推断算法如何?Java 中的类型推断与 Haskell 中的类型推断有何不同?
  2. 请给我一个例子，说明可以用 Java/Scala 编写但不能用 Haskell 编写的情况(根据这些平台的模块化特性也是如此)，反之亦然.

提前致谢.

解决方案

根据 TAPL，§23.2:

<块引用>

参数多态性(...)，允许单片要一般"键入的代码，使用变量代替实际类型，以及然后根据需要用特定类型实例化.参数定义是统一的:它们的所有实例的行为都相同.(...)

Ad-hoc 多态性，相比之下，允许多态值显示在不同类型查看"时的不同行为.最普遍的ad-hoc 多态性的例子是重载，它将单个具有许多实现的功能符号；编译器(或运行时系统，取决于重载决议是静态的还是动态的)为每个应用程序选择适当的实现函数，基于参数的类型.

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

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

交换 :: (A; B) ->(乙；甲)交换 (x; y) = (y; x)

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

但没有预先存在的构造提供 ad-hoc 多态性，它旨在让您编写适用于几个但并非全部的函数> 类型.类型类被实现为实现这一目标的一种方式.

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

在 :: (Ord a) a -> 之间一个->一个->布尔在 x y z = x ≤ y ^ y ≤ z

其中 Ord 是定义函数 (_ ≤ _) 的类.使用时，(between "abc" "d" "ghi") 静态解析为字符串选择正确的instance(而不是例如integers) - 恰好在(Java 的)方法重载的时候.

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

<小时>

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

  1. 对于 Haskell，这是因为它具有 impredicative(又名第一类)多态性，类型推断是不可判定的.请注意，在这一点上，Java 仅限于一阶多态(Scala 扩展的东西).

  2. 对于 Java，这是因为它支持 逆变子类型.

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

  1. 对于 Haskell，推理适用于所有非高度多态"的术语，并根据已发布的著名算法扩展做出认真的努力来返回正确的结果:

    • Haskell 的推理的核心是基于 Hindley-Milner，在推断应用程序的类型时立即为您提供完整的结果，类型变量(例如 A 和 B 在上面的例子中)只能用 非多态 类型实例化(我正在简化，但这本质上是你可以在例如 Ocaml 中找到的 ML 风格的多态性.).
    • 最近的 GHC 将确保可能需要类型注释 仅适用于具有非 Damas-Milner 类型的 let-binding 或 λ-abstraction.
    • Haskell 甚至在其最复杂的扩展(例如 GADT).无论如何，提议的扩展几乎总是出现在一篇带有扩展类型推断的正确性证明的论文中.

  2. 对于 Java，类型推断以更有限的方式应用:

    <块引用>

    在 Java 5 发布之前，Java 中没有类型推断.根据 Java 语言文化，每个变量、方法和动态分配的对象的类型都必须由程序员显式声明.当 Java 5 中引入泛型(按类型参数化的类和方法)时，该语言保留了对变量、方法和分配的这一要求.但是多态方法(按类型参数化)的引入要求(i)程序员在每个多态方法调用站点提供方法类型参数或(ii)语言支持方法类型参数的推断.为了避免给程序员增加额外的文书负担，Java 5 的设计者选择执行类型推断来确定多态方法调用的类型参数.(来源，强调我的)

    推理算法是本质上是 GJ 的，但带有 有点 kludgy 添加通配符作为事后的想法(请注意，我不是最新的 J2SE 6.0 中可能进行的更正).方法的巨大概念差异在于 Java 的推理是 local，从某种意义上说，表达式的推断类型仅取决于从类型系统生成的约束及其子表达式的类型，但不在上下文中.

    请注意，关于不完整的党线 &有时不正确的类型推断相对宽松.根据 规范:p><块引用>

    还要注意，类型推断不会以任何方式影响可靠性.如果推断的类型是无意义的，则调用将产生类型错误.类型推断算法应该被视为一种启发式算法，旨在在实践中表现良好.如果它无法推断出所需的结果，则可以使用显式类型参数.

I would like to understand the key difference between parametric polymorphism such as polymorphism of generic classes/functions in the Java/Scala/C++ languages and "ad-hoc" polymorphism in the Haskell type system. I'm familiar with the first kind of languages, but I have never worked with the Haskell.

More precisely:

  1. How is type inference algorithm e.g. in Java different from the type inference in Haskell?
  2. Please, give me an example of the situation where something can be written in Java/Scala but can not be written in Haskell(according to the modular features of these platforms too), and vice-versa.

Thanks in advance.

解决方案

As per the 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.

So, if you consider successive stages of history, non-generic official Java (a.k.a pre-J2SE 5.0, bef. sept. 2004) had ad-hoc polymorphism - so you could overload a method - but not parametric polymorphism, so you couldn't write a generic method. Afterwards you could do both, of course.

By comparison, since its very beginning in 1990, Haskell was parametrically polymorphic, meaning you could write:

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

where A and B are type variables can be instantiated to all types, without assumptions.

But there was no preexisting construct giving ad-hoc polymorphism, which intends to let you write functions that apply to several, but not all types. Type classes were implemented as a way of achieving this goal.

They let you describe a class (something akin to a Java interface), giving the type signature of the functions you want implemented for your generic type. Then you can register some (and hopefully, several) instances matching this class. In the meantime, you can write a generic method such as : 

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

where the Ord is the class that defines the function (_ ≤ _). When used, (between "abc" "d" "ghi") is resolved statically to select the right instance for strings (rather than e.g. integers) - exactly at the moment when (Java's) method overloading would.

You can do something similar in Java with bounded wildcards. But the key difference between Haskell and Java on that front is that only Haskell can do dictionary passing automatically: in both languages, given two instances of Ord T, say b0 and b1, you can build a function f that takes those as arguments and produces the instance for the pair type (b0, b1), using, say, the lexicographic order. Say now that you are given (("hello", 2), ((3, "hi"), 5)). In Java you have to remember the instances for string and int, and pass the correct instance (made of four applications of f!) in order to apply between to that object. Haskell can apply compositionality, and figure out how to build the correct instance given just the ground instances and the f constructor (this extends to other constructors, of course) .

Now, as far as type inference goes (and this should probably be a distinct question), for both languages it is incomplete, in the sense that you can always write an un-annotated program for which the compiler won't be able to determine the type.

  1. for Haskell, this is because it has impredicative (a.k.a. first-class) polymorphism, for which type inference is undecidable. Note that on that point, Java is limited to first-order polymorphism (something on which Scala expands).

  2. for Java, this is because it supports contravariant subtyping.

But those languages mainly differ in the range of program statements to which type inference applies in practice, and in the importance given to the correctness of the type inference results.

  1. For Haskell, inference applies to all "non-highly polymorphic" terms, and make a serious effort to return sound results based on published extensions of a well-known algorithm:

    • At its core, Haskell's inference is based on Hindley-Milner, which gives you complete results as soon as when infering the type of an application, type variables (e.g. the A and B in the example above) can be only instantiated with non-polymorphic types (I'm simplifying, but this is essentially the ML-style polymorphism you can find in e.g. Ocaml.).
    • a recent GHC will make sure that a type annotation may be required only for a let-binding or λ-abstraction that has a non-Damas-Milner type.
    • Haskell has tried to stay relatively close to this inferrable core across even its most hairy extensions (e.g. GADTs). At any rate, proposed extensions nearly always come in a paper with a proof of the correctness of the extended type inference .

  2. For Java, type inference applies in a much more limited fashion anyway :

    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)

    The inference algorithm is essentially that of GJ, but with a somewhat kludgy addition of wildcards as an afterthought (Note that I am not up to date on the possible corrections made in J2SE 6.0, though). The large conceptual difference in approach is that Java's inference is local, in the sense that the inferred type of an expression depends only on constraints generated from the type system and on the types of its sub-expressions, but not on the context.

    Note that the party line regarding the incomplete & sometimes incorrect type inference is relatively laid back. As per 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.

相关文章