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 .
Los tipos en una visión más general pueden asociarse a un uso designado, sugiriendo y restringiendo las actividades posibles para un objeto de ese tipo. Muchos sustantivos en el lenguaje especifican tales usos. Por ejemplo, la palabra correa indica un uso diferente al de la palabra línea . Llamar a algo mesa indica una designación diferente a la de llamarlo leña , aunque materialmente podría ser lo mismo. Si bien sus propiedades materiales hacen que las cosas sean utilizables para algunos propósitos, también están sujetas a designaciones particulares. Este es especialmente el caso en campos abstractos, como las matemáticas y la informática, donde el material finalmente son sólo bits o fórmulas.
Para excluir usos no deseados, pero materialmente posibles, el concepto de tipos se define y se aplica en muchas variaciones. En matemáticas, la paradoja de Russell provocó las primeras versiones de la teoría de tipos. En los lenguajes de programación, los ejemplos típicos son los "errores de tipo", por ejemplo, ordenar a una computadora que sume valores que no son números. Aunque materialmente posible, el resultado ya no sería significativo y tal vez desastroso para el proceso en general.
En una mecanografía , una expresión se opone a un tipo. Por ejemplo, , y son términos separados con el tipo de números naturales . Tradicionalmente, la expresión va seguida de dos puntos y su tipo, como por ejemplo . Esto significa que el valor es de tipo . Esta forma también se utiliza para declarar nuevos nombres, por ejemplo , de forma muy parecida a introducir un nuevo personaje en una escena con las palabras "detective Decker".
A diferencia de una historia donde las designaciones se desarrollan lentamente, en los lenguajes formales los objetos a menudo tienen que definirse con su tipo desde el principio. Además, si las expresiones son ambiguas, es posible que se necesiten tipos para hacer explícito el uso previsto. Por ejemplo, la expresión podría tener un tipo pero también podría leerse como un número racional o real o incluso como texto sin formato .
Como consecuencia, los programas o pruebas pueden estar tan sobrecargados de tipos que es deseable deducirlos del contexto. Esto puede ser posible recopilando los usos de expresiones sin tipo (incluidos nombres no definidos). Si, por ejemplo, se utiliza un nombre n aún no definido en una expresión , se podría concluir que n es al menos un número. El proceso de deducir el tipo a partir de una expresión y su contexto es inferencia de tipos .
En general, no sólo los objetos, sino también las actividades tienen tipos y pueden introducirse simplemente por su uso. Para una historia de Star Trek , una actividad tan desconocida podría ser "radiante", que por el bien del flujo de la historia simplemente se ejecuta y nunca se presenta formalmente. Sin embargo, se puede deducir su tipo (transporte) según lo que suceda. Además, tanto objetos como actividades se pueden construir a partir de sus partes. En tal entorno, la inferencia de tipos no sólo puede volverse más compleja, sino también más útil, ya que permite recopilar una descripción completa de todo lo que hay en una escena compuesta, sin dejar de ser capaz de detectar usos conflictivos o no deseados.
En una tipificación, una expresión E se opone a un tipo T, escrito formalmente como E : T. Por lo general, una tipificación sólo tiene sentido dentro de algún contexto, que se omite aquí.
En este contexto, las siguientes preguntas son de particular interés:
Para el cálculo lambda escrito simplemente , las tres preguntas son decidibles . La situación no es tan cómoda cuando se permiten tipos más expresivos .
Los tipos son una característica presente en algunos lenguajes fuertemente tipados estáticamente . Suele ser característico de los lenguajes de programación funcionales 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 con 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 la libertad de omitir anotaciones de tipo y al mismo tiempo permitir 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 adoptar en tiempo de ejecución . Cada vez más, la compilación justo a tiempo desdibuja 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 sólo en tiempo de ejecución, estos lenguajes se escriben dinámicamente . En otros lenguajes, el tipo de expresión sólo se conoce en el momento de la compilación ; Estos lenguajes están tipificados estáticamente . En la mayoría de los lenguajes de tipo 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 ; resultado de retorno ; } 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 número entero , y devuelve un número entero. int result;declara que la variable local resultes un número entero. En un lenguaje hipotético que admita la inferencia de tipos, el código podría escribirse así:
add_one ( x ) { var resultado ; /* resultado de variable de tipo inferido */ var resultado2 ; /* resultado variable de tipo inferido #2 */ resultado = x + 1 ; resultado2 = x + 1,0 ; /* esta línea no funcionará (en el idioma 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 el momento de la compilación. En el ejemplo anterior, el compilador inferiría eso resulty xtendría un 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 en contrario, +toma dos números enteros y devuelve un número entero. (Así es como funciona, por ejemplo, OCaml ). A partir de esto, el inferenciador de tipos puede inferir que el tipo de x + 1es un número entero, lo que significa resultque es un número entero y, por lo tanto, el valor de retorno de add_onees un número entero. De manera similar, dado que +requiere que ambos argumentos sean del mismo tipo, xdebe ser un número entero y, por lo tanto, add_oneacepta un número entero como argumento.
Sin embargo, en la línea siguiente, resultado2 se calcula sumando un decimal 1.0con aritmética de punto flotante , lo que provoca un conflicto en el uso de xexpresiones 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 cambio, generan un mensaje de error en tal situación. Este comportamiento puede ser preferible ya que la inferencia de tipos puede no siempre ser algorítmicamente neutral, como lo ilustra el problema anterior de precisión de punto flotante.
Un algoritmo de generalidad intermedia declara implícitamente resultado2 como una variable de punto flotante, y la suma se convierte implícitamente xen una variable de 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 de tipos implícita , que fuerza los datos a un tipo de datos diferente, a menudo sin restricciones.
Finalmente, una desventaja significativa del algoritmo complejo de inferencia de tipos es que la resolución de 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 justo a tiempo permite enfoques híbridos en los que el tipo de argumentos proporcionados por los distintos 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. Luego, 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 :
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 a menudo puede inferir el tipo de una variable o la firma de tipo de una función, sin que se hayan proporcionado anotaciones de tipo explícitas. En muchos casos, es posible omitir completamente 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 recopila 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, verdadero: Bool; 42: Entero; 3.14159: Real; etc.). Es a través del reconocimiento de la eventual reducción de expresiones a valores atómicos tipificados 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 polimorfismo y programación de orden superior , no siempre es posible que el compilador infiera tanto y, en ocasiones, las anotaciones de tipo son necesarias para la desambiguación. Por ejemplo, se sabe que la inferencia de tipos con recursividad polimórfica es indecidible. Además, se pueden utilizar anotaciones de tipo explícitas para optimizar el código obligando 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 del módulo de satisfacibilidad . [dieciséis]
Como ejemplo, la función de 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 La inferencia de tipos en la mapfunción se realiza de la siguiente manera. mapes una función de dos argumentos, por lo que su tipo está restringido a tener la forma a → b → c. En Haskell, los patrones []y (first:rest)siempre coinciden con las listas, por lo que el segundo argumento debe ser un tipo de lista: b = [d]for some type d. Su primer argumento fse aplica al argumento first, que debe tener un tipo d, correspondiente al tipo en el argumento de la lista, por lo que f :: d → e( ::significa "es de tipo") para algún tipo e. El valor de retorno de map f, finalmente, es una lista de todo lo que fproduce, por lo que [e].
Juntar las piezas conduce a map :: (d → e) → [d] → [e]. No hay nada especial en las variables de tipo, por lo que se pueden reetiquetar como
mapa :: ( a → b ) → [ a ] → [ b ] Resulta que éste es también 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 argumentos y resultados de fno se infieren, sino que se dejan como variables de tipo, por lo que mapse pueden aplicar a funciones y listas de varios tipos, siempre que los tipos reales coincidan en cada invocación. .
El algoritmo utilizado por primera vez para realizar la inferencia de tipos ahora se denomina informalmente algoritmo de Hindley-Milner, aunque el algoritmo debería atribuirse correctamente a Damas y Milner. [17] También se le llama 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 descubrimiento de 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 tipo simple que fue ideado por Haskell Curry y Robert Feys en 1958. [ cita necesaria ] En 1969, J. Roger Hindley amplió este trabajo y demostró que su algoritmo siempre infería más tipo generales. En 1978, Robin Milner , [18] independientemente del trabajo de Hindley, proporcionó un algoritmo equivalente, el Algoritmo 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, especialmente la inferencia de tipos correcta (retroceso), introducirá el uso del tipo más general apropiado; sin embargo, esto puede tener implicaciones ya que los tipos más generales pueden no siempre ser algorítmicamente neutrales, siendo los casos típicos:
Los algoritmos de inferencia de tipos se han utilizado para analizar lenguajes naturales y lenguajes de programación. [19] [20] [21] Los algoritmos de inferencia de tipos también se utilizan en algunas inducciones gramaticales [22] [23] y sistemas gramaticales basados en restricciones para lenguajes naturales. [24]