4.2. Monad 类型类
不必为每个是单子的类型分别导入像 ok 或 andThen 这样的运算符，Lean 标准库包含一个类型类，允许对它们进行重载，从而同一组运算符可用于任意单子。
单子有两个操作，它们等价于 ok 和 andThen：
class Monad (m : Type → Type) where
pure : α → m α
bind : m α → (α → m β) → m β这个定义略作了简化。 Lean 库中的实际定义稍微更复杂一些，并将在后文给出。
可以通过调整它们各自的 andThen 操作的定义，来创建 Option 和 Except ε 的 Monad 实例：
instance : Monad Option where
pure x := some x
bind opt next :=
match opt with
| none => none
| some x => next x
instance : Monad (Except ε) where
pure x := Except.ok x
bind attempt next :=
match attempt with
| Except.error e => Except.error e
| Except.ok x => next x
例如，firstThirdFifthSeventh 曾分别针对 Option α 和 Except String α 返回类型来定义。
现在，它可以针对任何单子以多态方式定义。
不过，它确实需要一个查找函数作为参数，因为不同的单子可能会以不同方式无法找到结果。
bind 的中缀版本是 >>=，它在示例中扮演与 ~~> 相同的角色。
def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α)
(xs : List α) : m (α × α × α × α) :=
lookup xs 0 >>= fun first =>
lookup xs 2 >>= fun third =>
lookup xs 4 >>= fun fifth =>
lookup xs 6 >>= fun seventh =>
pure (first, third, fifth, seventh)
给定慢速哺乳动物和快速鸟类的示例列表，firstThirdFifthSeventh 的这一实现可以与 Option 一起使用：
def slowMammals : List String :=
["Three-toed sloth", "Slow loris"]
def fastBirds : List String := [
"Peregrine falcon",
"Saker falcon",
"Golden eagle",
"Gray-headed albatross",
"Spur-winged goose",
"Swift",
"Anna's hummingbird"
]#eval firstThirdFifthSeventh (fun xs i => xs[i]?) slowMammals#eval firstThirdFifthSeventh (fun xs i => xs[i]?) fastBirds
在将 Except 的查找函数 get 重命名为更具体的名称之后，完全相同的 firstThirdFifthSeventh 实现也可以与 Except 一起使用：
def getOrExcept (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#eval firstThirdFifthSeventh getOrExcept slowMammals#eval firstThirdFifthSeventh getOrExcept fastBirds4.2.1. 一般的单子操作
由于许多不同类型都是单子，对任意单子具有多态性的函数非常强大。
例如，函数 mapM 是 map 的一个版本，它使用 Monad 来顺序执行并组合函数应用所得的结果：
def mapM [Monad m] (f : α → m β) : List α → m (List β)
| [] => pure []
| x :: xs =>
f x >>= fun hd =>
mapM f xs >>= fun tl =>
pure (hd :: tl)
函数参数 f 的返回类型决定将使用哪个 Monad 实例。
换言之，mapM 可用于产生日志的函数、可能失败的函数，或使用可变状态的函数。
由于 f 的类型决定了可用的效果，API 设计者可以对它们进行严格控制。
如本章引言所述，State σ α 表示使用类型为 σ 的可变变量并返回类型为 α 的值的程序。
这些程序实际上是从初始状态到一个由值和最终状态组成的二元组的函数。
Monad 类要求其参数期望一个单一类型参数；也就是说，它应当是一个 Type → Type。
这意味着 State 的实例应提及状态类型 σ，而该状态类型会成为该实例的一个参数：
instance : Monad (State σ) where
pure x := fun s => (s, x)
bind first next :=
fun s =>
let (s', x) := first s
next x s'
这意味着，在使用 bind 排序的对 get 和 set 的调用之间，状态的类型不能改变；对于有状态计算而言，这是一个合理的规则。
运算符 increment 将保存的状态增加给定的量，并返回旧值：
def increment (howMuch : Int) : State Int Int :=
get >>= fun i =>
set (i + howMuch) >>= fun () =>
pure i
将 mapM 与 increment 一起使用，会得到一个计算列表中各项之和的程序。
更具体地说，可变变量包含当前为止的和，而结果列表包含逐步累计的和。
换言之，mapM increment 的类型为 List Int → State Int (List Int)，展开 State 的定义会得到 List Int → Int → (Int × List Int)。
它以初始和作为参数，该参数应为 0：
#eval mapM increment [1, 2, 3, 4, 5] 04.2.2. 恒等单子
单子将带有效果的程序，例如失败、异常或日志记录，编码为由数据和函数构成的显式表示。 然而，有时 API 会为了灵活性而写成使用单子，但该 API 的客户端可能并不需要任何被编码的效果。 恒等单子 是一种没有效果的单子。 它允许纯代码与单子式 API 一起使用：
def Id (t : Type) : Type := t
instance : Monad Id where
pure x := x
bind x f := f x
pure 的类型应为 α → Id α，但 Id α 会约化为 α。
类似地，bind 的类型应为 α → (α → Id β) → Id β。
因为这会约化为 α → (α → β) → β，所以可以将第二个参数应用于第一个参数以得到结果。
4.2.3. Monad 约定
正如 BEq 和 Hashable 的每一对实例都应保证任意两个相等的值具有相同的散列值一样，Monad 的每个实例也应遵守一个约定。
首先，pure 应是 bind 的左恒等元。
也就是说，bind (pure v) f 应与 f v 相同。
其次，pure 应是 bind 的右恒等元，因此 bind v pure 与 v 相同。
最后，bind 应满足结合律，因此 bind (bind v f) g 与 bind v (fun x => bind (f x) g) 相同。
这一约定更一般地规定了带有效果的程序所应满足的性质。
由于 pure 没有效果，将它的效果与 bind 排序不应改变结果。
bind 的结合律基本上说明，只要保持事情发生的顺序，排序本身的簿记方式并不重要。