83

I understand that the ST monad is something like a little brother of IO, which in turn is the state monad with added RealWorld magic. I can picture states and I can picture that RealWorld is somehow put into IO, but every time I write a type signature of ST the s of the ST monad confuses me.

Take, for example, ST s (STArray s a b). How does the s work there? Is it just used to build up some artificial data dependency between computations without being able to be referenced like states in the state monad (due to the forall)?

I'm just throwing out ideas and would really appreciate someone more knowledgeable than I to explain it to me.

stites
  • 4,903
  • 5
  • 32
  • 43
David
  • 8,275
  • 5
  • 26
  • 36
  • If you search for "ST monad", there's an entry that kind of answers my question as a side answer to a question about STArrays. Not sure if my question here's a duplicate now. http://stackoverflow.com/questions/8197032/starray-documentation-for-newbies-and-state-st-related-questions – David Sep 18 '12 at 00:00
  • 2
    It's so tempting to simply answer "Yes." to your question. :) – AndrewC Sep 18 '12 at 00:30
  • I guess adding a link to the question and closing it would a) make searching for this easier in the future, and b) save some answerers some time. – David Sep 18 '12 at 00:33
  • 2
    I'll point you to [my writeup on rank-2 types](http://stackoverflow.com/questions/12031878/what-is-the-purpose-of-rank2types/12033549#12033549), which should help you understand the `ST` monad as well. Once you understand how rank-2 types can control "who chooses" the type used for a type variable, that should help you understand how `ST` operations use rank-2 to prevent its computations from being used illicitly. – Luis Casillas Sep 18 '12 at 00:58
  • You can write `a :: ST Int Int; a = return 2` `ST` is a perfectly ordinary state monad, except it uses an unboxed pair as output of the state function `State# s -> (# State# s, a #)` which makes it impractical to deal with. The mystery is entirely in `runST` which has a rank 2 type, though ST itself isnt one. – applicative Sep 27 '12 at 02:27

3 Answers3

80

The s keeps objects inside the ST monad from leaking to the outside of the ST monad.

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

Okay, this is a type error (which is a good thing! we don't want STRef to leak outside the original computation!). It's a type error because of the extra s. Remember that runST has the signature:

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

This means that the s on the computation that you're running has to have no constraints on it. So when you try to evaluate a:

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

The result would have type STRef s Int, which is wrong since the s has "escaped" outside of the forall in runST. Type variables always have to appear on the inside of a forall, and Haskell allows implicit forall quantifiers everywhere. There's simply no rule that allows you to to meaningfully figure out the return type of a.

Another example with forall: To clearly show why you can't allow things to escape a forall, here is a simpler example:

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

Of course f id is an error, since it would return either a list of Char or a list of Int depending on whether the boolean is true or false. It's simply wrong, just like the example with ST.

On the other hand, if you didn't have the s type parameter then everything would type check just fine, even though the code is obviously pretty bogus.

How ST actually works: Implementation-wise, 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 this safely is because of the type signature of all ST-related functions, especially the part with the forall.

Dietrich Epp
  • 205,541
  • 37
  • 345
  • 415
  • Could you "break" the safety of ST by using `realWorld#` directly in client code, to mimic `runSTRep` ? It's a bad idea of course, but I'm wondering what the protections are, besides `realworld#` being an obviously unsafe value to use in a program. http://hackage.haskell.org/package/base-4.6.0.1/docs/src/GHC-ST.html#runST – misterbee Jan 08 '14 at 15:03
  • @misterbee [Yep](https://hackage.haskell.org/package/base-4.8.1.0/docs/Control-Monad-ST.html#v:stToIO), and it not even necessarily unsafe. Remember, `s` only exists at the type level. – PyRulez Nov 25 '15 at 20:06
28

The s is just a hack that makes the type system stop you doing things which would be unsafe. It doesn't "do" anything at run-time; it just makes the type checker reject programs that do dubious things. (It is a so-called phantom type, a thing with only exists in the type checker's head, and doesn't affect anything at run-time.)

MathematicalOrchid
  • 61,854
  • 19
  • 123
  • 220
0

Take, for example, ST s (STArray s a b): how does the s work there?

Time for a GHCi session:

GHCi, version 8.4.3: http://www.haskell.org/ghc/  :? for help
Prelude> let _ = (\x -> x^4) 5 in x

<interactive>:2:27: error: Variable not in scope: x
Prelude>

The scope (or frame of reference) for the local variable x is the lambda/anonymous function \x -> x^4 - outside that scope, x is otherwise undefined, hence the error.

The type for runST:

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

works in similar fashion: the scope of the locally-quantified type-variable s is the type ST s a (the type of runST's parameter) - if s appears in the type of the result, it too is outside its scope and also lacks a sensible definition, causing a type-error.

So if you:

  • have an action m :: ST s (STArray s a b)

  • and you inadvertently try to extract the mutable array from m:

      … (let arr = runST m in …) …

...the escape of s outside its scope:

forall s . ST s (STArray s a)

(and its detection by the type system) stops the sharing of mutable state, a well-known source of elusive errors, particularly in the context of parallelism and concurrency.

atravers
  • 455
  • 4
  • 8
  • So you mean that because runST extracts a from a ST s a and it happens that this a has an s in it (a is a STRef s a' ) it is why the compiler complains? Every where it is written that it's the rank2 polymorphism of runST which forbids to extract the a from a ST s a. – user3680029 Aug 08 '21 at 16:12
  • Not `runST`: it's the [extended] Haskell type system which detects the escape of the locally-quantified type-variable `s`, resulting in the error message. – atravers Aug 09 '21 at 00:03
  • The rankN explanation is more clear for me even if still very abstract... runST has to have the freedom to choose s but then it's given a locked representation and the compiler starts yelling this is my understanding of the ST. – user3680029 Aug 09 '21 at 21:40
  • Alright, try this: make up a mock `ST` module using `runST = undefined`, `newSTRef = undefined`, `readSTRef = undefined` (with the appropriate type declarations and signatures), then try sneaking a `STRef` out of (or into) a `runST` call... – atravers Aug 10 '21 at 13:01
  • probably your reasoning is similar to the one of the rankN one - I just don't saw this every explanation is going in the rank2 polymorphism, for instance I understand rank2 in situation when you give o polymorphic function and the implementation is able to choose/adapt the type but have problem to understand why it's restictring the function domain (for ex. @dfeuer response in https://stackoverflow.com/questions/12031878/what-is-the-purpose-of-rank2types/24717685?noredirect=1#comment121399355_24717685) – user3680029 Aug 13 '21 at 11:54
  • I agree with that suggestion by dfeuer: write up a new question which precisely describes what you would like to know or understand (alternately, what it is about higher-rank types that you're not sure about - provide examples.) – atravers Aug 13 '21 at 14:11