Equality & Duck Typing

Python has multiple notions of equality: is, ==, and structural comparison. In everyday code the distinctions rarely matter — but for formal verification they are everything. Deppy borrows the answer from homotopy type theory: different equalities correspond to different path types. This chapter introduces all three, then shows how Deppy extends the same idea to Python's duck typing — treating structural conformance as a path between types.

Python's Three Equalities

Every Python programmer eventually trips over the difference between is and ==. Deppy makes the distinction explicit by mapping each form of equality to a different path type:

Here is a quick demonstration of how these diverge:

# Identity vs. value equality
a = [1, 2, 3]
b = [1, 2, 3]
a == b   # True  — same contents
a is b   # False — different objects in memory
c = a
a is c   # True  — c is an alias for a

Deppy never relies on CPython interning behaviour. When verifying a is b, it demands an Id path — a proof that the two names refer to the same object. For a == b, a ValuePath suffices.

The __eq__ / __hash__ Contract

Python's data model requires: if a == b then hash(a) == hash(b). Violating this breaks dictionaries and sets. Deppy verifies this automatically for any class with custom __eq__.

class Point:
    def __init__(self, x: float, y: float):
        self.x, self.y = x, y

    def __eq__(self, other: object) -> bool:
        if not isinstance(other, Point):
            return False
        return self.x == other.x and self.y == other.y

    def __hash__(self) -> int:
        return hash((self.x, self.y))

Deppy verifies:

# Deppy output:
# ✓ Point.__eq__ is reflexive     (∀p. p == p)
# ✓ Point.__eq__ is symmetric     (∀p,q. p == q → q == p)
# ✓ Point.__eq__ is transitive    (∀p,q,r. p == q ∧ q == r → p == r)
# ✓ __eq__/__hash__ contract      (∀p,q. p == q → hash(p) == hash(q))

Now consider a broken implementation:

class BrokenPoint:
    def __init__(self, x: float, y: float):
        self.x, self.y = x, y

    def __eq__(self, other: object) -> bool:
        if not isinstance(other, BrokenPoint):
            return False
        return self.x == other.x and self.y == other.y

    def __hash__(self) -> int:
        return hash(self.x)  # ✗ ignores y!

# Deppy output:
# ✓ BrokenPoint.__eq__ is reflexive
# ✓ BrokenPoint.__eq__ is symmetric
# ✓ BrokenPoint.__eq__ is transitive
# ⚠ __eq__/__hash__ quality warning
#   hash ignores field y — unequal points will collide excessively.
#   Recommendation: hash should use all fields compared by __eq__.

from dataclasses import dataclass

@dataclass(frozen=True)
class Point:
    x: float
    y: float

# Deppy: ✓ all equality/hash properties verified automatically

Duck Typing as Paths

"If it walks like a duck and quacks like a duck, it's a duck." In Python, any object with the right methods can substitute for any other — no inheritance required. Deppy formalises this with DuckPath: a path between two types sharing the same interface. A DuckPath(A, B, P) proves that A and B both conform to protocol P, so either can be supplied wherever P is expected.

from typing import Protocol, runtime_checkable

@runtime_checkable
class Drawable(Protocol):
    def draw(self) -> None: ...
    def bounding_box(self) -> tuple[float, float, float, float]: ...


class Circle:
    def __init__(self, cx: float, cy: float, r: float):
        self.cx, self.cy, self.r = cx, cy, r

    def draw(self) -> None:
        print(f"○ at ({self.cx}, {self.cy}) r={self.r}")

    def bounding_box(self) -> tuple[float, float, float, float]:
        return (self.cx-self.r, self.cy-self.r, self.cx+self.r, self.cy+self.r)

class Square:
    def __init__(self, x: float, y: float, side: float):
        self.x, self.y, self.side = x, y, side

    def draw(self) -> None:
        print(f"□ at ({self.x}, {self.y}) side={self.side}")

    def bounding_box(self) -> tuple[float, float, float, float]:
        return (self.x, self.y, self.x+self.side, self.y+self.side)

Deppy produces:

# Deppy output:
# ✓ DuckPath(Circle, Square, Drawable)
#   Circle.draw   : (self) -> None       ≡  Drawable.draw
#   Circle.bounding_box : (self) -> tuple ≡  Drawable.bounding_box
#   Square.draw   : (self) -> None       ≡  Drawable.draw
#   Square.bounding_box : (self) -> tuple ≡  Drawable.bounding_box

The DuckPath says Circle and Square are interchangeable at the Drawable interface — not in every context. Functions depending on .r will not accept a Square.

Behavioral Equivalence

Two implementations are behaviorally equivalent if they produce the same output for all valid inputs. Deppy can prove this — enabling safe refactoring without test suites.

def insertion_sort(lst: list[int]) -> list[int]:
    result = list(lst)
    for i in range(1, len(result)):
        key = result[i]
        j = i - 1
        while j >= 0 and result[j] > key:
            result[j + 1] = result[j]
            j -= 1
        result[j + 1] = key
    return result

def selection_sort(lst: list[int]) -> list[int]:
    result = list(lst)
    for i in range(len(result)):
        min_idx = i
        for j in range(i + 1, len(result)):
            if result[j] < result[min_idx]:
                min_idx = j
        result[i], result[min_idx] = result[min_idx], result[i]
    return result

# Deppy verification:
# ✓ behavioral_equiv(insertion_sort, selection_sort)
#   Both produce a sorted permutation of the input.
#   Since sorted permutations are unique, outputs are equal (ValuePath).

Behavioral equivalence enables safe refactoring: replace one implementation with another, and Deppy guarantees identical observable behaviour.

Protocol Conformance Proofs

Deppy can prove that a class implements a Protocol by checking each required method for existence and type compatibility — no inheritance needed.

from typing import Protocol, Iterator

class Iterable(Protocol):
    def __iter__(self) -> Iterator: ...

class Range:
    def __init__(self, start: int, stop: int):
        self.start, self.stop = start, stop

    def __iter__(self) -> Iterator[int]:
        current = self.start
        while current < self.stop:
            yield current
            current += 1

# Deppy output:
# ✓ Range implements Iterable
#   __iter__: (self) -> Iterator[int]
#   return type Iterator[int] ≤ Iterator (covariant). Conformance proven.

For explicit annotation, use @implements — purely documentary, but Deppy will error if conformance breaks:

from deppy import implements

@implements(Iterable)
class Range:
    ...

Proving Interface Equivalence

Let's put it all together. We define a CacheProtocol, implement it two ways, and prove both are interchangeable at the protocol boundary.

from typing import Protocol, Optional

class CacheProtocol(Protocol):
    def get(self, key: str) -> Optional[str]: ...
    def put(self, key: str, value: str) -> None: ...
    def size(self) -> int: ...


class DictCache:
    def __init__(self):
        self._store: dict[str, str] = {}

    def get(self, key: str) -> Optional[str]:
        return self._store.get(key)

    def put(self, key: str, value: str) -> None:
        self._store[key] = value

    def size(self) -> int:
        return len(self._store)
class ListCache:
    def __init__(self):
        self._entries: list[tuple[str, str]] = []

    def get(self, key: str) -> Optional[str]:
        for k, v in self._entries:
            if k == key:
                return v
        return None

    def put(self, key: str, value: str) -> None:
        self._entries = [(k, v) for k, v in self._entries if k != key]
        self._entries.append((key, value))

    def size(self) -> int:
        return len(self._entries)

# Deppy output:
# ✓ DictCache  implements CacheProtocol
# ✓ ListCache  implements CacheProtocol
# ✓ DuckPath(DictCache, ListCache, CacheProtocol)
# ✓ Behavioral equivalence: identical outputs for all operation sequences.

Exercise

from typing import Protocol

class Comparable(Protocol):
    def __lt__(self, other: "Comparable") -> bool: ...
    def __eq__(self, other: object) -> bool: ...


class Temperature:
    def __init__(self, celsius: float):
        self.celsius = celsius

    def __lt__(self, other: "Temperature") -> bool:
        return self.celsius < other.celsius

    def __eq__(self, other: object) -> bool:
        return isinstance(other, Temperature) and self.celsius == other.celsius

class Version:
    def __init__(self, major: int, minor: int, patch: int):
        self.parts = (major, minor, patch)

    def __lt__(self, other: "Version") -> bool:
        return self.parts < other.parts

    def __eq__(self, other: object) -> bool:
        return isinstance(other, Version) and self.parts == other.parts

# ✓ Temperature implements Comparable
# ✓ Version     implements Comparable
# ✓ DuckPath(Temperature, Version, Comparable)
#
# Strict total order — Temperature.__lt__:
#   ✓ Irreflexive  ✓ Transitive  ✓ Total
# Strict total order — Version.__lt__:
#   ✓ Irreflexive  ✓ Transitive  ✓ Total