IO

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

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

IO アクションの例

標準入出力

標準出力ストリームに何かを書き込んだり、標準入力ストリームから何かを受け取ったりする処理は IO アクションです。以下は、ユーザによりキーボードから入力された文字を受け取って、挨拶を返す単純なプログラムの例です。

/-- キーボードからユーザの入力を取得する -/
def getUserInput : IO String := do
  -- 入力待ちであることをアピールする
  IO.print "> "
  let stdin ← IO.getStdin
  let input ← stdin.getLine
  -- trim をしないと余計な改行が入る
  return input.trimAscii.copy

/-- 標準入力から入力された名前に対して挨拶をする -/
def main : IO Unit := do
  IO.println "誰に挨拶しますか？"
  let name ← getUserInput
  IO.println s!"Hello, {name}!"

標準出力に書き込んだ後、同じ行を上書きすることによって、ターミナル上でアニメーションを表示することができます。以下は、処理の進捗を表すスピナーを表示する例です。

def spinnerFrames : Array String :=
  #["⠋", "⠙", "⠹", "⠸", "⠼", "⠴", "⠦", "⠧", "⠇", "⠏"]

/-- ターミナルに対して、現在のカーソルがある行全体を消せと指示する -/
def IO.clearLine : IO Unit := do
  IO.print "\r\x1b[2K"

def main : IO Unit := do
  -- 標準出力ストリームを取得する
  let stdout ← IO.getStdout

  for i in List.range 80 do
    let frame := spinnerFrames[i % spinnerFrames.size]!
    IO.print s!"\r{frame} 処理中..."

    -- 標準出力への変更をすぐに反映させる
    stdout.flush

    -- ここに「少しずつ進む重い処理」を書く
    IO.sleep 20

  -- 行を消して完了表示
  IO.clearLine
  IO.println "完了"

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

余談ですが、Lean 4 でもクワイン(quine)を書くことができます。

ファイル操作

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

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
  -- コンパイラに最適化されて実行順序が変わらないように、`IO.lazyPure` で包む
  let result ← IO.lazyPure <| fun _ => 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]

このコードは Lake.DSL.Meta のコードをほぼそのまま引用したものです。 ↩

Lean by Example

IO

IO アクションの例

標準入出力

ファイル操作

ランダム性

時刻

IO からの脱出