Tipo de inferencia

Inferencia de tipos ( eng. type inference ): en programación , la capacidad del compilador de inferir lógicamente el tipo del valor de la expresión misma . El mecanismo de inferencia de tipos se introdujo por primera vez en el lenguaje ML , donde el compilador siempre infiere el tipo polimórfico más general para cualquier expresión. Esto no solo reduce el tamaño del código fuente y aumenta su concisión, sino que a menudo aumenta la reutilización del código [1] .

La inferencia de tipos es característica de los lenguajes de programación funcional , aunque con el tiempo se ha implementado parcialmente en lenguajes orientados a objetos ( C# , D , Visual Basic .NET , Nim , C++11 , Vala , Java [a] ), donde se limita a la capacidad de omitir el tipo de un identificador en una definición con inicialización (ver azúcar sintáctico ). Por ejemplo:

var s = "¡Hola, mundo!" ; // El tipo de la variable s (de cadena) se deriva del inicializador

Algoritmos

Algoritmo de Hindley-Milner

El algoritmo Hindley-Milner es un mecanismo de inferencia de tipo expresión implementado en lenguajes de programación basados en el sistema de tipos Hindley-Milner , como ML (el primer lenguaje de esta familia), Standard ML , OCaml , Haskell , F# , Fortress y buu _ El lenguaje Nemerle utiliza este algoritmo con una serie de modificaciones necesarias [2] .

El mecanismo de inferencia de tipo se basa en la capacidad de inferir automáticamente, total o parcialmente, el tipo de una expresión obtenida al evaluar alguna expresión. Dado que este proceso se realiza sistemáticamente durante la traducción del programa, el compilador a menudo puede inferir el tipo de una variable o función sin especificar explícitamente los tipos de esos objetos. En muchos casos, se pueden omitir declaraciones de tipo explícitas; esto se puede hacer para objetos bastante simples o para lenguajes con sintaxis simple. Por ejemplo, el lenguaje Haskell tiene un mecanismo de inferencia de tipos bastante potente, por lo que no es necesario especificar los tipos de funciones en este lenguaje de programación. El programador puede especificar el tipo de una función explícitamente para restringir su uso a tipos de datos específicos o para un formato de código fuente más estructurado.

Para obtener información para la inferencia correcta del tipo de una expresión en ausencia de una declaración explícita del tipo de esta expresión, el traductor recopila dicha información de las declaraciones explícitas de los tipos de subexpresiones (variables, funciones) incluidas en la expresión estudiada, o utiliza información implícita sobre los tipos de valores atómicos. Dicho algoritmo no siempre ayuda a determinar el tipo de una expresión, especialmente en los casos de uso de funciones de orden superior y polimorfismo paramétrico de naturaleza bastante compleja. Por lo tanto, en casos complejos, cuando sea necesario evitar ambigüedades, se recomienda especificar explícitamente el tipo de expresiones.

El modelo de tipificación en sí se basa en el algoritmo de inferencia de tipo de expresión, que tiene como fuente el mecanismo de derivación de tipo de expresión utilizado en el cálculo λ tipado , que fue propuesto en 1958 por H. Curry y R. Face. Además, Roger Hindley en 1969 amplió el propio algoritmo y demostró que deriva el tipo de expresión más general. En 1978 , Robin Milner , independientemente de R. Hindley, probó las propiedades de un algoritmo equivalente. Y finalmente, en 1985 , Louis Damas finalmente demostró que el algoritmo de Milner está completo y puede usarse para tipos polimórficos. En este sentido, el algoritmo de Hindley-Milner a veces también se denomina algoritmo de Damas-Milner .

El sistema de tipos se define en el modelo Hindley-Milner de la siguiente manera:

Los tipos primitivos son tipos de expresión. $v$
Las variables de tipo paramétrico α son tipos de expresión.
Si y son tipos de expresión, entonces el tipo es el tipo de expresión. $\sigma _{{1}}$ $\sigma _{{2}}$ $\sigma _{{1}}\flecha derecha \sigma _{{2}}$
Un símbolo es un tipo de expresiones. $\bot$

Las expresiones cuyos tipos se evalúan se definen de una forma bastante estándar:

Las constantes son expresiones.
Las variables son expresiones.
Si y son expresiones, entonces ( ) es una expresión. $e_{{1}}$ $e_{{2}}$ $e_{{1}}e_{{2}}$
Si es una variable y es una expresión, entonces es una expresión. $v$ $mi$ $\lambda ve$

Se dice que un tipo es una instancia de tipo cuando hay alguna conversión tal que: $\sigma _{{1}}$ $\sigma _{{2}}$ $\rho$

$\sigma _{{1}}=\rho (\sigma _{{2}})$

En este caso, se suele suponer que las conversiones de tipo están sujetas a restricciones, que son las siguientes: $\rho$

$\rho (\sigma_{{1}}\rightarrow \sigma_{{2}})=\rho (\sigma_{{1}})\rightarrow \rho (\sigma_{{2}})$
$\rho (v)=v$

El algoritmo de inferencia de tipos en sí consta de dos pasos: la generación de un sistema de ecuaciones y la posterior solución de estas ecuaciones.

Construcción de un sistema de ecuaciones

La construcción de un sistema de ecuaciones se basa en las siguientes reglas:

${\ estilo de visualización \ Gamma v = \ tau}$ - si el enlace está en . $v:\tau$ $\Gama$
${\ estilo de visualización \ Gamma (ge) = \ tau}$ — si , dónde y . $\tau _{{1}}=\tau _{{2}}\flecha derecha \tau$ ${\ estilo de visualización \ tau _ {1} = \ gamma g}$ ${\ estilo de visualización \ tau _ {2} = \ gamma e}$
${\displaystyle \Gamma (\lambda ve)=\tau \rightarrow \tau _{e))$ - en el caso de que , donde sea con la unión añadida . ${\ estilo de visualización \ tau _ {e} = \ Gamma 'e}$ $\gamma '$ $\Gama$ $v:\tau$

En estas reglas, un símbolo es un conjunto de asociaciones entre variables y sus tipos: $\Gama$

$\Gamma =v_{{1}}:A_{{1}},v_{{2}}:A_{{2}},\ldots ,v_{{n}}:A_{{n}}$

Resolver un sistema de ecuaciones

La solución del sistema de ecuaciones construido se basa en el algoritmo de unificación . Este es un algoritmo bastante simple. Hay alguna función que toma una ecuación de tipos como entrada y devuelve una sustitución que hace que los lados izquierdo y derecho de la ecuación sean iguales ("los unifica"). La sustitución es simplemente una proyección de tipos variables sobre los tipos mismos. Tales sustituciones se pueden calcular de varias formas, que dependen de la implementación específica del algoritmo de Hindley-Milner. $tu$

Véase también

Notas

Comentarios

↑ soporte agregado en Java SE 10

Fuentes

↑ Andrew W. Appel. Una crítica del ML estándar. — Universidad de Princeton, versión revisada de CS-TR-364-92, 1992.
↑ Michal Moskal. Escriba Inferencia con aplazamiento . — 2005.

Enlaces

Implementando el Algoritmo Hindley-Milner en Perl
Mensaje de correo electrónico archivado de Roger Hindley, explica la historia de la inferencia de tipos
Inferencia de tipos polimórficos de Michael Schwartzbach, ofrece una descripción general de la inferencia de tipos polimórficos.
Principales esquemas tipográficos para programas funcionales. Una copia recompuesta del artículo de Damas y Milner que describía las pruebas de integridad y solidez.
Tutorial e implementación completa en Standard ML El tutorial incluye parte de la historia lógica de los sistemas de tipos, así como una descripción detallada del algoritmo implementado. Se corrigen algunos errores tipográficos en el artículo original de Damas Milner.
Artículo básico de verificación de tipos de Luca Cardelli, describe el algoritmo, incluye implementación en Modula-2
Implementación de la inferencia de tipo Hindley-Milner en Scala , por Andrew Forrest (consultado el 30 de julio de 2009)
Implementación de Hindley-Milner en Perl 5, por Nikita Borisov (enlace no disponible) . Fecha de acceso: 12 de marzo de 2009. Archivado desde el original el 18 de febrero de 2007. (indefinido)
¿Qué es Hindley-Milner? (¿y por qué es genial?) Explica Hindley-Milner, ejemplos en Scala
http://fprog.ru/2010/issue5/roman-dushkin-hindley-milner/ Modelo de escritura Hindley-Milner y un ejemplo de su implementación en Haskell