Monad_Zoos翻訳 (#41)

* 翻訳開始

* Combined翻訳完了

* Except翻訳完了

* Id翻訳完了

* Option翻訳完了

* State翻訳完了

Author: s-taiga

GLOSSARY.md

@@ -193,6 +193,7 @@
 | parse | パース | |
 | parser | パーサ | |
 | pattern matching | パターンマッチ | |
+| phantom type | 幽霊型 | |
 | polymorphic | 多相 | |
 | precedence | 優先順位 | 構文解析・演算子等の優先具合を指す |
 | predicate | 述語 | |

Manual/Monads/Zoo/Combined.lean

@@ -19,18 +19,26 @@ set_option pp.rawOnError true
 
 set_option linter.unusedVariables false
 
+/-
 #doc (Manual) "Combined Error and State Monads" =>
+-/
+#doc (Manual) "エラーと状態モナドの結合（Combined Error and State Monads）" =>
 
 ```lean (show := false)
 variable (ε : Type u) (σ σ' : Type u) (α : Type u)
 ```
 
+:::comment
 The {name}`EStateM` monad has both exceptions and mutable state.
 {lean}`EStateM ε σ α` is logically equivalent to {lean}`ExceptT ε (StateM σ) α`.
 While {lean}`ExceptT ε (StateM σ)` evaluates to the type {lean}`σ → Except ε α × σ`, the type {lean}`EStateM ε σ α` evaluates to {lean}`σ → EStateM.Result ε σ α`.
 {name}`EStateM.Result` is an inductive type that's very similar to {name}`Except`, except both constructors have an additional field for the state.
 In compiled code, this representation removes one level of indirection from each monadic bind.
 
+:::
+
+{name}`EStateM` モナドは例外と可変状態の両方を持ちます。 {lean}`EStateM ε σ α` は {lean}`ExceptT ε (StateM σ) α` と論理的に等価です。 {lean}`ExceptT ε (StateM σ)` が {lean}`σ → Except ε α × σ` 型に評価されるのに対して、 {lean}`EStateM ε σ α` は {lean}`σ → EStateM.Result ε σ α` 型に評価されます。 {name}`EStateM.Result` は {name}`Except` とよく似た帰納型ですが、どちらのコンストラクタにも状態を表すフィールドが追加されています。コンパイルされたコードでは、この表現は各モナドの bind から1段階インダイレクションを取り除きます。
+
 ```lean (show := false)
 /-- info: σ → Except ε α × σ -/
 #guard_msgs in
@@ -53,28 +61,58 @@ In compiled code, this representation removes one level of indirection from each
 
 {docstring EStateM.fromStateM}
 
+:::comment
 # State Rollback
+:::
 
+# 状態のロールバック（State Rollback）
+
+
+:::comment
 Composing {name}`StateT` and {name}`ExceptT` in different orders causes exceptions to interact differently with state.
 In one ordering, state changes are rolled back when exceptions are caught; in the other, they persist.
 The latter option matches the semantics of most imperative programming languages, but the former is very useful for search-based problems.
 Often, some but not all state should be rolled back; this can be achieved by “sandwiching” {name}`ExceptT` between two separate uses of {name}`StateT`.
 
-To avoid yet another layer of indirection via the use of {lean}`StateT σ (EStateM ε σ') α`, {name}`EStateM` offers the {name}`EStateM.Backtrackable` {tech}[型クラス]type class.
+:::
+
+{name}`StateT` と {name}`ExceptT` を異なる順序で合成すると例外と状態の相互作用は異なるものになります。片方の順序では、例外が捕捉された時に状態の変更がロールバックされ、もう一方では状態が持続します。後者のオプションはほとんどの命令型プログラミング言語のセマンティックスに一致しますが、前者は検索ベースの問題に対して非常に便利です。またしばしば、すべてではなく一部の状態だけがロールバックされるべき場合もあります；これは {name}`ExceptT` を2つの {name}`StateT` で「サンドイッチ」することで実現できます。
+
+:::comment
+To avoid yet another layer of indirection via the use of {lean}`StateT σ (EStateM ε σ') α`, {name}`EStateM` offers the {name}`EStateM.Backtrackable` {tech}[type class].
 This class specifies some part of the state that can be saved and restored.
 {name}`EStateM` then arranges for the saving and restoring to take place around error handling.
 
+:::
+
+{lean}`StateT σ (EStateM ε σ') α` の使用によるさらに別のレイヤーからのインダイレクトを避けるために、 {name}`EStateM` は {name}`EStateM.Backtrackable` {tech}[型クラス] を提供します。このクラスは保存と復元が可能な状態の一部を指定します。 {name}`EStateM` はエラー処理を中心に保存と復元が行われるよう調整します。
+
 {docstring EStateM.Backtrackable}
 
+:::comment
 There is a universally-applicable instance of {name EStateM.Backtrackable}`Backtrackable` that neither saves nor restores anything.
 Because instance synthesis chooses the most recent instance first, the universal instance is used only if no other instance has been defined.
 
+:::
+
+{name EStateM.Backtrackable}`Backtrackable` には普遍的に適用可能なインスタンスがありますが、これは何も保存も復元もしません。インスタンス統合は最新のインスタンスを最初に選択するため、他のインスタンスが定義されていない場合にのみこの普遍的なインスタンスが使用されます。
+
 {docstring EStateM.nonBacktrackable}
 
+:::comment
 # Implementations
+:::
 
+# 実装（Implementations）
+
+
+:::comment
 These functions are typically not called directly, but rather are accessed through their corresponding type classes.
 
+:::
+
+これらの関数は通常、直接呼び出されることはなく、対応する型クラスを通じてアクセスされます。
+
 {docstring EStateM.map}
 
 {docstring EStateM.pure}

Manual/Monads/Zoo/Except.lean

@@ -19,17 +19,30 @@ set_option pp.rawOnError true
 
 set_option linter.unusedVariables false
 
+/-
 #doc (Manual) "Exceptions" =>
+-/
+#doc (Manual) "例外（Exceptions）" =>
 %%%
 tag := "exception-monads"
 %%%
 
+:::comment
 Exception monads describe computations that terminate early (fail).
 Failing computations provide their caller with an _exception_ value that describes _why_ they failed.
 In other words, computations either return a value or an exception.
 The inductive type {name}`Except` captures this pattern, and is itself a monad.
 
+:::
+
+例外モナドは早期に終了（失敗）する計算を記述します。失敗した計算は、 _なぜ_ 失敗したかを示す _例外_ 値を呼び出し元に提供します。言い換えると、計算は値か例外を返します。帰納型 {name}`Except` はこのパターンを捕捉しており、それ自体がモナドです。
+
+:::comment
 # Exceptions
+:::
+
+# 例外（Exceptions）
+
 
 {docstring Except}
 
@@ -52,7 +65,12 @@ The inductive type {name}`Except` captures this pattern, and is itself a monad.
 {docstring Except.toBool}
 
 
+:::comment
 # Type Class
+:::
+
+# 型クラス（Type Class）
+
 
 {docstring MonadExcept}
 
@@ -68,11 +86,21 @@ The inductive type {name}`Except` captures this pattern, and is itself a monad.
 
 {docstring tryCatchThe}
 
+:::comment
 # “Finally” Computations
+:::
+
+# 「finally」の計算（“Finally” Computations）
+
 
 {docstring MonadFinally}
 
+:::comment
 # Transformer
+:::
+
+# 変換子（Transformer）
+
 
 {docstring ExceptT}
 
@@ -95,7 +123,12 @@ The inductive type {name}`Except` captures this pattern, and is itself a monad.
 {docstring ExceptT.adapt}
 
 
+:::comment
 # Exception Monads in Continuation Passing Style
+:::
+
+# 継続渡しスタイルの例外モナド（Exception Monads in Continuation Passing Style）
+
 
 ```lean (show := false)
 universe u
@@ -104,12 +137,17 @@ variable (ε : Type u)
 variable {m : Type u → Type v}
 ```
 
+:::comment
 Continuation-passing-style exception monads represent potentially-failing computations as functions that take success and failure continuations, both of which return the same type, returning that type.
 They must work for _any_ return type.
 An example of such a type is {lean}`(β : Type u) → (α → β) → (ε → β) → β`.
 {lean}`ExceptCpsT` is a transformer that can be applied to any monad, so {lean}`ExceptCpsT ε m α` is actually defined as {lean}`(β : Type u) → (α → m β) → (ε → m β) → m β`.
 Exception monads in continuation passing style have different performance characteristics than {name}`Except`-based state monads; for some applications, it may be worth benchmarking them.
 
+:::
+
+継続渡しスタイルの例外モナドは、失敗する可能性のある計算を、成功と失敗を取る関数として表します。この継続はどちらも同じ型を返し、この関数はその型を返します。例外モナドは _どのような_ 戻り値の型でも動作しなければなりません。このような型の例は {lean}`(β : Type u) → (α → β) → (ε → β) → β` です。 {lean}`ExceptCpsT` は任意のモナドに適用できる変換子であるため、 {lean}`ExceptCpsT ε m α` は実際には {lean}`(β : Type u) → (α → m β) → (ε → m β) → m β` と定義されています。継続渡しスタイルの例外モナドは、 {name}`Except` ベースの状態モナドとは異なるパフォーマンス特性を持ちます；アプリケーションによってはベンチマークを取る価値があるかもしれません。
+
 ```lean (show := false)
 /-- info: (β : Type u) → (α → m β) → (ε → m β) → m β -/
 #guard_msgs in

Manual/Monads/Zoo/Id.lean

@@ -19,14 +19,24 @@ set_option pp.rawOnError true
 
 set_option linter.unusedVariables false
 
+/-
 #doc (Manual) "Identity" =>
+-/
+#doc (Manual) "恒等モナド（Identity）" =>
 
+:::comment
 The identity monad {name}`Id` has no effects whatsoever.
 Both {name}`Id` and the corresponding implementation of {name}`pure` are the identity function, and {name}`bind` is reversed function application.
 The identity monad has two primary use cases:
  1. It can be the type of a {keywordOf Lean.Parser.Term.do}`do` block that implements a pure function with local effects.
  2. It can be placed at the bottom of a stack of monad transformers.
 
+:::
+
+恒等モナド {name}`Id` は何の作用も持ちません。 {name}`Id` と対応する {name}`pure` の実装はどちらも恒等関数であり、 {name}`bind` は関数適用を逆転させたものです。恒等モナドには主に2つの使用例があります：
+ 1. {keywordOf Lean.Parser.Term.do}`do` ブロックの型にして、局所的に作用を持つ純粋関数を実装することができます。
+ 2. モナド変換子のスタックの一番下に置くことができます。
+
 ```lean (show := false)
 -- Verify claims
 example : Id = id := rfl
@@ -39,8 +49,16 @@ example : (bind (m := Id)) = (fun (x : α) (f : α → Id β) => f x) := rfl
 
 {docstring Id.run}
 
-:::example "Local Effects with the Identity Monad"
+:::comment
+::example "Local Effects with the Identity Monad"
+:::
+::::example "恒等モナドによる局所的な作用"
+:::comment
 This code block implements a countdown procedure by using simulated local mutability in the identity monad.
+:::
+
+このコードブロックは恒等モナドのシミュレートされた局所的な可変性を使ってカウントダウン処理を実装しています。
+
 ```lean (name := idDo)
 #eval Id.run do
   let mut xs := []
@@ -51,6 +69,6 @@ This code block implements a countdown procedure by using simulated local mutabi
 ```leanOutput idDo
 [9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
 ```
-:::
+::::
 
 {docstring Id.hasBind}

Manual/Monads/Zoo/Option.lean

@@ -19,16 +19,24 @@ set_option pp.rawOnError true
 
 set_option linter.unusedVariables false
 
+/-
 #doc (Manual) "Option" =>
+-/
+#doc (Manual) "オプション（Option）" =>
 %%%
 tag := "option-monad"
 %%%
 
+:::comment
 Ordinarily, {lean}`Option` is thought of as data, similarly to a nullable type.
 It can also be considered as a monad, and thus a way of performing computations.
 The {lean}`Option` monad and its transformer {lean}`OptionT` can be understood as describing computations that may terminate early, discarding the results.
 Callers can check for early termination and invoke a fallback if desired using {name}`OrElse.orElse` or by treating it as a {lean}`MonadExcept Unit`.
 
+:::
+
+通常、 {lean}`Option` は nullable 型と同じようなデータとして考えられます。また、モナド、つまり計算を実行する方法として考えることもできます。 {lean}`Option` モナドとその変換子 {lean}`OptionT` は、結果を破棄して早期に終了する可能性のある計算を記述するものとして理解することができます。呼び出し元は {name}`OrElse.orElse` を使用するか、 {lean}`MonadExcept Unit` として扱うことで早期終了をチェックし、必要に応じてフォールバックを呼び出すことができます。
+
 {docstring OptionT}
 
 {docstring OptionT.run}

Manual/Monads/Zoo/Reader.lean

@@ -19,7 +19,10 @@ set_option pp.rawOnError true
 
 set_option linter.unusedVariables false
 
+/-
 #doc (Manual) "Reader" =>
+-/
+#doc (Manual) "リーダ（Reader）" =>
 %%%
 tag := "reader-monad"
 %%%