13. Dependent Types: Π and Σ

Working System

This chapter uses reusable code from book/advanced/dependent_codes.py.

We model dependent types semantically using type codes and a bounded membership checker dep.is_in. For function types (Π-types), membership is tested on a finite sample of inputs, controlled by a depth parameter.

This is an executable model for learning, not a full dependent type checker.

13. Dependent Types: Π and Σ#

Goal. Extend propositions-as-types with dependent types, and use runnable examples to see how Π-types and Σ-types generalize implication and conjunction.

You will learn

  • The idea of a dependent type \(\Pi(x:A).B(x)\) as a function whose result type depends on the input

  • The idea of a dependent type \(\Sigma(x:A).B(x)\) as a pair of data plus a certificate

  • How \(\Pi\) behaves like universal quantification (\(\forall\)) and \(\Sigma\) like existential quantification (\(\exists\))

  • How to encode simple specifications (like parity and vector length) using \(\Pi/\Sigma\)

Roadmap#

  1. Give the semantic meaning of codes, \(\Pi\), and \(\Sigma\).

  2. Implement and check basic inhabitants (evenness, equality-singletons).

  3. Add finite index types (Fin(n)) and length-indexed vectors (Vec(A,n)).

  4. Build dependent functions like head and map that preserve invariants.

Mathematical Background#

This chapter uses a semantic view: each code \(A\) denotes a set of Python values \(\den{A}\).

Definition (Semantic Interpretation)

A code \(A\) denotes a set \(\den{A}\) of values. We write

\[ v \in \den{A} \]

to mean that \(v\) is a value of type \(A\).

The two dependent type formers are interpreted as follows.

Definition (Π and Σ)

For codes \(A\) and a family \(B(x)\), define

\[ \den{\Pi(x:A).B(x)} := \{ f \mid \forall a \in \den{A},\ f(a) \in \den{B(a)} \}, \]
\[ \den{\Sigma(x:A).B(x)} := \{ (a,b) \mid a \in \den{A},\ b \in \den{B(a)} \}. \]

Logical reading:

  • \(\Pi(x:A).B(x)\) behaves like \(\forall x\!:\!A.\ B(x)\).

  • \(\Sigma(x:A).B(x)\) behaves like \(\exists x\!:\!A.\ B(x)\).

Remark (Bounded Checking)

Our function-membership checker cannot quantify over infinite domains. dep.is_in(f, PiCode(A, B)) tests \(f(a) \in \den{B(a)}\) for a finite sample of inputs \(a \in \den{A}\).

This makes the examples runnable, but it is not a substitute for a real dependent type checker.

from pathlib import Path
import sys

book_root = Path.cwd()
if not (book_root / "advanced").exists():
    book_root = book_root.parent
if str(book_root) not in sys.path:
    sys.path.insert(0, str(book_root))

from advanced import dependent_codes as dep

Universe of Type Codes#

We start with a small universe of codes:

  • NatCode() for \(\mathbb{N}\) (Python ints \(\ge 0\))

  • BoolCode() for booleans

  • UnitCode() for a singleton type (inhabited by ())

  • EmptyCode() for an uninhabited type

We also introduce two finite/indexed codes:

  • FinCode(n) for \(\{0,\dots,n-1\}\)

  • VecCode(A,n) for vectors of length \(n\) with elements in \(A\)

These two are useful because they let us write specifications like:

\[ \Sigma(n:\mathbb{N}).\mathrm{Vec}(\mathrm{Bool}, n) \]

which reads: there exists a length \(n\) and a boolean vector of that length.

Nat = dep.NatCode()
Bool = dep.BoolCode()
Unit = dep.UnitCode()
Empty = dep.EmptyCode()

print("() in Unit:", dep.is_in((), Unit))
print("0 in Empty:", dep.is_in(0, Empty))

Fin5 = dep.FinCode(5)
print("3 in Fin(5):", dep.is_in(3, Fin5))
print("7 in Fin(5):", dep.is_in(7, Fin5))
print("sample Fin(5):", dep.sample_values(Fin5, depth=10))

VecB3 = dep.VecCode(Bool, 3)
print("[T,F,T] in Vec(Bool,3):", dep.is_in([True, False, True], VecB3))
print("sample Vec(Bool,3):", dep.sample_values(VecB3, depth=3))

() in Unit: True
0 in Empty: False
3 in Fin(5): True
7 in Fin(5): False
sample Fin(5): [0, 1, 2, 3, 4]
[T,F,T] in Vec(Bool,3): True
sample Vec(Bool,3): [(False, False, False), (True, True, True), (False, True, False)]

Π-Types as Dependent Functions (\(\forall\))#

A Π-type packages the idea of a function that works uniformly for all inputs.

A classic dependent example is a function that produces an evenness witness for \(2n\):

\[ \Pi(n:\mathbb{N}).\ \mathrm{Even}(2n). \]

In our code universe, EvenProofCode(m) is inhabited by the half \(k\) such that \(m = 2k\). So a witness for Even(2n) is just n.

double_even_type = dep.PiCode(Nat, lambda n: dep.EvenProofCode(2 * n))

double_even = lambda n: n
bad_double_even = lambda n: n + 1

print("double_even inhabits Π:", dep.is_in(double_even, double_even_type, depth=8))
print("bad_double_even rejected:", dep.is_in(bad_double_even, double_even_type, depth=8))

double_even inhabits Π: True
bad_double_even rejected: False

Σ-Types as Data + Certificate (\(\exists\))#

A Σ-type is a dependent pair: a value together with evidence about it.

For example, the proposition “there exists an even number” can be written as

\[ \Sigma(n:\mathbb{N}).\ \mathrm{Even}(n). \]

An inhabitant is a pair (n, k) where \(n = 2k\).

exists_even = dep.SigmaCode(Nat, lambda n: dep.EvenProofCode(n))

w1 = (4, 2)  # 4 = 2*2
w2 = (6, 3)  # 6 = 2*3
bad = (6, 4)  # claims 6 = 2*4

print("w1 inhabits Σ(n).Even(n):", dep.is_in(w1, exists_even, depth=8))
print("w2 inhabits Σ(n).Even(n):", dep.is_in(w2, exists_even, depth=8))
print("bad rejected:", dep.is_in(bad, exists_even, depth=8))

w1 inhabits Σ(n).Even(n): True
w2 inhabits Σ(n).Even(n): True
bad rejected: False

Example: Length-Indexed Vectors and Finite Index Types#

In dependent type theory, a length-indexed vector is a family of types

\[ \mathrm{Vec}(A,n) : \mathbb{N} \to \mathsf{Type}. \]

In our toy model:

  • VecCode(A,n) is inhabited by lists/tuples of length n whose elements inhabit A.

  • FinCode(n) is inhabited by indices \(0,\dots,n-1\).

This is already enough to state useful specifications.

Example (existential vector):

\[ \Sigma(n:\mathbb{N}).\ \mathrm{Vec}(\mathrm{Bool}, n). \]
VecBool = lambda n: dep.VecCode(Bool, n)
exists_vec = dep.SigmaCode(Nat, lambda n: VecBool(n))

w = (3, [True, False, True])

print("w inhabits Σ(n).Vec(Bool,n):", dep.is_in(w, exists_vec, depth=6))

w inhabits Σ(n).Vec(Bool,n): True

Dependent Functions Preserve Invariants#

Dependent types shine when a function’s output type tracks an invariant.

Example: head#

If a vector has length \(n+1\), taking its head is always safe:

\[ \Pi(n:\mathbb{N}).\ \mathrm{Vec}(\mathrm{Bool}, n+1) \to \mathrm{Bool}. \]

Example: map preserves length#

Mapping a function across a vector does not change its length:

\[ \Pi(n:\mathbb{N}).\ (\mathrm{Bool}\to\mathrm{Nat}) \to \mathrm{Vec}(\mathrm{Bool},n) \to \mathrm{Vec}(\mathrm{Nat},n). \]

These are not deep theorems; they are specifications made precise by dependent types.

# head : Π n. Vec(Bool,n+1) -> Bool
head_ty = dep.PiCode(Nat, lambda n: dep.implies_code(VecBool(n + 1), Bool))
head = lambda n: (lambda xs: xs[0])

print("head inhabits Π:", dep.is_in(head, head_ty, depth=5))

# map : Π n. (Bool->Nat) -> Vec(Bool,n) -> Vec(Nat,n)
Nat = dep.NatCode()
map_ty = dep.PiCode(
    Nat,
    lambda n: dep.implies_code(
        dep.implies_code(Bool, Nat),
        dep.implies_code(VecBool(n), dep.VecCode(Nat, n)),
    ),
)

map_vec = lambda n: (lambda f: (lambda xs: [f(x) for x in xs]))

print("map_vec inhabits Π:", dep.is_in(map_vec, map_ty, depth=4))

head inhabits Π: True
map_vec inhabits Π: True

Recovering Non-Dependent Logic#

Non-dependent special cases recover familiar STLC connectives.

  • Implication / function type:

\[ A \to B \cong \Pi(x:A).B \]

  • Conjunction / product:

\[ A \land B \cong \Sigma(x:A).B \]

(where \(B\) does not depend on \(x\)).

This is why Π and Σ are often presented as the dependent versions of \(\to\) and \(\times\).

A = dep.BoolCode()
B = dep.NatCode()

imp = dep.implies_code(A, B)
conj = dep.and_code(A, B)

f = lambda b: 1 if b else 0
p = (True, 3)

print("f inhabits A->B encoded as Π:", dep.is_in(f, imp, depth=6))
print("p inhabits A×B encoded as Σ:", dep.is_in(p, conj, depth=6))

f inhabits A->B encoded as Π: True
p inhabits A×B encoded as Σ: True

Reuse Note

All code in this chapter is reusable from advanced/dependent_codes.py:

  • codes: NatCode, BoolCode, FinCode, VecCode, PiCode, SigmaCode

  • bounded membership: is_in(value, code, depth=...)

  • sampling (for experimentation): sample_values(code, depth=...)

  • logical helpers: implies_code, and_code

If you extend the universe (add a new Code), update both sample_values and is_in.

Exercise

  1. (Π as forall) Define id_nat = lambda n: n and check it inhabits \(\Pi(n:\mathbb{N}).\mathrm{EqNat}(n)\) using dep.PiCode(Nat, lambda n: dep.EqNatCode(n)).

  2. (Σ as exists) Build the type \(\Sigma(n:\mathbb{N}).\mathrm{Vec}(\mathrm{Bool}, n)\) and check that (0, []) and (3, [True, False, True]) inhabit it.

  3. (Invariant-preserving) Define tail : Π n. Vec(Bool,n+1) -> Vec(Bool,n) and check it inhabits its dependent type.

  4. (Counterexample) Define a wrong tail-like function (for example, always dropping two elements) and confirm dep.is_in rejects it. See solutions: Exercise 13 (Dependent Types)

Summary#

  • Π-types are dependent functions; their logical reading is universal quantification.

  • Σ-types are dependent pairs; their logical reading is existential quantification.

  • Dependent types let you express invariants in the type (like vector length).

  • Our executable model checks Π-membership by finite sampling: good for learning and experimentation.

Next: Chapter 14 shifts perspective to sequent calculus and shows equivalence to natural deduction/proof terms.

Contents