How does the ST monad work?

Question

I understand that the ST monad is like the younger brother of IO, which, in turn, is the state monad with the added magic of RealWorld . I can imagine the state, and I can imagine that RealWorld somehow fits in IO, but every time I write a signature like ST , s ST monad confuses me.

Take for example ST s (STArray sab) . How does s work? Is it just used to create some kind of artificial data dependency between computations, not being able to refer as states in the state monad (due to forall )?

I just throw away ideas and really appreciate someone more knowledgeable than me to explain it to me.

Answer 1

s stores objects inside the ST monad from leakage outside the ST monad.

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

Well, this is a type error (that's good, we don’t want STRef leak out of the original calculations!). This is a type error due to extra s . Remember that runST has a signature:

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

This means that in s there should be no restrictions on the calculation you performed. Therefore, when you try to evaluate a :

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

The result will be of type STRef s Int , which is incorrect, since s "escaped" outside of forall in runST . Type variables should always appear inside forall , and Haskell allows implicit forall quantifiers everywhere. There simply is no rule to significantly interpret the return type of a .

Another example with forall : To clearly show why you cannot let things escape forall , here is a simpler example:

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

Of course, f id is an error, as it will return either a Char list or an Int list, depending on whether the boolean value is true or false. This is simply wrong, as in the example with ST .

On the other hand, if you did not have a parameter of type s , then everything will gain verification just fine, although the code is clearly quite fictitious.

How ST works: Implementation, the ST monad is actually the same as the IO monad, but with a slightly different interface. When you use the ST monad, you actually get unsafePerformIO or the equivalent behind the scenes. The reason you can do it safely is a signature like all ST related functions, especially the part with forall .

Answer 2

s is just a hack that forces a system like that to stop you from doing insecure things. It does not do anything at runtime; it just makes type checking reject programs that do dubious things. (This is the so-called phantom type, a thing that exists only in the type checking head and does not affect anything at runtime.)