¿Cuáles son los límites de la inferencia de tipos?

Question

¿Cuáles son los límites de la inferencia de tipos? ¿Qué tipo de sistemas no tienen ningún algoritmo general de inferencia?

Answer 1

Joe Wells mostró que la inferencia de tipos es indecidible para Sistema F, que es el cálculo lambda polimórfica 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 está todavía abierto: ¿cuál es la mejor manera de integrar Tipos Generalizado algebraica datos en Hindley-Milner inferencia de tipos? Cada año Simon Peyton Jones sube con una nueva respuesta, que es supuestamente mejor que la respuesta del año anterior. No he leído la versión de marzo de 2009 y por lo que no puedo decir si creo que va a ser definitiva.

Answer 2

Un sistema de tipo dependiente del valor (o en el sistema de tipo corto, dependiente) puede describir los tipos que dicen cosas como: "En el momento de la evaluación (tiempo de ejecución), el valor de esta variable será siempre igual al valor de esa variable , que se calcula con un proceso de evaluación diferente". deducir automáticamente este tipo a partir del código implica pruebas automáticas de teoremas. Si el conjunto de teoremas se puede expresar está restringido a los comprobable de forma automática, que no sería un problema, pero en el caso de las lenguas escritas de forma dependiente, este no es generalmente el caso.

Así sistemas dependientemente mecanografiado no pueden tener en general (y completa) la inferencia de tipos.

Estoy seguro de que alguien puede dar una respuesta formal y completa moral ...