モナド型クラス
モナドの型ごとに 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
どちらのメソッドも正しい型です。ではなぜこのインスタンスはモナドの約定を破っているのでしょうか?