8.5. さまざまなモナド（Varieties of Monads）

IO モナドは非常に多くの作用を持ち、世界と相互作用する必要のあるプログラムを書くために用いられます。これについては専用の節で説明されています。 IO を使用するプログラムは本質的にブラックボックスです：これは大抵特に検証しやすいものではありません。

多くのアルゴリズムは、より小さな作用のセットで表現するほうが簡単です。例えば、可変状態はプログラムの値と状態の両方を含むタプルを渡すことでシミュレートできます。これらのシミュレートされた作用は言語のプリミティブではなく普通のコードを使って定義されるため、形式的に推論することが容易です。

標準ライブラリではよく使われる作用を扱うための抽象化が提供されています。よく使われる作用の多くはいくつかのカテゴリに分類されます：

可変状態を伴う状態モナド（state monad）: 計算中に変更される可能性のあるデータにアクセスできる計算では 可変状態 （mutable state）を使用します。状態モナドの節で説明されているように、状態はさまざまな方法で実装することができ、 MonadState 型クラスで捕捉されています。

パラメータ化された計算であるリーダモナド（reader monad）: コンテキストから提供されたパラメータの値を読み取ることができる計算はほとんどのプログラミング言語に存在しますが、状態と例外を第一級の機能として備えている多くの言語には新しいパラメータ化された計算を定義するための組み込み機能がありません。一般的に、これらの計算は呼び出された時にパラメータ値が提供され、ローカルでオーバーライドできることもあります。パラメータ値は 動的範囲 （dynamic extent）を持ちます：コールスタックで最も最近に提供された値が使用されます。パラメータ値は一連の関数呼び出しで変更されない値を渡すことでシミュレートできます；しかし、この技法はコードを読みにくくし、間違って次の呼び出しに間違った値を渡してしまう危険性があります。また状態の変更を慎重に規律することで可変状態を使ってパラメータ値をシミュレートすることもできます。パラメータを保持し、呼び出しスタックの位置でオーバーライドすることを可能にしたモナドは リーダモナド と呼ばれます。リーダモナドは MonadReader 型クラスで捕捉されています。さらに、パラメータ値をローカルでオーバーライドできるモナドは MonadWithReader 型クラスで捕捉されます。

例外を持つ例外モナド（exception monad）: 例外値で早期終了する可能性のある計算には例外（exception）を使用します。これは通常、正常終了のためのコンストラクタとエラーによる早期終了のためのコンストラクタの直和型によってモデル化されます。例外モナドは例外モナドの節で説明されており、 MonadExcept 型クラスで捕捉されます。

8.5.1. モナド型クラス（Monad Type Classes）

MonadState や MonadExcept のような型クラスを使うことでクライアントコードはモナドに対して多相的になります。自動持ち上げと合わせて、これはプログラムを多くの異なるモナドで再利用可能にし、リファクタリングに対してより堅牢にします。

モナド内の作用が1つの方法でしか相互作用しないとは限らない点に注意することが重要です。例えば、状態と例外を持つモナドは、例外が投げられた時に状態の変更をロールバックすることもあれば、しないこともあります。もしこれが関数の正しさにとって重要であれば、より特殊なシグネチャを使うべきです。

作用の順序

関数 sumNonFives は状態モナドを使用してリストの内容の足し算を行い、 5 に遭遇した場合、早期に終了します。

def sumNonFives {m}
    [Monad m] [MonadState Nat m] [MonadExcept String m]
    (xs : List Nat) :
    m Unit := do
  for x in xs do
    if x == 5 then
      throw "Five was encountered"
    else
      modify (· + x)

これを以下のモナドで実行すると 5 が発生した時点の状態が返されます：

(Except.error "Five was encountered", 10)#eval
  sumNonFives (m := ExceptT String (StateM Nat))
    [1, 2, 3, 4, 5, 6] |>.run |>.run 0

(Except.error "Five was encountered", 10)

別の以下のモナドでは、状態は破棄されます：

Except.error "Five was encountered"#eval
  sumNonFives (m := StateT Nat (Except String))
    [1, 2, 3, 4, 5, 6] |>.run 0

Except.error "Five was encountered"

2つ目のケースでは、例外ハンドラは状態を Lean.Parser.Term.termTry : termtry の開始時の値にロールバックします。したがって以下の関数は正しくありません：

/-- Computes the sum of the non-5 prefix of a list. -/
def sumUntilFive {m}
    [Monad m] [MonadState Nat m] [MonadExcept String m]
    (xs : List Nat) :
    m Nat := do
  MonadState.set 0
  try
    sumNonFives xs
  catch _ =>
    pure ()
  get

1つ目のモナドでは答えは正しくなります：

Except.ok 10#eval
  sumUntilFive (m := ExceptT String (StateM Nat))
    [1, 2, 3, 4, 5, 6] |>.run |>.run' 0

Except.ok 10

もう一つでは正しくなりません：

Except.ok 0#eval
  sumUntilFive (m := StateT Nat (Except String))
    [1, 2, 3, 4, 5, 6] |>.run' 0

Except.ok 0

1つのモナドが同じ作用の複数のバージョンをサポートすることがあります。例えば、可変な Nat と可変な String があったり、2つの別々のリーダのパラメータがあるかもしれません。それらの型が異なる限り、両方にアクセスできると便利でしょう。典型的な使用例では、型クラスでオーバーロードされるモナド演算の中には instance synthesis で型情報を利用できるものもあれば、そうでないものもあります。例えば、 set に渡される引数は使用する状態の型を決定しますが、 get ではそのような引数を取りません。 set のアプリケーションに存在する型情報は、複数の状態が利用可能な場合に正しいインスタンスを選択するために使用することができます。これはインスタンスを選択するために使用できるように、可変状態の型を入力パラメータまたは半出力パラメータにする必要があることを示唆しています。一方、 get の使用には型情報がないことから、可変状態の型は MonadState の出力パラメータであるべきであり、型クラス統合はモナド自体から状態の型を決定します。

この二律背反は、作用の型クラスの多くに2つのバージョンを持たせることで解決されます。半出力パラメータを持つバージョンの接尾辞は -Of で、その操作は必要に応じて明示的に型を取ります。例えば MonadStateOf ・ MonadReaderOf ・ MonadExceptOf などです。明示的な型パラメータを持つ操作は getThe ・ readThe ・ tryCatchThe などのように -The で終わる名前を持ちます。出力パラメータを持つバージョンの名前は装飾されません。標準ライブラリでは、典型的なユースケースで良い推論動作をするものに基づいて、各型クラスの -Of と装飾されていないバージョンの操作を混ぜてエクスポートしています。

演算	所有するクラス	注記
`get`	`MonadState`	出力パラメータによって型推論が改善します
`set`	`MonadStateOf`	半出力パラメータは `set` の引数の型情報を使用します
`modify`	`MonadState`	注釈の無い関数を許可するには、出力パラメータが必要です
`modifyGet`	`MonadState`	注釈の無い関数を許可するには、出力パラメータが必要です
`read`	`MonadReader`	引数の型情報がないため、出力パラメータが必要です
`readThe`	`MonadReaderOf`	半出力パラメータは提供された型を使用して統合を誘導します
`withReader`	`MonadWithReader`	出力パラメータによって関数の型注釈の必要性を回避しています
`withTheReader`	`MonadWithReaderOf`	半出力パラメータは提供された型を使用して統合を誘導します
`throw`	`MonadExcept`	出力パラメータによってコンストラクタのドット記法を例外のために使用できます
`throwThe`	`MonadExceptOf`	半出力パラメータは提供された型を使用して統合を誘導します
`tryCatch`	`MonadExcept`	出力パラメータによってコンストラクタのドット記法を例外のために使用できます
`tryCatchThe`	`MonadExceptOf`	半出力パラメータは提供された型を使用して統合を誘導します

状態の型

以下の状態モナド M は2つの別々の状態を持ちます： Nat と String です。

abbrev M := StateT Nat (StateM String)

get は MonadState.get のエイリアスであるため、状態の型は出力パラメータです。これは Lean が自動的に状態の型を選択することを意味し、この場合は一番外側のモナド変換子からのものとなります：

get : M Nat#check (get : M _)

get : M Nat

状態の型は出力パラメータであるため、一番外側のみを使用することができます。

#check (failed to synthesize
  MonadState String M
Additional diagnostic information may be available using the `set_option diagnostics true` command.get : M String)

failed to synthesize
  MonadState String M
Additional diagnostic information may be available using the `set_option diagnostics true` command.

MonadStateOf から getThe を使用して明示的に状態の型を提供することで、両方の状態を読むことができます。

(getThe String, getThe Nat) : M String × M Nat#check ((getThe String, getThe Nat) : M String × M Nat)

(getThe String, getThe Nat) : M String × M Nat

状態の型は MonadStateOf の半出力パラメータであるため、状態のセットはどちらの型でも機能します。

set 4 : M PUnit#check (set 4 : M Unit)

set 4 : M PUnit

set "Four" : M PUnit#check (set "Four" : M Unit)

set "Four" : M PUnit

8.5.2. モナド変換子（Monad Transformers）🔗

モナド変換子 （monad transformer）とは、モナドを与えると新しいモナドを返す関数のことです。通常、この新しいモナドは、もとのモナドのすべての作用といくつかの追加作用を持ちます。

モナド変換子は以下から構成されます：

関数 T 、既存のモナドから新しいモナドの型を構築します
T m α を m の変形に適応させる関数 run、これは多くの場合追加のパラメータを必要とし、 m の下でより特定の型を返します
[Monad m] → Monad (T m) のインスタンス、これにより変換されたモナドをモナドとして使用することができます
MonadLift のインスタンス、もとのモナドのコードを変換後のモナドで使用できるようにします
可能であれば、変換後のモナドアクションをもとのモナドで使用できるようにする MonadControl m (T m) のインスタンス

通常、モナド変換子はそれが導入する作用を記述する1つ以上の型クラスのインスタンスを提供します。変換子の Monad と MonadLift インスタンスは変換されたモナドでコードを書くことを実用的にし、型クラスのインスタンスは変換されたモナドを多相関数で使うことを可能にします。

恒等モナド変換子

恒等モナド変換子は、変換されたモナドへの機能の追加・削除を行いません。その定義は適切に特殊化された恒等関数です：

def IdT (m : Type u → Type v) : Type u → Type v := m

同様に、 run 関数は追加の引数を必要とせず、 m α を返すだけです：

def IdT.run (act : IdT m α) : m α := act

モナドのインスタンスは type ascriptions を介して選択され、変換されたモナドのモナドインスタンスに依存します：

instance [Monad m] : Monad (IdT m) where
  pure x := (pure x : m _)
  bind x f := (x >>= f : m _)

IdT m は m と definitionally equal であるため、 MonadLift m (IdT m) インスタンスはリフトされるアクションを変更する必要はありません：

instance : MonadLift m (IdT m) where
  monadLift x := x

MonadControl インスタンスも同様にシンプルです。

instance [Monad m] : MonadControl m (IdT m) where
  stM α := α
  liftWith f := f (fun x => Id.run <| pure x)
  restoreM v := v

Lean の標準ライブラリは ReaderT ・ ExceptT ・ StateT などの多くの異なるモナドの変換子バージョンを提供しており、また StateCpsT ・ StateRefT ・ ExceptCpsT などの他の表現を使用した変種も提供しています。さらに、 EStateM モナドは ExceptT と StateT を組み合わせたものと同等ですが、パフォーマンスを向上させるためにより特化した表現を使用することができます。

8.5.3. 恒等モナド（Identity）

恒等モナド Id は何の作用も持ちません。 Id と対応する pure の実装はどちらも恒等関数であり、 bind は関数適用を逆転させたものです。恒等モナドには主に2つの使用例があります：

Lean.Parser.Term.do : termdo ブロックの型にして、局所的に作用を持つ純粋関数を実装することができます。
モナド変換子のスタックの一番下に置くことができます。

def

Id.{u} (type : Type u) : Type u

def

Id.run.{u_1} {α : Type u_1} (x : Id α) : α

恒等モナドによる局所的な作用

このコードブロックは恒等モナドのシミュレートされた局所的な可変性を使ってカウントダウン処理を実装しています。

[9, 8, 7, 6, 5, 4, 3, 2, 1, 0]#eval Id.run do
  let mut xs := []
  for x in [0:10] do
    xs := x :: xs
  pure xs

[9, 8, 7, 6, 5, 4, 3, 2, 1, 0]

def

Id.hasBind.{u_1} : Bind Id

8.5.4. 状態（State）🔗

状態モナドは可変な値へのアクセスを提供します。基礎となる実装は、タプルを使用して可変性をシミュレートしたものとすることもでき、また ST.Ref のようなものを使用してミューテーションを保証することもできます。タプルを使用する実装であっても、値への一意な参照がある場合には Lean がミューテーションを使用するため、実際には実行時にミューテーションを使用する可能性がありますが、これには get や set よりも modify や modifyGet を好むプログラミングスタイルが必要です。

8.5.4.1. 一般的な状態の API（General State API）

type class

MonadState.{u, v} (σ : outParam (Type u))
    (m : Type u → Type v) : Type (max (u + 1) v)

Similar to MonadStateOf, but σ is an outParam for convenience.

Instance Constructor

MonadState.mk.{u, v}

Methods

get : m σ

(← get) : σ gets the state out of a monad m.

set : σ → m PUnit

set (s : σ) replaces the state with value s.

modifyGet : {α : Type u} → (σ → α × σ) → m α

modifyGet (f : σ → α × σ) applies f to the current state, replaces the state with the return value, and returns a computed value.

It is equivalent to do let (a, s) := f (← get); put s; pure a, but modifyGet f may be preferable because the former does not use the state linearly (without sufficient inlining).

def

MonadState.get.{u, v} {σ : outParam (Type u)}
  {m : Type u → Type v}
  [self : MonadState σ m] : m σ

(← get) : σ gets the state out of a monad m.

def

modify.{u, v} {σ : Type u} {m : Type u → Type v}
    [MonadState σ m] (f : σ → σ) : m PUnit

modify (f : σ → σ) applies the function f to the state.

It is equivalent to do set (f (← get)), but modify f may be preferable because the former does not use the state linearly (without sufficient inlining).

def

MonadState.modifyGet.{u, v}
  {σ : outParam (Type u)} {m : Type u → Type v}
  [self : MonadState σ m] {α : Type u} :
  (σ → α × σ) → m α

modifyGet (f : σ → α × σ) applies f to the current state, replaces the state with the return value, and returns a computed value.

It is equivalent to do let (a, s) := f (← get); put s; pure a, but modifyGet f may be preferable because the former does not use the state linearly (without sufficient inlining).

def

getModify.{u, v} {σ : Type u}
    {m : Type u → Type v} [MonadState σ m]
    (f : σ → σ) : m σ

getModify f gets the state, applies function f, and returns the old value of the state. It is equivalent to get <* modify f but may be more efficient.

type class

MonadStateOf.{u, v} (σ : semiOutParam (Type u))
    (m : Type u → Type v) : Type (max (u + 1) v)

An implementation of MonadState. In contrast to the Haskell implementation, we use overlapping instances to derive instances automatically from monadLift.

Instance Constructor

MonadStateOf.mk.{u, v}

Methods

get : m σ

(← get) : σ gets the state out of a monad m.

set : σ → m PUnit

set (s : σ) replaces the state with value s.

modifyGet : {α : Type u} → (σ → α × σ) → m α

modifyGet (f : σ → α × σ) applies f to the current state, replaces the state with the return value, and returns a computed value.

It is equivalent to do let (a, s) := f (← get); put s; pure a, but modifyGet f may be preferable because the former does not use the state linearly (without sufficient inlining).

def

getThe.{u, v} (σ : Type u) {m : Type u → Type v}
    [MonadStateOf σ m] : m σ

Like get, but with σ explicit. This is useful if a monad supports MonadStateOf for multiple different types σ.

def

modifyThe.{u, v} (σ : Type u)
    {m : Type u → Type v} [MonadStateOf σ m]
    (f : σ → σ) : m PUnit

Like modify, but with σ explicit. This is useful if a monad supports MonadStateOf for multiple different types σ.

def

modifyGetThe.{u, v} {α : Type u} (σ : Type u)
    {m : Type u → Type v} [MonadStateOf σ m]
    (f : σ → α × σ) : m α

Like modifyGet, but with σ explicit. This is useful if a monad supports MonadStateOf for multiple different types σ.

8.5.4.2. タプルベースの状態モナド（Tuple-Based State Monads）

タプルベースの状態モナドは σ 型の値をもたらす α 型の状態を持つ計算を、例えば σ → α × σ のように開始状態を受け取り、最終状態と対になった値をもたらす関数として表現します。 Monad 演算は、計算を通して状態を正しくスレッド化します。

def

StateM.{u} (σ α : Type u) : Type u

def

StateT.{u, v} (σ : Type u) (m : Type u → Type v)
    (α : Type u) : Type (max u v)

def

StateT.run.{u, v} {σ : Type u}
    {m : Type u → Type v} {α : Type u}
    (x : StateT σ m α) (s : σ) : m (α × σ)

def

StateT.get.{u, v} {σ : Type u}
    {m : Type u → Type v} [Monad m]
    : StateT σ m σ

def

StateT.set.{u, v} {σ : Type u}
    {m : Type u → Type v} [Monad m]
    : σ → StateT σ m PUnit

def

StateT.orElse.{u, v} {σ : Type u}
    {m : Type u → Type v} [Alternative m]
    {α : Type u} (x₁ : StateT σ m α)
    (x₂ : Unit → StateT σ m α) : StateT σ m α

def

StateT.failure.{u, v} {σ : Type u}
    {m : Type u → Type v} [Alternative m]
    {α : Type u} : StateT σ m α

def

StateT.run'.{u, v} {σ : Type u}
    {m : Type u → Type v} [Functor m]
    {α : Type u} (x : StateT σ m α) (s : σ)
    : m α

def

StateT.bind.{u, v} {σ : Type u}
    {m : Type u → Type v} [Monad m]
    {α β : Type u} (x : StateT σ m α)
    (f : α → StateT σ m β) : StateT σ m β

def

StateT.modifyGet.{u, v} {σ : Type u}
    {m : Type u → Type v} [Monad m] {α : Type u}
    (f : σ → α × σ) : StateT σ m α

def

StateT.lift.{u, v} {σ : Type u}
    {m : Type u → Type v} [Monad m] {α : Type u}
    (t : m α) : StateT σ m α

def

StateT.map.{u, v} {σ : Type u}
    {m : Type u → Type v} [Monad m]
    {α β : Type u} (f : α → β)
    (x : StateT σ m α) : StateT σ m β

def

StateT.pure.{u, v} {σ : Type u}
    {m : Type u → Type v} [Monad m] {α : Type u}
    (a : α) : StateT σ m α

8.5.4.3. 継続渡しスタイルの状態モナド（State Monads in Continuation Passing Style）

継続渡しスタイルの状態モナドは、どのような型に対しても初期状態と、値・更新された状態を受け取る継続（関数としてモデル化されます）を受け取る関数として状態を持つ計算を表現します。このような型の例は (δ : Type u) → σ → (α → σ → δ) → δ ですが、 StateCpsT はどのモナドにも適用できる変換子です。継続渡しスタイルの状態モナドはタプルベースの状態モナドとは異なるパフォーマンス特性を持ちます；アプリケーションによってはベンチマークを取る価値があるかもしれません。

def

StateCpsT.{u, v} (σ : Type u)
    (m : Type u → Type v) (α : Type u)
    : Type (max (u + 1) v)

def

StateCpsT.lift.{u, v} {α σ : Type u}
    {m : Type u → Type v} [Monad m] (x : m α)
    : StateCpsT σ m α

def

StateCpsT.runK.{u, v} {α σ : Type u}
    {m : Type u → Type v} {β : Type u}
    (x : StateCpsT σ m α) (s : σ)
    (k : α → σ → m β) : m β

def

StateCpsT.run'.{u, v} {α σ : Type u}
    {m : Type u → Type v} [Monad m]
    (x : StateCpsT σ m α) (s : σ) : m α

def

StateCpsT.run.{u, v} {α σ : Type u}
    {m : Type u → Type v} [Monad m]
    (x : StateCpsT σ m α) (s : σ) : m (α × σ)

8.5.4.4. 可変参照からの状態モナド（State Monads from Mutable References）

モナド StateRefT σ m は m が ST の計算を持ち上げることができるモナドである場合に使用できる、特殊な状態モナド変換子です。 MonadState の演算は、純粋な関数ではなく ST.Ref を使用して実装されます。これにより、ミューテーションが実行時に実際に使用されることが保証されます。

ST と EST は可変性をカプセル化するために runST の多相関数引数と一緒に使用される幽霊型パラメータを必要とします。これを変換子のパラメータとして要求するのではなく、補助の型クラス STWorld を使用して m から直接伝播させます。

この変換子自体は普通の関数ではなく、構文拡張とエラボレータとして定義されています。これは STWorld がメソッドを持たないためです：これは内側のモナドから変換後のモナドに情報を伝播するためだけに存在します。それにもかかわたず、そのインスタンスは項です；これを保持すると不必要に大きい型になる可能性があります。

type class

STWorld (σ : outParam Type) (m : Type → Type)
    : Type

Instance Constructor

STWorld.mk

Methods

syntax

StateRefT σ m の構文は2つの引数を取ります：

term ::= ...
    | StateRefT term (macroDollarArg
       | term)

そのエラボレータは STWorld ω m のインスタンスを統合し、 m が可変参照をサポートしていることを保証します。 ω の値を発見した後、 StateRefT' ω σ m の項を生成し、統合されたインスタンスを破棄します。

def

StateRefT' (ω σ : Type) (m : Type → Type)
    (α : Type) : Type

def

StateRefT'.get {ω σ : Type} {m : Type → Type}
    [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ

def

StateRefT'.set {ω σ : Type} {m : Type → Type}
    [MonadLiftT (ST ω) m] (s : σ)
    : StateRefT' ω σ m PUnit

def

StateRefT'.modifyGet {ω σ : Type}
    {m : Type → Type} {α : Type}
    [MonadLiftT (ST ω) m] (f : σ → α × σ)
    : StateRefT' ω σ m α

def

StateRefT'.run {ω σ : Type} {m : Type → Type}
    [Monad m] [MonadLiftT (ST ω) m] {α : Type}
    (x : StateRefT' ω σ m α) (s : σ) : m (α × σ)

def

StateRefT'.run' {ω σ : Type} {m : Type → Type}
    [Monad m] [MonadLiftT (ST ω) m] {α : Type}
    (x : StateRefT' ω σ m α) (s : σ) : m α

def

StateRefT'.lift {ω σ : Type} {m : Type → Type}
    {α : Type} (x : m α) : StateRefT' ω σ m α

8.5.5. リーダ（Reader）🔗

type class

MonadReader.{u, v} (ρ : outParam (Type u))
    (m : Type u → Type v) : Type v

Similar to MonadReaderOf, but ρ is an outParam for convenience.

Instance Constructor

MonadReader.mk.{u, v}

Methods

read : m ρ

(← read) : ρ reads the state out of monad m.

type class

MonadReaderOf.{u, v} (ρ : semiOutParam (Type u))
    (m : Type u → Type v) : Type v

An implementation of Haskell's MonadReader (sans functional dependency; see also MonadReader in this module). It does not contain local because this function cannot be lifted using monadLift. local is instead provided by the MonadWithReader class as withReader.

Note: This class can be seen as a simplification of the more "principled" definition

class MonadReaderOf (ρ : Type u) (n : Type u → Type u) where
  lift {α : Type u} : ({m : Type u → Type u} → [Monad m] → ReaderT ρ m α) → n α

Instance Constructor

MonadReaderOf.mk.{u, v}

Methods

read : m ρ

(← read) : ρ reads the state out of monad m.

def

readThe.{u, v} (ρ : Type u)
    {m : Type u → Type v} [MonadReaderOf ρ m]
    : m ρ

Like read, but with ρ explicit. This is useful if a monad supports MonadReaderOf for multiple different types ρ.

type class

MonadWithReader.{u, v} (ρ : outParam (Type u))
    (m : Type u → Type v) : Type (max (u + 1) v)

Similar to MonadWithReaderOf, but ρ is an outParam for convenience.

Instance Constructor

MonadWithReader.mk.{u, v}

Methods

withReader : {α : Type u} → (ρ → ρ) → m α → m α

withReader (f : ρ → ρ) (x : m α) : m α runs the inner x : m α inside a modified context after applying the function f : ρ → ρ.

type class

MonadWithReaderOf.{u, v}
    (ρ : semiOutParam (Type u))
    (m : Type u → Type v) : Type (max (u + 1) v)

MonadWithReaderOf ρ adds the operation withReader : (ρ → ρ) → m α → m α. This runs the inner x : m α inside a modified context after applying the function f : ρ → ρ. In addition to ReaderT itself, this operation lifts over most monad transformers, so it allows us to apply withReader to monads deeper in the stack.

Instance Constructor

MonadWithReaderOf.mk.{u, v}

Methods

withReader : {α : Type u} → (ρ → ρ) → m α → m α

withReader (f : ρ → ρ) (x : m α) : m α runs the inner x : m α inside a modified context after applying the function f : ρ → ρ.

def

withTheReader.{u, v} (ρ : Type u)
    {m : Type u → Type v}
    [MonadWithReaderOf ρ m] {α : Type u}
    (f : ρ → ρ) (x : m α) : m α

Like withReader, but with ρ explicit. This is useful if a monad supports MonadWithReaderOf for multiple different types ρ.

def

ReaderT.{u, v} (ρ : Type u)
    (m : Type u → Type v) (α : Type u)
    : Type (max u v)

An implementation of Haskell's ReaderT. This is a monad transformer which equips a monad with additional read-only state, of type ρ.

def

ReaderM.{u} (ρ α : Type u) : Type u

def

ReaderT.adapt.{u, v} {ρ : Type u}
    {m : Type u → Type v} {ρ' α : Type u}
    (f : ρ' → ρ)
    : ReaderT ρ m α → ReaderT ρ' m α

adapt (f : ρ' → ρ) precomposes function f on the reader state of a ReaderT ρ, yielding a ReaderT ρ'.

def

ReaderT.read.{u, v} {ρ : Type u}
    {m : Type u → Type v} [Monad m]
    : ReaderT ρ m ρ

(← read) : ρ gets the read-only state of a ReaderT ρ.

def

ReaderT.run.{u, v} {ρ : Type u}
    {m : Type u → Type v} {α : Type u}
    (x : ReaderT ρ m α) (r : ρ) : m α

If x : ReaderT ρ m α and r : ρ, then x.run r : ρ runs the monad with the given reader state.

def

ReaderT.orElse.{u_1, u_2}
    {m : Type u_1 → Type u_2} {ρ α : Type u_1}
    [Alternative m] (x₁ : ReaderT ρ m α)
    (x₂ : Unit → ReaderT ρ m α) : ReaderT ρ m α

def

ReaderT.bind.{u, v} {ρ : Type u}
    {m : Type u → Type v} [Monad m]
    {α β : Type u} (x : ReaderT ρ m α)
    (f : α → ReaderT ρ m β) : ReaderT ρ m β

The bind operation of the ReaderT monad.

def

ReaderT.failure.{u_1, u_2}
    {m : Type u_1 → Type u_2} {ρ α : Type u_1}
    [Alternative m] : ReaderT ρ m α

def

ReaderT.pure.{u, v} {ρ : Type u}
    {m : Type u → Type v} [Monad m] {α : Type u}
    (a : α) : ReaderT ρ m α

The pure operation of the ReaderT monad.

8.5.6. オプション（Option）🔗

通常、 Option は nullable 型と同じようなデータとして考えられます。また、モナド、つまり計算を実行する方法として考えることもできます。 Option モナドとその変換子 OptionT は、結果を破棄して早期に終了する可能性のある計算を記述するものとして理解することができます。呼び出し元は OrElse.orElse を使用するか、 MonadExcept Unit として扱うことで早期終了をチェックし、必要に応じてフォールバックを呼び出すことができます。

def

OptionT.{u, v} (m : Type u → Type v)
    (α : Type u) : Type v

def

OptionT.run.{u, v} {m : Type u → Type v}
    {α : Type u} (x : OptionT m α)
    : m (Option α)

def

OptionT.lift.{u, v} {m : Type u → Type v}
    [Monad m] {α : Type u} (x : m α)
    : OptionT m α

def

OptionT.mk.{u, v} {m : Type u → Type v}
    {α : Type u} (x : m (Option α))
    : OptionT m α

def

OptionT.pure.{u, v} {m : Type u → Type v}
    [Monad m] {α : Type u} (a : α) : OptionT m α

def

OptionT.bind.{u, v} {m : Type u → Type v}
    [Monad m] {α β : Type u} (x : OptionT m α)
    (f : α → OptionT m β) : OptionT m β

def

OptionT.fail.{u, v} {m : Type u → Type v}
    [Monad m] {α : Type u} : OptionT m α

def

OptionT.orElse.{u, v} {m : Type u → Type v}
    [Monad m] {α : Type u} (x : OptionT m α)
    (y : Unit → OptionT m α) : OptionT m α

def

OptionT.tryCatch.{u, v} {m : Type u → Type v}
    [Monad m] {α : Type u} (x : OptionT m α)
    (handle : Unit → OptionT m α) : OptionT m α

8.5.7. 例外（Exceptions）🔗

例外モナドは早期に終了（失敗）する計算を記述します。失敗した計算は、なぜ失敗したかを示す例外値を呼び出し元に提供します。言い換えると、計算は値か例外を返します。帰納型 Except はこのパターンを捕捉しており、それ自体がモナドです。

8.5.7.1. 例外（Exceptions）

inductive type

Except.{u, v} (ε : Type u) (α : Type v)
    : Type (max u v)

Except ε α is a type which represents either an error of type ε, or an "ok" value of type α. The error type is listed first because Except ε : Type → Type is a Monad: the pure operation is ok and the bind operation returns the first encountered error.

Constructors

error.{u, v} {ε : Type u} {α : Type v} : ε → Except ε α

A failure value of type ε

ok.{u, v} {ε : Type u} {α : Type v} : α → Except ε α

A success value of type α

def

Except.pure.{u, u_1} {ε : Type u} {α : Type u_1}
    (a : α) : Except ε α

def

Except.bind.{u, u_1, u_2} {ε : Type u}
    {α : Type u_1} {β : Type u_2}
    (ma : Except ε α) (f : α → Except ε β)
    : Except ε β

def

Except.map.{u, u_1, u_2} {ε : Type u}
    {α : Type u_1} {β : Type u_2} (f : α → β)
    : Except ε α → Except ε β

def

Except.mapError.{u, u_1, u_2} {ε : Type u}
    {ε' : Type u_1} {α : Type u_2} (f : ε → ε')
    : Except ε α → Except ε' α

def

Except.tryCatch.{u, u_1} {ε : Type u}
    {α : Type u_1} (ma : Except ε α)
    (handle : ε → Except ε α) : Except ε α

def

Except.orElseLazy.{u, u_1} {ε : Type u}
    {α : Type u_1} (x : Except ε α)
    (y : Unit → Except ε α) : Except ε α

def

Except.isOk.{u, u_1} {ε : Type u} {α : Type u_1}
    : Except ε α → Bool

def

Except.toOption.{u, u_1} {ε : Type u}
    {α : Type u_1} : Except ε α → Option α

def

Except.toBool.{u, u_1} {ε : Type u}
    {α : Type u_1} : Except ε α → Bool

Returns true if the value is Except.ok, false otherwise.

8.5.7.2. 型クラス（Type Class）

type class

MonadExcept.{u, v, w} (ε : outParam (Type u))
    (m : Type v → Type w)
    : Type (max (max u (v + 1)) w)

Similar to MonadExceptOf, but ε is an outParam for convenience.

Instance Constructor

MonadExcept.mk.{u, v, w}

Methods

throw : {α : Type v} → ε → m α

throw : ε → m α "throws an error" of type ε to the nearest enclosing catch block.

tryCatch : {α : Type v} → m α → (ε → m α) → m α

tryCatch (body : m α) (handler : ε → m α) : m α will catch any errors in body and pass the resulting error to handler. Errors in handler will not be caught.

def

MonadExcept.ofExcept.{u_1, u_2, u_3}
    {m : Type u_1 → Type u_2} {ε : Type u_3}
    {α : Type u_1} [Monad m] [MonadExcept ε m]
    : Except ε α → m α

"Unwraps" an Except ε α to get the α, or throws the exception otherwise.

def

MonadExcept.orElse.{u, v, w} {ε : Type u}
    {m : Type v → Type w} [MonadExcept ε m]
    {α : Type v} (t₁ : m α) (t₂ : Unit → m α)
    : m α

A MonadExcept can implement t₁ <|> t₂ as try t₁ catch _ => t₂.

def

MonadExcept.orelse'.{u, v, w} {ε : Type u}
  {m : Type v → Type w} [MonadExcept ε m]
  {α : Type v} (t₁ t₂ : m α)
  (useFirstEx : Bool := true) : m α

Alternative orelse operator that allows to select which exception should be used. The default is to use the first exception since the standard orelse uses the second.

type class

MonadExceptOf.{u, v, w}
    (ε : semiOutParam (Type u))
    (m : Type v → Type w)
    : Type (max (max u (v + 1)) w)

An implementation of Haskell's MonadError class. A MonadError ε m is a monad m with two operations:

throw : ε → m α "throws an error" of type ε to the nearest enclosing catch block
tryCatch (body : m α) (handler : ε → m α) : m α will catch any errors in body and pass the resulting error to handler. Errors in handler will not be caught.

The try ... catch e => ... syntax inside do blocks is sugar for the tryCatch operation.

Instance Constructor

MonadExceptOf.mk.{u, v, w}

Methods

throw : {α : Type v} → ε → m α

throw : ε → m α "throws an error" of type ε to the nearest enclosing catch block.

tryCatch : {α : Type v} → m α → (ε → m α) → m α

tryCatch (body : m α) (handler : ε → m α) : m α will catch any errors in body and pass the resulting error to handler. Errors in handler will not be caught.

def

throwThe.{u, v, w} (ε : Type u)
    {m : Type v → Type w} [MonadExceptOf ε m]
    {α : Type v} (e : ε) : m α

This is the same as throw, but allows specifying the particular error type in case the monad supports throwing more than one type of error.

def

tryCatchThe.{u, v, w} (ε : Type u)
    {m : Type v → Type w} [MonadExceptOf ε m]
    {α : Type v} (x : m α) (handle : ε → m α)
    : m α

This is the same as tryCatch, but allows specifying the particular error type in case the monad supports throwing more than one type of error.

8.5.7.3. 「finally」の計算（“Finally” Computations）

type class

MonadFinally.{u, v} (m : Type u → Type v)
    : Type (max (u + 1) v)

Instance Constructor

MonadFinally.mk.{u, v}

Methods

tryFinally' : {α β : Type u} → m α → (Option α → m β) → m (α × β)

tryFinally' x f runs x and then the "finally" computation f. When x succeeds with a : α, f (some a) is returned. If x fails for m's definition of failure, f none is returned. Hence tryFinally' can be thought of as performing the same role as a finally block in an imperative programming language.

8.5.7.4. 変換子（Transformer）

def

ExceptT.{u, v} (ε : Type u)
    (m : Type u → Type v) (α : Type u) : Type v

def

ExceptT.lift.{u, v} {ε : Type u}
    {m : Type u → Type v} [Monad m] {α : Type u}
    (t : m α) : ExceptT ε m α

def

ExceptT.run.{u, v} {ε : Type u}
    {m : Type u → Type v} {α : Type u}
    (x : ExceptT ε m α) : m (Except ε α)

def

ExceptT.pure.{u, v} {ε : Type u}
    {m : Type u → Type v} [Monad m] {α : Type u}
    (a : α) : ExceptT ε m α

def

ExceptT.bind.{u, v} {ε : Type u}
    {m : Type u → Type v} [Monad m]
    {α β : Type u} (ma : ExceptT ε m α)
    (f : α → ExceptT ε m β) : ExceptT ε m β

def

ExceptT.bindCont.{u, v} {ε : Type u}
    {m : Type u → Type v} [Monad m]
    {α β : Type u} (f : α → ExceptT ε m β)
    : Except ε α → m (Except ε β)

def

ExceptT.tryCatch.{u, v} {ε : Type u}
    {m : Type u → Type v} [Monad m] {α : Type u}
    (ma : ExceptT ε m α)
    (handle : ε → ExceptT ε m α) : ExceptT ε m α

def

ExceptT.mk.{u, v} {ε : Type u}
    {m : Type u → Type v} {α : Type u}
    (x : m (Except ε α)) : ExceptT ε m α

def

ExceptT.map.{u, v} {ε : Type u}
    {m : Type u → Type v} [Monad m]
    {α β : Type u} (f : α → β)
    (x : ExceptT ε m α) : ExceptT ε m β

def

ExceptT.adapt.{u, v} {ε : Type u}
    {m : Type u → Type v} [Monad m]
    {ε' α : Type u} (f : ε → ε')
    : ExceptT ε m α → ExceptT ε' m α

8.5.7.5. 継続渡しスタイルの例外モナド（Exception Monads in Continuation Passing Style）

継続渡しスタイルの例外モナドは、失敗する可能性のある計算を、成功と失敗を取る関数として表します。この継続はどちらも同じ型を返し、この関数はその型を返します。例外モナドは どのような 戻り値の型でも動作しなければなりません。このような型の例は (β : Type u) → (α → β) → (ε → β) → β です。 ExceptCpsT は任意のモナドに適用できる変換子であるため、 ExceptCpsT ε m α は実際には (β : Type u) → (α → m β) → (ε → m β) → m β と定義されています。継続渡しスタイルの例外モナドは、 Except ベースの状態モナドとは異なるパフォーマンス特性を持ちます；アプリケーションによってはベンチマークを取る価値があるかもしれません。

def

ExceptCpsT.{u, v} (ε : Type u)
    (m : Type u → Type v) (α : Type u)
    : Type (max (u + 1) v)

def

ExceptCpsT.runCatch.{u_1, u_2}
    {m : Type u_1 → Type u_2} {α : Type u_1}
    [Monad m] (x : ExceptCpsT α m α) : m α

def

ExceptCpsT.runK.{u, u_1} {m : Type u → Type u_1}
    {β ε α : Type u} (x : ExceptCpsT ε m α)
    (s : ε) (ok : α → m β) (error : ε → m β)
    : m β

def

ExceptCpsT.run.{u, u_1} {m : Type u → Type u_1}
    {ε α : Type u} [Monad m]
    (x : ExceptCpsT ε m α) : m (Except ε α)

def

ExceptCpsT.lift.{u_1, u_2}
    {m : Type u_1 → Type u_2} {α ε : Type u_1}
    [Monad m] (x : m α) : ExceptCpsT ε m α

8.5.8. エラーと状態モナドの結合（Combined Error and State Monads）

EStateM モナドは例外と可変状態の両方を持ちます。 EStateM ε σ α は ExceptT ε (StateM σ) α と論理的に等価です。 ExceptT ε (StateM σ) が σ → Except ε α × σ 型に評価されるのに対して、 EStateM ε σ α は σ → EStateM.Result ε σ α 型に評価されます。 EStateM.Result は Except とよく似た帰納型ですが、どちらのコンストラクタにも状態を表すフィールドが追加されています。コンパイルされたコードでは、この表現は各モナドの bind から1段階インダイレクションを取り除きます。

def

EStateM.{u} (ε σ α : Type u) : Type u

EStateM ε σ is a combined error and state monad, equivalent to ExceptT ε (StateM σ) but more efficient.

inductive type

EStateM.Result.{u} (ε σ α : Type u) : Type u

Result ε σ α is equivalent to Except ε α × σ, but using a single combined inductive yields a more efficient data representation.

Constructors

ok.{u} {ε σ α : Type u} : α → σ → EStateM.Result ε σ α

A success value of type α, and a new state σ.

error.{u} {ε σ α : Type u} : ε → σ → EStateM.Result ε σ α

A failure value of type ε, and a new state σ.

def

EStateM.run.{u} {ε σ α : Type u}
    (x : EStateM ε σ α) (s : σ)
    : EStateM.Result ε σ α

Execute an EStateM on initial state s to get a Result.

def

EStateM.run'.{u} {ε σ α : Type u}
    (x : EStateM ε σ α) (s : σ) : Option α

Execute an EStateM on initial state s for the returned value α. If the monadic action throws an exception, returns none instead.

def

EStateM.adaptExcept.{u} {ε σ α ε' : Type u}
    (f : ε → ε') (x : EStateM ε σ α)
    : EStateM ε' σ α

Map the exception type of a EStateM ε σ α by a function f : ε → ε'.

def

EStateM.fromStateM {ε σ α : Type}
    (x : StateM σ α) : EStateM ε σ α

8.5.8.1. 状態のロールバック（State Rollback）

StateT と ExceptT を異なる順序で合成すると例外と状態の相互作用は異なるものになります。片方の順序では、例外が捕捉された時に状態の変更がロールバックされ、もう一方では状態が持続します。後者のオプションはほとんどの命令型プログラミング言語のセマンティックスに一致しますが、前者は検索ベースの問題に対して非常に便利です。またしばしば、すべてではなく一部の状態だけがロールバックされるべき場合もあります；これは ExceptT を2つの StateT で「サンドイッチ」することで実現できます。

StateT σ (EStateM ε σ') α の使用によるさらに別のレイヤーからのインダイレクトを避けるために、 EStateM は EStateM.Backtrackable 型クラスを提供します。このクラスは保存と復元が可能な状態の一部を指定します。 EStateM はエラー処理を中心に保存と復元が行われるよう調整します。

type class

EStateM.Backtrackable.{u}
    (δ : outParam (Type u)) (σ : Type u)
    : Type u

Auxiliary instance for saving/restoring the "backtrackable" part of the state. Here σ is the state, and δ is some subpart of it, and we have a getter and setter for it (a "lens" in the Haskell terminology).

Instance Constructor

EStateM.Backtrackable.mk.{u}

Methods

save : σ → δ

save s : δ retrieves a copy of the backtracking state out of the state.

restore : σ → δ → σ

restore (s : σ) (x : δ) : σ applies the old backtracking state x to the state s to get a backtracked state s'.

Backtrackable には普遍的に適用可能なインスタンスがありますが、これは何も保存も復元もしません。インスタンス統合は最新のインスタンスを最初に選択するため、他のインスタンスが定義されていない場合にのみこの普遍的なインスタンスが使用されます。

def

EStateM.nonBacktrackable.{u} {σ : Type u}
    : EStateM.Backtrackable PUnit σ

Dummy default instance. This makes every σ trivially "backtrackable" by doing nothing on backtrack. Because this is the first declared instance of Backtrackable _ σ, it will be picked only if there are no other Backtrackable _ σ instances registered.

8.5.8.2. 実装（Implementations）

これらの関数は通常、直接呼び出されることはなく、対応する型クラスを通じてアクセスされます。

def

EStateM.map.{u} {ε σ α β : Type u} (f : α → β)
    (x : EStateM ε σ α) : EStateM ε σ β

The map operation of the EStateM monad.

def

EStateM.pure.{u} {ε σ α : Type u} (a : α)
    : EStateM ε σ α

The pure operation of the EStateM monad.

def

EStateM.bind.{u} {ε σ α β : Type u}
    (x : EStateM ε σ α) (f : α → EStateM ε σ β)
    : EStateM ε σ β

The bind operation of the EStateM monad.

def

EStateM.orElse.{u} {ε σ α δ : Type u}
    [EStateM.Backtrackable δ σ]
    (x₁ : EStateM ε σ α)
    (x₂ : Unit → EStateM ε σ α) : EStateM ε σ α

Implementation of orElse for EStateM where the state is Backtrackable.

def

EStateM.orElse'.{u} {ε σ α δ : Type u}
  [EStateM.Backtrackable δ σ]
  (x₁ x₂ : EStateM ε σ α)
  (useFirstEx : Bool := true) : EStateM ε σ α

Alternative orElse operator that allows to select which exception should be used. The default is to use the first exception since the standard orElse uses the second.

def

EStateM.seqRight.{u} {ε σ α β : Type u}
    (x : EStateM ε σ α)
    (y : Unit → EStateM ε σ β) : EStateM ε σ β

The seqRight operation of the EStateM monad.

def

EStateM.tryCatch.{u} {ε σ δ : Type u}
    [EStateM.Backtrackable δ σ] {α : Type u}
    (x : EStateM ε σ α)
    (handle : ε → EStateM ε σ α) : EStateM ε σ α

Implementation of tryCatch for EStateM where the state is Backtrackable.

def

EStateM.throw.{u} {ε σ α : Type u} (e : ε)
    : EStateM ε σ α

The throw operation of the EStateM monad.

def

EStateM.get.{u} {ε σ : Type u} : EStateM ε σ σ

The get operation of the EStateM monad.

def

EStateM.set.{u} {ε σ : Type u} (s : σ)
    : EStateM ε σ PUnit

The set operation of the EStateM monad.

def

EStateM.modifyGet.{u} {ε σ α : Type u}
    (f : σ → α × σ) : EStateM ε σ α

The modifyGet operation of the EStateM monad.