haskell - tipos - Escriba error al atribuir un tipo de campo válido a una variable de límite permitido

tipos de datos en access 2010

Question

¿Es esto un error en el verificador de tipos?

Prelude> let (x :: forall a. a -> a) = id in x 3
<interactive>:0:31:
Couldn''t match expected type `forall a. a -> a''
with actual type `a0 -> a0''
In the expression: id
In a pattern binding: (x :: forall a. a -> a) = id

El hecho de que lo anterior falla al escribir cheque, pero esta contorsión tiene éxito:

Prelude> let (x :: (forall a. a -> a) -> Int) = (/f -> f 3) in x id
3

me lleva a pensar que la "conversión prenex débil" (ver página 23 de este documento ) podría estar relacionada de alguna manera. Incrustar un forall en una posición contravariante donde no puede "flotar" parece mantenerlo a salvo de este extraño error.

Answer 1

Lo que creo que está sucediendo aquí es esto: en la inferencia de tipo estándar de Damas-Milner, las ligaduras son el único lugar donde ocurre la generalización de un tipo. La firma de tipo que utiliza su ejemplo anómalo es una firma de tipo de patrón que "restringe el tipo de patrón de la manera obvia". Ahora, en este ejemplo, no es "obvio" si esta restricción debe ocurrir antes o después de la generalización, pero su ejemplo fallido demuestra, creo, que se aplica antes de la generalización.

Dicho de manera más concreta: en un let binding, let x = id in ... , lo que sucede es el tipo de id forall a. a->a forall a. a->a se crea forall a. a->a instancia en un monotipo, digamos a0 -> a0 , que luego se asigna como el tipo de x y luego se generaliza como forall a0. a0 -> a0 forall a0. a0 -> a0 . Si, como creo, la firma del tipo de patrón se comprueba antes de la generalización, básicamente se está pidiendo al compilador que verifique que el monotipo a0 -> a0 es más general que el tipo policístico para todo forall a. a -> a forall a. a -> a , que no es.

Si movemos la firma de tipo al nivel de enlace, let x :: forall a. a-> a; x = id in ... let x :: forall a. a-> a; x = id in ... let x :: forall a. a-> a; x = id in ... la firma se comprueba después de la generalización (ya que esto está expresamente permitido para permitir la recursión polimórfica), y no se produce ningún error de tipo.

Si es un error o no es, creo, una cuestión de opinión. No parece haber una especificación real que nos diga cuál es el comportamiento correcto aquí; solo hay nuestras expectativas Sugeriría discutir el asunto con la gente de GHC.

Answer 2

No es una respuesta real, pero es demasiado tiempo para un comentario:
Bien puede ser un error. Jugando un poco con la expresión, como era de esperar

let x :: forall a. a -> a; x = id in x 3

funciona si está habilitado escribir foralls explícitos. Sin embargo, es un tipo rango 1 estándar de pantano. Alguna otra variación:

$ ghci-6.12.3 -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables
Prelude> let (x :: forall a. a -> a) = /y -> id y in x 3
3

Bueno, eso funciona, no sé por qué la lambda se comporta de manera diferente, pero lo hace. Sin embargo:

$ ghci -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables
Prelude> let (x :: forall a. a -> a) = /y -> id y in x 3
<interactive>:0:31:
Couldn''t match expected type `t0 -> t1''
with actual type `forall a. a -> a''
The lambda expression `/ y -> id y'' has one argument,
but its type `forall a. a -> a'' has none
In the expression: / y -> id y
In a pattern binding: (x :: forall a. a -> a) = / y -> id y

(7.2.2; 7.0.4 da el mismo error). Eso es sorprendente