diff --git a/examples/early-return/EarlyReturn.lean b/examples/early-return/EarlyReturn.lean index 87f8e8f4..41bab5c0 100644 --- a/examples/early-return/EarlyReturn.lean +++ b/examples/early-return/EarlyReturn.lean @@ -50,6 +50,6 @@ theorem mains_match : main = Nested.main := by simp [main, Nested.main] simp [bind, EStateM.bind, EStateM.pure, liftM, monadLift, pure, ite] funext s - repeat split <;> try simp + repeat split <;> try simp_all cases argv <;> - simp [instDecidableEqString, instDecidableEqList, List.hasDecEq, bne, BEq.beq, List.beq, not, instDecidableEqBool, Bool.decEq] + simp [instDecidableEqString, instDecidableEqList, List.hasDecEq, bne, BEq.beq, List.beq, not, instDecidableEqBool, Bool.decEq, IO.FS.Stream.putStrLn, IO.FS.Stream.putStr, String.push, String.decEq, String.trim, instDecidableNot, *] diff --git a/functional-programming-lean/src/SUMMARY.md b/functional-programming-lean/src/SUMMARY.md index 12115b6c..3016ef01 100644 --- a/functional-programming-lean/src/SUMMARY.md +++ b/functional-programming-lean/src/SUMMARY.md @@ -49,7 +49,7 @@ - [IOとReaderを組み合わせる](monad-transformers/reader-io.md) - [モナド組み立てキット](monad-transformers/transformers.md) - [モナド変換子の順序](monad-transformers/order.md) - - [More `do` Features](monad-transformers/do.md) + - [さらなる `do` の機能](monad-transformers/do.md) - [Additional Conveniences](monad-transformers/conveniences.md) - [Summary](monad-transformers/summary.md) - [Programming with Dependent Types](dependent-types.md) diff --git a/functional-programming-lean/src/monad-transformers/do.md b/functional-programming-lean/src/monad-transformers/do.md index 70947717..31c4d7a2 100644 --- a/functional-programming-lean/src/monad-transformers/do.md +++ b/functional-programming-lean/src/monad-transformers/do.md @@ -1,108 +1,211 @@ + +# さらなる `do` の機能 + + + +Leanの `do` 記法はモナドを使ったプログラムを書くにあたって命令型プログラミング言語と同じように書くための構文を提供しています。`do` 記法はモナドを使ったプログラムのための構文を提供するだけでなく、ある種のモナド変換子を使うための構文を提供しています。 + +## 分岐1つの `if` + + + +モナドを扱うときによくあるパターンはある条件が真である場合にのみ副作用を実行することです。例えば、`countLetters` は母音か子音かのチェックを含んでおり、どちらでもない文字は状態に影響を与えません。これは `else` ブランチが `pure ()` に評価されることで捕捉されます: + ```lean {{#example_decl Examples/MonadTransformers/Defs.lean countLettersModify}} ``` + + +`if` が式ではなく、`do` ブロック内の文である場合、`else pure ()` は単に省略することができ、Leanは自動的に補完します。以下の `countLetters` の定義は完全に等価です: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean countLettersNoElse}} ``` + + +状態モナドを使ってあるモナド的なチェックを満たすリストの項目を数えるプログラムは次のように書くことができます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean count}} ``` + + +同様に、`if not E1 then STMT...` は代わりに `unless E1 do STMT...` と書くことができます。モナドチェックを満たさない要素をカウントする `count` の逆は `if` を `unless` に置き換えて書くことができます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean countNot}} ``` + + +分岐1つの `if` と `unless` を理解するのに、モナド変換子について考える必要はありません。これらは単に足りない分岐を `pure ()` に置き換えるだけです。しかし本節の残りで紹介する拡張機能は、Leanが `do` ブロックを自動的に書き換えて、`do` ブロックが書かれているモナドの上にローカルな変換子を追加する必要があります。 + +## 早期リターン + + + +標準ライブラリにはあるチェックを満たすリストの最初の要素を返す `List.find?` という関数があります。`Option` がモナドであることを利用しないシンプルな実装では、再帰関数を使ってリスト上をループし、お望みの要素のところで `if` でループを止めます。 + ```lean {{#example_decl Examples/MonadTransformers/Do.lean findHuhSimple}} ``` + + +命令型言語では関数の実行を中断するのに通常 `return` キーワードを用いて呼び出し元に値を返します。Leanでは、これを `do` 記法で使用することができます。`return` は `do` ブロックの実行を停止し、`return` に渡された引数をそのモナドから返される値とします。つまり、`List.find?` は以下のように書くことができます。 + ```lean {{#example_decl Examples/MonadTransformers/Do.lean findHuhFancy}} ``` + + +命令型言語の早期リターンは現在のスタックフレームを巻き戻すだけの例外に似ています。早期リターンと例外はどちらもコードブロックの実行を終了し、そのコードの結果を投げられた例外の値で効率的に置き換えます。裏側では、Leanにおいての早期リターンは `ExceptT` を用いて実装されています。早期リターンを用いる各 `do` ブロックは例外ハンドラ(関数 `tryCatch` において用いられる意味)でラップされています。早期リターンは例外として値を投げることに変換され、ハンドラは投げられた値をキャッチしてそのまま返します。言い換えると、`do` ブロックの元の戻り値の型は例外の型としても使われます。 + + +これをより具体的にすると、補助関数 `runCatch` は例外の型と戻り値の型が同じ時にモナド変換子のスタックの一番上から `ExceptT` の層を取り除きます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean runCatch}} ``` + + +`List.find?` を `do` ブロックで早期リターンを使用する実装から使用しない実装に変換するには、`do` ブロックを `runCatch` で包み、早期リターンを `throw` に置き換えます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean desugaredFindHuh}} ``` + + +早期リターンを用いた方が良い別のシチュエーションとして、引数や入力が正しくない場合に早期に終了するコマンドラインアプリがあります。多くのプログラムでは、プログラム本体に進む前に引数や入力を検証するセクションから始まります。次のバージョンの [挨拶プログラム `hello-name`](../hello-world/running-a-program.md) はコマンドライン引数が与えられていないことをチェックします: + ```lean {{#include ../../../examples/early-return/EarlyReturn.lean:main}} ``` + + +これを引数無しで実行し、`David` という名前を入力すると以前のものと同じ結果になります: + ``` $ {{#command {early-return} {early-return} {./run} {lean --run EarlyReturn.lean}}} {{#command_out {early-return} {./run} }} ``` + + +しかし入力待ちへの回答の代わりにコマンドライン引数として名前を指定するとエラーになります: + ``` $ {{#command {early-return} {early-return} {./too-many-args} {lean --run EarlyReturn.lean David}}} {{#command_out {early-return} {./too-many-args} }} ``` + + +そして名前を入力しない場合は別のエラーになります: + ``` $ {{#command {early-return} {early-return} {./no-name} {lean --run EarlyReturn.lean}}} {{#command_out {early-return} {./no-name} }} ``` + + +上記で見たように早期リターンを使うプログラムでは制御の流れをネストする必要が無くなりますが、これを早期リターンを使わないように実装すると以下のようになります: + ```lean {{#include ../../../examples/early-return/EarlyReturn.lean:nestedmain}} ``` + + +早期リターンについてLeanと命令型言語でのそれの大きな違いは、Leanの早期リターンは現在の `do` ブロックのみに適用されるという点です。関数の定義全体が1つの同じ `do` ブロック内にある場合、この違いは問題になりません。しかし、`do` が他の構造体の中にある場合はその違いが明らかになります。例えば、`greet` の以下の定義について: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean greet}} ``` + +式 `{{#example_in Examples/MonadTransformers/Do.lean greetDavid}}` を評価すると `David` ではなく `{{#example_out Examples/MonadTransformers/Do.lean greetDavid}}` になります。 + + + +## 繰り返し処理 + +可変状態を扱うような全てのプログラムが状態を引数として受け取るプログラムとして書けるように、すべての繰り返しは再帰関数として書くことができます。その観点で言えば、`List.find?` はまさに再帰関数として見ることができます。結論から言うと、その場合の定義はリストの構造を反映したものになっています:もし先頭がチェックを通過すればその要素が返されます;さもなくば後続のリストを見に行きます。もしリストに要素が1つも無ければ、結果は `none` になります。一方で見方を変えれば、`List.find?` は繰り返し処理の関数として見ることができます。この関数はとどのつまり、チェックを満たすものが見つかるまで順番に要素を調べ、見つかった時点で終了するものだからです。ループが戻らずに終了した場合、結果は `none` になります。 + + + +### `ForM` による繰り返し + + +Leanにはコンテナ型に対する繰り返しをモナド上で行うことを記述する型クラスがあります。このクラスは `ForM` と呼ばれます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean ForM}} ``` + +この定義はとても汎用的です。パラメータ `m` は想定している作用を持つモナド、`γ` は繰り返しを行うコレクション、そして `α` はコレクションの要素の型です。通常、`m` はどんなモナドでも構いませんが、例えば `IO` での繰り返し処理のみをサポートするようなデータ構造とすることも可能です。メソッド `forM` はコレクションと各要素に作用を及ぼすモナドのアクションを受け取り、アクションの実行を担います。 + + + +このクラスの `List` に対するインスタンスは `m` としてどんなモナドでも取ることができます。`γ` には `List α` を、クラスの `α` にはリストに渡しているものと同じ `α` を設定します: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean ListForM}} ``` + + +[`doug` で使った関数 `doList`](reader-io.md#implementation) はリスト用の `forM` です。`forM` は `do` ブロックで使われることを想定されているため、`Applicative` ではなく `Monad` を用います。`forM` を使うことで `countLetters` はさらに短くなります: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean countLettersForM}} ``` + + +これの `Many` に対するインスタンスも同じようなものになります: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean ManyForM}} ``` + + +`γ` はどんな型でもよいため、`ForM` は多相的ではないコレクションもサポートしています。非常に単純なコレクションとして、与えられた数より小さい自然数を降順に並べたものを考えます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean AllLessThan}} ``` + + +これの `forM` 演算子は指定されたアクションをそれぞれの小さい `Nat` に適用します: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean AllLessThanForM}} ``` + + +`IO.println` を5未満の各数値に適用することは `forM` で以下のように実装できます: + ```lean {{#example_in Examples/MonadTransformers/Do.lean AllLessThanForMRun}} ``` @@ -157,41 +306,84 @@ Running `IO.println` on each number less than five can be accomplished with `for {{#example_out Examples/MonadTransformers/Do.lean AllLessThanForMRun}} ``` + + +特定のモナドでのみ動作する `ForM` インスタンスの例として、標準入力のようなIOストリームから読み込まれた行に対してループするものがあります: + ```lean {{#include ../../../examples/formio/ForMIO.lean:LinesOf}} ``` + + +この `forM` の定義はストリームが有限である保証がないことから `partial` とマークされています。この場合、`IO.FS.Stream.getLine` は `IO` モナドのみで動作するため他のモナドをループに使用することができません。 + + +次のサンプルプログラムではこの繰り返し構造を使って、文字を含まない行をフィルタリングします: + ```lean {{#include ../../../examples/formio/ForMIO.lean:main}} ``` + + +`test-data` ファイルの中身が以下の場合: + ``` {{#include ../../../examples/formio/test-data}} ``` + + +`ForMIO.lean` に格納されているこのプログラムを実行すると次のような出力が得られます: + ``` $ {{#command {formio} {formio} {lean --run ForMIO.lean < test-data}}} {{#command_out {formio} {lean --run ForMIO.lean < test-data} {formio/expected}}} ``` + + +### 繰り返し処理の停止 + + +`forM` を使う場合、繰り返し処理の途中で早期に終了することは難しいです。`AllLessThan` 内の `Nat` を `3` に達するまで繰り返し処理する関数を書くには、繰り返しを途中で止める手段が必要になります。これを実現する1つの方法は、`OptionT` モナド変換子と一緒に `forM` を使うことです。そのためにまず `OptionT.exec` を定義して、戻り値と変換された計算が成功したかどうかの両方の情報を破棄します: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean OptionTExec}} ``` + + +そして `OptionT` の `Alternative` インスタンスで失敗させるようにすることで、繰り返し処理を早期に終了させることができます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean OptionTcountToThree}} ``` + + +以下の簡易的なテストで、この解決策が機能することが確認できます: + ```lean {{#example_in Examples/MonadTransformers/Do.lean optionTCountSeven}} ``` @@ -199,13 +391,23 @@ A quick test demonstrates that this solution works: {{#example_out Examples/MonadTransformers/Do.lean optionTCountSeven}} ``` + + +しかし、このコードはあまり読みやすくありません。繰り返し処理を早期に終了することは一般的なタスクであることから、Leanはこれを容易に実現できるよう追加の糖衣構文を用意しています。上記の関数は以下のようにも書けます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean countToThree}} ``` + + +試しに動かしてみると前のものと同じように動作することがはっきりするでしょう: + ```lean {{#example_in Examples/MonadTransformers/Do.lean countSevenFor}} ``` @@ -213,61 +415,112 @@ Testing it reveals that it works just like the prior version: {{#example_out Examples/MonadTransformers/Do.lean countSevenFor}} ``` + + +この文章を書いている時点では、構文 `for ... in ... do ...` は `ForIn` という型クラスを使用したものに脱糖されます。このクラスは状態と早期リターンを担保した `ForM` をより複雑にしたものです。しかし、`for` ループをリファクタリングして、よりシンプルな `ForM` を使うようにする計画があります。それまでの間、`ForM.forIn` という `ForM` インスタンスを `ForIn` インスタンスに変換するアダプタが用意されています。`ForM` インスタンスに基づく `for` ループを使えるようにするには、以下のように `AllLessThan` と `Nat` を適切に置き換えて追加します: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean ForInIOAllLessThan}} ``` + +ただし、このアダプタは(ほとんどのものがそうですが)モナドの制約を受けない `ForM` インスタンスにしか使えないことに注意してください。これは、このアダプタがベースのモナドではなく `StateT` と `ExceptT` を使用するためです。 + + + +早期リターンは `for` ループでサポートされています。早期リターンを伴う `do` ブロックを例外のモナド変換子を使うものに変換する流れは、`forM` の中でも以前の `OptionT` による繰り返しの停止と同じように適用できます。このバージョンの `List.find?` はどちらも用います: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean findHuh}} ``` + + +`break` に加え、`for` ループは繰り返し内でループ本体の残りをスキップするための `continue` をサポートしています。上記とは別の(しかしわかりづらい) `List.find?` の形式化はチェックを満たさない要素をスキップします: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean findHuhCont}} ``` + + +`Range` は開始番号、終了番号、ステップからなる構造体です。これは開始番号から始まり終了番号までステップずつ増えていく整数の数列を表しています。Leanではこの範囲を構成するための特別な記法を用意しており、角括弧と数値、そしてコロンを用いた4つの組み合わせによって記述できます。終点は必ず指定しなければなりませんが、始点とステップは任意で、デフォルトではそれぞれ `0` と `1` になります: + + +| 式 | 開始 | 終了 | ステップ | リストとしての値 | |------------|------------|------------|------|---------| | `[:10]` | `0` | `10` | `1` | `{{#example_out Examples/MonadTransformers/Do.lean rangeStopContents}}` | | `[2:10]` | `2` | `10` | `1` | `{{#example_out Examples/MonadTransformers/Do.lean rangeStartStopContents}}` | | `[:10:3]` | `0` | `10` | `3` | `{{#example_out Examples/MonadTransformers/Do.lean rangeStopStepContents}}` | | `[2:10:3]` | `2` | `10` | `3` | `{{#example_out Examples/MonadTransformers/Do.lean rangeStartStopStepContents}}` | + + +開始番号が範囲に含まれて **いる** 一方で終了番号は含まれていないことに注意してください。3つの引数はすべて `Nat` であり、これは範囲を逆向きに数えることができないことを意味します。つまり開始番号が終了番号以上であるような範囲では、単に何の数値も含まなくなります。 + + +範囲は `for` ループと一緒に使うことで範囲から数値を引き出すことができます。次のプログラムは4から8までの偶数を数えます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean fourToEight}} ``` + + +実行すると次を得ます: + ```output info {{#example_out Examples/MonadTransformers/Do.lean fourToEightOut}} ``` + + +最後に、`for` ループは `in` 節をカンマで区切ることで複数のコレクションを並列に繰り返し処理することができます。繰り返しは最初のコレクションの要素がなくなると停止するので、次の宣言: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean parallelLoop}} ``` + + +は以下の3行を出力します: + ```lean {{#example_in Examples/MonadTransformers/Do.lean parallelLoopOut}} ``` @@ -275,81 +528,156 @@ produces three lines of output: {{#example_out Examples/MonadTransformers/Do.lean parallelLoopOut}} ``` + +## 可変変数 + + + +早期の `return` 、`else` の無い `if` 、`for` ループに加えて、Leanは `do` ブロック内で使える局所可変変数をサポートしています。裏側では、これらの可変変数は、本当の意味での可変変数としての実装にではなく、`StateT` を使うように脱糖されます。繰り返しになりますが、関数プログラミングは命令型言語をシミュレートすることができます。 + + +局所可変変数はただの `let` の代わりに `let mut` で導入します。以下の定義 `two` は恒等モナド `Id` を使って作用を持ち込まない `do` 記法を利用しており、`2` になります: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean two}} ``` + + +このコードは `StateT` を使って `1` を2回加算する定義と同じです: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean twoStateT}} ``` + + +局所可変変数はモナド変換子のための便利な記法を提供する `do` 記法の他の全ての機能とうまく連動します。定義 `three` は要素数が3つの数値リストの数を数えます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean three}} ``` + + +同じように、`six` はリストの要素を足し合わせます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean six}} ``` + + +`List.count` はリスト内で何らかのチェックを満たす要素の数を数えます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean ListCount}} ``` + + +局所可変変数は明示的にローカルで `StateT` を使用するよりも使いやすく、読みやすくなります。しかし、命令型言語での無制限な可変変数のような完全な力は持っていません。特に、これらは導入された `do` ブロックの中でしか変更できません。これは、例えば `for` ループを同じ機能を持つ再帰的な補助関数に置き換えることができないことを意味します。このバージョンの `List.count` : + ```lean {{#example_in Examples/MonadTransformers/Do.lean nonLocalMut}} ``` + + +は `found` を更新しようとした時に次のようなエラーを出します: + ```output info {{#example_out Examples/MonadTransformers/Do.lean nonLocalMut}} ``` + +これは再帰関数が恒等モナドで記述され、変数が導入された `do` ブロックのモナドだけが `StateT` で変換されるからです。 + + + +## どこまでを `do` ブロックとみなすか? + +`do` 記法の多くの機能は1つの `do` ブロックにのみ適用されます。早期リターンは現在のブロックを終了させ、可変変数はそれが定義されたブロックの中でしか可変にできません。これらを効果的に使うには、何をもって「同じブロック」であるのかを知ることが重要です。 + + + +一般的に言って、`do` キーワードにつづくインデントされたブロックはブロックとみなされ、その内部にある一連の文はブロックの一部となります。しかし、ブロックに含まれている独立したブロックの文は、含まれているにもかかわらず外側のブロックの一部とはみなされません。ただし、実際に何を同じブロックとみなすかはやや曖昧であるため、いくつかの例を挙げておきましょう。ルールの性質は可変変数を持つプログラムを用意し、どこで変数の更新が可能かをみることで正確にテストすることができます。以下のプログラムでは変数の更新が含まれており、このことからこの更新が可変変数と同じブロックの中にあることがはっきりします: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean sameBlock}} ``` + + +`:=` を使った `let` 文の名前定義の一部が `do` ブロックで、そのブロック中で更新が起こった場合はこの更新は外側のブロックの一部とはみなされません: + ```lean {{#example_in Examples/MonadTransformers/Do.lean letBodyNotBlock}} ``` ```output error {{#example_out Examples/MonadTransformers/Do.lean letBodyNotBlock}} ``` + + +しかし、`do` ブロックが `←` を使った `let` の名前定義内にある場合、これは外側のブロックの一部とみなされます。次のプログラムは正常に動きます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean letBodyArrBlock}} ``` + + +同じように、`do` ブロックが関数の引数に置かれている場合も外側のブロックから独立します。次のプログラムは正常に動きます: + ```lean {{#example_in Examples/MonadTransformers/Do.lean funArgNotBlock}} ``` @@ -357,14 +685,24 @@ The following program is not accepted: {{#example_out Examples/MonadTransformers/Do.lean funArgNotBlock}} ``` + + +`do` キーワードが完全に冗長である場合、新しいブロックは導入されません。次のプログラムは正常に動き、本節の最初のプログラムと等価です: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean collapsedBlock}} ``` + + +`do` の下にある(`match` や `if` で導入されるような)分岐の内容は冗長な `do` の有無にかかわらず、外側のブロックの一部とみなされます。以下のプログラムはすべて正常に動きます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean ifDoSame}} @@ -374,8 +712,13 @@ The following programs are all accepted: {{#example_decl Examples/MonadTransformers/Do.lean matchDoDoSame}} ``` + + +同じように、`for` や `unless` 記法の一部として出てくる `do` は構文の一部に過ぎず、新しい `do` ブロックを導入するものではありません。以下のプログラムも正常に動きます: + ```lean {{#example_decl Examples/MonadTransformers/Do.lean doForSame}} @@ -383,15 +726,29 @@ These programs are also accepted: ``` + + +## 命令型か関数型か? + +Leanの `do` 記法がもたらす命令的な機能によって、多くのプログラムはRustやJava、C#のような言語によるそれと同等なプログラムと非常によく似たものになります。この類似性は命令型のアルゴリズムをLeanに翻訳する際に非常に便利です。実際にいくつかのタスクでは命令的に考えるほうがとても自然です。モナドとモナド変換子の導入により、命令型プログラムを純粋関数型言語で書くことができるようになり、モナドに特化した構文である `do` 記法(局所的に変換される可能性あり)により関数型プログラマは2つの長所を得ることができます:不変性と型システムを通じて利用可能な作用を厳密に制御することによって得られる強力な推論原理と、作用を使用するプログラムを見慣れたものにし読みやすくする構文とライブラリのコンビです。モナドとモナド変換子によって関数型プログラミングと命令型プログラミングの違いは見方の問題に帰着します。 + + +## 演習問題 + + * `doug` を `doList` 関数の代わりに `for` を使って書き直してください。本節で紹介した機能を使ってコードを改善できそうな箇所はありそうでしょうか?あったらやってみましょう!