Monad_Zoo翻訳 (#40)

* 翻訳開始

* 翻訳完了

* 用語対応

Author: s-taiga

Manual/IO.lean

@@ -93,7 +93,7 @@ Error handling is accomplished by layering an appropriate exception monad transf
 
 :::
 
-{lean}`IO α` 型は副作用を実行することによって {lean}`α` 型の値を返すか、エラーを投げるべきプロセスについての記述です。これは世界全体を状態とする {tech}[state monad] として考えることができます。 {lean}`StateM Nat Bool` 型の値が自然数をミューテーションさせる能力を持ちながら {lean}`Bool` を計算することと同じように、 {lean}`IO Bool` 型の値は世界を変化させる可能性を有しながら {lean}`Bool` を計算します。エラー処理は、適切な例外モナド変換子をこの上に重ねることで達成されます。
+{lean}`IO α` 型は副作用を実行することによって {lean}`α` 型の値を返すか、エラーを投げるべきプロセスについての記述です。これは世界全体を状態とする {tech}[状態モナド] として考えることができます。 {lean}`StateM Nat Bool` 型の値が自然数をミューテーションさせる能力を持ちながら {lean}`Bool` を計算することと同じように、 {lean}`IO Bool` 型の値は世界を変化させる可能性を有しながら {lean}`Bool` を計算します。エラー処理は、適切な例外モナド変換子をこの上に重ねることで達成されます。
 
 :::::
 
@@ -208,7 +208,7 @@ The most-used constructor is {name IO.Error.userError}`userError`, which covers
 
 :::
 
-{lean}`IO` モナドにおけるエラー処理は、他の {tech}[exception monad] と同じ機能を使用します。特に、例外のスローとキャッチは {name}`MonadExceptOf` {tech}[型クラス] のメソッドを使用します。 {lean}`IO` で投げられる例外は {lean}`IO.Error` 型を持ちます。このコンストラクタは、ファイルが存在しないなど、ほとんどのオペレーティングシステムで発生する低レベルのエラーを表します。最もよく使われるエラーは {name IO.Error.userError}`userError` で、これは他のすべてのケースをカバーし、問題を説明する文字列を含みます。
+{lean}`IO` モナドにおけるエラー処理は、他の {tech}[例外モナド] と同じ機能を使用します。特に、例外のスローとキャッチは {name}`MonadExceptOf` {tech}[型クラス] のメソッドを使用します。 {lean}`IO` で投げられる例外は {lean}`IO.Error` 型を持ちます。このコンストラクタは、ファイルが存在しないなど、ほとんどのオペレーティングシステムで発生する低レベルのエラーを表します。最もよく使われるエラーは {name IO.Error.userError}`userError` で、これは他のすべてのケースをカバーし、問題を説明する文字列を含みます。
 
 {docstring IO.Error}
 

Manual/IO/Ref.lean

@@ -32,7 +32,7 @@ Mutable references have a type {lean}`IO.Ref` that indicates that a cell is muta
 
 :::
 
-通常の {tech}[state monads] は計算の値とともに状態の内容を追跡するタプルを使用して状態のある計算をエンコードしますが、Lean のランタイムシステムは、常に可変なメモリセルにバックアップされた可変参照も提供しています。可変参照は {lean}`IO.Ref` 型を持ちます。これによってセルが可変であることが示され、読み取りと書き込みは明示的に行う必要があります。 {lean}`IO.Ref` は {lean}`ST.Ref` を使って実装されているため、 {ref "mutable-st-references"}[{lean}`ST.Ref` API] をすべて {lean}`IO.Ref` と一緒に使うことができます。
+通常の {tech}[状態モナド] は計算の値とともに状態の内容を追跡するタプルを使用して状態のある計算をエンコードしますが、Lean のランタイムシステムは、常に可変なメモリセルにバックアップされた可変参照も提供しています。可変参照は {lean}`IO.Ref` 型を持ちます。これによってセルが可変であることが示され、読み取りと書き込みは明示的に行う必要があります。 {lean}`IO.Ref` は {lean}`ST.Ref` を使って実装されているため、 {ref "mutable-st-references"}[{lean}`ST.Ref` API] をすべて {lean}`IO.Ref` と一緒に使うことができます。
 
 {docstring IO.Ref}
 

Manual/Monads/Lift.lean

@@ -180,7 +180,7 @@ There are also instances of {name}`MonadLift` for most of the standard library's
 For example, state monad actions can be lifted across reader and exception transformers, allowing compatible monads to be intermixed freely:
 :::
 
-また、標準ライブラリの {tech}[monad transformers] のほとんどに {name}`MonadLift` インスタンスがあるため、ベースとなるモナドアクションを追加作業無しに変換されたモナドで使用することができます。例えば、状態モナドアクションは、リーダと例外の変換を横断して持ち上げることができるため、互換性のあるモナドを自由に混在させることができます：
+また、標準ライブラリの {tech}[モナド変換子] のほとんどに {name}`MonadLift` インスタンスがあるため、ベースとなるモナドアクションを追加作業無しに変換されたモナドで使用することができます。例えば、状態モナドアクションは、リーダと例外の変換を横断して持ち上げることができるため、互換性のあるモナドを自由に混在させることができます：
 
 ````lean (keep := false)
 def incrBy (n : Nat) : StateM Nat Unit := modify (+ n)

Manual/Monads/Syntax.lean

@@ -692,7 +692,7 @@ These effects are implemented via transformations of the entire {keywordOf Lean.
 
 :::
 
-{keywordOf Lean.Parser.Term.do}`do` 記法は、データに依存する逐次計算のサポートに加えて、早期リターン・ローカルの可変状態・早期終了のループなど、さまざまな作用におけるローカルでの追加作用もサポートしています。これらの作用は、ローカルの脱糖ではなく、 {tech}[monad transformers] のような方法で {keywordOf Lean.Parser.Term.do}`do` ブロック全体の変換によって実装されています。
+{keywordOf Lean.Parser.Term.do}`do` 記法は、データに依存する逐次計算のサポートに加えて、早期リターン・ローカルの可変状態・早期終了のループなど、さまざまな作用におけるローカルでの追加作用もサポートしています。これらの作用は、ローカルの脱糖ではなく、 {tech}[モナド変換子] のような方法で {keywordOf Lean.Parser.Term.do}`do` ブロック全体の変換によって実装されています。
 
 :::comment
 ## Early Return
@@ -793,7 +793,7 @@ When {keywordOf Lean.Parser.Term.do}`do` blocks contain mutable bindings, the {k
 
 :::
 
-このようなローカルの可変な束縛は、そのレキシカルスコープの外では可変ではないため、 {tech}[state monad] よりも強力ではありません；この性質によって推論も簡単になります。 {keywordOf Lean.Parser.Term.do}`do` ブロックに可変な束縛が含まれている場合、 {keywordOf Lean.Parser.Term.do}`do` エラボレータは {lean}`StateT` と同じように式を変換し、新しいモナドを構築して正しい値で初期化します。
+このようなローカルの可変な束縛は、そのレキシカルスコープの外では可変ではないため、 {tech}[状態モナド] よりも強力ではありません；この性質によって推論も簡単になります。 {keywordOf Lean.Parser.Term.do}`do` ブロックに可変な束縛が含まれている場合、 {keywordOf Lean.Parser.Term.do}`do` エラボレータは {lean}`StateT` と同じように式を変換し、新しいモナドを構築して正しい値で初期化します。
 
 :::comment
 ## Control Structures