Inferencia de tipos

La inferencia de tipos , a veces llamada reconstrucción de tipos , ^{[1] : 320} se refiere a la detección automática del tipo de una expresión en un lenguaje formal . Estos incluyen lenguajes de programación y sistemas de tipos matemáticos , pero también lenguajes naturales en algunas ramas de la informática y la lingüística .

En un lenguaje tipificado, el tipo de un término determina las formas en que puede o no usarse en ese idioma. Por ejemplo, considere el idioma inglés y los términos que podrían llenar el espacio en blanco en la frase "cantar _". El término "una canción" es de tipo cantable, por lo que podría colocarse en el espacio en blanco para formar una frase con sentido: "cantar una canción". Por otro lado, el término "un amigo" no tiene el tipo cantable, por lo que "cantar a un amigo" es un sinsentido. En el mejor de los casos, podría ser una metáfora; la evasión de las reglas de tipo es una característica del lenguaje poético.

El tipo de un término también puede afectar la interpretación de las operaciones que lo involucran. Por ejemplo, "una canción" es de tipo componible, por lo que lo interpretamos como la cosa creada en la frase "escribir una canción". Por otro lado, "un amigo" es de tipo destinatario, por lo que lo interpretamos como el destinatario en la frase "escribir a un amigo". En lenguaje normal, nos sorprendería si "escribir una canción" significara dirigir una carta a una canción o "escribir a un amigo" significara redactar un borrador de un amigo en un papel.

Los términos con diferentes tipos pueden incluso referirse materialmente a lo mismo. Por ejemplo, interpretaríamos "colgar el tendedero" como ponerlo en uso, pero "colgar la correa" como guardarla, aunque, en contexto, tanto "tendedero" como "correa" podrían referirse a la misma cuerda, solo que en momentos diferentes.

Los tipos se utilizan a menudo para evitar que un objeto se considere de forma demasiado general. Por ejemplo, si el sistema de tipos trata todos los números como iguales, un programador que accidentalmente escribe código donde 4se supone que significa "4 segundos" pero se interpreta como "4 metros" no recibiría ninguna advertencia de su error hasta que causara problemas en tiempo de ejecución. Al incorporar unidades al sistema de tipos, estos errores se pueden detectar mucho antes. Como otro ejemplo, la paradoja de Russell surge cuando cualquier cosa puede ser un elemento de un conjunto y cualquier predicado puede definir un conjunto, pero una tipificación más cuidadosa ofrece varias formas de resolver la paradoja. De hecho, la paradoja de Russell dio origen a las primeras versiones de la teoría de tipos.

Hay varias formas en que un término puede obtener su tipo:

• El tipo puede provenir de algún lugar externo al pasaje. Por ejemplo, si un hablante hace referencia a "una canción" en inglés, por lo general no tiene que decirle al oyente que "una canción" se puede cantar y componer; esa información es parte de su conocimiento previo compartido.
• El tipo se puede declarar explícitamente. Por ejemplo, un programador podría escribir una declaración como delay: seconds := 4en su código, donde los dos puntos son el símbolo matemático convencional para marcar un término con su tipo. Es decir, esta declaración no solo establece delayel valor 4, sino que la delay: secondsparte también indica que delayel tipo de es una cantidad de tiempo en segundos.
• El tipo se puede inferir del contexto. Por ejemplo, en la frase "lo compré por una canción", podemos observar que intentar darle al término "una canción" tipos como "cantable" y "componible" llevaría a un sinsentido, mientras que el tipo "cantidad de dinero" sí funciona. Por lo tanto, sin necesidad de que nos lo digan, concluimos que "canción" aquí debe significar "poco o nada", como en la expresión inglesa " por una canción ", no "una pieza musical, generalmente con letra".

Especialmente en los lenguajes de programación, puede que no haya mucho conocimiento previo compartido disponible para la computadora. En los lenguajes de tipado manifiesto , esto significa que la mayoría de los tipos deben declararse explícitamente. La inferencia de tipos tiene como objetivo aliviar esta carga, liberando al autor de la obligación de declarar tipos que la computadora debería poder deducir del contexto.

En una tipificación, una expresión E se opone a un tipo T, escrito formalmente como E : T. Normalmente, una tipificación solo tiene sentido dentro de algún contexto, que se omite aquí.

En este contexto, las siguientes preguntas revisten especial interés:

1. E : T? En este caso, se dan tanto una expresión E como un tipo T. Ahora bien, ¿es E realmente una T? Este escenario se conoce como verificación de tipos .
2. E : _? Aquí, solo se conoce la expresión. Si hay una manera de derivar un tipo para E, entonces hemos logrado la inferencia de tipos .
3. _ : T? Al revés. Dado solo un tipo, ¿existe alguna expresión para él o el tipo no tiene valores? ¿Existe algún ejemplo de una T? Esto se conoce como inhabitación de tipo .

En el caso del cálculo lambda de tipos simples , las tres preguntas son decidibles . La situación no es tan cómoda cuando se permiten tipos más expresivos .

This section needs additional citations for verification. Please help improve this article by adding citations to reliable sources in this section. Unsourced material may be challenged and removed. (November 2020) (Learn how and when to remove this message)

Los tipos son una característica presente en algunos lenguajes fuertemente tipados estáticamente . A menudo es característico de los lenguajes de programación funcional en general. Algunos lenguajes que incluyen inferencia de tipos incluyen C23 , ^[2] C++11 , ^[3] C# (a partir de la versión 3.0), Chapel , Clean , Crystal , D , F# , ^[4] FreeBASIC , Go , Haskell , Java (a partir de la versión 10), Julia , ^[5] Kotlin , ^[6] ML , Nim , OCaml , Opa , Q#, RPython , Rust , ^[7] Scala , ^[8] Swift , ^[9] TypeScript , ^[10] Vala , ^[11] Dart , ^[12] y Visual Basic ^[13] (a partir de la versión 9.0). La mayoría de ellos utilizan una forma simple de inferencia de tipos; el sistema de tipos Hindley–Milner puede proporcionar una inferencia de tipos más completa. La capacidad de inferir tipos automáticamente facilita muchas tareas de programación, dejando al programador libre de omitir las anotaciones de tipos y al mismo tiempo permitiendo la verificación de tipos.

En algunos lenguajes de programación, todos los valores tienen un tipo de datos declarado explícitamente en tiempo de compilación , lo que limita los valores que una expresión particular puede tomar en tiempo de ejecución . Cada vez más, la compilación justo a tiempo difumina la distinción entre tiempo de ejecución y tiempo de compilación. Sin embargo, históricamente, si el tipo de un valor se conoce solo en tiempo de ejecución, estos lenguajes son de tipado dinámico . En otros lenguajes, el tipo de una expresión se conoce solo en tiempo de compilación ; estos lenguajes son de tipado estático . En la mayoría de los lenguajes de tipado estático, los tipos de entrada y salida de funciones y variables locales normalmente deben proporcionarse explícitamente mediante anotaciones de tipo. Por ejemplo, en ANSI C :

int add_one ( int x ) { int resultado ; /* declarar resultado entero */       resultado = x + 1 ; devolver resultado ; }      

La firma de esta definición de función, int add_one(int x), declara que add_onees una función que toma un argumento, un entero , y devuelve un entero. int result;declara que la variable local resultes un entero. En un lenguaje hipotético que admita la inferencia de tipos, el código podría escribirse así:

add_one ( x ) { var result ; /* variable de tipo inferido result */ var result2 ; /* variable de tipo inferido result #2 */        result = x + 1 ; result2 = x + 1.0 ; /* esta línea no funcionará (en el lenguaje propuesto) */ return result ; }            

Esto es idéntico a cómo se escribe el código en el lenguaje Dart , excepto que está sujeto a algunas restricciones adicionales como se describe a continuación. Sería posible inferir los tipos de todas las variables en tiempo de compilación. En el ejemplo anterior, el compilador inferiría eso resulty xtendría el tipo entero ya que la constante 1es de tipo entero y, por lo tanto, add_onees una función int -> int. La variable result2no se usa de manera legal, por lo que no tendría un tipo.

En el lenguaje imaginario en el que está escrito el último ejemplo, el compilador asumiría que, en ausencia de información que indique lo contrario, +toma dos enteros y devuelve un entero. (Así es como funciona, por ejemplo, en OCaml ). A partir de esto, el inferenciador de tipos puede inferir que el tipo de x + 1es un entero, lo que significa resultque es un entero y, por lo tanto, el valor de retorno de add_onees un entero. De manera similar, dado que +requiere que ambos argumentos sean del mismo tipo, xdebe ser un entero y, por lo tanto, add_oneacepta un entero como argumento.

Sin embargo, en la línea siguiente, result2 se calcula añadiendo un decimal 1.0con aritmética de punto flotante , lo que provoca un conflicto en el uso de xpara expresiones tanto de números enteros como de punto flotante. El algoritmo de inferencia de tipos correcto para tal situación se conoce desde 1958 y se sabe que es correcto desde 1982. Revisa las inferencias anteriores y utiliza el tipo más general desde el principio: en este caso, el punto flotante. Sin embargo, esto puede tener implicaciones perjudiciales; por ejemplo, utilizar un punto flotante desde el principio puede introducir problemas de precisión que no habrían existido con un tipo entero.

Sin embargo, con frecuencia se utilizan algoritmos de inferencia de tipos degenerados que no pueden dar marcha atrás y, en su lugar, generan un mensaje de error en esa situación. Este comportamiento puede ser preferible, ya que la inferencia de tipos puede no ser siempre neutral desde el punto de vista algorítmico, como lo ilustra el problema de precisión de punto flotante anterior.

Un algoritmo de generalidad intermedia declara implícitamente result2 como una variable de punto flotante, y la suma convierte implícitamente xa un punto flotante. Esto puede ser correcto si los contextos de llamada nunca suministran un argumento de punto flotante. Tal situación muestra la diferencia entre la inferencia de tipo , que no implica la conversión de tipo , y la conversión de tipo implícita , que fuerza los datos a un tipo de datos diferente, a menudo sin restricciones.

Finalmente, una desventaja significativa del algoritmo de inferencia de tipos complejo es que la resolución de la inferencia de tipos resultante no será obvia para los humanos (especialmente debido al retroceso), lo que puede ser perjudicial ya que el código está destinado principalmente a ser comprensible para los humanos.

La reciente aparición de la compilación en tiempo real permite enfoques híbridos en los que el tipo de argumentos suministrados por los diversos contextos de llamada se conoce en el momento de la compilación y puede generar una gran cantidad de versiones compiladas de la misma función. Cada versión compilada se puede optimizar para un conjunto diferente de tipos. Por ejemplo, la compilación JIT permite que haya al menos dos versiones compiladas de add_one :

Una versión que acepta una entrada entera y utiliza conversión de tipo implícita.

Una versión que acepta un número de punto flotante como entrada y utiliza instrucciones de punto flotante en todo momento.

La inferencia de tipos es la capacidad de deducir automáticamente, ya sea parcial o totalmente, el tipo de una expresión en tiempo de compilación. El compilador suele poder inferir el tipo de una variable o la signatura de tipo de una función sin necesidad de que se hayan proporcionado anotaciones de tipo explícitas. En muchos casos, es posible omitir por completo las anotaciones de tipo de un programa si el sistema de inferencia de tipos es lo suficientemente sólido o el programa o lenguaje es lo suficientemente simple.

Para obtener la información necesaria para inferir el tipo de una expresión, el compilador reúne esta información como un agregado y una reducción posterior de las anotaciones de tipo dadas para sus subexpresiones, o mediante una comprensión implícita del tipo de varios valores atómicos (por ejemplo, true: Bool; 42: Integer; 3.14159: Real; etc.). Es a través del reconocimiento de la reducción final de las expresiones a valores atómicos tipados implícitamente que el compilador de un lenguaje de inferencia de tipos puede compilar un programa completamente sin anotaciones de tipo.

En formas complejas de programación de orden superior y polimorfismo , no siempre es posible que el compilador infiera tanto, y las anotaciones de tipo son ocasionalmente necesarias para la desambiguación. Por ejemplo, se sabe que la inferencia de tipo con recursión polimórfica es indecidible. Además, las anotaciones de tipo explícitas se pueden utilizar para optimizar el código al obligar al compilador a utilizar un tipo más específico (más rápido/más pequeño) del que había inferido. ^[14]

Algunos métodos de inferencia de tipos se basan en la satisfacción de restricciones ^[15] o en teorías de módulo de satisfacibilidad ^[16] .

A modo de ejemplo, la función Haskellmap aplica una función a cada elemento de una lista y puede definirse como:

mapa f [] = [] mapa f ( primero : resto ) = f primero : mapa f resto             

(Recuerde que :en Haskell denota cons , estructurando un elemento principal y una cola de lista en una lista más grande o desestructurando una lista no vacía en su elemento principal y su cola. No denota "de tipo" como en matemáticas y en otras partes de este artículo; en Haskell se escribe ::en su lugar ese operador "de tipo").

La inferencia de tipos en la mapfunción procede de la siguiente manera. mapes una función de dos argumentos, por lo que su tipo está restringido a tener la forma . En Haskell, los patrones y siempre coinciden con listas, por lo que el segundo argumento debe ser un tipo de lista: para algún tipo . Su primer argumento se aplica al argumento , que debe tener tipo , correspondiente con el tipo en el argumento de lista, por lo que ( significa "es de tipo") para algún tipo . El valor de retorno de , finalmente, es una lista de lo que produce, por lo que .a -> b -> c[](first:rest)b = [d]dffirstdf :: d -> e::emap ff[e]

Juntar las partes conduce a . No hay nada especial en las variables de tipo, por lo que se puede volver a etiquetar comomap :: (d -> e) -> [d] -> [e]

mapa :: ( a -> b ) -> [ a ] ​​-> [ b ]        

Resulta que este también es el tipo más general, ya que no se aplican más restricciones. Como el tipo inferido de mapes paramétricamente polimórfico , el tipo de los argumentos y resultados de fno se infiere, sino que se dejan como variables de tipo y, por lo tanto, mapse pueden aplicar a funciones y listas de varios tipos, siempre que los tipos reales coincidan en cada invocación.

Los algoritmos que utilizan los programas, como los compiladores, son equivalentes al razonamiento informal estructurado que se ha descrito anteriormente, pero un poco más detallado y metódico. Los detalles exactos dependen del algoritmo de inferencia elegido (consulte la siguiente sección para conocer el algoritmo más conocido), pero el ejemplo que se muestra a continuación ofrece una idea general. Empezamos de nuevo con la definición de map:

mapa f [] = [] mapa f ( primero : resto ) = f primero : mapa f resto             

(Nuevamente, recuerda que :aquí se encuentra el constructor de lista de Haskell, no el operador "de tipo", que Haskell escribe ::.)

Primero, creamos nuevas variables de tipo para cada término individual:

• αdenotará el tipo mapque queremos inferir.
• βdenotará el tipo de fen la primera ecuación.
• [γ]deberá denotar el tipo de []en el lado izquierdo de la primera ecuación.
• [δ]deberá denotar el tipo de []en el lado derecho de la primera ecuación.
• εdenotará el tipo de fen la segunda ecuación.
• ζ -> [ζ] -> [ζ]denotará el tipo de :en el lado izquierdo de la primera ecuación. (Este patrón se conoce por su definición).
• ηdenotará el tipo de first.
• θdenotará el tipo de rest.
• ι -> [ι] -> [ι]deberá denotar el tipo de :en el lado derecho de la primera ecuación.

Luego, creamos nuevas variables de tipo para las subexpresiones creadas a partir de estos términos, restringiendo el tipo de la función que se invoca en consecuencia:

• κdenotará el tipo de . Concluimos que donde el símbolo "similar" significa "se unifica con"; estamos diciendo que , el tipo de , debe ser compatible con el tipo de una función que toma a y una lista de s y devuelve a .map f []α ~ β -> [γ] -> κ~αmapβγκ
• λdenotará el tipo de . Concluimos que .(first:rest)ζ -> [ζ] -> [ζ] ~ η -> θ -> λ
• μdenotará el tipo de . Concluimos que .map f (first:rest)α ~ ε -> λ -> μ
• νdenotará el tipo de . Concluimos que .f firstε ~ η -> ν
• ξdenotará el tipo de . Concluimos que .map f restα ~ ε -> θ -> ξ
• οdenotará el tipo de . Concluimos que .f first : map f restι -> [ι] -> [ι] ~ ν -> ξ -> ο

También restringimos los lados izquierdo y derecho de cada ecuación para que se unifiquen entre sí: κ ~ [δ]y μ ~ ο. En total, el sistema de unificaciones a resolver es:

α ~ β -> [γ] -> κζ -> [ζ] -> [ζ] ~ η -> θ -> λα ~ ε -> λ -> με ~ η -> να ~ ε -> θ -> ξι -> [ι] -> [ι] ~ ν -> ξ -> οκ ~ [δ]μ ~ ο

Luego sustituimos hasta que no se puedan eliminar más variables. El orden exacto es irrelevante; si el código verifica el tipo, cualquier orden conducirá a la misma forma final. Comencemos sustituyendo y οpor :μ[δ]κ

α ~ β -> [γ] -> [δ]ζ -> [ζ] -> [ζ] ~ η -> θ -> λα ~ ε -> λ -> οε ~ η -> να ~ ε -> θ -> ξι -> [ι] -> [ι] ~ ν -> ξ -> ο

Sustituyendo ζpor η, [ζ]por θy λ, ιpor ν, y [ι]por ξy ο, todo es posible porque un constructor de tipo como es invertible en sus argumentos:· -> ·

α ~ β -> [γ] -> [δ]α ~ ε -> [ζ] -> [ι]ε ~ ζ -> ι

Sustituyendo ζ -> ιpor εy β -> [γ] -> [δ]por α, manteniendo la segunda restricción para que podamos recuperarnos αal final:

α ~ (ζ -> ι) -> [ζ] -> [ι]β -> [γ] -> [δ] ~ (ζ -> ι) -> [ζ] -> [ι]

Y, finalmente, sustituyendo (ζ -> ι)así βcomo ζpor γy ιpor δporque un constructor de tipo como es invertible elimina todas las variables específicas de la segunda restricción:[·]

α ~ (ζ -> ι) -> [ζ] -> [ι]

No son posibles más sustituciones y el reetiquetado nos da lo mismo que encontramos sin entrar en detalles.map :: (a -> b) -> [a] -> [b]

El algoritmo que se utilizó por primera vez para realizar la inferencia de tipos se denomina ahora informalmente algoritmo Hindley-Milner, aunque el algoritmo debería atribuirse correctamente a Damas y Milner. ^[17] También se lo denomina tradicionalmente reconstrucción de tipos . ^{[1] : 320} Si un término está bien tipificado de acuerdo con las reglas de tipificación de Hindley-Milner, entonces las reglas generan una tipificación principal para el término. El proceso de descubrir esta tipificación principal es el proceso de "reconstrucción".

El origen de este algoritmo es el algoritmo de inferencia de tipos para el cálculo lambda de tipos simples que fue ideado por Haskell Curry y Robert Feys en 1958. ^{[ cita requerida ]} En 1969 J. Roger Hindley extendió este trabajo y demostró que su algoritmo siempre infería el tipo más general. En 1978 Robin Milner , ^[18] independientemente del trabajo de Hindley, proporcionó un algoritmo equivalente, Algorithm W. En 1982 Luis Damas ^[17] finalmente demostró que el algoritmo de Milner es completo y lo extendió para soportar sistemas con referencias polimórficas.

Por diseño, la inferencia de tipos inferirá el tipo más general apropiado. Sin embargo, muchos lenguajes, especialmente los lenguajes de programación más antiguos, tienen sistemas de tipos ligeramente poco sólidos, en los que el uso de tipos más generales puede no ser siempre neutral desde el punto de vista algorítmico. Algunos casos típicos incluyen:

• Los tipos de punto flotante se consideran generalizaciones de los tipos enteros. En realidad, la aritmética de punto flotante tiene diferentes problemas de precisión y ajuste que los de los números enteros.
• Los tipos variantes o dinámicos se consideran generalizaciones de otros tipos en los casos en que esto afecta la selección de sobrecargas de operadores. Por ejemplo, el +operador puede sumar números enteros, pero puede concatenar variantes como cadenas, incluso si esas variantes contienen números enteros.

Los algoritmos de inferencia de tipos se han utilizado para analizar lenguajes naturales , así como lenguajes de programación. ^{[19] [20] [21]} Los algoritmos de inferencia de tipos también se utilizan en algunos sistemas de inducción gramatical ^{[22] [23]} y de gramática basada en restricciones para lenguajes naturales. ^[24]

• Mensaje de correo electrónico archivado de Roger Hindley, que 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.
• Artículo de Luca Cardelli sobre verificación de tipos básica, que describe el algoritmo e incluye la implementación en Modula-2
• Implementación de la inferencia de tipos 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 en Wayback Machine (archivado el 18 de febrero de 2007)
• ¿Qué es Hindley-Milner? (¿Y por qué es genial?) Explicación de Hindley-Milner, ejemplos en Scala