MRO & Descriptors

C3 linearization as a sheaf, descriptor lookup as a 4-fibre fibration.

The Two Halves of Attribute Lookup

Python's attribute access — obj.attr — runs through two orthogonal mechanisms. The MRO walks the class hierarchy in C3 order asking each ancestor "do you define attr?" The descriptor protocol picks one of four routes whenever the answer is "yes": data descriptor, instance dict, non-data descriptor, or __getattr__. Both are choice points, but they choose differently — MRO picks one class out of many; descriptors pick one route out of four.

Deppy gives them complementary kernel encodings. MRO becomes a DuckPath through the linearization; shared methods across overlapping bases form a Cocycle; super() is PathComp. Descriptor lookup becomes a Fiber with four branches — one per protocol case.

MRO as a DuckPath

The MROTable dataclass tracks the inheritance graph and memoizes C3 linearization. Each lookup is a path through the linearization, skipping classes that don't define the attribute:

from deppy.proofs.psdl_mro import MROTable, emit_mro_dispatch_path

t = MROTable()
t.declare('Animal', methods={'speak': 'a'})
t.declare('Dog', bases=['Animal'], methods={'speak': 'd'})
t.declare('Puppy', bases=['Dog'])

print(t.linearize('Puppy'))
# ['Puppy', 'Dog', 'Animal']

p = emit_mro_dispatch_path(t, 'Puppy', 'speak')
print(p)
# DuckPath(PyObjType(), PyObjType(),
#         [skip_Puppy.speak: ..., resolve_Dog.speak: ...])

Puppy doesn't define speak, so the path records a skip step; Dog does, so the path resolves there. The linearization stops as soon as a method is found — the DuckPath reflects exactly that sequence.

From PSDL: mro_lookup

from deppy.proofs.psdl import compile_psdl

src = 'mro_lookup(Cls, "method")\nsuper_call("Cls", "method")'
res = compile_psdl(src, foundations={})
print(res.term_repr)
# Cut(_psdl_step_1, DuckPath(…), PathComp(…))

mro_lookup compiles to DuckPath; super_call compiles to PathComp — the sequential composition of the call site's method and the next class's method.

Diamonds & the Cocycle

When two parent classes both define a method, C3 picks one — but verifying the choice is consistent across many call sites is itself a proof obligation. Deppy uses a Cocycle: the "agreement on overlaps" condition from Čech cohomology, applied to method tables.

from deppy.proofs.psdl_mro import MROTable, emit_mro_cocycle

t = MROTable()
t.declare('A', methods={'m': 'a'})
t.declare('B', bases=['A'], methods={'m': 'b'})
t.declare('C', bases=['A'], methods={'m': 'c'})
t.declare('D', bases=['B', 'C'])

print(t.linearize('D'))
# ['D', 'B', 'C', 'A']

c = emit_mro_cocycle(t, 'D', ['m'])
print(c)
# Cocycle(C^1, 1 components, 3 boundary pairs, δ unwitnessed)

The cocycle records all the (parent, child) pairs whose method tables must agree. The kernel checks δc = 0 — the cocycle condition — to be sure the linearization is consistent. When two parents disagree on a shared method and there's no override, the cocycle has a non-trivial coboundary and the kernel rejects.

Descriptors: a 4-Fibre Fiber

Reading obj.attr follows Python's well-known precedence:

1. Data descriptor on the class (__get__ + __set__) — wins outright.
2. Instance dict entry — wins if no data descriptor.
3. Non-data descriptor on the class (__get__ only) — wins if no instance entry.
4. __getattr__ fallback — final route.

Deppy encodes this as a 4-branch Fiber over the lookup site. emit_descriptor_fiber builds the kernel object directly:

from deppy.proofs.psdl_descriptors import emit_descriptor_fiber

f = emit_descriptor_fiber('obj', 'Cls', 'attr')
print(f)
# Fiber(Var(name='_attr_obj_attr'),
#       [PyObjType(), PyObjType(), PyObjType(), PyObjType()])

Each of the four PyObjType() entries corresponds to one branch of the precedence rule. At verification time the kernel asks "which branch fires?" by consulting the DescriptorRegistry, which records the descriptor kind (DATA, NON_DATA, INSTANCE, GETATTR) for each declared attribute.

From PSDL: descriptor_get

from deppy.proofs.psdl import compile_psdl
src = 'descriptor_get(obj, "Cls", "attr")'
res = compile_psdl(src, foundations={})
print(res.term_repr)
# Fiber(Var(name='_attr_obj_attr'), 4 fibres)

Monkey-patching: descriptor_set

Setting an attribute that was previously held in a different protocol slot — say replacing an instance value with a data descriptor — is a monkey-patch. Deppy emits a Patch kernel term, which carries the contract proof that the new value still satisfies the attribute's declared spec:

src = 'descriptor_set(obj, "Cls", "attr", new_value)'
res = compile_psdl(src, foundations={})
print(res.term_repr)
# Patch(…)

Why Two Different Encodings?

MRO and descriptors look alike from the outside (both are "lookups that pick one of several routes") but the right kernel object for each is different:

• MRO is variable-length. A class can inherit from any number of bases, with arbitrarily nested overlaps — the right encoding is a path of unbounded length, with overlap- agreement enforced by a Čech cocycle.
• Descriptor protocol is fixed-arity. There are exactly four routes, every time. The right encoding is a 4-branch fibration, where each branch carries its own type information for the descriptor's __get__ / __set__ signature.

What's Next

Operator Dispatch — the __r*__ fallback — uses a related but distinct construct (ConditionalDuckPath) because the condition is whether the LHS implements __op__, not which class is in scope. Then Coalgebras: Generators & Async covers yield and await.