if vs bif in monad has different action order in branches

Stream: lean4

[Gavin Zhao]

Consider the following monad code:

def action_1 : IO Int := pure 42
def action_2 : IO Int := pure 24

def action_with_if : IO Int :=
  do
    if 3 == 5
    then pure 0
    else pure ((← action_1) + (← action_2))

def action_with_bif : IO Int :=
  do
    bif 3 == 5
    then pure 0
    else pure ((← action_1) + (← action_2))

The expected behavior is that if 3 != 5, then action_1 and action_2 would not run. if indeed does this. However, for bif, when I unfold action_with_bif, I see that action_1 and action_2 runs regardless of what the boolean condition evaluates to:

theorem actions_are_equal : action_with_if = action_with_bif :=
  by
    unfold action_with_if
    unfold action_with_bif
    sorry

We can see that the goal is

⊢ (if (3 == 5) = true then pure 0
  else do
    let __do_lift ← action_1
    let __do_lift_1 ← action_2
    pure (__do_lift + __do_lift_1)) =
  do
  let __do_lift ← action_1
  let __do_lift_1 ← action_2
  bif 3 == 5 then pure 0 else pure (__do_lift + __do_lift_1)

This is already semantics difference here. If 3 != 5, action_1 and action_2 shouldn't even run. I thought that bif (i.e. cond) is just a specialized ifon Bool, so they should be exactly the same.

Is this expected behavior? At the very least I think this is very counter-intuitive. Playground link here.

[Aaron Liu]

I am slighly surprised at this

[Aaron Liu]

Regular if then else has special support in do notation (you can omit the else branch so it has to be doing something different) but for bif you can't omit the else branch so I think it might just be a term that's been coerced into the monad? Like this

def action_with_bif : IO Int :=
  do
    (cond (3 == 5)
    (pure 0)
    (pure ((← action_1) + (← action_2))))

which would explain why action_1 and action_2 are lifted outside the bif.

[Gavin Zhao]

From a user's perspective, I'm pretty sure someone will write incorrect code because of this given the documentation for bif/cond kind of says "we're equivalent to if and you should prefer using us if you're comparing booleans".

[Aaron Liu]

yeah I agree this is bad

[Aaron Liu]

just trying to figure out why it does this

[Cameron Zwarich]

It only works for if because the do notation macro has special support for if. Despite bif expanding to cond and cond having the macro_inline attribute, this expansion actually occurs as part of compilation, not in the elaborator. It wouldn't be too difficult for the do notation to support bif (and it probably should), but it would still not work for cond.