向C++程序员解释ML类型推断

Question

ML如何在以下函数定义中执行类型推断：

let add a b = a + b

它是否像C++模板一样，在模板实例化之前不执行类型检查，在模板实例化之后，如果类型支持必要的操作，函数就会工作，否则就会抛出编译错误？

例如，下面的函数模板

template <typename NumType>
NumType add(NumType a, NumType b) {
  return a + b;
}

将适用于

add<int>(23, 11);

但不适用于

add<ostream>(cout, fout);

我猜测的是正确的还是ML类型推断的工作方式不同？

附言:对不起，我的英语很差，它不是我的母语。

Answer 1

我建议你看看这篇文章：What is Hindley-Milner? (and why is it cool)

这是他们用来解释类型推断的最简单的例子(它不是ML，但概念是相同的)：

def foo(s: String) = s.length
// note: no explicit types
def bar(x, y) = foo(x) + y

只要看看bar的定义，我们就可以很容易地看到它的类型必须是(String，Int)=>Int。简而言之，这就是类型推断。有关更多信息和示例，请阅读整篇文章。

我不是C++专家，但我认为模板是更接近泛型/参数化的东西，这是不同的东西。

Answer 2

我认为试图将ML类型推断与C++中的几乎任何东西联系起来，更有可能导致混淆，而不是理解。C++根本没有任何类似于类型推断的东西。

C++中唯一不显式类型化的部分是模板，但是(在大多数情况下)它们支持泛型编程。您给出的C++函数模板可能同样适用于一组无界类型--例如，您的代码使用NumType作为模板参数，但可以使用字符串。单个程序可以实例化您的add，以便在一个位置添加两个字符串，在另一个位置添加两个数字。

ML类型推断不适用于泛型编程。在C或C++中，您显式定义一个参数的类型，然后编译器检查您尝试对该参数执行的所有操作是否都是该类型所允许的。ML与之相反:它查看您对参数所做的事情，并计算出您必须是什么类型才能做这些事情。如果你尝试做一些相互矛盾的事情，它会告诉你没有能满足约束的类型。

这在C或C++中几乎是不可能的，这很大程度上是因为允许所有的隐式类型转换。例如，如果我在ML中有类似a + b的东西，它可以立即得出结论，a和b必须是ints -但在C或C++中，它们几乎可以是整数、指针或浮点类型的任意组合(但约束条件是它们不能都是指针)，或者使用重载operator+的已定义类型(例如，std::string)。在ML中，查找类型在最坏的情况下可能是指数级的，但几乎总是相当快的。在C++中，我估计它更多地是指数型的，在很多情况下可能是欠约束的，所以给定的函数可以有许多不同的签名中的任何一个。

Answer 3

ML使用Hindley-Milner type inference。在这个简单的例子中，它所要做的就是查看函数体，并查看它是否使用了带参数的+并返回该参数。因此，它可以推断参数必须是+接受的参数类型(即int)，并且函数返回+返回的类型(也是int)。因此，推断出的add类型是int -> int -> int。

请注意，在SML (而不是CAML)中，+也是为int以外的其他类型定义的，但当有多种可能性时，它仍然会推断出int (即，您定义的add函数不能用于添加两个浮点数)。