モナド
C#とKotlinでは、?. 演算子でnullの可能性がある値に対してプロパティを検索したりメソッドを呼び出したりすることができます。レシーバが null の場合、式全体がnullになります。それ以外の場合、もとの null でない値が呼び出しを受けます。?. は連鎖して使用することができ、この場合一番初めに現れる null の結果によって一連の処理が終了します。このようにnullチェックの連鎖させ方は、ネストの深い if 文を書いたりメンテしたりするよりもずっと便利です。
同様に、例外はエラーコードを手作業でチェックしたり伝播させたりするよりもはるかに便利です。また、ロギングは各関数がログの結果と戻り値の両方を返すのではなく、専用のロギングフレームワークを持つことで最も簡単に実現できます。連鎖したnullチェックと例外は、通常、言語設計者側にこのユースケースを予測する必要がある一方で、ロギングフレームワークでは通常、ログの蓄積からロギングを行うコードを切り離すために副作用を利用します。
これらの機能やその他はすべて、Monad と呼ばれる共通のAPIのインスタンスとしてライブラリ化することができます。LeanはこのAPIを使うための専用の構文を提供しますが、裏で何が起こっているのかを理解することを阻害してもいます。この章では、手作業によるnullチェックのネストに関する細かい説明から始まり、そこから便利で一般的なAPIへと発展していきます。信じがたい読者におかれましては、ぜひその疑念を抱いたまま読み進めてください。
none チェック：DRY原則
Leanにおいて、nullチェックをパターンマッチで連鎖させることができます。リストの最初の要素の取得は、ただインデックス記法を使うだけで可能です：
def first (xs : List α) : Option α :=
xs[0]?
空のリストは最初の要素を持たないため、この結果は Option 型となります。最初と3番目の要素を取り出すには、それぞれ none ではないことをチェックする必要があります：
def firstThird (xs : List α) : Option (α × α) :=
match xs[0]? with
| none => none
| some first =>
match xs[2]? with
| none => none
| some third =>
some (first, third)
同様に、1番目と3番目、5番目の要素の取得ではさらに none でないことのチェックが増えます：
def firstThirdFifth (xs : List α) : Option (α × α × α) :=
match xs[0]? with
| none => none
| some first =>
match xs[2]? with
| none => none
| some third =>
match xs[4]? with
| none => none
| some fifth =>
some (first, third, fifth)
そしてこの流れで7番目の要素の取得を追加するといよいよ手に負えなくなってきます：
def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) :=
match xs[0]? with
| none => none
| some first =>
match xs[2]? with
| none => none
| some third =>
match xs[4]? with
| none => none
| some fifth =>
match xs[6]? with
| none => none
| some seventh =>
some (first, third, fifth, seventh)
このコードでは、数字の抽出と数字がすべて存在していることのチェックという2つの関心事に対処しようとしています。しかし、2つ目の関心事には none のケースを処理するコードをコピペすることで対処しています。これがこのコードの根本的な問題です。プログラミングにおいて、一般的に繰り返し処理を補助関数として抽出することは良い習慣です：
def andThen (opt : Option α) (next : α → Option β) : Option β :=
match opt with
| none => none
| some x => next x
この補助関数はC#やKotlinの ?. と同じように使用され、none 値の伝播を行います。この関数は2つの引数を取ります：オプション値と、値が none でない場合に適用する関数です。第1引数が none の場合、この補助関数は none を返します。第1引数が none でない場合、第2引数の関数が some コンストラクタの中身に適用されます。
これで、firstThird はパターンマッチの代わりに andThen を使って書き換えることができます：
def firstThird (xs : List α) : Option (α × α) :=
andThen xs[0]? fun first =>
andThen xs[2]? fun third =>
some (first, third)
Leanで関数に引数を渡す際には括弧を付ける必要はありません。以下は括弧と関数の本体にインデントを付けた同等の定義です：
def firstThird (xs : List α) : Option (α × α) :=
andThen xs[0]? (fun first =>
andThen xs[2]? (fun third =>
some (first, third)))
andThen 補助関数は値が流れる「パイプライン」のようなものを提供します。この事実は上記のやや変わったインデントバージョンでよりはっきりします。andThen を記述する構文を改善することで、これらの計算をさらに理解しやすくすることができます。
中置演算子
Leanでは、infix 、infixl 、infixr コマンドを使って、それぞれ非結合、左結合、右結合演算子を宣言することができます。左結合 演算子が連続して複数回使用されると、式の左側に括弧が積みあがっていきます。加算演算子 + は左結合であるため、w + x + y + z は (((w + x) + y) + z) と同等です。指数演算子 ^ は右結合であるため、w ^ x ^ y ^ z は (w ^ (x ^ (y ^ z))) と同等です。< などの比較演算子は非結合演算子であるため、x < y < z は構文エラーであり、手作業で括弧を入れる必要があります。
以下の宣言によって andThen は中置演算子となります：
infixl:55 " ~~> " => andThen
コロンの後ろの数字は新しい中置演算子の 優先順位 を宣言しています。通常の数学表記において + と * はどちらも左結合ですが、x + y * z は x + (y * z) と等価です。Leanでは、+ の優先順位は65で、* の優先順位は70です。優先順位の高い演算子は低い演算子よりも前に適用されます。~~> の宣言から、+ と * はどちらもこの演算子よりも優先順位が高いため、+ と * が先に適用されます。一般的に、演算子の集まりに対して最も便利な優先順位を定義するには、いろんなパターンを何度も試して経験値をためる必要があります。
新しい中置演算子の後ろに続くのは二重矢印 => で、これは中置演算子に使用する名前付き関数を指定します。Leanの標準ライブラリはこの機能を使って + と * をそれぞれ HAdd.hAdd と HMul.hMul を指し示す中置演算子として定義しており、型クラスを使ってこれらの中置演算子をオーバーロードできるようにしています。しかし、ここでは andThen は普通の関数です。
andThen のために中置演算子を定義することで、firstThird は none チェックの「パイプライン」感を前面に押し出した形で書き直すことができます：
def firstThirdInfix (xs : List α) : Option (α × α) :=
xs[0]? ~~> fun first =>
xs[2]? ~~> fun third =>
some (first, third)
このスタイルの方は大きな関数の記述をより簡潔にします：
def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) :=
xs[0]? ~~> fun first =>
xs[2]? ~~> fun third =>
xs[4]? ~~> fun fifth =>
xs[6]? ~~> fun seventh =>
some (first, third, fifth, seventh)
エラーメッセージの伝播
Leanのような純粋関数型言語には、エラー処理のための例外アルゴリズムが組み込まれていません。なぜなら、例外をスローしたりキャッチしたりすることは式のステップバイステップな評価モデルの範囲外であるからです。しかし、関数型プログラムでもエラー処理は必要です。firstThirdFifthSeventh の場合、リストがどれくらいの長さで、どこで検索に失敗したかを知ることはユーザにとって重要でしょう。
この実現方法として、エラーと計算結果のどちらにもなりうるデータ型を定義し、例外を持つ関数をこのデータ型を返す関数に変換することが通例です：
inductive Except (ε : Type) (α : Type) where
| error : ε → Except ε α
| ok : α → Except ε α
deriving BEq, Hashable, Repr
型変数 ε は関数が発生させる可能性のあるエラーの型を表します。呼び出し元はエラーと成功の両方を処理することが期待されているため、型変数 ε はJavaのチェックされた例外のリストのような役割を果たします。
Option と同様に、Except はリスト内のエントリが見つからなかった場合に使用することができます。この場合のエラーの型は String です：
def get (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
範囲内の値の検索は Except.ok を出力します：
def ediblePlants : List String :=
["ramsons", "sea plantain", "sea buckthorn", "garden nasturtium"]
#eval get ediblePlants 2
Except.ok "sea buckthorn"
範囲外の値の検索は Except.error を出力します：
#eval get ediblePlants 4
Except.error "Index 4 not found (maximum is 3)"
1回のリストの検索はこれで結果かエラーの返却を便利にします：
def first (xs : List α) : Except String α :=
get xs 0
しかし、2回の検索となると潜在的なエラーの対応が要求されます：
def firstThird (xs : List α) : Except String (α × α) :=
match get xs 0 with
| Except.error msg => Except.error msg
| Except.ok first =>
match get xs 2 with
| Except.error msg => Except.error msg
| Except.ok third =>
Except.ok (first, third)
リストの検索を追加すると、必要なエラー処理も増えます：
def firstThirdFifth (xs : List α) : Except String (α × α × α) :=
match get xs 0 with
| Except.error msg => Except.error msg
| Except.ok first =>
match get xs 2 with
| Except.error msg => Except.error msg
| Except.ok third =>
match get xs 4 with
| Except.error msg => Except.error msg
| Except.ok fifth =>
Except.ok (first, third, fifth)
ここにまたリスト検索を追加するとかなり手に負えなくなってきます：
def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) :=
match get xs 0 with
| Except.error msg => Except.error msg
| Except.ok first =>
match get xs 2 with
| Except.error msg => Except.error msg
| Except.ok third =>
match get xs 4 with
| Except.error msg => Except.error msg
| Except.ok fifth =>
match get xs 6 with
| Except.error msg => Except.error msg
| Except.ok seventh =>
Except.ok (first, third, fifth, seventh)
繰り返しになりますが、よくあるパターンを補助関数にくくりだすことができます。関数の各ステップでエラーチェックが行われ、成功した場合のみ後続の計算が行われます。Except のために andThen の新しいバージョンを以下のように定義することができます：
def andThen (attempt : Except e α) (next : α → Except e β) : Except e β :=
match attempt with
| Except.error msg => Except.error msg
| Except.ok x => next x
Option とまったく同じように、このバージョンの andThen は firstThird のより簡潔な定義を提供します：
def firstThird' (xs : List α) : Except String (α × α) :=
andThen (get xs 0) fun first =>
andThen (get xs 2) fun third =>
Except.ok (first, third)
Option と Except のどちらの場合も、2つのパターンが繰り返されています：1つは各ステップでの中間結果のチェックで、これは andThen にくくりだされています。もう1つは最終的な成功結果であり、それぞれ some と Except.ok で表されます。便宜上、成功は ok という補助関数にくくりだすことができます：
def ok (x : α) : Except ε α := Except.ok x
同じように、失敗も fail という補助関数にくくりだすことが可能です：
def fail (err : ε) : Except ε α := Except.error err
ok と fail を使うことで、get はもうちょっと読みやすくなります：
def get (xs : List α) (i : Nat) : Except String α :=
match xs[i]? with
| none => fail s!"Index {i} not found (maximum is {xs.length - 1})"
| some x => ok x
andThen のための中置演算子を追加することで、firstThird は Option を返すバージョンと同じくらい簡潔になります：
infixl:55 " ~~> " => andThen
def firstThird (xs : List α) : Except String (α × α) :=
get xs 0 ~~> fun first =>
get xs 2 ~~> fun third =>
ok (first, third)
このテクニックはより大きい関数に対しても同様にスケールアップします：
def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) :=
get xs 0 ~~> fun first =>
get xs 2 ~~> fun third =>
get xs 4 ~~> fun fifth =>
get xs 6 ~~> fun seventh =>
ok (first, third, fifth, seventh)
ロギング
ある数値が偶であるとは、2で割った時に余りがないことです：
def isEven (i : Int) : Bool :=
i % 2 == 0
関数 sumAndFindEvens は総和を計算しつつ、リストを進みながら偶数のみを記憶します：
def sumAndFindEvens : List Int → List Int × Int
| [] => ([], 0)
| i :: is =>
let (moreEven, sum) := sumAndFindEvens is
(if isEven i then i :: moreEven else moreEven, sum + i)
この関数はプログラミングにおけるよくあるパターンのシンプルな例です。多くのプログラムはデータ構造を一度走査し、メインの結果を計算しながら脇役的な結果を蓄積する必要があります。この例の1つがロギングです：IO アクションであるプログラムは常にログをディスク上のファイルに記録することができますが、ディスクはLeanの関数の数学的世界の外側にあるため、IO に基づくログについて証明することは非常に難しくなります。別の例として、木に含まれるすべてのノードの総和を通りがけ順で計算しながら、同時に通過した各ノードを記録するような関数があります：
def inorderSum : BinTree Int → List Int × Int
| BinTree.leaf => ([], 0)
| BinTree.branch l x r =>
let (leftVisited, leftSum) := inorderSum l
let (hereVisited, hereSum) := ([x], x)
let (rightVisited, rightSum) := inorderSum r
(leftVisited ++ hereVisited ++ rightVisited, leftSum + hereSum + rightSum)
sumAndFindEvens と inorderSum のどちらも共通の繰り返し構造を持ちます。計算の各ステップはメインの結果とそれに沿って貯めたデータのリストからなるペアを返却します。その後これらのリストは結合され、計算されたメインの結果とペアにされます。sumAndFindEvens を少し書き換えるだけで偶数の保存と合計の計算をよりきれいに分けた共通の構造がよりはっきりします：
def sumAndFindEvens : List Int → List Int × Int
| [] => ([], 0)
| i :: is =>
let (moreEven, sum) := sumAndFindEvens is
let (evenHere, ()) := (if isEven i then [i] else [], ())
(evenHere ++ moreEven, sum + i)
この明確さのおかげで、値と蓄積された結果からなるペアには固有の名前を与えることできます：
structure WithLog (logged : Type) (α : Type) where
log : List logged
val : α
同様に、計算の次のステップへ値を渡す際に蓄積された結果のリストを保存するプロセスは、再び andThen という名前の補助関数にくくりだすことができます：
def andThen (result : WithLog α β) (next : β → WithLog α γ) : WithLog α γ :=
let {log := thisOut, val := thisRes} := result
let {log := nextOut, val := nextRes} := next thisRes
{log := thisOut ++ nextOut, val := nextRes}
結果がエラーである場合、ok は常に成功する操作を表します。しかし、ここではログに何も記録せずにそのまま値を返す操作です：
def ok (x : β) : WithLog α β := {log := [], val := x}
Except が処理の不確実さとして fail を提供するように、WithLog はアイテムをログに追加できるようにします。この操作には特に意味のある戻り値がないため、Unit を返却します：
def save (data : α) : WithLog α Unit :=
{log := [data], val := ()}
WithLog と andThen 、ok 、save によってロギングという関心事から総和の関心事の分離を以下のプログラムによって実現できます：
def sumAndFindEvens : List Int → WithLog Int Int
| [] => ok 0
| i :: is =>
andThen (if isEven i then save i else ok ()) fun () =>
andThen (sumAndFindEvens is) fun sum =>
ok (i + sum)
def inorderSum : BinTree Int → WithLog Int Int
| BinTree.leaf => ok 0
| BinTree.branch l x r =>
andThen (inorderSum l) fun leftSum =>
andThen (save x) fun () =>
andThen (inorderSum r) fun rightSum =>
ok (leftSum + x + rightSum)
ここでもまた、中置演算子が正しいステップに焦点を合わせるのに役立ちます：
infixl:55 " ~~> " => andThen
def sumAndFindEvens : List Int → WithLog Int Int
| [] => ok 0
| i :: is =>
(if isEven i then save i else ok ()) ~~> fun () =>
sumAndFindEvens is ~~> fun sum =>
ok (i + sum)
def inorderSum : BinTree Int → WithLog Int Int
| BinTree.leaf => ok 0
| BinTree.branch l x r =>
inorderSum l ~~> fun leftSum =>
save x ~~> fun () =>
inorderSum r ~~> fun rightSum =>
ok (leftSum + x + rightSum)
木構造のノードへの採番
木の 通り順 （inorder numbering）は木の中の各データポイントに、その木を通り順に訪れた際の各ステップを割り当てます。例として以下の木 aTree を考えてみましょう：
open BinTree in
def aTree :=
branch
(branch
(branch leaf "a" (branch leaf "b" leaf))
"c"
leaf)
"d"
(branch leaf "e" leaf)
これの通り順は以下のようになります：
BinTree.branch
(BinTree.branch
(BinTree.branch (BinTree.leaf) (0, "a") (BinTree.branch (BinTree.leaf) (1, "b") (BinTree.leaf)))
(2, "c")
(BinTree.leaf))
(3, "d")
(BinTree.branch (BinTree.leaf) (4, "e") (BinTree.leaf))
木は再帰関数で処理することが最も自然ですが、木における通常の再帰パターンでは通り順の採番を計算することは難しいです。これは、木の左側の部分木のどこかに割り当てられる最大の番号がノードのデータ値の採番を決定することに使われ、さらに右の部分木の採番の開始位置を決定することに使われるからです。命令型言語では、この問題は次に割り当てる番号を格納する可変変数を使用することで回避できます。次のPythonプログラムでは、可変変数を使って通り順の採番を計算します：
class Branch:
def __init__(self, value, left=None, right=None):
self.left = left
self.value = value
self.right = right
def __repr__(self):
return f'Branch({self.value!r}, left={self.left!r}, right={self.right!r})'
def number(tree):
num = 0
def helper(t):
nonlocal num
if t is None:
return None
else:
new_left = helper(t.left)
new_value = (num, t.value)
num += 1
new_right = helper(t.right)
return Branch(left=new_left, value=new_value, right=new_right)
return helper(tree)
aTree に相当するPythonの採番対象は以下のようになり：
a_tree = Branch("d",
left=Branch("c",
left=Branch("a", left=None, right=Branch("b")),
right=None),
right=Branch("e"))
これの採番結果は以下になります：
>>> number(a_tree)
Branch((3, 'd'), left=Branch((2, 'c'), left=Branch((0, 'a'), left=None, right=Branch((1, 'b'), left=None, right=None)), right=None), right=Branch((4, 'e'), left=None, right=None))
Leanには可変変数が無いにもかかわらず、回避策が存在します。違う視点から見てみると、可変変数は2つの関連した側面を持っていると考えることができます：すなわち、関数が呼び出された時の値とその関数が終了した時点での値です。言い換えれば、可変変数を使う関数は、可変変数の初期値を引数として取り、その変数の最終結果と関数の結果のペアを返す関数とみなすことができます。この最終値は次のステップの引数として渡すことができます。
Pythonの例で可変変数を宣言している外部関数と、その変数を更新する内部の補助関数が使われているように、この関数は、変数の初期値を提供し、採番された木の計算中に変数の値をスレッドする内部の補助関数の結果を明示的に返す外部関数としてLean上で実装できます：
def number (t : BinTree α) : BinTree (Nat × α) :=
let rec helper (n : Nat) : BinTree α → (Nat × BinTree (Nat × α))
| BinTree.leaf => (n, BinTree.leaf)
| BinTree.branch left x right =>
let (k, numberedLeft) := helper n left
let (i, numberedRight) := helper (k + 1) right
(i, BinTree.branch numberedLeft (k, x) numberedRight)
(helper 0 t).snd
このコードは none を伝播する Option コードと error を伝播する Except コード、ログを蓄積する WithLog コードと同じように2つの関心事が混在しています：カウンタの値の伝播と、実際に木を走査して結果を見つけることです。これらの場合と同じように、andThen 補助関数を定義することで、計算のあるステップから別のステップに状態を伝播させることができます。このためにまず初めに行うことは、引数として入力状態を受け取り、値と一緒に出力状態を返すパターンに名前を付けることです：
def State (σ : Type) (α : Type) : Type :=
σ → (σ × α)
State の場合、ok は入力状態を変更せずに、与えられた値と一緒に返却する関数です：
def ok (x : α) : State σ α :=
fun s => (s, x)
可変変数を扱う場合、値の読み取りと新しい値での更新との2つの基本的な演算があります。現在の値の読み取りは、入力状態を変更せずに出力状態に置き、さらにその値を値フィールドに置く関数として実装できます：
def get : State σ σ :=
fun s => (s, s)
新しい値の書き込みは、入力状態を無視し、与えられた値を出力状態に設定することで構成されます：
def set (s : σ) : State σ Unit :=
fun _ => (s, ())
最終的に、状態を使用する2つの計算は、まず最初の関数の出力状態と戻り値を取得し、それらを次の関数に渡すことでつなげることができます：
def andThen (first : State σ α) (next : α → State σ β) : State σ β :=
fun s =>
let (s', x) := first s
next x s'
infixl:55 " ~~> " => andThen
State とその補助関数を使うことで、局所的な可変変数をシミュレートすることができます：
def number (t : BinTree α) : BinTree (Nat × α) :=
let rec helper : BinTree α → State Nat (BinTree (Nat × α))
| BinTree.leaf => ok BinTree.leaf
| BinTree.branch left x right =>
helper left ~~> fun numberedLeft =>
get ~~> fun n =>
set (n + 1) ~~> fun () =>
helper right ~~> fun numberedRight =>
ok (BinTree.branch numberedLeft (n, x) numberedRight)
(helper t 0).snd
State は1つの可変変数のみをシミュレートするため、get と set の呼び出しで特定の変数名を指定する必要がありません。
モナド：関数的デザインパターン
これらの例は以下のようにまとめられます：
OptionやExcept ε、WithLog logged、State σなどの多相型- この型を持つプログラム列における繰り返される側面のケアを行う
andThen演算 - この型を扱う中で（ある意味で）もっとも退屈な方法である
ok演算 - その他、この型を用いる
noneやfail、save、getなどの演算のあつまり
このAPIのスタイルは モナド （monad）と呼ばれます。モナドの考え方は圏論と呼ばれる数学の1分野から派生したものですが、プログラミングで用いるにあたって圏論の理解は必要ありません。モナドの重要な考え方は、純粋関数型言語であるLeanが提供するツールを用いることで、それぞれのモナドが特定の種類の副作用をエンコードするということです。例えば、Option は none を返して失敗するプログラムを表し、Except は例外を投げるプログラムを、WithLog は実行中にログを蓄積するプログラムを、State は単一の可変変数を持つプログラムをそれぞれ表します。