添字・パラメータ・宇宙レベル

帰納型の添字とパラメータの区別は、単にコンストラクタ間で型への引数が変化するか、もしくはしないかを記述する方法だけにとどまりません。帰納型の引数がパラメータか添字かは、それらの宇宙レベル間の関係を決定するときに重要になります。特に、帰納型はパラメータと同じ宇宙レベルを持つことが可能ですが、添字に対しては宇宙レベルは大きくなければなりません。この制約はLeanがプログラミング言語としてだけでなく、定理証明器としても使用できるようにするために必要です。こうしなければLeanの論理は一貫性が無くなることでしょう。型に対する引数がパラメータと添字のどちらにするべきかを決定する正確なルールと共に、これらのルールを説明するにはエラーメッセージを使って実験するのは良い方法です。

一般的に、帰納型の定義ではパラメータはコロンの前、添字はコロンの後に取られます。パラメータには関数の引数のように名前が与えられる一方、添字には型のみが記述されます。これは Vect の定義で見ることができます：

inductive Vect (α : Type u) : Nat → Type u where
   | nil : Vect α 0
   | cons : α → Vect α n → Vect α (n + 1)

この定義では、α はパラメータで Nat は添字です。パラメータは定義全体を通して参照することができますが（例えば、Vect.cons は第一引数の型として α を使用しています）、それらは常に一貫使用される必要があります。添字は変更されることが期待されるため、データ型の定義の先頭で引数として提供されるのではなく、コンストラクタごとに個別の値が割り当てられます。

パラメータを使った非常にシンプルなデータ型として次の WithParameter を考えます：

inductive WithParameter (α : Type u) : Type u where
  | test : α → WithParameter α

宇宙レベル u は、パラメータと帰納型自体の両方に使用することができ、これはパラメータがデータ型の宇宙レベルを増大させないことを示します。同様に、複数のパラメータがある場合、帰納型はどちらか大きい方の宇宙レベルを受け取ります：

inductive WithTwoParameters (α : Type u) (β : Type v) : Type (max u v) where
  | test : α → β → WithTwoParameters α β

パラメータはデータ型の宇宙レベルを増加させないため、より便利に扱うことができます。Leanは添字のように（コロンの後に）記述されるがパラメータのように用いられる引数を識別し、それらをパラメータに変えようとします：以下の帰納的データ型はどちらもコロンの後にパラメータが記述されています：

inductive WithParameterAfterColon : Type u → Type u where
  | test : α → WithParameterAfterColon α

inductive WithParameterAfterColon2 : Type u → Type u where
  | test1 : α → WithParameterAfterColon2 α
  | test2 : WithParameterAfterColon2 α

最初のデータ型の宣言でパラメータに名前が付けられていない場合、一貫して使用される限り各コンストラクタで異なる名前を使用しても良いです。次の宣言はLeanに受け入れられます：

inductive WithParameterAfterColonDifferentNames : Type u → Type u where
  | test1 : α → WithParameterAfterColonDifferentNames α
  | test2 : β → WithParameterAfterColonDifferentNames β

しかし、この柔軟性は、パラメータの名前を明示的に宣言するデータ型には適用されません：

inductive WithParameterBeforeColonDifferentNames (α : Type u) : Type u where
  | test1 : α → WithParameterBeforeColonDifferentNames α
  | test2 : β → WithParameterBeforeColonDifferentNames β

inductive datatype parameter mismatch
  β
expected
  α

同様に、添字に名前を付けようとするとエラーになります：

inductive WithNamedIndex (α : Type u) : Type (u + 1) where
  | test1 : WithNamedIndex α
  | test2 : WithNamedIndex α → WithNamedIndex α → WithNamedIndex (α × α)

inductive datatype parameter mismatch
  α × α
expected
  α

適切な宇宙レベルを用い添字をコロンの後ろに置くことで、Leanに許容される宣言となります：

inductive WithIndex : Type u → Type (u + 1) where
  | test1 : WithIndex α
  | test2 : WithIndex α → WithIndex α → WithIndex (α × α)

帰納型の宣言においてコロンの後にある引数がすべてのコンストラクタで一貫して使用されていればパラメータであるとLeanが判断できる場合もありますが、それでもすべてのパラメータはすべての添字より前に来る必要があります。添字の後にパラメータを置こうとすると、引数自体が添字と見なされ、データ型の宇宙レベルを上げる必要があります：

inductive ParamAfterIndex : Nat → Type u → Type u where
  | test1 : ParamAfterIndex 0 γ
  | test2 : ParamAfterIndex n γ → ParamAfterIndex k γ → ParamAfterIndex (n + k) γ

invalid universe level in constructor 'ParamAfterIndex.test1', parameter 'γ' has type
  Type u
at universe level
  u+2
it must be smaller than or equal to the inductive datatype universe level
  u+1

パラメータは型である必要はありません。次の例は Nat のような通常のデータ型をパラメータとして使用できることを示しています：

inductive NatParam (n : Nat) : Nat → Type u where
  | five : NatParam 4 5

inductive datatype parameter mismatch
  4
expected
  n

エラーメッセージの通りに n を使用すると、宣言が受理されます：

inductive NatParam (n : Nat) : Nat → Type u where
  | five : NatParam n 5

これらの実験から何が結論付けられるでしょうか？パラメータと添字のルールは以下の通りです：

1. パラメータは各コンストラクタの型で同じものを使用しなければなりません。
2. すべてのパラメータはすべての添字より前に来なければなりません。
3. 定義されるデータ型の宇宙レベルは最も低くても最大のパラメータのものと同じ大きさでなければならず、最大の添字より大きくなければなりません。
4. コロンの前に書かれた名前付きの引数は常にパラメータであり、コロンの後ろに書かれた引数は通常は添字です。コロンの後ろにある引数が一貫して使われ、かつ添字より後ろに来ないように使われている場合、それらをパラメータに変更するよう判断できます。

どれがパラメータであるかわからない場合は、Leanのコマンド #print を使ってデータ型の引き数のうちいくつがパラメータなのかをチェックすることができます。例えば、Vect の場合、パラメータ数が1であることが示されます：

#print Vect

inductive Vect.{u} : Type u → Nat → Type u
number of parameters: 1
constructors:
Vect.nil : {α : Type u} → Vect α 0
Vect.cons : {α : Type u} → {n : Nat} → α → Vect α n → Vect α (n + 1)

データ型の引き数の順番を決める際に、どの引数をパラメータにし、どの引数を添字にするかを考えることには価値があります。可能な限り多くの引数をパラメータにすることは宇宙レベルを制御し、複雑なプログラムの型チェックを容易にすることができます。これを可能にする1つの方法は、引数リストにおいてすべてのパラメータがすべての添字の前に来るようにすることです。

さらに、Leanはコロンの後にある引数がなんであろうともその使われ方からパラメータであることを判断することができますが、パラメータを明示的な名前で書くことは良い考え方です。こうすることで読み手に意図が明確に伝わ子、コンストラクタ間で引数が誤って一貫しない使われ方をした際にLeanがエラーを報告するようになります。