Monads

Monads m: Type u → Type v are a common structure for sequencing computations that can:

• involve elements in a collection such as a list List,
• fail or have no result, such as Option,
• depend on and alter state, such as StateM,
• take a long time, such as Task,
• have side effects, such as IO, ...

Operations

Monads have the following operations:

• pure : α → m α lifts a value into the monad; return is closely related.
• bind : m α → (α → m β) → m β sequences two computations, also called flatMap in concrete cases.
• map : (α → β) → m α → m β applies a function to the result of a computation.
• flatten : m (m α) → m α collapses nested monadic layers.

These are not independent. The definition of monads only requires pure and bind, but map and flatten can be defined in terms of them.

Do notation

The value of monads is that we can use the do notation to avoid explicitly writing bind and pure. Formally, a do block is just syntax for a term in Lean, with type of the form m α for some α. The do block is translated into a series of bind and pure calls.

Example: Stack

This is just like a list but we put elements at the end.

inductive Stack (α : Type) : Type

• empty {α : Type} : Stack α
• push {α : Type} : Stack α → α → Stack α

instance instInhabitedStack {a✝ : Type} : Inhabited (Stack a✝)

Equations

• instInhabitedStack = { default := Stack.empty }

instance instReprStack {α✝ : Type} [Repr α✝] : Repr (Stack α✝)

Equations

• instReprStack = { reprPrec := reprStack✝ }

def Stack.last? {α : Type} : Stack α → Option α

Equations

• Stack.empty.last? = none
• (a.push a_1).last? = some a_1

def Stack.pop? {α : Type} : Stack α → Option (Stack α × α)

Equations

• Stack.empty.pop? = none
• (a.push a_1).pop? = some (a, a_1)

def Stack.eg : Stack Nat

Equations

• Stack.eg = ((Stack.empty.push 1).push 2).push 3

def Stack.pure {α : Type} (a : α) : Stack α

Equations

• Stack.pure a = Stack.empty.push a

def Stack.map {α β : Type} (f : α → β) (s : Stack α) : Stack β

Equations

• Stack.map f Stack.empty = Stack.empty
• Stack.map f (a.push a_1) = (Stack.map f a).push (f a_1)

def Stack.eg2 : Stack Nat

Equations

• Stack.eg2 = Stack.map (fun (x : Nat) => x * x + 1) Stack.eg

def Stack.eg₃ : Stack Bool

Equations

• Stack.eg₃ = Stack.map (fun (x : Nat) => decide (x % 2 = 0)) Stack.eg

def Stack.append {α : Type} (s₁ s₂ : Stack α) : Stack α

Equations

• s₁.append Stack.empty = s₁
• s₁.append (a.push a_1) = (s₁.append a).push a_1

def Stack.flatten {α : Type} (ss : Stack (Stack α)) : Stack α

Equations

• Stack.empty.flatten = Stack.empty
• (ss_2.push s).flatten = ss_2.flatten.append s

def Stack.flatMap {α β : Type} (f : α → Stack β) (s : Stack α) : Stack β

Equations

• Stack.flatMap f s = (Stack.map f s).flatten

instance Stack.instMonad : Monad Stack

Equations

• Stack.instMonad = Monad.mk

Why flatten: example

def Monads.half? (n : Nat) : Option Nat

Equations

• Monads.half? n = if n % 2 = 0 then some (n / 2) else none

In the following, flatMap is used to apply half? to the result of half?. However, do notation lets us get it conveniently.

First we see a naive version using map.

def Monads.quarter?? (n : Nat) : Option (Option Nat)

Equations

• Monads.quarter?? n = Option.map Monads.half? (Monads.half? n)

def Monads.quarter? (n : Nat) : Option Nat

Equations

• Monads.quarter? n = do let n' ← Monads.half? n let n'' ← Monads.half? n' pure n''

def Monads.quarter?' (n : Nat) : Option Nat

Equations

• Monads.quarter?' n = (Monads.half? n).bind Monads.half?

A simple monad is Id, which is just the identity function. It is useful for writing do blocks that do not involve any monadic operations.