La inferencia de tipos es una característica predominante de los lenguajes de programación funcionales tales como ML, Haskell, C#, Vala y Ocaml.

La inferencia de tipos asigna automáticamente un tipo de datos a una función sin necesidad de que el programador lo escriba. El tipo de las funciones es reconstruido a partir de un análisis estático del programa realizado por el compilador o intérprete del lenguaje, a partir de las definiciones previas y del uso de las variables en el cuerpo de las funciones.

Ejemplo

Una definición de la función longitud de lista en Haskell se puede definir de la siguiente forma:

-- Función longitud
-- [] denota una lista vacía 
-- (prim:resto) denota una lista formada por un elemento, prim, concatenado o construido con el resto 
-- : operador constructor de listas.
function longitud
longitud [] = 0
longitud (prim:resto) = 1 + longitud resto

Al leer esta definición se observa que su argumento es una lista, que los valores de los elementos de la lista no influyen en el resultado y que este resultado siempre es un número (cero o el resultado de una suma). De estas observaciones, el compilador puede deducir el tipo de la función, que es:

longitud :: [a] -> Int 

Este tipo resultante se lee como sigue: al recibir una lista con elementos de cualquier tipo, siendo todos los elementos de la misma del mismo tipo, (representado por a en la sintaxis de Haskell), la función producirá un entero (tipo Int de Haskell).

En la inferencia de tipos no interviene sobrecarga de operadores, que se manejan con la noción de polimorfismo ad hoc, sino cuantificaciones universales que conducen a la noción de polimorfismo parametrizado.

Algoritmo Hindley-Milner de inferencia de tipos

El algoritmo comúnmente utilizado para realizar inferencia de tipos es el que normalmente se denomina algoritmo de Hindley-Milner o algoritmo de Damas-Milner. Tiene sus orígenes en el algoritmo de tipos para el cálculo Lambda tipificado, el cual fue propuesto por Haskell B. Curry y Robert Feys en 1958.

En 1969 Roger Hindley extendió ese trabajo y demostró que ese algoritmo siempre deduce el tipo más general posible.

En 1978 Robin Milner, de forma independiente al trabajo de Hindley propuso un algoritmo equivalente para el lenguaje de programación ML.

En 1985 Luis Damas, estudiante de Milner, finalmente demostró que el algoritmo de Milner es completo y lo extendió para dar soporte a la noción de referencia polimórfica.