Monads in Lean

This post demonstrates how to use monads in the Lean programming language (Lean 4, to be specific). If you're not familiar with Lean, this part of the language is very similar to other functional programming languages, like Haskell or OCaml. Motivating example - evaluating expressions Suppose we want to write a simple numerical expression evaluator that supports numbers with addition and division: inductive Expr where | num : Int → Expr | add : Expr → Expr → Expr | div : Expr → Expr → Expr What happens when we encounter a division by zero? We'll want our evaluator to report this as a failure, which will be represented explicitly using the the Option type: def safeDiv (x y : Int) : Option Int := if y == 0 then none else some (x / y) With this in hand, the eval function can be written as follows: def eval : Expr → Option Int | .num n => some n | .add a b => match eval a with | none => none | some x => match eval b with | none => none | some y => some (x + y) | .div a b => match eval a…

Commenting on Bubbles has been removed. Why? If you want to talk about this post, write to the author, use the comments on their blog if it has them, or reply with a "RE:" post on your own blog. Suggestions? feedback@bubbles.town