Inferencia de tipo
La inferencia de tipo se refiere a la detección automática del tipo de 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 vista más general se pueden asociar 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 otra designación que llamarlo leña , aunque podría ser materialmente lo mismo. Si bien sus propiedades materiales hacen que las cosas se puedan utilizar para algunos propósitos, también están sujetas a designaciones particulares. Este es especialmente el caso en campos abstractos, a saber, matemáticas e informática, donde el material es finalmente sólo bits o fórmulas.
Para excluir usos no deseados, pero materialmente posibles, el concepto de tipos se define y 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 "errores de tipo", por ejemplo, ordenar a una computadora que sume valores que no son números. Si bien es materialmente posible, el resultado ya no sería significativo y quizás desastroso para el proceso en general.
En una tipificación , 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 . Esto significa que el valor es de tipo . Este formulario también se utiliza para declarar nuevos nombres, por ejemplo , de forma muy similar a la introducción de un nuevo personaje en una escena con las palabras "detective Decker".
Al contrario de una historia, donde las designaciones se desarrollan lentamente, los objetos en los lenguajes formales 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 puede tener un tipo , pero también puede leerse como un número racional o real o incluso como un texto sin formato.
Como consecuencia, los programas o las pruebas pueden estar tan sobrecargados de tipos que es deseable deducirlos del contexto. Esto puede ser posible mediante la recopilación de los usos de expresión sin tipo (incluidos los nombres no definidos). Si, por ejemplo, se usa 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 de una expresión y su contexto es la inferencia de tipos .
