Zulip Chat Archive

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):


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
  s <- readST
  a <- readSTRef v
  writeSTRef v True
  writeST s
  b <- readSTRef v
  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

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: Aug 03 2023 at 10:10 UTC