Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Is ST referentialy transparent?

Tags:

haskell

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
like image 459
sevo Avatar asked Dec 11 '22 09:12

sevo


1 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

like image 110
Joachim Breitner Avatar answered Dec 27 '22 17:12

Joachim Breitner