¿Puede alguien completamente explicar la palabra clave forall en un inglés claro y sencillo?

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

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

• Es un cuantificador. Tienes que tener al menos un poco de lógica (cálculo de predicados) para haber visto un cuantificador universal o existencial. Si nunca has visto el cálculo de predicados o no te sientes cómodo con los cuantificadores (y haber visto estudiantes durante los exámenes de calificación de doctorado que no se sienten cómodos), entonces para usted, no hay una explicación fácil de forall.

• Es un cuantificador tipo. Si no has visto System F y no has practicado la escritura de tipos polimórficos, encontrarás forall confuso. La experiencia con Haskell o ML no es suficiente, porque normalmente estos lenguajes omiten el forall de los tipos polimórficos. (En mi mente, este es un lenguaje-diseño error.)

• En Haskell en particular, forall se usa de maneras que encuentro confusas. (No soy un teórico de tipos, pero mi trabajo me pone en contacto con un lote de teoría de tipos, y estoy bastante cómodo con ella. Para mí, la principal fuente de confusión es que forall se usa para codificar un tipo que yo mismo preferiría escribir con exists. Está justificado por un poco complicado de isomorfismo de tipo que involucra cuantificadores y flechas, y cada vez que quiero entenderlo, tengo para buscar cosas y resolver el isomorfismo yo mismo.

  Si no te sientes cómodo con la idea del isomorfismo de tipos, o si no tienes ninguna práctica pensando en los isomorfismos de tipos, este uso de forall te va a obstaculizar.

• Mientras que el concepto general de forall es siempre el mismo (enlace para introducir una variable de tipo), los detalles de los diferentes usos pueden variar significativamente. El inglés informal no es una buena herramienta para explicar las variaciones. Realmente entiende lo que está pasando, necesitas matemáticas. En este caso, las matemáticas relevantes se pueden encontrar en el texto introductorio de Benjamin Pierce Tipos y Lenguajes de programación , que es un libro muy bueno.

En cuanto a sus ejemplos particulares, {[43]]}

• runST debería hacer que te duela la cabeza. Los tipos de rango más alto (forall a la izquierda de una flecha) rara vez se encuentran en la naturaleza. Les animo a leer el documento que introdujo runST: "Hilos de Estado Funcionales perezosos". Este es un muy buen artículo, y le dará una intuición mucho mejor para el tipo de runST en particular y para los tipos de rango superior en general. La explicación toma varias páginas, está muy bien hecha, y no voy a tratar de condensarla aquí.

• Considere

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

  Si llamo a bar, simplemente puedo elegir cualquier tipo a que me guste, y puedo pasarle una función de tipo a a tipo a. Por ejemplo, I puede pasar la función (+1) o la función reverse. Se puede pensar en el forall como diciendo "Tengo que elegir el tipo ahora". (La palabra técnica para elegir el tipo es instanciar.)

  Las restricciones a la llamada 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 falla, como undefined. La razón es que con foo, el forall está a la izquierda de la flecha, así que como el llamante de foo no tengo que elegir lo que a es-más bien es la implementación de foo que tiene que elegir lo que a es. Debido a que forall está a la izquierda de la flecha, en lugar de por encima de la flecha como en bar, la instanciación tiene lugar 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 se puede entender solo por alguien que ha estudiado matemáticas. Incluso las explicaciones parciales son difíciles de entender sin matemáticas. Pero tal vez mis explicaciones parciales, no matemáticas ayudan 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 tipos están escritos y todo tiene que ver con árboles de sintaxis abstracta. En la sintaxis abstracta, a forall toma el nombre de una variable de tipo, y luego hay un tipo completo "debajo" del forall. Una flecha toma dos tipos (tipo argumento y tipo resultado) y forma un nuevo tipo (el tipo función). El tipo de argumento es "a la izquierda de" la flecha; es el hijo izquierdo de la flecha en el árbol de sintaxis abstracta.

Ejemplos:

• En forall a . [a] -> [a], el forall está 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 " a forall a la izquierda de an flecha". (Estoy usando tipos como este en un optimizador en el que estoy trabajando.)

Mi respuesta original:

¿Puede alguien explicar completamente la palabra clave forall en un inglés claro y sencillo

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

Solo hay una cosa que recordar acerca de 'forall': enlaza tipos a some scope . 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 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 los puedes encontrar introducidos en el GHC Users Manual, S7.8 ., particularmente el excelente S7.8. 5 en anidado formas de 'forall'.

En Haskell, solemos dejar el aglutinante para los tipos, cuando el tipo es universalmente cuantificado, así:

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

Es equivalente a:

length :: [a] -> Int

Eso es todo.

Dado que ahora puede enlazar variables de tipo a algún ámbito, puede tener ámbitos otros que el nivel superior (" universalmente cuantificado "), como su primer ejemplo, donde la variable de tipo solo es visible dentro de la estructura de datos. Esto permite para tipos ocultos (" tipos existenciales "). O podemos tener arbitrario anidamiento de enlaces ("tipos de rango N").

Para entender profundamente los sistemas de tipos, necesitará aprender algo de jerga. Eso es la naturaleza de la informática. Sin embargo, los usos simples, como los anteriores, deben ser capaz de ser captado intuitivamente, a través de la analogía con ' let ' en el nivel de valor. Un gran introducción es[37]}Launchbury y Peyton Jones .

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

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

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

Por lo tanto, considere la función 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á lo mismo hecho a const:

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

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

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

Tenga en cuenta que el tipo de la función dada a bar como argumento depende del parámetro type de bar. Considere si usted tuvo 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 bar2 cualquier parámetro de tipo que no sea 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 bar, foo en realidad no toma ningún tipo parámetros en absoluto! Toma una función que por sí misma toma un parámetro de tipo, luego aplica esa función a dos tipos diferentes.

Así que cuando vea un forall en una firma de tipo, piense en ello como una expresión lambda para las firmas de tipo. Al igual que las lambdas regulares, el alcance de forall se extiende lo más a la derecha posible, hasta encerrar paréntesis, y al igual que las variables enlazadas en una lambda regular, las variables de tipo enlazadas por una forall solo están en alcance dentro de la expresión cuantificada.

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

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

Either = /\a b -> ...

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

Por otro lado, una función que "pattern coincide" en sus parámetros de tipo, devolviendo diferentes valores para diferentes tipos, 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 "pattern coincide" con sus parámetros de tipo y devuelve un tipo arbitrario existente es una familia de tipos o dependencia funcional {en el primer caso, incluso ya se parece mucho a una definición de función.

Aquí hay una explicación rápida y sucia en términos claros con la que probablemente ya esté familiarizado.

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

Cuantificación universal

Un tipo universalmente cuantificado es un tipo de la forma forall a. f a. Un valor de ese tipo puede ser considerado como una función que toma un tipo a como argumento y devuelve un valor de tipo f a. Excepto que en Haskell estos argumentos de tipo son pasados implícitamente por el sistema de tipos. Esta "función" tiene que darle el mismo valor sin importar el tipo que reciba, por lo que el valor es polimórfico.

Por ejemplo, considere el tipo forall a. [a]. Un valor de ese tipo toma otro tipo a y le devuelve una lista de elementos del mismo tipo a. Por supuesto, sólo hay una posible aplicación. Tendría que darte la lista vacía porque a podría ser absolutamente 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 forall a. a -> a. El llamador de tal función proporciona tanto un tipo a como un valor de tipo a. La implementación debe devolver un valor del mismo tipo a. Solo hay una posible implementación de nuevo. Tendría que devolver el mismo valor que se le dio.

Existencial cuantificación

Un tipo existencialmente cuantificado tendría la forma exists a. f a, si Haskell soportara esa notación. Un valor de ese tipo puede considerarse como un par (o un "producto") que consiste en un tipo a y un valor de tipo f a.

Por ejemplo, si tenemos un valor de tipo exists a. [a], tiene una lista de elementos de algún tipo. Podría ser cualquier tipo, pero incluso si usted no sabe lo que es hay mucho que podría hacer a tal lista. Podrías invierta, o podría contar el número de elementos, o realizar cualquier otra operación de lista que no dependa del tipo de los elementos.

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

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

Puede ser confuso, pero en realidad está describiendo el tipo del constructor de datos SB:

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

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

runST y amigos

Dado eso, ¿en qué se diferencian?

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

Tomemos primero 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 darle una función de tipo Int -> Int para ejemplo. Pero foo es diferente. Requiere que la implementación de foo sea capaz de pasar cualquier tipo que desee a la función que le damos. Así que la única función que podríamos razonablemente darle es id.

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

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

Así que runST tiene que ser capaz de producir un valor de tipo a, no importa qué tipo damos como a. Para hacerlo, necesita un argumento de type forall s. ST s a que bajo el capó es solo una función de type forall s. s -> (a, s). Esa función entonces tiene que ser capaz de producir un valor de tipo (a, s) no importa qué tipo la implementación de runST decide dar como s.

OK, ¿y 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. Tipo el sistema garantiza que esta mutación es local a la implementación de runST.

El tipo de runST es un ejemplo de un tipo polimórfico rank-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 rank-1, pero se convierte en rank-2 si se requiere que los tipos de argumentos sean polimórficos, con su propio cuantificador forall. Y si una función toma argumentos rank-2 entonces su tipo es rango-3, y así sucesivamente. En general, un tipo que toma argumentos polimórficos de rank n tiene rank n + 1.

La razón por la que 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 superior y existenciales.

Probablemente sea mejor leer y entender esas dos cosas por separado, en lugar de tratar de obtener una explicación de por qué 'forall' es un bit apropiado de sintaxis en ambos al mismo tiempo.

¿Puede alguien explicar completamente la palabra clave forall en un inglés claro y sencillo (o, si existe en algún lugar, señalar una explicación tan clara que me he perdido) que no asuma que soy un matemático empapado en la jerga?

Voy a tratar de explicar solo el significado y tal vez la aplicación de forall en el contexto de Haskell y sus sistemas de tipos.

Pero antes de que entiendas que me gustaría dirigirte a una charla muy accesible y agradable por Runar Bjarnason tituló"Constraints Liberate, Liberties Constrain". La charla está llena de ejemplos de casos de uso del mundo real, así como ejemplos en Scala para apoyar esta declaración, aunque no menciona forall. Intentaré explicar la perspectiva forall a continuación.

                CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN

Es muy importante digerir y creer esta declaración para proceder con la siguiente explicación, así que les insto a que vean la charla(al menos partes de ella).

Ahora un ejemplo muy común, mostrando la expresividad del sistema de tipos 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 identity o lo que es más popularmente conocido id.

En las etapas iniciales de mi aprendizaje de Haskell, siempre me pregunté las siguientes funciones: {[36]]}

foo 5 = 6

foo True = False

Ambos satisfacen la firma de tipo anterior, entonces por qué la gente de Haskell afirma que es id solo 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

Así que, ahora volvamos a la declaración: Las restricciones liberan, las libertades restringen

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

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

Y

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

Tratemos de probar la primera afirmación: {[36]]}

Una restricción a nivel de tipo..

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

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

se convierte en una libertad a nivel de término nos da la libertad o flexibilidad para escribir todos estos

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

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

Así que ahora a lo que se traduce esta firma de tipo: foo :: (Num a) => a -> a es:

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

Esto se conoce como cuantificación existencial, que se traduce como existen algunas instancias de a para las cuales 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 la adición de una restricción(que a debe pertenecer al conjunto de Números), libera el término nivel para tener múltiples implementaciones posibles.

Ahora llegando al segundo 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 en el nivel de tipo:

foo :: forall a. a -> a

Ahora esto se traduce como:

∀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 limitarnos a nivel de término. No podemos escritura más larga

foo 5 = 7

Porque esta implementación no satisfaría si pusiéramos a como 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 identity

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

¿Cómo es existencial existencial?

Con Cuantificación Existencial, forall s en data definiciones media que, el valor contenido puede ser de cualquier tipo adecuado, no que debeser de todos los tipos adecuados. -- la respuesta de yachiru

Una explicación de por qué {[7] {} en[8]} definiciones son isomorfos a (exists a. a) (pseudo-Haskell) se puede encontrar en wikilibros del "Haskell/Existencialmente cuantificada tipos " .

El siguiente es un breve resumen literal:

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

Cuando el patrón de coincidencia/deconstrucción MkT x, ¿cuál es el tipo de x?

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

x puede ser 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:{[51]]}

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 "forall realmente significa 'para todos'". Una distinción importante a hacer es el impacto de forallen la definición versus función aplicación.

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

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

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

Si a forall está dentro del tipo del parámetro de función (es decir, a Rank2Type), entonces significa el parámetro aplicadodebe ser verdaderamente polimórfico, para ser consistente con la idea de forallsignifica la definición es polimórfica. En este caso, el tipo del 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", como señala Norman)

Por lo tanto, la razón por la que existencial data definiciones permite cualquier a es porque el constructor de datos es un polimórfico función :

MkT :: forall a. a -> T

Tipo de MkT :: a -> *

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

valueT :: forall a. [a]

Tipo de valor :: a

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

[] :: [t]

Diferencias

Aunque el significado de forall es consistente en ExistentialQuantification y RankNType, existentials tiene una diferencia ya que el constructor data se puede usar en la coincidencia de patrones. Como se documenta en la guía del usuario de ghc :

Cuando la coincidencia de patrones, cada coincidencia de patrones 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 de patrón.