Part 5 — Dependent-Type Methods

The theoretical heart of Deppy — why homotopy type theory is the right foundation for verifying Python.

Why Homotopy Type Theory for Python?

Every formal verification tool must answer a deceptively simple question: what does it mean for two things to be "the same"?

In most languages this has a straightforward answer. In Haskell, two values are equal when == returns True. In Java, .equals() decides it. But Python is different. Python lives in a world of duck typing, protocols, dynamic dispatch, and multiple inheritance — a world where "sameness" is nuanced, contextual, and structural.

Traditional type theories — System F, dependent types à la Coq, even refinement types — model equality as a proposition: either two things are equal or they are not. This binary view cannot capture duck typing. A list is not literally a tuple, yet they are interchangeable in many contexts. We need a notion of equality that is evidence-bearing and context-sensitive.

Homotopy type theory (HoTT) provides exactly this. In HoTT, equality is not a mere proposition — it is a type whose inhabitants are paths. A path p : a =A b is evidence that a and b are connected. There can be many different paths (different reasons two things are equal), and those paths can themselves be compared via higher paths.

The Deep Insight: Duck Typing = Path Equivalence

Here is the key observation that makes Deppy possible:

Two Python objects are "the same" for a given protocol precisely when there exists a path between them in the type that the protocol defines.

Consider a protocol Iterable. A list and a range object are different types, but both support __iter__. In Deppy this is modeled as:

# Two concrete types
my_list  : list[int]   = [1, 2, 3]
my_range : range        = range(1, 4)

# Path evidence: they are equal *as Iterables*
p : PathType(Iterable[int], my_list, my_range)
p = duck_path(Iterable[int], my_list, my_range)

# Now any proof about my_list-as-Iterable transports to my_range
proof_range = transport(property, p, proof_list)

This is not merely an analogy. The duck_path constructor builds a genuine proof term that two objects satisfy the same protocol operations, and transport carries proofs along that path. The path might be non-trivial — it records exactly how the two objects relate.

Types as Spaces, Programs as Points, Equalities as Paths

The homotopy interpretation gives us three fundamental correspondences:

This table is not window dressing — every row corresponds to a concrete data structure and algorithm inside Deppy. When you write a @guarantee-annotated Python function, Deppy literally constructs spaces, paths, fibrations, and Čech covers to verify it.

A Topological View of a Python Program

Think of a Python function's type signature as a space. The function itself is a point in the space of all functions with that signature. Two implementations of the same interface are two points in the same space, and a proof that they behave the same is a path connecting them.

# Two sorting algorithms — two points in the same space
def bubble_sort(xs: list[int]) -> list[int]: ...
def merge_sort(xs: list[int]) -> list[int]: ...

# A path between them: proof that ∀xs. bubble_sort(xs) = merge_sort(xs)
# This is a continuous family of equalities, not a single bit.
p : PathType(
    (list[int] -> list[int]),
    bubble_sort,
    merge_sort
)
# Constructed via function extensionality (FunExt)
p = funext(lambda xs: sort_equivalence_proof(xs))

The Four Key Methods

Part 5 introduces the four dependent-type methods that power Deppy's verification engine. Each addresses a different aspect of Python verification, and together they cover the full landscape of real-world Python code.

Beyond F*, Dafny, and Liquid Haskell

To appreciate what Deppy brings, let's compare with the state of the art in formal verification:

The key differentiator is not any single feature but the combination: path types for structural equality, Čech decomposition for branching code, fibrations for class hierarchies, and transport for proof reuse — all working together in a cubical type theory that naturally accommodates Python's dynamic, duck-typed semantics.

Why Cubical Homotopy Type Theory?

Deppy is built on cubical type theory (CCHM / Cartesian cubical), not classical HoTT. The distinction matters:

• Classical HoTT postulates univalence as an axiom. It is consistent but not computational — you can state that A ≃ B → A = B, but you cannot compute with the resulting equality.
• Cubical type theory makes univalence a theorem that computes. Paths are literal functions from an interval type 𝕀, and transport along a path produces a concrete program, not just a logical assertion.

For a verification tool this is crucial. When Deppy transports a proof from list to tuple, it needs to compute the adapted proof term. Cubical paths make this possible.

# In cubical Deppy, a path is a function from the interval
# PathAbs(i, body) — at i=0 we get the left endpoint, at i=1 the right

p = PathAbs("i", lambda i:
    # Interpolate between list and tuple representations
    interp(list_repr, tuple_repr, i)
)

# PathApp evaluates the path at a specific point
PathApp(p, 0)   # → list_repr   (left endpoint)
PathApp(p, 1)   # → tuple_repr  (right endpoint)
PathApp(p, 0.5) # → midpoint    (computes!)

What You'll Learn

The five chapters in Part 5 build on each other:

1. Path Types & Transport — the foundation. You'll learn what paths are, how to construct them (Refl, Sym, Trans, Cong, Ap, FunExt), and how transport carries proofs along them. This chapter also covers univalence, the most powerful principle in HoTT.
2. Čech Decomposition — decomposing branching Python code into patches and gluing local proofs into global correctness. You'll see how if/elif/else, match/case, and try/except are all instances of the same topological construction.
3. Fibrations — modeling class hierarchies, generics, and module structures as fiber bundles. You'll learn how to verify a property per-subclass and conclude it holds globally.
4. PSDL: Python-syntax Tactics — Deppy's tactic language, whose source is just Python. Walrus binding, postfix navigation on equalities, operator overloading (p @ q, ~p, f * p, p ** k), comprehensions as induction, assert with proof tag (assert P, "qed"), and the cubical-effect mapping table tying it all to the kernel.
5. Homotopy Tactics — the kernel-level tactic engine that PSDL targets. Includes homotopy-native tactics that have no analogue in other systems.

The Mental Model

Before we dive into the chapters, here is the mental model to carry with you throughout Part 5:

# The verification pipeline (conceptual)

# 1. Parse Python → extract type information
space   = type_to_space(function_signature)

# 2. Function body → point in the space
point   = term_to_point(function_body)

# 3. Specification → target region of the space
target  = spec_to_region(guarantee_annotation)

# 4. Verify: construct a path from point to target
proof   = find_path(point, target, space)
#          ↑ uses Čech decomposition, fibrations, transport

# 5. If proof exists → verified ✅
#    If no path can be found → report the obstruction
#    (The obstruction is a cohomology class — a witness
#     explaining WHY the proof fails.)

This is the engine that runs under every @guarantee annotation. The surface is simple; the topology underneath is what makes it powerful.

A Taste of What's Coming

To whet your appetite, here is a small example that uses paths, transport, and Čech decomposition together:

from deppy import guarantee, check, assume

@guarantee("returns absolute value: result >= 0 and (result == x or result == -x)")
def my_abs(x: int) -> int:
    if x >= 0:
        return x       # Patch U₁: x ≥ 0
    else:
        return -x      # Patch U₂: x < 0

Now suppose we have a second absolute-value implementation:

def my_abs2(x: int) -> int:
    return x if x >= 0 else -x

Deppy constructs a path between my_abs and my_abs2 via function extensionality (they agree on all inputs), then transports the verified guarantee along the path — so my_abs2 is verified for free.

Notation Guide

Throughout Part 5 we use the following notation:

Ready? Let's begin with the most important chapter in the entire book: Path Types & Transport →