依存型と型の宇宙

値を使って、型や命題を細かく表現します。

17.1 型が値に依存する

普通の List(A) では、要素の型 A は分かりますが、リストの長さは型に含まれません。依存型を使うと、値に応じて型の形を変えられます。Tauto の a = b も、a と b という値に依存した命題です。

import std::Base

theorem equal_to_self(n: Nat): n = n {
  Refl
}

✓ theorem equal_to_self : ∀ n: Nat. n = n

この定理の結果型は、引数 n によって具体的な等式が変わります。Bool を返すだけの関数と違って、型の検査が、命題の証拠を確かめます。

17.2 Prop と Type

Prop は証明すべき命題の世界、Type はデータや型の世界です。必要に応じて、Type1、Type2 などの高い宇宙が使われます。宇宙のレベルを引数に取る型も書けます。

import std::Base

inductive UBox(u: Level, A: Type(u)): Type(u) {
  ubox(value: A): UBox(u, A)
}

theorem small_box(): UBox(0, Nat) {
  ubox(0, Nat, 3)
}

✓ UBox
✓ theorem small_box : UBox@0(Nat)

ok      UBox@0
ok      small_box

u: Level は宇宙の高さを表す引数で、数値の宇宙レベルを指定して使います。宇宙多相には制限があり、自由な記号レベルの推論を前提にしてはいけません。

17.3 型の強さは仕様の強さ

型にたくさんの条件を押し込むほど、検査で排除できる誤りも増えます。しかし型が複雑になると、「何を保証するための型か」を読む労力も増えます。Tauto では、意図した性質をまず素朴な命題で書いて、必要な性質だけを証明する学び方をおすすめします。

演習 17.1：n = n と n = 0 は、なぜまったく違う主張なのでしょうか。