Describa la inferencia del tipo Damas-Milner de forma que un alumno CS101 pueda comprender

Question

Hindley-Milner es un sistema de tipos que es la base de los sistemas tipo de muchos lenguajes de programación funcionales bien conocidos. Damas-Milner es un algoritmo que infiere (¿deduce?) Tipos en un sistema tipo Hindley-Milner.

Wikipedia da una descripción del algoritmo que, hasta donde puedo decir, equivale a una sola palabra: "unificación". Eso es todo? Si es así, eso significa que la parte interesante es el sistema de tipo en sí mismo, no el tipo de inferencia.

Si Damas-Milner es más que unificación, me gustaría una descripción de Damas-Milner que incluya un ejemplo simple e, idealmente, algún código.

Además, a menudo se dice que este algoritmo hace una deducción. ¿Es realmente un sistema de inferencia? Pensé que solo estaba deduciendo los tipos.

preguntas relacionadas:

• What is Hindley Miller?
• Type inference to unification problem

Answer 1

Damas Milner es sólo un uso estructurado de la unificación.

Cuando vuelve a aparecer en una expresión lambda, crea un nuevo nombre de variable. Cuando, en un subtema, encuentra esa variable utilizada de un modo que requeriría un tipo dado, registra la unificación de esa variable y ese tipo. Si alguna vez intenta unificar dos tipos que no tienen sentido, como decir que una variable individual es tanto un Int como una función de a -> b, entonces le grita por hacer algo malo.

Además, a menudo se dice que este algoritmo hace una deducción. ¿Es realmente un sistema de inferencia? Pensé que solo estaba deduciendo los tipos.

Deducir los tipos es type inference. Verificar que las anotaciones de tipo sean válidas para un término determinado es comprobación de tipo. Son problemas diferentes.

Si es así, eso significa que la parte interesante es el sistema de tipo en sí, no el tipo de inferencia.

Comúnmente se dice que los sistemas de tipo Hindley-Milner están equilibrados en una cúspide. Si agrega mucha más funcionalidad, resulta imposible inferir los tipos. Así que escriba las extensiones del sistema que puede superponer sobre un sistema de tipo Hindley-Milner sin destruir sus propiedades de inferencia, que son realmente las partes más interesantes de los lenguajes funcionales modernos. En algunos casos, mezclamos la inferencia de tipos y la verificación de tipos, por ejemplo, en Haskell muchas de las extensiones modernas no se pueden inferir, pero se pueden verificar, por lo que requieren anotaciones de tipo para funciones avanzadas, como la recursión polimórfica.

Answer 2

Wikipedia da una descripción del algoritmo que, hasta donde puedo decir, equivale a una sola palabra: "unificación". Eso es todo? Si es así, eso significa que la parte interesante es el sistema de tipo en sí mismo, no el tipo de inferencia.

IIRC, la parte interesante de la inferencia de tipo Damas-Milner Algoritmo W es que infiere los tipos más generales posibles.