3. 型システム（The Type System）🔗

項（term）は式（expression）としても知られ、Lean のコア言語における意味の基本単位です。これらはエラボレータによってユーザが書いた構文から生成されます。Lean の型システムは項をその型（type）に関連付けます。型は集合を表し、項は集合の個々の要素を表すと考えることができます。Lean の型理論のルールに従った型を持つ項は well-typed と言います。well-typed である項のみが意味を持ちます。

項は依存型付きラムダ計算です；関数抽象・適用・変数・let 束縛を含みます。束縛変数に加えて、項言語の変数はコンストラクタ・型コンストラクタ・再帰子・定義された定数（defined constant）・不透明な定数を参照することができます。コンストラクタ・型コンストラクタ・再帰子・不透明な定数は置換の対象にはなりませんが、定義された定数はその定義に置き換えることができます。

導出（derivation）は使用される正確な推論規則を明示的に示すことで項の well-typed さを示します。暗黙的に、well-typed な項は、その well-typed であることを示す導出の代わりにすることができます。Lean の型理論は well-typed な項から導出を再構築することができるほど十分に明示的であり、完全な導出を保存することで発生するオーバーヘッドを大幅に削減することができるにもかかわらず、この理論は現代の研究数学を表現するに足る表現力を保ちます。これは、証明項が定理の真理について十分な根拠となり、独立した検証が可能であることを意味します。

型を持つことに加えて、項は definitional equality訳注：形容詞的に用いることもあり、その場合は definitionally equal と記述されます。によっても関連付けられます。これは機械的にチェック可能な関係であり、計算動作に応じて項を等しくします。definitional equality には簡約（reduction）の以下の形式が含まれます：

β (beta): 束縛された変数への置換によって、引数に関数抽象を適用する

δ (delta): 定義された定数の出現箇所を定義の値で置き換える

ι (iota): コンストラクタをターゲットとする再帰子の簡約（原始再帰）

ζ (zeta): let 束縛変数を定義された値に置き換える

すべての可能な簡約が行われた項は 正規形 （normal form）となります。

definitional equality には関数と単一コンストラクタの帰納型についてのη同値が含まれます。つまり、 fun x => f x は f に definitionally equal であり、 S がフィールド f1 と f2 を持つ構造体である時には S.mk x.f1 x.f2 は x と definitionally equal です。また証明の irrelevance も特徴づけ、同じ命題の2つの証明は definitionally equal です。これは反射的・対称的・合同的です。

definitional equality は変換にも用いられます：2つの項が definitionally equal であり、ある項がその一方を型として持つ場合、その項はもう一方の項も型として持ちます。definitional equality は簡約を含むため、データに対する計算から型が生じることがあります。

型の計算

自然数を渡すと、関数 LengthList は正確にその数のエントリを持つリストに対応する型を計算します：

def LengthList (α : Type u) : Nat → Type u
  | 0 => PUnit
  | n + 1 => α × LengthList α n

Lean のタプルは右側にネストしているため、複数のネストした括弧は必要ありません：

example : LengthList Int 0 := ()

example : LengthList String 2 :=
  ("Hello", "there", ())

長さが項目数と一致しない場合、計算された型はその項と一致しません：

example : LengthList String 5 :=
  ("Wrong", "number", application type mismatch
  ("number", ())
argument
  ()
has type
  Unit : Type
but is expected to have type
  LengthList String 3 : Type())

application type mismatch
  ("number", ())
argument
  ()
has type
  Unit : Type
but is expected to have type
  LengthList String 3 : Type

Lean の基本型は宇宙・関数型・帰納型の型コンストラクタです。定義された定数・再帰子の適用・関数適用・ axioms ・不透明な定数は、これらが任意の他の型の項を生じさせることができるのと同様に、さらに型を与えることができます。