モナド変換子の順序

モナド変換子のスタックからモナドを構成する場合、モナド変換子を重ねる順番に注意が必要です。同じ変換子のあつまりでも異なる順番で並べると異なるモナドになります。

以下の countLetters は前節のものとほぼ同じですが、具体的なモナドを提示する代わりに利用可能な作用の組を記述するために型クラスを使用する点が異なります：

def countLetters [Monad m] [MonadState LetterCounts m] [MonadExcept Err m] (str : String) : m 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

状態と例外についてのモナド変換子の組み合わせ方には2通りあり、それぞれ両方の型クラスのインスタンスを持つモナドになります：

abbrev M1 := StateT LetterCounts (ExceptT Err Id)
abbrev M2 := ExceptT Err (StateT LetterCounts Id)

例外が発生しない入力に対してプログラムを実行した場合、どちらのモナドも似たような結果を出力します：

#eval countLetters (m := M1) "hello" ⟨0, 0⟩

Except.ok ((), { vowels := 2, consonants := 3 })

#eval countLetters (m := M2) "hello" ⟨0, 0⟩

(Except.ok (), { vowels := 2, consonants := 3 })

しかし、これらの戻り値には微妙な違いがあります。M1 の場合、外側のコンストラクタは Except.ok で、ユニットのコンストラクタと最終状態のペアを含んでいます。M2 の場合、外側のコンストラクタはペアで、その中にはユニットのコンストラクタを適用した Except.ok が含まれています。最終状態は Except.ok の外側になっています。どちらの場合もプログラムは母音と子音の数を返します。

一方、例外が出る文字列を入力にした場合、母音と子音のカウントを返すモナドは1つだけです。M1 を使うと例外の値だけが返されます：

#eval countLetters (m := M1) "hello!" ⟨0, 0⟩

Except.error (StEx.Err.notALetter '!')

M2 を使うと、例外の値は例外が投げられた時の状態とのペアからなります：

#eval countLetters (m := M2) "hello!" ⟨0, 0⟩

(Except.error (StEx.Err.notALetter '!'), { vowels := 2, consonants := 3 })

M2 ではデバッグ時に役立つ情報が多く得られるため、M2 の方が M1 より優れていると考えたくなるかもしれません。しかし、同じプログラムでも M1 と M2 で 異なる 計算結果を返すかもしれず、これらの答えのうちどちらか一方が他方より必ずしも優れているという原理的な理由はありません。これは上記のプログラムに例外を処理するステップを追加するとよくわかります：

def countWithFallback
    [Monad m] [MonadState LetterCounts m] [MonadExcept Err m]
    (str : String) : m Unit :=
  try
    countLetters str
  catch _ =>
    countLetters "Fallback"

このプログラムは常に成功しますが、実際の入力に対して異なる結果で成功することもあります。例外が投げられなければ出力は countLetters と同じです：

#eval countWithFallback (m := M1) "hello" ⟨0, 0⟩

Except.ok ((), { vowels := 2, consonants := 3 })

#eval countWithFallback (m := M2) "hello" ⟨0, 0⟩

(Except.ok (), { vowels := 2, consonants := 3 })

しかし、例外が投げられキャッチされた場合、最終結果は大きく異なります。M1 の場合、最終状態には "Fallback" の文字数だけが含まれます：

#eval countWithFallback (m := M1) "hello!" ⟨0, 0⟩

Except.ok ((), { vowels := 2, consonants := 6 })

M2 での最終状態には "hello" と "Fallback" の両方の文字数が含まれます。これは命令型言語で見られるような挙動です：

#eval countWithFallback (m := M2) "hello!" ⟨0, 0⟩

(Except.ok (), { vowels := 4, consonants := 9 })

M1 では、例外を投げると例外がキャッチされた時点まで状態を「ロールバック」します。M2 では、例外のスローとキャッチにまたがって状態の変更が持続します。この違いは M1 と M2 の定義を展開することでわかります。M1 α は展開すると LetterCounts → Except Err (α × LetterCounts) となり、M2 α は展開すると LetterCounts → Except Err α × LetterCounts となります。これはつまり、M1 α は文字数の初期値を受け取り、エラーか「 α と更新された文字数」のペアを返す関数を記述しています。M1 で例外が投げられると、最終的な状態は無くなります。M2 α は文字数の初期値を受け取り、更新された文字数とエラーか α のペアを返す関数を記述しています。M2 での例外送出には状態が伴います。

可換なモナド

関数型プログラミングの専門用語では、2つのモナド変換子がプログラムの意味を変えることなく並べ替えられる場合可換（commute）と呼ばれます。StateT と ExceptT を並べ替えたときにプログラムの結果が異なる可能性があるということは、状態と例外が可換ではないということを意味します。一般的に、モナド変換子が可換であることを期待するべきではありません。

全てのモナド変換子が可換ではありませんが、可換であるものもあります。例えば、StateT を2つ使用した場合、これは並べ替えることができます。StateT σ (StateT σ' Id) α の定義を展開すると σ → σ' → ((α × σ) × σ') 型が得られ、StateT σ' (StateT σ Id) α からは σ' → σ → ((α × σ') × σ) が得られます。言い換えると、両者の違いは σ 型と σ' 型を戻り値内の異なる場所にてネストし、異なる順序で引数を受け取るということです。クライアントコードは同じ入力を提供する必要があり、同じ出力を受け取ることができます。

可変状態と例外を持つプログラミング言語のうちほとんどは M2 のように動作します。そのような言語では例外が投げられたときに状態をロールバック しなければならない ように記述するのは難しく、通常は M1 の明示的な状態値の受け渡しによく似た方法でシミュレーションする必要があります。モナド変換子は手元の問題に対して作用の順序の解釈を選択する自由を与え、そして両者の選択は同じくらい容易にプログラム可能です。しかし、変換子の順序の選択には注意が必要です。この素晴らしい表現力を使うには表現されているものが意図通りかをチェックする責任が伴い、countWithFallback の型シグネチャはおそらく必要以上に多相的になります。

演習問題

ReaderT と StateT の定義を展開し、その結果の型を推論して ReaderT と StateT が可換であることを確認してください。
ReaderT と ExceptT は可換になるでしょうか？定義を展開し、結果の型を推論して答えを確認してください。
モナド変換子 ManyT をMany の定義と適切な Alternative インスタンスに基づいて構築してください。そしてそれが Monad の約定を満たすことを確認してください。
ManyT は　StateT と可換になるでしょうか？もしそうなら、定義を展開し、結果の型を推論して答えを確認してください。もしそうでないなら、ManyT (StateT σ Id) と StateT σ (ManyT Id) のプログラムを書いてください。それぞれのプログラムはモナド変換子の順序に対してより理にかなったものにしてください。

Functional Programming in Lean 日本語訳

モナド変換子の順序

可換なモナド

演習問題