8.2. モナドの持ち上げ（Lifting Monads）

あるモナドが別のモナドに対して最低限同等の能力を持つとき、後者のモナドからのアクションは前者のモナドからのアクションを期待するコンテキストで使うことができます。これはあるモナドから別のモナドへのアクションの 持ち上げ （lift）と呼ばれます。Lean は可能な場合は自動で持ち上げを挿入します；持ち上げは MonadLift 型クラスで定義されます。モナドの自動持ち上げは一般的な coercion メカニズムの前に試行されます。

🔗type class
MonadLift.{u, v, w}
    (m : semiOutParam (Type u → Type v))
    (n : Type u → Type w)
    : Type (max (max (u + 1) v) w)

A function for lifting a computation from an inner Monad to an outer Monad. Like Haskell's MonadTrans, but n does not have to be a monad transformer. Alternatively, an implementation of MonadLayer without layerInvmap (so far).

Instance Constructor

MonadLift.mk.{u, v, w}

Methods

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

Lifts a value from monad m into monad n.

モナド間の 持ち上げ は反射的かつ推移的です：

  • どのモナドもそれ自身のアクションを実行することができます。

  • m から m' への持ち上げ、および m' から n への持ち上げは m n への持ち上げを生成するために合成することができます。 ユーティリティの型クラス MonadLiftT は MonadLift インスタンスの反射的かつ推移的な閉包によって持ち上げを構築します。ユーザは MonadLiftT のインスタンスを新たに定義すべきではありませんが、ユーザが提供するモナドの複数のモナドからアクションを実行する必要がある多相関数のインスタンス暗黙パラメータとして便利です。

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

The reflexive-transitive closure of MonadLift. monadLift is used to transitively lift monadic computations such as StateT.get or StateT.put s. Corresponds to Haskell's MonadLift.

Instance Constructor

MonadLiftT.mk.{u, v, w}

Methods

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

Lifts a value from monad m into monad 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 α 型であり、2つの型が definitionally equal ではない場合、Lean はエラーを報告する前に持ち上げと強制の挿入を試みます。これには以下の可能性があります：

  1. m と n が同じモナドに単一化できる場合、 α と β は同じではありません。この場合、モナドの持ち上げは必要ありませんが、モナド内の値は coerce されなければなりません。適切な強制が見つかった場合、 Lean.Internal.coeM の呼び出しが挿入されます：

    Lean.Internal.coeM.{u, v} {m : Type u → Type v} {α β : Type u} [(a : α) → CoeT α a β] [Monad m] (x : m α) : m β

  1. α と β が単一化できる場合、モナドが異なります。この場合、 m α 型の式を n α 型に変換するにはモナドの持ち上げが必要です。 m が n に持ち上げられる場合（つまり MonadLiftT m n のインスタンスがある場合）、 MonadLiftT.monadLift のエイリアスである liftM の呼び出しが挿入されます。

    liftM.{u, v, w} {m : Type u → Type v} {n : Type u → Type w} [self : MonadLiftT m n] {α : Type u} : m α → n α

  1. 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 ・強制が展開されます。

IO モナドの持ち上げ

MonadLift BaseIO IO のインスタンスがあるため、IO でも BaseIO アクションを実行することができます：

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 α
変換されたモナドの持ち上げ

また、標準ライブラリの モナド変換子 のほとんどに MonadLift インスタンスがあるため、ベースとなるモナドアクションを追加作業無しに変換されたモナドで使用することができます。例えば、状態モナドアクションは、リーダと例外の変換を横断して持ち上げることができるため、互換性のあるモナドを自由に混在させることができます：

def declaration uses 'sorry'incrBy (n : Nat) : StateM Nat Unit := modify (def incrOrFail : ReaderT Nat (ExceptT String (StateM Nat)) Unit := do if (← read) > 5 then throw "Too much!" incrBy (← read)

持ち上げを無効にすると、このコードは機能しなくなります：

set_option autoLift false def declaration uses 'sorry'incrBy (n : Nat) : StateM Nat Unit := modify (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 : Type but is expected to have type ReaderT Nat (ExceptT String (StateM Nat)) Unit : TypeincrBy (← read)

autoLift を false に設定することで自動持ち上げを無効にすることができます。

🔗option
autoLift

Default value: true

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

8.2.1. 持ち上げの引き下げ（Reversing Lifts）

モナドの結合において、モナドの持ち上げだけでは必ずしも十分ではありません。モナドによって提供される多くの操作は高階であり、 同じモナド内の アクションをパラメータとして取ります。これらの操作がより強力なモナドに持ち上げられたとしても、その引数はもとのモナドに制限されます。

このような「持ち上げの引き下げ」をサポートする型クラスが2つあります： MonadFunctor と MonadControl です。 MonadFunctor m n のインスタンスは、 m の完全な多相関数を n として解釈する方法を説明します。この多相関数は α として すべて の型に対して機能しなければなりません：これは {α : Type u} → m α → m α という型を持ちます。このような関数は、作用を持つかもしれないが、与えられた特定の値に基づいて作用を持つことはできない関数として考えることができます。 MonadControl m n のインスタンスは m から n への任意のアクションを解釈する方法を説明すると同時に、 m アクションが n アクションを実行できるようにする「逆インタプリタ」を提供します。

8.2.1.1. モナド関手（Monad Functors）

🔗type class
MonadFunctor.{u, v, w}
    (m : semiOutParam (Type u → Type v))
    (n : Type u → Type w)
    : Type (max (max (u + 1) v) w)

A functor in the category of monads. Can be used to lift monad-transforming functions. Based on MFunctor from the pipes Haskell package, but not restricted to monad transformers. Alternatively, an implementation of MonadTransFunctor.

Instance Constructor

MonadFunctor.mk.{u, v, w}

Methods

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

Lifts a monad morphism f : {β : Type u} → m β → m β to monadMap f : {α : Type u} → n α → n α.

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

The reflexive-transitive closure of MonadFunctor. monadMap is used to transitively lift Monad morphisms.

Instance Constructor

MonadFunctorT.mk.{u, v, w}

Methods

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

Lifts a monad morphism f : {β : Type u} → m β → m β to monadMap f : {α : Type u} → n α → n α.

8.2.1.2. MonadControl による持ち上げの引き下げ（Reversible Lifting with 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 is a way of stating that the monad m can be 'run inside' the monad n.

This is the same as MonadBaseControl in Haskell. To learn about MonadControl, see the comment above this docstring.

Instance Constructor

MonadControl.mk.{u, v, w}

Methods

stM : Type u → Type u
liftWith : {α : Type u} → (({β : Type u} → n β → m (MonadControl.stM m n β)) → m α) → n α
restoreM : {α : Type u} → m (MonadControl.stM m n α) → n α
🔗type class
MonadControlT.{u, v, w} (m : Type u → Type v)
    (n : Type u → Type w)
    : Type (max (max (u + 1) v) w)

Transitive closure of MonadControl.

Instance Constructor

MonadControlT.mk.{u, v, w}

Methods

stM : Type u → Type u
liftWith : {α : Type u} → (({β : Type u} → n β → m (stM m n β)) → m α) → n α
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 α
🔗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 α
例外と持ち上げ

一例として 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 MonadStateOf (Array UInt8) (Except String) Additional diagnostic information may be available using the `set_option diagnostics true` command.modifyThe (Array UInt8) (·.push b)) fun e => failed to synthesize MonadStateOf (Array String) (Except String) Additional diagnostic information may be available using the `set_option diagnostics true` command.modifyThe (Array String) (·.push e)) 
failed to synthesize
  MonadStateOf (Array String) (Except String)
Additional diagnostic information may be available using the `set_option diagnostics true` command.

StateT は MonadControl インスタンスを持つため、 liftM の代わりに control を使用することができます。これは内側のアクションに外側のモナドのインタプリタを提供します。 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)) 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])