总结

组合单子

在从头开始编写单子时，有一些设计模式倾向于描述将每种作用添加到单子中的方式。读取器作用是通过让单子的类型成为读取器环境中的一个函数来添加的，状态作用是通过包含一个从初始状态到与最终状态配对的值的函数来添加的，失败或异常是通过在返回类型中包含一个和类型来添加的，日志或其他输出是通过在返回类型中包含一个积类型来添加的。现有的单子也可以成为返回类型的一部分，从而将其作用包含在新的单子中。

这些设计模式通过定义单子转换器（Monad transformers），将某种作用添加到某个基本单子中，从而形成一个可重复使用的软件组件库。单子转换器以较简单的单子类型为参数，返回增强的单子类型。单子转换器至少应提供以下实例：

假定内部类型已经是一个单子的 Monad 实例
一个 MonadLift 实例，用于将作用从内部单子转换到转换后的单子中

单子转换器可以多态结构或归纳数据类型的形式实现，但最常见的形式是从底层单子类型到增强单子类型的函数。

作用的类型类

一种常见的设计模式是，通过定义一个具有特定作用的单子、一个将作用添加到另一个单子的单子转换器，以及一个为作用提供通用接口的类型类，来实现特定的作用。这样编写的程序只需指定所需的作用，因此调用者可以提供任何具有合适作用的单子。

有时，辅助类型信息（如提供状态的单子中的状态类型，或提供异常的单子中的异常类型）是输出参数，有时则不是。输出参数对于每种作用只使用一次的简单程序最有用，但当给定程序中使用同一作用的多个实例时，类型检查器有可能过早提交错误的类型。因此，通常会提供两种版本（的类型类），普通参数版本的类型类名称以 -Of 结尾。

单子转换器不可交换

需要注意的是，改变单子中转换器的顺序会改变使用该单子的程序的含义。例如，对 StateT 和 ExceptT 重新排序可能导致程序在抛出异常时丢失状态修改，也可能导致程序保持变化。虽然大多数命令式语言只提供了后者，但单子转换器所提供的更大灵活性要求我们深思熟虑，为手头的任务选择正确的转换器。

单子转换器的 `do`-标记

Lean 的 do 代码块支持提前返回（代码块以某个值结束）、局部可变变量、带有 break 和 continue 的 for 循环，以及单分支的 if 语句。虽然这看似引入了命令式特性，会妨碍使用 Lean 编写证明，但实际上它只不过是为单子转换器的某些常见用法提供了一种更方便的语法。在幕后，do 代码块所使用的单子会通过适当使用 ExceptT 和 StateT 进行转换，以支持这些附加作用。