Chapter 9 — Duck Typing & Protocols

"If it walks like a duck and quacks like a duck, then it is a duck." This ancient Python proverb encodes a profound type-theoretic idea: type identity is determined by behavior, not by name. In homotopy type theory, this is exactly the notion of a path between types — two types are equal if they support the same operations with compatible behaviors.

This chapter is the signature contribution of Deppy. We show how Python's Protocol classes (PEP 544) are modeled as behavioral specifications in HoTT, and how the DuckPath proof term provides machine-checked evidence that a class conforms to a protocol without inheriting from it.

Protocols as Behavioral Specifications

A Python Protocol declares a set of methods with their signatures. Any class that provides those methods — regardless of its inheritance hierarchy — is considered a structural subtype of the Protocol:

from __future__ import annotations
from typing import Protocol, runtime_checkable

@runtime_checkable
class Renderable(Protocol):
    """Anything that can be rendered to a string representation."""

    def render(self, indent: int = 0) -> str:
        """Return a string representation at the given indent level."""
        ...

    def render_width(self) -> int:
        """Return the width in characters of the rendered output."""
        ...

In Deppy, this Protocol is not just a type hint — it is a formal specification. Deppy extracts:

• The method signatures (parameter types, return types)
• The behavioral contracts (from docstrings and @guarantee annotations)
• The structural requirements (which dunder methods are needed)

Deppy Protocol Specification

from deppy import protocol_spec, guarantee

@protocol_spec
class Renderable(Protocol):
    @guarantee("result is a non-empty string")
    def render(self, indent: int = 0) -> str: ...

    @guarantee("returns a non-negative integer")
    def render_width(self) -> int: ...

# Deppy generates the formal spec:
# ProtocolSpec(Renderable) = {
#   render     : (self, int?) → str  | guarantee: len(result) > 0
#   render_width : (self) → int       | guarantee: result >= 0
# }

The DuckPath Proof Term

The central proof object in this chapter is DuckPath[C, P] — a witness that class C structurally conforms to Protocol P. Formally, a DuckPath is a path in the protocol universe:

DuckPath[C, P] : C =_{ProtocolUniverse} P

A DuckPath is valid if and only if for every method m in P, the class C has a method C.m such that:
(1) C.m's parameter types are contravariant-compatible with P.m's, and
(2) C.m's return type is covariant-compatible with P.m's, and
(3) C.m satisfies all @guarantee annotations on P.m.

Constructing a DuckPath

from deppy.hott import DuckPath, MethodPath, SignatureCheck

# A class that doesn't inherit from Renderable
class HTMLElement:
    def __init__(self, tag: str, children: list[HTMLElement] | None = None):
        self.tag = tag
        self.children = children or []
        self.attrs: dict[str, str] = {}

    def render(self, indent: int = 0) -> str:
        pad = " " * indent
        attr_str = " ".join(
            f'{k}="{v}"' for k, v in self.attrs.items()
        )
        opening = f"{pad}<{self.tag}" + (f" {attr_str}" if attr_str else "") + ">"
        if not self.children:
            return f"{opening}</{self.tag}>"
        child_str = "\n".join(c.render(indent + 2) for c in self.children)
        return f"{opening}\n{child_str}\n{pad}</{self.tag}>"

    def render_width(self) -> int:
        lines = self.render().split("\n")
        return max(len(line) for line in lines)

# Deppy automatically constructs this DuckPath:
duck_proof = DuckPath.auto_construct(HTMLElement, Renderable)
# DuckPath[HTMLElement, Renderable]:
#   MethodPath(render):       sig ✓  ret ✓  guarantee ✓
#   MethodPath(render_width): sig ✓  ret ✓  guarantee ✓
#   Status: VALID ✅

Inside a MethodPath

Each MethodPath in the DuckPath contains detailed evidence:

# Inspecting the proof internals
mp = duck_proof.method_paths["render"]
print(mp.details())

# Output:
# MethodPath(HTMLElement.render → Renderable.render):
#   Parameters:
#     self  : HTMLElement  ≤  Self          [OK — self is always compatible]
#     indent: int          ≡  int           [OK — exact match]
#     indent default: 0    ≡  0             [OK — defaults match]
#   Return:
#     str                  ≡  str           [OK — exact match]
#   Guarantees:
#     "result is a non-empty string":
#       Z3 query: len(result) > 0
#       Proved by: tag is always non-empty ∧ output contains tag
#       Status: Z3_VERIFIED ✅

Example: The Iterable Protocol

Python's iteration protocol is the most pervasive duck typing example. Let's verify that a custom data structure satisfies it:

from __future__ import annotations
from typing import Protocol, TypeVar, Generic, Iterator
from deppy import guarantee, verify

T = TypeVar("T")

class IterableProto(Protocol[T]):
    def __iter__(self) -> Iterator[T]: ...
    def __next__(self) -> T: ...

@verify
class RingBuffer(Generic[T]):
    """A fixed-size circular buffer that supports iteration."""

    def __init__(self, capacity: int) -> None:
        assert capacity > 0
        self._buf: list[T] = []
        self._cap = capacity
        self._pos = 0
        self._iter_idx = 0

    def push(self, item: T) -> None:
        if len(self._buf) < self._cap:
            self._buf.append(item)
        else:
            self._buf[self._pos] = item
        self._pos = (self._pos + 1) % self._cap

    def __iter__(self) -> RingBuffer[T]:
        self._iter_idx = 0
        return self

    def __next__(self) -> T:
        if self._iter_idx >= len(self._buf):
            raise StopIteration
        item = self._buf[self._iter_idx]
        self._iter_idx += 1
        return item

Deppy's verification output:

$ python -m deppy check ring_buffer.py --verbose
Analyzing RingBuffer...

✓ DuckPath[RingBuffer[T], IterableProto[T]]
  ├── __iter__: RingBuffer[T] → RingBuffer[T]
  │   └── Return type RingBuffer[T] ≤ Iterator[T]
  │       (valid because RingBuffer has __next__)
  ├── __next__: RingBuffer[T] → T
  │   ├── Return type T ≡ T  [exact match]
  │   └── StopIteration raised when exhausted  ✓
  └── Status: VALID ✅

✓ Termination: __next__ decreases (len(_buf) - _iter_idx)
✓ Safety: no index-out-of-bounds in __next__
  └── Z3: _iter_idx < len(_buf) at access point

3/3 obligations verified (0.12s)

Example: File-Like Objects

Python's ecosystem is full of file-like objects: StringIO, BytesIO, actual files, network sockets with makefile(), HTTP response bodies. They all satisfy the same protocol without sharing a common base class. Let's verify this:

from __future__ import annotations
from typing import Protocol, Optional
from deppy import guarantee, protocol_spec

@protocol_spec
class ReadableFile(Protocol):
    @guarantee("returns at most n bytes/chars")
    def read(self, n: int = -1) -> str | bytes: ...

    def readline(self) -> str | bytes: ...

    @guarantee("returns False after close()")
    def readable(self) -> bool: ...

    def close(self) -> None: ...

# Now verify multiple classes against this protocol:
from io import StringIO, BytesIO

# Deppy can verify standard library classes too
path_stringio = DuckPath.auto_construct(StringIO, ReadableFile)
path_bytesio  = DuckPath.auto_construct(BytesIO,  ReadableFile)

# Both are valid — StringIO.read returns str, BytesIO.read returns bytes
# Both are subtypes of str | bytes, so the DuckPath holds

We can also verify a custom file-like object:

@verify
class LogCapture:
    """Captures log output into an in-memory buffer."""

    def __init__(self) -> None:
        self._buffer: list[str] = []
        self._pos = 0
        self._closed = False

    @guarantee("returns at most n characters")
    def read(self, n: int = -1) -> str:
        if self._closed:
            raise ValueError("I/O operation on closed file")
        full = "\n".join(self._buffer[self._pos:])
        if n == -1:
            self._pos = len(self._buffer)
            return full
        result = full[:n]
        # advance position by lines consumed
        consumed_lines = result.count("\n")
        self._pos += consumed_lines
        return result

    def readline(self) -> str:
        if self._closed:
            raise ValueError("I/O operation on closed file")
        if self._pos >= len(self._buffer):
            return ""
        line = self._buffer[self._pos]
        self._pos += 1
        return line + "\n"

    def readable(self) -> bool:
        return not self._closed

    def close(self) -> None:
        self._closed = True

    def write(self, msg: str) -> None:
        if self._closed:
            raise ValueError("I/O operation on closed file")
        self._buffer.append(msg)

$ python -m deppy check log_capture.py --verbose
✓ DuckPath[LogCapture, ReadableFile]
  ├── read:     (self, int=-1) → str  ≤  (self, int=-1) → str|bytes
  │   ├── Param compat: int ≡ int  ✓
  │   ├── Return: str ≤ str|bytes  ✓  (str is subtype of union)
  │   └── Guarantee "returns at most n chars":
  │       Z3 query: (n ≥ 0) → len(result) ≤ n
  │       Status: Z3_VERIFIED ✅
  ├── readline: (self) → str  ≤  (self) → str|bytes  ✓
  ├── readable: (self) → bool  ≡  (self) → bool  ✓
  │   └── Guarantee "returns False after close()":
  │       Z3 query: (self._closed == True) → (result == False)
  │       Status: Z3_VERIFIED ✅
  ├── close:    (self) → None  ≡  (self) → None  ✓
  └── Status: VALID ✅

Note: LogCapture has extra method write not in ReadableFile — OK
  (structural subtyping allows extra methods)

Path Construction: The Theory

How does Deppy actually construct the path between two duck-typed objects? The construction mirrors the cubical type theory interval:

# Simplified internal representation of DuckPath construction
from deppy.hott.cubical import Interval, PathType, refl, ap

def construct_duck_path(
    cls: type,
    proto: type[Protocol],
) -> PathType[type, cls, proto]:
    """
    Construct a path in the protocol universe from cls to proto.

    In cubical type theory, a path A =_U B is a function
    p : I → U such that p(0) = A and p(1) = B.

    For duck typing, we construct this path by interpolating
    between the method tables:
      p(i) = { m : merge(cls.m, proto.m, i) for m in proto.methods }
    where merge(f, g, 0) = f, merge(f, g, 1) = g,
    and merge is defined iff f and g are signature-compatible.
    """
    proto_methods = inspect_protocol_methods(proto)
    cls_methods   = inspect_class_methods(cls)

    method_paths = {}
    for name, proto_sig in proto_methods.items():
        if name not in cls_methods:
            raise DuckPathError(
                f"Class {cls.__name__} missing method {name}"
            )
        cls_sig = cls_methods[name]

        # Check contravariant params, covariant return
        param_path = check_param_compatibility(cls_sig, proto_sig)
        ret_path   = check_return_compatibility(cls_sig, proto_sig)

        # The method path is the product of param and return paths
        method_paths[name] = MethodPath(
            source=cls_sig, target=proto_sig,
            param_evidence=param_path,
            return_evidence=ret_path,
        )

    # The DuckPath is the product of all method paths
    return DuckPath(
        source=cls, target=proto,
        method_paths=method_paths,
        # Valid iff all method paths are valid
        is_valid=all(mp.is_valid for mp in method_paths.values()),
    )

Variance and Compatibility

DuckPath construction requires careful variance checking. Python's type system has nuanced rules about when a method signature is "compatible":

# Deppy's actual variance analyzer — pure Python via inspect.
# No Z3 needed: variance positions follow PEP 484 rules and
# compose under a meet lattice (covariant ⊓ contravariant = invariant).
from deppy.proofs.psdl_variance import (
    analyze_class_variance, VariancePos, emit_variance_check,
)

def check_param_compatibility(cls: type, type_var: str):
    """Walk cls's methods/fields, tag each occurrence, take the meet."""
    report = analyze_class_variance(
        cls,
        type_var_name=type_var,
        declared=VariancePos.COVARIANT,
    )
    # Method return types ↦ covariant; method params ↦ contravariant;
    # mutable fields ↦ invariant; frozen fields ↦ covariant.
    if report.consistent_with_declaration:
        return emit_variance_check(report)  # kernel ProofTerm
    raise ValueError(
        f"variance violations: {report.occurrences}"
    )

The analyzer is invoked at proof time via the PSDL primitive verify_variance(Cls, type_var=..., declared=...), which emits a VarianceCheck ProofTerm into the kernel. Soundness is established at the meta-level in metatheory/Deppy.lean §32.

Dynamic Attribute Resolution

Python allows classes to define __getattr__, which intercepts attribute lookups for attributes that don't exist on the object. This means a class can satisfy a Protocol dynamically — it might not have the methods in its __dict__, but __getattr__ synthesizes them on demand:

class DynamicProxy:
    """Proxy that delegates all method calls to a target object."""

    def __init__(self, target: object) -> None:
        self._target = target

    def __getattr__(self, name: str) -> Any:
        return getattr(self._target, name)

# Does DynamicProxy satisfy Renderable?
# It depends on what _target is!

Deppy handles this with conditional DuckPaths — a DuckPath that is valid given certain conditions on the object's state:

# Deppy generates a conditional DuckPath:
cond_proof : ConditionalDuckPath[DynamicProxy, Renderable] = (
    ConditionalDuckPath.construct(
        condition="isinstance(self._target, Renderable)",
        # Under this condition, __getattr__ delegates to a Renderable,
        # so all method lookups succeed with compatible signatures
        evidence=FiberedLookup(
            fiber_over="_target",
            base_path=DuckPath.auto_construct(
                target_type=Renderable,
                proto=Renderable
            ),
            transport_through="__getattr__",
        )
    )
)
# Status: CONDITIONALLY VALID ✅
# Condition: _target must satisfy Renderable

Composing DuckPaths

DuckPaths compose. If A duck-types as B and B duck-types as C, then A duck-types as C:

from deppy.hott import path_compose

# Given:
p1 : DuckPath[HTMLElement, Renderable]   # from earlier
p2 : DuckPath[Renderable, Displayable]  # if Displayable ⊆ Renderable

# Then we can compose:
p3 : DuckPath[HTMLElement, Displayable] = path_compose(p1, p2)
# p3 is valid iff both p1 and p2 are valid

# This corresponds to path composition in HoTT:
# p1 : A =_U B
# p2 : B =_U C
# p1 · p2 : A =_U C

When DuckPaths Fail

Not everything that looks like a duck is actually a duck. Deppy provides detailed error reports when a DuckPath cannot be constructed:

class BadElement:
    def render(self) -> None:  # wrong return type!
        print("<div/>")

    # missing render_width entirely!

$ python -m deppy check bad_element.py --verbose
✗ DuckPath[BadElement, Renderable]: INVALID

  ├── render: SIGNATURE MISMATCH
  │   ├── Parameters:
  │   │   Protocol requires: (self, indent: int = 0)
  │   │   Class provides:    (self)
  │   │   ✗ Missing parameter 'indent'
  │   └── Return type:
  │       Protocol requires: str
  │       Class provides:    None
  │       ✗ None is not a subtype of str
  │
  ├── render_width: MISSING
  │   ✗ BadElement has no method 'render_width'
  │
  └── 2 errors, 0 warnings

Suggestion: Add render_width(self) → int to BadElement,
and change render to accept indent: int = 0 and return str.

Comparison with F*: Interfaces vs. DuckPaths

The fundamental difference between Deppy and F* (or any language with nominal typing) is captured in this table:

Advanced: Generic Protocols

Protocols can be generic, and DuckPaths must handle type variables correctly. Here's a more complex example with a generic Comparable protocol:

from __future__ import annotations
from typing import Protocol, TypeVar
from deppy import guarantee, verify

T = TypeVar("T")

class Comparable(Protocol):
    @guarantee("antisymmetric: (a ≤ b ∧ b ≤ a) → a == b")
    @guarantee("transitive: (a ≤ b ∧ b ≤ c) → a ≤ c")
    def __le__(self, other: Comparable) -> bool: ...

    @guarantee("consistent with __le__: (a < b) ↔ (a ≤ b ∧ a ≠ b)")
    def __lt__(self, other: Comparable) -> bool: ...

@verify
class Temperature:
    def __init__(self, kelvin: float) -> None:
        assert kelvin >= 0.0, "Temperature cannot be below absolute zero"
        self._k = kelvin

    def __le__(self, other: Temperature) -> bool:
        return self._k <= other._k

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

    def __eq__(self, other: object) -> bool:
        if not isinstance(other, Temperature):
            return NotImplemented
        return self._k == other._k

$ python -m deppy check temperature.py --verbose
✓ DuckPath[Temperature, Comparable]
  ├── __le__: (self: Temperature, other: Temperature) → bool
  │   ├── Param 'other': Temperature ≤ Comparable
  │   │   (valid: Temperature satisfies Comparable — recursive check)
  │   ├── Guarantee "antisymmetric":
  │   │   Z3 encoding:
  │   │     ∀ a_k b_k : Real.
  │   │       (a_k ≥ 0 ∧ b_k ≥ 0) →
  │   │       ((a_k ≤ b_k ∧ b_k ≤ a_k) → a_k == b_k)
  │   │   Status: Z3_VERIFIED ✅
  │   └── Guarantee "transitive":
  │       Z3 encoding:
  │         ∀ a_k b_k c_k : Real.
  │         (a_k ≥ 0 ∧ b_k ≥ 0 ∧ c_k ≥ 0) →
  │         ((a_k ≤ b_k ∧ b_k ≤ c_k) → a_k ≤ c_k)
  │       Status: Z3_VERIFIED ✅
  ├── __lt__:
  │   └── Guarantee "consistent with __le__":
  │       Z3 encoding:
  │         ∀ a_k b_k : Real.
  │         (a_k ≥ 0 ∧ b_k ≥ 0) →
  │         ((a_k < b_k) ↔ (a_k ≤ b_k ∧ a_k ≠ b_k))
  │       Status: Z3_VERIFIED ✅
  └── Status: VALID ✅

Runtime Protocol Checking

With @runtime_checkable Protocols, Python's isinstance performs a structural check at runtime. Deppy connects this to the static DuckPath:

@runtime_checkable
class Renderable(Protocol):
    def render(self, indent: int = 0) -> str: ...
    def render_width(self) -> int: ...

def display(obj: object) -> None:
    if isinstance(obj, Renderable):
        # Here, Deppy narrows obj's type:
        # obj : object  →  obj : Renderable
        # This is justified by the DuckPath that isinstance checks
        print(obj.render())
        # ✅ Safe: obj.render() is valid because isinstance verified
        #    the structural conformance at runtime
    else:
        print(repr(obj))

# Deppy's verification of 'display':
# Branch 1: isinstance(obj, Renderable) == True
#   → DuckPath[type(obj), Renderable] exists at runtime
#   → obj.render : (int?) → str  is valid
#   → print(obj.render()) : None  ✓
# Branch 2: isinstance(obj, Renderable) == False
#   → repr(obj) : str  always valid  ✓

Exercises