参数多态性与Ad-hoc多态性 [英] Parametric polymorphism vs Ad-hoc polymorphism

问题描述

我想了解参数多态性（例如Java / Scala / C ++语言中泛型类/函数的多态性）和Haskell类型系统中的ad-hoc多态性之间的主要区别。我对第一种语言很熟悉，但我从未与Haskell合作过。

更确切地说：

1. 类型推理算法如何？在Java中与Haskell中的类型推断不同吗？


2. 请给我一个例子，说明可以用Java / Scala编写某些东西但不能用Haskell写的东西（根据这些平台的模块化功能也是如此），反之亦然。

预先致谢。 class =h2_lin>解决方案

根据 TAPL

a>，§23.2：

参数多态性（...）允许输入一段
代码一般来说，使用变量代替实际类型，
然后根据需要使用特定类型实例化。参数定义
是统一的：它们的所有实例表现相同。 （...）

相比之下，Ad-hoc多态性允许多态值在不同类型的查看时显示
不同的行为。 ad-hoc多态的最常见
例子是重载，它将单个
函数符号与许多实现相关联;编译器（或运行时系统，取决于重载解析是静态的还是动态的）根据参数的类型为
函数的每个应用程序选择适当的实现。

所以，如果你考虑连续的历史阶段，非泛型官方Java（aka pre- J2SE 5.0 ，bef。sept。2004）有ad-hoc多态性 - 所以你可以重载方法 - 但不是参数多态，所以你不能编写一个通用方法。当然，你也可以做到这一点。

通过比较，从一开始，Haskell是参数多态的，这意味着你可以这样写：

  swap ::（A; B） - > （B; A）
 swap（x; y）=（y; x）
  

其中A和B是类型变量，可以被实例化为所有类型，没有任何假设。

但是没有预先存在的构造给予 ad -hoc 多态，它可以让你编写适用于几个，但不是所有类型的函数。类型类是实现这个目标的一种方式。

它们允许您描述类（类似于Java接口），给出类型签名你想为你的泛型类型实现的功能。然后，你可以注册一些（有希望的是， ）实例匹配这个类。与此同时，您可以编写一个通用方法，例如：::（Ord a）a - >之间的

  a  - > a  - > Bool 
之间xyz = x≤y ^ y≤z 
  

其中 Ord 是定义函数（_≤_）的类。当使用（在abcdghi）之间时<静态解析来选择正确的实例对于字符串（而不是整数） - 恰好在（Java的）方法重载时。

您可以在Java中使用有界通配符。但Haskell和Java之间的关键区别在于，只有Haskell可以自动执行字典传递：在两种语言中，给定两个 Ord T ，例如 b0 和 b1 ，您可以构建一个函数 f ，它将这些参数作为参数，并使用比方说词典顺序为pair类型（b0，b1）生成实例。现在说你给了（（hello，2），（（3，hi），5））。在Java中，您必须记住 string 和 int 的实例，并传递正确的实例（由四个应用程序 f ！），以便在之间应用到该对象。 Haskell可以应用组合性，并找出如何构建正确的实例，只给出底层实例和
$ b $ hr

<现在，就类型推断而言（这可能是一个明显的问题），对于这两种语言来说，它是不完整的，因为您可以始终写编译器无法确定类型的未注释的程序。



1. 对于Haskell来说，这是因为它有 impredicative （aka first-class）多态性，这种类型推断是不可判定的。请注意，在这一点上，Java仅限于一阶多态（用于Scala扩展的某些内容）。对于Java，这是因为它支持 href =http://research.microsoft.com/pubs/64041/fool2007.pdf =noreferrer> contravariant subtyping 。

但是这些语言在实践中的主要区别在适用于类型推断的程序语句范围内，对正确性的重要性对于Haskell，推理适用于所有非高度多态的术语，并使得我们认真努力地根据已知算法的已发布扩展来返回声音结果：



• Haskell的核心推断基于< a href =http://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_inference_algorithm#Hindley.E2.80.93Milner_type_inference_algorithm =noreferrer> Hindley-Milner ， es在推断应用程序的类型时尽快完成结果， type variables （例如，上面例子中的 A 和 B ）只能用非多态实例化类型（我正在简化，但这实质上就是您可以在Ocaml中找到的ML样式多态）。
  
• 最近的GHC将确保可能需要类型注释<只有对于一个具有非结构元素的let-binding或λ-abraction，href =http://research.microsoft.com/en-us/um/people/simonpj/papers/ carboxy/ =noreferrer Damas-Milner类型。


• Haskell试图保持与这个可推测的核心相对接近，即使是最毛茸茸的扩展（例如 GADT ）。无论如何，所提出的扩展几乎总是出现在具有扩展类型推断的正确性证明的论文中。

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

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

推理算法基本上是 GJ的 ，但是有点 kludgy 添加通配符作为事后考虑（请注意，我没有及时了解J2SE 6.0中可能的更正，但）。方法中的概念上的巨大差异在于，Java的推理是 local ，因为表达式的推断类型仅依赖于类型系统及其子表达式的类型生成的约束，不在上下文中。

请注意，关于不完整&有时不正确的类型推断是相对悠闲的。按照规范：

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

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.

这篇关于参数多态性与Ad-hoc多态性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！