opciones - if en haskell ejemplos

Tipos existenciales vs. cuantificados universalmente en Haskell

Question

¿Cuál es exactamente la diferencia entre estos? Creo que entiendo cómo funcionan los tipos existenciales, son como tener una clase base en OO sin una forma de lanzar hacia abajo. ¿Cómo son diferentes los tipos universales?

Answer 1

Los términos "universal" y "existencial" provienen aquí de los cuantificadores de nombre similar en lógica de predicados .

La cuantificación universal normalmente se escribe como ∀, que puede leer como "para todos", y significa más o menos lo que parece: en una declaración lógica que se asemeja a "∀x ..." lo que sea que esté en lugar del "..." es cierto para todas las posibles "x" que pueda elegir de cualquier conjunto de cosas que se cuantifiquen.

La cuantificación existencial se escribe normalmente como ∃, que puede leer como "existe", y significa que en una declaración lógica que se asemeja a "∃x ..." lo que esté en lugar del "..." es cierto para algunos no especificados "x" tomado del conjunto de cosas que se están cuantificando.

En Haskell, las cosas que se cuantifican son tipos (ignorando ciertas extensiones de lenguaje, al menos), nuestras declaraciones lógicas también son tipos, y en lugar de ser "verdaderas", pensamos en "se puede implementar".

Entonces, un tipo universalmente cuantificado como forall a. a -> a 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

Como a se cuantifica de manera universal, 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 ⁽¹⁾ .

En Haskell, la cuantificación universal es el "valor por defecto": cualquier variable de tipo en una firma está implícitamente cuantificada universalmente, razón por la cual el tipo de id se escribe normalmente como a a -> a . Esto también se conoce como polimorfismo paramétrico , a menudo simplemente llamado "polimorfismo" en Haskell, y en algunos otros idiomas (por ejemplo, C #) conocido como "genéricos".

Un tipo cuantificado existencialmente como exists a. a -> a exists a. a -> a significa que, para un tipo particular "a", podemos implementar una función cuyo tipo es a -> a . Cualquier función funcionará, entonces escogeré una:

func :: exists a. a -> a
func True = False
func False = True

... que es, por supuesto, la función "no" en booleanos. Pero la trampa es que no podemos usarlo como tal, porque todo lo que sabemos sobre el tipo "a" es que existe. Cualquier información sobre qué tipo podría ser se ha descartado, lo que significa que no podemos aplicar func a ningún valor.

Esto no es muy útil.

Entonces, ¿qué podemos hacer con func ? Bueno, sabemos que es una función del mismo tipo para su entrada y salida, por lo que podríamos componerlo consigo mismo, por ejemplo. Básicamente, las únicas cosas que puedes hacer con algo que tiene un tipo existencial son las cosas que puedes hacer en función de las partes no existenciales del tipo. Del mismo modo, dado algo de tipo exists a. [a] exists a. [a] podemos encontrar su longitud, o concatenarla a sí misma, o soltar algunos elementos, o cualquier otra cosa que podamos hacer a cualquier lista.

Ese último bit nos lleva de vuelta a los cuantificadores universales, y la razón por la cual Haskell ⁽²⁾ no tiene tipos existenciales directamente (mi exists arriba es completamente ficticia, ¡ay!), Ya que las cosas con tipos cuantificados existencialmente solo se pueden usar con operaciones que tienen tipos universalmente cuantificados, podemos escribir que el tipo exists a. a exists a. a como todo forall r. (forall a. a -> r) -> r forall r. (forall a. a -> r) -> r 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 del tipo r .

Si no está claro para usted por qué son casi equivalentes, tenga en cuenta que el tipo general no se cuantifica de manera universal para a , sino que se necesita un argumento que se cuantifique universalmente para a , que luego puede usar con cualquier tipo específico que elija .

Por otro lado, aunque Haskell no tiene realmente una noción de subtipado en el sentido habitual, podemos tratar a los cuantificadores como una forma de subtipificación, con una jerarquía que va de lo universal a lo concreto a lo existencial. Algo de tipo para todo forall a. a 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 exists a. a , haciendo de ese un tipo padre de todo. Por supuesto, el primero es imposible (no hay valores de tipo para todo el mundo excepto errores) y el último es inútil (no se puede hacer nada con el tipo exists a. a ), pero la analogía funciona en papel al menos . :]

Tenga en cuenta que la equivalencia entre un tipo existencial y un argumento universalmente cuantificado funciona por la misma razón que la variance voltea para las entradas de funciones.

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 no hay manera real de hablar de tipos existenciales en absoluto.