モナド型クラス

モナドの型ごとに ok や andThen のような演算子を導入する代わりに、Lean標準ライブラリにはそれらをオーバーロードできる型クラスがあるため、同じ演算子を 任意の モナドに使うことができます。モナドには ok と andThen に相当する2つの演算があります：

class Monad (m : Type → Type) where
  pure : α → m α
  bind : m α → (α → m β) → m β

この定義は実態より若干簡略化されています。Leanのライブラリにおける実際の定義はもう少し複雑ですが、それは後程紹介しましょう。

Option と Except の Monad インスタンスは、それぞれの andThen 演算を適合させることで作成できます：

instance : Monad Option where
  pure x := some x
  bind opt next :=
    match opt with
    | none => none
    | some x => next x

instance : Monad (Except ε) where
  pure x := Except.ok x
  bind attempt next :=
    match attempt with
    | Except.error e => Except.error e
    | Except.ok x => next x

例として出した firstThirdFifthSeventh は Option α と Except String α の戻り値型に対して個別に定義されていました。しかし今やこの関数を 任意の モナドに多相的に定義することができます。ただし、別のモナドによる異なる実装では結果を見つけることができないかもしれないため、引数としてルックアップ関数が必要です。例で出した ~~> と同じ役割を果たしていた bind の中置バージョンは >>= です。

def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α) :=
  lookup xs 0 >>= fun first =>
  lookup xs 2 >>= fun third =>
  lookup xs 4 >>= fun fifth =>
  lookup xs 6 >>= fun seventh =>
  pure (first, third, fifth, seventh)

この firstThirdFifthSeventh の実装は、のろい哺乳類と速い鳥の名前のリストを例として Option について利用することが可能です：

def slowMammals : List String :=
  ["Three-toed sloth", "Slow loris"]

def fastBirds : List String := [
  "Peregrine falcon",
  "Saker falcon",
  "Golden eagle",
  "Gray-headed albatross",
  "Spur-winged goose",
  "Swift",
  "Anna's hummingbird"
]

#eval firstThirdFifthSeventh (fun xs i => xs[i]?) slowMammals

none

#eval firstThirdFifthSeventh (fun xs i => xs[i]?) fastBirds

some ("Peregrine falcon", "Golden eagle", "Spur-winged goose", "Anna's hummingbird")

Except のルックアップ関数 get をもう少し実態に即したものに名称変更することで、先ほどと全く同じ firstThirdFifthSeventh の実装を Except についても使うことができます：

def getOrExcept (xs : List α) (i : Nat) : Except String α :=
  match xs[i]? with
  | none => Except.error s!"Index {i} not found (maximum is {xs.length - 1})"
  | some x => Except.ok x

#eval firstThirdFifthSeventh getOrExcept slowMammals

Except.error "Index 2 not found (maximum is 1)"

#eval firstThirdFifthSeventh getOrExcept fastBirds

Except.ok ("Peregrine falcon", "Golden eagle", "Spur-winged goose", "Anna's hummingbird")

m が Monad インスタンスを持っていなければならないということは、>>= と pure 演算が利用できるということを意味します。

良く使われるモナドの演算

実に多くの型がモナドであるため、任意の モナドに対して多相性を持つ関数は非常に強力です。例えば、関数 mapM はモナド用の map で、Monad を使って関数を適用した結果を順番に並べたり組み合わせたりします：

def mapM [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs =>
    f x >>= fun hd =>
    mapM f xs >>= fun tl =>
    pure (hd :: tl)

関数 f の戻り値の型によって、どの Monad インスタンスを使うかが決まります。つまり、mapM はログを生成する関数や失敗する可能性のある関数、可変状態を使用する関数などのどれにでも使用することができるのです。f の型が利用可能な作用を決定するため、API設計者はその作用を厳密に制御することができます。

本章の導入 で説明したように、State σ α という型は σ 型の可変変数を使用し、α 型の値を返すプログラムを表します。これらのプログラムは、実際には初期状態から値と最終状態のペアへの関数です。Monad クラスは引数がただの型であることを求めます。つまり、Monad となる型は Type → Type であることを要求されます。したがって State のインスタンスは状態の型 σ を指定しておく必要があり、これがインスタンスのパラメータになることを意味します：

instance : Monad (State σ) where
  pure x := fun s => (s, x)
  bind first next :=
    fun s =>
      let (s', x) := first s
      next x s'

これは bind を使って get と set を連続して呼び出している間において状態の型を変更できないことを意味し、ステートフルな計算の規則として理にかなっています。increment 演算子は保存された状態を指定された量だけ増価させ、古い値を返します：

def increment (howMuch : Int) : State Int Int :=
  get >>= fun i =>
  set (i + howMuch) >>= fun () =>
  pure i

mapM を increment と一緒に使うと、リスト内の要素の合計を計算するプログラムになります。より具体的には、可変変数には最終的な合計が格納され、戻り値のリストには実行中の各合計が格納されます。言い換えると、mapM increment は List Int → State Int (List Int) 型を持ち、State の定義を展開すると List Int → Int → (Int × List Int) が得られます。これらは引数として合計の初期値を引数に取り、これは 0 でなければなりません：

#eval mapM increment [1, 2, 3, 4, 5] 0

(15, [0, 1, 3, 6, 10])

ロギングの作用 はWithLog を使って表現することができました。State と同様に、その Monad インスタンスはログに記録されているデータの型に対して多相的です：

instance : Monad (WithLog logged) where
  pure x := {log := [], val := x}
  bind result next :=
    let {log := thisOut, val := thisRes} := result
    let {log := nextOut, val := nextRes} := next thisRes
    {log := thisOut ++ nextOut, val := nextRes}

saveIfEven は偶数についてログを出力して、引数について何もせずに返却する関数です：

def saveIfEven (i : Int) : WithLog Int Int :=
  (if isEven i then
    save i
   else pure ()) >>= fun () =>
  pure i

この関数を mapM と一緒に使うと、偶数についてのログと変更されていないリストがペアになった結果が得られます：

#eval mapM saveIfEven [1, 2, 3, 4, 5]

{ log := [2, 4], val := [1, 2, 3, 4, 5] }

恒等モナド

モナドは失敗、例外、ロギングなどの作用を持つプログラムをデータや関数として明示的に表現します。しかし、柔軟性のためにモナドを使用するように設計されたAPIに対して、時にはエンコードされた作用を必要としない利用者もいます。恒等モナド （identity monad）は作用を持たないモナドであり、純粋なコードをモナドAPIで使用することを可能にします：

def Id (t : Type) : Type := t

instance : Monad Id where
  pure x := x
  bind x f := f x

pure の型は α → Id α であるべきですが、Id α はただの α に簡約されます。同様に、bind の型は α → (α → Id β) → Id β であるべきです。これは α → (α → β) → β に簡約されるため、2番目の引数を1番目の引数に適用して結果を求めることができます。

恒等関手を使うことで、mapM は map と同じものになります。ただし、このように呼ぶにあたって、Leanは意図したモナドが Id であることのヒントを要求します：

#eval mapM (m := Id) (· + 1) [1, 2, 3, 4, 5]

[2, 3, 4, 5, 6]

ヒントを無くすとエラーになります：

#eval mapM (· + 1) [1, 2, 3, 4, 5]

failed to synthesize instance
  HAdd Nat Nat (?m.9063 ?m.9065)

このエラーでは、あるメタ変数を別の変数に適用することで、Leanが型レベルの計算を逆方向に実行していないことを示しています。この関数の戻り値の型は、ほかの型に適用されたモナドであることが期待されます。同様に、型がどのモナドを使用するかについての具体的なヒントを提供しない関数で mapM を使用すると、「インスタンス問題のスタック」というメッセージが表示されます：

#eval mapM (fun x => x) [1, 2, 3, 4, 5]

typeclass instance problem is stuck, it is often due to metavariables
  Monad ?m.9063

モナドの約定

Beq と Hashable のインスタンスのすべてのペアが等しい2つの値が同じハッシュ値を持つことを保証しなければならないように、Monad のインスタンスにも従うべき約定が存在します。まず、pure は bind の左単位でなければなりません。つまり、bind (pure v) f は f v と同じでなければなりません。次に、pure は bind の右単位でもあるべきで、bind v pure は v と同じとなります。最後に、bind は結合的であるべきで、bind (bind v f) g は bind v (fun x => bind (f x) g) と同じです。

この約定はより一般的に作用を持つプログラムに期待される特性を規定しています。pure は作用を持たないため、bind で作用を続けても結果は変わらないはずです。bind の結合性は、基本的に物事が起こっている順序が保たれていれば、処理の実行順番自体はどう行っても問題ないことを言っています。

演習問題

木へのマッピング

関数 BinTree.mapM を定義してください。リストの mapM と同様に、この関数は木の各データ要素に行きがけ順でモナド関数を適用する必要があります。型シグネチャは以下のようになります：

def BinTree.mapM [Monad m] (f : α → m β) : BinTree α → m (BinTree β)

Optionモナドの約定

まず Option の Monad インスタンスがモナドの約定を満たすことへの根拠を書き出してください。次に、以下のインスタンスを考えてみましょう：

instance : Monad Option where
  pure x := some x
  bind opt next := none

どちらのメソッドも正しい型です。ではなぜこのインスタンスはモナドの約定を破っているのでしょうか？