Inferencia de tipos
Keywords: Inferencia de tipos, 1958, 1969, 1978, 1985, Compilador, Cálculo Lambda, Haskell, Haskell Curry
Inferencia de tipos es una característica predominante de los lenguajes de programación funcional tales como ML, Haskell 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 interpretador del lenguaje, a partir de las definiciones previas y del uso de las variables en el cuerpo de las funciones.
Ejemplo
La función longitud en Haskell se define como sigue:
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: al recibir una lista con elementos de cualquier 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 al goritmo de Hindley-Milner o algoritmo de Damas-Milner.
- Este algoritmo 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.
Referencias
- Correo electrónico de Roger Hindley explicando la historia de la inferencia de tipos.