その他の便利機能

ネストされたアクション

feline の関数の多くは IO アクションの結果に名前を付けてすぐ一度だけ使うというパターンを繰り返していました。例えば、dump の場合：

partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf ← stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    let stdout ← IO.getStdout
    stdout.write buf
    dump stream

stdout のところでこのパターンが発生しています：

    let stdout ← IO.getStdout
    stdout.write buf

同様に、fileStream も以下のコード片を含みます：

  let fileExists ← filename.pathExists
  if not fileExists then

Leanが do ブロックをコンパイルする時、括弧のすぐ下にある左矢印からなる式は、それを包含する最も近い do に持ち上げられ、その式の結果が一意な名前に束縛されます。この一意名でもともとの式が置き換えられます。つまり、dump は次のように書くこともできます：

partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf ← stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    (← IO.getStdout).write buf
    dump stream

このバージョンの dump では、一度しか使わない名前の導入を避けることができるため、プログラムを大幅に簡略にすることができます。ネストされた式のコンテキストからLeanが持ち上げた IO アクションは ネストされたアクション と呼ばれます。

fileStream も同じテクニックを使って簡略にできます：

def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
  if not (← filename.pathExists) then
    (← IO.getStderr).putStrLn s!"File not found: {filename}"
    pure none
  else
    let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
    pure (some (IO.FS.Stream.ofHandle handle))

ここでは、handle というローカル名をネストされたアクションを使って削除することもできますが、その場合は式が長く複雑になってしまいます。ネストされたアクションを使うことが良い場合が多いとはいえ、中間的な結果に名前を付けておくと便利なこともあります。

しかし、ネストされたアクションは do ブロックの中で起こる IO アクションの短縮表記に過ぎないことを覚えておくことが重要です。アクションの実行に伴う副作用は同じ順序で発生し、副作用の実行が式の評価と混在することはありません。これが混乱を招く可能性がある例として、実行されたことを世界に通知した後にデータを返す以下の補助的な定義を考えてみましょう：

def getNumA : IO Nat := do
  (← IO.getStdout).putStrLn "A"
  pure 5

def getNumB : IO Nat := do
  (← IO.getStdout).putStrLn "B"
  pure 7

これらの定義はユーザ入力を検証したり、データベースを読み込んだり、ファイルを開いたりするようなより複雑な IO コードの代用を意図しています。

数字Aが5の時は 0 を、それ以外の時は B の数値を表示するプログラムは次のように書けます：

def test : IO Unit := do
  let a : Nat := if (← getNumA) == 5 then 0 else (← getNumB)
  (← IO.getStdout).putStrLn s!"The answer is {a}"

しかし、このプログラムはおそらく意図した以上の副作用（ユーザ入力のプロンプトやデータベースの読み取りなど）を持ちます。getNumA の定義では、常に 5 を返すことが明確になっているので、このプログラムではBの数値を読み込むべきではありません。しかし、プログラムを実行すると次のような出力が得られます：

A
B
The answer is 0

getNumB was executed because test is equivalent to this definition:

def test : IO Unit := do
  let x ← getNumA
  let y ← getNumB
  let a : Nat := if x == 5 then 0 else y
  (← IO.getStdout).putStrLn s!"The answer is {a}"

これはネストされたアクションは 最も近い do ブロックに持ち上げられるルールによるものです。なぜならここでの文は a を定義している let であって if は do ブロックの中の文ではないため、この if の分岐は暗黙的に do ブロックで囲まれないのです。実際、条件式の型は IO Nat ではなく Nat であるため、このようにラップすることはできません。

do の柔軟なレイアウト

Leanにおいて、do 式は空白に対して敏感です。do の各 IO アクションや局所的な束縛はそれぞれ独立した行で始まり、インデントも同じでなければなりません。ほとんどすべての do はこのように書くべきです。しかしまれに空白やインデントを手動で制御する必要や、複数の小さなアクションを1行に書くと便利な場合があります。このような場合、改行はセミコロンに、インデントは波括弧に置き換えることができます。

例えば、以下のプログラムはすべての等価です：

-- This version uses only whitespace-sensitive layout
def main : IO Unit := do
  let stdin ← IO.getStdin
  let stdout ← IO.getStdout

  stdout.putStrLn "How would you like to be addressed?"
  let name := (← stdin.getLine).trim
  stdout.putStrLn s!"Hello, {name}!"

-- This version is as explicit as possible
def main : IO Unit := do {
  let stdin ← IO.getStdin;
  let stdout ← IO.getStdout;

  stdout.putStrLn "How would you like to be addressed?";
  let name := (← stdin.getLine).trim;
  stdout.putStrLn s!"Hello, {name}!"
}

-- This version uses a semicolon to put two actions on the same line
def main : IO Unit := do
  let stdin ← IO.getStdin; let stdout ← IO.getStdout

  stdout.putStrLn "How would you like to be addressed?"
  let name := (← stdin.getLine).trim
  stdout.putStrLn s!"Hello, {name}!"

慣用的なLeanの do のコードでは波括弧を使うことはほとんどありません。

#eval による IO アクションの実行

Leanの #eval コマンドは単に式の評価だけでなく、IO アクションを実行するために使用することができます。通常、#eval コマンドをLeanファイルに追加すると、Leanは指定された式を評価し、結果の値を文字列に変換して、その文字列をツールチップやinfoウィンドウに表示します。IO アクションは文字列に変換できないからといって失敗させるのではなく、#eval はそのアクションを実行し、その副作用を執り行います。実行結果が Unit 型の値 () の場合、結果の文字列は表示されませんが、文字列に変換できる型であればLeanは結果の値を表示します。

つまり、countdown と runActions の定義があらかじめ与えられているとした時：

#eval runActions (countdown 3)

は以下を出力します。

3
2
1
Blast off!

これは IO アクションを実行することによって生成される出力であり、アクション自体の不透明な表現ではありません。言い換えれば、IO アクションに対して #eval は指定された式の 評価 と、結果のアクションの値の 実行 をどちらも行います。

#eval を使って IO アクションを素早くテストすることはプログラム全体をコンパイルして実行することよりもはるかに便利です。しかし、いくつかの制限があります。例えば、標準入力からの読み込みは単に空の入力を返すだけになります。さらに、IO アクションはLeanがユーザに提供する新参情報を更新する必要があるたびに再実行され、これによって実行タイミングが予測できなくなります。例えば、ファイルを読み書きするアクションは、都合の悪い時に実行される可能性があります。