An EIO monad that cannot throw exceptions.
9.1. 論理モデル（Logical Model）
概念的に、Lean は項の評価や簡約と副作用の 実行 を区別します。項の簡約は β や δ のような規則で指定され、いつでも・どこでも発生する可能性があります。正しい順序で実行されなければならない副作用は Lean の論理で抽象的に記述されます。プログラムが実行されると、Lean のランタイムシステムは記述された作用を実際に実行する責任を負います。
IO α 型は副作用を実行することによって α 型の値を返すか、エラーを投げるべきプロセスについての記述です。これは世界全体を状態とする 状態モナド として考えることができます。 StateM Nat Bool 型の値が自然数をミューテーションさせる能力を持ちながら Bool を計算することと同じように、 IO Bool 型の値は世界を変化させる可能性を有しながら Bool を計算します。エラー処理は、適切な例外モナド変換子をこの上に重ねることで達成されます。
世界全体をメモリ上で表現することはできないため、実際の実装ではその状態を表す抽象的なトークンを使用します。Lean のランタイムシステムは、プログラムの実行時に最初のトークンを提供する責任を負い、各プリミティブのアクションは世界を表すトークンを受け入れ、終了時に別のトークンを返します。これにより作用が適切な順序で発生することが保証され、Lean の項の簡約セマンティクスから副作用の実行が明確に分離されます。
一般的な再帰による停止しない処理は、 IO で説明される作用とは別に扱われます。無限ループによって終了しない可能性のあるプログラムは partial 関数として定義する必要があります。論理的な観点からは、これらは任意の定数として扱われます； IO である必要はありません。
IO の非常に重要な特性は、値が「エスケープ」する方法がないということです。いくつかの明確にマークされた安全でない演算子を使用しない限り、プログラムは IO Nat から純粋な Nat を取り出す方法がありません。これにより副作用の正しい順序が保たれ、副作用のあるプログラムが副作用を持つものとして明確にマークされることが保証されます。
9.1.1. IO ・ EIO ・ BaseIO モナド（The IO, EIO and BaseIO Monads）
現実世界と相互作用するプログラムで典型的に使われるモナドが2つあります：
この区別により、アクションの型シグネチャを見れば例外が発生するかどうかがわかります。 BaseIO アクションは必要に応じて自動的に IO に昇格します。
def
IO : Type → Type
def
BaseIO : Type → Type
IO と BaseIO はどちらもエラーの型をパラメータとする EIO のインスタンスです。 IO は EIO IO.Error として定義される一方、 BaseIO は EIO Empty として定義されます。 Lean 以外のライブラリへのバインディングなど、状況によっては EIO をカスタムのエラー型で使用すると便利です。これによってそれらのアクションとそれ以外の IO アクションの間に境界を設けてエラーハンドリングされることが保証されます。
def
EIO (ε : Type) : Type → Type
9.1.2. エラーとエラーハンドリング（Errors and Error Handling）
IO モナドにおけるエラー処理は、他の 例外モナド と同じ機能を使用します。特に、例外のスローとキャッチは MonadExceptOf 型クラス のメソッドを使用します。 IO で投げられる例外は IO.Error 型を持ちます。このコンストラクタは、ファイルが存在しないなど、ほとんどのオペレーティングシステムで発生する低レベルのエラーを表します。最もよく使われるエラーは userError で、これは他のすべてのケースをカバーし、問題を説明する文字列を含みます。
inductive type
IO.Error : TypeImitate the structure of IOErrorType in Haskell: https://hackage.haskell.org/package/base-4.12.0.0/docs/System-IO-Error.html#t:IOErrorType
Constructors
unexpectedEof : IO.Error
例外のスローとキャッチ
このプログラムは制御フローに例外を使用して繰り返しパスワードを要求します。例外の構文は IO だけでなく、すべての例外モナドで使用できます。不正なパスワードが提供されると例外が投げられ、パスワードチェックを繰り返すループでキャッチされます。正しいパスワードが指定された場合、制御はチェックを通過してループを終了し、他の例外は再度投げられます。
def accessControl : IO Unit := do
IO.println "What is the password?"
let password ← (← IO.getStdin).getLine
if password.trim != "secret" then
throw (.userError "Incorrect password")
else return
def repeatAccessControl : IO Unit := do
repeat
try
accessControl
break
catch
| .userError "Incorrect password" =>
continue
| other =>
throw other
def main : IO Unit := do
repeatAccessControl
IO.println "Access granted!"
以下の入力で実行すると：
stdinpublicinfosecondtrysecretこのプログラムは以下を出力します：
stdoutWhat is the password?What is the password?What is the password?Access granted!