非技术性解说

在大多数的编程语言中，所有值都有一个类型，它描述特定值的数据种类。在一些语言中，表达式的类型只在运行时才知道；这些语言被称作动态类型语言。而另一些语言中，表达式的类型在编译时就知道，这些语言叫做静态类型语言。在静态类型语言中，函数的输入和输出与局部变量的类型一般必须用类型标注明确的提供。例如，在 C 语言中:

int addone(int x) { int result; /*声明整数 result (C 语言)*/ result = x+1; return result; }

这个函数定义开始处， 声明了 是函数，接受一个整数类型的参数，并返回一个整数。 声明了局部变量 是个整数。在支持类型推论的建议的语言中，代码可写为如下:

addone(x) { var result; /*推论类型 result (在建议的语言中)*/ var result2; /*推论类型 result #2 */ result = x+1; result2 = x+1.; /* 此行不工作 */ return result;}

这看起来非常像在动态类型语言中写出的代码，但是提供了一些额外的约束（见下）使得能够在编译时推断出所有变量的类型。在上面的例子中，因为 总是接受两个整数并返回一个整数。编译器可以推论出 的值是个整数，因此 是个整数， 的返回值是个整数。类似的，因为 要求它的两个实际参数都是整数， 必须是整数，因此 接受一个整数实际参数。

但是在随后一行中 result2 加上了一个浮点数 ""，导致了 同时用于整数和浮点数的冲突。这种情况将生成编译时间错误消息。在老语言中，result2 可以被隐含的声明为浮点变量，通过隐含的转换表达式中的整数 ，简单的因为小数点意外的被放到了整数 1 的后面。这种情况说明了二者之间的区别，“类型推论”不涉及类型转换，而“隐含类型转换”经常没有限制的把数据强制成高精度的数据类型。

技术描述

类型推论指的是要么部分要么完全自动演绎的能力，把值的类型从表达式的最终计算中推导出来。因为这个过程在编译时间系统性的进行，编译器经常能推出变量的类型或函数的类型标署，而不用给出明确的类型标注。在很多情况下，如果推论系统足够强壮或程序足够简单，有可能完全从程序中省略类型标注。

要获得正确推导出缺乏类型标注的一个表达式的类型所必要的信息，编译器要么随着给它的子表达式(它们自身可以是变量或函数)的类型标注的聚集(aggregate)和后续简约来收集这种信息，要么通过各种原子值的类型的隐含理解(比如 () : 单位; true : 布尔; 42 : 整数; 3.14159 : 实数; 等等)。通过表达式的最终简约到隐含类型原子值的识别，类型推论语言的编译器有能力编译完全没有类型标注的程序。在高阶编程和多态性的高度复杂的情况下，编译器不能总是如此推论，偶尔需要类型标注来去除歧义。

例子

例如，考虑 Haskell 函数 ，它把一个函数应用于一个列表的每个元素上，它可定义为:

map f [] = []map f (first:rest) = f first : map f rest

明显的函数 接受一个列表作为第二个实际参数，它的第一个实际参数 是可以应用于这个列表的元素的类型上函数，而 的结果被构造为其元素是 的结果的一列表。所以假定列表包含同样类型的元素，我们能可靠的构造出类型标署

map :: (a -> b) -> [a] -> [b]

这里的语法 "" 指示接受 作为它的形式参数并生成 的一个过程。 "" 等价于 ""。

注意 的推论类型是参数化多态的: 实际参数和 的结果的类型是不推出的，而是留作类型变量，所以 可以应用于各种类型的函数和列表，只要在每次调用中实际类型是匹配的。

Hindley–Milner 类型推论算法

进行类型推论的常用算法是 Hindley–Milner 或 Damas–Milner 算法。