モナド組み立てキット
ReaderT
だけが便利なモナド変換子ではありません。本節では、さらに多くの変換子について説明します。各モナド変換子は以下のように構成されています:
- モナドを引数に取る定義もしくはデータ型
T
。これは(Type u → Type v) → Type u → Type v
のような型を持ちますが、モナドの前に別で引数を受け取ることもできます。 Monad m
のインスタンスに依存したT m
のMonad
インスタンス。これにより変換されたモナドをモナドとして使うことができます。- 任意のモナド
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
bind
and pure
}=
OptionT.mk do
match ← pure (some v) with
| none => pure none
| some x => f x
OptionT.mk do
let y ← pure (some v)
match y with
| none => pure none
| some x => f x
do
-notation }=
OptionT.mk
(pure (some v) >>= fun y =>
match y with
| none => pure none
| some x => f x)
m
}=
OptionT.mk
(match some v with
| none => pure none
| some x => f x)
match
}=
OptionT.mk (f v)
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.