Solución:
Los términos “universal” y “existencial” aquí provienen de los cuantificadores denominados de manera similar en la lógica de predicados.
La cuantificación universal se escribe normalmente como ∀, que puede leerse como “para todos”, y significa aproximadamente lo que parece: en una declaración lógica que se asemeja a “∀x. …” lo que sea que esté en lugar de “…” es true para todas las “x” posibles, puede elegir entre cualquier conjunto de cosas sobre el que se esté cuantificando.
La cuantificación existencial se escribe normalmente como ∃, que se puede leer como “existe”, y significa que en un enunciado lógico parecido a “∃x. …” lo que sea que esté en lugar de “…” es true para alguna “x” no especificada tomada del conjunto de cosas sobre las que se cuantifica.
En Haskell, las cosas que se cuantifican son tipos (ignorando ciertas extensiones del lenguaje, al menos), nuestras declaraciones lógicas también son tipos, y en lugar de ser “true”pensamos en” se puede implementar “.
Entonces, un tipo cuantificado universalmente como forall a. a -> a significa que, para cualquier tipo posible “a”, podemos implementar una función cuyo tipo sea a -> a. Y de hecho podemos:
id :: forall a. a -> a
id x = x
Ya que a está cuantificado universalmente, no sabemos nada al respecto y, por lo tanto, no podemos inspeccionar el argumento de ninguna manera. Entonces id es la única función posible de ese tipo(1).
En Haskell, la cuantificación universal es la “predeterminada”: cualquier tipo de variable en una firma se cuantifica implícitamente universalmente, por lo que el tipo de id normalmente se escribe como a -> a. Esto también se conoce como polimorfismo paramétrico, a menudo llamado simplemente “polimorfismo” en Haskell, y en algunos otros lenguajes (por ejemplo, C #) conocido como “genéricos”.
Un existencialmente tipo cuantificado como exists a. a -> a significa que, para algunos en particular tipo “a”, podemos implementar una función cuyo tipo es a -> a. Cualquier función servirá, así que elegiré una:
func :: exists a. a -> a
func True = False
func False = True
… que es, por supuesto, la función “no” en los valores booleanos. Pero el problema es que no podemos usar como tal, porque todo lo que sabemos sobre el tipo “a” es que existe. Cualquier información sobre cuales el tipo que podría ser se ha descartado, lo que significa que no podemos aplicar func a cualquier valor.
Esto no es muy útil.
Y qué pueden hacemos con func? Bueno, sabemos que es una función con el mismo tipo para su entrada y salida, por lo que podríamos componerla consigo misma, por ejemplo. Esencialmente, las únicas cosas que puede hacer con algo que tiene un tipo existencial son las cosas que puede hacer basándose en las partes no existenciales del tipo. Del mismo modo, dado algo de tipo exists a. [a] podemos encontrar su longitud, o concatenarlo consigo mismo, o eliminar algunos elementos, o cualquier otra cosa que podamos hacer en cualquier lista.
Esa última parte nos lleva de vuelta a los cuantificadores universales y la razón por la que Haskell(2) no tiene tipos existenciales directamente (mi exists anterior es completamente ficticio, por desgracia): dado que las cosas con tipos cuantificados existencialmente solo se pueden usar con operaciones que tienen tipos cuantificados universalmente, podemos escribir el tipo exists a. a como forall r. (forall a. a -> r) -> r– en otras palabras, para todos los tipos de resultados r, dada una función que para todos los tipos a toma un argumento de tipo a y devuelve un valor de tipo r, podemos obtener un resultado de tipo r.
Si no tiene claro por qué son casi equivalentes, tenga en cuenta que el tipo general no se cuantifica universalmente para a– más bien, toma un argumento que en sí mismo está universalmente cuantificado para a, que luego puede usar con cualquier tipo específico que elija.
Aparte, aunque Haskell no tiene realmente una noción de subtipificación en el sentido habitual, podemos tratar a los cuantificadores como si expresaran una forma de subtipificación, con una jerarquía que va de universal a concreta y a existencial. Algo de tipo forall a. a podría convertirse a cualquier otro tipo, por lo que podría verse como un subtipo de todo; por otro lado, cualquier tipo podría convertirse al tipo exists a. a, convirtiéndolo en un padre de todo. Por supuesto, lo primero es imposible (no hay valores de tipo forall a. a excepto errores) y este último es inútil (no se puede hacer nada con el tipo exists a. a), pero la analogía funciona al menos sobre el papel. :]
Tenga en cuenta que la equivalencia entre un tipo existencial y un argumento cuantificado universalmente funciona por la misma razón que la varianza cambia para las entradas de función.
Entonces, la idea básica es aproximadamente que los tipos cuantificados universalmente describen cosas que funcionan igual para cualquier tipo, mientras que los tipos existenciales describen cosas que funcionan con un tipo específico pero desconocido.
1: Bueno, no del todo, solo si ignoramos las funciones que causan errores, como notId x = undefined, incluidas las funciones que nunca terminan, como loopForever x = loopForever x.
2: Bueno, GHC. Sin extensiones, Haskell solo tiene los cuantificadores universales implícitos y ninguna forma real de hablar sobre los tipos existenciales.
Bartosz Milewski en su libro ofrece una buena idea de por qué Haskell no necesita un cuantificador existencial:
en pseudo-Haskell:
(exists x. p x x) -> c ≅ forall x. p x x -> cNos dice que una función que toma un tipo existencial es equivalente a una función polimórfica. Esto tiene mucho sentido, porque dicha función debe estar preparada para manejar cualquiera de los tipos que pueden estar codificados en el tipo existencial. Es el mismo principio que nos dice que una función que acepta un tipo de suma debe implementarse como una declaración de caso, con una tupla de controladores, uno para cada tipo presente en la suma. Aquí, el tipo de suma se reemplaza por un coendo y una familia de manejadores se convierte en un final o una función polimórfica.
Por tanto, un ejemplo de un tipo cuantificado existencialmente en Haskell es
data Sum = forall a. Constructor a (i.e. forall a. (Constructor_a:: a -> Sum) ≅ Constructor:: (exists a. a) -> Sum)
que se puede considerar como una suma
data Sum = int | char | bool | .... En contraste, un ejemplo de un tipo cuantificado universalmente en Haskell es
data Product = Constructor (forall a. a)
que puede pensarse como un producto data Product = int char bool ....
valoraciones y comentarios
Recuerda comunicar esta sección si lograste el éxito.