18.2. 提升单子🔗

当一个 monad 至少与另一个 monad 一样有能力时，则后一个 monad 的操作可以在期望前一个 monad 操作的上下文中使用。这称为 lifting 从一个单子到另一个单子的动作。 Lean 在电梯可用时自动插入电梯；电梯在 MonadLift 类型类别中定义。在通用强制机制之前尝试自动 monad 提升。

type class

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)

Computations in the monad m can be run in the monad n. These translations are inserted automatically by the compiler.

Usually, n consists of some number of monad transformers applied to m, but this is not mandatory.

New instances should use this class, MonadLift. Clients that require one monad to be liftable into another should instead request MonadLiftT, which is the reflexive, transitive closure of MonadLift.

Instance Constructor

MonadLift.mk.{u, v, w}

Methods

monadLift : {α : Type u} → m α → n α

Translates an action from monad m into monad n.

Lifting 在单子之间是自反和及物的：

任何 monad 都可以运行自己的操作。
从 m 到 m' 以及从 m' 到 n 的提升可以组合起来产生从 m 到 n 的提升。实用程序类型类 MonadLiftT 通过 MonadLift 实例的自反和传递闭包构造提升。用户不应定义 MonadLiftT 的新实例，但它可用作需要在某些用户提供的 monad 中从多个 monad 运行操作的多态函数的实例隐式参数。

type class

MonadLiftT.{u, v, w} (m : Type u → Type v) (n : Type u → Type w) :
  Type (max (max (u + 1) v) w)
MonadLiftT.{u, v, w} (m : Type u → Type v)
  (n : Type u → Type w) :
  Type (max (max (u + 1) v) w)

Computations in the monad m can be run in the monad n. These translations are inserted automatically by the compiler.

Usually, n consists of some number of monad transformers applied to m, but this is not mandatory.

This is the reflexive, transitive closure of MonadLift. Clients that require one monad to be liftable into another should request an instance of MonadLiftT. New instances should instead be defined for MonadLift itself.

Instance Constructor

MonadLiftT.mk.{u, v, w}

Methods

monadLift : {α : Type u} → m α → n α

Translates an action from monad m into monad n.

Monad Lifts in Function Signatures

函数 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 中，所以它可以在许多 monad 中使用，并且主体不需要将自身限制为 IO。实例隐式参数 MonadLiftT BaseIO m 允许使用 MonadLift 的自反传递闭包来组装电梯。

当需要 n β 类型的术语，但提供的术语具有 m α 类型，并且这两种类型在定义上不相等时，Lean 会在报告错误之前尝试插入提升和强制转换。有以下几种可能：

如果m和n可以统一为同一个monad，那么α和β就不相同。在这种情况下，不需要 monad 提升，但 monad 中的值必须是强制。如果找到适当的强制，则会插入对 Lean.Internal.coeM 的调用，该调用具有以下签名：
Lean.Internal.coeM.{u, v} {m : Type u → Type v} {α β : Type u} [(a : α) → CoeT α a β] [Monad m] (x : m α) : m β
如果 α 和 β 可以统一，则 monad 不同。在这种情况下，需要使用 monad lift 将类型为 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 是实现细节，而不是公共 API 的一部分。在结果项中，Lean.Internal.coeM、Lean.Internal.liftCoeM 和强制的出现被展开。

Lifting IO Monads

有一个 MonadLift BaseIO IO 的实例，因此任何 BaseIO 操作也可以在 IO 中运行：

def fromBaseIO (act : BaseIO α) : IO α := act

在幕后插入 liftM：

fun {α} act => liftM act : {α : Type} → BaseIO α → EIO IO.Error α#check fun {α} (act : BaseIO α) => (act : IO α)

fun {α} act => liftM act : {α : Type} → BaseIO α → EIO IO.Error α

Live ↪

Lifting Transformed Monads

大多数标准库的 monad 转换器也有 MonadLift 的实例，因此基本 monad 操作可以在转换后的 monad 中使用，无需额外工作。例如，状态 monad 操作可以在读取器和异常转换器之间提升，从而允许兼容的 monad 自由混合：

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!"
  Type mismatch
  incrBy __do_lift✝
has type
  StateM Nat Unit
but is expected to have type
  ReaderT Nat (ExceptT String (StateM Nat)) UnitincrBy (← read)

Type mismatch
  incrBy __do_lift✝
has type
  StateM Nat Unit
but is expected to have type
  ReaderT Nat (ExceptT String (StateM Nat)) Unit

通过将 autoLift 设置为 false 可以禁用自动提升。

option

autoLift

Default value: true

Insert monadic lifts (i.e., liftM and coercions) when needed.

18.2.1. 倒车升降机🔗

Monad 提升并不总是足以组合 monad。 monad 提供的许多操作都是高阶的，在同一个 monad 中采取操作作为参数。即使这些操作被提升到一些更强大的 monad，它们的参数仍然仅限于原始 monad。

有两个类型类支持这种“反向提升”：MonadFunctor 和 MonadControl。 MonadFunctor m n 的实例解释了如何将 m 中的完全多态函数解释为 n。此多态函数必须适用于所有类型 α：它的类型为 {α : Type u} → m α → n α。这样的函数可以被认为是一个可能有效果的函数，但不能根据提供的特定值来实现这一点。 MonadControl m n 的实例解释了如何将 m 的任意操作解释为 n，同时提供允许 m 操作运行 n 操作的“反向解释器”。

18.2.1.1. 单子函子🔗

type class

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)

A way to interpret a fully-polymorphic function in m into n. Such a function can be thought of as one that may change the effects in m, but can't do so based on specific values that are provided.

Clients of MonadFunctor should typically use MonadFunctorT, which is the reflexive, transitive closure of MonadFunctor. New instances should be defined for MonadFunctor.

Instance Constructor

MonadFunctor.mk.{u, v, w}

Methods

monadMap : {α : Type u} → ({β : Type u} → m β → m β) → n α → n α

Lifts a fully-polymorphic transformation of m into n.

type class

MonadFunctorT.{u, v, w} (m : Type u → Type v) (n : Type u → Type w) :
  Type (max (max (u + 1) v) w)
MonadFunctorT.{u, v, w}
  (m : Type u → Type v)
  (n : Type u → Type w) :
  Type (max (max (u + 1) v) w)

This is the reflexive, transitive closure of MonadFunctor. It automatically chains together MonadFunctor instances as needed. Clients of MonadFunctor should typically use MonadFunctorT, but new instances should be defined for MonadFunctor.

Instance Constructor

MonadFunctorT.mk.{u, v, w}

Methods

monadMap : {α : Type u} → ({β : Type u} → m β → m β) → n α → n α

Lifts a fully-polymorphic transformation of m into n.

18.2.1.2. 使用 `MonadControl` 进行可逆提升🔗

type class

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)

A way to lift a computation from one monad to another while providing the lifted computation with a means of interpreting computations from the outer monad. This provides a means of lifting higher-order operations automatically.

Clients should typically use control or controlAt, which request an instance of MonadControlT: the reflexive, transitive closure of MonadControl. New instances should be defined for MonadControl itself.

Instance Constructor

MonadControl.mk.{u, v, w}

Methods

stM : Type u → Type u

A type that can be used to reconstruct both a returned value and any state used by the outer monad.

liftWith : {α : Type u} → (({β : Type u} → n β → m (MonadControl.stM m n β)) → m α) → n α

Lifts an action from the inner monad m to the outer monad n. The inner monad has access to a reverse lifting operator that can run an n action, returning a value and state together.

restoreM : {α : Type u} → m (MonadControl.stM m n α) → n α

Lifts a monadic action that returns a state and a value in the inner monad to an action in the outer monad. The extra state information is used to restore the results of effects from the reverse lift passed to liftWith's parameter.

type class

MonadControlT.{u, v, w} (m : Type u → Type v) (n : Type u → Type w) :
  Type (max (max (u + 1) v) w)
MonadControlT.{u, v, w}
  (m : Type u → Type v)
  (n : Type u → Type w) :
  Type (max (max (u + 1) v) w)

Instance Constructor

MonadControlT.mk.{u, v, w}

Methods

stM : Type u → Type u

A type that can be used to reconstruct both a returned value and any state used by the outer monad.

liftWith : {α : Type u} → (({β : Type u} → n β → m (stM m n β)) → m α) → n α

Lifts an action from the inner monad m to the outer monad n. The inner monad has access to a reverse lifting operator that can run an n action, returning a value and state together.

restoreM : {α : Type u} → stM m n α → n α

def

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 α

Lifts an operation from an inner monad to an outer monad, providing it with a reverse lifting operator that allows outer monad computations to be run in the inner monad. The lifted operation is required to return extra information that is required in order to reconstruct the reverse lift's effects in the outer monad; this extra information is determined by stM.

This function takes the inner monad as an implicit parameter. Use controlAt to specify it explicitly.

def

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 α

This function takes the inner monad as an explicit parameter. Use control to infer the monad.

Exceptions and Lifting

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 ()

Except.ok #[1, 58, 255, 2]#eval getBytes #[1, 58, 255, 300, 2, 1000000] |>.run #[] |>.map (·.2)

Except.ok #[1, 58, 255, 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 =>
         failed to synthesize instance of type class
  MonadStateOf (Array UInt8) (Except String)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.modifyThe (Array UInt8) (·.push b))
        fun e =>
          failed to synthesize instance of type class
  MonadStateOf (Array String) (Except String)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.modifyThe (Array String) (·.push e))

failed to synthesize instance of type class
  MonadStateOf (Array String) (Except String)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

由于 StateT 具有 MonadControl 实例，因此可以使用 control 代替 liftM。它为内部动作提供了外部单子的解释器。对于 StateT，该解释器期望内部 monad 返回一个包含更新状态的元组，并负责提供初始状态并从元组中提取更新状态。

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))

Except.ok (#["Out of range: 300", "Out of range: 1000000"], #[1, 58, 255, 2])#eval
  getBytes' #[1, 58, 255, 300, 2, 1000000]
  |>.run #[] |>.run #[]
  |>.map (fun (((), bytes), errs) => (bytes, errs))

Except.ok (#["Out of range: 300", "Out of range: 1000000"], #[1, 58, 255, 2])

Live ↪

18.1.	法律
18.2.	提升单子
18.3.	句法
18.4.	API 参考
18.5.	单子的种类

18.2. 提升单子🔗

Instance Constructor

Methods

Instance Constructor

Methods

18.2.1. 倒车升降机🔗

18.2.1.1. 单子函子🔗

Instance Constructor

Methods

Instance Constructor

Methods

18.2.1.2. 使用 MonadControl 进行可逆提升🔗

Instance Constructor

Methods

Instance Constructor

Methods

18.2.1.2. 使用 `MonadControl` 进行可逆提升🔗