Dependent Types and Universes

Use values to express types and propositions more precisely.

17.1 Types can depend on values

An ordinary List(A) describes its element type A, but its type does not include its length. Dependent types can change shape according to a value. Tauto's a = b is already a proposition depending on the values a and b.

import std::Base

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

// The proposition depends on the supplied natural number.

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

The theorem's specific result equality depends on its argument n. Unlike a function that merely returns Bool, type checking verifies evidence of the proposition.

17.2 Prop and Type

Prop is the world of propositions to be proved; Type is the world of data and types. Higher universes such as Type1 and Type2 are used when needed. You can also define types parameterized by a universe level.

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)
}

// Instantiate a universe-polymorphic box at numeric universe level zero.

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

ok      UBox@0
ok      small_box

u: Level is a universe-level parameter, used with a numeric level. Universe polymorphism has restrictions; do not assume unrestricted inference of free symbolic levels.

17.3 Stronger types express stronger specifications

The more conditions a type expresses, the more errors checking can exclude. However, complex types also take more effort to read and understand. When learning Tauto, start by stating the intended property as a simple proposition, then prove only the properties you need.

Exercise 17.1: Why are n = n and n = 0 very different claims?