宇宙

議論をシンプルにするために、本書ではこれまで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 の各クラスは実際の定義と完全に一致するようになります。

Functional Programming in Lean 日本語訳

宇宙

ユーザ定義型

宇宙多相

宇宙多相的な定義の記述

Prop と多相

多相の実践

`Prop` と多相