haskell - trigonometricas - runST y composición de funciones

funciones compuestas

Question

¿Por qué este typecheck:

runST $ return $ True

Mientras que lo 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

Answer 1

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

Answer 2

La respuesta corta es que la inferencia de tipo no siempre funciona con tipos de rango superior. En este caso, no puede inferir el tipo de (.) , Pero el tipo verifica si agregamos una anotación de tipo explícito:

> :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 también ocurre con su primer ejemplo, si reemplazamos ($) 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)''

De nuevo, esto se puede resolver agregando 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 está sucediendo aquí es que hay una regla de tipeo especial en GHC 7 que solo se aplica al operador estándar ($) . Simon Peyton-Jones explica este comportamiento en una respuesta en la lista de correo de los usuarios de GHC :

Este es un ejemplo motivador para la inferencia de tipos que puede tratar con tipos impredicativos. Considere el tipo de ($) :

($) :: forall p q. (p -> q) -> p -> q

En el ejemplo, necesitamos instanciar p con (forall s. ST sa) , y eso es lo que polimorfismo impredicativo significa: instanciar una variable de tipo con un tipo polimórfico.

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

Sin embargo, la gente tan a menudo escribe

runST $ do ...

que en GHC 7 implementé una regla de tipeo especial, solo para usos infrecuentes de ($) . Solo piense en (f $ x) como una nueva forma sintáctica, con la regla de tipado obvia, y listo.

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

Answer 3

Los mensajes son un poco confusos (o eso siento). Déjame reescribir tu código:

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

Otra forma de decir esto es que el monomórfico m0 a0 (el resultado del retorno, si se obtiene un a0) no se puede unificar con (forall s.ST sa).