Dependent Types: Pi and Sigma as Generalised Function and Pair

In the simply typed lambda calculus the type of a function is fixed: A → B says that inputs of type A produce outputs of type B, and B cannot mention the input. That restriction is what makes type checking a matter of matching syntax trees. Dependent types remove it. A function’s result type may mention the argument’s value, so (n : Nat) → Vec A n is a type whose inhabitants produce a vector of a length determined by the input.

Pi: function types whose codomain depends

The dependent function type, written (x : A) → B x or Π (x : A). B x, generalises the arrow. When B does not mention x, the two coincide, and most systems treat A → B as notation for a Pi type with an unused binder.

The formation rule requires that B be a type whenever x ranges over A. That condition is not decorative. It means the type former B is itself a function from values to types, so the language needs a way to compute types, and computing types is the same operation as computing terms. A type-level function such as Vec A : Nat → Type is a term of a function type whose codomain is a universe, and it reduces by the same rules as any other term.

Introduction is abstraction, as in the simply typed case, and elimination is application. What changes is the typing rule for application: the result type is obtained by substituting the argument into the codomain. If f : (n : Nat) → Vec Bool n and k : Nat, then f k : Vec Bool k. The type of the application is not known until the argument is known, and if the argument is a computation rather than a literal, the checker must evaluate it.

That evaluation is the source of most of the implementation complexity. Two types are considered equal when they have the same normal form, so checking f (2 + 2) against Vec Bool 4 requires reducing 2 + 2. The check is therefore an interpreter run inside the type checker, and its termination is not optional: a non-terminating type-level computation would hang the checker. This is why total languages insist that every definable function terminates, a constraint examined in Termination Checking and the Price of Consistency.

Sigma: pairs whose second component depends

The dependent pair type, Σ (x : A). B x, generalises conjunction and the existential quantifier at once. An inhabitant is a pair (a , b) where a : A and b : B a. The first projection returns the witness, the second returns the evidence, and the type of the second projection depends on the first component’s value.

total : Σ[ n ∈ ℕ ] Vec Bool n
total = 3 , true ∷ false ∷ true ∷ []

The type of the pair is not fixed in advance: the second component’s type depends on the value of the first, so the pair is well typed only when the vector’s length matches the number written.

The type alone does not say whether the pair is being used as data or as a proof. In a language with a separate universe of propositions, the same shape appears twice: a dependent pair former in the universe of types, whose components are relevant at runtime, and an existential quantifier in the universe of propositions, whose second component is erased. The distinction matters for extraction, because the erased version compiles to a single value while the relevant version compiles to two.

The eliminator is the interesting part. For a non-dependent pair, the eliminator is projection, and the computation rules are fst (a, b) = a and snd (a, b) = b. For a dependent pair, the motive of the eliminator may mention the pair itself, so the eliminator cannot simply project: it must be given a function that consumes both components together. Projections can be derived from the eliminator when the motive does not depend on the second component, and they cannot when it does.

Indexed families and the arithmetic that leaks into types

The canonical example is a list indexed by its length.

data Vec (A : Set) : ℕ → Set where
  []  : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

append : ∀ {A n m} → Vec A n → Vec A m → Vec A (n + m)
append []        ys = ys
append (x ∷ xs)  ys = x ∷ append xs ys

Two details in that definition carry the whole story. The type Vec A : ℕ → Set is a family, not a single type, so each length gives a different type and Vec A 3 and Vec A 4 are not interchangeable. And the type of append mentions n + m, so the checker must know how addition behaves on the specific indices involved.

The second clause typechecks because suc n + m reduces to suc (n + m) by the definition of addition, which recurses on its first argument. The base clause typechecks because zero + m reduces to m. Had the type been written with the arguments in the other order, as m + n, the base case would require m + zero = m, which does not hold by computation for a variable m: the recursion is on the first argument, so m + zero is stuck. The proof obligation is real, and it is discharged by a propositional equality rather than by reduction, which is the distinction taken up in Definitional and Propositional Equality.

The consequence for library design is significant. Index arithmetic determines which programs typecheck without proof, and the choice between n + m and m + n in a signature is a choice about how much proving the user must do. This is why dependently typed libraries spend effort on lemmas that rewrite indices, and why the orientation of those lemmas is not arbitrary.

Formation, and why the universe matters

A dependent type former is a function into a universe, so the universe must be able to contain it. If Nat → Set were itself an element of Set, the system would be inconsistent by Girard’s argument, and no total language permits it. The standard solution is a hierarchy: Set is an element of Set₁, which is an element of Set₂, and so on, with each former landing one level up from its components.

The hierarchy is usually implicit. A checker infers the levels, and the user sees a single Set except when a definition forces a higher level and the inference fails. When it fails the error is typically about a universe constraint rather than about the program’s logic, and resolving it means restructuring the definition so that the offending type former does not quantify over the universe it lives in.

Predicativity is what keeps the hierarchy from collapsing. In an impredicative universe a type can quantify over all types including itself, and a single level suffices. The calculus of constructions combines an impredicative type of propositions with a predicative hierarchy of types, so impredicative quantification stays at the level of propositions and does not yield a type of all types.

What dependent types cost

Three costs are structural rather than incidental.

Type checking is evaluation. Since types can compute, checking requires a normaliser, and the normaliser’s performance is the checker’s performance. Practical systems use the technique described in Normalisation by Evaluation for Conversion Checking rather than substitution, because substitution under binders copies the argument once per occurrence and repeatedly renames bound variables; evaluation into a domain passes the argument as a value and never copies syntax.

Inference is undecidable in general. For the simply typed calculus, type inference without annotations is decidable. For dependent types it is not, and systems require annotations on binders and on functions whose type cannot be reconstructed. Elaborators that accept unannotated binders recover them by higher-order unification, which searches for a substitution making two types definitionally equal; that search is undecidable in general, so it is bounded by heuristics and by the order in which constraints are attempted. The elaborator fills in the rest, and its behaviour is where most user-visible surprises originate, as discussed in Elaboration: Filling in What the Program Did Not Say.

Equality of types is not syntactic. Two types that are equal by computation are interchangeable, so a checker cannot hash types and compare. It must compare normal forms, and in the presence of functions in types it must compare under binders, which is exactly where naive comparison breaks down.

None of these costs is avoidable, and each is a consequence of the same decision: allowing values to appear inside types.

Why the generality is worth it

The payoff is that specifications become types. A sorting function can be given the type that says its output is ordered and is a permutation of its input, and a caller that depends on those properties needs no runtime check. A protocol handler can be indexed by the state of the protocol, so that sending a message in the wrong state is a type error rather than a runtime error.

The properties are not free. Every index in a type is a proof obligation somewhere, and the obligations accumulate along the boundary between the indexed and unindexed parts of a program. The usual engineering response is to keep indices at the interfaces and erase them internally, which requires the compiler to determine which parts of a term are relevant to computation and which are merely evidence. That determination is a property of the type, not of the syntax, and it is the reason dependent types are a design constraint on the whole language rather than a library feature.