RealWorld in the IO Monad

Stream: new members

[Deming Xu]

I just found out that IO contains a RealWorld internally. And I wrote a program to experiment.

In this example, if I let Lean run main1 (rename main1 to main and then lean --run realworld.lean), Lean will only ask me to enter 1>>> and then print 1. If I run main2, Lean will ask 1>>> and 2>>>, and then print 1 and 2.

What I want to confirm is whether this behavior is due to some kind of automatic pruning optimization of Lean? In other words, in main1, Lean detects that I don't use msg2, s2 and s4 (these three variables are not needed to calculate the return value), so it removes the second and fourth lines in the actual generated code?

/-
IO α is basically a state machine:
RealWorld → (α × RealWorld)

It takes the state of RealWorld and reads it,
does operations,
and returns the new modified RealWorld together with a result α.
-/

#print IO
-- @[reducible] def IO : Type → Type := EIO IO.Error
#print EIO
-- def EIO : Type → Type → Type := fun ε ↦ EStateM ε IO.RealWorld
#print IO.RealWorld
-- def IO.RealWorld : Type := Unit
#print EStateM
-- def EStateM.{u} := fun ε σ α ↦ σ → EStateM.Result ε σ α
#print EStateM.Result
-- EStateM.Result.ok : {ε σ α : Type u} → α → σ → EStateM.Result ε σ α
-- EStateM.Result.error : {ε σ α : Type u} → ε → σ → EStateM.Result ε σ α

example : IO Unit := by
  unfold IO
  unfold EIO
  unfold EStateM
  change IO Unit -- change the goal back to the original one
  exact IO.println ""

/-- turn the error case into ok case, by making a fake result with a default value. -/
def EStateM.Result.getD {ε σ α : Type} [Inhabited α] (x : EStateM.Result ε σ α) : α × σ :=
  match x with
  | EStateM.Result.ok a s => (a, s)
  | EStateM.Result.error _ s => (default, s)

def getLine (prompt : String) : IO String := do
  IO.print prompt
  let line := (← (← IO.getStdin).getLine).trim
  return s!"For prompt '{prompt.trim}', you entered: '{line}'"

def main1 : IO Unit := fun s0 : IO.RealWorld =>
  let (msg1, s1) := getLine "1>>> " s0 |>.getD;
  let (msg2, s2) := getLine "2>>> " s0 |>.getD;
  let ((), s3) := IO.println msg1 s0 |>.getD;
  let ((), s4) := IO.println msg2 s0 |>.getD;
  EStateM.Result.ok () s3

/-
lean --run realworld.lean

1>>> 1
For prompt '1>>>', you entered: '1'

Here I calculated msg2, but I did not use it, so Lean did not ask user for ">>>2 "
-/


def main2 : IO Unit := fun s0 : IO.RealWorld =>
  let (msg1, s1) := getLine "1>>> " s0 |>.getD;
  let (msg2, s2) := getLine "2>>> " s0 |>.getD;
  let ((), s3) := IO.println (msg1 ++ "\n" ++ msg2) s0 |>.getD;
  let ((), s4) := IO.println msg2 s0 |>.getD;
  EStateM.Result.ok () s3

/-
lean --run realworld.lean

1>>> 1
2>>> 2
For prompt '1>>>', you entered: '1'
For prompt '2>>>', you entered: '2'
-/

[Henrik Böving]

Yeah it's just doing dead code analysis, the point of the RealWorld value is to prevent dead code analysis and reorderings from happening to code like IO that relies on a certain execution order.

[Deming Xu]

I searched for RealWorld on zulip, and it turns out that RealWorld should be treated as a value that can only be used once. Similar to Rust, you can't implicitly copy a value by mentioning it twice.

I feel that after watching RealWorld, my doubts about the IO Monad have finally been resolved. When I learned Haskell's Monad a year ago, I felt that Monad itself was understandable, but the problem was that IO as an instance of Monad was opaque and it was not an inductive type, so you can't really grasp what println getline etc are doing behind the scenes.

After reading this RealWorld example code, and considering the rule that every RealWorld can only be used once, I think I can finally imagine how these Monad codes are converted into ordinary C++, while the RealWorld ensures that the code is not affected by the radical optimization in functional languages, and that these functions are still pure. Then the pure and bind API in the IO Monad is just one way of ensuring that you're using each RealWorld exactly once.

It would be great if those web articles explaining Monad could mention RealWorld.

[Mauricio Collares]

Deming Xu said:

It would be great if those web articles explaining Monad could mention RealWorld.

I'd say the key is to pick the source material judiciously. For example, both #fpil and Peyton-Jones' "Tackling the Awkward Squad" mention the RealWorld model, and the latter even explains the advantages of disadvantages of such a model.