まとめ
依存型
依存型とは型が関数呼び出しや通常のデータコンストラクタのような型ではないコードを含むものであり、型システムの表現力を飛躍的に高めてくれます。引数の 値 から型を 計算 できるということは、関数の戻り値の型を引数の値によって変えることができるということです。これは例えば、データベースのクエリの結果の型を、潜在的に失敗するかもしれないキャスト操作などの必要無しに、データベースのスキーマと発行された特定のクエリに依存させるために使用することができます。クエリが変更されると、それを実行した結果の型も変更されるため、コンパイル時に即座にフィードバックを得ることができます。
関数の戻り値の型が値に依存する場合、パターンマッチで値を分析すると、値を表す変数がパターン内のコンストラクタで置き換えられるため型が 絞り込まれる ことがあります。関数の型シグネチャは戻り値の型が引数の値に依存する方法を文書化したものであり、パターンマッチは戻り値の型が各引数の可能性に対してどのように満たされるかを説明するものです。
型の中で発生する通常のコードは型チェック中に実行されますが、無限にループする可能性のある partial 関数は呼び出されません。ほとんどの場合、この計算は 本書の冒頭 で紹介した通常の評価のルールに従い、最終的な値が見つかるまで式は逐次値を置き換えられていきます。型チェック中の計算には実行時の計算と異なる重要な点があります：型の中のいくつかの値はその時点では値がわからない 変数 である場合があります。このような場合、パターンマッチは「詰まり」、例えばパターンマッチによって特定のコンストラクタが選択されるまで、あるいは選択されない限り処理を続行しません。型レベルの計算は一種の部分評価と見なすことができ、プログラム中の十分既知の部分だけが評価され、それ以外の部分は放置されます。
ユニバースパターン
依存型を使う際によくあるパターンは、型システムのサブセットを切り出すことです。例えば、データベースのクエリライブラリは可変長の文字列や固定長の文字列、特定の範囲の数値を返すかもしれませんが、関数やユーザ定義のデータ型、IO アクションなどは決して返しません。型システムのドメイン固有のサブセットの定義は、まず希望する型の構造にマッチするコンストラクタを持つデータ型を定義し、次にこのデータ型からの値を正真正銘の型に解釈する関数を定義することで行えます。コンストラクタは問題の対象の型の コード と呼ばれ、パターン全体は Tarski風ユニバース と呼ばれたり、文脈から Type 3 や Prop のような宇宙を意味するものではないことが明らかな場合は単に ユニバース と呼ばれたりします。
カスタムのユニバースは関心のあるタイプごとにインスタンスを持つ型クラスを定義することの代替手段です。型クラスは拡張可能ですが、拡張性が常に望まれるとは限りません。カスタムユニバースを定義すると、型を直接扱うよりも多くの利点があります：
- 等値性の検査や直列化など、宇宙の あらゆる 型に対して機能する汎用的な操作はコードの再帰によって実装することができます。
- 外部システムが受け入れる型を正確に表現することができ、コードによるデータ型の定義は何が期待されるかを文書化する役割を果たします。
- Leanのパターンマッチの完全性についてのチェッカはコードの取り忘れがないことを保証しますが、一方で型クラスによる解決策ではインスタンスが無いことによるエラーはクライアントコードに先送りにされます。
添字族
データ型は2種類の異なる引数を取ることができます：パラメータ はデータ型の各コンストラクタで同一の値ですが、添字 はそれぞれのコンストラクタで異なる場合があります。与えられた添字の選択によって、データ型のコンストラクタの中で利用可能なものが限定されます。例として、Vect.nil は長さの添字が 0 の場合にのみ利用可能であり、Vect.cons は長さの添字が n に対して n + 1 の場合にのみ利用可能です。通常、パラメータはデータ宣言のコロンの前に名前付き引数として記述され、添字はコロンの後に関数型の引き数として記述されますが、Leanはコロンの後にある引数がパラメータとして使用されるケースを推測することができます。
添字族によってデータ間の複雑な関係を式にすることができ、すべてコンパイラによってチェックされます。データ型の不変量は直接エンコードすることができ、一時的であってもそれを変更することはできません。コンパイラがデータ型の不変量を知ることには大きな利点があります：コンパイラはプログラマにそれらを満たすために何をすべきかを知らせることができるようになります。コンパイル時のエラー、特にアンダースコアに起因するエラーを戦略的に利用することで、プログラミングの思考プロセスの一部をLeanに委ねることが可能になり、プログラマはほかのことに気を配ることができるようになります。
添字族を使って不変量をエンコードすると困難が生じる可能性があります。まず、それぞれの不変量は独自のデータ型を必要とし、そのデータ型は独自のサポートのためのライブラリを必要とします。つまるところ、List.append と Vect.append は互換性が無いということです。これはコードの重複につながります。第二に、添字族を便利に使用するには、型の中で使用される関数の再帰構造が型チェックされるプログラムの再帰構造と一致する必要があります。添字族によるプログラミングはこのように適切な一致を起こせるように手配する技術なのです。一致のミスの回避のために等式の証明に訴えることは可能ですが、これは難しく、難解な正当化がちりばめられたプログラムとなってしまいます。第三に、型チェック中に大きな値に対して複雑なコードを実行すると、コンパイル時の速度低下を招く可能性があります。複雑なプログラムでこのような速度低下を避けるには特殊なテクニックが必要になります。
定義上と命題の同値
Leanの型チェッカは2つの型が交換可能かどうかを、時々ではありますがチェックしなければなりません。型は任意のプログラムを含むことができるため、型チェッカは任意のプログラムの同値性をチェックできなければなりません。しかし、任意のプログラムについて完全に一般的な数学的な同値をチェックする効率的なアルゴリズムは存在しません。これを回避するために、Leanは2つの同値の概念を含んでいます：
- 定義上の同値 とは、同値性の下位の近似であり、基本的にはモジュロ計算と束縛変数の名前の変更の構文表現の同値性をチェックします。Leanは定義上の同値が必要とされる状況では、自動的に定義上の同値をチェックします。
- 命題の同値 はプログラマによって明示的に証明され、明示的に呼び出されなければなりません。その見返りとして、Leanは証明が有効であること、そして呼び出しが正しいゴールを達成することを自動的にチェックします。
この2つの同値の概念はプログラマとLean自身の間の分業を表しています。定義上の同値は単純ですが自動的であり、命題の同値は手動ですが、表現力豊かです。命題の同値は型にはまり込んだプログラムを解きほぐすことに使えます。
しかし、型レベルの計算を解くために命題の同値を多用することは一般的にコードの臭いとなります。これは通常、型の一致がうまく設計されていないことを意味し、型と添字を再設計するか、必要な不変量を強制するために別のテクニックを使用する方が良い考えです。命題の同値がプログラムの仕様を満たしていることを証明するためであったり、部分型の一部として使われる分には違和感はあまりありません。