特別な型

メモリ上でのデータ表現を理解することは非常に重要です。通常、このような表現はデータ型の定義から理解することができます。各コンストラクタはタグと参照カウントを含むヘッダを持つメモリ上のオブジェクトに対応します。コンストラクタの引数はそれぞれ対応するオブジェクトへのポインタで表されます。言い換えると、List は本当に連結リストであり、structure からフィールドを取り出すことはまさにポインタを追跡することになります。

しかし、このルールにはいくつかの重要な例外があります。いくつかの型はコンパイラによって特別に扱われます。例えば、UInt32 型は Fin (2 ^ 32) として定義されていますが、実行時には機械語に基づく実際のネイティブ実装に置き換えられます。同様に、Nat の定義が List Unit に似た実装を示唆している一方で、実際の実行時の表現においては、十分に小さい数には即座に機械語を使用し、大きい数には効率的な任意精度の算術ライブラリを使用します。Leanのコンパイラはパターンマッチを使用する定義をこの表現に適した演算に変換し、加算や減算のような演算の呼び出しには基礎となる算術ライブラリの高速な演算にマッピングされます。この結果、足し算は加算する値の大きさに比例して時間がかかるようなものになるべくもありません。

いくつかの型が特別な表現を持っているということは、それらを扱う際に注意が必要だということでもあります。これらの型のほとんどは、コンパイラによって特別に扱われる structure からなります。これらの構造体では、コンストラクタやフィールドアクセサを直接使用すると効率的な表現から証明に便利な遅い表現への高価な変換が引き起こされる可能性があります。例えば、String は文字のリストを含む構造体として定義されていますが、文字列の実行時の表現ではUTF-8が使用され、文字へのポインタの連結リストは使用されません。文字のリストにコンストラクタを適用すると、UTF-8でエンコードされたバイト文字列が作成され、構造体のフィールドにアクセスすると、UTF-8表現をデコードして連結リストを割り当てるために、文字列に対して線形に時間がかかります。配列も同じように表現されます。論理的な観点からは、配列は配列要素を含む構造体ですが、実行時の表現は動的配列です。実行時にはコンストラクタがリストを配列に変換し、フィールドアクセサが配列から連結リストを割り当てます。さまざまな配列操作はコンパイラによって効率的なバージョンに置き換えられ、新しい配列を割り当てる代わりに可能な限り配列を更新するようにします。

型自体と命題の証明のどちらもコンパイルされたコードからは完全に消去されます。言い換えればそれらはスペースを取らず、証明の一部として実行されていただろう計算も同様に消去されます。つまり、証明はプログラム実行中に遅い変換ステップを課されることなく、帰納的に定義されたリストとしての文字列や配列に対して、帰納法による証明などの便利なインタフェースを利用することができます。これらの組み込み型では、データの便利な論理表現によって、プログラムが遅くなることはありません。

構造体型が非型で非証明のフィールドを1つだけ持つ場合、コンストラクタ自体が実行時に消滅し、その1つだけの引数に置き換えられます。つまり、部分型はその基本の型に対して間接的に参照する追加のレイヤーを持たずに、基本型と同じように表現されます。同様に、Fin はメモリ上では単なる Nat であり、Nat や String の異なる使用を追跡するための単一のフィールドを持つ構造体をパフォーマンスを落とすことなく作成することができます。コンストラクタに非型で非証明の引数が無い場合、コンストラクタも消滅し、ポインタが使用される定数値に置き換えられます。つまり、true ・false ・none はヒープに割り当てられたオブジェクトへのポインタではなく、定数値となります。

以下の型は特別な表現を持ちます：

演習問題

Pos の定義 はLeanが Nat を効率的な型にコンパイルすることを利用していません。実行時において、これは本質的に連結リストとなってしまいます。別の方法として、部分型に関する最初の節 で説明したように、Leanの高速な Nat 型を内部で使用できるようにする部分型を定義することができます。実行時にはこの証明は消去されます。結果の構造体はたった一つのデータフィールドを持つため、これは Pos の新しい表現が Nat の表現と同じであることを意味します。

定理 ∀ {n k : Nat}, n ≠ 0 → k ≠ 0 → n + k ≠ 0 を証明したのちに、この Pos の新しい表現への ToString と Add のインスタンスを定義してください。その次に、必要な定理を証明しながら Mul のインスタンスを定義してください。