haskell - ¿Por qué no se puede especializar el tipo de ID para(para todos a. A-> a)->(para todos b. B-> b)?

polymorphism impredicativetypes

Question

Tomemos la humilde función de identidad en Haskell,

id :: forall a. a -> a

Dado que Haskell supuestamente es compatible con el polimorfismo imprevisivo, parece razonable que pueda ser capaz de "restringir" la id al tipo (forall a. a -> a) -> (forall b. b -> b) través de una asignación de tipo. Pero esto no funciona:

Prelude> id :: (forall a. a -> a) -> (forall b. b -> b)
<interactive>:1:1:
Couldn''t match expected type `b -> b''
with actual type `forall a. a -> a''
Expected type: (forall a. a -> a) -> b -> b
Actual type: (forall a. a -> a) -> forall a. a -> a
In the expression: id :: (forall a. a -> a) -> (forall b. b -> b)
In an equation for `it'':
it = id :: (forall a. a -> a) -> (forall b. b -> b)

Por supuesto, es posible definir una nueva forma restringida de la función de identidad con la firma deseada:

restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId x = x

Sin embargo, definirlo en términos de la id general no funciona:

restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId = id -- Similar error to above

Entonces, ¿qué está pasando aquí? Parece que podría estar relacionado con dificultades con la impredicatividad, pero habilitar -XImpredicativeTypes no hace ninguna diferencia.

Answer 1

¿Por qué está esperando un tipo de (forall a. a -> a) -> b -> b

Creo que el tipo para todos forall b.(forall a. a -> a) -> b -> b es equivalente al tipo que dio. Es solo una representación canónica de la misma, donde el forall se desplaza tanto a la izquierda como sea posible.

Y la razón por la que no funciona es que el tipo dado es en realidad más polimórfico que el tipo de id :: forall c. c -> c, que requiere que los tipos de argumento y retorno sean iguales. Pero el forall a en su tipo prohíbe efectivamente que se unifique con cualquier otro tipo.

Answer 2

No soy un experto en tipos impredictivos, por lo que esta es a la vez una respuesta potencial y un intento de aprender algo de los comentarios.

No tiene sentido especializarse

// a . a -> a (1)

a

(// a . a -> a) -> (// b . b -> b) (2)

y no creo que los tipos impredictivos sean una razón para permitirlo. Los cuantificadores tienen el efecto de hacer los tipos representados por el lado izquierdo y derecho de (2) conjuntos desiguales en general. Sin embargo, la a -> a en (1) implica que los lados izquierdo y derecho son conjuntos equivalentes.

Por ejemplo, puede concretar (2) a (int -> int) -> (string -> string). Pero por cualquier sistema, sé que este no es un tipo representado por (1).

El mensaje de error parece ser el resultado de un intento del inferencer de tipo Haskel de unificar el tipo de id

// a . a -> a

con el tipo que has dado

// c . (c -> c) -> // d . (d -> d)

Aquí estoy unificando las variables cuantificadas para mayor claridad.

El trabajo del inferencista de tipo es encontrar una asignación más general para a , c , d que haga que las dos expresiones sean sintácticamente iguales. En última instancia, se encuentra que se requiere para unificar c y d . Dado que se cuantifican por separado, se encuentra en un callejón sin salida y se cierra.

Quizás esté haciendo la pregunta porque el inferencista de tipo básico, con una asignación (c -> c) -> (d -> d) , simplemente avanzará y establecerá c == d . El tipo resultante sería

(c -> c) -> (c -> c)

que es solo taquigrafía para

//c . (c -> c) -> (c -> c)

Esta es probablemente la expresión de tipo menos general (tipo teórico menor límite superior) para el tipo de x = x donde x está limitado a ser una función con el mismo dominio y dominio compartido.

El tipo de "ID restringido" tal como se da es, en un sentido real, excesivamente general. Si bien nunca puede llevar a un error de tipo de tiempo de ejecución, hay muchos tipos descritos por la expresión que le ha dado, como el mencionado (int -> int) -> (string -> string) - que son imposibles operativamente a pesar de que El tipo los permitiría.

Answer 3

Usted es absolutamente correcto que para todos forall b. (forall a. a -> a) -> b -> b forall b. (forall a. a -> a) -> b -> b no es equivalente a (forall a. a -> a) -> (forall b. b -> b) para todos (forall a. a -> a) -> (forall b. b -> b) .

A menos que se indique lo contrario, las variables de tipo se cuantifican en el nivel más externo. Entonces (a -> a) -> b -> b es una abreviatura de (forall a. (forall b. (a -> a) -> b -> b)) para todos (forall a. (forall b. (a -> a) -> b -> b)) . En el Sistema F, donde el tipo de abstracción y la aplicación se hacen explícitos, esto describe un término como f = Λa. Λb. λx:(a -> a). λy:b. xy f = Λa. Λb. λx:(a -> a). λy:b. xy f = Λa. Λb. λx:(a -> a). λy:b. xy Para ser claro para cualquiera que no esté familiarizado con la notación, Λ es un lambda que toma un tipo como parámetro, a diferencia de λ que toma un término como parámetro.

La persona que llama f primero proporciona un parámetro de tipo a , luego suministra un parámetro de tipo b , luego proporciona dos valores x e y que se adhieren a los tipos elegidos. Lo importante a tener en cuenta es que la persona que llama elige a y b . Por lo tanto, la persona que llama puede realizar una aplicación como f String Int length por ejemplo, para producir un término String -> Int .

Usando -XRankNTypes puede anotar un término colocando explícitamente el cuantificador universal, no tiene que estar en el nivel más externo. Su término restrictedId con el tipo (forall a. a -> a) -> (forall b. b -> b) podría ejemplificarse aproximadamente en el Sistema F como g = λx:(forall a. a -> a). if (x Int 0, x Char ''d'') > (0, ''e'') then x else id g = λx:(forall a. a -> a). if (x Int 0, x Char ''d'') > (0, ''e'') then x else id . Observe cómo g , la persona que llama, puede aplicar x tanto a 0 como a ''e'' al crear una instancia con un tipo.

Pero en este caso, la persona que llama no puede elegir el tipo de parámetro como lo hizo antes con f . Notarás las aplicaciones x Int y x Char dentro de la lambda. Esto obliga a la persona que llama a proporcionar una función polimórfica, por lo que un término como g length no es válido porque la length no se aplica a Int o Char .

Otra forma de pensarlo es dibujar los tipos de f y g como un árbol. El árbol para f tiene un cuantificador universal como raíz, mientras que el árbol para g tiene una flecha como raíz. Para llegar a la flecha en f , la persona que llama crea una instancia de los dos cuantificadores. Con g , ya es un tipo de flecha y la persona que llama no puede controlar la creación de instancias. Esto obliga a la persona que llama a proporcionar un argumento polimórfico.

Por último, por favor perdona mis ejemplos inventados. Gabriel Scherer describe algunos usos más prácticos del polimorfismo de rango más alto en usos moderadamente prácticos del Sistema F sobre ML . También puede consultar los capítulos 23 y 30 de TAPL o hojear la documentación de las extensiones del compilador para encontrar más detalles o mejores ejemplos prácticos de polimorfismo de rango superior.