Monads in Lean

Lean monads are introduced through a recursive evaluator for arithmetic expressions that can fail on division by zero. Returning an Option makes failure explicit, but nested pattern matching repeatedly checks for none and stops evaluation when it appears. Factoring that behavior into a helper reveals the key pattern: bind takes a wrapped result and a continuation, propagating failure or passing a successful value onward. Lean’s Monad interface supplies pure and bind, and do notation makes chains of dependent computations concise. The same evaluator can then be generalized to any monad: using Option gives failure without details, while Except carries an error message such as “division by zero.” This illustrates how a computation’s sequencing can be separated from the way its effects are handled.

Further examples show monads modeling accumulated information and changing state. A LoggedOption combines an optional result with a list of messages, appending logs as evaluation proceeds; this is presented as a writer-style monad. A state monad represents a computation as a function from an initial variable environment to an optional result and updated environment. An extended evaluator uses it for variable lookup and assignment, allowing a store on the left side of an addition to affect evaluation of the right side while still propagating division errors. Finally, an IO greeting program demonstrates the same do notation for interacting with the outside world: reading input and printing messages are sequenced while their effects remain encapsulated in IO.