ST monad is impossible

Stream: general

[Mario Carneiro]

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]

so Haskell is inconsistent? :o

[Mario Carneiro]

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]

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]

So Haskell's proofs are incorrect? :o

[Kevin Buzzard]

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]

System F is inconsistent with the types-as-sets model

[Kevin Buzzard]

I'll tell him if I ever run into him again

[Mario Carneiro]

Unfortunately wikipedia doesn't say where his name came from

[Mario Carneiro]

The type system System F was apparently carefully named though -

According to Girard, the "F" in System F was picked by chance.

[Kevin Buzzard]

The quote about where Ferry Corsten got it from on discogs is not backed up by a reliable secondary source.

[Kevin Buzzard]

It is a very cool name though. You can see why it caught on in the Haskell community.

[Mario Carneiro]

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
(False,True)
(False,True)

[Reid Barton]

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.