技术文章演示如何在 Lean 编程语言中使用 monad

这篇文章演示如何在 Lean 编程语言（具体来说是 Lean 4）中使用 monad。如果你不熟悉 Lean，这门语言的这一部分与其他函数式编程语言（如 Haskell 或 OCaml）非常相似。

假设我们要写一个简单的数值表达式求值器，支持数字的加法和除法： inductive Expr where | num : Int → Expr | add : Expr → Expr → Expr | div : Expr → Expr → Expr

遇到除零时会发生什么？我们希望求值器将其报告为失败，这可以用 Option 类型显式表示： def safeDiv (x y : Int) : Option Int := if y == 0 then none else some (x / y)

有了这个，eval 函数可以写成如下形式： def eval : Expr → Option Int | .num n => some n | .add a b => match eval a with | none => none | some x => match eval b with | none => none | some y => some (x + y) | .div a b => match eval a with | none => none | some x => match eval b with | none => none | some y => safeDiv x y

safeDiv 返回一个 Option；为了把可能出现的失败传播给调用者，eval 也返回 Option，而且——此外——还必须对可能出现 none 值的情况做大量繁琐的检查。有没有更好的办法？

注意这里重复出现的一种常见代码模式： 我们可以把它提取成一个辅助函数： def withSome (result : Option α) (onSuccess : α → Option β) : Option β := match result with | none => none | some x => onSuccess x

然后用这个辅助函数重写 eval： def evalWithSome : Expr → Option Int | .num n => some n | .add a b => withSome (evalWithSome a) (fun x => withSome (evalWithSome b) (fun y => some (x + y))) | .div a b => withSome (evalWithSome a) (fun x => withSome (evalWithSome b) (fun y => safeDiv x y))

这已经好多了；我们还可以用运算符重载让它更简洁： infixl:55 " >>? " => withSome

def evalOp : Expr → Option Int | .num n => some n | .add a b => evalOp a >>? fun x => evalOp b >>? fun y => some (x + y) | .div a b => evalOp a >>? fun x => evalOp b >>? fun y => safeDiv x y

恭喜——我们基本上已经发明了 monad！

简化形式下，Lean 中的 Monad 类型类定义如下： class Monad (m : Type → Type) where pure : α → m α bind : m α → (α → m β) → m β

在我们的代码中，pure 等价于 some，bind 等价于 withSome；事实上，Option 的 Monad 实例大致是这样的： instance : Monad Option where pure x := some x bind opt next := match opt with | none => none | some x => next x

Lean 中已经定义了一个类似 >>? 的 monad 运算符；它叫做 >>=，会采用 Monad 类型类的 bind 方法。因此我们可以用标准的 Monad 实例重写求值器，而不必定义 withSome 或 >>? 运算符 [1]： def evalBind : Expr → Option Int | .num n => pure n | .add a b => evalBind a >>= fun x => evalBind b >>= fun y => some (x + y) | .div a b => evalBind a >>= fun x => evalBind b >>= fun y => safeDiv x y

我们还可以进一步使用 do 记法，它是围绕 >>= 的语法糖，让我们可以把求值器重写成： def evalDo : Expr → Option Int | .num n => pure n | .add a b => do let x ← evalDo a let y ← evalDo b some (x + y) | .div a b => do let x ← evalDo a let y ← evalDo b safeDiv x y

如果你看过处理 I/O 的 Lean 代码，这种记法应该很熟悉；我们稍后会在文章中重新讨论 I/O。

函数式编程语言非常强调无副作用的纯函数。毫无疑问，这类函数更容易推理、调试，甚至更容易优化（通过记忆化）。话虽如此，现实世界是混乱的，有时副作用不可避免；monad 帮助在函数式程序中封装副作用。

核心思想是：副作用被封装在 Monad 内部，Monad 包装了计算返回的值。bind 方法（或等价的 >>= 运算符）让我们可以取出一个被包装的值，并将其推入序列中的下一个计算。如果你熟悉续延传递风格（CPS），这可能看起来很眼熟。续延本身也可以用 monad 建模 [2]。 bind : m α → (α → m β) → m β

这里有一个心智模型可以帮助理解： 将多个 bind 链接在一起，本质上就是一系列计算，同时跟踪副作用。monad 将计算做什么与它们如何被排序解耦。程序员描述计算的顺序及其依赖关系，而 monad 的 bind 实现则负责组合其副作用所需的簿记工作。

我们的求值器案例研究展示了副作用的一个例子：以 none 值从计算中提前返回。

让我们看看另一种惯用的做法，使用 Except 类型，它包含一个成功结果或一个错误值（与 Rust 中的 Result 类型非常相似）。

我们首先写一个返回异常的 safeDiv 版本： def safeDivExc (x y : Int) : Except String Int := if y == 0 then .error "division by zero" else .ok (x / y)

与其为 Except 编写一个全新的 eval 变体，我们将创建一个适用于任何 Monad 的通用版本 [3]： def evalM {m : Type → Type} [Monad m] (div : Int → Int → m Int) : Expr → m Int | .num n => pure n | .add a b => do let x ← evalM div a let y ← evalM div b pure (x + y) | .div a b => do let x ← evalM div a let y ← evalM div b div x y

现在 evalM 可以与 safeDivExc 一起使用，实现一个除法返回 Except 的求值器；与 safeDiv 一起使用时，它将等价于我们之前编写的 Option 专用 evalDo。 #eval evalM safeDiv (.add (.num 4) (.div (.num 6) (.num 0))) #eval evalM safeDivExc (.add (.num 4) (.div (.num 6) (.num 0)))

记录计算——writer monad 的一个例子 让我们看一个更高级的例子：一个求值器，它还将执行的计算记录在一个线性的字符串日志中。这里的挑战在于

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）