モナドのための do
記法
モナドに基づくAPIは非常に強力ですが、匿名関数を伴った >>=
の明示的な使用は多少煩雑さがあります。HAdd.hAdd
を呼び出す代わりに中置演算子を使うように、Leanはモナドを使うプログラムの読み書きを簡単にすることができる do
記法 と呼ばれる構文を提供しています。これは IO
でプログラムを書くときに使われる do
記法とまったく同じもので、実際 IO
もモナドです。
ハローワールド! では、do
記法は IO
アクションの組み合わせのために用いられていましたが、これらのプログラムの意味は IO
に基づいて直接説明されていました。モナドを使ったプログラミングを理解することは、do
がどのようなモナド演算子の使い方に変換されるかという観点から説明できるようになることを意味します。
do
の翻訳規則の1つ目は、do
の中の文がただ1つの式 E
である場合です。この場合、do
は削除されます。
do E
上記は以下のように訳されます。
E
2つ目の翻訳規則は、do
の最初の文がローカル変数を束縛する矢印付きの let
である場合に使用されます。これは、その変数名を束縛する関数と一緒に >>=
を使うように訳されます。したがって、
do let x ← E1
Stmt
...
En
は以下のように訳されます。
E1 >>= fun x =>
do Stmt
...
En
do
ブロックの最初の文が式の場合、その式は Unit
を返すモナドのアクションであるとみなされ、脱糖後の後続関数は Unit
コンストラクタにパターンマッチするものとなるため、
do E1
Stmt
...
En
は以下のように訳されます。
E1 >>= fun () =>
do Stmt
...
En
最後に、do
ブロックの最初の文が :=
を使った let
の場合、翻訳された形は普通のlet式になります。したがって、
do let x := E1
Stmt
...
En
は以下のように訳されます。
let x := E1
do Stmt
...
En
Monad
クラスを用いた firstThirdFifthSeventh
の定義は以下のようなものでした:
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)
do
記法を使うことで、劇的に読みやすくなります:
def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α) := do
let first ← lookup xs 0
let third ← lookup xs 2
let fifth ← lookup xs 4
let seventh ← lookup xs 6
pure (first, third, fifth, seventh)
Monad
型クラスを用いずに、木のノードに採番する関数 number
は次のように記述しました:
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
Monad
と do
を用いると、定義からわずらわしさが軽減されます:
def number (t : BinTree α) : BinTree (Nat × α) :=
let rec helper : BinTree α → State Nat (BinTree (Nat × α))
| BinTree.leaf => pure BinTree.leaf
| BinTree.branch left x right => do
let numberedLeft ← helper left
let n ← get
set (n + 1)
let numberedRight ← helper right
ok (BinTree.branch numberedLeft (n, x) numberedRight)
(helper t 0).snd
IO
について do
で得られた恩恵は、ほかのモナドでも享受できます。例えば、ネストされたアクションはどのモナドでも動作します。もともとの mapM
の定義は以下の通りです:
def mapM [Monad m] (f : α → m β) : List α → m (List β)
| [] => pure []
| x :: xs =>
f x >>= fun hd =>
mapM f xs >>= fun tl =>
pure (hd :: tl)
do
記法によって、これは以下のように書くことができます:
def mapM [Monad m] (f : α → m β) : List α → m (List β)
| [] => pure []
| x :: xs => do
let hd ← f x
let tl ← mapM f xs
pure (hd :: tl)
ネストされたアクションを使うことで、もとの非モナドな map
と同じくらい短い記述にすることができます:
def mapM [Monad m] (f : α → m β) : List α → m (List β)
| [] => pure []
| x :: xs => do
pure ((← f x) :: (← mapM f xs))
ネストされたアクションを使うことで、number
をより簡潔にすることができます:
def increment : State Nat Nat := do
let n ← get
set (n + 1)
pure n
def number (t : BinTree α) : BinTree (Nat × α) :=
let rec helper : BinTree α → State Nat (BinTree (Nat × α))
| BinTree.leaf => pure BinTree.leaf
| BinTree.branch left x right => do
pure (BinTree.branch (← helper left) ((← increment), x) (← helper right))
(helper t 0).snd
演習問題
evaluateM
とそのヘルパー、そしていくつかの異なるユースケース例を、>>=
を明示的に呼び出す代わりにdo
記法を使用して書き直してください。firstThirdFifthSeventh
をネストされたアクションを使って書き直してください。