モナドのための 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 をネストされたアクションを使って書き直してください。