13

The ST monad, originally devised by Launchbury and Peyton Jones, allows Haskell programmers to write imperative code (with mutable variables, arrays, etc.) while obtaining a pure interface to that code.

More concretely, the polymorphic type of the entry point function

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

ensures that all side-effects of the ST computation is contained, and the resulting value is pure.

Has this ever been rigorously (or even formally) proven?

Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139
  • Rigorously proven – in what framework? _All_ types in Haskell contain only pure values, so proving this property is a bit like proving that a given natural number, defined in some way, is not negative. – leftaroundabout Apr 23 '17 at 19:55
  • 4
    This paper claims that it hasn't: `none of the papers we came across in our literature study actually establishes the safety of the ST monad in Haskell` http://people.seas.harvard.edu/~pbuiras/publications/KeyMonadHaskell2016.pdf – danidiaz Apr 23 '17 at 20:00
  • @leftaroundabout: I believe the issue is proving that an STRef can never escape from its runST prison. – Paul Johnson Apr 23 '17 at 20:07
  • 2
    @PaulJohnson That's delicate indeed. Since it _can_ escape, if wrapped in an existential or `Dynamic`. But in such case, even if it can be fed to `readSTRef, writeSTRef`, the resulting action is still existentially quantified, hence can not be passed to `runST`. Proving all of this formally apparently is not trivial. – chi Apr 23 '17 at 20:35
  • Great reference, @danidiaz; that probably constitutes a valid answer. – Joachim Breitner Apr 23 '17 at 20:46
  • I noticed that I did not clarify what I mean with “pure”, and now I notice that there does not seem to exist a standard formal definition of pureness, let alone a proof that Haskell or Core is pure… What a rabbit hole. – Joachim Breitner Apr 24 '17 at 02:36
  • 1
    Amr Sabry argues in [What is a Purely Functional Language](https://doi.org/10.1017/S0956796897002943), that *lazy* `ST` isn't pure according to the definition of purity Sabry provides. To answer your question, the first thing you'd need to do is actually define "pure". Sabry provides arguments why the typical "definitions" are, perhaps, inadequate and proposes an alternative. – Derek Elkins left SE Apr 24 '17 at 03:22
  • @DerekElkins, theoretical concerns aside, lazy ST had a major concurrency bug (fixed in 8.2) that made it really impure in multi-threaded programs. – dfeuer Apr 24 '17 at 18:18

2 Answers2

15

Here is an Agda formalization by Andrea Vezzosi, which proves that runST is safe and total for an ST monad with readable/writable refs. It relies on postulated parametricity, i. e. the truth of the free theorems for the involved definitions, which is as expected, since parametricity is precisely the reason why the forall s. trick works.

However, the proof assumes that we can't put values inside an STRef s with types which themselves depend on ST s. In Haskell we can use such dependency to get looping without recursion:

loop :: ()
loop = runST $ do
  x <- newSTRef (pure ())
  writeSTRef x $ do
    y <- readSTRef x
    y
  y <- readSTRef x
  y

Probably this version of the ST monad is still safe, just does not have provably total writeSTRef and readSTRef.

András Kovács
  • 29,931
  • 3
  • 53
  • 99
  • So one would have to prove parametricity for Haskell or Core, which, as far as I know, also has not been done yet. – Joachim Breitner Apr 23 '17 at 21:14
  • Also, without commentary, the Agda formalization is not easy for me to follow, I must admit. – Joachim Breitner Apr 24 '17 at 01:49
  • `do y <- readSTRef x; y` is the same as `join (readSTRef x)`, right? – dfeuer Apr 24 '17 at 18:22
  • 3
    I did a [much simpler](https://gist.github.com/AndrasKovacs/07310be00e2a1bb9e94d7c8dbd1dced6) Agda formalization of ST, if you're interested. It also computes properly, without any unsafe shenanigans. – András Kovács Apr 25 '17 at 16:36
  • @AndrásKovács, how does your theorem relate to the ones proven in the two papers in the other answer? – Joachim Breitner Mar 08 '23 at 13:49
  • @JoachimBreitner I only do total ST where ST actions can't be stored in STRefs. The papers include unrestricted (non-total) ST. Probably my formalization can be extended to a universe hierarchy where we can store "small" ST actions in "large" STRefs. – András Kovács Mar 09 '23 at 10:09
  • I’d love to see a longer paper/blog post/talk about this :-) The size difference to, say, https://github.com/scaup/sem_backs_st/tree/e14aa7f421de94df5c1369d2b4b44d8644243cec is enormous – Joachim Breitner Mar 09 '23 at 16:20
9

It just so happens that Amin Timany et al. have published a paper at POPL2018 about exactly this topic, titled

Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal:
A Logical Relation for Monadic Encapsulation of State
Proving contextual equivalences in the presence of runST

https://dl.acm.org/doi/10.1145/3158152

Four years later, there is another paper on this, now proving that adding ST preserves all equational properties of the language (in a simply typed call-by-value language):

Koen Jacobs, Dominique Devriese, Amin Timany:
Purity of an ST monad: full abstraction by semantically typed back-translation

https://dl.acm.org/doi/10.1145/3527326

Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139
Dominique Devriese
  • 2,998
  • 1
  • 15
  • 21