From 72486a544964d5c6e668a3169a7ac3f34ac42035 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Sat, 24 Aug 2024 16:32:34 +0900 Subject: [PATCH] =?UTF-8?q?=E3=82=BB=E3=83=AB=E3=83=95=E3=83=AC=E3=83=93?= =?UTF-8?q?=E3=83=A5=E3=83=BC?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- functional-programming-lean/src/SUMMARY.md | 2 +- .../src/monads/class.md | 48 +++++++++---------- 2 files changed, 25 insertions(+), 25 deletions(-) diff --git a/functional-programming-lean/src/SUMMARY.md b/functional-programming-lean/src/SUMMARY.md index be2e2052..864ab0f6 100644 --- a/functional-programming-lean/src/SUMMARY.md +++ b/functional-programming-lean/src/SUMMARY.md @@ -31,7 +31,7 @@ - [その他の便利な機能](type-classes/conveniences.md) - [まとめ](type-classes/summary.md) - [モナド](./monads.md) - - [The Monad Type Class](./monads/class.md) + - [モナド型クラス](./monads/class.md) - [Example: Arithmetic in Monads](./monads/arithmetic.md) - [`do`-Notation for Monads](./monads/do.md) - [The `IO` Monad](./monads/io.md) diff --git a/functional-programming-lean/src/monads/class.md b/functional-programming-lean/src/monads/class.md index c8b1d074..2b46f8d0 100644 --- a/functional-programming-lean/src/monads/class.md +++ b/functional-programming-lean/src/monads/class.md @@ -9,7 +9,7 @@ Rather than having to import an operator like `ok` or `andThen` for each type th Monads have two operations, which are the equivalent of `ok` and `andThen`: --> -モナドの型ごとに `ok` や `andThen` のような演算子を導入する代わりに，Lean標準ライブラリにはそれらをオーバーロードできる型クラスがあるため，同じ演算子を **任意の** モナドに使うことができます．モナドには `ok` と `andThen` に相当する2つの演算があります： +モナドの型ごとに `ok` や `andThen` のような演算子を導入する代わりに、Lean標準ライブラリにはそれらをオーバーロードできる型クラスがあるため、同じ演算子を **任意の** モナドに使うことができます。モナドには `ok` と `andThen` に相当する2つの演算があります： ```lean {{#example_decl Examples/Monads/Class.lean FakeMonad}} @@ -19,13 +19,13 @@ This definition is slightly simplified. The actual definition in the Lean library is somewhat more involved, and will be presented later. --> -この定義は実態より若干簡略化されています．Leanのライブラリにおける実際の定義はもう少し複雑ですが，それは後程紹介しましょう． +この定義は実態より若干簡略化されています。Leanのライブラリにおける実際の定義はもう少し複雑ですが、それは後程紹介しましょう。 -`Option` と `Except` の `Monad` インスタンスは，それぞれの `andThen` 演算を適合させることで作成できます： +`Option` と `Except` の `Monad` インスタンスは、それぞれの `andThen` 演算を適合させることで作成できます： ```lean {{#example_decl Examples/Monads/Class.lean MonadOptionExcept}} @@ -38,7 +38,7 @@ It does, however, require a lookup function as an argument, because different mo The infix version of `bind` is `>>=`, which plays the same role as `~~>` in the examples. --> -例として出した `firstThirdFifthSeventh` は `Option α` と `Except String α` の戻り値型に対して個別に定義されていました．しかし今やこの関数を **任意の** モナドに多相的に定義することができます．ただし，別のモナドによる異なる実装では結果を見つけることができないかもしれないため，引数としてルックアップ関数が必要です．例で出した `~~>` と同じ役割を果たしていた `bind` の中置バージョンは `>>=` です． +例として出した `firstThirdFifthSeventh` は `Option α` と `Except String α` の戻り値型に対して個別に定義されていました。しかし今やこの関数を **任意の** モナドに多相的に定義することができます。ただし、別のモナドによる異なる実装では結果を見つけることができないかもしれないため、引数としてルックアップ関数が必要です。例で出した `~~>` と同じ役割を果たしていた `bind` の中置バージョンは `>>=` です。 ```lean {{#example_decl Examples/Monads/Class.lean firstThirdFifthSeventhMonad}} @@ -48,7 +48,7 @@ The infix version of `bind` is `>>=`, which plays the same role as `~~>` in the Given example lists of slow mammals and fast birds, this implementation of `firstThirdFifthSeventh` can be used with `Option`: --> -この `firstThirdFifthSeventh` の実装は，のろい哺乳類と速い鳥の名前のリストを例として `Option` について利用することが可能です： +この `firstThirdFifthSeventh` の実装は、のろい哺乳類と速い鳥の名前のリストを例として `Option` について利用することが可能です： ```lean {{#example_decl Examples/Monads/Class.lean animals}} @@ -69,7 +69,7 @@ Given example lists of slow mammals and fast birds, this implementation of `firs After renaming `Except`'s lookup function `get` to something more specific, the very same implementation of `firstThirdFifthSeventh` can be used with `Except` as well: --> -`Except` のルックアップ関数 `get` をもう少し実態に即したものに名称変更することで，先ほどと全く同じ `firstThirdFifthSeventh` の実装を `Except` についても使うことができます： +`Except` のルックアップ関数 `get` をもう少し実態に即したものに名称変更することで、先ほどと全く同じ `firstThirdFifthSeventh` の実装を `Except` についても使うことができます： ```lean {{#example_decl Examples/Monads/Class.lean getOrExcept}} @@ -89,7 +89,7 @@ After renaming `Except`'s lookup function `get` to something more specific, the The fact that `m` must have a `Monad` instance means that the `>>=` and `pure` operations are available. --> -`m` が `Monad` インスタンスを持っていなければならないということは，`>>=` と `pure` 演算が利用できるということを意味します． +`m` が `Monad` インスタンスを持っていなければならないということは、`>>=` と `pure` 演算が利用できるということを意味します。 -実に多くの型がモナドであるため，**任意の** モナドに対して多相性を持つ関数は非常に強力です．例えば，関数 `mapM` はモナド用の `map` で，`Monad` を使って関数を適用した結果を順番に並べたり組み合わせたりします： +実に多くの型がモナドであるため、**任意の** モナドに対して多相性を持つ関数は非常に強力です。例えば、関数 `mapM` はモナド用の `map` で、`Monad` を使って関数を適用した結果を順番に並べたり組み合わせたりします： ```lean {{#example_decl Examples/Monads/Class.lean mapM}} @@ -113,7 +113,7 @@ In other words, `mapM` can be used for functions that produce logs, for function Because `f`'s type determines the available effects, they can be tightly controlled by API designers. --> -関数 `f` の戻り値の型によって，どの `Monad` インスタンスを使うかが決まります．つまり，`mapM` はログを生成する関数や失敗する可能性のある関数，可変状態を使用する関数などのどれにでも使用することができるのです．`f` の型が利用可能な作用を決定するため，API設計者はその作用を厳密に制御することができます． +関数 `f` の戻り値の型によって、どの `Monad` インスタンスを使うかが決まります。つまり、`mapM` はログを生成する関数や失敗する可能性のある関数、可変状態を使用する関数などのどれにでも使用することができるのです。`f` の型が利用可能な作用を決定するため、API設計者はその作用を厳密に制御することができます。 -[本章の導入](../monads.md#numbering-tree-nodes) で説明したように，`State σ α` という型は `σ` 型の可変変数を使用し，`α` 型の値を返すプログラムを表します．これらのプログラムは，実際には初期状態から値と最終状態のペアへの関数です．`Monad` クラスは引数がただの型であることを求めます．つまり，`Monad` となる型は `Type → Type` であることを要求されます．したがって `State` のインスタンスは状態の型 `σ` を指定しておく必要があり，これがインスタンスのパラメータになることを意味します： +[本章の導入](../monads.md#numbering-tree-nodes) で説明したように、`State σ α` という型は `σ` 型の可変変数を使用し、`α` 型の値を返すプログラムを表します。これらのプログラムは、実際には初期状態から値と最終状態のペアへの関数です。`Monad` クラスは引数がただの型であることを求めます。つまり、`Monad` となる型は `Type → Type` であることを要求されます。したがって `State` のインスタンスは状態の型 `σ` を指定しておく必要があり、これがインスタンスのパラメータになることを意味します： ```lean {{#example_decl Examples/Monads/Class.lean StateMonad}} @@ -132,7 +132,7 @@ This means that the type of the state cannot change between calls to `get` and ` The operator `increment` increases a saved state by a given amount, returning the old value: --> -これは `bind` を使って `get` と `set` を連続して呼び出している間において状態の型を変更できないことを意味し，ステートフルな計算の規則として理にかなっています．`increment` 演算子は保存された状態を指定された量だけ増価させ，古い値を返します： +これは `bind` を使って `get` と `set` を連続して呼び出している間において状態の型を変更できないことを意味し、ステートフルな計算の規則として理にかなっています。`increment` 演算子は保存された状態を指定された量だけ増価させ、古い値を返します： ```lean {{#example_decl Examples/Monads/Class.lean increment}} @@ -145,7 +145,7 @@ In other words, `{{#example_in Examples/Monads/Class.lean mapMincrement}}` has t It takes an initial sum as an argument, which should be `0`: --> -`mapM` を `increment` と一緒に使うと，リスト内の要素の合計を計算するプログラムになります．より具体的には，可変変数には最終的な合計が格納され，戻り値のリストには実行中の各合計が格納されます．言い換えると，`{{#example_in Examples/Monads/Class.lean mapMincrement}}` は `{{#example_out Examples/Monads/Class.lean mapMincrement}}` 型を持ち，`State` の定義を展開すると `{{#example_out Examples/Monads/Class.lean mapMincrement2}}` が得られます．これらは引数として合計の初期値を引数に取り，これは `0` でなければなりません： +`mapM` を `increment` と一緒に使うと、リスト内の要素の合計を計算するプログラムになります。より具体的には、可変変数には最終的な合計が格納され、戻り値のリストには実行中の各合計が格納されます。言い換えると、`{{#example_in Examples/Monads/Class.lean mapMincrement}}` は `{{#example_out Examples/Monads/Class.lean mapMincrement}}` 型を持ち、`State` の定義を展開すると `{{#example_out Examples/Monads/Class.lean mapMincrement2}}` が得られます。これらは引数として合計の初期値を引数に取り、これは `0` でなければなりません： ```lean {{#example_in Examples/Monads/Class.lean mapMincrementOut}} @@ -159,7 +159,7 @@ A [logging effect](../monads.md#logging) can be represented using `WithLog`. Just like `State`, its `Monad` instance is polymorphic with respect to the type of the logged data: --> -[ロギングの作用](../monads.md#logging) は`WithLog` を使って表現することができました．`State` と同様に，その `Monad` インスタンスはログに記録されているデータの型に対して多相的です： +[ロギングの作用](../monads.md#logging) は`WithLog` を使って表現することができました。`State` と同様に、その `Monad` インスタンスはログに記録されているデータの型に対して多相的です： ```lean {{#example_decl Examples/Monads/Class.lean MonadWriter}} @@ -168,7 +168,7 @@ Just like `State`, its `Monad` instance is polymorphic with respect to the type `saveIfEven` is a function that logs even numbers but returns its argument unchanged: --> -`saveIfEven` は偶数についてログを出力して，引数について何もせずに返却する関数です： +`saveIfEven` は偶数についてログを出力して、引数について何もせずに返却する関数です： ```lean {{#example_decl Examples/Monads/Class.lean saveIfEven}} @@ -177,7 +177,7 @@ Just like `State`, its `Monad` instance is polymorphic with respect to the type Using this function with `mapM` results in a log containing even numbers paired with an unchanged input list: --> -この関数を `mapM` と一緒に使うと，偶数についてのログと変更されていないリストがペアになった結果が得られます： +この関数を `mapM` と一緒に使うと、偶数についてのログと変更されていないリストがペアになった結果が得られます： ```lean {{#example_in Examples/Monads/Class.lean mapMsaveIfEven}} @@ -200,7 +200,7 @@ Sometimes, however, an API will be written to use a monad for flexibility, but t The _identity monad_ is a monad that has no effects, and allows pure code to be used with monadic APIs: --> -モナドは失敗，例外，ロギングなどの作用を持つプログラムをデータや関数として明示的に表現します．しかし，柔軟性のためにモナドを使用するように設計されたAPIに対して，時にはエンコードされた作用を必要としない利用者もいます．**恒等モナド** （identity monad）は作用を持たないモナドであり，純粋なコードをモナドAPIで使用することを可能にします： +モナドは失敗、例外、ロギングなどの作用を持つプログラムをデータや関数として明示的に表現します。しかし、柔軟性のためにモナドを使用するように設計されたAPIに対して、時にはエンコードされた作用を必要としない利用者もいます。**恒等モナド** （identity monad）は作用を持たないモナドであり、純粋なコードをモナドAPIで使用することを可能にします： ```lean {{#example_decl Examples/Monads/Class.lean IdMonad}} @@ -211,14 +211,14 @@ Similarly, the type of `bind` should be `α → (α → Id β) → Id β`. Because this reduces to `α → (α → β) → β`, the second argument can be applied to the first to find the result. --> -`pure` の型は `α → Id α` であるべきですが，`Id α` はただの `α` に簡約されます．同様に，`bind` の型は `α → (α → Id β) → Id β` であるべきです．これは `α → (α → β) → β` に簡約されるため，2番目の引数を1番目の引数に適用して結果を求めることができます． +`pure` の型は `α → Id α` であるべきですが、`Id α` はただの `α` に簡約されます。同様に、`bind` の型は `α → (α → Id β) → Id β` であるべきです。これは `α → (α → β) → β` に簡約されるため、2番目の引数を1番目の引数に適用して結果を求めることができます。 -恒等関手を使うことで，`mapM` は `map` と同じものになります．ただし，このように呼ぶにあたって，Leanは意図したモナドが `Id` であることのヒントを要求します： +恒等関手を使うことで、`mapM` は `map` と同じものになります。ただし、このように呼ぶにあたって、Leanは意図したモナドが `Id` であることのヒントを要求します： ```lean {{#example_in Examples/Monads/Class.lean mapMId}} @@ -244,7 +244,7 @@ The return type of the function is expected to be the monad applied to some othe Similarly, using `mapM` with a function whose type doesn't provide any specific hints about which monad is to be used results in an "instance problem stuck" message: --> -このエラーでは，あるメタ変数を別の変数に適用することで，Leanが型レベルの計算を逆方向に実行していないことを示しています．この関数の戻り値の型は，ほかの型に適用されたモナドであることが期待されます．同様に，型がどのモナドを使用するかについての具体的なヒントを提供しない関数で `mapM` を使用すると，「インスタンス問題のスタック」というメッセージが表示されます： +このエラーでは、あるメタ変数を別の変数に適用することで、Leanが型レベルの計算を逆方向に実行していないことを示しています。この関数の戻り値の型は、ほかの型に適用されたモナドであることが期待されます。同様に、型がどのモナドを使用するかについての具体的なヒントを提供しない関数で `mapM` を使用すると、「インスタンス問題のスタック」というメッセージが表示されます： ```lean {{#example_in Examples/Monads/Class.lean mapMIdId}} @@ -268,7 +268,7 @@ Secondly, `pure` should be a right identity of `bind`, so `bind v pure` is the s Finally, `bind` should be associative, so `bind (bind v f) g` is the same as `bind v (fun x => bind (f x) g)`. --> -`Beq` と `Hashable` のインスタンスのすべてのペアが等しい2つの値が同じハッシュ値を持つことを保証しなければならないように，`Monad` のインスタンスにも従うべき約定が存在します．まず，`pure` は `bind` の左単位でなければなりません．つまり，`bind (pure v) f` は `f v` と同じでなければなりません．次に，`pure` は `bind` の右単位でもあるべきで，`bind v pure` は `v` と同じとなります．最後に，`bind` は結合的であるべきで，`bind (bind v f) g` は `bind v (fun x => bind (f x) g)` と同じです． +`Beq` と `Hashable` のインスタンスのすべてのペアが等しい2つの値が同じハッシュ値を持つことを保証しなければならないように、`Monad` のインスタンスにも従うべき約定が存在します。まず、`pure` は `bind` の左単位でなければなりません。つまり、`bind (pure v) f` は `f v` と同じでなければなりません。次に、`pure` は `bind` の右単位でもあるべきで、`bind v pure` は `v` と同じとなります。最後に、`bind` は結合的であるべきで、`bind (bind v f) g` は `bind v (fun x => bind (f x) g)` と同じです。 -この約定はより一般的に作用を持つプログラムに期待される特性を規定しています．`pure` は作用を持たないため，`bind` で作用を続けても結果は変わらないはずです．`bind` の結合性は，基本的に物事が起こっている順序が保たれていれば，処理の実行順番自体はどう行っても問題ないことを言っています． +この約定はより一般的に作用を持つプログラムに期待される特性を規定しています。`pure` は作用を持たないため、`bind` で作用を続けても結果は変わらないはずです。`bind` の結合性は、基本的に物事が起こっている順序が保たれていれば、処理の実行順番自体はどう行っても問題ないことを言っています。 -関数 `BinTree.mapM` を定義してください．リストの `mapM` と同様に，この関数は木の各データ要素に行きがけ順でモナド関数を適用する必要があります．型シグネチャは以下のようになります： +関数 `BinTree.mapM` を定義してください。リストの `mapM` と同様に、この関数は木の各データ要素に行きがけ順でモナド関数を適用する必要があります。型シグネチャは以下のようになります： ``` def BinTree.mapM [Monad m] (f : α → m β) : BinTree α → m (BinTree β) @@ -314,7 +314,7 @@ First, write a convincing argument that the `Monad` instance for `Option` satisf Then, consider the following instance: --> -まず `Option` の `Monad` インスタンスがモナドの約定を満たすことへの根拠を書き出してください．次に，以下のインスタンスを考えてみましょう： +まず `Option` の `Monad` インスタンスがモナドの約定を満たすことへの根拠を書き出してください。次に、以下のインスタンスを考えてみましょう： ```lean {{#example_decl Examples/Monads/Class.lean badOptionMonad}} @@ -324,5 +324,5 @@ Both methods have the correct type. Why does this instance violate the monad contract? --> -どちらのメソッドも正しい型です．ではなぜこのインスタンスはモナドの約定を破っているのでしょうか？ +どちらのメソッドも正しい型です。ではなぜこのインスタンスはモナドの約定を破っているのでしょうか？