1. 21

  2. 8

    Thanks to ST, I now know that this not the case, which is a huge relief. If required, I can do a literal translation of the algorithm, and clean it up (or not) later.

    That is not completely true, because you can only embed in ST algorithms that follow a rather simple region discipline in the way the effects flow into the program (the computation has to promise to stop performing effects in the future, and at that time its value becomes accessible as a pure value). This captures a large class of interesting programs, but still there are some algorithms that are observationally pure but internally use mutable states in a way that does not follow this discipline. They cannot be “proven pure” by using ST alone. You can of course write them in Haskell, but their type will carry the impurity annotation and may force you to restructure the rest of your program.

    For a practical example, take laziness: a simple implementation of call-by-need evaluation (where thunks are “memoized” after they have been forced) in a strict language is a function that captures a mutable reference, and mutates it on the first time it is called. This is observationally pure (Haskell uses mutation in this way underneath), but it cannot be given a non-effectful type using ST – its effect discipline is more complex than that, as the initial value (the unevaluated thunk) is returned to the rest of the program while there is still one write to be performed in the future.

    1. 6

      The ST monad is very clever. It’s one of the first places I was exposed to using more abstract types to actually prove something interesting about the way the program works. The Haskell wiki has an explanation, which took me some time to understand: https://wiki.haskell.org/Monad/ST

      The punchline is that if you have a function run :: (forall s. ST s a) -> a, no mention of “s” can escape the expression in which it’s bound (the parentheses), so if a contains s, the compiler will throw an error. The type of all mutable values is tagged with s, so if you try to return a mutable value, a will contain s (like STRef s Int, MVector s Double, etc.). You can “freeze” a mutable value into an immutable one, which will get rid of the s in the type, so you can return it without the compiler complaining.