モナド組み立てキット

ReaderT だけが便利なモナド変換子ではありません。本節では、さらに多くの変換子について説明します。各モナド変換子は以下のように構成されています：

  1. モナドを引数に取る定義もしくはデータ型 T 。これは (Type u → Type v) → Type u → Type v のような型を持ちますが、モナドの前に別で引数を受け取ることもできます。
  2. Monad m のインスタンスに依存した T m の Monad インスタンス。これにより変換されたモナドをモナドとして使うことができます。
  3. 任意のモナド m に対して m α 型のアクションを T m α 型のアクションに変換する MonadLift インスタンス。これにより、変換後のモナドでベースとなったモナドのアクションを使用できるようになります。

さらに、ベースとなった Monad インスタンスがモナドの約定に従うのであれば、変換子の Monad インスタンスは Monad の約定に従わなければなりません。加えて、monadLift (pure x) は変換後のモナドでは pure x と等価になるべき、また monadLift は monadLift (x >>= f) が monadLift x >>= fun y => monadLift (f y) と同じになるように bind に対して分配されるべきです。

多くのモナド変換子はさらに MonadReader というスタイルでモナドで利用可能な実際の作用を記述する型クラスを定義しています。これによりコードが柔軟さを増します：インタフェースにのみ依存するプログラムを書くことができるようになり、ベースのモナドに対して特定の変換子によって実装されることが要求されません。型クラスはプログラムが要求を表現するための方法であり、モナド変換子はこれらの要求を満たすための便利なツールです。

OptionT による失敗

Option モナドで表現される失敗と Except モナドで表現される例外はどちらもそれぞれ対応する変換子があります。Option の場合、別のモナドに失敗を追加するには、そのモナドが通常なら含んでいる α 型ではなく Option α 型を保持するようにすることで可能です。例えば、IO (Option α) はいつも α 型を返すとは限らないような IO アクションを表します。これよりモナド変換子 OptionT の定義が導かれます：

def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
  m (Option α)

実際の OptionT の例として、ユーザに質問するプログラムを考えてみましょう。関数 getSomeInput は一行の入力を受け取り、その両端から空白を取り除きます。切り取られた入力が空でなければそれを返しますが、空白以外の文字がなければ関数は失敗します：

def getSomeInput : OptionT IO String := do
  let input ← (← IO.getStdin).getLine
  let trimmed := input.trim
  if trimmed == "" then
    failure
  else pure trimmed

この関数を用いたアプリケーションとして、ユーザの名前と好きなカブトムシの種類を確認するものを作れます：

structure UserInfo where
  name : String
  favoriteBeetle : String

ユーザに入力を求めても、IO だけを使う関数のような冗長さはありません：

def getUserInfo : OptionT IO UserInfo := do
  IO.println "What is your name?"
  let name ← getSomeInput
  IO.println "What is your favorite species of beetle?"
  let beetle ← getSomeInput
  pure ⟨name, beetle⟩

しかし、この関数は単なる IO ではなく OptionT IO コンテキストで実行されるため、最初の getSomeInput の呼び出しに失敗すると、制御がカブトムシに関する質問に到達せずに getUserInfo 全体も失敗します。メインの関数である interact は純粋な IO のコンテキストで getUserInfo を呼び出し、これによってその中の Option をパターンマッチすることで呼び出しが成功したか失敗したかチェックすることができます。

def interact : IO Unit := do
  match ← getUserInfo with
  | none => IO.eprintln "Missing info"
  | some ⟨name, beetle⟩ => IO.println s!"Hello {name}, whose favorite beetle is {beetle}."

OptionT のモナドインスタンス

モナドインスタンスを書いてみると難点が明らかになります。型に基づくと、pure はベースとなるモナド m の pure を some と共に使用する必要があります。ちょうど Option の bind が最初の引数で分岐し、none を伝播するように、OptionT の bind は最初の引数を構成するモナドアクションを実行し、その結果で分岐して none を伝播しなければなりません。この構想に従うと以下の定義が得られますが、Leanはこれを受け入れません：

instance [Monad m] : Monad (OptionT m) where
  pure x := pure (some x)
  bind action next := do
    match (← action) with
    | none => pure none
    | some v => next v

エラーメッセージには不可解な型の不一致が示されます：

application type mismatch
  pure (some x)
argument
  some x
has type
  Option α✝ : Type ?u.25
but is expected to have type
  α✝ : Type ?u.25

問題はLeanが pure を使用するにあたって間違った Monad インスタンスを選択していることです。同様のエラーは bind の定義でも発生します。これに対する1つの解決策は、型注釈を使ってLeanに正しい Monad インスタンスを教えてあげることです：

instance [Monad m] : Monad (OptionT m) where
  pure x := (pure (some x) : m (Option _))
  bind action next := (do
    match (← action) with
    | none => pure none
    | some v => next v : m (Option _))

この解決策は機能しますが、エレガントではないですし、コードも少々煩雑になります。

別の解決策は、型注釈がLeanを正しいインスタンスに導く関数を定義することです。実は OptionT は構造体として定義することもできます：

structure OptionT (m : Type u → Type v) (α : Type u) : Type v where
  run : m (Option α)

これにより、コンストラクタ OptionT.mk とフィールドアクセサ OptionT.run が型クラス推論を正しいインスタンスに導くため問題は解決します。この解決策の欠点は、直接の定義はコンパイル時のみの特徴である一方で、構造体の値を使用するコードでは実行時に構造体の値のメモリ確保と解放を繰り返し行う必要があることです。両方の長所を生かすには、OptionT.mk と OptionT.run と同じ役割を果たしつつ、しかし直接の定義で動くような関数を定義することです：

def OptionT.mk (x : m (Option α)) : OptionT m α := x

def OptionT.run (x : OptionT m α) : m (Option α) := x

どちらの関数も入力を変更せずに返しますが、OptionT のインタフェースを提示するつもりのコードと、ベースのモナド m のインタフェースを提示するつもりのコードとの境界をはっきりさせます。これらの補助関数を使うことで、Monad インスタンスはより読みやすくなります：

instance [Monad m] : Monad (OptionT m) where
  pure x := OptionT.mk (pure (some x))
  bind action next := OptionT.mk do
    match ← action with
    | none => pure none
    | some v => next v

ここで、OptionT.mk を使うことによって、その引数が m のインタフェースを使用するコードと見做されるべきことが示され、これによってLeanは正しい Monad インスタンスを選択することができます。

モナドインスタンスを定義した後、モナドの約定が満たされていることをチェックするのは良い考えです。最初のステップは bind (pure v) f が f v と同じであることを示すことです。以下がその手順です：

bind (pure v) f
={ Unfolding the definitions of bind and pure }= 
OptionT.mk do
  match ← pure (some v) with
  | none => pure none
  | some x => f x
={ Desugaring nested action syntax }= 
OptionT.mk do
  let y ← pure (some v)
  match y with
  | none => pure none
  | some x => f x
={ Desugaring do-notation }= 
OptionT.mk
  (pure (some v) >>= fun y =>
    match y with
    | none => pure none
    | some x => f x)
={ Using the first monad rule for m }= 
OptionT.mk
  (match some v with
   | none => pure none
   | some x => f x)
={ Reduce match }= 
OptionT.mk (f v)
={ Definition of OptionT.mk }= 
f v

2つ目のルールは bind w pure が w に等しいというものです。これを示すために、bind と pure の定義を展開してみましょう：

OptionT.mk do
    match ← w with
    | none => pure none
    | some v => pure (some v)

このパターンマッチでは、どちらのケースでもマッチされたパターンと同じ結果になります。つまり、これは w >>= fun y => pure y と等価であり、m の2番目のモナドルールのインスタンスです。

最後のルールは bind (bind v f) g が bind v (fun x => bind (f x) g) と同じというものです。これも bind と pure の定義を展開し、ベースのモナド m に委譲することで同じようにチェックすることができます。

Alternative インスタンス

OptionT の便利な使用例として、Alternative 型クラスを使用するというものがあります。成功した結果は pure によって既に示されており、Alternative の failure メソッドと orElse メソッドによって複数のサブプログラムから最初に成功した結果を返すプログラムを書くことができます：

instance [Monad m] : Alternative (OptionT m) where
  failure := OptionT.mk (pure none)
  orElse x y := OptionT.mk do
    match ← x with
    | some result => pure (some result)
    | none => y ()

持ち上げ

アクションを m から OptionT m に持ち上げるには計算結果を some で囲むだけで良いです：

instance [Monad m] : MonadLift m (OptionT m) where
  monadLift action := OptionT.mk do
    pure (some (← action))

例外

モナド変換子版の Except は同じくモナド変換子版の Option にとてもよく似ています。型 m α の何かしらのモナドのアクションに型 ε の例外を追加するには α に例外を追加して m (Except ε α) 型を生成することでできます：

def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
  m (Except ε α)

OptionT では mk と run 関数を使って型チェッカに正しい Monad インスタンスを導いていました。この技法は ExceptT でも有効です：

def ExceptT.mk {ε α : Type u} (x : m (Except ε α)) : ExceptT ε m α := x

def ExceptT.run {ε α : Type u} (x : ExceptT ε m α) : m (Except ε α) := x

ExceptT の Monad インスタンスも OptionT 版のインスタンスにそっくりです。唯一の違いは none の代わりに特定のエラー値を伝播することです：

instance {ε : Type u} {m : Type u → Type v} [Monad m] : Monad (ExceptT ε m) where
  pure x := ExceptT.mk (pure (Except.ok x))
  bind result next := ExceptT.mk do
    match ← result with
    | .error e => pure (.error e)
    | .ok x => next x

ExceptT.mk と ExceptT.run の型注釈にはひっそりとですが細かい指定があります：α と ε の宇宙レベルが明示的にアノテーションされています。もしこれらが明示的にアノテーションされていない場合、Leanは α と ε に異なる多相宇宙変数を割り当てたより一般的な型注釈を生成します。しかし、ExceptT の定義ではどちらも m の引数に指定できるため、同じ宇宙であることが期待されます。これにより Monad インスタンスにて、宇宙レベルの解決に失敗してしまう事態を引き起こす可能性があります：

def ExceptT.mk (x : m (Except ε α)) : ExceptT ε m α := x

instance {ε : Type u} {m : Type u → Type v} [Monad m] : Monad (ExceptT ε m) where
  pure x := ExceptT.mk (pure (Except.ok x))
  bind result next := ExceptT.mk do
    match (← result) with
    | .error e => pure (.error e)
    | .ok x => next x

stuck at solving universe constraint
  max ?u.12144 ?u.12145 =?= u
while trying to unify
  ExceptT ε m α✝
with
  (ExceptT ε m α✝) ε m α✝

この手のエラーメッセージは通常、制約不足の宇宙変数が原因です。これを診断するのは難しいですが、解析の最初の一歩としてある定義で再利用され、ほかの定義では再利用されていない宇宙変数を探すと良いでしょう。

Option とは異なり、Except データ型は通常、データ構造として使用されることはありません。いつも Monad インスタンスを持った制御構造として使用されます。このことから、Except ε のアクションを ExceptT ε m に持ち上げてベースのモナド m のアクションのようにすることは合理的でしょう。例外の作用しか持たないアクションはモナド m からの作用を持つことができないため、Except のアクションを ExceptT のアクションに持ち上げるには m の pure で包みます：

instance [Monad m] : MonadLift (Except ε) (ExceptT ε m) where
  monadLift action := ExceptT.mk (pure action)

m のアクションはその中に例外を持たないため、その値を Except.ok で包む必要があります。これは Functor が Monad のスーパークラスであることを利用して実現できます。つまり、関数を任意のモナドの計算結果に適用するために Functor.map を利用します：

instance [Monad m] : MonadLift m (ExceptT ε m) where
  monadLift action := ExceptT.mk (.ok <$> action)

例外の型クラス

例外処理は基本的に2つの操作から成り立ちます：例外を投げる機能と例外から回復する機能です。これまでは、この2つの機能はそれぞれ Except のコンストラクタとパターンマッチを使って実現してきました。しかし、これでは例外を使用するプログラムを例外処理作用に限定した実装になってしまいます。型クラスを使用してこれらの操作をキャプチャすることで、例外を使用するプログラムで例外のスローとキャッチをサポートする 任意の モナドを使うことができるようになります。

例外を投げるには例外を引数として取り、モナドのアクションが要求される任意のコンテキストで可能であるべきです。ここで言う「任意のコンテキスト」は m α と書くことで型として記述できます。なぜなら任意の型を生成することはできないため、throw 操作はプログラム中のその部分から制御を離脱させるようなことをしなければならないからです。例外のキャッチは任意のモナドのアクションと一緒にハンドラを受け入れるべきです。このハンドラは例外からアクションの型に戻る方法を説明するべきです：

class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) where
  throw : ε → m α
  tryCatch : m α → (ε → m α) → m α

MonadExcept の宇宙レベルは ExceptT のそれとは異なります。ExceptT では ε と α は同じレベルでしたが、MonadExcept ではそのような制限は課しません。これは MonadExcept では例外の値を m の中に置くことがないからです。この最大限に一般的な宇宙シグネチャから、この定義において ε と α が完全に独立しているということが認識されます。より一般的であるということは、型クラスがより多様な型に対してインスタンス化できるということです。

MonadExcept を使ったプログラムの例として簡単な割り算サービスを考えてみましょう。プログラムは2つのパーツに分けられます：ユーザにエラーハンドリング付きで文字列ベースのフロントエンドと、実際に割り算を行うバックエンドです。フロントエンドとバックエンドはどちらも例外を投げます。前者は不正な入力に対して、後者はゼロ除算エラーに対してです。これらの例外は以下の帰納型で表されます：

inductive Err where
  | divByZero
  | notANumber : String → Err

バックエンドはゼロであるかをチェックし、可能な場合は割り算を実行します：

def divBackend [Monad m] [MonadExcept Err m] (n k : Int) : m Int :=
  if k == 0 then
    throw .divByZero
  else pure (n / k)

フロントエンドの補助関数 asNumber は渡された文字列が数値でない場合に例外を発生させます。フロントエンド全体は入力を Int に変換し、バックエンドを呼びつつ例外が発生した際には読みやすい文字列のエラーを返します：

def asNumber [Monad m] [MonadExcept Err m] (s : String) : m Int :=
  match s.toInt? with
  | none => throw (.notANumber s)
  | some i => pure i

def divFrontend [Monad m] [MonadExcept Err m] (n k : String) : m String :=
  tryCatch (do pure (toString (← divBackend (← asNumber n) (← asNumber k))))
    fun
      | .divByZero => pure "Division by zero!"
      | .notANumber s => pure s!"Not a number: \"{s}\""

例外のスローとキャッチはよく使われる機能であるため、Leanでは MonadExcept を使った特別な記法を用意しています。+ が HAdd.hAdd の省略形だったように、try と catch は tryCatch メソッドの省略形として使用できます：

def divFrontend [Monad m] [MonadExcept Err m] (n k : String) : m String :=
  try
    pure (toString (← divBackend (← asNumber n) (← asNumber k)))
  catch
    | .divByZero => pure "Division by zero!"
    | .notANumber s => pure s!"Not a number: \"{s}\""

Except と ExceptT に加えて、 MonadExcept のインスタンスには一見すると例外とは思えないような型に対しての便利なインスタンスが存在します。例えば、Option による失敗は何のデータも含まない例外を投げていると見ることができるため、Option と一緒に try ... catch ... 構文を使うための MonadExcept Unit Option インスタンスが存在します。

状態

あるモナドにて可変状態のシミュレーションを行えるようにするには、そのモナドのアクションが引数として開始状態を受け取り、その結果と一緒に最終状態を返すことでできます。状態モナドの束縛演算子はあるアクションの最終状態を次のアクションへ引数として渡し、プログラム中の状態を縫い合わせます。このパターンはモナド変換子でも表現されます：

def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
  σ → m (α × σ)

ここでもまた、このモナドのインスタンスは State のインスタンスに非常に似ています。唯一の違いは、入力と出力の状態が純粋なコードではなく、ベースのモナドの中で受け渡され、返される点です：

instance [Monad m] : Monad (StateT σ m) where
  pure x := fun s => pure (x, s)
  bind result next := fun s => do
    let (v, s') ← result s
    next v s'

これに対応する型クラスは get と set メソッドを持ちます。get と set の欠点の一つに、状態を更新する際に間違った状態をあまりにも容易に set できるようにしてしまうというものがあります。これは状態を取得・更新し、更新された状態を保存するという流れがプログラムによっては自然な書き方だからです。例えば、以下のプログラムは文字列中の発音区別のない英語の母音と子音の数をかぞえます：

structure LetterCounts where
  vowels : Nat
  consonants : Nat
deriving Repr

inductive Err where
  | notALetter : Char → Err
deriving Repr

def vowels :=
  let lowerVowels := "aeiuoy"
  lowerVowels ++ lowerVowels.map (·.toUpper)

def consonants :=
  let lowerConsonants := "bcdfghjklmnpqrstvwxz"
  lowerConsonants ++ lowerConsonants.map (·.toUpper )

def countLetters (str : String) : StateT LetterCounts (Except Err) Unit :=
  let rec loop (chars : List Char) := do
    match chars with
    | [] => pure ()
    | c :: cs =>
      let st ← get
      let st' ←
        if c.isAlpha then
          if vowels.contains c then
            pure {st with vowels := st.vowels + 1}
          else if consonants.contains c then
            pure {st with consonants := st.consonants + 1}
          else -- modified or non-English letter
            pure st
        else throw (.notALetter c)
      set st'
      loop cs
  loop str.toList

ここで set st' の代わりに set st といとも簡単に書き間違えうるのです。大きなプログラムでは、このようなミスは解析の難しいバグにつながる可能性があります。

get の呼び出しにネストしたアクションを使えばこの問題は解決しますが、いつでもこのやり方が通用するわけではありません。例えば、構造体のあるフィールドを別の2つのフィールドをもとに更新する関数を考えます。この場合、get に対するネストされたアクションを別々に2度呼び出す必要があります。Leanのコンパイラは値の参照が1つの場合にのみ有効な最適化を含むため、状態への参照が重複するとコードが著しく遅くなる可能性があります。潜在的なパフォーマンスの問題と潜在的なバグの両方を回避するには、状態の変換に関数を用いる modify を使用することで対処できます：

def countLetters (str : String) : StateT LetterCounts (Except Err) Unit :=
  let rec loop (chars : List Char) := do
    match chars with
    | [] => pure ()
    | c :: cs =>
      if c.isAlpha then
        if vowels.contains c then
          modify fun st => {st with vowels := st.vowels + 1}
        else if consonants.contains c then
          modify fun st => {st with consonants := st.consonants + 1}
        else -- modified or non-English letter
          pure ()
      else throw (.notALetter c)
      loop cs
  loop str.toList

この型クラスは modify に似た modifyGet という関数を持っており、これは戻り値の計算と古い状態の変換の両方を一度に行うことができます。この関数は最初の要素が戻り値で2番目の要素が新しい状態であるペアを返します；modify は Unit のコンストラクタを modifyGet で使われているこのペアにただ追加しただけの関数です：

def modify [MonadState σ m] (f : σ → σ) : m Unit :=
  modifyGet fun s => ((), f s)

MonadState の定義は以下の通りです：

class MonadState (σ : outParam (Type u)) (m : Type u → Type v) : Type (max (u+1) v) where
  get : m σ
  set : σ → m PUnit
  modifyGet : (σ → α × σ) → m α

PUnit は Unit 型を宇宙多相にして Type の代わりに Type u にできるようにしたものです。modifyGet には get と set を用いたデフォルト実装を利用することも可能ですが、その場合はそもそも modifyGet を便利にするための最適化が働かないためデフォルト実装は役に立ちません。

Of クラスと The 関数

ここまで見てきた、MonadExcept の例外の型や、MonadState の状態の型のように追加の情報を受け取るモナドの型クラスはすべてこの追加情報の型を出力パラメータとして保持していました。単純なプログラムであれば、StateT ・ReaderT ・ExceptT からどれか1つを組み合わせたモナドは状態の型、環境の型、例外の型のうちどれか1つしか持たないため一般的に利用しやすいです。しかし、モナドが複雑になってくると複数の状態やエラーの型を含むようになります。この場合、出力パラメータを用いると同じ do ブロックで両方の状態をターゲットにすることができなくなります。

このような場合のために、追加の情報を出力パラメータとしない追加の型クラスがあります。これらの型クラスでは名前に Of という単語を使っています。例えば、MonadStateOf は MonadState に似ていますが、outParam 修飾子を持ちません：

同じように、追加情報の型を暗黙の引数ではなく 明示的に 受け取る型クラスのメソッドがあります。MonadStateOf の場合、getThe があり、型は次のようになります：

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

また modifyThe は以下の型になります。

(σ : Type u) → {m : Type u → Type v} → [MonadStateOf σ m] → (σ → σ) → m PUnit

setThe が無いのは、新しい状態の型だけでそれを包む状態のモナド変換として何を使うかを決定できるからです。

Leanの標準ライブラリには Of バージョンのインスタンスで定義された Of なしバージョンのインスタンスが存在します。言い換えると Of バージョンを実装すると、両方の実装が得られます。一般的には、Of バージョンを実装し、それからそのクラスの Of なしバージョンを使ってプログラムをまず書き、出力パラメータが煩わしくなってきたところで Of バージョンに移行すると良いでしょう。

変換子と Id

恒等モナド Id は何の作用も持たないモナドで、何らかの理由でモナドが要求されるものの実際にはモナドとしての性質が不要な場合に用いられます。Id のもう一つの使い方は、モナド変換子のスタックの一番下に置くことです。例えば、StateT σ Id は State σ と同じように動作します。

演習問題

モナドの約定

紙と鉛筆を使って、本節の各モナド変換子についてモナド変換子のルールが満たされていることをチェックしてください。

ロギング変換子

WithLog のモナド変換子を定義してください。また対応する型クラス MonadWithLog を定義し、ロギングと例外を組み合わせたプログラムを書いてください。

ファイル数のカウント

doug のモナドを StateT に変更して、確認したディレクトリとファイルの数をカウントするようにしてください。実行の最後には以下のようなレポートを表示してください：

  Viewed 38 files in 5 directories.