type-inference - textual - que es la inferencia tipos
¿Cuáles son los límites de la inferencia de tipos? (2)
¿Cuáles son los límites de la inferencia de tipos? ¿Qué sistemas de tipo no tienen algoritmo de inferencia general?
Un sistema de tipo dependiente del valor (O, en pocas palabras, sistema de tipo dependiente) puede describir tipos que dicen cosas como: "En el momento de la evaluación (tiempo de ejecución), el valor de esta variable siempre será igual al valor de esa variable, que es computado con un proceso de evaluación diferente ". La deducción automática de este tipo del código conlleva pruebas automáticas de teoremas. Si el conjunto de teoremas que puede expresar está restringido a los demostrables automáticamente, eso no sería un problema, pero en el caso de lenguajes de tipo dependiente, generalmente este no es el caso.
Los sistemas tipificados de manera dependiente no pueden tener una inferencia de tipo general (y completa).
Estoy seguro de que alguien puede dar una respuesta moral formal y completa ...
Joe Wells demostró que la inferencia de tipos es indecidible para el Sistema F, que es el cálculo lambda polimórfico más básico, descubierto independientemente por Girard y Reynolds. Este es el resultado más importante que muestra los límites de la inferencia de tipos.
Aquí hay un problema importante que todavía está abierto: ¿cuál es la mejor manera de integrar los tipos de datos algebraicos generalizados en la inferencia de tipo Hindley-Milner? Cada año, Simon Peyton Jones presenta nuevas respuestas, que supuestamente son mejores que las del año anterior. No he leído la versión de marzo de 2009 y, por lo tanto, no puedo decir si creo que será definitiva.