¿Por qué no se aplica forall (uso de RankNTypes) por defecto?

Question

no estoy tan familiarizado con forall, pero recientemente leer esta pregunta: What does the `forall` keyword in Haskell/GHC do?

En una de las respuestas es este ejemplo:

{-# LANGUAGE RankNTypes #-} 
liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b) 
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v) 

La explicación es buena y entiendo lo forall está haciendo aquí. Pero me pregunto, ¿hay alguna razón en particular por la cual este no sea el comportamiento predeterminado? ¿Hay alguna vez en que sería desventajoso?

Editar: Quiero decir, ¿hay alguna razón por la cual no se pueda insertar el forall por defecto?

Answer 1

Bueno, no es parte del estándar Haskell 2010, por lo que no está activado por defecto, y se ofrece como una extensión de idioma. En cuanto a por qué no está en el estándar, los tipos de rango-n son bastante más difíciles de implementar que los tipos normales de rango 1 que tiene Haskell; tampoco son necesarios con tanta frecuencia, por lo que el Comité probablemente decidió no molestarse con ellos por razones de simplicidad de lenguaje e implementación.

Por supuesto, eso no significa que los tipos rank-n no sean útiles; lo son, mucho, y sin ellos no tendríamos herramientas valiosas como el ST monad (que ofrece un estado mutable local eficiente, como IO, donde todo lo que puede hacer es usar IORef s). Pero agregan bastante complejidad al lenguaje y pueden causar un comportamiento extraño al aplicar transformaciones de código aparentemente benignas. Por ejemplo, algunos verificadores de tipo rank-n permitirán runST (do { ... }) pero rechazan runST $ do { ... }, aunque las dos expresiones son siempre equivalentes sin los tipos rank-n. Consulte this SO question para ver un ejemplo del comportamiento inesperado (ya veces molesto) que puede causar.

Si, como sepp2k pregunta, que está en lugar de preguntar por qué forall tiene que ser añadido de forma explícita al tipo de firmas para conseguir el aumento de la generalidad, el problema es que (forall x. x -> f x) -> (a, b) -> (f a, f b) es en realidad un tipo más restrictivo que (x -> f x) -> (a, b) -> (f a, f b). Con este último, puede pasar cualquier función del formulario x -> f x (para cualquier f y x), pero con el primero, la función que pasa debe funcionar para todox. Entonces, por ejemplo, una función de tipo String -> IO String sería un argumento permisible para la segunda función, pero no la primera; debería tener el tipo a -> IO a en su lugar. ¡Sería bastante confuso si este último se transformara automáticamente en el primero! Son dos tipos muy diferentes.

Podría tener más sentido con los implícitos forall s explicitados:

forall f x a b. (x -> f x)   -> (a, b) -> (f a, f b) 
forall f a b. (forall x. x -> f x) -> (a, b) -> (f a, f b) 

Answer 2

sospecho que los tipos de mayor rango no están habilitadas por defecto porque they make type inference undecidable. Esta es también la razón por la que, incluso con la extensión habilitada, necesita usar la palabra clave forall para obtener un tipo de rango superior: GHC supone que todos los tipos son de rango 1 a menos que se indique explícitamente lo contrario para deducir la mayor cantidad de información de tipo posible.

Dicho de otra manera, no hay una manera general de inferir un tipo de rango superior (forall x. x -> f x) -> (a,b) -> (f a, f b), por lo que la única forma de obtener ese tipo es mediante una firma de tipo explícita.

Editar: según los comentarios de Vitus anteriores, la inferencia de tipo rango 2 es decidible, pero el polimorfismo de rango superior no lo es. Entonces, esta firma de tipo es técnicamente inferible (aunque el algoritmo es más complejo).Si la complejidad extra de permitir la inferencia de tipo polimórfico de rango 2 vale la pena es discutible ...