「andThen」からモナドを理解する：高度な抽象化の第一歩

はじめに

関数型プログラミングには、「モナド（monad）」という強力な抽象化ツールが存在します。 しかし、それはしばしば初心者にとって難解なものとされます。 モナドが提供する抽象化の対象は、我々が日常的に利用するデータ構造や操作の中に実は数多く存在しているのです。 その共通性に着目することで、モナドはそれほど遠い存在ではなく、むしろ身近なものであることが分かります。

ある種のデータ構造には、その構造を持つ値から始めて関数を次々と適用していくandThen関数が考えられます。 この記事でandThen関数を出発点として、モナドの理解への第一歩を踏み出しましょう。

OptionやMaybeにおけるandThen

Option（あるいはMaybe）は、値が存在しない状況を表現するデータ型です。 何らかの値xが存在する場合（some x）にはOptionの値を返す関数fを適用し、存在しない場合（none）はそのまま存在しないとするandThen関数を考えましょう。 Lean 4でコード例を示す ⧉と以下のようになります。

def andThen (v : Option α) (f : α → Option β) : Option β :=
  match v with
  | none   => none
  | some x => f x

この関数の使用例として、正の自然数に対してだけその数を2倍した値を返し、0に対しては値を返さない（言い換えるとnoneを返す）mayDouble関数を適用するコードを示します。

def mayDouble : Nat → Option Nat :=
  fun (x : Nat) =>
    match x with
    | 0 => none
    | n => some (2 * n)

#eval andThen (some 5) mayDouble -- some 10 （正なので倍にされた）
#eval andThen (some 0) mayDouble -- none （0なので値を返さなかった）
#eval andThen  none    mayDouble -- none （値がないのでそのまま）

例外処理におけるandThen

EitherやExceptのような構造は、成功か失敗かの結果を表現します。 このデータ型に対しては、前の処理が成功して値xを持つ場合（ok x）にのみ次の関数fを適用し、失敗してエラーeである場合（error e）はそのままエラーを受け流すようなandThen関数を考えられます。 Lean 4でコード例を示します。 ⧉ 前節で示したOptionのandThenと見た目が似ていますね。

def andThen (v : Except ε α) (f : α → Except ε β) : Except ε β :=
  match v with
  | .error e => Except.error e
  | .ok x    => f x

この関数の使用例として、自然数を返す処理が成功した場合に、その結果が正の自然数だった場合にはそれを2倍した値で成功とし、そうでない（すなわち0だった）場合にはエラーを返すdoubleIfPos関数を適用するコードを示します。

def doubleIfPos : Nat → Except String Nat :=
  fun (x : Nat) =>
    match x with
    | 0 => .error "It is 0."
    | n => .ok (2 * n)

#eval andThen (.ok 5) doubleIfPos
-- Except.ok 10 （正の値で成功なので倍）
#eval andThen (.ok 0) doubleIfPos
-- Except.error "It is 0." （成功だが0だったのでエラー）
#eval andThen (.error "Error!") doubleIfPos
-- Except.error "Error!" （前の処理が失敗なのでそのまま）

状態遷移におけるandThen

状態を保持しながら計算するための構造は、与えられた状態に対して計算結果とともに次の状態を返すような関数の型Stateと考えることができます。

def State (σ : Type) (α : Type) := σ → (σ × α)
-- σが状態を区別するための値の型で、αが計算結果の型です。

少し分かりにくい構造ですが、簡単な例を通して説明していきます。 ある自然数から0まで1ずつカウントダウンしていくことを考えましょう。 状態の種類としては、初期状態Init、カウントダウン中のProgress、停止状態Stopを考えましょう。

（任意の状態における）自然数からカウントダウンを1回行う関数stepを考えます。 既に0だったら停止状態にしておけば良いですね。停止状態のようなそれ以降遷移しない一定の状態は、前の状態（引数）によらず常に一定の値を返す関数として表現できます。今の例では(Stop, 0)を返す関数で表現できます（finishedと名付けます）。 また、1のときも停止状態に遷移させます。 2以上のときは1減らしてカウントダウン中とするわけですが、もし停止状態だったら減らさないでおきたいですね。初期状態かカウントダウン中だったら減らすことにしましょう。 Lean 4のコードで示す ⧉と以下のようになります。

def finished : State MyStates Nat := fun _ => (Stop, 0)

def step : Nat → State MyStates Nat :=
  fun (n : Nat) =>
    match n with
    | 0   => finished
    | 1   => finished
    | _+2 => -- 2以上
        fun s =>
          match s with
          | Stop          => (Stop, n)
          | Init|Progress => (Progress, n-1)

このようなStateの構造に対して、現在の状態vと次の状態へと移行する計算fをつなぐようなandThen関数が考えられます。

def andThen (v : State σ α) (f : α → State σ β) : State σ β :=
  fun (s : σ) =>
    let ((s' : σ), (x : α)) := v s
    f x s'

具体例でこの関数がandThenと呼べるものになっていることを確認しましょう。 少し難しいのでひとまずそうなっていることを認めていただいて次の節まで読み飛ばしていただいても構いません。

初期状態として3（＝(Init, 3)）から始めて、1回カウントダウン（step関数を適用）すればカウントダウン中の2（＝(Progress, 2)）になり、さらに1回カウントダウンするとカウントダウン中の1（＝(Progress, 1)）、更にカウントダウンすると停止状態（＝finished = (Stop, 0)）になることを、andThen関数を使って確かめます。

-- 初期状態
def i3 : State MyStates Nat := fun _ => (Init, 3)

-- 初期状態の確認
#reduce i3
-- fun s => (Init, 3)

-- 1回カウントダウン
#reduce andThen i3 step
-- fun s => (Progress, 2)

-- 2回カウントダウン
#reduce andThen (andThen i3 step) step
-- fun s => (Progress, 1)

-- 3回カウントダウン
#reduce andThen (andThen (andThen i3 step) step) step
-- fun s => (Stop, 0)

-- これは`finished`の“定数”と同じ
#reduce andThen finished step
-- fun s => (Stop, 0)

さて、Stateに対するandThen関数はOptionやExceptのandThenとは全く異なるように見えるでしょう。 しかし、実はこれにも共通しているところがあり、その共通点こそが「モナド」なのです。

andThen関数とモナドのbind関数

Option、Except、Stateの3つの構造に対してandThen関数を見てきましたが、その共通点は一体どこにあるのでしょうか。 前節で見たように処理の中身は違うことがあるようなので、それぞれの1️行目に秘密がありそうです。

def andThen (v : Option   α) (f : α → Option   β) : Option   β :=

def andThen (v : Except ε α) (f : α → Except ε β) : Except ε β :=

def andThen (v : State σ  α) (f : α → State σ  β) : State σ  β :=

お分かりいただけますでしょうか。 andThen関数はそのシグネチャがOption, Except ε, State σで共通しているのです。 「このようなシグネチャのandThen関数を定義できる型」を総称する気持ちでmと名付けて置き換えてみましょう。

def andThen (v : m α) (f : α → m β) : m β :=

モナドの定義に触れたことがある方にはどこか見覚えのあるのではないでしょうか。 これがまさしく、モナドのbind操作のシグネチャと一致するのです。

実際、Lean 4ではMonadにはこれと同じシグネチャの関数bindを定義することが（型クラスBindを通して）要請されます。

  bind : {α β : Type u} → m α → (α → m β) → m β

（Lean 4のGitHubリポジトリより引用 ⧉）

おわりに

本記事では、Option, Except, Stateの3つの構造に対するandThen関数を通じて、それらのシグネチャがMonadのbind関数のシグネチャへと一般化できることを見ました。 モナドという抽象化ツールは難解に見えますが、よく使われるデータ構造や操作からその共通点を見つけることで、ほんの少しでも理解へ近づける手助けになれましたら幸いです。

参考文献

  1. はじめに
  2. OptionやMaybeにおけるandThen
  3. 例外処理におけるandThen
  4. 状態遷移におけるandThen
  5. andThen関数とモナドのbind関数
  6. おわりに
  7. 参考文献