Probablemente deberíamos distinguir los “algoritmos de inferencia de tipos” de los “sistemas de tipos inferidos (por lo general)”. Voy a comenzar con este último, ya que sospecho que es cómo la mayoría de la gente entendería la pregunta.
De todas las cosas que podríamos caracterizar como inferencia de tipos, las cosas bastante aburridas que ocurren en Java y C # son probablemente más comunes . Aparte de eso, para la inferencia de tipos global, es decir, donde no escribe tipos en su programa (a menos que lo desee) y se garantiza que el sistema de tipos solo admite términos que se pueden escribir, por lo que sé, los descendientes de Hindley / Damas-Milner son El único juego en la ciudad.
Los sistemas de tipos reales en uso no son, en su mayor parte, puramente HM sino extensiones. De los principales idiomas basados en HM, Standard ML todavía está bastante cerca, pero otros idiomas se han alejado en diferentes direcciones. Ocaml ha ampliado HM con subtipos y tipos de fila, mientras que Haskell ha ampliado HM con clases de tipos, los cuales implican restricciones de tipo. En ese sentido, la variante HM más popular podría ser la HM (X) de Sulzman et al., Que es HM parametrizada por un sistema de restricción, aunque Ocaml y Haskell generalmente no se presentan en ese marco. Ocaml y Haskell también se han extendido con polimorfismo de rango superior. Por lo tanto, podríamos decir que otro sistema de tipos comúnmente inferido es uno para el que la inferencia de tipos es indecidible: Sistema F [matemática] _ \ omega [/ matemática]. El FPH de Haskell y lo que sea que esté haciendo Ocaml obviamente no infiere los tipos F [matemática] _ \ omega [/ matemática], pero hacen una inferencia de tipos impresionante al tratar con una gran parte de eso. Junto con FPH hay una variedad de otros acrónimos de tres letras como MLF, HMF y HML, todos los cuales son intentos de hacer inferencia tipo HM para subconjuntos más grandes del Sistema F.
- ¿Qué consejo me das, si realmente quiero comenzar a programar?
- ¿Por qué usar sigmoid y tanh como funciones de activación en LSTM o RNN no es problemático, pero este no es el caso en otras redes neuronales?
- ¿Cuáles son algunos buenos proyectos importantes de ML o AI?
- ¿Cuáles son los temas más candentes en matemáticas aplicadas?
- ¿Qué tan prestigioso es publicar en NIPS?
La otra cosa interesante que sucede en la inferencia de tipos, y no sé qué tan común es, es la inferencia de tipos local. Scala es probablemente el idioma más popular en este momento con inferencia de tipo local no trivial. El sistema de tipos de Scala no se puede inferir globalmente, pero la inferencia de tipos locales ayuda a eliminar la necesidad de la mayoría de las instancias de tipos y algunas anotaciones de tipos en variables enlazadas. (Typed Racket y el idioma en el que trabajo también usan inferencia de tipos local, aunque no creo que califiquen como “comunes”. Pero lo que quito de esto es que las personas que desean que los sistemas de tipos hagan cosas cada vez más difíciles , la inferencia de tipo local puede ser cada vez más atractiva).
En cuanto a los algoritmos de inferencia de tipos, eso es más difícil de responder porque en realidad no sé exactamente qué algoritmos están usando todos. Existen varios algoritmos distintos para HM puro, y algunos son más adecuados que otros para diversas extensiones.
Damas y Milner (1982) primero dieron su sistema de tipos en una forma no algorítmica. En particular, no especifica dónde aplicar las reglas de generalización e instanciación. Su contribución clave es el Algoritmo W, una versión algorítmica de su sistema de tipos que es sólida y completa. Es decir, si W devuelve un resultado, entonces hay una derivación válida de ese resultado en su sistema de tipos y, por el contrario, si un término es tipificable en su sistema de tipos, entonces W encuentra el esquema de tipos principal ( es decir, el más general). Hay otros algoritmos para este mismo tipo de sistema. En particular, el algoritmo J también es sólido y completo para HM, y muchas personas consideran que es más fácil de entender.
Sin embargo, sospecho que ni W ni J es el algoritmo de inferencia de tipo más común (estilo HM) en este momento. Ambos algoritmos W y J llaman al algoritmo de Robinson para la unificación de primer orden como una “subrutina”. En lugar de intercalar generación y restricción de restricciones, es posible separar la inferencia de tipos en dos fases, la primera de las cuales atraviesa el término y genera una restricción, y el segundo resuelve la restricción por unificación. Creo que la idea se originó con Wand (aunque no puedo entender dónde). La mejor explicación de esto que conozco es el capítulo de Pottier y Rémy “La esencia de la inferencia de tipos de ML”, en Temas avanzados en tipos y lenguajes de programación (Pierce).
Mencioné anteriormente que los sistemas de tipos inferidos hoy en día tienden a extenderse en formas que caen en el marco HM (X), como las clases de subtipo y tipo. Varias de las extensiones de polimorfismo de primera clase también están en términos de restricciones, aunque no sé si eso los hace candidatos para la X en HM (X). Mientras que el documento original HM (X) usa una extensión del Algoritmo J (si no recuerdo mal), Pottier y Rémy lo refundieron utilizando el enfoque de resolución de restricciones, y tiene mucho sentido de esa manera. Sospecho que este nuevo enfoque es más común (o se está volviendo más común) que los algoritmos como W en este punto. Por lo tanto, puede ser que el sistema de tipos inferido más común (no trivialmente) en este momento sea (instancias de) HM (X), y el algoritmo de inferencia de tipo más común es el algoritmo de Pottier y Rémy para HM (X).
