simbolos - ¿Qué hace la palabra clave `forall` en Haskell/GHC?




listas en haskell (6)

¿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:

  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 , foo y bar arriba).
  2. 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).
  3. 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

y

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.


¿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 .


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 .





forall