Semantics of IO don't match provable properties?

Stream: lean4

[Niels Voss]

I was experimenting with the IO monad and noticed that it was defined using EStateM and IO.RealWorld. I was worried that this gives you too much control over the monad, to the point where you can "reset time" by saving and restoring an old version of the world.

import Mathlib

set_option autoImplicit false

def run : IO Unit := fun world =>
  let r := (do println! "hello") world
  match r with -- force evaluation of r
  | EStateM.Result.ok _ _ =>
    if (0 : ℚ) = 0 then -- irreducible computation to prevent optimization
      (do println! "ok") world
    else (do println! "ok2") world
  | EStateM.Result.error _ _ =>
    (do println! "ok") world

theorem run_eq_ok : run = println! "ok" := by
  funext w
  unfold run
  aesop

#eval run
/-
hello
ok
-/

Here, run prints both "hello" and "ok", but we can prove that it only prints "ok". Of course, the problem comes down to the fact that we are using the same IO.RealWorld value twice. But I think this problem could have been avoided if IO was made into an opaque monad instead of something easily unfoldable. Do I basically have to accept that proofs about the properties of IO functions are meaningless because their logical representation doesn't match their behavior?

[Edward van de Meent]

it gets worse if you look at the definition of IO.RealWorld :sweat_smile:

[Edward van de Meent]

it's not even opaque

[Niels Voss]

I assumed that would get fixed eventually. But the ability to use values of IO.RealWorld twice seems like a very deep issue.

[Kyle Miller]

Lean doesn't have support for affine types, which could address this. (Or inventing time travel so if you use an old version of the world you can just go back in time :smile:)

Another issue is that even if you had this, things like IO.Ref have no axioms, and Mario thinks the obvious axioms might even lead to inconsistencies.

[Niels Voss]

I mean, any axioms for IO.Ref would almost certainly be unsound if you could just send the world back in time. Would changing IO to an opaque monad fix these issues, or would it lead to the same problems?

[Edward van de Meent]

Kyle Miller said:

(Or inventing time travel so if you use an old version of the world you can just go back in time :smile:)

maybe you may have the compiler optimise the first print away, to make this consistent?

[Niels Voss]

It actually took me a while to get a program where the compiler didn't optimize the first print away. That's why I had to use Rat in my example, since it is complicated enough that the compiler couldn't deduce that (0 : Rat) = 0 is defeq to True.

However, I suspect that optimizing the first print away in general is an undecidable problem. Especially because that first print could have instead been a readLine that returned a useful value, that we later use in conjunction with the old world.

[Niels Voss]

Is there any way in which Lean can support something that behaves semantically like affine types without having to modify the kernel?

[Kyle Miller]

I doubt there's a "sufficiently smart compiler" that would solve the issue through optimization; that readLine example points to it not just being undecidable, but impossible.

[Kyle Miller]

Niels Voss said:

Would changing IO to an opaque monad fix these issues, or would it lead to the same problems?

Sorry, I don't know, though my suspicion would be that without proper affine type support there are bound to be other semantic leaks. I don't know if there are well-known tricks in the literature though.

[Kyle Miller]

Niels Voss said:

Is there any way in which Lean can support something that behaves semantically like affine types without having to modify the kernel?

You should be able to bolt an affine type checker on top of Lean. I don't know if I have the correct link, but here's an example of homotopy type theory in Lean 4: https://github.com/forked-from-1kasper/ground_zero It adds an extra checker to make sure that theorems are only doing HoTT-appropriate things. The trusted code base would expand to include your checker and some amount of the elaborator.

[Niels Voss]

Kyle Miller said:

You should be able to bolt an affine type checker on top of Lean. I don't know if I have the correct link, but here's an example of homotopy type theory in Lean 4: https://github.com/forked-from-1kasper/ground_zero It adds an extra checker to make sure that theorems are only doing HoTT-appropriate things.

Maybe this could be used in conjunction with something like Part, which would prevent the code from being run unless it was proven to be safe. (I was also thinking of how Part could in theory let you write unsafe code with stuff like malloc and free but not actually run it unless it was safe)

[Edward van de Meent]

i suppose ideally we'd have all IO things be defined with partial?

[Edward van de Meent]

or would that be annoying?

[Niels Voss]

well maybe we should leave IO alone because so much depends on it and just accept that proofs about IO are useless, but it might be good to have a more safe monad that was actually semantically valid that would be good enough to replace IO in most cases

[Niels Voss]

I was originally thinking that we could define something like AffineM T : Type -> Type := StateT T Part but I'm actually not sure that's good enough

[Kyle Miller]

Yeah, often there's the "programming type" and the "proving type". If there's a "proving IO" with good semantics, then you would need to extend your trusted code base with the "proving IO -> programming IO" evaluator, which is probably not that much code.

[Mario Carneiro]

I believe that making IO opaque (such that you can't even tell it's a function type) would be sufficient to avoid leaks related to time travelling tokens because the token wouldn't be available in the first place. But the issue Kyle mentioned about IO.Ref is deeper than that and would still be the case even if everything related to IO.Ref was opaque (it already is to a great extent), because it has to do with the fact that IO.Ref can be used to construct state larger than an IO Unit value could store (by cardinality considerations, just by virtue of being a type living at a fixed universe)

[Kyle Miller]

Have you thought about any solutions to that problem @Mario Carneiro?

Maybe there could be an inductive type T that represents all the values that an IO.Ref could store, and the interface requires an injective function from your type to T and a decoding function. Theoretically IO.Ref uses T, but behind the scenes the runtime would just use your type directly.

[Mario Carneiro]

Yeah, I had a demo that did basically that somewhere

[Mario Carneiro]

it was mediated by a typeclass so you didn't have to do too much work

[Mario Carneiro]

def ST' (ω α : Type) : Type := StateM (Array ω) α

namespace ST'
class IsRef (ω α : Type) where
  get : ω → Option α
  set : α → ω

def Ref (ω α : Type) : Type := Nat × IsRef ω α

def mkRef {ω α} [inst : IsRef ω α] (a : α) : ST' ω (Ref ω α) :=
  fun m => ((m.size, inst), m.push (inst.set a))
def Ref.get {ω α} [Inhabited α] (r : @& Ref ω α) : ST' ω α :=
  fun m => ((m[r.1]?.bind r.2.get).get!, m) -- ignore the `get!` here
def Ref.set {ω α} (r : @& Ref ω α) (a : α) : ST' ω Unit :=
  fun m => ((), m.set! r.1 (r.2.set a))

def run (ω) (x : ST' ω α) : α := (x #[]).1

[Edward van de Meent]

could you give a concrete example of an issue that IO.Ref causes?

[Edward van de Meent]

because i don't quite get what the problem is

[Mario Carneiro]

I don't have an actual proof of false, so it's a bit handwavy

[Edward van de Meent]

any anecdotal evidence?

[Edward van de Meent]

because from my understanding, i don't quite see how IO.Ref creates "too large" IO Units

[Mario Carneiro]

import Mathlib.Logic.Function.Basic

variable {σ : Type} -- this type parameter doesn't matter

-- For fixed r, this function has type α → ST σ Unit.
-- But it's injective? `α` need not be smaller than `ST σ Unit`
def set' {α} (r : ST.Ref σ α) (x : α) : ST σ Unit := r.set x

def inv {α} (r : ST.Ref σ α) (m : ST σ Unit) : ST σ α := do m; r.get

-- this is not exactly true, but this is the idea
axiom set'_inv {α} (r : ST.Ref σ α) (x : α) : inv r (set' r x) = pure x

-- reasonable axiom because `runST` allows you to get the `α` out
axiom pure_inj {α} : Function.Injective (pure : α → ST σ α)

-- so what happens if `α := (ST σ Unit -> Prop)`?

def foo : False := PLift.down <| runST fun σ => do
  let r ← ST.mkRef (σ := σ) (fun _ : ST σ Unit => False)
  let set' := set' r
  let inv := inv r
  have H : ∀ x, inv (set' x) = pure x := set'_inv r
  have : Function.Injective set' := fun x y h => by
    have := congr_arg inv h
    rw [H, H] at this
    exact pure_inj this
  nomatch Function.cantor_injective _ this