プログラムの実行

Lean プログラムを実行する最も簡単な方法は、Lean の実行ファイルに --run オプションを使用することです。Hello.lean という名前のファイルを作成し、以下の内容を入力してみましょう。

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

次に、コマンドラインから以下を実行してください。

lean --run Hello.lean

このプログラムは Hello, world! を表示して終了します。

挨拶の構造

Lean を --run オプション付きで実行すると、プログラムの main 定義が呼び出されます。コマンドライン引数を取らないプログラムの場合、main の型は IO Unit であるべきです。この型には矢印（→）が含まれていません。これは main が関数でないことを意味します。つまり、main は副作用を持つ関数ではなく、実行される作用の説明から成り立っています。

前の章で議論したように、Unit は最も単純な帰納型です。Unit のコンストラクタは一つだけで、unit という引数を取らない関数です。C言語系のプログラミング言語には、何の値も返さない void 関数の概念があります。一方 Lean では、すべての関数が引数を取り、値を返します。引数や返り値がないことは、代わりに Unit 型を使用して示すことができます。Bool が1ビットの情報を表すなら、Unit が表すのは0ビットの情報です。

IO α は、「実行されると型 α の値を返すか、または例外をスローするようなプログラム」の型です。IO α 型を持つプログラムは、実行中に副作用を発生させる可能性があり、IO アクションと呼ばれます。Lean は、変数への値の代入と副作用のない部分式の簡約という数学的モデルに厳密に従う「式の評価」と、外部システムに依存して世界と相互作用する「IO アクションの実行」を区別します。IO.println は文字列から IO アクションへの関数で、実行すると指定された文字列を標準出力に書き込みます。この IO アクションは文字列を出力する過程で環境から情報を読み取らないため、IO.println の型は String → IO Unit です。もし何か値を返すなら、返り値の型は IO Unit ではなくなります。

関数型プログラミングと作用

Lean の計算モデルは数学的な式の評価に基づいています。変数は正確に1つの値を持ち、時間が経っても変化することはありません。式を評価した結果も変わることがなく、同じ式を評価するたびに常に同じ結果が得られます。

一方で、実用上プログラムは世界と相互作用する必要があります。入力や出力を行わないプログラムは、ユーザからデータを要求したり、ディスクにファイルを作成したり、ネットワーク接続を開いたりすることはできません。Lean は Lean 自身で記述されていますが、Lean コンパイラはファイルを読み込んだり、ファイルを作成したり、テキストエディタと対話したりします。ファイルの内容は時間によって変化しうるにも関わらず、「同じ式は常に同じ結果を返す」ような言語で、どうやって「ファイルをディスクから読み込む」というプログラムを実現しているのでしょうか？

この明らかな矛盾は、副作用について少し異なる考え方をすることで解決できます。とあるカフェを想像してみてください。コーヒーとサンドイッチを販売していて、従業員が2人います。このカフェには2人の従業員がいます。注文された料理を作るコックと、客と話して注文を取るカウンターの従業員の2人です。コックは不愛想な人物で、外の世界と接触したくないというのが本音ですが、そのカフェの名物である料理とドリンクを一貫して提供するのはとても得意です。しかし、そのためにはコックには平穏と静けさが必要で、会話で邪魔されてはいけません。カウンターの従業員はフレンドリーな人間ですが、キッチンの仕事は全くできません。客はカウンターの従業員と話し、カウンターの従業員はすべての調理をコックに任せます。コックが客に質問がある場合（アレルギーの確認など）、カウンターの従業員に小さなメモを送り、その従業員が客とやり取りし、返事を書いたメモをコックに返します。

これは例え話で、コックは Lean 言語を表しています。注文が入ると、コックは一貫して注文されたものを忠実に提供します。カウンターの従業員は、世界と相互作用する周囲のランタイムシステムです。支払いを受け取り、食事を運び、お客さんと話をします。2人の従業員は協力して、レストランのすべての機能を提供しますが、彼らの責任は分かれており、それぞれが得意なタスクを実行します。客を遠ざけることでコックが本当においしいコーヒーやサンドイッチを作ることに集中できるのと同じように、Lean は副作用を隔離することで、プログラムを正式な数学的証明の一部として使うことができます。副作用がないことには、プログラムが理解しやすくなるという利点もあります。コンポーネント間の微妙な結合を生み出す隠れた状態変化がないため、プログラムを互いに切り離された部分の集まりとして理解できるからです。コックのメモは、Lean 式を評価して生成される IO アクションを表し、カウンターの従業員の返事は、実行結果から渡される値です。

この副作用のモデルは、Lean 言語全体、コンパイラ、およびランタイムシステム（RTS）の総合的な動作方法とかなり類似しています。ランタイムシステム内のプリミティブな部分はCで書かれており、すべての基本的な作用を実装しています。プログラムを実行する際、RTS は main アクションを呼び出します。呼び出された main アクションは、実行されるべき新しい IO アクションを RTS に返します。RTS はこれらのアクションを実行し、ユーザの Lean コードに計算を実行させます。Lean という内部の視点からは、プログラムに副作用はなく、IO アクションは実行されるべきタスクの説明にすぎません。プログラムのユーザという外部の視点からは、副作用のレイヤが存在していて、プログラムのコアロジックへのインターフェースを形成しているように見えます。

現実世界の関数型プログラミング

Lean における副作用について考えるもう一つの有用な方法は、IO アクションを、世界全体を引数として受け取り、値と新しい世界の組を返す関数と考えることです。この場合、標準入力からテキストを読み取ることは純粋な関数です。なぜなら、異なる世界が引数として都度渡されるからです。標準出力にテキストを書き込むことも純粋な関数です。なぜなら、関数が返す世界は実行開始時のものと異なるからです。プログラムは世界を再利用しないように、新しい世界を返し損ねないように、よくよく注意する必要があります。それは結局、タイムトラベルまたは世界の終了を意味するからです。注意深い抽象化で副作用を隔離することにより、Lean は安全なプログラミングスタイルを実現しています。世界が与えられたら常に新しい世界を返すようなプリミティブ IO アクションを、その条件を保つツールとだけ組み合わせている限り、問題は発生しないのです。

このモデルは実装できません。結局のところ、宇宙全体を Lean の値に変えてメモリに配置することはできません。ただし、このモデルのバリエーションを、世界を表す抽象トークンを使用して実装することは可能です。プログラムが開始するとき、世界のトークンが渡されます。その後、このトークンは IO プリミティブに渡され、返されたトークンも同様に次のステップに渡されます。プログラムの終了時には、トークンは OS に返されます。

この副作用のモデルは、Lean 内部で RTS によって実行されるタスクの説明としての IO アクションがどのように表現されているかを良く説明しています。実際の世界を変える関数は抽象性の壁の背後に隠れています。しかし、実際のプログラムは通常、1つだけでなく一連の作用から成り立っています。プログラムが複数の作用を利用できるようにするために、Lean には do 記法と呼ばれるサブ言語があり、プリミティブな IO アクションを安全に組み合わせて、より大きく有用なプログラムを作ることができます。

IO アクションの結合

ほとんどの有用なプログラムは、出力を生成するだけでなく、入力を受け付けます。さらに、入力データをもとに計算を行い、決定を下すこともあります。次のプログラム、HelloName.lean は、ユーザに名前を尋ね、それから挨拶をします。

def main : IO Unit := 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}!"

このプログラムでは、main アクションは do ブロックで構成されています。do ブロックには、一連の文(statement)が含まれています。それぞれの文は、let によるローカル変数の定義だったり、実行されるアクションであったりします。SQL がデータベースと対話するための特別な目的の言語と考えることができるように、do 構文は、Lean 内で命令型プログラムをモデル化するための専用のサブ言語だと考えることができます。do ブロックで構築された IO アクションは、文を順番に実行することで実行されます。

このプログラムは、前のプログラムと同じ方法で実行できます。

lean --run HelloName.lean

ユーザが David と応答する場合、プログラムとの対話セッションが次のように表示されます。

How would you like to be addressed?
David
Hello, David!

型のシグネチャ行は、Hello.lean のものと同じです。

def main : IO Unit := do

唯一の違いは、キーワード do で終わることです。do はコマンドのシーケンスを開始します。キーワード do に続くインデントされた各行は、同じ一連のコマンドの一部です。

最初の2行は、次のように記載されています。

  let stdin ← IO.getStdin
  let stdout ← IO.getStdout

これらの行は、ライブラリアクション IO.getStdin および IO.getStdout を実行して stdin と stdout のハンドルを取得します。do ブロックの中の let は、通常の式の中の let とはやや異なる意味を持ちます。通常、let で導入されたローカル定義は、すぐにそのローカル定義に続く式でしか使用できません。do ブロックでは、let によって導入されたローカル束縛は、次の式だけでなく、do ブロックの残りのすべての文で使用できます。さらに、通常 let は := を使って定義される名前とその定義を結びつけますが、do 内部の let 束縛においては、代わりに左矢印（← または <-）を使うことがあります。矢印を使用するということは、式の値が IO アクションであり、そのアクションの実行結果をローカル変数に保存するということを意味します。言い換えれば、矢印の右側の式が型 IO α を持つ場合、その変数は do ブロックの残りの部分で型 α を持ちます。IO.getStdin および IO.getStdout は stdin と stdout をプログラム内でローカルに上書きできるようにするための便利な IO アクションです。C 言語のように stdin と stdout がグローバル変数であったら、（Lean では一度束縛した値は変更できないので）これを上書きすることはできませんが、IO アクションなら実行ごとに異なる値を返すことができます。

do ブロックの次の部分は、ユーザに名前を尋ねます。

  stdout.putStrLn "How would you like to be addressed?"
  let input ← stdin.getLine
  let name := input.dropRightWhile Char.isWhitespace

最初の行は質問を stdout に書き込み、2番目の行は stdin から入力をリクエストし、3番目の行は入力行から末尾の改行（および末尾の空白）を削除します。name の定義では、String.dropRightWhile は IO アクションではなく、通常の文字列関数であるため、← ではなく := を使用しています。

最後に、プログラムの最終行は以下のようなものです。

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

ここでは文字列補間を使って、与えられた名前を挨拶の文字列に挿入し、その結果を stdout に書き込んでいます。