In what sense is Option.or strict in the second argument?

Stream: new members

[Kevin Cheung]

From the documentation:

def Option.or {α : Type u_1} : Option α → Option α → Option α
If the first argument is some a, returns some a, otherwise returns the second
argument. This is similar to <|>/orElse, but it is strict in the second argument.
In what sense is it "strict" in the second argument? When I ran the following, both lines at the end printed only "left":

def left := some (dbgTrace "left" fun _ => 0)
def right := some (dbgTrace "right" fun _ => 1)

#eval Option.or left right -- why isn't right evaluated?
#eval left <|> right

Any help is greatly appreciated.

[Markus Himmel]

The behavior you're seeing is due to the compiler inlining Option.or. You can observe the difference if you hide or and orElse behind definitions:

def left := some (dbgTrace "left" fun _ => 0)
def right := some (dbgTrace "right" fun _ => 1)

def a (left right : Option Nat) := Option.or left right
def b (left : Option Nat) (right : Unit → Option Nat) := left.orElse right

#eval a left right
#eval b left (fun _ => right)

[Kevin Cheung]

Thank you. Is there a way to just turn off inlining?

[Markus Himmel]

In general, inlining is crucial to the performance of Lean code because often the compiler needs to "see" how a definition uses its input in order to perform destructive updates. I'm not aware of a way to turn off inlining for imported functions that are marked to be inlined. If you care about "observable effects" of the code like your dbgTrace, then working in a monad like IO is likely a better option.

[Kevin Cheung]

I see. Thank you.