resueltos - Haskell cuantificación existencial en detalle

funciones proposicionales y cuantificadores

Question

Tengo una idea general de qué es la cuantificación existencial de los tipos y dónde se puede utilizar. Sin embargo, desde mi experiencia hasta ahora, hay muchas advertencias que deben entenderse para poder utilizar el concepto de manera efectiva.

Pregunta: ¿Existen buenos recursos que expliquen cómo se implementa la cuantificación existencial en GHC? Es decir

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

Mi objetivo es comprender mejor los mensajes de error que GHC me lanza. Los mensajes generalmente dicen algo como "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 documentos 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 tipos de Haskell, debe leer sobre los tipos de datos algebraicos generalizados (GADT), que combinan tipos existenciales con otras características. Sugiero "Inferencia de tipos completa y decidible para GADT", en la lista de documentos en http://research.microsoft.com/en-us/people/simonpj/ .

La cuantificación existencial en realidad funciona de manera muy 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 iguales. Ambos tienen un parámetro de tipo libre a porque ambos constructores de datos son polimórficos. Pero mientras aparece a en el tipo de retorno de toUniv , no aparece en el tipo de retorno 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 los universales.

En segundo lugar, tenga en cuenta el tipo de rango 2 para todos forall a. a -> b forall a. a -> b en useExis . Esta es la gran diferencia en la inferencia de tipos. El tipo existencial tomado de la coincidencia de patrón (Exis x) actúa como una variable de tipo oculta adicional que se pasa al cuerpo de la función, y no se debe unificar 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 estar unificados. En ambos casos, forzamos que el tipo de x se unifique 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".