Inferència de tipos

La inferència de tipos és una característica predominant dels llenguages de programació funcionals tals com ML, Haskell, C#, Vala i OCaml.

L'inferència de tipos assigna automàticament un tipo de senyas a una funció sense necessitat de que el programador ho escriga. El tipo de les funcions és reconstruït a partir d'un anàlisis estàtic del programa realisat pel compilador o intérpret del llenguage, a partir de les definicions prèvies i de l'us de les variables en el cos de les funcions.

Eixemple

Una definició de la funció llongitut de llista en Haskell es pot definir de la següent forma:

-- Funció llongitut
-- [] denota una llista buida 
-- (prim:restant) denota una llista formada per un element, prim, concatenat o construït en el restant 
-- : operador constructor de llistes.
function llongitut
llongitut [] = 0
llongitut (prim:restant) = 1 + llongitut reste

En llegir esta definició s'observa que el seu argument és una llista, que els valors dels elements de la llista no influïxen en el resultat i que este resultat sempre és un número (zero o el resultat d'una suma). D'estes observacions, el compilador pot deduir el tipo de la funció, que és:

llongitut :: [a] -> Int 

Este tipo resultant es llig com seguix: en rebre una llista en elements de qualsevol tipo, sent tots els elements de la mateixa del mateix tipo, (representat per a en la sintaxis de Haskell), la funció produirà un sancer (tipo Int de Haskell).

En l'inferència de tipos no intervé sobrecàrrega d'operadors, que es manegen en la noció de polimorfisme ad hoc, sino quantificacions universals que conduïxen a la noció de polimorfisme parametrizado.

Algoritme Hindley-Milner d'inferència de tipos

L'algoritme comunament utilisat per a realisar inferència de tipos és el que normalment es denomina algoritme de Hindley-Milner o algoritme de Dames-Milner. Té els seus orígens en l'algoritme de tipos per al càlcul Lambda tipificat, el qual va ser propost per Haskell B. Curry i Robert Feys en 1958.

En 1969 Roger Hindley va estendre eixe treball i va demostrar que eixe algoritme sempre deduïx el tipo més general possible.

En 1978 Robin Milner, de forma independent al treball de Hindley va propondre un algoritme equivalent per al llenguage de programació ML.

En 1985 Luis Dames, estudiant de Milner, finalment va demostrar que l'algoritme de Milner és complet i ho va estendre per a donar soport a la noció de referència polimòrfica.