まとめ

評価 vs 実行

副作用とはファイルの読み込み・例外の発生・産業機械の起動など、数式の評価を超えたプログラムの実行についての側面です。ほとんどの言語では評価中に副作用が発生することを許可していますが、Leanでは許可していません。その代わりに、Leanには IO という型があり、副作用を使用するプログラムの 記述 を表現します。これらの記述は言語のランタイムシステムによって実行されます。このランタイムシステムはLeanの式の評価器を呼び出して特定の計算を実行します。IO α 型の値は IO アクション と呼ばれます。最も単純なものは pure で、これは引数をそのまま返し、実際の副作用を持ちません。

IO アクションは世界全体を引数として受け取り、副作用が発生した新しい世界を返す関数として理解することもできます。その裏では、IO ライブラリは世界が決して複製されたり、新しく作られたり、破壊されたりしないことを保証しています。全宇宙は大きすぎてメモリに収まらないため、この副作用のモデルを実際に実装することはできませんが、現実の世界をプログラム中で受け渡されるトークンとして表現することができます。

IO アクション main はプログラムが開始された時に実行されます。main は以下3つのうちどれかの型を持ちます：

  • main : IO Unit はコマンドライン引数を読むことができず、常に終了コード 0 を返す単純なプログラムに使われます。
  • main : IO UInt32 は成功または失敗を知らせる引数のないプログラムに使われます。
  • main : List String → IO UInt32 はコマンドライン引数を取り、成功または失敗を知らせるプログラムに使われます。

do 記法

Leanの標準ライブラリは、ファイルからの読み込みや書き込み、標準入出力とのやり取りなどの作用を表す基本的な IO アクションを数多く提供しています。これらの基本的な IO アクションは、副作用を持つプログラムを書くための組み込みドメイン固有言語である do 記法を使ってより大きな IO アクションにまとめることができます。do 記法は以下のような一連の 文 を含んでいます：

  • IO アクションを表す式
  • let と := を使った通常のローカル定義、定義された名前は渡された式の値を指します。
  • let と ← を使ったローカル定義、定義された名前は渡された式の値を実行した結果を指します。

do で記述された IO アクションは一度に1文ずつ実行されます。

さらに、do の直下にある if 式と match 式は、暗黙的にそれぞれの分岐に do があると見なされます。do 式の内部では、ネストされたアクション は括弧の直下にある左矢印で記述された式です。Leanコンパイラは、暗黙的にそれらを最も近い do （match や if の分岐に暗黙的にあるものも含みます）に結び付け、一意な名前を付けます。この一意な名前によってネストされたアクションのもともとの位置を置き換えます。

プログラムのコンパイルと実行

lean --run FILE というコマンドで main 定義を持つ単一ファイルで構成されるLeanプログラムを実行することができます。これは簡単なプログラムの実行には良い方法ですが、ほとんどのプログラムは最終的に複数のファイルを持つプロジェクトへと成長するので、実行する前にコンパイルする必要があります。

Leanのプロジェクトは、依存関係やビルド構成に関する情報とともにライブラリや実行可能ファイルのコレクションである パッケージ へと編成されます。パッケージはLeanのビルドツールであるLakeを使って記述します。新しいディレクトリにLakeパッケージを作成するには lake new を、現在のディレクトリに作成するには lake init を使用します。Lakeのパッケージ構成もドメイン固有言語です。プロジェクトをビルドするには lake build を使用します。

部分性

式評価の数学的モデルに従うことから導かれる結論の1つとして、すべての式が値を持たなければならないということがあります。これにより、データ型のすべてのコンストラクタをカバーできない不完全なパターンマッチと無限ループに陥る可能性のあるプログラムの両方が除外されます。Leanはすべての match 式がすべてのケースをカバーすること、すべての再帰関数は構造的に再帰的であるか停止の明示的な証明があることを保証します。

しかし、実際のプログラムの中にはPOSIXのストリームのように無限ループする可能性のあるデータを扱うために、無限ループの可能性を必要とするものがあります。これに対してLeanは逃げ道を用意しています：定義が partial とマークされた関数は停止する必要がありません。これには代償が伴います。型はLean言語の第一級であるため、関数は型を返すことができます。しかし、関数が無限ループに入ると型チェッカが無限ループも入る可能性があるため、部分関数は型チェック中に評価されません。さらに、数学的な証明では部分関数の定義を検査することができないため、部分関数を使用するプログラムは形式的な証明にあまり適していません。