opciones - hola mundo en haskell

¿Qué hace la palabra clave `forall` en Haskell/GHC? (8)

¿Alguien puede explicar completamente la palabra clave forall en un lenguaje claro y sencillo?

No. (Bueno, tal vez Don Stewart pueda).

Aquí están las barreras para una explicación simple y clara o para todos:

Es un cuantificador. Tienes que tener al menos un poco de lógica (cálculo de predicado) para haber visto un cuantificador universal o existencial. Si nunca ha visto cálculos de predicados o no se siente cómodo con los cuantificadores (y he visto estudiantes durante los exámenes de calificación de doctorado que no se sienten cómodos), entonces no hay una explicación fácil para todos.
Es un cuantificador de tipo . Si no has visto el Sistema F y no has practicado la escritura de tipos polimórficos, encontrarás algo confuso. La experiencia con Haskell o ML no es suficiente, porque normalmente estos lenguajes omiten el forall de los tipos polimórficos. (En mi opinión, esto es un error de diseño de lenguaje).
En Haskell en particular, forall se usa en formas que me resultan confusas. (No soy un teórico del tipo, pero mi trabajo me pone en contacto con una gran cantidad de teoría de tipos, y me siento bastante cómodo con ella). Para mí, la principal fuente de confusión es que forall se utiliza para codificar un tipo. que yo mismo preferiría escribir con exists . Está justificado por un poco complicado de isomorfismo de tipo que incluye cuantificadores y flechas, y cada vez que quiero entenderlo, tengo que buscar cosas y resolver el isomorfismo por mi cuenta.
Si no te sientes cómodo con la idea del isomorfismo de tipo, o si no tienes alguna práctica pensando en los isomorfismos de tipo, este uso de forall es un obstáculo para ti.
Si bien el concepto general de forall es siempre el mismo (vinculante para introducir una variable de tipo), los detalles de los diferentes usos pueden variar significativamente. El inglés informal no es una herramienta muy buena para explicar las variaciones. Para entender realmente lo que está pasando, necesitas algunas matemáticas. En este caso, las matemáticas relevantes se pueden encontrar en el texto introductorio Tipos y lenguajes de programación de Benjamin Pierce, que es un muy buen libro.

En cuanto a sus ejemplos particulares,

runST debería hacer que te duela la cabeza. Los tipos de rango superior (para todos a la izquierda de una flecha) rara vez se encuentran en la naturaleza. Le animo a leer el documento que introdujo runST : "Lazy Functional State Threads" . Este es un documento realmente bueno, y le dará una mejor intuición para el tipo de runST en particular y para los tipos de rango más alto en general. La explicación toma varias páginas, está muy bien hecha, y no voy a intentar condensarla aquí.
Considerar
foo :: (forall a. a -> a) -> (Char,Bool) bar :: forall a. ((a -> a) -> (Char, Bool))
Si llamo a la bar , simplemente puedo elegir el tipo a que me gusta, y puedo pasarle una función de tipo a tipo a . Por ejemplo, puedo pasar la función (+1) o la función reverse . Puedes pensar en el forall como si dijera "Ahora puedo elegir el tipo". (La palabra técnica para seleccionar el tipo es instanciar ).
Las restricciones para llamar a foo son mucho más estrictas: el argumento de foo debe ser una función polimórfica. Con ese tipo, las únicas funciones que puedo pasar a foo son id o una función que siempre diverge o cometa errores, como undefined . La razón es que con foo , el forall está a la izquierda de la flecha, de modo que como interlocutor de foo no puedo elegir qué es, sino que es la implementación de foo que elige qué es. Debido a que forall está a la izquierda de la flecha, en lugar de sobre la flecha como en la bar , la creación de instancias se lleva a cabo en el cuerpo de la función en lugar de en el sitio de la llamada.

Resumen: una explicación completa de la palabra clave forall requiere matemáticas y solo puede ser entendida por alguien que haya estudiado las matemáticas. Incluso las explicaciones parciales son difíciles de entender sin las matemáticas. Pero tal vez mis explicaciones parciales y no matemáticas ayuden un poco. ¡Ve a leer Launchbury y Peyton Jones en runST !

Anexo: jerga "arriba", "abajo", "a la izquierda de". Estos no tienen nada que ver con las formas textuales en que se escriben los tipos y todo lo relacionado con los árboles de sintaxis abstracta. En la sintaxis abstracta, un forall toma el nombre de una variable de tipo, y luego hay un tipo completo "debajo" del forall. Una flecha toma dos tipos (argumento y tipo de resultado) y forma un nuevo tipo (el tipo de función). El tipo de argumento es "a la izquierda de" la flecha; Es el elemento izquierdo de la flecha en el árbol de sintaxis abstracta.

Ejemplos:

En forall a . [a] -> [a] forall a . [a] -> [a] , el forall está por encima de la flecha; lo que está a la izquierda de la flecha es [a] .
En
forall n f e x . (forall e x . n e x -> f -> Fact x f) -> Block n e x -> f -> Fact x f
el tipo entre paréntesis se llamaría "un forall a la izquierda de una flecha". (Estoy usando tipos como este en un optimizador en el que estoy trabajando).

Estoy empezando a entender cómo se usa la palabra clave forall en los llamados "tipos existenciales", como este:

data ShowBox = forall s. Show s => SB s

Sin embargo, este es solo un subconjunto de cómo se usa forall y simplemente no puedo envolver mi mente en torno a su uso en cosas como esta:

runST :: forall a. (forall s. ST s a) -> a

O explicando por qué estos son diferentes:

foo :: (forall a. a -> a) -> (Char,Bool) bar :: forall a. ((a -> a) -> (Char, Bool))

O todo el material de RankNTypes ...

Tiendo a preferir el inglés claro y libre de jerga en lugar de los tipos de lenguaje que son normales en los entornos académicos. La mayoría de las explicaciones que intento leer sobre esto (las que puedo encontrar en los motores de búsqueda) tienen estos problemas:

Están incompletos. Explican una parte del uso de esta palabra clave (como "tipos existenciales") que me hace sentir feliz hasta que leo el código que lo usa de una manera completamente diferente (como runST , foo y bar arriba).
Están llenos de suposiciones de que he leído lo último en cualquier rama de las matemáticas discretas, la teoría de categorías o el álgebra abstracta que es popular esta semana. (Si nunca vuelvo a leer las palabras "consultar el documento para obtener detalles de la implementación", será demasiado pronto).
Están escritos de manera que con frecuencia convierten incluso conceptos simples en gramática y semántica torcidas y torcidas.

Asi que...

A la pregunta real. ¿Alguien puede explicar completamente la palabra clave forall en un lenguaje claro y sencillo (o, si existe en alguna parte, señalar una explicación tan clara que no haya visto) que no asuma que soy un matemático impregnado de la jerga?

Editado para añadir:

Hubo dos respuestas sobresalientes de las de mayor calidad a continuación, pero desafortunadamente solo puedo elegir una como la mejor. La respuesta de Norman fue detallada y útil, explicando las cosas de una manera que mostraba algunos de los fundamentos teóricos de forall y, al mismo tiempo, mostrándome algunas de las implicaciones prácticas de la misma. La respuesta de yairchu cubrió un área que nadie más mencionó (variables de tipo de ámbito) e ilustró todos los conceptos con código y una sesión de GHCi. Si fuera posible seleccionar los dos lo mejor, lo haría. Desafortunadamente, no puedo y, después de analizar detenidamente ambas respuestas, he decidido que yairchu recorta ligeramente a Norman debido al código ilustrativo y la explicación adjunta. Sin embargo, esto es un poco injusto, porque realmente necesitaba las dos respuestas para comprender esto hasta el punto de que forall no me deja con una leve sensación de temor cuando lo veo en una firma de tipo.

¿Alguien puede explicar completamente la palabra clave forall en un lenguaje claro y sencillo (o, si existe en alguna parte, señalar una explicación tan clara que no haya visto) que no asuma que soy un matemático impregnado de la jerga?

Voy a intentar explicar el significado y tal vez la aplicación de forall en el contexto de Haskell y sus sistemas tipográficos.

Pero antes de que entiendas, me gustaría dirigirte a una charla muy accesible y agradable de Runar Bjarnason titulada " Restricciones Liberar, Restricciones de Libertades ". La charla está llena de ejemplos de casos de uso del mundo real, así como ejemplos en Scala para respaldar esta afirmación, aunque no se menciona en absoluto. Trataré de explicar la perspectiva general a continuación.

CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN

Es muy importante digerir y creer en esta declaración para continuar con la siguiente explicación, por lo que le insto a que vea la charla (al menos en parte).

Ahora, un ejemplo muy común, que muestra la expresividad del sistema de tipos de Haskell es esta firma de tipo:

foo :: a -> a

Se dice que dada esta firma de tipo, solo hay una función que puede satisfacer este tipo y que es la función de identity o lo que se conoce más popularmente.

En las etapas iniciales de mi aprendizaje de Haskell, siempre me preguntaba las siguientes funciones:

foo 5 = 6 foo True = False

ambos satisfacen la firma de tipo anterior, entonces, ¿por qué la gente de Haskell afirma que es solo la id que satisface la firma de tipo?

Esto se debe a que hay un forall implícito oculto en la firma de tipo. El tipo real es:

id :: forall a. a -> a

Entonces, ahora volvamos a la afirmación: Las restricciones liberan, las libertades restringen

Traduciendo eso al sistema de tipos, esta declaración se convierte en:

Una restricción en el nivel de tipo, se convierte en una libertad en el nivel de término

Una libertad en el nivel de tipo, se convierte en una restricción en el nivel de término

Intentemos probar la primera afirmación:

Una restricción en el nivel de tipo.

Así que poniendo una restricción en nuestra firma de tipo

foo :: (Num a) => a -> a

se convierte en una libertad a nivel de término que nos da la libertad o flexibilidad para escribir todo esto

foo 5 = 6 foo 4 = 2 foo 7 = 9 ...

Lo mismo se puede observar al restringir a con cualquier otra clase de tipos, etc.

Entonces, a lo que se traduce esta firma de tipo: foo :: (Num a) => a -> a a es:

∃a , st a -> a, ∀a ∈ Num

Esto se conoce como cuantificación existencial, que se traduce en que existen algunas instancias de a para las que una función cuando se alimenta algo de tipo a devuelve algo del mismo tipo, y todas esas instancias pertenecen al conjunto de Números.

Por lo tanto, podemos ver que agregar una restricción (que debería pertenecer al conjunto de Números), libera el nivel de término para tener múltiples implementaciones posibles.

Ahora llegando a la segunda declaración y la que realmente lleva la explicación de forall :

Una libertad en el nivel de tipo, se convierte en una restricción en el nivel de término

Así que ahora liberemos la función al nivel de tipo:

foo :: forall a. a -> a

Ahora esto se traduce en:

∀a , a -> a

lo que significa que la implementación de esta firma de tipo debe ser tal que sea a -> a para todas las circunstancias.

Así que ahora esto comienza a restringirnos en el nivel de término. Ya no podemos escribir

foo 5 = 7

Porque esta implementación no satisfaría si ponemos un Bool . a puede ser un Char o un [Char] o un tipo de datos personalizado. Bajo cualquier circunstancia debe devolver algo del tipo similar. Esta libertad a nivel de tipo es lo que se conoce como cuantificación universal y la única función que puede satisfacer esto es

foo a = a

que se conoce comúnmente como la función de identity

Por lo tanto, forall es una liberty a nivel de tipo, cuyo propósito real es constrain el término de nivel a una implementación particular.

Están llenos de suposiciones de que he leído lo último en cualquier rama de las matemáticas discretas, la teoría de categorías o el álgebra abstracta que es popular esta semana. (Si nunca vuelvo a leer las palabras "consultar el documento para obtener detalles de la implementación", será demasiado pronto).

Er, y ¿qué pasa con la lógica de primer orden simple? forall es bastante claro en referencia a la cuantificación universal , y en ese contexto el término existential tiene más sentido, aunque sería menos incómodo si existiera una palabra clave. Si la cuantificación es efectivamente universal o existencial depende de la ubicación del cuantificador en relación con el lugar donde se utilizan las variables en qué lado de la flecha de función y todo es un poco confuso.

Entonces, si eso no ayuda, o si simplemente no le gusta la lógica simbólica, desde una perspectiva de programación más funcional, puede pensar que las variables de tipo son solo parámetros de tipo (implícitos) para la función. Las funciones que toman parámetros de tipo en este sentido se escriben tradicionalmente con una lambda mayúscula por cualquier razón, que escribiré aquí como // .

Por lo tanto, considere la función de id :

id :: forall a. a -> a id x = x

Podemos reescribirlo como lambdas, moviendo el "parámetro de tipo" fuera de la firma de tipo y agregando anotaciones de tipo en línea:

id = //a -> (/x -> x) :: a -> a

Aquí está la misma cosa hecha para const :

const = //a b -> (/x y -> x) :: a -> b -> a

Así que su función de bar podría ser algo como esto:

bar = //a -> (/f -> (''t'', True)) :: (a -> a) -> (Char, Bool)

Tenga en cuenta que el tipo de función dada a la bar como argumento depende del parámetro de tipo de bar . Considera si tuvieras algo como esto en su lugar:

bar2 = //a -> (/f -> (f ''t'', True)) :: (a -> a) -> (Char, Bool)

Aquí bar2 está aplicando la función a algo de tipo Char , por lo que dar a bar2 cualquier parámetro de tipo distinto a Char causará un error de tipo.

Por otro lado, esto es lo que foo podría parecer:

foo = (/f -> (f Char ''t'', f Bool True))

A diferencia de la bar , ¡ foo no toma ningún tipo de parámetros! Toma una función que a su vez toma un parámetro de tipo, luego aplica esa función a dos tipos diferentes .

Entonces, cuando vea un forall en una firma de tipo, solo piense en ella como una expresión lambda para las firmas de tipo . Al igual que las lambdas normales, el alcance de forall extiende lo más a la derecha posible, hasta el paréntesis, y al igual que las variables vinculadas en un lambda regular, las variables de tipo unidas a la forall solo están dentro del alcance dentro de la expresión cuantificada.

Post scriptum : Tal vez se pregunte: ahora que estamos pensando en las funciones que toman parámetros de tipo, ¿por qué no podemos hacer algo más interesante con esos parámetros que colocarlos en una firma de tipo? La respuesta es que podemos!

Una función que coloca las variables de tipo junto con una etiqueta y devuelve un nuevo tipo es un constructor de tipo , en el que podría escribir algo como esto:

Either = //a b -> ...

Pero necesitaríamos una notación completamente nueva, porque la forma en que se escribe ese tipo, como Either ab , ya sugiere "aplicar la función Either a estos parámetros".

Por otro lado, una función que tipo de "concordancias de patrón" en sus parámetros de tipo, devolviendo valores diferentes para tipos diferentes, es un método de una clase de tipo . Una ligera expansión a mi // sintaxis anterior sugiere algo como esto:

fmap = // f a b -> case f of Maybe -> (/g x -> case x of Just y -> Just b g y Nothing -> Nothing b) :: (a -> b) -> Maybe a -> Maybe b [] -> (/g x -> case x of (y:ys) -> g y : fmap [] a b g ys [] -> [] b) :: (a -> b) -> [a] -> [b]

Personalmente, creo que prefiero la sintaxis real de Haskell ...

Una función que "empareja" sus parámetros de tipo y devuelve un tipo arbitrario y existente es una familia de tipos o una dependencia funcional; en el primer caso, incluso se parece mucho a una definición de función.

¿Cómo es existencial existencial?

Con la Cuantificación existencial, todas data definiciones de data significan que, el valor contenido puede ser de cualquier tipo adecuado, no que debe ser de todos los tipos adecuados. - la respuesta de yachiru

Una explicación de por qué data definiciones de data en general son isomorfas para (exists a. a) (pseudo-Haskell) se puede encontrar en los "tipos cuantificados de Haskell / existencialmente" de wikibooks .

El siguiente es un breve resumen textual:

data T = forall a. MkT a -- an existential datatype MkT :: forall a. a -> T -- the type of the existential constructor

Cuando se empareja / deconstruye MkT x , ¿cuál es el tipo de x ?

foo (MkT x) = ... -- -- what is the type of x?

x puede ser de cualquier tipo (como se indica en el forall ), por lo que su tipo es:

x :: exists a. a -- (pseudo-Haskell)

Por lo tanto, los siguientes son isomorfos:

data T = forall a. MkT a -- an existential datatype data T = MkT (exists a. a) -- (pseudo-Haskell)

forall significa forall

Mi interpretación simple de todo esto es que "para todos realmente significa ''para todos''". Una distinción importante que se debe hacer es el impacto de forall en la aplicación de definición versus función.

Un forall significa que la definición del valor o función debe ser polimórfica.

Si lo que se está definiendo es un valor polimórfico, significa que el valor debe ser válido para todos los adecuados, lo que es bastante restrictivo.

Si lo que se define es una función polimórfica, significa que la función debe ser válida para todos los adecuados, lo que no es restrictivo porque el hecho de que sea polimórfica no significa que el parámetro que se aplica tenga que ser polimórfico. Es decir, si la función es válida para todos los a , entonces a la inversa, cualquier a adecuado puede aplicarse a la función. Sin embargo, el tipo de parámetro solo se puede elegir una vez en la definición de la función.

Si un forall está dentro del tipo de parámetro de función (es decir, un Rank2Type ), significa que el parámetro aplicado debe ser realmente polimórfico, para que sea coherente con la idea de que la definición de medios es polimórfica. En este caso, el tipo de parámetro se puede elegir más de una vez en la definición de la función ( "y se elige por la implementación de la función", según lo señalado por Norman )

Por lo tanto, la razón por data definiciones de data existenciales permite que cualquiera sea es porque el constructor de datos es una función polimórfica:

MkT :: forall a. a -> T

tipo de MkT :: a -> *

Lo que significa que cualquier a se puede aplicar a la función. A diferencia de, digamos, un valor polimórfico:

valueT :: forall a. [a]

tipo de valorT :: a

Lo que significa que la definición de valueT debe ser polimórfica. En este caso, valueT se puede definir como una lista vacía [] de todos los tipos.

[] :: [t]

Diferencias

A pesar de que el significado de foralles consistente en ExistentialQuantificationy RankNType, existencials tiene una diferencia ya que el dataconstructor se puede usar en la comparación de patrones. Como se documenta en la guía del usuario de ghc :

Cuando se combina el patrón, cada coincidencia de patrón introduce un nuevo tipo distinto para cada variable de tipo existencial. Estos tipos no se pueden unificar con ningún otro tipo, ni pueden escapar del alcance de la coincidencia del patrón.

Aquí hay una explicación rápida y sucia en términos sencillos con los que es probable que ya esté familiarizado.

La palabra clave forall solo se usa de una manera en Haskell. Siempre significa lo mismo cuando lo ves.

Cuantificacion universal

Un tipo universalmente cuantificado es un tipo de formulario para todos forall a. fa forall a. fa . Un valor de ese tipo puede considerarse como una función que toma un tipo a como su argumento y devuelve un valor de tipo fa . Excepto que en Haskell estos argumentos de tipo son pasados implícitamente por el sistema de tipos. Esta "función" tiene que proporcionarle el mismo valor, independientemente del tipo que reciba, por lo que el valor es polimórfico .

Por ejemplo, considere el tipo para todos forall a. [a] forall a. [a] . Un valor de ese tipo toma otro tipo a y le devuelve una lista de elementos de ese mismo tipo a . Por supuesto, solo hay una implementación posible. Tendría que darle la lista vacía porque podría ser absolutamente de cualquier tipo. La lista vacía es el único valor de lista que es polimórfico en su tipo de elemento (ya que no tiene elementos).

O el tipo para todos forall a. a -> a forall a. a -> a . La persona que llama a dicha función proporciona tanto un tipo a como un valor de tipo a . La implementación entonces tiene que devolver un valor de ese mismo tipo a . Solo hay una posible implementación de nuevo. Tendría que devolver el mismo valor que se le dio.

Cuantificacion existencial

Un tipo cuantificado existencialmente tendría la forma exists a. fa exists a. fa , si haskell apoyó esa notación. Un valor de ese tipo se puede considerar como un par (o un "producto") que consiste en un tipo a y un valor de tipo fa .

Por ejemplo, si tiene un valor de tipo exists a. [a] exists a. [a] , tienes una lista de elementos de algún tipo. Podría ser de cualquier tipo, pero incluso si no sabe qué es lo que puede hacer con esa lista. Puede revertirlo o puede contar el número de elementos, o realizar cualquier otra operación de lista que no dependa del tipo de elementos.

OK, así que espera un minuto. ¿Por qué Haskell usa forall para indicar un tipo "existencial" como el siguiente?

data ShowBox = forall s. Show s => SB s

Puede ser confuso, pero realmente describe el tipo de constructor de datos SB :

SB :: forall s. Show s => s -> ShowBox

Una vez construido, puede pensar que un valor de tipo ShowBox consiste en dos cosas. Es un tipo s junto con un valor de tipo s . En otras palabras, es un valor de un tipo cuantificado existencialmente. ShowBox realmente podría escribirse como exists s. Show s => s exists s. Show s => s , si Haskell soporta esa notación.

runST y amigos

Dado eso, ¿en qué se diferencian estos?

foo :: (forall a. a -> a) -> (Char,Bool) bar :: forall a. ((a -> a) -> (Char, Bool))

Tomemos primero la bar . Toma un tipo a y una función de tipo a -> a , y produce un valor de tipo (Char, Bool) . Podríamos elegir Int como a y asignarle una función de tipo Int -> Int por ejemplo. Pero foo es diferente. Requiere que la implementación de foo sea capaz de pasar cualquier tipo que quiera a la función que le demos. Así que la única función que podríamos razonablemente darle es id .

Ahora deberíamos poder abordar el significado del tipo de runST :

runST :: forall a. (forall s. ST s a) -> a

Por runST tanto, runST debe ser capaz de generar un valor de tipo a , sin importar qué tipo damos como. Para ello, necesita un argumento de tipo forall s. ST sa forall s. ST sa que bajo el capó es solo una función de tipo para todos forall s. s -> (a, s) forall s. s -> (a, s) . Esa función tiene que ser capaz de producir un valor de tipo (a, s) sin importar qué tipo la implementación de runST decida dar como s .

¿OK y eso qué? El beneficio es que esto pone una restricción en el llamador de runST en que el tipo a no puede involucrar al tipo s en absoluto. No puede pasarle un valor de tipo ST s [s] , por ejemplo. Lo que eso significa en la práctica es que la implementación de runST es libre de realizar la mutación con el valor de tipo s . El sistema de tipos garantiza que esta mutación es local para la implementación de runST .

El tipo de runST es un ejemplo de un tipo polimórfico de rango 2 porque el tipo de su argumento contiene un cuantificador forall . El tipo de foo anterior también es de rango 2. Un tipo polimórfico ordinario, como el de bar , es rango-1, pero se convierte en rango-2 si se requiere que los tipos de argumentos sean polimórficos, con su propio cuantificador para todos. Y si una función toma argumentos de rango 2, entonces su tipo es rango 3, y así sucesivamente. En general, un tipo que toma argumentos polimórficos de rango n tiene rango n + 1 .

Comencemos con un ejemplo de código:

foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b foob postProcess onNothin onJust mval = postProcess val where val :: b val = maybe onNothin onJust mval

Este código no se compila (error de sintaxis) en Haskell 98. Requiere una extensión para admitir la palabra clave forall .

Básicamente, hay 3 usos comunes diferentes para la palabra clave forall (o al menos así parece ), y cada uno tiene su propia extensión Haskell: ScopedTypeVariables , RankNTypes / Rank2Types , ExistentialQuantification .

El código anterior no recibe un error de sintaxis con ninguno de los habilitados, sino solo con las comprobaciones de tipo con ScopedTypeVariables habilitado.

Variables de tipo de ámbito:

Las variables de tipo de ámbito ayudan a especificar tipos para el código dentro de las cláusulas. Hace que la b en val :: b la misma que la b en foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b .

Un punto confuso : puede que escuche que cuando omite el forall de un tipo, en realidad todavía está allí implícitamente. ( De la respuesta de Norman: "normalmente estos idiomas omiten el forall de los tipos polimórficos" ). Esta afirmación es correcta, pero se refiere a los otros usos de forall , y no al uso de ScopedTypeVariables .

Tipos de rango-N:

Comencemos con que mayb :: b -> (a -> b) -> Maybe a -> b es equivalente a mayb :: forall a b. b -> (a -> b) -> Maybe a -> b mayb :: forall a b. b -> (a -> b) -> Maybe a -> b , excepto cuando ScopedTypeVariables está habilitado.

Esto significa que funciona para cada a y b .

Digamos que quieres hacer algo como esto.

ghci> let putInList x = [x] ghci> liftTup putInList (5, "Blah") ([5], ["Blah"])

¿Cuál debe ser el tipo de este liftTup ? Es liftTup :: (forall x. x -> fx) -> (a, b) -> (fa, fb) . Para ver por qué, intentemos codificarlo:

ghci> let liftTup liftFunc (a, b) = (liftFunc a, liftFunc b) ghci> liftTup (/x -> [x]) (5, "Hello") No instance for (Num [Char]) ... ghci> -- huh? ghci> :t liftTup liftTup :: (t -> t1) -> (t, t) -> (t1, t1)

"Hmm ... ¿por qué GHC deduce que la tupla debe contener dos del mismo tipo? Digamos que no tienen que ser"

-- test.hs liftTup :: (x -> f x) -> (a, b) -> (f a, f b) liftTup liftFunc (t, v) = (liftFunc t, liftFunc v) ghci> :l test.hs Couldnt match expected type ''x'' against inferred type ''b'' ...

Hmm así que aquí ghc no nos permite aplicar liftFunc en v porque v :: b y liftFunc quiere una x . ¡Realmente queremos que nuestra función obtenga una función que acepte cualquier x posible!

{-# LANGUAGE RankNTypes #-} liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b) liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

Entonces, no es liftTup que funciona para todas las x , es la función que cumple lo que hace.

Cuantificación existencial:

Vamos a usar un ejemplo:

-- test.hs {-# LANGUAGE ExistentialQuantification #-} data EQList = forall a. EQList [a] eqListLen :: EQList -> Int eqListLen (EQList x) = length x ghci> :l test.hs ghci> eqListLen $ EQList ["Hello", "World"] 2

¿En qué se diferencia eso de Rank-N-Types?

ghci> :set -XRankNTypes ghci> length (["Hello", "World"] :: forall a. [a]) Couldnt match expected type ''a'' against inferred type ''[Char]'' ...

Con Rank-N-Types, todo significa que su expresión debe coincidir con todas las a s posibles. Por ejemplo:

ghci> length ([] :: forall a. [a]) 0

Una lista vacía funciona como una lista de cualquier tipo.

Por lo tanto, con la Cuantificación existencial, todas data definiciones de data significan que, el valor contenido puede ser de cualquier tipo adecuado, no que debe ser de todos los tipos adecuados.

La razón por la cual hay diferentes usos de esta palabra clave es que en realidad se usa en al menos dos extensiones de sistema de tipos diferentes: tipos de rango más alto y existenciales.

Probablemente sea mejor leer y entender estas dos cosas por separado, en lugar de intentar obtener una explicación de por qué ''para todos'' es un poco de sintaxis apropiada en ambos al mismo tiempo.

Mi respuesta original:

¿Alguien puede explicar completamente la palabra clave forall en un lenguaje claro y sencillo?

Como indica Norman, es muy difícil dar una explicación clara y clara en inglés de un término técnico de la teoría de tipos. Aunque todos estamos tratando.

Solo hay una cosa que recordar acerca de ''forall'': une los tipos a algún alcance . Una vez que entiendes eso, todo es bastante fácil. Es el equivalente de ''lambda'' (o una forma de ''let'') en el nivel de tipo: Norman Ramsey utiliza la noción de "izquierda" / "arriba" para transmitir este mismo concepto de alcance en su excelente respuesta .

La mayoría de los usos de ''forall'' son muy simples, y puede encontrarlos introducidos en el Manual del usuario de GHC, S7.8 ., En particular, el excelente S7.8.5 en las formas anidadas de ''forall''.

En Haskell, por lo general, dejamos de lado la carpeta para tipos, cuando el tipo está universalmente cuantificado, así:

length :: forall a. [a] -> Int

es equivalente a:

length :: [a] -> Int

Eso es.

Como ahora puede vincular las variables de tipo a algún ámbito, puede tener otros ámbitos que no sean el nivel superior (" cuantificados universalmente "), como su primer ejemplo, donde la variable de tipo solo es visible dentro de la estructura de datos. Esto permite tipos ocultos (" tipos existenciales "). O podemos tener anidación arbitraria de enlaces ("tipos de rango N").

Para comprender a fondo los sistemas de tipos, tendrá que aprender un poco de jerga. Esa es la naturaleza de la informática. Sin embargo, los usos simples, como el anterior, deberían poder ser captados intuitivamente, a través de una analogía con ''dejar'' en el nivel de valor. Una gran introducción es Launchbury y Peyton Jones .