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

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

Sin embargo, esto es solo un subconjunto de cómo forallse usa y simplemente no puedo entender cómo se usa en cosas como esta:

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

O explicando por qué son diferentes:

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

O todo el RankNTypesasunto ...

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

1. 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, fooy bararriba).
2. Están repletos de suposiciones que he leído lo último en cualquier rama de matemáticas discretas, teoría de categorías o álgebra abstracta que es popular esta semana. (Si no leí las palabras "consultar el documento sea cual sea para los detalles de la implementación" de nuevo, será demasiado pronto.)
3. Están escritos de manera que con frecuencia convierten incluso conceptos simples en gramática y semántica tortuosamente retorcida y fracturada.

Entonces...

A la pregunta real. ¿Alguien puede explicar completamente la forallpalabra clave en un inglés claro y simple (o, si existe en algún lugar, señalar una explicación tan clara que me haya perdido) que no asume que soy un matemático inmerso en la jerga?

Editado para agregar:

Hubo dos respuestas destacadas 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 mostró algunos de los fundamentos teóricos forally al mismo tiempo me mostró algunas de las implicaciones prácticas de la misma. la respuesta de yairchucubrió 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 ambos de la mejor manera, lo haría. Desafortunadamente, no puedo y, después de mirar detenidamente ambas respuestas, he decidido que Yairchu supera ligeramente a Norman debido al código ilustrativo y la explicación adjunta. Sin embargo, esto es un poco injusto, porque realmente necesitaba ambas respuestas para entender esto hasta el punto que forallno me deja con una leve sensación de temor cuando lo veo en una firma de tipo.

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 forallpalabra clave.

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

El código anterior no obtiene un error de sintaxis con ninguno de los habilitados, sino solo verificaciones de tipo con ScopedTypeVariableshabilitado.

Variables de tipo con ámbito:

Las variables de tipo con ámbito ayudan a especificar tipos para el código dentro de las wherecláusulas. Esto hace que el ben val :: bel mismo que el bde foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b.

Un punto confuso : puede escuchar que cuando omite el forallde un tipo, en realidad todavía está implícitamente allí. ( 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 forally no al ScopedTypeVariablesuso.

Rango-N-Tipos:

Comencemos con eso mayb :: b -> (a -> b) -> Maybe a -> bes equivalente a mayb :: forall a b. b -> (a -> b) -> Maybe a -> b, excepto cuando ScopedTypeVariablesestá habilitado.

Esto significa que funciona para todos ay cada uno 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 esto liftTup? Es liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b). 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 infiere 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 apliquemos liftFuncel vdebido v :: by liftFuncquiere una x. ¡Realmente queremos que nuestra función obtenga una función que acepte cualquier posible x!

{-# 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 liftTupque funcione para todos x, es la función que obtiene lo que hace.

Cuantificación existencial:

Usemos 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

¿Cómo es eso diferente de Rank-N-types?

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

Con Rango-N-Tipos, forall asignifica que su expresión debe ajustarse a todos los as posibles . Por ejemplo:

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

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

Entonces, con la cuantificación existencial, foralls en las datadefiniciones significa que, el valor contenido puede ser de cualquier tipo adecuado, no que debe ser de todos los tipos adecuados.

¿Alguien puede explicar completamente la palabra clave forall en inglés claro y claro?

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

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

• Es un cuantificador. Debe tener al menos un poco de lógica (cálculo de predicados) para haber visto un cuantificador universal o existencial. Si nunca ha visto el cálculo 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 están cómodos), entonces no hay una explicación fácil para usted forall.

• Es un cuantificador de tipo . Si no ha visto el Sistema F y ha tenido algo de práctica escribiendo tipos polimórficos, le resultará forallconfuso. La experiencia con Haskell o ML no es suficiente, porque normalmente estos idiomas omiten los foralltipos polimórficos. (En mi opinión, este es un error de diseño del lenguaje).

• En Haskell en particular, forallse usa de formas que me parecen confusas. (No soy un teórico de tipos, pero mi trabajo me pone en contacto con mucha teoría de tipos, y me siento bastante cómodo con eso). Para mí, la principal fuente de confusión es que forallse 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 que buscar cosas y resolver el isomorfismo yo mismo.

  Si no se siente cómodo con la idea del isomorfismo de tipo, o si no tiene ninguna práctica pensando en isomorfismos de tipo, este uso foralllo va a obstaculizar.

• Si bien el concepto general de forallsiempre es 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 comprender realmente lo que está sucediendo, 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 libro muy bueno.

En cuanto a sus ejemplos particulares,

• runST debería hacerte doler la cabeza. Los tipos de rango superior (a la izquierda de una flecha) rara vez se encuentran en la naturaleza. Le animo a leer el documento que introdujo runST: "Hilos de estado funcional perezoso" . Este es un documento realmente bueno, y le dará una intuición mucho mejor para el tipo runSTen 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í.

• Considerar

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

  Si llamo bar, simplemente puedo elegir cualquier tipo aque me guste y puedo pasarle una función de tipo aa tipo a. Por ejemplo, puedo pasar la función (+1)o la función reverse. Puedes pensar forallque dice "Ahora tengo que elegir el tipo". (La palabra técnica para elegir el tipo es instanciar ).

  Las restricciones a las llamadas fooson mucho más estrictas: el argumento foo debe ser una función polimórfica. Con ese tipo, las únicas funciones a las que puedo pasar fooson ido una función que siempre diverge o errores, como undefined. La razón es que foo, con , forallestá a la izquierda de la flecha, de modo que la persona que llama foono puedo elegir lo que aes, sino que la implementación de fooeso es elegir lo que aes. Debido a que forallestá a la izquierda de la flecha, en lugar de 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 forallpalabra clave requiere matemática y solo puede ser entendida por alguien que haya estudiado matemática. Incluso las explicaciones parciales son difíciles de entender sin las matemáticas. Pero tal vez mis explicaciones parciales, no matemáticas, ayuden un poco. ¡Ve a leer Launchbury y Peyton Jones 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 tienen mucho que ver con los árboles de sintaxis abstracta. En la sintaxis abstracta, a foralltoma 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 está "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á 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 poco a la izquierda de una flecha". (Estoy usando tipos como este en un optimizador en el que estoy trabajando).

Mi respuesta original:

¿Alguien puede explicar completamente la palabra clave forall en inglés claro y claro?

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. Sin embargo, todos lo intentamos.

Solo hay una cosa para recordar sobre 'forall': vincula 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 ., Particularmente el excelente S7.8.5 sobre formas anidadas de 'forall'.

En Haskell, generalmente dejamos el aglutinante para los tipos, cuando el tipo está universalmente cuantificado, así:

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

es equivalente a:

length :: [a] -> Int

Eso es.

Como puede vincular las variables de tipo ahora a cierto alcance, puede tener ámbitos distintos del nivel superior (" universalmente cuantificado "), 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 anidamiento arbitrario de enlaces ("tipos de rango N").

Para comprender a fondo los sistemas de tipos, deberá aprender algo de jerga. Esa es la naturaleza de la informática. Sin embargo, los usos simples, como los anteriores, deberían poder captarse intuitivamente, por analogía con 'let' en el nivel de valor. Una gran introducción es Launchbury y Peyton Jones .

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

Er, ¿y qué hay de la lógica simple de primer orden? foralles bastante claro en referencia a la cuantificación universal , y en ese contexto el término existencial también tiene más sentido, aunque sería menos incómodo si hubiera una existspalabra 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 usan 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 le gusta la lógica simbólica, desde una perspectiva más funcional de programación, 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 usando una lambda mayúscula por cualquier razón, que escribiré aquí como /\.

Entonces, considere la idfunción:

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 para const:

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

Entonces su barfunción 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 barcomo argumento depende del barparámetro de tipo de. Considere si tenía algo como esto en su lugar:

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

Aquí bar2está aplicando la función a algo de tipo Char, por lo que dar bar2cualquier parámetro de tipo distinto de Charcausará un error de tipo.

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

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

¡A diferencia bar, en foorealidad no toma ningún tipo de parámetro! Toma una función que en sí misma toma un parámetro de tipo, luego aplica esa función a dos tipos diferentes .

Entonces, cuando vea una forallfirma de tipo, piense en ella como una expresión lambda para firmas de tipo . Al igual que las lambdas regulares, el alcance de se forallextiende lo más hacia la derecha posible, hasta encerrar paréntesis, y al igual que las variables unidas en un lambda regular, las variables de tipo unidas por a forallsolo están dentro del alcance dentro de la expresión cuantificada.

Post scriptum : Quizás te preguntes, 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 tipos , que podría escribir de la siguiente manera:

Either = /\a b -> ...

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

Por otro lado, una función que tipo de "patrón coincide" en sus parámetros de tipo, que devuelve diferentes valores para diferentes tipos, es un método de una clase de tipo . Una ligera expansión de 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 "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 se parece mucho a una definición de función.

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

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

Cuantificación universal

Un tipo universalmente cuantificado es un tipo de la forma forall a. f a. Un valor de ese tipo puede considerarse 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 ay le devuelve una lista de elementos del mismo tipo a. Solo hay una implementación posible, por supuesto. Tendría que darle la lista vacía porque apodrí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 dicha función proporciona tanto un tipo acomo un valor de tipo a. La implementación debe devolver un valor del mismo tipo a. Solo hay una posible implementación nuevamente. Tendría que devolver el mismo valor que se le dio.

Cuantificación existencial

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

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

OK, espera un minuto. ¿Por qué Haskell usa forallpara denotar un tipo "existencial" como el siguiente?

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

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

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

Una vez construido, puede pensar en un valor de tipo ShowBoxque consta de dos cosas. Es un tipo sjunto con un valor de tipo s. En otras palabras, es un valor de un tipo cuantificado existencialmente. ShowBoxrealmente podría escribirse como exists s. Show s => ssi Haskell apoyara esa notación.

runST y amigos

Dado eso, ¿cómo son diferentes?

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

Primero tomemos bar. Toma un tipo ay una función de tipo a -> a, y produce un valor de tipo (Char, Bool). Podríamos elegir Intcomo el ay darle una función de tipo, Int -> Intpor ejemplo. Pero fooes diferente. Requiere que la implementación de foopoder pasar cualquier tipo que desee a la función que le damos. Entonces, la única función que razonablemente podríamos darle es id.

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

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

Por lo tanto, runSTdebe ser capaz de producir un valor de tipo a, sin importar el tipo que le demos a. Para hacerlo, utiliza un argumento de tipo forall s. ST s aque ciertamente debe de alguna manera producir el a. Además, debe ser capaz de producir un valor de tipo, asin importar el tipo de implementación que runSTdecida dar s.

¿OK y eso qué? El beneficio es que esto impone una restricción a la persona runSTque llama, ya que el tipo ano puede involucrar al tipo sen 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 runSTes libre de realizar una mutación con el valor de tipo s. El tipo garantiza que esta mutación sea local para la implementación de runST.

El tipo de runSTes un ejemplo de un tipo polimórfico de rango 2 porque el tipo de su argumento contiene un forallcuantificador. El tipo de fooarriba 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 forallcuantificador. 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 ntiene rango n + 1.

¿Alguien puede explicar por completo la palabra clave para todos en un inglés claro y claro (o, si existe en algún lugar, señalar una explicación tan clara que me he perdido) que no asume que soy un matemático inmerso en la jerga?

Voy a tratar de explicar solo el significado y quizás la aplicación forallen el contexto de Haskell y sus sistemas de tipos.

Pero antes de que comprendan que me gustaría dirigirlos a una charla muy accesible y agradable de Runar Bjarnason titulada " Restricciones liberan, liberan restricciones ". 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 forall. Trataré de explicar la forallperspectiva a continuación.

                CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN

Es muy importante digerir y creer que esta declaración proceda con la siguiente explicación, por lo que le insto a que vea la charla (al menos partes de ella).

Ahora, un ejemplo muy común, que muestra 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 esa es la identityfunción o lo que se conoce más popularmente id.

En las primeras etapas 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 idsolo el que satisface la firma de tipo?

Esto se debe a que hay una implícita foralloculta en la firma de tipo. El tipo real es:

id :: forall a. a -> a

Entonces, 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 en el nivel de tipo, se convierte en una restricción en el nivel de término

Tratemos de probar la primera afirmación:

Una restricción en el nivel de tipo.

Poniendo una restricción a nuestra firma tipo

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

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

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

Lo mismo puede observarse restringiendo acon cualquier otra clase de tipo, etc.

Entonces, a qué se foo :: (Num a) => a -> atraduce este tipo de firma es:

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

Esto se conoce como cuantificación existencial, que se traduce en que existen algunos casos aen los que una función cuando se alimenta algo de tipo adevuelve 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 adebería pertenecer al conjunto de Números) libera el término nivel 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 a nivel de tipo:

foo :: forall a. a -> a

Ahora esto se traduce en:

∀a , a -> a

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

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

foo 5 = 7

porque esta implementación no satisfaría si ponemos acomo a Bool. apuede ser un Charo un [Char]o un tipo de datos personalizado. En todas las circunstancias, debería 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 identityfunción

Por foralllo tanto, es un libertynivel de tipo, cuyo propósito real es constrainel nivel de término para una implementación particular.

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 comprender esas dos cosas por separado, en lugar de tratar de obtener una explicación de por qué 'forall' es una sintaxis apropiada en ambos al mismo tiempo.

¿Cómo es existencial existencial?

Con la cuantificación existencial, foralls en las datadefiniciones significa 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é forallen datalas definiciones son isomorfo a (exists a. a)(pseudo-Haskell) se puede encontrar en "Haskell / tipos Existencialmente cuantificados" de Wikilibros .

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 coinciden / deconstruyen patrones MkT x, ¿de qué tipo son x?

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

xpuede 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 isomórficos:

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 " forallrealmente significa 'para todos'". Una distinción importante es el impacto de forallla aplicación de definición versus función .

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

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

Si lo que se está definiendo es una función polimórfica , significa que la función debe ser válida para todos los adecuados a, lo cual no es tan restrictivo porque el hecho de que la función sea polimórfica no significa que el parámetro que se aplique tenga que ser polimórfico. Es decir, si la función es válida para todos a, a la inversa, se puede aplicar cualquier función adecuada 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.a

Si a forallestá dentro del tipo de parámetro de función (es decir, a Rank2Type), significa que el parámetro aplicado debe ser verdaderamente polimórfico, para ser coherente con la idea de que la definición de forallmedios 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 mediante la implementación de la función", como lo señala Norman )

Por lo tanto, la razón por la cual las datadefiniciones existenciales permiten cualquiera a 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 cualquiera apuede aplicarse a la función. A diferencia de, digamos, un valor polimórfico :

valueT :: forall a. [a]

tipo de valor T :: a

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

[] :: [t]

Las diferencias

Aunque el significado de foralles consistente en ExistentialQuantificationy RankNType, los existenciales tienen una diferencia ya que el dataconstructor 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 tipo nuevo y distinto para cada variable de tipo existencial. Estos tipos no pueden unificarse con ningún otro tipo, ni pueden escapar del alcance de la coincidencia de patrones.