9. IO🔗

Lean は純粋関数型プログラミング言語です。Lean のコードは実行時に正格評価されますが、型チェック、特に definitional equality のチェックをする際に使用される評価の順序は形式的に指定されておらず、パフォーマンスを向上させる今後変更の可能性がある多くのヒューリスティックを使用しています。つまり、副作用（ファイル I/O・例外・可変な参照など）を実行する操作を単純に追加すると、作用の順序が特定されないプログラムになります。型チェックでは、自由変数を持つ項でさえも簡約されます；これは副作用の予測をさらに難しくします。最後に、Lean のロジックの基本法則は、関数は定義域の各要素を値域の一意な値にマッピングする 関数 であるということです。コンソール I/O・任意の可変状態・乱数生成などの副作用を含めると、この原則に反することになります。

副作用を持つ可能性のあるプログラムを純粋な関数と区別するための型（一般的に IO α と書かれる）があります。論理的に言えば、 IO は副作用のシーケンスとデータの依存関係を記述します。ファイルからの読み込みなどの基本的な副作用の多くは、Lean の論理の視点からすると不透明な定数です。その他の副作用は、実行時のコードと論理的に同等なコードによって指定されます。実行時には、コンパイラは通常のコードを生成します。

  1. 9.1. 論理モデル（Logical Model）
    1. 9.1.1. IO ・ EIO ・ BaseIO モナド（The IO, EIO and BaseIO Monads）
    2. 9.1.2. エラーとエラーハンドリング（Errors and Error Handling）
      1. 9.1.2.1. IO エラーの構成（Constructing IO Errors）
  2. 9.2. 制御構造（Control Structures）
  3. 9.3. コンソール出力（Console Output）
  4. 9.4. 可変参照（Mutable References）
    1. 9.4.1. 状態変換（State Transformers）
      1. 9.4.1.1. 読み込みと書き込み（Reading and Writing）
      2. 9.4.1.2. 比較（Comparisons）
      3. 9.4.1.3. 並行性（Concurrency）
  5. 9.5. ファイル・ファイルハンドラ・ストリーム（Files, File Handles, and Streams）
    1. 9.5.1. 低レベルのファイル API（Low-Level File API）
    2. 9.5.2. ストリーム（Streams）
    3. 9.5.3. パス（Paths）
    4. 9.5.4. ファイルシステムの対話（Interacting with the Filesystem）
    5. 9.5.5. 標準 I/O（Standard I/O）
    6. 9.5.6. ファイルとディレクトリ（Files and Directories）
  6. 9.6. 環境変数（Environment Variables）
  7. 9.7. タイミング（Timing）
  8. 9.8. プロセス（Processes）
    1. 9.8.1. 現在のプロセス（Current Process）
    2. 9.8.2. プロセスの実行（Running Processes）
  9. 9.9. 乱数（Random Numbers）
    1. 9.9.1. 乱数生成（Random Generators）
    2. 9.9.2. システムの乱数（System Randomness）
  10. 9.10. Tasks and Threads