haskellsemanticsproofst-monad

Is there a proof that runST is indeed pure?


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?


Solution

  • 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