tipos - if en haskell ejemplos

Las variables de tipo de ámbito requieren foralls explícitos. ¿Por qué?

Question

Si desea utilizar las variables de tipo de ámbito léxico de GHC, también tiene que usar la cuantificación universal explícita . Es decir, debe agregar todas las declaraciones a las firmas de tipo de sus funciones:

{-# LANGUAGE ExplicitForAll, ScopedTypeVariables #-}
f :: forall a . [a] -> [a] -- The `forall` is required here ...
f (x:xs) = xs ++ [x :: a] -- ... to relate this `a` to the ones above.

¿Esto realmente tiene algo que ver con la cuantificación, o los escritores de extensión simplemente cooptaron la palabra clave forall como un marcador conveniente donde se aplica el nuevo alcance más amplio?

En otras palabras, ¿por qué no podemos dejar de lado el forall como de costumbre? ¿No estaría claro que las variables de tipo en anotaciones dentro del cuerpo de la función se refieren a variables del mismo nombre en la firma de la función? ¿O sería el tipeo de alguna manera problemático o ambiguo?

Answer 1

Sí, el cuantificador es significativo y es necesario para que los tipos tengan sentido.

En primer lugar, tenga en cuenta que no hay tal cosa como una firma de tipo "no cuantificada" en Haskell. Las firmas sin un forall están realmente cuantificadas implícitamente. Este código ...

f :: [a] -> [a] -- No `forall` here ...
f (x:xs) = xs ++ [x :: a] -- ... or here.

... realmente significa esto:

f :: forall a . [a] -> [a] -- With a `forall` here ...
f (x:xs) = xs ++ [x :: forall a . a] -- ... and another one here.

Así que vamos a averiguar lo que esto dice. Lo importante es observar que las variables de tipo llamadas a en las firmas para f y para x están unidas por cuantificadores separados . Esto significa que son variables diferentes , a pesar de compartir un nombre. Así que el código anterior es equivalente a esto:

f :: forall a . [a] -> [a]
f (x:xs) = xs ++ [x :: forall b . b] -- I''ve changed `a` to `b`

Con los nombres diferenciados, ahora está claro no solo que las variables de tipo en las firmas para f y x no están relacionadas, sino que la firma para x afirma que x puede tener cualquier tipo. Pero esto es imposible, ya que x debe tener el tipo particular vinculado a a cuando f se aplica a un argumento. Y de hecho el comprobador de tipos rechaza este código.

Por otro lado, con un solo forall en la firma para f ...

f :: forall a . [a] -> [a] -- A `forall` here ...
f (x:xs) = xs ++ [x :: a] -- ... but not here.

... la a en la firma en x está limitada por el cuantificador al principio de la firma de tipo f , por lo que a representa el mismo tipo que el tipo representado por las variables llamadas a en la firma de f .