runST et composition des fonctions

Question

Pourquoi cette vérification de type :

runST $ return $ True

Ce qui n'est pas le cas de ce qui suit :

runST . return $ True

Le GHCI se plaint :

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

La réponse courte est que l'inférence de type ne fonctionne pas toujours avec les types de rang supérieur. Dans ce cas, il est impossible de déduire le type de (.) mais il vérifie le type si nous ajoutons une annotation de type explicite :

> :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

Le même problème se pose avec votre premier exemple, si nous remplaçons ($) avec notre propre version :

> 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)'

Là encore, ce problème peut être résolu en ajoutant des annotations de type :

> :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

Ce qui se passe ici, c'est qu'il existe une règle de typage spéciale dans GHC 7 qui ne s'applique qu'à la norme ($) opérateur. Simon Peyton-Jones explique ce comportement dans une réponse sur la liste de diffusion des utilisateurs de GHC :

Il s'agit d'un exemple motivant f types imprédicatifs. Considérons le type de ($) :

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

Dans l'exemple, nous avons besoin d'instancier p con (forall s. ST s a) , polymorphisme imprédicatif : instancier une variable de type avec un type polymorphe. type polymorphe.

Malheureusement, je ne connais pas de système d'une complexité raisonnable capable de vérifier les caractères suivants [ceci] sans aide. Il existe de nombreux systèmes compliqués, et j'ai été co-auteur d'articles sur au moins deux d'entre eux, mais ils sont tous trop compliqués. co-auteur d'articles sur au moins deux d'entre eux, mais ils sont tous trop Jolly Complicated pour vivre dans GHC. Nous avions une implémentation de mais je l'ai supprimée lors de l'implémentation du nouveau vérificateur de caractères. Personne ne l'a compris.

Pourtant, on écrit si souvent

runST $ do ... 

que dans GHC 7, j'ai mis en place une règle de typage spéciale, uniquement pour les utilisations infixes de ($) . Il suffit de penser à (f $ x) comme une nouvelle forme syntaxique syntaxique, avec la règle de typage évidente, et le tour est joué.

Votre deuxième exemple échoue parce qu'il n'y a pas de règle de ce type pour (.) .

Answer 2

Le runST $ do { ... } est si courant, et le fait qu'il n'y ait normalement pas de vérification de type est si ennuyeux, que GHC a inclus un certain nombre de ST -pour le faire fonctionner. Ces bidouillages sont probablement en train de tirer ici pour le ($) mais pas la version (.) version.

Answer 3

Les messages sont un peu confus (c'est du moins ce que je pense). Laissez-moi réécrire votre code :

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

Une autre façon de l'exprimer est de dire que le monomorphe m0 a0 (le résultat du retour, s'il obtenait un a0) ne peut pas être unifié avec (forall s.ST s a).