Haskell rango dos polimorfismo error de compilación

Question

Dadas las siguientes definiciones:

import Control.Monad.ST 
import Data.STRef 

fourty_two = do 
    x <- newSTRef (42::Int) 
    readSTRef x 

Los siguiente se compila bajo GHC:

main = (print . runST) fourty_two -- (1) 

pero esto no significa:

main = (print . runST) $ fourty_two -- (2) 

Pero entonces como bdonlan señala en un comentario, esto compila:

main = ((print . runST) $) fourty_two -- (3) 

Pero, esto no compila

main = (($) (print . runST)) fourty_two -- (4) 

lo que parece indicar que (3) sólo se compila debido al tratamiento especial de infija $, sin embargo, todavía no explica por qué (1) compila

Preguntas:

1) He leído las siguientes dos preguntas (first, second), y he hecho creer $ solamente puede representarse con tipos monomorfas. Pero supondría de manera similar que . solo se puede instanciar con tipos monomórficos y, como resultado, fallaría de manera similar. ¿Por qué el primer código tiene éxito pero el segundo código no? (por ejemplo, ¿existe una regla especial GHC para el primer caso que no se puede aplicar en el segundo?)

2) ¿Hay una extensión GHC actual que compila el segundo código? (Quizás ImpredicativePolymorphism hizo esto en algún momento, pero parece obsoleta, tiene todo lo reemplazó?)

3) ¿Hay alguna manera de definir decir `my_dollar` el uso de extensiones de GHC para hacer lo $ hace, sino que también es capaz de manejar polimórfica tipos, entonces (print . runST) `my_dollar` fourty_two compila?

Editar: Respuesta propuesta:

Además, la siguiente falla al compilar:

main = ((.) print runST) fourty_two -- (5) 

Esto es lo mismo que (1), excepto que no se utiliza la versión infija de ..

Como resultado, parece que GHC tiene reglas especiales para $ y ., pero solo sus versiones de infijo.

Answer 1

1. No estoy seguro de entender por qué el segundo no funciona. Podemos ver el tipo de print . runST y observar que es suficientemente polimórfico, por lo que la culpa no se encuentra en (.). Sospecho que la regla especial que GHC tiene para infix ($) simplemente no es suficiente. SPJ y sus amigos pueden estar dispuestos a volver a examinarlo si propone este fragmento como un error en su rastreador.

   En cuanto a por qué funciona el tercer ejemplo, bueno, eso es porque de nuevo el tipo de ((print . runST) $) es suficientemente polimórfico; de hecho, es igual al tipo de print . runST.

2. Nada ha reemplazado a ImpredicativePolymorphism, porque la gente de GHC no ha visto ningún caso de uso en el que la conveniencia del programador adicional fuera mayor que el potencial adicional para los errores del compilador. (No creo que verían esto como convincente, tampoco, aunque por supuesto que no soy la autoridad.)

3. podemos definir un poco menos polimórficos ($$):

   {-# LANGUAGE RankNTypes #-} 
   infixl 0 $$ 
   ($$) :: ((forall s. f s a) -> b) -> ((forall s. f s a) -> b) 
   f $$ x = f x 
   

   Luego, su ejemplo typechecks bien con este nuevo operador:

   *Main> (print . runST) $$ fourty_two 
   42 
   

Answer 2

No puedo decir con demasiada autoridad sobre este tema, pero aquí es lo que creo que puede estar ocurriendo:

Considere lo que el typechecker tiene que hacer en cada uno de estos casos. (print . runST) tiene tipo Show b => (forall s. ST s t) -> IO(). fourty_two tiene tipo ST x Int.

El forall aquí es un calificador de tipo existencial - aquí, significa que el argumento pasado en tiene que ser universal, en s.Es decir, debe pasar en un tipo polimórfico que admite cualquier valor para s en absoluto. Si no indica explícitamente forall, Haskell lo coloca en el nivel más externo de la definición de tipo. Esto significa que fourty_two :: forall x. ST x Int y (print . runST) :: forall t. Show t => (forall s. ST s t) -> IO()

Ahora, podemos coincidir con forall x. ST x Intforall s. ST s t dejando t = Int, x = s. Entonces el caso de llamada directa funciona. ¿Qué ocurre si usamos $?

tiene ($) :: forall a b. (a -> b) -> a -> b. Cuando resolver a y b, ya que el tipo de $ no tiene ningún tipo de alcance explícita de esta manera, el argumento de xfourty_two se levantó a cabo con el alcance más externa en el tipo de ($) - por lo ($) :: forall x t. (a = forall s. ST s t -> b = IO()) -> (a = ST x t) -> IO(). En este punto, intenta hacer coincidir a y b, y falla.

Si en su lugar escribe ((print . runST) $) fourty_two, el compilador primero resuelve el tipo de ((print . runST $). Resuelve el tipo de ($) para ser forall t. (a = forall s. ST s t -> b = IO()) -> a -> b; tenga en cuenta que dado que la segunda ocurrencia de a no está restringida, ¡no tenemos esa variable de tipo molesto que se escapa al alcance más externo! Y así la coincidencia tiene éxito, la función se aplica parcialmente, y el tipo general de la expresión es forall t. (forall s. ST s t) -> IO(), que está justo donde comenzamos, y por lo tanto tiene éxito.