Is ST referentialy transparent?

user_3858142 0
Viewed 177

Why is ST designed to disallow the following code as shown in the wikibook? The article seems to suggest that ST effects would leak into another ST if this was allowed, but I don't really understand why.

It seems that I cannot run a specific ST s (STRef s a). Are ST effects contained and referentially transparent, but such use is still considered invalid?

Intuition tells me that there is difference between semantics of IO and ST related to that there is one IO and many independent ST, but I'm not sure.

> runST (newSTRef True)

<interactive>:5:8: error:
    • Couldn't match type ‘a’ with ‘STRef s Bool’
        because type variable ‘s’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a type expected by the context:
          forall s. ST s a
        at <interactive>:5:1-21
      Expected type: ST s a
        Actual type: ST s (STRef s Bool)
    • In the first argument of ‘runST’, namely ‘(newSTRef True)’
      In the expression: runST (newSTRef True)
      In an equation for ‘it’: it = runST (newSTRef True)
    • Relevant bindings include it :: a (bound at <interactive>:5:1)

> :t newSTRef
newSTRef :: a -> ST s (STRef s a)

> :t runST
runST :: (forall s. ST s a) -> a
haskell
2 Answers

More an answer to the question title than the question itself, but still:

Yes, ST is referentially transparent.

For a long time this was just conjectured and believed, and only this year we have a proper proof for that:

A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal
Conditionally accepted to POPL 2018
http://iris-project.org/ Preprint PDF

user_9462260

I don't really understand what you're asking, so I'm going to pretend your question is:

Why is ST designed to disallow runST (newSTRef True)?

If that were allowed, it would no longer be referentially transparent:

main = do
    let r = runST (newSTRef True)
    evaluate (runST (writeSTRef r False))
    print (runST (readSTRef r))

This code would output False.

main = do
    evaluate (runST (writeSTRef (runST (newSTRef True)) False))
    print (runST (readSTRef (runST (newSTRef True))))

This code (the result of inlining r in every user) would output True, because each instance of runST (newSTRef True) would allocate a new STRef variable.

The way runST is actually implemented ensures that all resources allocated within an ST s action cannot escape that action.

The difference between IO and ST s is that there is no runIO function. You can create multiple independent IO actions, but they don't matter without runIO (they're just values). The only way to actually run an IO action is to bind it to main and let the runtime system pick it up (it's like there's a single implicit runIO wrapped around main), so there's only one single IO action that will ever get executed in a program.

Of course this single action can be composed by combining multiple smaller actions, but in the end it's still a monolith. On the other hand, runST allows multiple ST s actions to be executed independently.

user_18486540
Related