Siguiendo la referencia de Paul Snively a la analogía de Curry-Howard, la inferencia de tipos puede verse como una prueba de teorema dual a automatizada : en ATP, el usuario establece un teorema T y le pide al sistema que proporcione una prueba P tal que P: T (” P es una prueba de T “), mientras que en la inferencia de tipos, el usuario da una prueba P y le pide al sistema que encuentre un teorema T tal que P: T. O para decirlo esquemáticamente:
- la prueba / verificación de tipo considera el problema P: T
- ¿La prueba automática del teorema (o “inferencia de prueba”) considera el problema? : T
- la inferencia de tipos considera el problema P:?
Desafortunadamente, al igual que la demostración automatizada de teoremas, la inferencia de tipos sufre el principal problema cultural de que el dominio se define demasiado libremente y las expectativas poco realistas son rampantes. Al igual que no es realista pedir un sistema que tome un teorema general de las matemáticas y devuelva una prueba (un punto que fue impulsado por Turing), no es realista pedir un sistema que tome un código arbitrario y devuelva un tipo. De hecho, en general, tanto la inferencia de prueba como la inferencia de tipo en este sentido pueden ser indecidibles o intratables. Hay tres tipos de respuestas:
- Renunciar a la inferencia, colocando anotaciones en todas partes para que un fragmento de código (o dualmente, un lema) siempre esté acompañado de un tipo (prueba).
- Intente identificar lenguajes de tipos (pruebas) relativamente inexpresivos para los que el problema de inferencia de tipo global (prueba) sea manejable. Por ejemplo, Yair Minsky ha llamado inferencia tipo Hindley-Milner el punto dulce de ML.
- Después de toparse con cuellos de botella inevitables con los dos primeros enfoques (el tamaño del código con verificación global, el tamaño del lenguaje con inferencia global), finalmente acepte la realidad y aprenda sobre la verificación e inferencia bidireccional.
Dada la forma en que formulé estas tres alternativas, puede decir dónde están mis simpatías. De hecho, creo que es una de las principales falacias en la teoría de tipos que los problemas de verificación e inferencia pueden estar separados. Por otro lado, más positivamente, Conor McBride en particular ha hablado extensamente sobre la interacción de la verificación y la inferencia, y sus escritos sobre Epigram presentan una visión diferente de lo que trata la teoría de tipos. Terminaré con una cita de “Epigrama: programación práctica con tipos dependientes”:
Tal vez sea extraño que el texto del programa no sea enteramente el trabajo del programador. Es el registro de una asociación en la que decimos cuál es el plan y la máquina nos ayuda a llevarlo a cabo. Compare esto con el modelo de programación de ‘inferencia de tipos’, donde anotamos los detalles de la ejecución y la máquina intenta adivinar el plan. En su forma pura, esto requiere la restricción de los planes a aquellos que son lo suficientemente descarados como para ser adivinados. A medida que avanzamos más allá del sistema Hindley-Milner, nos encontramos escribiendo información de tipo de todos modos.

La ‘inferencia de tipo’ tiene, por lo tanto, dos aspectos: ‘inferencia de nivel superior’ (inferir esquemas de tipo, como con Hindley-Milner ‘let’) e ‘inferir tipos dados de inferencia de programa’: inferir detalles cuando se instancia un esquema, como con Hindley-Milner variables Epigram rechaza el primero, pero lleva el segundo más lejos que nunca. Como los tipos representan una declaración de diseño de mayor nivel que los programas, deberíamos preferir escribirlos si hacen que los programas sean más baratos.
