IO

IO は、入出力(input / output)などの外界とのやり取りを含む計算を表すモナドです。ファイル操作・入出力・乱数・時刻の取得などの副作用のある処理を包んで、副作用のない処理と区別します。

IO α の項は、「実行すると α の値を得られるかもしれない計算」を表します。特に、IO α の項は計算によって得られる値そのものではありません。このニュアンスを強調するために、IO α の項のことを IO アクション と呼ぶことがあります。

IO アクションの例

標準入出力

「ターミナルに文字列を出力する」という操作や、「標準入力から文字列を読み込む」という操作は IO で扱われます。以下は、入力された文字を受け取って、挨拶を返す単純なプログラムの例です。

/-- 標準入力から入力された名前に対して挨拶をする -/
def main : IO Unit := do
  let stdin ← IO.getStdin
  let stdout ← IO.getStdout

  stdout.putStrLn "誰に挨拶しますか？"
  let input ← stdin.getLine
  let name := input.trimAscii -- これをしないと余計な改行が入る

  stdout.putStrLn s!"Hello, {name}!"

出力というのは奥が深いもので、出力が自分自身と等しくなるようなコードを書くこともできます。そのようなコードを クワイン（Quine） と呼ぶのですが、Lean 4 ではクワインはたとえば次のようにして作ることができます。¹

def s := "\ndef main : IO Unit := do\n  IO.println (\"def s := \" ++ s.quote)\n  IO.println (s)"

def main : IO Unit := do
  IO.println ("def s := " ++ s.quote)
  IO.println (s)

/-
info: def s := "\ndef main : IO Unit := do\n  IO.println (\"def s := \" ++ s.quote)\n  IO.println (s)"

def main : IO Unit := do
  IO.println ("def s := " ++ s.quote)
  IO.println (s)
-/
#eval main

また、ユーザの入力を扱うことができるということは、対話的(interactive)なプログラムを書くことができるということです。たとえば、以下のようなプログラムを書くことができます。

ファイル操作

以下は、ファイルを読んでその内容を表示するような簡単なコマンドラインツールを実装する例です。

open IO FS System

/-- シンプルな `cat` コマンドの実装。

コマンドライン引数からファイル名を受け取り、そのファイルの内容を表示する。
ファイル名が指定されていない場合や、複数指定された場合にはエラーメッセージを表示する。
-/
def main (args : List String) : IO Unit := do
  match args with
  | [] => println "ファイル名を指定してください。"
  | [fileName] =>
    let filePath : FilePath := fileName
    let fileExists ← filePath.pathExists
    if fileExists then
      let contents ← readFile filePath
      println contents
    else
      println s!"ファイルは存在しません: {fileName}"
  | _ => println "複数のファイル名は指定できません。1つだけ指定してください。"

ランダム性

乱数を扱うような操作は IO アクションです。

/-- 長さ `n` で、中身の値が 0 以上 `bound` 以下であるようなリストをランダム生成する -/
def randList (n : Nat) (bound : Nat) : IO (List Nat) := do
  let mut out := []
  for _ in [0 : n] do
    -- ランダムに 0 以上 bound 以下の自然数を生成する
    let x ← IO.rand 0 bound

    -- 生成した自然数をリストに追加する
    out := x :: out
  return out

#eval randList 5 10

時刻

時刻を扱うような操作も IO アクションです。

/-- フィボナッチ数列 -/
def fibonacci (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | n + 2 => fibonacci n + fibonacci (n + 1)

/-- `fibonacci` の計算にかかった時間を計測する -/
def computeTime : IO Unit := do
  let start_time ← IO.monoMsNow
  let result := fibonacci 30
  let end_time ← IO.monoMsNow
  IO.println s!"Result: {result}, Time taken: {end_time - start_time} ms"

#eval computeTime

IO からの脱出

IO アクションは基本的に「副作用のある計算」であり、IO から脱出する安全かつ汎用的な関数はありません。言い換えれば、runIO : IO α → α というような参照透過な関数はありません。

しかし Lean は自由度が高い言語でありまして、この制約も破ることができます。unsafe な機能を使ってよければ、IO から脱出することができます。²

import Lean

open Lean Meta Elab Term

def toExprIO {α : Type} [ToExpr α] (x : IO α) : IO Expr :=
  toExpr <$> x

elab tk:"run_io " t:doSeq : term <= expectedType => withRef t do
  let expectedType := mkApp (mkConst ``IO) expectedType
  let v ← elabTermEnsuringType (← `(do $t)) expectedType
  synthesizeSyntheticMVarsNoPostponing
  let v ← instantiateMVars v
  if (← logUnassignedUsingErrorInfos (← getMVars v)) then
    throwAbortTerm
  let v ← mkAppM ``toExprIO #[v]
  let io ← unsafe evalExpr (IO Expr) (mkApp (mkConst ``IO) (mkConst ``Expr)) v
  let (out, x) ← IO.FS.withIsolatedStreams io.toBaseIO
  unless out.isEmpty do
    logInfoAt tk out
  match x with
  | .ok x => return x
  | .error e => throwErrorAt tk e.toString

-- 使用例。ランダムな数を選んでいるのに、型を `Nat` にすることができる
def number : Nat := run_io IO.rand 0 1000

-- 実行前に既に値が決定されているため、
-- 平気で証明ができる
example : 0 ≤ number ∧ number < 1001 := by
  simp [number.eq_def]

このコード例は leanprover-community/lean4-samples に対するPR からの引用です。 ↩
このコードは Lake.DSL.Meta のコードをほぼそのまま引用したものです。 ↩

Lean by Example

IO

IO アクションの例

標準入出力

ファイル操作

ランダム性

時刻

IO からの脱出