haskell - Código inesperadamente aceptado por GHC/GHCi

type-inference typechecking

Question

No entiendo por qué este código debe pasar la comprobación de tipos:

foo :: (Maybe a, Maybe b)
foo = let x = Nothing in (x,x)

Dado que cada componente está vinculado a la misma variable x , esperaría que el tipo más general para esta expresión sea (Maybe a, Maybe a) . Obtengo los mismos resultados si uso un lugar where lugar de un let . ¿Me estoy perdiendo de algo?

Answer 1

En pocas palabras, el tipo de x se generaliza por let . Este es un paso clave en el algoritmo de inferencia de tipo Hindley-Milner .

Concretamente, let x = Nothing asigna inicialmente x el tipo Maybe t , donde t es una variable de tipo nueva. Luego, el tipo se generaliza, cuantificando universalmente todas sus variables de tipo (técnicamente: excepto las que se usan en otros lugares, pero aquí solo tenemos t ). Esto causa x :: forall t. Maybe t x :: forall t. Maybe t . Tenga en cuenta que este es exactamente el mismo tipo que Nothing :: forall t. Maybe t Nothing :: forall t. Maybe t .

Por lo tanto, cada vez que usamos x en nuestro código, eso se refiere a un tipo potencialmente diferente, Maybe t , muy parecido a Nothing . Usar (x, x) obtiene el mismo tipo que (Nothing, Nothing) por este motivo.

En cambio, las lambdas no presentan el mismo paso de generalización. En comparación (/x -> (x, x)) Nothing "solo" tiene el tipo forall t. (Maybe t, Maybe t) forall t. (Maybe t, Maybe t) , donde ambos componentes se ven obligados a ser del mismo tipo. Aquí, a x se le asigna nuevamente el tipo Maybe t , con t fresco, pero no está generalizado. Entonces (x, x) se asigna el tipo (Maybe t, Maybe t) . Solo en el nivel superior generalizamos la adición de forall t , pero en ese momento es demasiado tarde para obtener un par heterogéneo.