Inferencia de tipo

En teoría de tipos , la inferencia de tipos (a veces llamada reconstrucción de tipos ) es la detección automática del tipo de una expresión . ^{[ 1 ]}^{: 320} Esto incluye 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 .

La tipabilidad se usa a veces como sinónimo de inferencia de tipos; sin embargo, algunos autores distinguen entre la tipabilidad como un problema de decisión (que tiene una respuesta de sí/no) y la inferencia de tipos como el cálculo de un tipo real para un término. ^{[ 2 ]}

Explicación no técnica

En un lenguaje tipado, el tipo de un término determina las formas en que puede o no usarse. Por ejemplo, consideremos el inglés y los términos que podrían completar la frase "sing _". El término "a song" es de tipo cantable, por lo que podría colocarse en el espacio en blanco para formar una frase con sentido: "sing a song". Por otro lado, el término "a friend" no es cantable, así que "sing a friend" carece de sentido. En el mejor de los casos, podría ser una metáfora; la flexibilidad en las reglas tipográficas 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 creación 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 el lenguaje común, nos sorprendería que "escribir una canción" significara escribirle una carta a una canción o que "escribir a un amigo" significara redactar una carta a un amigo.

Los términos con diferentes tipos pueden incluso referirse a la misma cosa. 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 tipados se utilizan a menudo para evitar que un objeto se considere demasiado general. Por ejemplo, si el sistema de tipos trata todos los números como iguales, un programador que accidentalmente escribe código donde 4debería significar "4 segundos" pero se interpreta como "4 metros" no se percataría de su error hasta que este 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 un tipado más preciso ofrece varias maneras de resolver la paradoja. De hecho, la paradoja de Russell impulsó las primeras versiones de la teoría de tipos.

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

El tipo de palabra podría provenir de fuera del texto. Por ejemplo, si un hablante se refiere a "una canción" en inglés, generalmente no necesita decirle al oyente que "una canción" es cantable y compositiva; esa información forma parte de su conocimiento previo compartido.
El tipo se puede declarar explícitamente. Por ejemplo, un programador podría escribir una instrucción como en 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 instrucción no solo asigna el valor , sino que la parte también indica que el tipo de es una cantidad de tiempo en segundos.delay: seconds := 4delay4delay: secondsdelay
El tipo se puede inferir del contexto. Por ejemplo, en la frase "Lo compré por una ganga", podemos observar que intentar asignarle al término "canción" tipos como "cantable" y "componible" resultaría absurdo, mientras que el tipo "cantidad de dinero" funciona. Por lo tanto, sin necesidad de que se nos diga, concluimos que "canción" aquí debe significar "poco o nada", como en la expresión inglesa " for a song" (por una ganga ), no "una pieza musical, generalmente con letra".

Especialmente en los lenguajes de programación, puede que la computadora no disponga de mucho conocimiento previo compartido. En los lenguajes con tipado manifiesto , esto significa que la mayoría de los tipos deben declararse explícitamente. La inferencia de tipos busca aliviar esta carga, liberando al programador de la necesidad de declarar tipos que la computadora debería poder deducir del contexto.

Verificación de tipos frente a inferencia de tipos

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

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

E : T? En este caso, se proporcionan tanto una expresión E como un tipo T. Ahora bien, ¿es E realmente un T? Este escenario se conoce como verificación de tipos .
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 .
_ : T? Al revés. Dado solo un tipo, ¿hay alguna expresión para él o el tipo no tiene valores? ¿Hay algún ejemplo de un T? Esto se conoce como habitabilidad de tipos .

Para el cálculo lambda con tipado simple , las tres preguntas son decidibles . La situación no es tan favorable cuando se permiten tipos más expresivos .

Tipos en los lenguajes de programación

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 C (desde C23 ), ^{[ 3 ]} C++ (desde C++11 ), ^{[ 4 ]} C# (a partir de la versión 3.0), Chapel , Clean , Crystal , D , Dart , ^{[ 5 ]} F# , ^{[ 6 ]} FreeBASIC , Go , Haskell , Java (a partir de la versión 10), Julia , ^{[ 7 ]} Kotlin , ^{[ 8 ]} ML , Nim , OCaml , Opa , Q#, RPython , Rust , ^{[ 9 ]} Scala , ^{[ 10 ]} Swift , ^{[ 11 ]} TypeScript , ^{[ 12 ]} Vala , ^{[ 13 ]} Zig y Visual Basic ^{[ 14 ]} (a partir de la versión 9.0). La mayoría utiliza una forma sencilla de inferencia de tipos; el sistema de tipos Hindley-Milner ofrece una inferencia más completa. La capacidad de inferir tipos automáticamente facilita muchas tareas de programación, permitiendo al programador omitir las anotaciones de tipo sin dejar de realizar la verificación de tipos.

En algunos lenguajes de programación, todos los valores tienen un tipo de dato 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 las funciones y las variables locales normalmente deben proporcionarse explícitamente mediante anotaciones de tipo. Por ejemplo, en ANSI C :

int incremento ( int x ) { int resultado ; // declarar resultado enteroresultado = x + 1 ; devolver resultado ; }

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

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

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 que resulty xtienen tipo entero ya que la constante 1es de tipo entero, y por lo tanto que increment()es una función int -> int. La variable result2no se usa de manera válida, 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, a falta de información en contrario, +toma dos enteros y devuelve un entero. (Así es como funciona, por ejemplo, en OCaml ). A partir de esto, el inferidor de tipos puede inferir que el tipo de x + 1es un entero, lo que significa que resultes 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 siguiente línea, result2se calcula sumando un decimal 1.0con aritmética de punto flotante , lo que provoca un conflicto en el uso de xpara expresiones tanto enteras 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, punto flotante. Sin embargo, esto puede tener implicaciones perjudiciales; por ejemplo, usar 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 retroceder y, en su lugar, generan un mensaje de error en tales situaciones. Este comportamiento puede ser preferible, ya que la inferencia de tipos no siempre es algorítmicamente neutral, como lo ilustra el problema anterior de la precisión de punto flotante.

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

Por último, una desventaja importante de los algoritmos complejos de inferencia de tipos es que la resolución de la inferencia de tipos resultante no será obvia para los humanos (sobre todo debido al retroceso), lo que puede ser perjudicial, ya que el código está pensado principalmente para ser comprensible para los humanos.

La reciente aparición de la compilación justo a tiempo permite enfoques híbridos donde el tipo de argumentos proporcionados por los distintos contextos de llamada se conoce en tiempo de compilación, y puede generar un gran número de versiones compiladas de la misma función. Cada versión compilada puede luego optimizarse para un conjunto diferente de tipos. Por ejemplo, la compilación JIT permite que haya al menos dos versiones compiladas de increment():

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

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

Descripción técnica

La inferencia de tipos es la capacidad de deducir automáticamente, parcial o totalmente, el tipo de una expresión en tiempo de compilación. El compilador suele ser capaz de inferir el tipo de una variable o la firma de tipo de una función, sin necesidad de 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 robusto o si el programa o el lenguaje son lo suficientemente sencillos.

Para obtener la información necesaria para inferir el tipo de una expresión, el compilador la recopila mediante la agregación y posterior reducción de las anotaciones de tipo asignadas a sus subexpresiones, o bien mediante la comprensión implícita del tipo de diversos valores atómicos (por ejemplo, true : booleano; 42 : entero; 3.14159 : real; etc.). Es gracias al reconocimiento de la eventual reducción de las expresiones a valores atómicos con tipo implícito que el compilador de un lenguaje con 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 tipos con recursión polimórfica es indecidible. Además, las anotaciones de tipo explícitas pueden usarse para optimizar el código al obligar al compilador a usar un tipo más específico (más rápido/más pequeño) que el que había inferido. ^{[ 15 ]}

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

Ejemplo de alto nivel

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

map f [] = [] map f ( first : rest ) = f first : map f rest

(Recordemos que :en Haskell denota cons , que estructura un elemento inicial y el final de una lista en una lista más grande, o desestructura una lista no vacía en su elemento inicial y su final. No denota "de tipo" como en matemáticas y en otras partes de este artículo; en Haskell, ese operador "de tipo" se escribe ::en su lugar).

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 ser de 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 el tipo , correspondiente al 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::emapff[e]

Al juntar las partes se obtiene . 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 es también el tipo más general, ya que no se aplican restricciones adicionales. Como el tipo inferido mapes paramétricamente polimórfico , el tipo de los argumentos y resultados fno se infiere, sino que se deja como variables de tipo, por lo que mapse puede aplicar a funciones y listas de varios tipos, siempre que los tipos reales coincidan en cada invocación.

Ejemplo detallado

Los algoritmos utilizados por programas como los compiladores son equivalentes al razonamiento informalmente estructurado descrito anteriormente, pero un poco más detallados y metódicos. Los detalles exactos dependen del algoritmo de inferencia elegido (véase la siguiente sección para conocer el algoritmo más conocido), pero el ejemplo que se muestra a continuación ilustra la idea general. Comenzamos nuevamente con la definición de map:

map f [] = [] map f ( first : rest ) = f first : map f rest

(Recuerde de nuevo que :aquí se trata del constructor de listas de Haskell, no del operador "de tipo", que Haskell escribe como ::.)

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

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

Luego creamos nuevas variables de tipo para las subexpresiones construidas 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 un y una lista de y devuelve un .mapf[]α ~ β -> [γ] -> κ~αmapβγκ
λdenotará el tipo de . Concluimos que .(first:rest)ζ -> [ζ] -> [ζ] ~ η -> θ -> λ
μdenotará el tipo de . Concluimos que .mapf(first:rest)α ~ ε -> λ -> μ
νdenotará el tipo de . Concluimos que .ffirstε ~ η -> ν
ξdenotará el tipo de . Concluimos que .mapfrestα ~ ε -> θ -> ξ
οdenotará el tipo de . Concluimos que .ffirst:mapfrestι -> [ι] -> [ι] ~ ν -> ξ -> ο

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:

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

Luego sustituimos hasta que no se puedan eliminar más variables. El orden exacto es irrelevante; si el código pasa la verificación de tipos, cualquier orden conducirá a la misma forma final. Comencemos sustituyendo οpor μ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 poder recuperarnos αal final:

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

Y, finalmente, sustituir (ζ -> ι)por β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 estos detalles.map::(a->b)->[a]->[b]

Algoritmo de inferencia tipo Hindley-Milner

El algoritmo utilizado inicialmente para realizar la inferencia de tipos se denomina informalmente algoritmo de Hindley-Milner, aunque debería atribuirse correctamente a Damas y Milner. ^{[ 18 ]} También se le conoce tradicionalmente como 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 con tipos simples , ideado por Haskell Curry y Robert Feys en 1958. 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 ^[¹⁹^] , independientemente del trabajo de Hindley, proporcionó un algoritmo equivalente, el Algoritmo W. En 1982, Luis Damas ^[¹⁸^] finalmente demostró que el algoritmo de Milner es completo y lo extendió para admitir sistemas con referencias polimórficas.

Efectos secundarios del uso del tipo más general

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 inestables, donde 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 coma flotante se consideran generalizaciones de los tipos enteros. En realidad, la aritmética de coma flotante presenta problemas de precisión y desbordamiento diferentes a los de los enteros.
Los tipos variantes/dinámicos se consideran generalizaciones de otros tipos cuando esto afecta la selección de sobrecargas de operadores. Por ejemplo, el +operador puede sumar enteros, pero puede concatenar variantes como cadenas, incluso si dichas variantes contienen enteros.