Is there a proof that runST is indeed pure?

Question

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?

Answer 1

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

Answer 2

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.