さらなる do の機能

Leanの do 記法はモナドを使ったプログラムを書くにあたって命令型プログラミング言語と同じように書くための構文を提供しています。do 記法はモナドを使ったプログラムのための構文を提供するだけでなく、ある種のモナド変換子を使うための構文を提供しています。

分岐1つの if

モナドを扱うときによくあるパターンはある条件が真である場合にのみ副作用を実行することです。例えば、countLetters は母音か子音かのチェックを含んでおり、どちらでもない文字は状態に影響を与えません。これは else ブランチが pure () に評価されることで捕捉されます：

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

if が式ではなく、do ブロック内の文である場合、else pure () は単に省略することができ、Leanは自動的に補完します。以下の countLetters の定義は完全に等価です：

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 throw (.notALetter c)
      loop cs
  loop str.toList

状態モナドを使ってあるモナド的なチェックを満たすリストの項目を数えるプログラムは次のように書くことができます：

def count [Monad m] [MonadState Nat m] (p : α → m Bool) : List α → m Unit
  | [] => pure ()
  | x :: xs => do
    if ← p x then
      modify (· + 1)
    count p xs

同様に、if not E1 then STMT... は代わりに unless E1 do STMT... と書くことができます。モナドチェックを満たさない要素をカウントする count の逆は if を unless に置き換えて書くことができます：

def countNot [Monad m] [MonadState Nat m] (p : α → m Bool) : List α → m Unit
  | [] => pure ()
  | x :: xs => do
    unless ← p x do
      modify (· + 1)
    countNot p xs

分岐1つの if と unless を理解するのに、モナド変換子について考える必要はありません。これらは単に足りない分岐を pure () に置き換えるだけです。しかし本節の残りで紹介する拡張機能は、Leanが do ブロックを自動的に書き換えて、do ブロックが書かれているモナドの上にローカルな変換子を追加する必要があります。

早期リターン

標準ライブラリにはあるチェックを満たすリストの最初の要素を返す List.find? という関数があります。Option がモナドであることを利用しないシンプルな実装では、再帰関数を使ってリスト上をループし、お望みの要素のところで if でループを止めます。

def List.find? (p : α → Bool) : List α → Option α
  | [] => none
  | x :: xs =>
    if p x then
      some x
    else
      find? p xs

命令型言語では関数の実行を中断するのに通常 return キーワードを用いて呼び出し元に値を返します。Leanでは、これを do 記法で使用することができます。return は do ブロックの実行を停止し、return に渡された引数をそのモナドから返される値とします。つまり、List.find? は以下のように書くことができます。

def List.find? (p : α → Bool) : List α → Option α
  | [] => failure
  | x :: xs => do
    if p x then return x
    find? p xs

命令型言語の早期リターンは現在のスタックフレームを巻き戻すだけの例外に似ています。早期リターンと例外はどちらもコードブロックの実行を終了し、そのコードの結果を投げられた例外の値で効率的に置き換えます。裏側では、Leanにおいての早期リターンは ExceptT を用いて実装されています。早期リターンを用いる各 do ブロックは例外ハンドラ（関数 tryCatch において用いられる意味）でラップされています。早期リターンは例外として値を投げることに変換され、ハンドラは投げられた値をキャッチしてそのまま返します。言い換えると、do ブロックの元の戻り値の型は例外の型としても使われます。

これをより具体的にすると、補助関数 runCatch は例外の型と戻り値の型が同じ時にモナド変換子のスタックの一番上から ExceptT の層を取り除きます：

def runCatch [Monad m] (action : ExceptT α m α) : m α := do
  match ← action with
  | Except.ok x => pure x
  | Except.error x => pure x

List.find? を do ブロックで早期リターンを使用する実装から使用しない実装に変換するには、do ブロックを runCatch で包み、早期リターンを throw に置き換えます：

def List.find? (p : α → Bool) : List α → Option α
  | [] => failure
  | x :: xs =>
    runCatch do
      if p x then throw x else pure ()
      monadLift (find? p xs)

早期リターンを用いた方が良い別のシチュエーションとして、引数や入力が正しくない場合に早期に終了するコマンドラインアプリがあります。多くのプログラムでは、プログラム本体に進む前に引数や入力を検証するセクションから始まります。次のバージョンの 挨拶プログラム hello-name はコマンドライン引数が与えられていないことをチェックします：

def main (argv : List String) : IO UInt32 := do
  let stdin ← IO.getStdin
  let stdout ← IO.getStdout
  let stderr ← IO.getStderr

  unless argv == [] do
    stderr.putStrLn s!"Expected no arguments, but got {argv.length}"
    return 1

  stdout.putStrLn "How would you like to be addressed?"
  stdout.flush

  let name := (← stdin.getLine).trim
  if name == "" then
    stderr.putStrLn s!"No name provided"
    return 1

  stdout.putStrLn s!"Hello, {name}!"

  return 0

これを引数無しで実行し、David という名前を入力すると以前のものと同じ結果になります：

$ lean --run EarlyReturn.lean
How would you like to be addressed?
David
Hello, David!

しかし入力待ちへの回答の代わりにコマンドライン引数として名前を指定するとエラーになります：

$ lean --run EarlyReturn.lean David
Expected no arguments, but got 1

そして名前を入力しない場合は別のエラーになります：

$ lean --run EarlyReturn.lean
How would you like to be addressed?

No name provided

上記で見たように早期リターンを使うプログラムでは制御の流れをネストする必要が無くなりますが、これを早期リターンを使わないように実装すると以下のようになります：

def main (argv : List String) : IO UInt32 := do
  let stdin ← IO.getStdin
  let stdout ← IO.getStdout
  let stderr ← IO.getStderr

  if argv != [] then
    stderr.putStrLn s!"Expected no arguments, but got {argv.length}"
    pure 1
  else
    stdout.putStrLn "How would you like to be addressed?"
    stdout.flush

    let name := (← stdin.getLine).trim
    if name == "" then
      stderr.putStrLn s!"No name provided"
      pure 1
    else
      stdout.putStrLn s!"Hello, {name}!"
      pure 0

早期リターンについてLeanと命令型言語でのそれの大きな違いは、Leanの早期リターンは現在の do ブロックのみに適用されるという点です。関数の定義全体が1つの同じ do ブロック内にある場合、この違いは問題になりません。しかし、do が他の構造体の中にある場合はその違いが明らかになります。例えば、greet の以下の定義について：

def greet (name : String) : String :=
  "Hello, " ++ Id.run do return name

式 greet "David" を評価すると David ではなく "Hello, David" になります。

繰り返し処理

可変状態を扱うような全てのプログラムが状態を引数として受け取るプログラムとして書けるように、すべての繰り返しは再帰関数として書くことができます。その観点で言えば、List.find? はまさに再帰関数として見ることができます。結論から言うと、その場合の定義はリストの構造を反映したものになっています：もし先頭がチェックを通過すればその要素が返されます；さもなくば後続のリストを見に行きます。もしリストに要素が1つも無ければ、結果は none になります。一方で見方を変えれば、List.find? は繰り返し処理の関数として見ることができます。この関数はとどのつまり、チェックを満たすものが見つかるまで順番に要素を調べ、見つかった時点で終了するものだからです。ループが戻らずに終了した場合、結果は none になります。

ForM による繰り返し

Leanにはコンテナ型に対する繰り返しをモナド上で行うことを記述する型クラスがあります。このクラスは ForM と呼ばれます：

class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂)) where
  forM [Monad m] : γ → (α → m PUnit) → m PUnit

この定義はとても汎用的です。パラメータ m は想定している作用を持つモナド、γ は繰り返しを行うコレクション、そして α はコレクションの要素の型です。通常、m はどんなモナドでも構いませんが、例えば IO での繰り返し処理のみをサポートするようなデータ構造とすることも可能です。メソッド forM はコレクションと各要素に作用を及ぼすモナドのアクションを受け取り、アクションの実行を担います。

このクラスの List に対するインスタンスは m としてどんなモナドでも取ることができます。γ には List α を、クラスの α にはリストに渡しているものと同じ α を設定します：

def List.forM [Monad m] : List α → (α → m PUnit) → m PUnit
  | [], _ => pure ()
  | x :: xs, action => do
    action x
    forM xs action

instance : ForM m (List α) α where
  forM := List.forM

doug で使った関数 doList はリスト用の forM です。forM は do ブロックで使われることを想定されているため、Applicative ではなく Monad を用います。forM を使うことで countLetters はさらに短くなります：

def countLetters (str : String) : StateT LetterCounts (Except Err) Unit :=
  forM str.toList fun c => do
    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 throw (.notALetter c)

これの Many に対するインスタンスも同じようなものになります：

def Many.forM [Monad m] : Many α → (α → m PUnit) → m PUnit
  | Many.none, _ => pure ()
  | Many.more first rest, action => do
    action first
    forM (rest ()) action

instance : ForM m (Many α) α where
  forM := Many.forM

γ はどんな型でもよいため、ForM は多相的ではないコレクションもサポートしています。非常に単純なコレクションとして、与えられた数より小さい自然数を降順に並べたものを考えます：

structure AllLessThan where
  num : Nat

これの forM 演算子は指定されたアクションをそれぞれの小さい Nat に適用します：

def AllLessThan.forM [Monad m] (coll : AllLessThan) (action : Nat → m Unit) : m Unit :=
  let rec countdown : Nat → m Unit
    | 0 => pure ()
    | n + 1 => do
      action n
      countdown n
  countdown coll.num

instance : ForM m AllLessThan Nat where
  forM := AllLessThan.forM

IO.println を5未満の各数値に適用することは forM で以下のように実装できます：

#eval forM { num := 5 : AllLessThan } IO.println

4
3
2
1
0

特定のモナドでのみ動作する ForM インスタンスの例として、標準入力のようなIOストリームから読み込まれた行に対してループするものがあります：

structure LinesOf where
  stream : IO.FS.Stream

partial def LinesOf.forM (readFrom : LinesOf) (action : String → IO Unit) : IO Unit := do
  let line ← readFrom.stream.getLine
  if line == "" then return ()
  action line
  forM readFrom action

instance : ForM IO LinesOf String where
  forM := LinesOf.forM

この forM の定義はストリームが有限である保証がないことから partial とマークされています。この場合、IO.FS.Stream.getLine は IO モナドのみで動作するため他のモナドをループに使用することができません。

次のサンプルプログラムではこの繰り返し構造を使って、文字を含まない行をフィルタリングします：

def main (argv : List String) : IO UInt32 := do
  if argv != [] then
    IO.eprintln "Unexpected arguments"
    return 1

  forM (LinesOf.mk (← IO.getStdin)) fun line => do
    if line.any (·.isAlpha) then
      IO.print line

  return 0

test-data ファイルの中身が以下の場合：

Hello!
!!!!!
12345
abc123

Ok

ForMIO.lean に格納されているこのプログラムを実行すると次のような出力が得られます：

$ lean --run ForMIO.lean < test-data
Hello!
abc123
Ok

繰り返し処理の停止

forM を使う場合、繰り返し処理の途中で早期に終了することは難しいです。AllLessThan 内の Nat を 3 に達するまで繰り返し処理する関数を書くには、繰り返しを途中で止める手段が必要になります。これを実現する1つの方法は、OptionT モナド変換子と一緒に forM を使うことです。そのためにまず OptionT.exec を定義して、戻り値と変換された計算が成功したかどうかの両方の情報を破棄します：

def OptionT.exec [Applicative m] (action : OptionT m α) : m Unit :=
  action *> pure ()

そして OptionT の Alternative インスタンスで失敗させるようにすることで、繰り返し処理を早期に終了させることができます：

def countToThree (n : Nat) : IO Unit :=
  let nums : AllLessThan := ⟨n⟩
  OptionT.exec (forM nums fun i => do
    if i < 3 then failure else IO.println i)

以下の簡易的なテストで、この解決策が機能することが確認できます：

#eval countToThree 7

6
5
4
3

しかし、このコードはあまり読みやすくありません。繰り返し処理を早期に終了することは一般的なタスクであることから、Leanはこれを容易に実現できるよう追加の糖衣構文を用意しています。上記の関数は以下のようにも書けます：

def countToThree (n : Nat) : IO Unit := do
  let nums : AllLessThan := ⟨n⟩
  for i in nums do
    if i < 3 then break
    IO.println i

試しに動かしてみると前のものと同じように動作することがはっきりするでしょう：

#eval countToThree 7

6
5
4
3

この文章を書いている時点では、構文 for ... in ... do ... は ForIn という型クラスを使用したものに脱糖されます。このクラスは状態と早期リターンを担保した ForM をより複雑にしたものです。しかし、for ループをリファクタリングして、よりシンプルな ForM を使うようにする計画があります。それまでの間、ForM.forIn という ForM インスタンスを ForIn インスタンスに変換するアダプタが用意されています。ForM インスタンスに基づく for ループを使えるようにするには、以下のように AllLessThan と Nat を適切に置き換えて追加します：

instance : ForIn m AllLessThan Nat where
  forIn := ForM.forIn

ただし、このアダプタは（ほとんどのものがそうですが）モナドの制約を受けない ForM インスタンスにしか使えないことに注意してください。これは、このアダプタがベースのモナドではなく StateT と ExceptT を使用するためです。

早期リターンは for ループでサポートされています。早期リターンを伴う do ブロックを例外のモナド変換子を使うものに変換する流れは、forM の中でも以前の OptionT による繰り返しの停止と同じように適用できます。このバージョンの List.find? はどちらも用います：

def List.find? (p : α → Bool) (xs : List α) : Option α := do
  for x in xs do
    if p x then return x
  failure

break に加え、for ループは繰り返し内でループ本体の残りをスキップするための continue をサポートしています。上記とは別の（しかしわかりづらい） List.find? の形式化はチェックを満たさない要素をスキップします：

def List.find? (p : α → Bool) (xs : List α) : Option α := do
  for x in xs do
    if not (p x) then continue
    return x
  failure

Range は開始番号、終了番号、ステップからなる構造体です。これは開始番号から始まり終了番号までステップずつ増えていく整数の数列を表しています。Leanではこの範囲を構成するための特別な記法を用意しており、角括弧と数値、そしてコロンを用いた4つの組み合わせによって記述できます。終点は必ず指定しなければなりませんが、始点とステップは任意で、デフォルトではそれぞれ 0 と 1 になります：

式開始終了ステップリストとしての値
[:10]0101[0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
[2:10]2101[2, 3, 4, 5, 6, 7, 8, 9]
[:10:3]0103[0, 3, 6, 9]
[2:10:3]2103[2, 5, 8]

開始番号が範囲に含まれて いる 一方で終了番号は含まれていないことに注意してください。3つの引数はすべて Nat であり、これは範囲を逆向きに数えることができないことを意味します。つまり開始番号が終了番号以上であるような範囲では、単に何の数値も含まなくなります。

範囲は for ループと一緒に使うことで範囲から数値を引き出すことができます。次のプログラムは4から8までの偶数を数えます：

def fourToEight : IO Unit := do
  for i in [4:9:2] do
    IO.println i

実行すると次を得ます：

4
6
8

最後に、for ループは in 節をカンマで区切ることで複数のコレクションを並列に繰り返し処理することができます。繰り返しは最初のコレクションの要素がなくなると停止するので、次の宣言：

def parallelLoop := do
  for x in ["currant", "gooseberry", "rowan"], y in [4:8] do
    IO.println (x, y)

は以下の3行を出力します：

#eval parallelLoop

(currant, 4)
(gooseberry, 5)
(rowan, 6)

可変変数

早期の return 、else の無い if 、for ループに加えて、Leanは do ブロック内で使える局所可変変数をサポートしています。裏側では、これらの可変変数は、本当の意味での可変変数としての実装にではなく、StateT を使うように脱糖されます。繰り返しになりますが、関数プログラミングは命令型言語をシミュレートすることができます。

局所可変変数はただの let の代わりに let mut で導入します。以下の定義 two は恒等モナド Id を使って作用を持ち込まない do 記法を利用しており、2 になります：

def two : Nat := Id.run do
  let mut x := 0
  x := x + 1
  x := x + 1
  return x

このコードは StateT を使って 1 を2回加算する定義と同じです：

def two : Nat :=
  let block : StateT Nat Id Nat := do
    modify (· + 1)
    modify (· + 1)
    return (← get)
  let (result, _finalState) := block 0
  result

局所可変変数はモナド変換子のための便利な記法を提供する do 記法の他の全ての機能とうまく連動します。定義 three は要素数が3つの数値リストの数を数えます：

def three : Nat := Id.run do
  let mut x := 0
  for _ in [1, 2, 3] do
    x := x + 1
  return x

同じように、six はリストの要素を足し合わせます：

def six : Nat := Id.run do
  let mut x := 0
  for y in [1, 2, 3] do
    x := x + y
  return x

List.count はリスト内で何らかのチェックを満たす要素の数を数えます：

def List.count (p : α → Bool) (xs : List α) : Nat := Id.run do
  let mut found := 0
  for x in xs do
    if p x then found := found + 1
  return found

局所可変変数は明示的にローカルで StateT を使用するよりも使いやすく、読みやすくなります。しかし、命令型言語での無制限な可変変数のような完全な力は持っていません。特に、これらは導入された do ブロックの中でしか変更できません。これは、例えば for ループを同じ機能を持つ再帰的な補助関数に置き換えることができないことを意味します。このバージョンの List.count ：

def List.count (p : α → Bool) (xs : List α) : Nat := Id.run do
  let mut found := 0
  let rec go : List α → Id Unit
    | [] => pure ()
    | y :: ys => do
      if p y then found := found + 1
      go ys
  return found

は found を更新しようとした時に次のようなエラーを出します：

`found` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intent to mutate but define `found`, consider using `let found` instead

これは再帰関数が恒等モナドで記述され、変数が導入された do ブロックのモナドだけが StateT で変換されるからです。

どこまでを do ブロックとみなすか？

do 記法の多くの機能は1つの do ブロックにのみ適用されます。早期リターンは現在のブロックを終了させ、可変変数はそれが定義されたブロックの中でしか可変にできません。これらを効果的に使うには、何をもって「同じブロック」であるのかを知ることが重要です。

一般的に言って、do キーワードにつづくインデントされたブロックはブロックとみなされ、その内部にある一連の文はブロックの一部となります。しかし、ブロックに含まれている独立したブロックの文は、含まれているにもかかわらず外側のブロックの一部とはみなされません。ただし、実際に何を同じブロックとみなすかはやや曖昧であるため、いくつかの例を挙げておきましょう。ルールの性質は可変変数を持つプログラムを用意し、どこで変数の更新が可能かをみることで正確にテストすることができます。以下のプログラムでは変数の更新が含まれており、このことからこの更新が可変変数と同じブロックの中にあることがはっきりします：

example : Id Unit := do
  let mut x := 0
  x := x + 1

:= を使った let 文の名前定義の一部が do ブロックで、そのブロック中で更新が起こった場合はこの更新は外側のブロックの一部とはみなされません：

example : Id Unit := do
  let mut x := 0
  let other := do
    x := x + 1
  other

`x` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intent to mutate but define `x`, consider using `let x` instead

しかし、do ブロックが ← を使った let の名前定義内にある場合、これは外側のブロックの一部とみなされます。次のプログラムは正常に動きます：

example : Id Unit := do
  let mut x := 0
  let other ← do
    x := x + 1
  pure other

同じように、do ブロックが関数の引数に置かれている場合も外側のブロックから独立します。次のプログラムは正常に動きます：

example : Id Unit := do
  let mut x := 0
  let addFour (y : Id Nat) := Id.run y + 4
  addFour do
    x := 5

`x` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intent to mutate but define `x`, consider using `let x` instead

do キーワードが完全に冗長である場合、新しいブロックは導入されません。次のプログラムは正常に動き、本節の最初のプログラムと等価です：

example : Id Unit := do
  let mut x := 0
  do x := x + 1

do の下にある（match や if で導入されるような）分岐の内容は冗長な do の有無にかかわらず、外側のブロックの一部とみなされます。以下のプログラムはすべて正常に動きます：

example : Id Unit := do
  let mut x := 0
  if x > 2 then
    x := x + 1

example : Id Unit := do
  let mut x := 0
  if x > 2 then do
    x := x + 1

example : Id Unit := do
  let mut x := 0
  match true with
  | true => x := x + 1
  | false => x := 17

example : Id Unit := do
  let mut x := 0
  match true with
  | true => do
    x := x + 1
  | false => do
    x := 17

同じように、for や unless 記法の一部として出てくる do は構文の一部に過ぎず、新しい do ブロックを導入するものではありません。以下のプログラムも正常に動きます：

example : Id Unit := do
  let mut x := 0
  for y in [1:5] do
   x := x + y

example : Id Unit := do
  let mut x := 0
  unless 1 < 5 do
    x := x + 1

命令型か関数型か？

Leanの do 記法がもたらす命令的な機能によって、多くのプログラムはRustやJava、C#のような言語によるそれと同等なプログラムと非常によく似たものになります。この類似性は命令型のアルゴリズムをLeanに翻訳する際に非常に便利です。実際にいくつかのタスクでは命令的に考えるほうがとても自然です。モナドとモナド変換子の導入により、命令型プログラムを純粋関数型言語で書くことができるようになり、モナドに特化した構文である do 記法（局所的に変換される可能性あり）により関数型プログラマは2つの長所を得ることができます：不変性と型システムを通じて利用可能な作用を厳密に制御することによって得られる強力な推論原理と、作用を使用するプログラムを見慣れたものにし読みやすくする構文とライブラリのコンビです。モナドとモナド変換子によって関数型プログラミングと命令型プログラミングの違いは見方の問題に帰着します。

演習問題

  • doug を doList 関数の代わりに for を使って書き直してください。本節で紹介した機能を使ってコードを改善できそうな箇所はありそうでしょうか？あったらやってみましょう！