How does IO.lazyPure work?

Stream: lean4

[Geoffrey Irving]

IO.lazyPure has no doc string, but from the name what I expected it to do is evaluate the computation only once the returned IO monad is run. But it doesn't seem to do that:

def lazyPure (fn : Unit → α) : IO α :=
  pure (fn ())

If I'm reading that right, it first calls the function, then constructs an IO monad out of it, which if run will immediately return the result that was already computed when lazyPure was called. Am I reading that right?

[Geoffrey Irving]

I'd expect it to look more like this, though I'm also not 100% sure this is lazy:

def lazyPure {α : Type} (f : Unit → α) : IO α := do
  let x := f ()
  pure x

[Sebastian Ullrich]

You cannot answer this question by looking only at the surface syntax. The IR looks correct.

[Sebastian Ullrich]

due to automatic eta expansion in the compiler

[Geoffrey Irving]

How does it know to make correct IR? Also, how do I look at the IR?

[Sebastian Ullrich]

It's trace.compiler.ir.result but I didn't mention it since the output is probably not very meaningful unless you already know about the option :)

[Geoffrey Irving]

I see, so the language itself has some laziness in the execution semantics.

[Geoffrey Irving]

I've written compilers.

[Sebastian Ullrich]

Not sure that would've helped me personally speaking! But if you're interested in the details, the IR described in our Counting Immutable Beans paper is still relatively close to what's in Lean today

[Eric Wieser]

What's the example where pure and lazyPure behave differently?

[Geoffrey Irving]

If you do pure, the computation happens in the outer function. If you then don't inline pure, it's bad. Here I think things only work since pure inlined into lazyPure.

[Geoffrey Irving]

The IR doesn't contain a pure call:

[result]
def BaseIO.lazyPure._rarg (x_1 : obj) (x_2 : obj) : obj :=
  let x_3 : obj := ctor_0[PUnit.unit];
  let x_4 : obj := app x_1 x_3;
  let x_5 : obj := ctor_0[EStateM.Result.ok] x_4 x_2;
  ret x_5
def BaseIO.lazyPure (x_1 : ◾) : obj :=
  let x_2 : obj := pap BaseIO.lazyPure._rarg;
  ret x_2

[Sebastian Ullrich]

For the sake of completeness it should also be mentioned that this function seems completely unused in core

[Timo Carlin-Burns]

I don't think pure needs to be inlined for lazyPure to have the desired semantics. If we take as an assumption that the compiler always uncurries top-level definitions before compiling them, then because IO α is defined as IO.RealWorld -> EStateM.Result IO.Error IO.RealWorld α, any function which is returning IO α will be compiled into a function taking IO.RealWorld as its final argument. In the example of lazyPure, that results in a definition like this, which will be lazy when partially applied regardless of whether pure is inlined.

def lazyPure (fn : Unit → α) (world : IO.RealWorld) : EStateM.Result IO.Error IO.RealWorld α :=
  (pure (fn ()) : IO α) world

I was confused about a similar situation with IO and FFI before.