## Stream: general

### Topic: ST monad is impossible

#### Mario Carneiro (Feb 09 2019 at 09:37):

Just a little proof that might be of general interest. Haskell uses an ST monad for handling mutable variables. Here's a reasonable axiomatization of the primitives:

constant State : Type → Type
constant State.run {α} : (∀ σ, State σ → State σ × α) → α

axiom State.run_eq {α} (f : ∀ σ, State σ → State σ × α)
{a} (h : ∀ σ s, (f σ s).2 = a) : State.run f = a

constant mut_var (σ α : Type) : Type

namespace mut_var

constant mk {σ α} : α → State σ → State σ × mut_var σ α
constant read {σ α} : mut_var σ α → State σ → State σ × α
constant write {σ α} : mut_var σ α → α → State σ → State σ
@[instance] constant decidable_eq {σ α} : decidable_eq (mut_var σ α)

inductive has_val {σ α} : mut_var σ α → State σ → α → Prop
| mk (a s) : has_val (mk a s).2 (mk a s).1 a
| read {v s a β} (v') : has_val v s a → has_val v (@read _ β v' s).1 a
| write_ne {v s a v'} (a') : v ≠ v' → has_val v s a → has_val v (write v' a' s) a
| write_eq {v s a} : has_val v (write v a s) a

axiom read_has_val {σ α} {v : mut_var σ α} {s a} :
has_val v s a → (read v s).2 = a

end mut_var


and here's a proof that it's not consistent:

example : false :=
plift.down $State.run$ λ σ s, false.elim $let v := (mut_var.mk (λ s' : State σ, false) s).2 in @function.cantor_injective (State σ) (λ p, v.write p s)$
@function.injective_of_left_inverse _ _ (λ s', (v.read s').2) _ $by exact λ p, mut_var.read_has_val mut_var.has_val.write_eq  #### Kenny Lau (Feb 09 2019 at 09:40): so Haskell is inconsistent? :o #### Mario Carneiro (Feb 09 2019 at 09:45): Not exactly; Haskell uses a different semantics for functions and types, so this proof is not directly applicable. In fact Haskell has a proof of soundness of the ST monad specifically #### Mario Carneiro (Feb 09 2019 at 09:47): They use System F for the underlying type theory, which is like Type : Type but without choice and other noncomputable things, so function spaces are "smaller than they appear" from the point of view of a rich type theory like lean #### Kevin Buzzard (Feb 09 2019 at 09:47): So Haskell's proofs are incorrect? :o #### Kevin Buzzard (Feb 09 2019 at 09:48): https://www.discogs.com/artist/68181-System-F I remember System F from my 90's raving days. Or is this another System F? #### Mario Carneiro (Feb 09 2019 at 09:48): System F is inconsistent with the types-as-sets model #### Kevin Buzzard (Feb 09 2019 at 09:49): I'll tell him if I ever run into him again #### Mario Carneiro (Feb 09 2019 at 09:50): Unfortunately wikipedia doesn't say where his name came from #### Mario Carneiro (Feb 09 2019 at 09:51): The type system System F was apparently carefully named though - According to Girard, the "F" in System F was picked by chance. #### Kevin Buzzard (Feb 09 2019 at 09:51): The quote about where Ferry Corsten got it from on discogs is not backed up by a reliable secondary source. #### Kevin Buzzard (Feb 09 2019 at 09:52): It is a very cool name though. You can see why it caught on in the Haskell community. #### Mario Carneiro (Feb 09 2019 at 11:06): Actually, it looks like the haskell implementation is not pure functional, although maybe I peeled back too many layers. Here are two ways to play with mutable variables in Haskell, demonstrating that restoring the state before a write does not actually undo the write {-# LANGUAGE MagicHash, UnboxedTuples #-} import GHC.ST import GHC.Base import Data.STRef data State s = State (State# s) readST :: ST s (State s) readST = ST (\s -> (# s, State s #)) writeST :: State s -> ST s () writeST (State s) = ST (\_ -> (# s, () #)) example1 :: (Bool, Bool) example1 = runST$ do
v <- newSTRef False
writeSTRef v True
writeST s
pure (a, b)

example2 :: IO (Bool, Bool)
example2 = IO $\s' -> let (# s, v #) = newMutVar# False s' in let (# _, a #) = readMutVar# v s in let _ = writeMutVar# v True s in let (# _, b #) = readMutVar# v s in (# s, (a, b) #) main = print example1 >> example2 >>= print  Each example should print (False, False). However: $ runhaskell test.hs
(False,True)
(False,True)


#### Reid Barton (Feb 09 2019 at 14:00):

It definitely isn't and isn't supposed to be pure functional--all these operations are O(1). In fact they are the same underlying operations used by IO, which is just the ST monad specialized to s = RealWorld. All these "state token" types have no representation at runtime.

Last updated: Dec 20 2023 at 11:08 UTC