runST y la función composición

¿Por qué este typecheck:runST y la función composición

runST $ return $ True

Aunque la siguiente no:

runST . return $ True

GHCi se queja:

Couldn't match expected type `forall s. ST s c0' 
      with actual type `m0 a0' 
Expected type: a0 -> forall s. ST s c0 
    Actual type: a0 -> m0 a0 
In the second argument of `(.)', namely `return' 
In the expression: runST . return

Fuente

2012-02-27 Grzegorz Chrupała

If '($)' podría recibir una firma de tipo depedently como '($): forall (a: *) (b: a -> *). ((x: a) -> b x) -> (x: a) -> b x' funcionaría sin trucos de GHC, y de manera similar para '(.)'. – danr

La respuesta corta es que la inferencia de tipo no siempre funciona con tipos de rango superior. En este caso, no es capaz de inferir el tipo de (.), pero el tipo comprueba si añadimos un tipo de anotación explícita:

> :m + Control.Monad.ST 
> :set -XRankNTypes 
> :t (((.) :: ((forall s0. ST s0 a) -> a) -> (a -> forall s1. ST s1 a) -> a -> a) runST return) $ True 
(((.) :: ((forall s0. ST s0 a) -> a) -> (a -> forall s1. ST s1 a) -> a -> a) runST return) $ True :: Bool

El mismo problema ocurre con el primer ejemplo, si sustituimos ($) con nuestra propia versión:

> let app f x = f x 
> :t runST `app` (return `app` True) 
<interactive>:1:14: 
    Couldn't match expected type `forall s. ST s t0' 
       with actual type `m0 t10' 
    Expected type: t10 -> forall s. ST s t0 
     Actual type: t10 -> m0 t10 
    In the first argument of `app', namely `return' 
    In the second argument of `app', namely `(return `app` True)'

una vez más, esto puede ser resuelto mediante la adición de anotaciones de tipo:

> :t (app :: ((forall s0. ST s0 a) -> a) -> (forall s1. ST s1 a) -> a) runST (return `app` True) 
(app :: ((forall s0. ST s0 a) -> a) -> (forall s1. ST s1 a) -> a) runST (return `app` True) :: Bool

Lo que ocurre aquí es que no hay una regla de tipado especial en GHC 7 que solo se aplica al operador estándar ($). Simon Peyton-Jones explica este comportamiento en a reply on the GHC users mailing list:

Este es un ejemplo motivador para la inferencia tipo que puede hacer frente a tipos impredicativas. Considere el tipo de ($):
($) :: forall p q. (p -> q) -> p -> q 
En el ejemplo que necesitamos para crear una instancia p con (forall s. ST s a), y eso es lo que significa polimorfismo impredicativo: crear instancias de una variable de tipo con un tipo polimórfico .

Tristemente, no conozco ningún sistema de complejidad razonable que pueda tipear [this] sin ayuda. Hay muchos sistemas complicados, y tengo sido coautor de trabajos en al menos dos, pero todos son demasiado Jolly Complicated para vivir en GHC. Tuvimos una implementación de boxy types, pero la saqué cuando implementé el nuevo typechecker. Nadie lo entendió.

Sin embargo, la gente tan a menudo escriben
runST $ do ... 
que en GHC 7 He implementado una regla de escribir especial, sólo para usos infijas de ($). Solo piense en (f $ x) como una nueva forma sintáctica , con la obvia regla de tipeo, y listo.

Su segundo ejemplo falla porque no existe tal regla para (.).

Fuente

2012-02-27 18:09:23 hammar

Gracias, está empezando a tener sentido ahora. –

El patrón runST $ do { ... } es tan común, y el hecho de que normalmente no haría check-type es tan molesto, que GHC incluyó algunos ST hacks de comprobación de tipos específicos para que funcione. Esos ataques probablemente están disparando aquí para la versión ($), pero no para la versión (.).

Fuente

2012-02-27 17:57:13

Punto de interés. Probablemente sea suficiente simplemente soltar el ($) tan pronto como se vea que se aplica a 2 argumentos. Debe ser fácilmente verificable reemplazándolo con una función personalizada que haga lo mismo que ($), y observe si el verificador de tipos se quejaría entonces. – Ingo

@Ingo: Sí, '' 'deje que la aplicación f x = f x en la aplicación runST' (return 'app' True)' '' no escriba check. Interesante. – hammar

@Hammar: Esto significa que aparentemente GHC pierde $, a pesar de que esto no es del todo correcto con tipos de rango más altos. – Ingo

Los mensajes son un poco confuso el punto (o eso siento). Permítanme volver a escribir el código:

runST (return True) -- return True is ST s Bool 
(runST . return) True -- cannot work

Otra forma de decir esto es que el monomorfa m0 a0 (el resultado de vuelta, si obtendría un a0) no puede ser unificado con (forall s.ST s a).

Fuente

2012-02-27 18:02:31 Ingo

No comprueba type: 'unsafePerformIO. return $ True' –

@Ingo: está analizando incorrectamente los dos ejemplos. 'runST $ return $ True' es' ($) runST (($) return True) ', y' runST. return $ True' es '($) ((.) runST return) True'. Harían lo mismo en ausencia de tipos de rango 2. – ehird

@ehird - Tienes razón, olvidé el punto. (Oye, eso rima ...) – Ingo

Respuesta

Cuestiones relacionadas