haskell - textual - Entendiendo los politipos en la inferencia de tipo Hindley-Milner

inferencia textual

Question

Estoy leyendo el artículo de Wikipedia sobre la Inferencia de Tipo Hindley-Milner para darle algún sentido. Hasta ahora esto es lo que he entendido:

1. Los tipos se clasifican como monotipos o politipos.
2. Los monotipos se clasifican además como constantes de tipo (como int o string ) o variables de tipo (como α y β ).
3. Las constantes de tipo pueden ser tipos concretos (como int y string ) o constructores de tipo (como Map y Set ).
4. Las variables de tipo (como α y β ) se comportan como marcadores de posición para tipos concretos (como int y string ).

Ahora tengo un poco de dificultad para entender los politipos, pero después de aprender un poco de Haskell, esto es lo que hago al respecto:

1. Los tipos mismos tienen tipos. Formalmente, los tipos de tipos se denominan tipos (es decir, hay diferentes tipos de tipos).
2. Los tipos concretos (como int y string ) y las variables de tipo (como α y β ) son de tipo * .
3. Los constructores de tipos (como Map y Set ) son abstracciones lambda de tipos (por ejemplo, Set es de tipo * -> * y Map es de tipo * -> * -> * ).

Lo que no entiendo es lo que significan los calificativos. Por ejemplo, ¿ ∀α.σ representa ∀α.σ ? Parece que no puedo entenderlo todo, y cuanto más leo el siguiente párrafo, más confuso me pongo:

Una función con politipo ∀α.α -> α por contraste puede asignar cualquier valor del mismo tipo a sí misma, y ​​la función de identidad es un valor para este tipo. Como otro ejemplo, ∀α (Set α) -> int es el tipo de una función que asigna todos los conjuntos finitos a números enteros. El recuento de miembros es un valor para este tipo. Tenga en cuenta que los calificadores solo pueden aparecer en el nivel superior, es decir, un tipo ∀α.α -> ∀α.α, por ejemplo, está excluido por la sintaxis de los tipos y que los monotipos están incluidos en los politipos, por lo que un tipo tiene la forma general α₁. . . ∀αₙ.τ .

Answer 1

Considere l = /x -> t en Haskell. Es una lambda, que representa un término t una variable x , que se sustituirá más adelante (por ejemplo, l 1 , lo que sea que signifique). De manera similar, ∀α.σ representa un tipo con una variable de tipo α , es decir, f : ∀α.σ si una función está parametrizada por un tipo α . En cierto sentido, σ depende de α , por lo que f devuelve un valor de tipo σ(α) , donde α se sustituirá en σ(α) más adelante, y obtendremos algún tipo concreto.

En Haskell se le permite omitir ∀ y definir funciones como id : a -> a . La razón para permitir omitir el cuantificador es básicamente porque solo se les permite el nivel superior (sin la extensión RankNTypes ). Puedes probar este código:

id2 : a -> a -- I named it id2 since id is already defined in Prelude
id2 x = x

Si le pregunta a ghci el tipo de id ( :t id ), devolverá a -> a . Para ser más precisos (más tipo de teoría), id tiene el tipo ∀a. a -> a ∀a. a -> a . Ahora, si usted agrega a su código:

val = id2 3

, 3 tiene el tipo Int , por lo que el tipo Int se sustituirá por σ y obtendremos el tipo concreto Int -> Int .

Answer 2

Primero, las clases y los tipos polimórficos son cosas diferentes. Puede tener un sistema de tipo HM donde todos los tipos son del mismo tipo (*), también podría tener un sistema sin polimorfismo pero con tipos complejos.

Si un término M es de tipo ∀at , significa que para cualquier tipo s podemos sustituir s por a t (a menudo escrito como t[a:=s] y tendremos que M es de tipo t[a:=s] . Esto es algo similar a la lógica, donde podemos sustituir cualquier término por una variable cuantificada universalmente, pero aquí estamos tratando con tipos.

Esto es precisamente lo que sucede en Haskell, solo que en Haskell no ves los cuantificadores. Todas las variables de tipo que aparecen en una firma de tipo se cuantifican de forma implícita, como si se hubieran encontrado delante del tipo. Por ejemplo, el map tendría tipo

map :: forall a . forall b . (a -> b) -> [a] -> [b]

Sin esta cuantificación universal implícita, las variables de tipo a y b tendrían que tener un significado fijo y el map no sería polimórfico.

El algoritmo HM distingue los tipos (sin cuantificadores, monotipos) y los esquemas de tipo (tipos universalmente cuantificados, politipos). Es importante que en algunos lugares use esquemas de tipo (como en let ), pero en otros lugares solo se permiten tipos. Esto hace que todo sea decidible.

También le sugiero que lea el artículo sobre el Sistema F. Es un sistema más complejo, que permite todo tipo de tipos (por lo tanto, todo lo que se llama simplemente tipo ), pero la inferencia / comprobación de tipos es indecidible. Puede ayudarte a entender cómo funciona todo. El sistema F se describe en profundidad en Girard, Lafont y Taylor, Pruebas y tipos .