Newshot 这篇文章演示如何在 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 值进行大量繁琐的检查。有没有更好的办法？
注意这里重复出现的一个常见代码模式：
- 检查 Option 的值
- 如果它是 none，则返回 none 而不继续执行
- 否则如果它是 some result，则用 result 继续计算
我们可以把它提取成一个辅助函数：
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！
表达式求值中作为 Monad 的 Option
简化形式下，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 内部，Monad 包裹了计算返回的值。bind 方法（或等价的 >>= 运算符）让我们可以取出一个被包裹的值，并将其推入序列中的下一个计算。这在延续传递风格（CPS）中可能看起来很熟悉。延续本身也可以用 monad 来建模 [2]。
bind 的定义是：
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 的一个例子
让我们看一个更高级的例子：一个求值器，它还将执行的计算记录在一个线性的字符串日志中。这里的挑战在于，我们仍然必须将其与 Option 结合以支持除零的情况，因此我们首先创建一个新的结构来携带计算的状态：
structure LoggedOption (α : Type) where
value : Option α
log : List String
这将是一次 eval 调用的结果；它产生一个可选值，以及一个字符串列表（日志）。以下是该类型的 Monad 实现：
instance : Monad LoggedOption where
pure x := ⟨some x, []⟩
bind v next :=
match v.value with
| none => ⟨none, v.log⟩
| some x =>
let nextResult := next x
⟨nextResult.value, v.log ++ nextResult.log⟩
主要思想是通过追加的方式将存储的日志与下一个计算的日志合并（从而累积一个线性日志）。以下是我们的求值器：
def evalLogged : Expr → LoggedOption Int
| .num n => pure n
| .add a b => do
let x ← evalLogged a
let y ← evalLogged b
⟨some (x + y), [s!"adding {x} and {y}"]⟩
| .div a b => do
let x ← evalLogged a
let y ← evalLogged b
match y with
| 0 => ⟨none, [s!"dividing {x} by zero"]⟩
| _ => ⟨some (x / y), [s!"dividing {x} by {y}"]⟩
注意 evalLogged 的代码不必过多处理日志记录的具体机制（除了添加新的日志条目之外）。所有这些都隐藏在 monad 实例内部。LoggedOption 是 writer monad 的一个例子，它是 state monad 的只写版本。
State monad
monad 在函数式编程语言中最重要的用例之一，是通过计算来建模可变状态。
有状态的计算被建模为一个函数：它接收初始状态，并返回一个元组，其中包含结果值和一个新的、更新后的状态。用 Lean 的记法表示：
def State (σ : Type) (α : Type) : Type :=
σ → (α × σ)
为了演示它的实际用法，我们来增强求值器，使其支持变量赋值和查找。我们的状态将是一个由名称和值组成的关联列表：
abbrev Vars := List (String × Int)
并且我们会为表达式枚举增加额外的操作：
inductive ExprV where
| num : Int → ExprV
| add : ExprV → ExprV → ExprV
| div : ExprV → ExprV → ExprV
| store : String → ExprV → ExprV
| load : String → ExprV
这将是我们的 state monad：
structure EvalM (α : Type) where
run : Vars → Option (α × Vars)
注意 run 函数与上面 State 签名之间的对应关系：
- 它接收当前状态，在我们的用例中，这个状态是一个关联列表，保存所有已定义变量的值。
- 它返回一个可选结果，该结果是某个值（在我们的例子中，是计算的结果）和一个更新后的状态组成的对。
这是它的 Monad 类实现：
instance : Monad EvalM where
pure x := ⟨fun vars => some (x, vars)⟩
bind action next := ⟨fun vars =>
match action.run vars with
| none => none
| some (x, vars') => (next x).run vars'⟩
最后是求值器：
def evalState : ExprV → EvalM Int
| .num n => pure n
| .add a b => do
let x ← evalState a
let y ← evalState b
pure (x + y)
| .div a b => do
let x ← evalState a
let y ← evalState b
⟨fun vars => (safeDiv x y).map (fun value => (value, vars))⟩
| .load name =>
⟨fun vars => do
let value ← vars.lookup name
pure (value, vars)⟩
| .store name rhs => do
let value ← evalState rhs
⟨fun vars =>
let vars' := (name, value) :: vars.filter (fun p => p.1 != name)
some (value, vars')⟩
不直接处理变量的操作（如 .num 和 .add）像之前一样完成自己的工作。.div 只需处理实际的 monad 类型，以确保在除零时传播 none。还要注意，这个求值器支持将 store 作为表达式，因为它们分别返回一个值和更新后的状态；因此，像下面这样的计算可以正常工作：
-- (x := 12) + (x / 3): the right operand sees the left operand's assignment.
#eval (evalState
(.add (.store "x" (.num 12))
(.div (.load "x") (.num 3)))).run []
产生结果 some (16, [("x", 12)])。
在具有可变状态的语言中，建模副作用很容易——只需赋值某个状态（例如结构体字段或类成员）。然而，在像 Lean 这样的函数式语言中，我们必须显式地在计算之间携带这个状态；monad 帮助我们优雅地做到这一点——通过隐藏实际携带状态的大部分机制，大部分代码得以免于簿记工作。
IO monad
文章标题：Lean 中的 Monad
正文： 在 Lean 和 Haskell 这类函数式编程语言中，最广为人知的 monad 例子大概就是 IO。任何写过与外部世界交互的“真正”程序的人，对 IO 都非常熟悉。下面是一个定制的“Hello”程序，通常是学习一门新编程语言前 15 分钟就会教的内容：
def greet : IO Unit := do
let stdin ← IO.getStdin
IO.println "What is your name?"
let name ← stdin.getLine
IO.println s!"Hello, {name}"
注意这里的 do 记法，它暗示了 monad 的存在。如前所述，do 是 monad 的 bind 方法（即 >>= 运算符）的语法糖；我们可以把这段代码更显式地重写为：
def greetBind : IO Unit :=
IO.getStdin >>= fun stdin =>
IO.println "What is your name?" >>= fun _ =>
stdin.getLine >>= fun name =>
IO.println s!"Hello, {name}"
本质上，IO 是一个 state monad，其中被携带的状态代表“外部世界”。像 println 这样的 IO 操作作用于这个世界，而它的状态通过 bind 传递下去，和其他 state monad 一样。
下面是我们表达式求值器的一个版本，它直接把日志输出到标准输出，而不是把日志收集为字符串列表：
def evalIO : Expr → OptionT IO Int
| .num n => pure n
| .add a b => do
let x ← evalIO a
let y ← evalIO b
IO.println s!"adding {x} and {y}"
pure (x + y)
| .div a b => do
let x ← evalIO a
let y ← evalIO b
IO.println s!"dividing {x} by {y}"
OptionT.mk (pure (safeDiv x y))
这里唯一不寻常的构造是 OptionT，它是一个 monad transformer，帮助我们把 Option（用于传播安全除法产生的失败）与 IO Monad 组合起来 [4]。
IO monad 也支持 throw，以实现类似 Python 的异常行为，但在本例中我们显式使用 Option；异常是编程偏好问题，在像 eval 这样的库函数内部使用异常，我觉得并不合适。
Lean 中的 Monad 定律
和 Haskell 中一样，Lean 中的 monad 应当遵守某些定律。它们是：
左单位元：把一个值包装进 pure 并立即通过 bind 传给 f，应当等价于直接对值调用 f：
pure v >>= f = f v
右单位元：从一个计算中取出值并立即用 pure 重新包装，不应改变该计算：
m >>= pure = m
结合律：运算的分组方式无关紧要，只要它们的顺序保持不变：
(m >>= f) >>= g = m >>= (fun v => f v >>= g)
我们来看看 Option 如何遵守这些定律。
对于左单位元，pure v 是 some v，而 bind 的实现把 some x 匹配到 next x，这等价于 f v。
对于右单位元，m >>= pure 只是把 some 值重新包装进 pure，对 none 则保持不变——这等价于保持原样。
对于结合律，如果 m 是 none，那么两边都是 none。如果 m 是 some v，左边是 f v >>= g，右边也归约为同样的结果，因此它们同样等价。
虽然 Lean 并不强制要求 Monad 实例遵守这些定律，但它有一个单独的类型类 LawfulMonad，它确实要求提供 Lean 证明；这对 Lean 的主要用途很有用——通过其强大的类型系统表达并证明关于程序的定理。但这是另一个话题了。
如需评论，请给我发邮件。