実例：`cat`

Unix の標準ユーティリティである cat はいくつかのコマンドラインオプションと、それに続く0個以上の入力ファイルを受け付けます。ファイルが指定されないか、指定したファイルのうち1つがダッシュ（-）の場合、ファイルを読む代わりに標準入力を対応する入力として受け付けます。入力の内容は次々に標準出力に書き出されます。指定した入力ファイルが存在しない場合、そのことが標準エラー出力に表示されますが、cat は入力を連結し続けます。存在しない入力ファイルがあったとき、0以外の終了コードが返されます。

この節では、feline と呼ばれる cat の簡易版について説明します。一般的なバージョンの cat と異なり、feline は行番号表示や非印字文字の表示、ヘルプテキストの表示といった機能のコマンドラインオプションはありません。さらに、端末デバイスに関連付けられた標準入力から複数回読み込むこともできません。

この節で最大限の効果を得るには、自分自身でコードを書いてください。コード例をコピーペーストしてもかまいませんが、手書きで入力することを推奨します。そうすることで、コードを入力し、ミスから回復し、コンパイラからのフィードバックを解釈するという機械的なプロセスを学びやすくなります。

はじめる

feline 実装の最初のステップは、パッケージを作成し、コードをどのように整理するかを決めることです。今回の場合、プログラムは非常に簡単なので、すべてのコードは Main.lean に書きます。最初のステップは lake new feline を実行することです。Lakefile を編集してライブラリを削除し、生成されたライブラリコードとその参照を Main.lean も削除します。これが完了すると、lakefile.lean は次のようになります：

import Lake
open Lake DSL

package «feline» {
  -- add package configuration options here
}

@[default_target]
lean_exe «feline» {
  root := `Main
}

そして Main.lean も次のようになります：

def main : IO Unit :=
  IO.println s!"Hello, cats!"

あるいは、lake new feline exe を実行すると lake にライブラリセクションを含まないテンプレートを使用するように指示されるため、ファイルを編集する必要がなくなります。

lake build を実行してコードがビルドできることを確認してください。

ストリームの連結

プログラムの基本的な骨組みができたので、実際にコードを入力するときがきました。cat の適切な実装は /dev/random のような無限の IO ストリームに使うことができます。これは出力する前に入力をメモリに読み込むことができないことを意味します。さらに、cat は一度に1文字ずつ処理すべきではありません。これは非常に遅いパフォーマンスにつながるためです。代わりに、一度に連続したデータブロックを読み取り、そのデータを標準出力に1ブロックずつ送るのがよいでしょう。

最初のステップはどのくらいの大きさのブロックを読み取るかを決めることです。簡単にするため、この実装では控えめに20キロバイトのブロックを使用します。USize は C 言語の size_t に類似しており、すべての有効な配列サイズを表すのに十分な大きさの符号なし整数型です。

def bufsize : USize := 20 * 1024

ストリーム

feline の主な処理は dump によって行われます。dump は一度に1ブロックずつ入力を読み込み、その結果を標準出力に出力し、入力の終わりに達するまでこれを繰り返します。

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

dump 関数は partial 関数（部分関数）として宣言されています。これは、引数が即座に小さくならない入力に対して再帰的に自分自身を呼び出すためです。関数が部分関数として定義されると、Lean はその終了を証明する必要がなくなります。一方で、部分関数は無限ループを許容するため、Lean の論理が不健全になる可能性があり、正しさの証明が非常に困難になります。しかし、dump が終了することを証明する方法はありません。なぜなら、無限の入力（例えば /dev/random からの入力）は実際に終了しないからです。このような場合、関数を partial 関数として宣言する以外の選択肢はありません。

IO.FS.Stream 型は POSIX ストリームを返します。内部的には、各 POSIX ストリーム操作のフィールドを持つ構造体です。各操作は対応する操作を提供する IO アクションとして表現されます。

structure Stream where
  flush   : IO Unit
  read    : USize → IO ByteArray
  write   : ByteArray → IO Unit
  getLine : IO String
  putStr  : String → IO Unit

Lean コンパイラには、標準入力、標準出力、標準エラー出力を表すストリームを取得するための IO アクションが含まれています（例えば dump で呼び出される IO.getStdout）。これらは通常の定義ではなく IO アクションである理由は、Lean がプロセス内でこれらの標準 POSIX ストリームを置き換えることを許可しているためです。これにより、カスタムの IO.FS.Stream を作成してプログラムの出力を文字列にキャプチャするなどの操作が容易になります。

dump の制御フローは本質的には while ループです。dump が呼び出されたとき、もしストリームがファイルの終端に達していたなら、pure () によって関数が終了します。このとき、pure () は Unit コンストラクタを返します。ストリームがファイルの終端に達していない場合は、1ブロック分のデータが読み込まれ、その内容が標準出力（stdout）に書き出されます。その後、dump は再帰的に自分自身を呼び出します。この再帰呼び出しは、stream.read が空のバイト配列を返すまで続きます。空のバイト配列が返されることは、ファイルの終端に達したことを意味します。

dump のように、do の中で if 式が使用される場合、if の各分岐には暗黙的に do が付与されます。つまり、else に続く一連の手順は、あたかも先頭に do があるかのような一連の IO アクションとして扱われます。また、if の分岐内で let によって導入された名前は、それぞれの分岐内でのみ有効であり、if の外側ではスコープに入らないことに注意してください。

dump を呼び出してもスタック領域が不足する心配はありません。これは、再帰呼び出しが関数内での最後の処理として実行され、その結果が直接返されるだけで、追加の操作や計算が行われないためです。このような再帰は末尾再帰（tail recursion）と呼ばれ、この本の後半でより詳しく説明されています。また、コンパイルされたコードが状態を保持する必要がないため、Lean コンパイラはこの再帰呼び出しを単なるジャンプ命令に変換できます。

feline が単に標準入力を標準出力にリダイレクトするだけであれば、dump だけで十分です。しかし、feline には、コマンドライン引数として与えられたファイルを開き、その内容を出力する機能も必要です。引数が存在するファイル名である場合、fileStream はそのファイルの内容を読み取るストリームを返します。一方で、引数がファイルではない場合、fileStream はエラーを出力し、none を返します。

def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
  let fileExists ← filename.pathExists
  if not fileExists then
    let stderr ← IO.getStderr
    stderr.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))

ファイルをストリームとして開くには、2つのステップが必要です。まず、ファイルを読み取りモードで開くことでファイルハンドルが作成されます。Lean のファイルハンドルは、基盤となるファイルディスクリプタを追跡します。ファイルハンドル値への参照がなくなると、ファイナライザがファイルディスクリプタを閉じます。次に、そのファイルハンドルに POSIX ストリームと同じインターフェースを与えます。これは IO.FS.Stream.ofHandle を使用して行われます。この関数は、Stream 構造体の各フィールドに、ファイルハンドル上で動作する対応する IO アクションを埋め込みます。

入力の処理

feline のメインループは、もう一つの末尾再帰関数である process です。process は、入力のいずれかが読み取れなかった場合にゼロではない終了コードを返すため、プログラム全体の現在の終了コードを表す exitCode を引数として受け取ります。さらに、処理する入力ファイルのリストも引数として受け取ります。

def process (exitCode : UInt32) (args : List String) : IO UInt32 := do
  match args with
  | [] => pure exitCode
  | "-" :: args =>
    let stdin ← IO.getStdin
    dump stdin
    process exitCode args
  | filename :: args =>
    let stream ← fileStream ⟨filename⟩
    match stream with
    | none =>
      process 1 args
    | some stream =>
      dump stream
      process exitCode args

if と同様に、do の中で使用される match の各分岐には、暗黙的にそれぞれ独自の do が付与されます。

ここでは3つの可能性があります。1つ目は、処理するファイルがもう残っていない場合で、このとき process はエラーコードを変更せずにそのまま返します。2つ目は、指定されたファイル名が "-" の場合で、このとき process は標準入力の内容をダンプした後、残りのファイル名を処理します。3つ目は、実際のファイル名が指定された場合です。このときは fileStream を使用してそのファイルを POSIX ストリームとして開こうとします。引数は ⟨ ... ⟩ で囲まれていますが、これは FilePath が文字列を含む単一フィールドの構造体だからです。もしファイルが開けなかった場合、そのファイルはスキップされ、process の再帰呼び出しで終了コードが 1 に設定されます。ファイルが開けた場合、ファイルの内容がダンプされ、その後の process の再帰呼び出しでは終了コードは変更されません。

process は構造的に再帰であるため、partial としてマークする必要はありません。すべての Lean のリストは有限で、各再帰呼び出しには入力リストの末尾が渡されます。そのため、process は終了しないことはありません。

Main の処理

最後のステップは　main アクションを記述することです。以前の例とは異なり、feline の main は関数です。Lean における main には、次の3つの種類があります：

main : IO Unit は、コマンドライン引数を読み取ることができず、常に終了コード 0 で成功を示すプログラムに対応します。
main : IO UInt32 は、C 言語の int main(void) に対応し、引数をとらず終了コードを返します。
main : List String → IO UInt32 は、C 言語の int main(int argc, char **argv) に対応し、引数を受け取り、成功または失敗を示す終了コードを返します。

引数がない場合、feline は標準入力から読み取るようにします。このとき、"-" 引数が1つ渡されたかのように扱います。引数が提供されている場合は、それぞれの引数を順番に処理します。

def main (args : List String) : IO UInt32 :=
  match args with
  | [] => process 0 ["-"]
  | _ =>  process 0 args

ニャー！

feline が正しく動作するか確認するための最初のステップは、コマンドラインで lake build を実行してビルドすることです。まず、引数なしで呼び出した場合、標準入力から受け取った内容をそのまま出力するはずです。次のように実行すると、

echo "It works!" | ./build/bin/feline

It works! が出力されます。

次に、引数を渡して呼び出すと、それらのファイルの内容が出力されるはずです。例えば test1.txt が、

It's time to find a warm spot

として、test2.txt が、

and curl up!

のとき、次のコマンドを実行すると、

./build/bin/feline test1.txt test2.txt

以下のような出力になるはずです。

It's time to find a warm spot
and curl up!

最後に、- の引数が適切に処理されることを確認します。

echo "and purr" | ./build/bin/feline test1.txt - test2.txt

結果は次のようになるはずです。

It's time to find a warm spot
and purr
and curl up!

演習問題

feline が使用方法の情報をサポートするように拡張しましょう。拡張したバージョンでは、--help 引数を受け取るようにします。この引数が渡された場合、feline で使用できるコマンドラインオプションについてのドキュメントが標準出力に表示されるようにします。

Functional Programming in Lean 日本語訳