4.2. Monad类型类
无需为每个单子都实现 ok 或 andThen 这样的运算符，Lean标准库包含一个类型类，
允许它们被重载，以便相同的运算符可用于 任何 单子。
单子有两个操作，分别相当于 ok 和 andThen：
class Monad (m : Type → Type) where
pure : α → m α
bind : m α → (α → m β) → m β这个定义略微简化了。 Lean 标准库中的实际定义更复杂一些，稍后会介绍。
Option 和 Except ε 的 Monad 实例，可以通过调整它们各自的 andThen 操作的定义来创建：
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)
给定作为示例的slowMammals和fastBirds列表，该 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 fastBirds
m 必须有 Monad 实例，这一事实这意味着可以使用 >>= 和 pure 运算符。
4.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 的类型直接决定了可用的效应(Effects)，因此API设计人员可以对其进行严格控制。
译者注：效应(Effects)是函数式编程中与 Monad 密切相关的主题，
实际上对效应的控制比此处原文所述更复杂一些，但超出了本文的内容。
另外副作用(Side Effects)也是一种效应。
如本章简介所介绍的，State σ α表示使用类型为 σ 的可变变量，并返回类型为 α 的值的程序。
这些程序实际上是从起始状态到值和最终状态构成的对(pair)的函数。
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] 0
可以使用 WithLog 表示日志记录效应。
就和 State 一样，它的 Monad 实例对于被记录数据的类型也是多态的：
instance : Monad (WithLog logged) where
pure x := {log := [], val := x}
bind result next :=
let {log := thisOut, val := thisRes} := result
let {log := nextOut, val := nextRes} := next thisRes
{log := thisOut ++ nextOut, val := nextRes}
saveIfEven函数记录偶数，但将参数原封不动返回：
def saveIfEven (i : Int) : WithLog Int Int :=
(if isEven i then
save i
else pure ()) >>= fun () =>
pure i
将 mapM 和该函数一起使用，会生成一个记录偶数的日志、和未更改的输入列表：
#eval mapM saveIfEven [1, 2, 3, 4, 5]4.2.2. 恒等单子
单子将具有效应(Effects)的程序（例如失败、异常或日志记录）编码为数据和函数的显式表示。 有时API会使用单子来提高灵活性，但API的使用方可能不需要任何效应。 恒等单子 (Identity Monad)是一个没有任何效应的单子，允许将纯(pure)代码与monadic 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 β。
由于这 归约 为 α → (α → β) → β，因此可以将第二个参数应用于第一个参数得到结果。
译者注：此处 归约 一词原文为reduces to，实际含义为beta-reduction，请见类型论相关资料。
使用恒等单子时，mapM等同于map。但是要以这种方式调用它，Lean需要额外的提示来表明目标单子是 Id：
#eval mapM (m := Id) (· + 1) [1, 2, 3, 4, 5]省略提示则会导致错误：
#eval mapM (· + 1) [1, 2, 3, 4, 5]
导致错误的原因是：一个元变量应用于另一个元变量，使得Lean不会反向运行类型计算。
函数的返回类型应该是应用于其他类型参数的单子。
类似地，将 mapM 和未提供任何特定单子类型信息的函数一起使用，会导致 “instance problem stuck” 错误：
#eval mapM (fun (x : Nat) => x) [1, 2, 3, 4, 5]4.2.3. 单子约定
正如 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满足的结合律则意味着先计算哪一部分无关紧要，只要保证效应的顺序不变即可。
4.2.4. 练习
4.2.4.1. 映射一棵树
定义函数BinTree.mapM。
通过类比列表的mapM，此函数应将单子函数应用于树中的每个节点，作为前序遍历。
类型签名应为：
def BinTree.mapM [Monad m] (f : α → m β) : BinTree α → m (BinTree β)4.2.4.2. Option单子的约定
首先充分论证 Option 的 Monad 实例满足单子约定。
然后，考虑以下实例：
instance : Monad Option where
pure x := some x
bind opt next := none这两个方法都有正确的类型。 但这个实例却违反了单子约定，为什么？