Menu
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?
956
The answer, for simplicities sake first for pure iron only, is simple: Iron rusts, meaning it oxidizes because iron atoms like to be surrounded by oxygen atoms (or sulfur atoms or...) far more than to be surround by brethren iron atoms. Being oxidized is closer to nirvana than being pure.
Known as the precious metals, platinum, gold and silver are all pure metals, therefore they contain no iron and cannot rust. Platinum and gold are highly non-reactive, and although silver can tarnish, it is fairly corrosion-resistant and relatively affordable by comparison.
All metals can corrode. Some, like pure iron, corrode quickly. Stainless steel, however, which combines iron and other alloys, is slower to corrode and is therefore used more frequently. All small group of metals, called the Noble Metals, are much less reactive than others.
Rust is the common name for a very common compound, iron oxide. Iron oxide, the chemical Fe2O3, is common because iron combines very readily with oxygen -- so readily, in fact, that pure iron is only rarely found in nature.
It just so happens that Amin Timany et al. have recently published a paper at POPL2018 about exactly this topic. You can find the paper here. Full disclosure: I haven't found the time to read it thoroughly yet myself :).
194
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.
43
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
