haskell - ¿Qué están haciendo estos "forallos" explícitos?

higher-rank-types

Question

¿Cuál es el propósito de los forall s en este código?

class Monad m where
(>>=) :: forall a b. m a -> (a -> m b) -> m b
(>>) :: forall a b. m a -> m b -> m b
-- Explicit for-alls so that we know what order to
-- give type arguments when desugaring

(Algún código omitido). Esto es del código para Monads .

Mis antecedentes: no entiendo realmente para todos o cuando Haskell los tiene implícitamente.

Además, y puede que no sea significativo, pero GHCi me permite omitir el forall cuando doy >> un tipo:

Prelude> :t (>>) :: Monad m => m a -> m b -> m b
(>>) :: Monad m => m a -> m b -> m b
:: (Monad m) => m a -> m b -> m b

(No hay error).

Answer 1

Mis antecedentes: no entiendo realmente para todos o cuando Haskell los tiene implícitamente.

De acuerdo, considere el tipo de id , a -> a . ¿Qué significa a medio y de dónde viene? Cuando define un valor, no puede usar variables arbitrarias que no estén definidas en ningún lugar. Necesita una definición de nivel superior, un argumento de función o una cláusula where , & c. En general, si usa una variable, debe estar vinculada en algún lugar.

Lo mismo ocurre con las variables de tipo, y forall es una de esas formas para vincular una variable de tipo. En cualquier lugar que vea una variable de tipo que no esté vinculada explícitamente (por ejemplo, la class Foo a where ... enlaza dentro de la definición de la clase), está vinculada implícitamente por un forall .

Por lo tanto, el tipo de id es implícitamente para todos forall a. a -> a forall a. a -> a . ¿Qué significa esto? Más o menos lo que dice. Podemos obtener un tipo a -> a para todos los tipos posibles a , o desde otra perspectiva, si selecciona cualquier tipo específico, puede obtener un tipo que represente "funciones de su tipo elegido a sí mismo". El último fraseo debe sonar un poco como definir una función, y como tal, se puede pensar que para todos es similar a una abstracción de lambda para los tipos.

GHC usa varias representaciones intermedias durante la compilación, y una de las transformaciones que aplica es hacer que la similitud con las funciones sea más directa: se hacen explícitas todas las implícitas, y en cualquier lugar que se use un valor polimórfico para un tipo específico, primero se aplica a un tipo argumento

Incluso podemos escribir forall s y lambdas como una expresión. Abusaré de la notación por un momento y la reemplazaré forall a. con //a => para la consistencia visual. En este estilo, podemos definir id = //a => /(x::a) -> (x::a) o algo similar. Entonces, una expresión como id True en tu código terminaría traducida a algo como id Bool True lugar; solo id True ya no tendría sentido.

Al igual que puede reordenar los argumentos de la función, también puede reordenar los argumentos de tipo, sujeto solo a la restricción (bastante obvia) de que los argumentos de tipo deben ir antes que los argumentos de valor de ese tipo. Dado que los elementos implícitos son siempre la capa más externa, GHC podría elegir el orden que desee al hacerlos explícitos. En circunstancias normales, esto obviamente no importa.

No estoy seguro de lo que está sucediendo exactamente en este caso, pero en base a los comentarios, supongo que la conversión al uso de argumentos de tipo explícito y la falta de observación de la notación de tareas do son, en cierto sentido, conscientes unos de otros, y por lo tanto, El orden de los argumentos de tipo se especifica explícitamente para asegurar la consistencia. Después de todo, si algo está aplicando ciegamente dos argumentos de tipo a una expresión, importa mucho si el tipo de esa expresión es para todos forall a b. ma -> mb -> mb forall a b. ma -> mb -> mb o forall b a. ma -> mb -> mb forall b a. ma -> mb -> mb !