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 类型推断的工作方式不同？
PS：对不起我的英语不好；这不是我的母语。
我建议你看看这篇文章：什么是 Hindley-Milner？（为什么它很酷）
这是他们用来解释类型推断的最简单的例子（它不是 ML，但想法是一样的）：
def foo(s: String) = s.length
// note: no explicit types
def bar(x, y) = foo(x) + y
只看bar的定义，我们很容易看出它的类型一定是(String, Int)=>Int。简而言之，这就是类型推断。阅读整篇文章以获取更多信息和示例。
我不是 C++ 专家，但我认为模板是更接近通用性/参数性的东西，这是不同的东西。
我认为试图将 ML 类型推断与 C++ 中的几乎所有内容联系起来更容易导致混淆而不是理解。C++ 根本没有任何类似于类型推断的东西。
C++ 中唯一没有明确键入的部分是模板，但（大部分）它们支持泛型编程。像您给出的 C++ 函数模板可能同样适用于无限制的类型集——例如，您NumType用作模板参数的代码，但可以使用字符串。单个程序可以实例化您add在一个地方添加两个字符串，在另一个地方添加两个数字。
ML 类型推断不适用于泛型编程。在 C 或 C++ 中，您显式定义参数的类型，然后编译器检查您尝试使用该参数执行的所有操作是否为该类型所允许。ML 逆转了这一点：它查看您对参数所做的事情，并确定您必须使用什么类型才能执行这些操作。如果您尝试做相互矛盾的事情，它会告诉您没有可以满足约束的类型。
这在 C 或 C++ 中几乎是不可能的，主要是因为允许的所有隐式类型转换。举个例子，如果我a + b在 ML 中有类似的东西，它可以立即得出结论，a并且b必须是整数——但在 C 或 C++ 中，它们几乎可以是整数、指针或浮点类型的任何组合（具有它们可以'不都是指针）或使用重载的定义类型operator+（例如，std::string）。在 ML 中，在最坏的情况下查找类型可能是指数级的，但几乎总是非常快。在 C++ 中，我估计它更频繁地呈指数增长，并且在很多情况下可能会受到不足的约束，因此给定的函数可以具有许多不同签名中的任何一个。
ML 使用Hindley-Milner 类型推断。在这个简单的例子中，它所要做的就是查看函数的主体，看看它+与参数一起使用并返回。因此，它可以推断出参数必须是+接受的参数类型（即 int），并且函数返回返回的类型+（也是 int）。因此推断的类型add是int -> int -> int。
请注意，在 SML（但不是 CAML）+中也定义了除 int 以外的其他类型，但是当有多种可能性时它仍然会推断 int（即add您定义的函数不能用于添加两个浮点数）。