例：モナドにおける算術

モナドは副作用のない言語で副作用のあるプログラムをエンコードする手段です。この事実を以って、純粋関数型言語で普通のプログラムを書くために大変面倒な手続きを踏まなければならないために、純粋関数型プログラムには重要なものが欠けていると認めているようなものだと考えるのは容易でしょう。しかし、Monad のAPIを使うことはプログラムに構文上のコストを課すことになる一方で2つの重要な利点をもたらします：

  1. プログラムはその型の中に、どの作用を使うか使うかについて表明しなければなりません。型シグネチャをざっと見ただけで、そのプログラムが何を受け入れ、何を返すかだけでなく、そのプログラムができることの すべて が記述されます。
  2. すべての言語で同じ作用が提供されているとは限りません。例えば、一部の言語だけが例外の機構を持ちます。他の言語には Icon言語における複数値検索 や、SchemeやRubyの継続などのようなユニークで独特な作用が存在します。モナドは どんな 作用でもエンコードできるため、プログラマは言語開発者が提供する作用に囚われることなく与えられたアプリケーションに最適な作用を選ぶことができます。

さまざまなモナドで意味をもつプログラムの一例として、算術式の評価器があります。

算術式

算術式は整数値のリテラルか2つの式に適用されるプリミティブな二項演算子です。演算子は加算、減算、乗算、除算からなります：

inductive Expr (op : Type) where
  | const : Int → Expr op
  | prim : op → Expr op → Expr op → Expr op


inductive Arith where
  | plus
  | minus
  | times
  | div

2 + 3 という式は以下のように表現されます：

open Expr in
open Arith in
def twoPlusThree : Expr Arith :=
  prim plus (const 2) (const 3)

また、14 / (45 - 5 * 9) は以下のように表現されます：

open Expr in
open Arith in
def fourteenDivided : Expr Arith :=
  prim div (const 14) (prim minus (const 45) (prim times (const 5) (const 9)))

式の評価

式の中に除算が含まれ、かつ0による除算は未定義であるため、評価には失敗の可能性があります。失敗の表現の手段の1つとして、Option を使うことができます：

def evaluateOption : Expr Arith → Option Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateOption e1 >>= fun v1 =>
    evaluateOption e2 >>= fun v2 =>
    match p with
    | Arith.plus => pure (v1 + v2)
    | Arith.minus => pure (v1 - v2)
    | Arith.times => pure (v1 * v2)
    | Arith.div => if v2 == 0 then none else pure (v1 / v2)

この定義では Monad Option のインスタンスを使用して、二項演算子の2つの分岐それぞれの評価による失敗を伝播します。しかし、この関数は部分式の評価と結果への二項演算子の適用という2つの関心事を混在させています。この状況は、この関数を2つの関数に分割することで改善することができます：

def applyPrim : Arith → Int → Int → Option Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y => if y == 0 then none else pure (x / y)

def evaluateOption : Expr Arith → Option Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateOption e1 >>= fun v1 =>
    evaluateOption e2 >>= fun v2 =>
    applyPrim p v1 v2

#eval evaluateOption fourteenDivided を実行すると期待通り none が出力されますが、これはあまり有用なエラーメッセージではありません。このコードは none コンストラクタを明示的に扱う代わりに >>= を使って書かれているため、失敗時にエラーメッセージを表示するために必要なのはわずかな修正だけです：

def applyPrim : Arith → Int → Int → Except String Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y =>
    if y == 0 then
      Except.error s!"Tried to divide {x} by zero"
    else pure (x / y)


def evaluateExcept : Expr Arith → Except String Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateExcept e1 >>= fun v1 =>
    evaluateExcept e2 >>= fun v2 =>
    applyPrim p v1 v2

変更点は、型シグネチャが Option ではなく Except String に言及していることと、失敗した場合に none ではなく Except.error を使用していることだけです。evaluate をモナドに対して多相にし、引数として applyPrim を渡すことで、1つの評価器で両方の形式でのエラー報告ができるようになります：

def applyPrimOption : Arith → Int → Int → Option Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y =>
    if y == 0 then
      none
    else pure (x / y)

def applyPrimExcept : Arith → Int → Int → Except String Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y =>
    if y == 0 then
      Except.error s!"Tried to divide {x} by zero"
    else pure (x / y)

def evaluateM [Monad m] (applyPrim : Arith → Int → Int → m Int): Expr Arith → m Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateM applyPrim e1 >>= fun v1 =>
    evaluateM applyPrim e2 >>= fun v2 =>
    applyPrim p v1 v2

これを applyPrimOption で使うとまさに evaluate の最初のバージョンと同じように動きます：

#eval evaluateM applyPrimOption fourteenDivided

none

同様に、applyPrimExcept を用いるとエラーメッセージのバージョンと同じように動作します：

#eval evaluateM applyPrimExcept fourteenDivided

Except.error "Tried to divide 14 by zero"

このコードはさらに改善できます。関数 applyPrimOption と applyPrimExcept の違いは除算の扱いだけであるため、除算を評価器の別のパラメータとして抽出することができます：

def applyDivOption (x : Int) (y : Int) : Option Int :=
    if y == 0 then
      none
    else pure (x / y)

def applyDivExcept (x : Int) (y : Int) : Except String Int :=
    if y == 0 then
      Except.error s!"Tried to divide {x} by zero"
    else pure (x / y)

def applyPrim [Monad m] (applyDiv : Int → Int → m Int) : Arith → Int → Int → m Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y => applyDiv x y

def evaluateM [Monad m] (applyDiv : Int → Int → m Int): Expr Arith → m Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateM applyDiv e1 >>= fun v1 =>
    evaluateM applyDiv e2 >>= fun v2 =>
    applyPrim applyDiv p v1 v2

このリファクタリングされたコードによって、2つのコードの実行の流れは失敗の扱いが異なるだけであるという事実がはっきりしました。

さらなる作用

評価器を扱うにあたって興味深いことは、失敗と例外だけにとどまりません。除算の唯一の副作用は失敗ですが、ほかのプリミティブな演算子を式に追加することで、ほかの作用を表現することが可能になります。

追加のリファクタリングの最初のステップとして、プリミティブのデータ型から除算を抜き出します：

inductive Prim (special : Type) where
  | plus
  | minus
  | times
  | other : special → Prim special

inductive CanFail where
  | div

CanFail という名前で、除算で導入される作用が潜在的な失敗であることを示唆します。

第二のステップは、evaluateM に対する除算のハンドラの引数の範囲を広げて、どんな特殊演算子でも処理できるようにすることです：

def divOption : CanFail → Int → Int → Option Int
  | CanFail.div, x, y => if y == 0 then none else pure (x / y)

def divExcept : CanFail → Int → Int → Except String Int
  | CanFail.div, x, y =>
    if y == 0 then
      Except.error s!"Tried to divide {x} by zero"
    else pure (x / y)

def applyPrim [Monad m] (applySpecial : special → Int → Int → m Int) : Prim special → Int → Int → m Int
  | Prim.plus, x, y => pure (x + y)
  | Prim.minus, x, y => pure (x - y)
  | Prim.times, x, y => pure (x * y)
  | Prim.other op, x, y => applySpecial op x y

def evaluateM [Monad m] (applySpecial : special → Int → Int → m Int): Expr (Prim special) → m Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateM applySpecial e1 >>= fun v1 =>
    evaluateM applySpecial e2 >>= fun v2 =>
    applyPrim applySpecial p v1 v2

作用なし

Empty 型はコンストラクタを持たないため、ScalaやKotlinの Nothing 型のように値を持ちません。ScalaとKotlinでは、Nothing 型はプログラムをクラッシュさせたり、例外を投げたり、常に無限ループに陥ったりする関数のような、決して結果を返さない計算の表現に用いることができます。関数やメソッドへの Nothing 型の引数は、適切な引数値が存在しないため、デッドコードを表します。Leanは無限ループや例外をサポートしていないものの、Empty は型システムに対して、関数を呼び出すことができないことを示すものとして有用です。E がコンストラクタを持たない型の式である時、nomatch E という構文を使うと、E を絶対に呼ぶことができないことを受けて、現在の式が結果を返す必要がないことをLeanに示します。

Prim のパラメータとして Empty を使用することは、Prim.plus 、Prim.minus 、Prim.times 以外に追加のケースが無いことを意味します。2つの整数に Empty 型の演算子を適用する関数は決して呼び出すことができないため、この関数は結果を返す必要はありません。したがって、これは 任意の モナドで使うことができます：

def applyEmpty [Monad m] (op : Empty) (_ : Int) (_ : Int) : m Int :=
  nomatch op

恒等モナドである Id と一緒に使うことで、何の作用も持たない式を評価することができます：

open Expr Prim in
#eval evaluateM (m := Id) applyEmpty (prim plus (const 5) (const (-14)))

-9

非決定論探索

0による除算に遭遇した際に単純に失敗させる代わりに、その計算を諦めて別の入力を試すのも賢い選択でしょう。適切なモナドがあれば、同じ evaluateM を使って失敗しない答えの 集合 を非決定論的に探索することができます。これには除算に加えて、結果の選択肢を指定する手段が必要になります。これを行う1つの方法は、失敗しない結果を探索している間に、評価者に引数のどちらかを選ぶように指示する関数 choose を式の言語に追加することです。

これで評価器の結果は単一の値ではなく値の多重集合になります。多重集合への評価のルールは以下の通りです：

  • 定数 \( n \) は単集合 \( {n} \) に評価されます。
  • 除算以外の算術演算子はオペランド1のデカルト積から各ペアに対して呼び出されます。したがって \( X + Y \) は \( \{ x + y \mid x ∈ X, y ∈ Y \} \) に評価されます。
  • 除算 \( X / Y \) は \( \{ x / y \mid x ∈ X, y ∈ Y, y ≠ 0\} \) に評価されます。つまり、 \( Y \) に含まれるすべての \( 0 \) の値は捨てられます。
  • 選択 \( \mathrm{choose}(x, y) \) は \( \{ x, y \} \) に評価されます。

例えば、 \( 1 + \mathrm{choose}(2, 5) \) は \( \{ 3, 6 \} \) に、 \(1 + 2 / 0 \) は \( \{\} \) に、 \( 90 / (\mathrm{choose}(-5, 5) + 5) \) は \( \{ 9 \} \) にそれぞれ評価されます。集合ではなく多重集合を使うことで、要素の一意性チェックの必要性を除いてコードを単純化します。

この非決定論的な作用を表現するモナドは答えが無い状況と、少なくとも1つの答えとそれ以外の答えがある状況を表現できなければなりません：

inductive Many (α : Type) where
  | none : Many α
  | more : α → (Unit → Many α) → Many α

このデータ型は List にとってもそっくりです。異なる点として、リストでは cons で後続のリストを格納していたのに対して、more は必要に応じて後続の値を計算する関数を格納しています。つまり、Many の利用者は、ある程度の数の結果が見つかった時点で検索を停止することができます。

単一の結果はそれ以上の結果を返さない more コンストラクタで表されます：

def Many.one (x : α) : Many α := Many.more x (fun () => Many.none)

計算結果の2つの多重集合の和は1つ目の多重集合が空かどうかをチェックすることによって計算できます。もし空であれば、2番目の多重集合が和の結果になります。そうでない場合、和は1つ目の多重集合の最初の要素に、1つ目の残りと2つ目の多重集合の和を続けたもので構成されます：

def Many.union : Many α → Many α → Many α
  | Many.none, ys => ys
  | Many.more x xs, ys => Many.more x (fun () => union (xs ()) ys)

探索プロセスをリストから始めると便利です。Many.fromList はリストを結果の多重集合に変換します：

def Many.fromList : List α → Many α
  | [] => Many.none
  | x :: xs => Many.more x (fun () => fromList xs)

同様に、検索の実行結果に対して、そこから何個かの値の抽出、もしくはすべて抽出できると便利です：

def Many.take : Nat → Many α → List α
  | 0, _ => []
  | _ + 1, Many.none => []
  | n + 1, Many.more x xs => x :: (xs ()).take n

def Many.takeAll : Many α → List α
  | Many.none => []
  | Many.more x xs => x :: (xs ()).takeAll

Monad Many インスタンスは bind 演算子を必要とします。非決定論的検索において、2つの演算の紐づけは、まず1つ目のステップからすべての可能性を取り出し、それらすべてについて後続のプログラムを走らせて、得られた結果の和を取ることで構成されます。言い換えると、例えば1つ目のステップで3つの可能性が返された場合、2つ目のステップではそれらすべてを試す必要があります。2つ目のステップでは各入力について任意の数の答えが返されるため、それらの和を取ることで探索空間全体を表現することになります。

def Many.bind : Many α → (α → Many β) → Many β
  | Many.none, _ =>
    Many.none
  | Many.more x xs, f =>
    (f x).union (bind (xs ()) f)

Many.one と Many.bind はモナドの約定に従います。Many.bind (Many.one v) f が f v と同じであることをチェックするには、式として取りうるものを可能な限り評価することから始めます：

Many.bind (Many.one v) f
===>
Many.bind (Many.more v (fun () => Many.none)) f
===>
(f v).union (Many.bind Many.none f)
===>
(f v).union Many.none

空の多重集合は union に対して右単位であるので、答えは f v に等しくなります。Many.bind v Many.one が v と等しいことをチェックするには、bind が v の各要素に Many.one を適用した和を取ることを考えてみましょう。言い換えると、もし v が {v1, v2, v3, ..., vn} の形式である場合、Many.bind v Many.one は {v1} ∪ {v2} ∪ {v3} ∪ ... ∪ {vn} であり、これは {v1, v2, v3, ..., vn} です。

最後に、Many.bind の結合性のチェックは、Many.bind (Many.bind bind v f) g が Many.bind v (fun x => Many.bind (f x) g) と同じであることを確かめましょう。もし v が {v1, v2, v3, ..., vn} の形式である場合、まず以下のようになり：

Many.bind v f
===>
f v1 ∪ f v2 ∪ f v3 ∪ ... ∪ f vn

これから以下が導かれ、

Many.bind (Many.bind bind v f) g
===>
Many.bind (f v1) g ∪
Many.bind (f v2) g ∪
Many.bind (f v3) g ∪
... ∪
Many.bind (f vn) g

また、同様に、

Many.bind v (fun x => Many.bind (f x) g)
===>
(fun x => Many.bind (f x) g) v1 ∪
(fun x => Many.bind (f x) g) v2 ∪
(fun x => Many.bind (f x) g) v3 ∪
... ∪
(fun x => Many.bind (f x) g) vn
===>
Many.bind (f v1) g ∪
Many.bind (f v2) g ∪
Many.bind (f v3) g ∪
... ∪
Many.bind (f vn) g

したがって、両辺は等しくなるため、Many.bind は結合的となります。

結果としてモナドのインスタンスは次のようになります：

instance : Monad Many where
  pure := Many.one
  bind := Many.bind

このモナドを使って、試しにリスト中の足し合わせたら15になるすべての組み合わせを計算してみます：

def addsTo (goal : Nat) : List Nat → Many (List Nat)
  | [] =>
    if goal == 0 then
      pure []
    else
      Many.none
  | x :: xs =>
    if x > goal then
      addsTo goal xs
    else
      (addsTo goal xs).union
        (addsTo (goal - x) xs >>= fun answer =>
         pure (x :: answer))

探索プロセスはリストに対して再帰的に行われます。空のリストに対しては、ゴールが 0 であれば探索を成功とし、そうでなければ失敗とします。リストが空でない場合、2つの可能性があります：リストの先頭がゴールより大きい場合とそうでない場合であり、前者の場合はどんな成功した探索にも寄与することができず、対して後者は可能性があります。もしリストの先頭が候補 ではない 場合、探索は後続のリストに対して実行されます。もし先頭要素が候補である場合、Many.union で組み合わされる2つの可能性があります：すなわち解が先頭要素を含む場合とそうでない場合です。先頭を含まない解は後続のリストに対して再帰することで得られ、先頭を含む解はゴールから先頭の値を引き、それと後続のリストに対する再帰呼び出し結果にもとの先頭要素を付け加えることで得られます。

結果の多重集合を生成する算術の評価器に戻ると、both と neither 演算子は以下のように書くことができます：

inductive NeedsSearch
  | div
  | choose

def applySearch : NeedsSearch → Int → Int → Many Int
  | NeedsSearch.choose, x, y =>
    Many.fromList [x, y]
  | NeedsSearch.div, x, y =>
    if y == 0 then
      Many.none
    else Many.one (x / y)

これらの演算子を用いて、先ほどの例を評価することができます：

open Expr Prim NeedsSearch

#eval (evaluateM applySearch (prim plus (const 1) (prim (other choose) (const 2) (const 5)))).takeAll

[3, 6]

#eval (evaluateM applySearch (prim plus (const 1) (prim (other div) (const 2) (const 0)))).takeAll

[]

#eval (evaluateM applySearch (prim (other div) (const 90) (prim plus (prim (other choose) (const (-5)) (const 5)) (const 5)))).takeAll

[9]

カスタムの環境

評価器は文字列を演算子として使えるようにし、文字列から演算子の実処理へのマッピングを提供することで、評価器をユーザが拡張できるようにすることができます。例えば、ユーザは剰余演算子や2つの引数に対して大きい方を返すものなどを評価器に拡張することができます。関数名から関数の実装へのマッピングは 環境 （environment）と呼ばれます。

環境は各再帰呼び出しで渡される必要があります。知らない人からすると、evaluateM は環境を保持するために余分な引数を必要とし、この引数は呼び出しのたびに渡される必要があると思われるかもしれません。しかし、このように引数を渡すこともモナドの一種であるため、適切な Monad インスタンスを使用することで、評価器を変更せずに使用することができます。

関数をモナドとして使用することは一般的に リーダ （reader）モナドと呼ばれます。リーダモナドで式を評価する場合、以下のルールが用いられます：

  • 定数 \( n \) は定数関数 \( λ e . n \) に評価され、
  • 算術演算子は引数をオペランドに渡す関数に評価され、したがって \( f + g \) が \( λ e . f(e) + g(e) \) に評価され、
  • カスタム演算子はカスタム演算子を引数に適用した結果に評価され、したがって \( f \ \mathrm{OP}\ g \) は未知の演算子に対してのフォールバックとして \( 0 \) を提供するようにして、以下のように評価されます。 \[ λ e . \begin{cases} h(f(e), g(e)) & \mathrm{if}\ e\ \mathrm{contains}\ (\mathrm{OP}, h) \\ 0 & \mathrm{otherwise} \end{cases} \]

    Leanでリーダモナドを定義するには、まず Reader 型クラスとユーザが環境を把握するための作用を定義します：

    def Reader (ρ : Type) (α : Type) : Type := ρ → α

def read : Reader ρ ρ := fun env => env

    慣例として、環境はギリシャ文字 ρ （発音は「rho」）が用いられます。

    算術式の定数が定数関数に評価されるという事実から Reader に対する pure の適切な定義が定数関数であることが示唆されます：

    def Reader.pure (x : α) : Reader ρ α := fun _ => x

    他方、bind は少々トリッキーです。この関数の型は Reader ρ α → (α → Reader ρ β) → Reader ρ β になります。この型は Reader の定義を展開した (ρ → α) → (α → ρ → β) → ρ → β によって理解しやすくなります。これは第1引数として環境を受け入れる関数を受け取り、第2引数は環境を環境を受け入れる関数の結果を、さらに別の環境を受け入れる関数に変換しなければなりません。これらを組み合わせた結果自体が環境を待つような関数となります。

    Leanを対話的に使うことで、この関数を書く手助けを得ることができます。最初のステップは、できるだけ多くのヒントを得るために、引数と戻り値の型をアンダースコア付きで明示的に書くことです：

    def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  _

    Leanはスコープ内でどの変数が使用可能か、そしてその結果に期待される型を記述したメッセージを提示します。地下鉄の入り口に似ていることから ターンスタイル と呼ばれる記号 ⊢ は、このメッセージでは ρ → β であるようなローカル変数と期待される型を分離しています：

    don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
⊢ ρ → β

    戻り値の型が関数であるため、最初のステップとしてアンダースコアの前に fun を付けるのが良いでしょう：

    def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => _

    この結果で得られるメッセージには、関数の引数がローカル変数として表示されるようになります：

    don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ
⊢ β

    コンテキスト内で β を生成できるのは next のみですが、これを得るには引数が2つ必要です。それぞれの引数にもアンダースコアを設定してみます：

    def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => next _ _

    2つのアンダースコアは以下に示している、それぞれに関連したメッセージを持ちます：

    don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ
⊢ α

    don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ
⊢ ρ

    1つ目のアンダースコアに取り掛かると、コンテキストで α を生み出すことができるのはただ1つだけ、すなわち result だけです：

    def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => next (result _) _

    ここで両方のアンダースコアは同じエラーになります：

    don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ
⊢ ρ

    嬉しいことに、どちらのアンダースコアも env で置き換えることができ、以下を得ます：

    def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => next (result env) env

    最終的なバージョンは Reader の展開を元に戻し、明示的な詳細を掃除することで得られます：

    def Reader.bind (result : Reader ρ α) (next : α → Reader ρ β) : Reader ρ β :=
  fun env => next (result env) env

    このような「型に従う」だけで正しい関数が書けるとは限らず、出来上がったプログラムを理解できないリスクもあります。しかし、書いていないプログラムよりも出来上がったプログラムの方が理解しやすいこともあり得ますし、アンダースコアを埋めていく過程で気づきを得ることもあります。今回の場合、Reader.bind は Id に対する bind と同じように動作しますが、追加の引数を受け取り、それを引数に渡すという点が異なり、この直観はこれがどう動くかということへの理解を助けます。

    定数関数を生成する Reader.pure と Reader.bind はモナドの約定に従います。Reader.bind (Reader.pure v) f が f v に等しいことを確認するには、最後のステップまで定義を置き換えれば十分です：

    Reader.bind (Reader.pure v) f
===>
fun env => f ((Reader.pure v) env) env
===>
fun env => f ((fun _ => v) env) env
===>
fun env => f v env
===>
f v

    すべての関数 f について、fun x => f x は f と同じであるため、約定の最初の部分が満たされます。Reader.bind r Reader.pure が r と同じであることを確認する場合にも同じテクニックが有効です：

    Reader.bind r Reader.pure
===>
fun env => Reader.pure (r env) env
===>
fun env => (fun _ => (r env)) env
===>
fun env => r env

    リーダのアクション r はそれ自体が関数であるため、これは r と等しくなります。結合性をチェックするには、Reader.bind (Reader.bind r f) g と Reader.bind r (fun x => Reader.bind (f x) g) の両方について同じことを行います：

    Reader.bind (Reader.bind r f) g
===>
fun env => g ((Reader.bind r f) env) env
===>
fun env => g ((fun env' => f (r env') env') env) env
===>
fun env => g (f (r env) env) env

    Reader.bind r (fun x => Reader.bind (f x) g)
===>
Reader.bind r (fun x => fun env => g (f x env) env)
===>
fun env => (fun x => fun env' => g (f x env') env') (r env) env
===>
fun env => (fun env' => g (f (r env) env') env') env
===>
fun env => g (f (r env) env) env

    以上より、Monad (Reader ρ) インスタンスが成立します：

    instance : Monad (Reader ρ) where
  pure x := fun _ => x
  bind x f := fun env => f (x env) env

    式評価器に渡されるカスタム環境はペアのリストとして表すことができます：

    abbrev Env : Type := List (String × (Int → Int → Int))

    例えば、exampleEnv は最大値と剰余関数を保持します：

    def exampleEnv : Env := [("max", max), ("mod", (· % ·))]

    Leanには、ペアのリストのキーに関連付けられた値を見つける関数 List.lookup がすでに存在するため、applyPrimReader はカスタム関数が環境に存在するかどうかをチェックするだけでよくなります。関数が不明な場合は 0 を返します：

    def applyPrimReader (op : String) (x : Int) (y : Int) : Reader Env Int :=
  read >>= fun env =>
  match env.lookup op with
  | none => pure 0
  | some f => pure (f x y)

    applyPrimReader と式と一緒に evaluateM を使うと、環境が必要な関数になります。幸運なことに、exampleEnv が利用できます：

    open Expr Prim in
#eval evaluateM applyPrimReader (prim (other "max") (prim plus (const 5) (const 4)) (prim times (const 3) (const 2))) exampleEnv

    9

    Many と同様に、Reader はほとんどの言語でエンコードすることが難しい作用の例ですが、型クラスとモナドによって他の作用と同じような利便性が提供されます。Common LispやClojure、Emacs Lispにある動的変数や特殊変数は Reader のように使うことができます。同様に、SchemeやRacketのパラメータオブジェクトは Reader に対応する作用です。Kotlinのイディオムであるコンテキストオブジェクトは似たような問題を解決することができますが、基本的には関数の引数を自動的に渡すための手段であるため、このイディオムは言語内の作用というよりはリーダモナドとしてエンコードされたものです。

    演習問題

    約定のチェック

    State σ と Except ε のモナドの約定をチェックしてください。

    失敗付きのリーダ

    リーダモナドの例を修正して、カスタム演算子が定義されていない場合に単に0を返すのではなく、失敗を示すことができるようにしてください。つまり、以下の定義に対して：

    def ReaderOption (ρ : Type) (α : Type) : Type := ρ → Option α

def ReaderExcept (ε : Type) (ρ : Type) (α : Type) : Type := ρ → Except ε α

    以下を行ってください：

    1. 適切な pure と bind 関数を書いてください。
    2. これらの関数が Monad の約定を満たすことをチェックしてください。
    3. ReaderOption と ReaderExcept に対しての Monad インスタンスを書いてください。
    4. 適切な applyPrim 演算子を定義し、いくつかの式に対して evaluateM を使ってテストしてください。

    評価器の追跡

    WithLog 型を評価器と一緒に用いることで、いくつかの演算の追跡をオプションで追加することができます。特に、ToTrace 型は与えられた演算子を追跡するためのシグナルを提供します：

    inductive ToTrace (α : Type) : Type where
  | trace : α → ToTrace α

    追跡付きの評価器では、式は Expr (Prim (ToTrace (Prim Empty))) 型でなければなりません。これは、式の演算子が加算と減算、乗算で構成され、それぞれを追跡したもので補強していることを示します。一番内側の Empty によって、trace の内部には特別な演算子は無く、基本的な3つの演算子だけであることを示しています。

    以下を行ってください：

    1. Monad (WithLog logged) インスタンスを実装してください。
    2. 追跡される演算子をその引数に適用し、演算子とその引数をログ出力するための applyTraced 関数を書いてください。型は ToTrace (Prim Empty) → Int → Int → WithLog (Prim Empty × Int × Int) Int です。

    もし演習問題を正しく解けたのなら、

    open Expr Prim ToTrace in
#eval evaluateM applyTraced (prim (other (trace times)) (prim (other (trace plus)) (const 1) (const 2)) (prim (other (trace minus)) (const 3) (const 4)))

    は以下の結果になるはずです。

    { log := [(Prim.plus, 1, 2), (Prim.minus, 3, 4), (Prim.times, 3, -1)], val := -3 }

    ヒント：Prim Empty 型の値は結果のログに表示されます。それらを #eval の結果として表示するには、以下のインスタンスが必要です：

    deriving instance Repr for WithLog
deriving instance Repr for Empty
deriving instance Repr for Prim
    1

    原文はoperatorsだがオペランドのミス？