When do we backtrack on failure in a monad?

Stream: lean4

[Thomas Murrills]

I'm under the impression that in several common monads, like MetaM, failure causes backtracking. Is this actually true?

If so, is there a typeclass that enforces this? Or is this contingent on the particular implementation of some definition, like Alternative.failure itself or run, for the given monad performing the backtracking? What actually causes backtracking-upon-failure behavior?

[Scott Morrison]

I think this is just up to whoever provides the Alternative instance. From Lean.Meta.Basic:

@[inline] protected def orElse (x : MetaM α) (y : Unit → MetaM α) : MetaM α := do
  let s ← saveState
  try x catch _ => s.restore; y ()

instance : OrElse (MetaM α) := ⟨Meta.orElse⟩

instance : Alternative MetaM where
  failure := fun {_} => throwError "failed"
  orElse  := Meta.orElse

[Scott Morrison]

I would actually really like to add the Alternative List instance with orElse being ++.

[Thomas Murrills]

So, then I guess the questions become: (1) does throwError by itself cause any backtracking? (2) where might orElse appear? For example, is there a hidden orElse generated in situations like do ... let a ← foo ...?

[Eric Wieser]

let some a ← foo certainly emits an orElse or something built upon it