From 38d1e6816b0cc2008d800dee24d2fa99ab9ae888 Mon Sep 17 00:00:00 2001 From: s-taiga <56785231+s-taiga@users.noreply.github.com> Date: Sat, 24 Aug 2024 17:47:49 +0900 Subject: [PATCH] =?UTF-8?q?5.4=E7=AB=A0=20io=20(#47)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 翻訳開始 * 翻訳完了 * コメントアウト位置修正 * セルフレビュー --- functional-programming-lean/src/SUMMARY.md | 2 +- functional-programming-lean/src/monads/io.md | 110 +++++++++++++++++++ 2 files changed, 111 insertions(+), 1 deletion(-) diff --git a/functional-programming-lean/src/SUMMARY.md b/functional-programming-lean/src/SUMMARY.md index af584208..ed271197 100644 --- a/functional-programming-lean/src/SUMMARY.md +++ b/functional-programming-lean/src/SUMMARY.md @@ -34,7 +34,7 @@ - [モナド型クラス](./monads/class.md) - [例：モナドにおける算術](./monads/arithmetic.md) - [モナドのための `do` 記法](./monads/do.md) - - [The `IO` Monad](./monads/io.md) + - [`IO` モナド](./monads/io.md) - [Additional Conveniences](monads/conveniences.md) - [Summary](monads/summary.md) - [Functors, Applicative Functors, and Monads](functor-applicative-monad.md) diff --git a/functional-programming-lean/src/monads/io.md b/functional-programming-lean/src/monads/io.md index 61030fa2..1db3f273 100644 --- a/functional-programming-lean/src/monads/io.md +++ b/functional-programming-lean/src/monads/io.md @@ -1,108 +1,209 @@ + +# IOモナド + + + +モナドとしての `IO` は2つの観点から理解することができます。これは [プログラムの実行](../hello-world/running-a-program.md) の節で説明したとおりです。それぞれの観点から、`IO` における `pure` と `bind` の意味の理解が促進されます。 + + +最初の観点では、`IO` アクションはLeanのランタイムシステム（RTS）に対する命令として捉えられていました。その命令は、例えば「このファイル記述子から文字列を読み込み、その文字列で純粋なLeanコードを再度呼んでください」などのようなものです。この観点は **外部的な** もので、オペレーティングシステム側からプログラムを見ています。この場合、`pure` は `IO` アクションであり、RTSにいかなる作用も要求しません。また、`bind` はRTSに対して、まず潜在的に作用を持つ操作を実行し、その結果得られた値で残りのプログラムを呼び出すように指示します。 + +2つ目の観点では、`IO` アクションは世界全体を変換すると考えられます。`IO` アクション自体は純粋です。というのもこれは一意な世界を引数として受け取り、変更後の世界を返すからです。この観点は **内部的な** もので、Leanの内部での `IO` の表現方法に一致します。Leanにおいて世界はトークンとして表現され、`IO` モナドは各トークンが正確に一度だけ利用されるように構造化されています。 + + + +これがどのように動作するかを知るためには、定義を1つずつはがしていくことが有用です。`#print` コマンドはLeanのデータ型と定義の内部を明らかにします。例えば、 + ```lean {{#example_in Examples/Monads/IO.lean printNat}} ``` + + +は以下の結果となります。 + ```output info {{#example_out Examples/Monads/IO.lean printNat}} ``` + + +また、 + ```lean {{#example_in Examples/Monads/IO.lean printCharIsAlpha}} ``` + + +は以下の結果となります。 + ```output info {{#example_out Examples/Monads/IO.lean printCharIsAlpha}} ``` + + +`#print` の出力にはこの本でまだ紹介されていないLeanの特徴が含まれることが時折あります。例えば、 + ```lean {{#example_in Examples/Monads/IO.lean printListIsEmpty}} ``` + + +は以下を出力します。 + ```output info {{#example_out Examples/Monads/IO.lean printListIsEmpty}} ``` + + +ここで、上記の定義名の後ろに `.{u}` が含まれ、また型に対してただの `Type` ではなく `Type u` と注釈されています。これについては今のところ無視して問題ありません。 + + +`IO` の定義を表示すると、思ったより単純な構造で定義されていることがわかります： + ```lean {{#example_in Examples/Monads/IO.lean printIO}} ``` ```output info {{#example_out Examples/Monads/IO.lean printIO}} ``` + + +`IO.Error` は `IO` アクションが投げる可能性のあるすべてのエラーを表します： + ```lean {{#example_in Examples/Monads/IO.lean printIOError}} ``` ```output info {{#example_out Examples/Monads/IO.lean printIOError}} ``` + + +`EIO ε α` は、`ε` 型のエラーで終了するか、`α` 型の値で成功するかのどちらかになる `IO` アクションを表します。つまり、`Except ε` と同じように `IO` モナドにもエラー処理と例外を定義することができます。 + + +さらに展開をはがすと、`EIO` もまたとてもシンプルな構造で定義されています： + ```lean {{#example_in Examples/Monads/IO.lean printEIO}} ``` ```output info {{#example_out Examples/Monads/IO.lean printEIO}} ``` + + +`EStateM` モナドはエラーと状態の両方を保持しています。つまり `Except` と `State` を組み合わせたものです。このモナドは `EStateM.Result` という別の型を使って定義されています： + ```lean {{#example_in Examples/Monads/IO.lean printEStateM}} ``` ```output info {{#example_out Examples/Monads/IO.lean printEStateM}} ``` + + +言い換えると、`EStateM ε σ α` 型を持つプログラムは初期状態として `σ` を受け取り、戻り値として `EStateM.Result ε σ α` を返す関数です。 + + +`EStateM.Result` の定義は `Except` とよく似ており、正常終了とエラーそれぞれに対して1つずつコンストラクタがあります： + ```lean {{#example_in Examples/Monads/IO.lean printEStateMResult}} ``` ```output info {{#example_out Examples/Monads/IO.lean printEStateMResult}} ``` + +`Except ε α` と同様に、`ok` コンストラクタには `α` 型の結果が、`error` コンストラクタには `ε` 型の例外が含まれます。`Except` とは異なり、どちらのコンストラクタにも計算の最終状態を示す状態のフィールドが追加されています。 + + + +`EStateM ε σ` の `Monad` インスタンスを定義するには `pure` と `bind` が必要です。`State` と同様に、`EStateM` の `pure` の実装は初期状態を受け取り、それを変更せずに返却します。これも `Except` と同様に、`ok` コンストラクタに引数を入れて返却します： + ```lean {{#example_in Examples/Monads/IO.lean printEStateMpure}} ``` ```output info {{#example_out Examples/Monads/IO.lean printEStateMpure}} ``` + +`protected` は `EStateM` 名前空間がオープンされていても、呼び出す際には `EStateM.pure` とフルネームを使う必要があることを意味します。 + + + +同様に、`EStateM` の `bind` は初期状態を引数に取ります。この初期状態は最初のアクションに渡されます。そして `Except` の `bind` と同様に、結果がエラーかどうかのチェックを行います。もしエラーであれば、そのエラーがそのまま返却され、`bind` の第2引数は未使用のままとなります。結果が成功だった場合は、2番目の引数は戻り値と結果の状態の両方に適用されます。 + ```lean {{#example_in Examples/Monads/IO.lean printEStateMbind}} ``` @@ -110,15 +211,24 @@ If the result was a success, then the second argument is applied to both the ret {{#example_out Examples/Monads/IO.lean printEStateMbind}} ``` + + +これらをすべてまとめると、`IO` は状態とエラーを同時に追跡するモナドということになります。利用可能なエラーのあつまりは、`IO.Error` というデータ型によって与えられ、これはプログラム中に起こりうる様々なエラーを記述するコンストラクタを持ちます。状態は `IO.RealWorld` という実世界を表すデータ型です。それぞれの基本的な `IO` アクションはこの実世界を受け取り、エラーまたは結果と対になった別の実世界を返します。`IO` では、`pure` は世界を変更せずに返しますが、`bind` はアクションから次のアクションに変更された世界を渡します。 + + +全宇宙はコンピュータのメモリに収まらないため、アクション間で取りまわされる世界は単なる表現にすぎません。世界のトークンが再利用されない限り、表現は安全です。このことは、世界のトークンはデータを一切含む必要がないことを意味します： + ```lean {{#example_in Examples/Monads/IO.lean printRealWorld}} ```