Haskell cuantificación existencial en detalle

Question

Tengo una idea general de qué cuantificación existencial en tipos es y donde se puede utilizar. Sin embargo, según mis experiencias hasta ahora, hay muchas advertencias que deben entenderse para utilizar el concepto de manera efectiva.

Pregunta: ¿Hay algún recurso que explique cómo se implementa la cuantificación existencial en GHC? Es decir.

• ¿Cómo funciona la unificación de tipos existenciales? ¿Qué es unificable y qué no lo es?
• ¿En qué orden se realizan las siguientes operaciones en los tipos?

Mi objetivo es comprender mejor los mensajes de error que GHC me lanza. Los mensajes generalmente dicen algo a lo largo de las líneas "this type using forall and this other type don't match", sin embargo, no explican por qué es así.

Answer 1

Los detalles esenciales están cubiertos en los artículos de Simon Peyton-Jones, aunque se necesita una gran cantidad de experiencia técnica para comprenderlos. Si desea leer un documento sobre cómo funciona la inferencia de tipo Haskell, debería leer acerca de los tipos de datos algebraicos generalizados (GADT), que combinan tipos existenciales con varias otras características. Sugiero "Inferencia de tipo completa y decidible para GADT", en la lista de documentos al http://research.microsoft.com/en-us/people/simonpj/.

La cuantificación existencial en realidad funciona de manera similar a la cuantificación universal. Aquí hay un ejemplo para resaltar los paralelos entre los dos. La función useExis es inútil, pero sigue siendo un código válido.

data Univ a = Univ a 
data Exis = forall a. Exis a 

toUniv :: a -> Univ a 
toUniv = Univ 

toExis :: a -> Exis 
toExis = Exis 

useUniv :: (a -> b) -> Univ a -> b 
useUniv f (Univ x) = f x 

useExis :: (forall a. a -> b) -> Exis -> b 
useExis f (Exis x) = f x 

En primer lugar, tenga en cuenta que toUniv y toExis son casi los mismos. Ambos tienen un parámetro de tipo libre a porque ambos constructores de datos son polimórficos. Pero mientras a aparece en el tipo de devolución de toUniv, no aparece en el tipo de devolución de toExis. Cuando se trata del tipo de errores de tipo que puede obtener al usar un constructor de datos, no hay una gran diferencia entre los tipos existenciales y universales.

En segundo lugar, tenga en cuenta el rango-2 tipo forall a. a -> b en useExis. Esta es la gran diferencia en la inferencia de tipo. El tipo existencial tomado de la coincidencia de patrón (Exis x) actúa como una variable de tipo oculto extra que se pasa al cuerpo de la función y no debe unificarse con otros tipos. Para aclarar esto, aquí hay algunas declaraciones erróneas de las dos últimas funciones en las que intentamos unificar tipos que no deberían unificarse. En ambos casos, forzamos el tipo de x para unificarlo con una variable de tipo no relacionada. En useUniv, la variable de tipo es parte del tipo de función. En useExis, es el tipo existencial de la estructura de datos.

useUniv' :: forall a b c. (c -> b) -> Univ a -> b 
useUniv' f (Univ x) = f x -- Error, can't unify 'a' with 'c' 
          -- Variable 'a' is there in the function type 

useExis' :: forall b c. (c -> b) -> Exis -> b 
useExis' f (Exis x) = f x -- Error, can't unify 'a' with 'c'. 
          -- Variable 'a' comes from the pattern "Exis x", 
          -- via the existential in "data Exis = forall a. Exis a".