宇宙
議論をシンプルにするために、本書ではこれまでLeanの重要な特徴である 宇宙 (universe)について触れてきませんでした。宇宙とは型を分類する型のことです。宇宙の例としては Type
と Prop
の2つが良く知られています。Type
は通常の型、例えば Nat
・String
・Int → String × Char
・IO Unit
などを分類します。Prop
は "nisse" = "elf"
や 3 > 2
のような真偽を表す命題を分類します。Prop
の型は Type
です:
#check Prop
Prop : Type
技術的な理由から、これら2つより上の宇宙が必要です。というのも Type
はそれ自身を Type
とすることができないからです。仮に出来てしまうと、論理的なパラドックスが構築できてしまい、Leanの定理証明器としての有用性を損なうことになります。
これに対する形式的な議論は ジラールのパラドックス (Girard's Paradox)として知られています。これは初期の集合論の矛盾を示すために用いられた ラッセルのパラドックス (Russell's Paradox)としてよく知られているパラドックスと関連しています。初期の集合論では集合はある性質によって定義することができます。例えば、全ての赤いものの集合、全ての果物の集合、全ての自然数の集合や、さらに全ての集合の集合なんてものまでが定義されます。ある集合が与えられると、ある要素がその集合に含まれているかどうかを問うことができます。例えば、「青い鳥」は「全ての赤いものの集合」には含まれませんが、「全ての赤いものの集合」は「全ての集合の集合」に含まれます。実は「全ての集合の集合」はそれ自身をも含んでいます。
では「全ての『自分自身を含まない集合』の集合」は何を含むでしょうか?「全ての赤いものの集合」はそれ自身は赤くないため、先ほどの集合に含まれます。「全ての集合の集合」はそれ自身を含むので、先ほどの集合に含まれません。しかし、「全ての『自分自身を含まない集合』の集合」はそれ自身を含むでしょうか?もし自分自身を含んでいるのなら、「全ての『自分自身を含まない集合』の集合」には含まれないことになります。しかし、もし自分自身を含んでいないのなら、「全ての『自分自身を含まない集合』の集合」に含まれなければなりません。
これは矛盾であるため、最初の仮定のうち何かがが間違っていたことを示しています。特に、任意の性質を与えることで集合を構成できるようにするのは強力すぎます。これ以降の集合論では、このパラドックスを取り除くために集合の形成を制限しています。
依存型理論において Type
に Type
を割り当てるようにすると、関連したパラドックスを構築することができます。Leanが一貫した論理的基礎を持ち、数学の道具として使えることを保証するためには、Type
はほかの型を持つ必要があります。この型を Type 1
と呼びます:
#check Type
Type : Type 1
同じように、 Type 1
は Type 2
型を、
Type 2
は Type 3
型を、
Type 3
は Type 4
型をそれぞれ持ち、これが続いていきます。
関数型は、引数の型と戻り値の型の両方を含むことができる最小の宇宙になります。つまり、Nat → Nat
は Type
型に、Type → Type
は Type 1
型に、Type 1 → Type 2
は Type 3
型になります。
このルールには1つ例外があります。関数の戻り値の型が Prop
である場合、引数が Type
や Type 1
のような大きな宇宙であってもこれらの関数の型はすべて Prop
に含まれます。特に、通常の型の値に対する述語も Prop
に含まれることになります。例えば、(n : Nat) → n = n + 0
は Nat
からその値自体と0を足したものが等しいという根拠への関数を表します。Nat
は Type
に含まれていますが、このルールによりこの関数の型は Prop
に含まれます。同様に、Type
は Type 1
に含まれているにも関わらず、関数型 Type → 2 + 2 = 4
もまた Prop
に含まれます。
ユーザ定義型
構造体と帰納的データ型は属する宇宙を指定して宣言することができます。そして、それぞれのデータ型がそれ自身の型を含まないほど十分な大きさの宇宙に存在することでパラドックスを回避しているかどうかをLeanはチェックします。例えば、以下の宣言では MyList
は Type
に属すると宣言されており、その型引数 α
も Type
に属すると宣言されています:
inductive MyList (α : Type) : Type where
| nil : MyList α
| cons : α → MyList α → MyList α
MyList
自体は Type → Type
型です。これは引数が Type
であることからこの関数型は Type 1
となり、型自体を格納するために使用することができないことを意味します:
def myListOfNat : MyList Type :=
.cons Nat .nil
application type mismatch
MyList Type
argument
Type
has type
Type 1 : Type 2
but is expected to have type
Type : Type 1
MyList
を更新して、その引数を Type 1
にすると、今度はLeanによって定義が拒否されます:
inductive MyList (α : Type 1) : Type where
| nil : MyList α
| cons : α → MyList α → MyList α
invalid universe level in constructor 'MyList.cons', parameter has type
α
at universe level
2
it must be smaller than or equal to the inductive datatype universe level
1
このエラーは α
型を持つ cons
の引数が MyList
よりも大きな宇宙であるために発生します。MyList
自身を Type 1
に配置することでこの問題は解決されますが、その代償として MyList
自身が Type
であることを期待するコンテキストで使用する場合には不便になります。
あるデータ型が許容されるかどうかを規定する具体的な少々複雑です。一般的に言えば、データ型を引数の中で最大の宇宙と同じところから始めることが最も簡単です。もしLeanがその定義を拒否したら、宇宙のレベルを1つあげます。これで大体はうまくいきます。
宇宙多相
データ型を特定の宇宙で定義すると、コードが重複する可能性があります。MyList
を Type → Type
と定めることは、型自体のリストには使えないことを意味します。一方で Type 1 → Type 1
と定めることは型のリストのリストには使えないことを意味します。この調子でデータ型をコピペして Type
・Type 1
・Type 2
……のそれぞれの定義を作成するのではなく、宇宙多相 (universe polymorphism)と呼ばれる機能を使用することで、これらの宇宙のいずれにでもインスタンス化できる単一の定義を記述することができます。
通常の多相型は、定義中の型を表すために変数を使用します。これによって、Leanはこの変数に異なる値を埋め込めるようになり、これらの定義が様々な型で使用できるようになります。同様に、宇宙多相は定義内の宇宙を変数で表すことができ、Leanはこの変数に異なる宇宙を埋め込めるようになり、様々な宇宙で使用できるようにします。型の変数が慣例的にギリシャ文字で命名されるのに対して、宇宙の引数は u
・v
・w
と命名されます。
この MyList
の定義では、特定の宇宙レベルを指定するのではなく、任意のレベルを表す変数 u
を使用します。Type
を使用したデータ型の場合、u
は 0
となり、 Type 3
を使用した場合、u
は 3
となります:
inductive MyList (α : Type u) : Type u where
| nil : MyList α
| cons : α → MyList α → MyList α
この定義により、MyList
の同じ定義を使って、実際の自然数と自然数型そのもののの両方をそれぞれ格納できます:
def myListOfNumbers : MyList Nat :=
.cons 0 (.cons 1 .nil)
def myListOfNat : MyList Type :=
.cons Nat .nil
さらに MyList
自体も格納できます:
def myListOfList : MyList (Type → Type) :=
.cons MyList .nil
これは論理的なパラドックスの記述を可能にしているように思えます。というのも宇宙システムの要点は自己言及的な型の除外だったからです。しかしこの裏では、MyList
の宇宙レベルの引数が出現している MyList
のそれぞれの個所で与えられています。要するに、MyList
の宇宙多相な定義は各レベルでデータ型の コピー を作成し、レベルの引数はどのコピーを使用するかを選択しているのです。これらのレベルの引数はドットと波括弧で記述します。したがって、MyList.{0} : Type → Type
と、MyList.{1} : Type 1 → Type 1
、MyList.{2} : Type 2 → Type 2
となります。
レベルの明示的に書くと、先ほどの例は以下のようになります:
def myListOfNumbers : MyList.{0} Nat :=
.cons 0 (.cons 1 .nil)
def myListOfNat : MyList.{1} Type :=
.cons Nat .nil
def myListOfList : MyList.{1} (Type → Type) :=
.cons MyList.{0} .nil
宇宙多相の定義が引数として複数の型を取る場合、最大限に柔軟性を上げるために各引数に独自のレベル変数を与えると良いでしょう。例えば、1つのレベル引数を持つバージョンの Sum
は次のように書くことができます:
inductive Sum (α : Type u) (β : Type u) : Type u where
| inl : α → Sum α β
| inr : β → Sum α β
この定義は複数のレベルで使うことができます:
def stringOrNat : Sum String Nat := .inl "hello"
def typeOrType : Sum Type Type := .inr Nat
しかし、この場合両方の引数が同じ宇宙に存在している必要があります:
def stringOrType : Sum String Type := .inr Nat
application type mismatch
Sum String Type
argument
Type
has type
Type 1 : Type 2
but is expected to have type
Type : Type 1
このデータ型は、2つの型引数の宇宙レベルに異なる変数を割り当て、出来上がるデータ型がこの2つの型引数のうち大きいほうのものになるように宣言することで、より柔軟なものにすることができます:
inductive Sum (α : Type u) (β : Type v) : Type (max u v) where
| inl : α → Sum α β
| inr : β → Sum α β
これにより、Sum
を異なる宇宙からの引数で使うことができます:
def stringOrType : Sum String Type := .inr Nat
Leanにおいて、宇宙レベルが期待される位置では以下すべての指定が認められています:
0
や1
などの具体的なレベルu
やv
などのレベルを表す変数- 2つのレベルに
max
を適用することで記述される大きい方のレベル + 1
で記述されるレベルの増加
宇宙多相的な定義の記述
ここまで本書で定義されたデータ型はすべて Type
であり、データとして最小の宇宙でした。List
や Sum
などのLeanの標準ライブラリの多相データ型を紹介する場合も、本書ではそれらの宇宙多相ではないバージョンを作成しました。実際には型レベルと型レベルでないプログラムの間でコードを再利用できるように宇宙多相を使用しています。
宇宙多相型を書く際には一般的なガイドラインがあります。まず、独立した型の引数は異なる宇宙変数を持つべきです。これにより多相定義をより多様な引数で使用できるようになり、コードの再利用の可能性が高まります。第二に、型全体は通常すべての宇宙変数の最大値以上になります。まずは小さい方から試してみてください。最後に、新しい型をできるだけ小さな宇宙に置くことでコンテキストによってはより柔軟に使用できるようになります。Nat
や String
のような多相でない型は Type 0
に直接置くと良いでしょう。
Prop
と多相
Type
や Type 1
などがプログラムやデータを分類する型を記述しているように、Prop
は論理命題を分類します。Prop
の型はある文が真であることの説得力のある根拠となるものを記述します。命題は多くの点で通常の型と似ています:どちらも帰納的に宣言でき、コンストラクタを持つことができ、関数を引数として取ることができます。しかし、データ型とは異なり、文が真であることを証明するためには どの 根拠が提供されるかは一般的には重要ではなく、根拠が提供されているという こと だけが重要です。一方でプログラムにおいては、例えばそれが Nat
を返すという事実だけでなく、それが 正しい Nat
であることが非常に重要です。
Prop
は宇宙の階層の一番下にあり、Prop
の型は Type
です。これは Prop
が Nat
と同じ理由で List
に引数として与えられることを意味します。命題のリストは List Prop
型を持ちます:
def someTruePropositions : List Prop := [
1 + 1 = 2,
"Hello, " ++ "world!" = "Hello, world!"
]
宇宙の引数を埋めることで、Prop
が Type
であることが明示的に示されます:
def someTruePropositions : List.{0} Prop := [
1 + 1 = 2,
"Hello, " ++ "world!" = "Hello, world!"
]
裏側では、Prop
と Type
は Sort
という1つの階層に統合されています。Prop
は Sort 0
と同じであり、Type 0
は Sort 1
、Type 1
は Sort 2
です。実は、Type u
は Sort (u+1)
と同じです。通常Leanでプログラムを書く際には関係ありませんが、ときどきエラーメッセージで出てくることがあります。そしてこれが CoeSort
クラスの名前を説明します。さらに、Prop
を Sort 0
とすることで、新たな宇宙演算子が使えるようになります。imax u v
と書かれる宇宙レベルは、v
が 0
の場合は 0
となり、それ以外では u
と v
の大きい方となります。これは Sort
と合わせることで、Prop
を返す関数の特別なルールを、Prop
と Type
の宇宙間で可能な限り取りまわせるコードを書くときに使用することができます。
多相の実践
本書の残りの部分では、多相データ型、構造体、クラスの定義はLeanの標準ライブラリと整合性をとるために、宇宙多相を使用します。これにより、Functor
と Applicative
、Monad
の各クラスは実際の定義と完全に一致するようになります。