当一个单子的能力至少与另一个单子相当时，后者的动作便可用于期望前者动作的上下文中。
这称为将动作从一个单子提升到另一个单子。
有可用的提升时，Lean 会自动插入它们；提升由类型类 MonadLift 定义。
自动单子提升会在通用的强制转换机制之前尝试。
MonadLift.{u, v, w} (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) : Type (max (max (u + 1) v) w)MonadLift.{u, v, w} (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) : Type (max (max (u + 1) v) w)
单子 m 中的计算可以在单子 n 中运行。编译器会自动插入这些转换。
通常，n 由若干单子变换器应用于 m 而成，但这不是强制要求。
新实例应使用此类型类 MonadLift。需要将一个单子提升到另一个单子的客户端则应请求
MonadLiftT；后者是 MonadLift 的自反传递闭包。
实例构造子
MonadLift.mk.{u, v, w}
方法
monadLift : {α : Type u} → m α → n α
将动作从单子 m 转换到单子 n。
单子之间的提升具有自反性和传递性：
任意单子都能运行自己的动作。
从 m 到 m' 的提升与从 m' 到 n 的提升可以复合，得到从 m 到 n 的提升。
辅助类型类 MonadLiftT 通过 MonadLift 实例的自反传递闭包构造提升。
用户不应定义新的 MonadLiftT 实例；不过，当多态函数需要在用户提供的某个单子中运行多个单子的动作时，它很适合作为该函数的实例隐式参数。
单子 m 中的计算可以在单子 n 中运行。编译器会自动插入这些转换。
通常，n 由若干单子变换器应用于 m 而成，但这不是强制要求。
这是 MonadLift 的自反传递闭包。需要将一个单子提升到另一个单子的客户端应请求
MonadLiftT 实例。新实例则应为 MonadLift 本身定义。
实例构造子
MonadLiftT.mk.{u, v, w}
方法
monadLift : {α : Type u} → m α → n α
将动作从单子 m 转换到单子 n。
函数 IO.withStdin 具有以下签名：
IO.withStdin.{u} {m : Type → Type u} {α : Type}
[Monad m] [MonadFinally m] [MonadLiftT BaseIO m]
(h : IO.FS.Stream) (x : m α) :
m α
由于它不要求参数严格位于 IO 中，因此可用于许多单子，其函数体也无需局限于 IO。
实例隐式参数 MonadLiftT BaseIO m 允许使用 MonadLift 的自反传递闭包来组装提升。
当期望类型为 n β 的项，但提供的项类型为 m α，且两种类型并非定义相等时，Lean 会先尝试插入提升和强制转换，再报告错误。
可能有以下几种情况：
如果 m 和 n 能统一为同一个单子，那么 α 和 β 并不相同。
此时不需要单子提升，但必须对单子中的值进行强制转换。
如果找到了适当的强制转换，就会插入对 Lean.Internal.coeM 的调用，其签名如下：
Lean.Internal.coeM.{u, v} {m : Type u → Type v} {α β : Type u}
[(a : α) → CoeT α a β] [Monad m]
(x : m α) :
m β
如果 α 和 β 可以统一，那么不同的是两个单子。
此时需要单子提升，将类型为 m α 的表达式变换为 n α。
如果 m 可以提升到 n（即存在 MonadLiftT m n 的实例），就会插入对 liftM 的调用；它是 MonadLiftT.monadLift 的别名。
liftM.{u, v, w}
{m : Type u → Type v} {n : Type u → Type w}
[self : MonadLiftT m n] {α : Type u} :
m α → n α
如果 m 与 n、α 与 β 都无法统一，但 m 可以提升到 n，且 α 可以强制转换为 β，那么可以组合一次提升与一次强制转换。
具体做法是插入对 Lean.Internal.liftCoeM 的调用：
Lean.Internal.liftCoeM.{u, v, w}
{m : Type u → Type v} {n : Type u → Type w}
{α β : Type u}
[MonadLiftT m n] [(a : α) → CoeT α a β] [Monad n]
(x : m α) :
n β
顾名思义，Lean.Internal.coeM 和 Lean.Internal.liftCoeM 属于实现细节，并非公共接口的一部分。
在最终生成的项中，出现的 Lean.Internal.coeM、Lean.Internal.liftCoeM 和强制转换都会被展开。
IO 单子
标准库的大多数单子变换器也有 MonadLift 实例，因此无需额外工作，便可在经过变换的单子中使用基础单子动作。
例如，状态单子动作可以跨越读取器变换器和异常变换器进行提升，从而自由混用兼容的单子：
def incrBy (n : Nat) : StateM Nat Unit := modify (· + n)
def incrOrFail : ReaderT Nat (ExceptT String (StateM Nat)) Unit := do
if (← read) > 5 then throw "Too much!"
incrBy (← read)
禁用提升会导致错误：
set_option autoLift false
def incrBy (n : Nat) : StateM Nat Unit := modify (. + n)
def incrOrFail : ReaderT Nat (ExceptT String (StateM Nat)) Unit := do
if (← read) > 5 then throw "Too much!"
incrBy (← read)
将选项 autoLift 设为 false 可以禁用自动提升。
单子提升并不总足以组合单子。 单子提供的许多操作都是高阶的，会接收同一个单子中的动作作为参数。 即使把这些操作提升到更强大的单子中，它们的实参仍受限于原单子。
有两个类型类支持这种“反向提升”：MonadFunctor 和 MonadControl。
MonadFunctor m n 的实例说明如何把 m 中的完全多态函数解释到 n 中。
这个多态函数必须适用于所有类型 α：其类型为 {α : Type u} → m α → n α。
可以认为这样的函数或许会产生效应，但不能依据所提供的具体值来产生效应。
MonadControl m n 的实例说明如何把 m 中的任意动作解释到 n 中，同时提供一个“反向解释器”，让该 m 动作能够运行 n 动作。
MonadFunctor.{u, v, w} (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) : Type (max (max (u + 1) v) w)MonadFunctor.{u, v, w} (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) : Type (max (max (u + 1) v) w)
一种将 m 中完全多态的函数解释到 n 中的方法。这样的函数可以被看作可能改变 m 中的
副作用，但不能根据所提供的具体值来改变副作用。
MonadFunctor 的客户端通常应使用 MonadFunctorT，后者是 MonadFunctor 的自反传递闭包。
新实例应为 MonadFunctor 定义。
实例构造子
MonadFunctor.mk.{u, v, w}
方法
monadMap : {α : Type u} → ({β : Type u} → m β → m β) → n α → n α
将 m 的完全多态变换提升到 n 中。
一种将 m 中完全多态的函数解释到 n 中的方法。这样的函数可以被看作可能改变 m 中的
副作用，但不能根据所提供的具体值来改变副作用。
这是 MonadFunctor 的自反传递闭包，会按需自动串接 MonadFunctor 实例。
MonadFunctor 的客户端通常应使用 MonadFunctorT，但新实例应为 MonadFunctor 定义。
实例构造子
MonadFunctorT.mk.{u, v, w}
方法
monadMap : {α : Type u} → ({β : Type u} → m β → m β) → n α → n α
将 m 的完全多态变换提升到 n 中。
MonadControl 进行可逆提升MonadControl.{u, v, w} (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) : Type (max (max (u + 1) v) w)MonadControl.{u, v, w} (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) : Type (max (max (u + 1) v) w)
一种将计算从一个单子提升到另一个单子的方法，同时为被提升的计算提供一种解释外层单子计算的 手段。这样便可自动提升高阶运算。
客户端通常应使用 control 或 controlAt，它们请求 MonadControlT 实例；后者是
MonadControl 的自反传递闭包。新实例应为 MonadControl 本身定义。
实例构造子
MonadControl.mk.{u, v, w}
方法
stM : Type u → Type u
可用于同时重建返回值及外层单子所用任何状态的类型。
liftWith : {α : Type u} → (({β : Type u} → n β → m (MonadControl.stM m n β)) → m α) → n α
将动作从内层单子 m 提升到外层单子 n。内层单子可以使用反向提升运算符来运行 n
动作，并一并返回值和状态。
restoreM : {α : Type u} → m (MonadControl.stM m n α) → n α
将内层单子中返回状态和值的单子动作提升为外层单子中的动作。额外状态信息用于恢复传给
liftWith 参数的反向提升所产生的副作用结果。
一种将计算从一个单子提升到另一个单子的方法，同时为被提升的计算提供一种解释外层单子计算的 手段。这样便可自动提升高阶运算。
客户端通常应使用 control 或 controlAt，它们请求 MonadControlT 实例；后者是
MonadControl 的自反传递闭包。新实例应为 MonadControl 本身定义。
实例构造子
MonadControlT.mk.{u, v, w}
control.{u, v, w} {m : Type u → Type v} {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u} (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n αcontrol.{u, v, w} {m : Type u → Type v} {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u} (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α
controlAt.{u, v, w} (m : Type u → Type v) {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u} (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n αcontrolAt.{u, v, w} (m : Type u → Type v) {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u} (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α
一个例子是 Except.tryCatch：
Except.tryCatch.{u, v} {ε : Type u} {α : Type v}
(ma : Except ε α) (handle : ε → Except ε α) :
Except ε α
它的两个参数都位于 Except ε 中。
MonadLift 可以提升处理器的整个应用。
函数 getBytes 使用状态和异常从 Nat 数组中提取各个字节；为了明确展示其结构，编写时没有使用 Lean.Parser.Term.do : termdo 记法或自动提升。
set_option autoLift false
def getByte (n : Nat) : Except String UInt8 :=
if n < 256 then
pure n.toUInt8
else throw s!"Out of range: {n}"
def getBytes (input : Array Nat) :
StateT (Array UInt8) (Except String) Unit := do
input.forM fun i =>
liftM (Except.tryCatch (some <$> getByte i) fun _ => pure none) >>=
fun
| some b => modify (·.push b)
| none => pure ()
#eval getBytes #[1, 58, 255, 300, 2, 1000000] |>.run #[] |>.map (·.2)
getBytes 使用提升后的动作所返回的 Option 来表示所需的状态更新。
如果对内部动作有多种响应方式，例如保存已处理的异常，这种做法很快就会变得难以驾驭。
理想情况下，应当直接在 tryCatch 调用内部执行状态更新。
然而，尝试保存字节和已处理的异常并不可行，因为 Except.tryCatch 的实参类型为 Except String Unit：
def getBytes' (input : Array Nat) :
StateT (Array String)
(StateT (Array UInt8)
(Except String)) Unit := do
input.forM fun i =>
liftM
(Except.tryCatch
(getByte i >>= fun b =>
modifyThe (Array UInt8) (·.push b))
fun e =>
modifyThe (Array String) (·.push e))
因为 StateT 有一个 MonadControl 实例，所以可以用 control 代替 liftM。
它为内部动作提供外部单子的解释器。
对于 StateT，该解释器期望内部单子返回一个包含更新后状态的元组，并负责提供初始状态以及从元组中提取更新后的状态。
def getBytes' (input : Array Nat) :
StateT (Array String)
(StateT (Array UInt8)
(Except String)) Unit := do
input.forM fun i =>
control fun run =>
(Except.tryCatch
(getByte i >>= fun b =>
run (modifyThe (Array UInt8) (·.push b))))
fun e =>
run (modifyThe (Array String) (·.push e))
#eval
getBytes' #[1, 58, 255, 300, 2, 1000000]
|>.run #[] |>.run #[]
|>.map (fun (((), bytes), errs) => (bytes, errs))