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

none

#eval firstThirdFifthSeventh (fun xs i => xs[i]?) fastBirds

some ("Peregrine falcon", "Golden eagle", "Spur-winged goose", "Anna's hummingbird")

在将 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

Except.error "Index 2 not found (maximum is 1)"

#eval firstThirdFifthSeventh getOrExcept fastBirds

Except.ok ("Peregrine falcon", "Golden eagle", "Spur-winged goose", "Anna's hummingbird")

m 必须有 Monad 实例，这一事实这意味着可以使用 >>= 和 pure 运算符。

通用的单子运算符

由于许多不同类型都是单子，因此对任何单子多态的函数非常强大。例如，函数 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

(15, [0, 1, 3, 6, 10])

可以使用 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]

{ log := [2, 4], val := [1, 2, 3, 4, 5] }

恒等单子

单子将具有效应(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]

[2, 3, 4, 5, 6]

省略提示则会导致错误：

#eval mapM (· + 1) [1, 2, 3, 4, 5]

failed to synthesize instance
  HAdd Nat Nat (?m.9063 ?m.9065)

导致错误的原因是：一个元变量应用于另一个元变量，使得Lean不会反向运行类型计算。函数的返回类型应该是应用于其他类型参数的单子。类似地，将 mapM 和未提供任何特定单子类型信息的函数一起使用，会导致"instance problem stuck"错误：

#eval mapM (fun x => x) [1, 2, 3, 4, 5]

typeclass instance problem is stuck, it is often due to metavariables
  Monad ?m.9063

单子约定

正如 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满足的结合律则意味着先计算哪一部分无关紧要，只要保证效应的顺序不变即可。

练习

映射一棵树

定义函数BinTree.mapM。通过类比列表的mapM，此函数应将单子函数应用于树中的每个节点，作为前序遍历。类型签名应为：

def BinTree.mapM [Monad m] (f : α → m β) : BinTree α → m (BinTree β)

Option单子的约定

首先充分论证 Option 的 Monad 实例满足单子约定。然后，考虑以下实例：

instance : Monad Option where
  pure x := some x
  bind opt next := none

这两个方法都有正确的类型。但这个实例却违反了单子约定，为什么？

Lean 函数式编程