IO

IO は、入出力という副作用を伴うプログラムを表します。IO α の項のことを IO アクションと呼ぶことがあります。

標準入出力

IO.println は、標準出力に文字列を出力します。たとえば、ターミナルに文字列を出力したりすることができます。

/- info: hello, world! -/
#eval
  let greet := "world"
  IO.println s!"hello, {greet}!"

ランダム性

ランダムな操作は 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