Comment fonctionne la monade ST?

Question

Je comprends que le ST monade est quelque chose comme un petit frère de IO, qui à son tour est l'état de monade avec ajout de RealWorld de la magie. Je peux imaginer les états, je ne peux imaginer que RealWorld est somoehow mis en IO, mais à chaque fois que j'écris un type de signature, l' s de la ST monade me confond, par exemple, ST s (STArray s a b). Comment l' s y travaillent? Est-il juste utilisé pour construire certains artificielle de la dépendance de données entre les calculs, sans en être réellement referrable (comme les états dans l'état de monade par exemple) en raison de l' forall?

Je suis juste jeter des choses, et apprécierais vraiment quelqu'un de plus compétent-il m'expliquer mieux.

Answer 1

L' s conserve les objets à l'intérieur de l' ST monade de fuite à l'extérieur de l' ST monade.

-- This is an error... but let's pretend for a moment...
let a = runST $ newSTRef (15 :: Int)
    b = runST $ writeSTRef a 20
    c = runST $ readSTRef a
in b `seq` c

Bon d'accord, c'est un type d'erreur (ce qui est une bonne chose! nous ne voulons pas d' STRef de fuite en dehors de l'original calcul!). C'est un type d'erreur en raison de la plus - s. Rappelez-vous que runST a la signature:

runST :: (forall s . ST s a) -> a

Cela signifie que l' s sur le calcul de ce que vous êtes en cours d'exécution a ne pas avoir de contraintes sur elle. Ainsi, lorsque vous essayez d'évaluer a:

a = runST (newSTRef (15 :: Int) :: forall s. ST s (STRef s Int))

Le résultat aurait de type STRef s Int, ce qui est faux puisque l' s a "échappé" à l'extérieur de l' forall en runST. Les variables de Type toujours figurer à l'intérieur d'un forall, et Haskell permet implicite forall quantificateurs partout. Il n'y a aucune règle qui permet de mieux comprendre le type de retour d' a.

Un autre exemple, forall: Pour montrer clairement pourquoi vous ne pouvez pas laisser les choses pour échapper à un forall, voici un exemple plus simple:

f :: (forall a. [a] -> b) -> Bool -> b
f g flag =
  if flag
  then g "abcd"
  else g [1,2]

> :t f length
f length :: Bool -> Int

> :t f id
-- error --

Bien sûr, f id est une erreur, car il serait de retour, soit une liste d' Char ou une liste d' Int selon que le booléen est vrai ou faux. C'est tout simplement une erreur, tout comme l'exemple avec ST.

D'autre part, si vous n'avez pas l' s type de paramètre puis tout contrôle de type tout à fait correcte, même si le code est évidemment assez bidon.

Comment ST fonctionne réellement: mise en Œuvre-sage, l' ST monade est en fait le même que l' IO monade, mais avec un peu différente de l'interface. Lorsque vous utilisez l' ST monade, vous obtenez réellement unsafePerformIO ou l'équivalent, en coulisses. La raison, vous pouvez le faire en toute sécurité en raison du type de la signature de tous ST-fonctions connexes, surtout la partie avec l' forall.

Answer 2

Le s est juste un hack qui fait que le système de typage vous empêche de faire des choses qui seraient dangereuses. Cela ne "fait" rien au moment de l'exécution; cela fait simplement que le vérificateur de types rejette les programmes qui font des choses douteuses. (Il s’agit d’un type dit fantôme , une chose n’existant que dans la tête du vérificateur de types et n’affectant en rien au moment de l’exécution.)