ステップ・バイ・ステップ

do ブロックは一行ずつ実行できます。前の節のプログラムから始めましょう：

  let stdin ← IO.getStdin
  let stdout ← IO.getStdout
  stdout.putStrLn "How would you like to be addressed?"
  let input ← stdin.getLine
  let name := input.dropRightWhile Char.isWhitespace
  stdout.putStrLn s!"Hello, {name}!"

標準入出力

最初の行は let stdin ← IO.getStdin で残りの部分は以下の通りです：

  let stdout ← IO.getStdout
  stdout.putStrLn "How would you like to be addressed?"
  let input ← stdin.getLine
  let name := input.dropRightWhile Char.isWhitespace
  stdout.putStrLn s!"Hello, {name}!"

← を使った let 文を実行するには、まず矢印の右側にある式（この場合は IO.getStdIn）を評価します。この式は単なる変数なので、その値が参照されます。結果として得られる値は組み込みのプリミティブな IO アクションです。次のステップはこの IO アクションを実行し、標準入力ストリームを表す値を得ることです。この値は IO.FS.Stream 型です。標準入力はその後、矢印の左側の名前（ここでは stdin）に関連付けられ、do ブロックの残りの部分で使用されます。

2行目の let stdout ← IO.getStdout の実行も同様に進みます。まず、IO.getStdout という式が評価され、標準出力を返す IO アクションが得られます。次に、このアクションが実行され、実際に標準出力が返されます。最後に、この値が stdout という名前に関連付けられ、do ブロックの残りの部分で使用されます。

質問をする

stdin と stdout が定まったので、ブロックの残りの部分は質問と答えから構成されます：

  stdout.putStrLn "How would you like to be addressed?"
  let input ← stdin.getLine
  let name := input.dropRightWhile Char.isWhitespace
  stdout.putStrLn s!"Hello, {name}!"

ブロックの最初の文である stdout.putStrLn "How would you like to be addressed?" は式から成り立っています。式を実行するにはまず評価します。今回の場合、IO.FS.Stream.putStrLn は IO.FS.Stream → String → IO Unit 型を持ちます。これはストリームと文字列を受け取り、IO アクションを返す関数であることを意味します。この式は関数呼び出しのためにアクセサ記法を使用しています。呼び出された関数には標準出力ストリームと文字列の2つの引数が適用されます。よってこの式の値は文字列と改行文字を出力ストリームに書き込む IO アクションです。値が決まった後、次のステップでそれを実行することにより、実際に文字列と改行文字が stdout に書き込まれます。式だけで構成される文は新しい変数を導入しません。

次の文は let input ← stdin.getLine です。IO.FS.Stream.getLine は IO.FS.Stream → IO String 型を持ちます。これはストリームを受け取り、文字列を返す IO アクションであることを意味します。これもアクセサ記法の一例です。この IO アクションが実行されると、プログラムはユーザが入力を完了するまで待機します。ユーザが "David" と入力したとすると、結果として得られる文字列（"David\n"）は input に関連付けられます（\n はエスケープシーケンスでここでは改行文字を表します）。

  let name := input.dropRightWhile Char.isWhitespace
  stdout.putStrLn s!"Hello, {name}!"

次の行 let name := input.dropRightWhile Char.isWhitespace は let 文です。このプログラムの他の let 文とは異なり、← ではなく := を使用しています。これは、式が評価されるものの、その結果の値は IO アクションである必要はなく、実行もされないことを意味します。今回の場合、String.dropRightWhile は文字列と文字に対する述語を受け取り、述語を満たす文字を末尾から全て削除した新しい文字列を返します。例えば、

#eval "Hello!!!".dropRightWhile (· == '!')

は次の文字列を返し、

"Hello"

また、

#eval "Hello...   ".dropRightWhile (fun c => not (c.isAlphanum))

は次の文字列を返します。

"Hello"

このように文字列の右側から英数字ではない文字を全て削除します。現在のプログラムの行では、空白文字（空白文字として改行文字も含まれる）が入力文字列の右側から削除され、その結果得られる "David" がこのブロックの残りの部分で name に関連付けられます。

ユーザへの挨拶

do ブロック内で実行される残りの文は以下の1行です：

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

putStrLn への文字列引数は文字列補完によって構築され、"Hello, David!" という文字列になります。この文は式なので、評価されると、文字列を改行とともに標準出力に表示する IO アクションが得られます。この式が評価されると、結果として得られる IO アクションが実行され、挨拶が表示されます。

値としての `IO` アクション

上記の説明では、式の評価と IO アクションの実行の区別がなぜ必要なのかわかりにくいかもしれません。結局のところ、各アクションは生成された直後に実行されます。他の言語のように、評価中に作用を実行しないのはなぜでしょうか？

答えは2つあります。まず、評価と実行を分離することで、プログラムはどの関数が副作用を持つか明示的に示す必要があります。副作用を持たないプログラムの部分は数学的な推論がしやすいため、プログラマが頭の中で考える場合でも Lean の形式証明の機能を使う場合でも、この分離はバグを回避しやすくします。次に、すべての IO アクションが生成された時点で実行される必要はありません。アクションを実行せずに記述できる機能により、通常の関数を制御構造として使用できるようになります。

例えば、twice 関数は IO アクションを引数にとり、最初のアクションを2回実行する新しいアクションを返します。

def twice (action : IO Unit) : IO Unit := do
  action
  action

例えば、以下を実行すると、

twice (IO.println "shy")

結果は、

shy
shy

のように出力されます。これは、基礎となるアクションを任意の回数実行するバージョンに一般化できます：

def nTimes (action : IO Unit) : Nat → IO Unit
  | 0 => pure ()
  | n + 1 => do
    action
    nTimes action n

基底ケースである Nat.zero では、結果は pure() です。pure 関数は副作用のない IO アクションを作成し、引数（この場合 Unit のコンストラクタ）を返します。何もせず何の興味深いものも返さないアクションである pure() はとても退屈であると同時に非常に便利です。再帰的なステップでは、do ブロックを使って、最初に action を実行した後にその再帰呼び出しの結果を実行するアクションを作成します。

Hello
Hello
Hello

制御構造として関数を使うことに加えて、IO アクションが第一級の値であるということは、後で実行するためにその値をデータ構造として保存できることを意味します。例えば、countdown 関数は Nat を引数にとり、未実行の Nat ごとの IO アクションのリストを返します：

def countdown : Nat → List (IO Unit)
  | 0 => [IO.println "Blast off!"]
  | n + 1 => IO.println s!"{n + 1}" :: countdown n

この関数は副作用がなく、何も出力しません。例えば、引数にこの関数を適用して、結果として得られるアクションのリストの長さを確認することができます：

def from5 : List (IO Unit) := countdown 5

このリストは6つの要素を含みます（各数値ごとのアクションに加えて、ゼロのときの "Blast off!"）：

#eval from5.length

runActions 関数はアクションのリストを受け取り、それらを順番に実行する一つのアクションを構築します：

def runActions : List (IO Unit) → IO Unit
  | [] => pure ()
  | act :: actions => do
    act
    runActions actions

これは nTimes と同じ構造ですが、Nat.succ ごとに実行されるアクションが1つずつあるのではなく、List.cons ごとに実行されるアクションがあります。同様に、runActions はそれ自体ではアクションを実行しません。アクションを実行する新しいアクションを作成し、そのアクションは main の一部として実行される位置に置かなければいけません：

def main : IO Unit := runActions from5

このプログラムを実行すると、以下のような出力が得られます：

5
4
3
2
1
Blast off!

プログラムを実行したときに何が起こっているのでしょうか？最初のステップは main の評価です。以下のように実行されます：

main
===>
runActions from5
===>
runActions (countdown 5)
===>
runActions
  [IO.println "5",
   IO.println "4",
   IO.println "3",
   IO.println "2",
   IO.println "1",
   IO.println "Blast off!"]
===>
do IO.println "5"
   IO.println "4"
   IO.println "3"
   IO.println "2"
   IO.println "1"
   IO.println "Blast off!"
   pure ()

IO アクションの結果は do ブロックです。do ブロックの各ステップが1つずつ実行され、期待する出力が得られます。最後のステップである pure() は何の作用もなく、runActions の定義として基底ケースが必要なため存在しています。

演習問題

次のプログラムの実行を、紙の上でステップ実行してください：

def main : IO Unit := do
  let englishGreeting := IO.println "Hello!"
  IO.println "Bonjour!"
  englishGreeting

プログラムをステップ実行しながら、いつ式が評価されて、いつ IO アクションが実行されるかを確認してください。IO アクションを実行した結果、副作用が発生したときは、それを書き留めます。紙の上での実行が終わった後、Lean を使ってプログラムを実行し、副作用に関するあなたの予想が正しかったかを再確認してください。

Functional Programming in Lean 日本語訳