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
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
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With