Monads

In C# and Kotlin, the ?. operator is a way to look up a property or call a method on a potentially-null value. If the receiver is null, the whole expression is null. Otherwise, the underlying non-null value receives the call. Uses of ?. can be chained, in which case the first null result terminates the chain of lookups. Chaining null-checks like this is much more convenient than writing and maintaining deeply nested ifs.

Similarly, exceptions are significantly more convenient than manually checking and propagating error codes. At the same time, logging is easiest to accomplish by having a dedicated logging framework, rather than having each function return both its log results and its return value. Chained null checks and exceptions typically require language designers to anticipate this use case, while logging frameworks typically make use of side effects to decouple code that logs from the accumulation of the logs.

All these features and more can be implemented in library code as instances of a common API called Monad. Lean provides dedicated syntax that makes this API convenient to use, but can also get in the way of understanding what is going on behind the scenes. This chapter begins with the nitty-gritty presentation of manually nesting null checks, and builds from there to the convenient, general API. Please suspend your disbelief in the meantime.

Checking for none: Don't Repeat Yourself

In Lean, pattern matching can be used to chain checks for null. Getting the first entry from a list can just use the optional indexing notation:

def first (xs : List α) : Option α :=
  xs[0]?

The result must be an Option because empty lists have no first entry. Extracting the first and third entries requires a check that each is not none:

def firstThird (xs : List α) : Option (α × α) :=
  match xs[0]? with
  | none => none
  | some first =>
    match xs[2]? with
    | none => none
    | some third =>
      some (first, third)

Similarly, extracting the first, third, and fifth entries requires more checks that the values are not none:

def firstThirdFifth (xs : List α) : Option (α × α × α) :=
  match xs[0]? with
  | none => none
  | some first =>
    match xs[2]? with
    | none => none
    | some third =>
      match xs[4]? with
      | none => none
      | some fifth =>
        some (first, third, fifth)

And adding the seventh entry to this sequence begins to become quite unmanageable:

def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) :=
  match xs[0]? with
  | none => none
  | some first =>
    match xs[2]? with
    | none => none
    | some third =>
      match xs[4]? with
      | none => none
      | some fifth =>
        match xs[6]? with
        | none => none
        | some seventh =>
          some (first, third, fifth, seventh)

The fundamental problem with this code is that it addresses two concerns: extracting the numbers and checking that all of them are present, but the second concern is addressed by copying and pasting the code that handles the none case. It is often good style to lift a repetitive segment into a helper function:

def andThen (opt : Option α) (next : α → Option β) : Option β :=
  match opt with
  | none => none
  | some x => next x

This helper, which is used similarly to ?. in C# and Kotlin, takes care of propagating none values. It takes two arguments: an optional value and a function to apply when the value is not none. If the first argument is none, then the helper returns none. If the first argument is not none, then the function is applied to the contents of the some constructor.

Now, firstThird can be rewritten to use andThen instead of pattern matching:

def firstThird (xs : List α) : Option (α × α) :=
  andThen xs[0]? fun first =>
  andThen xs[2]? fun third =>
  some (first, third)

In Lean, functions don't need to be enclosed in parentheses when passed as arguments. The following equivalent definition uses more parentheses and indents the bodies of functions:

def firstThird (xs : List α) : Option (α × α) :=
  andThen xs[0]? (fun first =>
    andThen xs[2]? (fun third =>
      some (first, third)))

The andThen helper provides a sort of "pipeline" through which values flow, and the version with the somewhat unusual indentation is more suggestive of this fact. Improving the syntax used to write andThen can make these computations even easier to understand.

Infix Operators

In Lean, infix operators can be declared using the infix, infixl, and infixr commands, which create (respectively) non-associative, left-associative, and right-associative operators. When used multiple times in a row, a left associative operator stacks up the opening parentheses on the left side of the expression. The addition operator + is left associative, so w + x + y + z is equivalent to (((w + x) + y) + z). The exponentiation operator ^ is right associative, so w ^ x ^ y ^ z is equivalent to (w ^ (x ^ (y ^ z))). Comparison operators such as < are non-associative, so x < y < z is a syntax error and requires manual parentheses.

The following declaration makes andThen into an infix operator:

infixl:55 " ~~> " => andThen

The number following the colon declares the precedence of the new infix operator. In ordinary mathematical notation, x + y * z is equivalent to x + (y * z) even though both + and * are left associative. In Lean, + has precedence 65 and * has precedence 70. Higher-precedence operators are applied before lower-precedence operators. According to the declaration of ~~>, both + and * have higher precedence, and thus apply first. Typically, figuring out the most convenient precedences for a group of operators requires some experimentation and a large collection of examples.

Following the new infix operator is a double arrow =>, which specifies the named function to be used for the infix operator. Lean's standard library uses this feature to define + and * as infix operators that point at HAdd.hAdd and HMul.hMul, respectively, allowing type classes to be used to overload the infix operators. Here, however, andThen is just an ordinary function.

Having defined an infix operator for andThen, firstThird can be rewritten in a way that brings the "pipeline" feeling of none-checks front and center:

def firstThirdInfix (xs : List α) : Option (α × α) :=
  xs[0]? ~~> fun first =>
  xs[2]? ~~> fun third =>
  some (first, third)

This style is much more concise when writing larger functions:

def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) :=
  xs[0]? ~~> fun first =>
  xs[2]? ~~> fun third =>
  xs[4]? ~~> fun fifth =>
  xs[6]? ~~> fun seventh =>
  some (first, third, fifth, seventh)

Propagating Error Messages

Pure functional languages such as Lean have no built-in exception mechanism for error handling, because throwing or catching an exception is outside of the step-by-step evaluation model for expressions. However, functional programs certainly need to handle errors. In the case of firstThirdFifthSeventh, it is likely relevant for a user to know just how long the list was and where the lookup failed.

This is typically accomplished by defining a datatype that can be either an error or a result, and translating functions with exceptions into functions that return this datatype:

inductive Except (ε : Type) (α : Type) where
  | error : ε → Except ε α
  | ok : α → Except ε α
deriving BEq, Hashable, Repr

The type variable ε stands for the type of errors that can be produced by the function. Callers are expected to handle both errors and successes, which makes the type variable ε play a role that is a bit like that of a list of checked exceptions in Java.

Similarly to Option, Except can be used to indicate a failure to find an entry in a list. In this case, the error type is a String:

def get (xs : List α) (i : Nat) : Except String α :=
  match xs[i]? with
  | none => Except.error s!"Index {i} not found (maximum is {xs.length - 1})"
  | some x => Except.ok x

Looking up an in-bounds value yields an Except.ok:

def ediblePlants : List String :=
  ["ramsons", "sea plantain", "sea buckthorn", "garden nasturtium"]

#eval get ediblePlants 2

Except.ok "sea buckthorn"

Looking up an out-of-bounds value yields an Except.error:

#eval get ediblePlants 4

Except.error "Index 4 not found (maximum is 3)"

A single list lookup can conveniently return a value or an error:

def first (xs : List α) : Except String α :=
  get xs 0

However, performing two list lookups requires handling potential failures:

def firstThird (xs : List α) : Except String (α × α) :=
  match get xs 0 with
  | Except.error msg => Except.error msg
  | Except.ok first =>
    match get xs 2 with
    | Except.error msg => Except.error msg
    | Except.ok third =>
      Except.ok (first, third)

Adding another list lookup to the function requires still more error handling:

def firstThirdFifth (xs : List α) : Except String (α × α × α) :=
  match get xs 0 with
  | Except.error msg => Except.error msg
  | Except.ok first =>
    match get xs 2 with
    | Except.error msg => Except.error msg
    | Except.ok third =>
      match get xs 4 with
      | Except.error msg => Except.error msg
      | Except.ok fifth =>
        Except.ok (first, third, fifth)

And one more list lookup begins to become quite unmanageable:

def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) :=
  match get xs 0 with
  | Except.error msg => Except.error msg
  | Except.ok first =>
    match get xs 2 with
    | Except.error msg => Except.error msg
    | Except.ok third =>
      match get xs 4 with
      | Except.error msg => Except.error msg
      | Except.ok fifth =>
        match get xs 6 with
        | Except.error msg => Except.error msg
        | Except.ok seventh =>
          Except.ok (first, third, fifth, seventh)

Once again, a common pattern can be factored out into a helper. Each step through the function checks for an error, and only proceeds with the rest of the computation if the result was a success. A new version of andThen can be defined for Except:

def andThen (attempt : Except e α) (next : α → Except e β) : Except e β :=
  match attempt with
  | Except.error msg => Except.error msg
  | Except.ok x => next x

Just as with Option, this version of andThen allows a more concise definition of firstThird:

def firstThird' (xs : List α) : Except String (α × α) :=
  andThen (get xs 0) fun first  =>
  andThen (get xs 2) fun third =>
  Except.ok (first, third)

In both the Option and Except case, there are two repeating patterns: there is the checking of intermediate results at each step, which has been factored out into andThen, and there is the final successful result, which is some or Except.ok, respectively. For the sake of convenience, success can be factored out into a helper called ok:

def ok (x : α) : Except ε α := Except.ok x

Similarly, failure can be factored out into a helper called fail:

def fail (err : ε) : Except ε α := Except.error err

Using ok and fail makes get a little more readable:

def get (xs : List α) (i : Nat) : Except String α :=
  match xs[i]? with
  | none => fail s!"Index {i} not found (maximum is {xs.length - 1})"
  | some x => ok x

After adding the infix declaration for andThen, firstThird can be just as concise as the version that returns an Option:

infixl:55 " ~~> " => andThen

def firstThird (xs : List α) : Except String (α × α) :=
  get xs 0 ~~> fun first =>
  get xs 2 ~~> fun third =>
  ok (first, third)

The technique scales similarly to larger functions:

def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) :=
  get xs 0 ~~> fun first =>
  get xs 2 ~~> fun third =>
  get xs 4 ~~> fun fifth =>
  get xs 6 ~~> fun seventh =>
  ok (first, third, fifth, seventh)

Logging

A number is even if dividing it by 2 leaves no remainder:

def isEven (i : Int) : Bool :=
  i % 2 == 0

The function sumAndFindEvens computes the sum of a list while remembering the even numbers encountered along the way:

def sumAndFindEvens : List Int → List Int × Int
  | [] => ([], 0)
  | i :: is =>
    let (moreEven, sum) := sumAndFindEvens is
    (if isEven i then i :: moreEven else moreEven, sum + i)

This function is a simplified example of a common pattern. Many programs need to traverse a data structure once, while both computing a main result and accumulating some kind of tertiary extra result. One example of this is logging: a program that is an IO action can always log to a file on disk, but because the disk is outside of the mathematical world of Lean functions, it becomes much more difficult to prove things about logs based on IO. Another example is a function that computes the sum of all the nodes in a tree with an inorder traversal, while simultaneously recording each nodes visited:

def inorderSum : BinTree Int → List Int × Int
  | BinTree.leaf => ([], 0)
  | BinTree.branch l x r =>
    let (leftVisited, leftSum) := inorderSum l
    let (hereVisited, hereSum) := ([x], x)
    let (rightVisited, rightSum) := inorderSum r
    (leftVisited ++ hereVisited ++ rightVisited, leftSum + hereSum + rightSum)

Both sumAndFindEvens and inorderSum have a common repetitive structure. Each step of computation returns a pair that consists of a list of data that have been saved along with the primary result. The lists are then appended, and the primary result is computed and paired with the appended lists. The common structure becomes more apparent with a small rewrite of sumAndFindEvens that more cleanly separates the concerns of saving even numbers and computing the sum:

def sumAndFindEvens : List Int → List Int × Int
  | [] => ([], 0)
  | i :: is =>
    let (moreEven, sum) := sumAndFindEvens is
    let (evenHere, ()) := (if isEven i then [i] else [], ())
    (evenHere ++ moreEven, sum + i)

For the sake of clarity, a pair that consists of an accumulated result together with a value can be given its own name:

structure WithLog (logged : Type) (α : Type) where
  log : List logged
  val : α

Similarly, the process of saving a list of accumulated results while passing a value on to the next step of a computation can be factored out into a helper, once again named andThen:

def andThen (result : WithLog α β) (next : β → WithLog α γ) : WithLog α γ :=
  let {log := thisOut, val := thisRes} := result
  let {log := nextOut, val := nextRes} := next thisRes
  {log := thisOut ++ nextOut, val := nextRes}

In the case of errors, ok represents an operation that always succeeds. Here, however, it is an operation that simply returns a value without logging anything:

def ok (x : β) : WithLog α β := {log := [], val := x}

Just as Except provides fail as a possibility, WithLog should allow items to be added to a log. This has no interesting return value associated with it, so it returns Unit:

def save (data : α) : WithLog α Unit :=
  {log := [data], val := ()}

WithLog, andThen, ok, and save can be used to separate the logging concern from the summing concern in both programs:

def sumAndFindEvens : List Int → WithLog Int Int
  | [] => ok 0
  | i :: is =>
    andThen (if isEven i then save i else ok ()) fun () =>
    andThen (sumAndFindEvens is) fun sum =>
    ok (i + sum)

def inorderSum : BinTree Int → WithLog Int Int
  | BinTree.leaf => ok 0
  | BinTree.branch l x r =>
    andThen (inorderSum l) fun leftSum =>
    andThen (save x) fun () =>
    andThen (inorderSum r) fun rightSum =>
    ok (leftSum + x + rightSum)

And, once again, the infix operator helps put focus on the correct steps:

infixl:55 " ~~> " => andThen

def sumAndFindEvens : List Int → WithLog Int Int
  | [] => ok 0
  | i :: is =>
    (if isEven i then save i else ok ()) ~~> fun () =>
    sumAndFindEvens is ~~> fun sum =>
    ok (i + sum)

def inorderSum : BinTree Int → WithLog Int Int
  | BinTree.leaf => ok 0
  | BinTree.branch l x r =>
    inorderSum l ~~> fun leftSum =>
    save x ~~> fun () =>
    inorderSum r ~~> fun rightSum =>
    ok (leftSum + x + rightSum)

Numbering Tree Nodes

An inorder numbering of a tree associates each data point in the tree with the step it would be visited at in an inorder traversal of the tree. For example, consider aTree:

open BinTree in
def aTree :=
  branch
    (branch
       (branch leaf "a" (branch leaf "b" leaf))
       "c"
       leaf)
    "d"
    (branch leaf "e" leaf)

Its inorder numbering is:

BinTree.branch
  (BinTree.branch
    (BinTree.branch (BinTree.leaf) (0, "a") (BinTree.branch (BinTree.leaf) (1, "b") (BinTree.leaf)))
    (2, "c")
    (BinTree.leaf))
  (3, "d")
  (BinTree.branch (BinTree.leaf) (4, "e") (BinTree.leaf))

Trees are most naturally processed with recursive functions, but the usual pattern of recursion on trees makes it difficult to compute an inorder numbering. This is because the highest number assigned anywhere in the left subtree is used to determine the numbering of a node's data value, and then again to determine the starting point for numbering the right subtree. In an imperative language, this issue can be worked around by using a mutable variable that contains the next number to be assigned. The following Python program computes an inorder numbering using a mutable variable:

class Branch:
    def __init__(self, value, left=None, right=None):
        self.left = left
        self.value = value
        self.right = right
    def __repr__(self):
        return f'Branch({self.value!r}, left={self.left!r}, right={self.right!r})'

def number(tree):
    num = 0
    def helper(t):
        nonlocal num
        if t is None:
            return None
        else:
            new_left = helper(t.left)
            new_value = (num, t.value)
            num += 1
            new_right = helper(t.right)
            return Branch(left=new_left, value=new_value, right=new_right)

    return helper(tree)

The numbering of the Python equivalent of aTree is:

a_tree = Branch("d",
                left=Branch("c",
                            left=Branch("a", left=None, right=Branch("b")),
                            right=None),
                right=Branch("e"))

and its numbering is:

>>> number(a_tree)
Branch((3, 'd'), left=Branch((2, 'c'), left=Branch((0, 'a'), left=None, right=Branch((1, 'b'), left=None, right=None)), right=None), right=Branch((4, 'e'), left=None, right=None))

Even though Lean does not have mutable variables, a workaround exists. From the point of view of the rest of the world, the mutable variable can be thought of as having two relevant aspects: its value when the function is called, and its value when the function returns. In other words, a function that uses a mutable variable can be seen as a function that takes the mutable variable's starting value as an argument, returning a pair of the variable's final value and the function's result. This final value can then be passed as an argument to the next step.

Just as the Python example uses an outer function that establishes a mutable variable and an inner helper function that changes the variable, a Lean version of the function uses an outer function that provides the variable's starting value and explicitly returns the function's result along with an inner helper function that threads the variable's value while computing the numbered tree:

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper (n : Nat) : BinTree α → (Nat × BinTree (Nat × α))
    | BinTree.leaf => (n, BinTree.leaf)
    | BinTree.branch left x right =>
      let (k, numberedLeft) := helper n left
      let (i, numberedRight) := helper (k + 1) right
      (i, BinTree.branch numberedLeft (k, x) numberedRight)
  (helper 0 t).snd

This code, like the none-propagating Option code, the error-propagating Except code, and the log-accumulating WithLog code, commingles two concerns: propagating the value of the counter, and actually traversing the tree to find the result. Just as in those cases, an andThen helper can be defined to propagate state from one step of a computation to another. The first step is to give a name to the pattern of taking an input state as an argument and returning an output state together with a value:

def State (σ : Type) (α : Type) : Type :=
  σ → (σ × α)

In the case of State, ok is a function that returns the input state unchanged, along with the provided value:

def ok (x : α) : State σ α :=
  fun s => (s, x)

When working with a mutable variable, there are two fundamental operations: reading the value and replacing it with a new one. Reading the current value is accomplished with a function that places the input state unmodified into the output state, and also places it into the value field:

def get : State σ σ :=
  fun s => (s, s)

Writing a new value consists of ignoring the input state, and placing the provided new value into the output state:

def set (s : σ) : State σ Unit :=
  fun _ => (s, ())

Finally, two computations that use state can be sequenced by finding both the output state and return value of the first function, then passing them both into the next function:

def andThen (first : State σ α) (next : α → State σ β) : State σ β :=
  fun s =>
    let (s', x) := first s
    next x s'

infixl:55 " ~~> " => andThen

Using State and its helpers, local mutable state can be simulated:

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper : BinTree α → State Nat (BinTree (Nat × α))
    | BinTree.leaf => ok BinTree.leaf
    | BinTree.branch left x right =>
      helper left ~~> fun numberedLeft =>
      get ~~> fun n =>
      set (n + 1) ~~> fun () =>
      helper right ~~> fun numberedRight =>
      ok (BinTree.branch numberedLeft (n, x) numberedRight)
  (helper t 0).snd

Because State simulates only a single local variable, get and set don't need to refer to any particular variable name.

Monads: A Functional Design Pattern

Each of these examples has consisted of:

• A polymorphic type, such as Option, Except ε, WithLog logged, or State σ
• An operator andThen that takes care of some repetitive aspect of sequencing programs that have this type
• An operator ok that is (in some sense) the most boring way to use the type
• A collection of other operations, such as none, fail, save, and get, that name ways of using the type

This style of API is called a monad. While the idea of monads is derived from a branch of mathematics called category theory, no understanding of category theory is needed in order to use them for programming. The key idea of monads is that each monad encodes a particular kind of side effect using the tools provided by the pure functional language Lean. For example, Option represents programs that can fail by returning none, Except represents programs that can throw exceptions, WithLog represents programs that accumulate a log while running, and State represents programs with a single mutable variable.