Operator Dispatch

__r*__ fallback as ConditionalDuckPath; subclass priority as outer Fiber.

Two-Phase Operator Resolution

When Python evaluates a + b it doesn't simply call a.__add__(b). The runtime first checks whether the LHS has an __add__ method and whether that method returns something other than NotImplemented. Only if the LHS forfeits does the runtime fall back to b.__radd__(a). And there's a wrinkle: if type(b) is a strict subclass of type(a), __radd__ goes first.

That's three potential routes per binary operator. Deppy encodes the whole pattern as a ConditionalDuckPath: a duck-typing path predicated on a runtime condition, with a fibration over the success / fallback / type-error cases.

Without Subclass Priority

The plain case (no subclass relation between the operands) compiles to a single conditional path:

from deppy.proofs.psdl_op_dispatch import emit_op_dispatch

print(emit_op_dispatch('+', 'a', 'b'))

Output:

ConditionalDuckPath(
    if "hasattr(type(lhs), '__add__') and lhs.__add__(b) is not NotImplemented":
        Fiber)

Three pieces here:

• The condition is the runtime predicate. It's symbolic — verification doesn't execute it; the kernel asks Z3 whether type(a) declares the operator dunder, and whether the call's return type excludes NotImplemented.
• The true branch is a Fiber with the forward __add__ path.
• The false branch (implied by the conditional) falls back to b.__radd__(a) with its own NotImplemented fibre, and finally to a TypeError witness if both forfeit.

From PSDL: op_dispatch

from deppy.proofs.psdl import compile_psdl

src = 'op_dispatch("+", a, b)'
res = compile_psdl(src, foundations={})
print(res.term_repr)
# ConditionalDuckPath(…)

Subclass Priority Adds an Outer Fiber

When type(b) is a subclass of type(a) (and not the same class), Python tries b.__radd__(a) first. Deppy wraps the conditional path in an outer Fiber over the issubclass question:

from deppy.proofs.psdl_op_dispatch import (
    emit_op_dispatch, OperatorRegistry,
)

reg = OperatorRegistry()
r = emit_op_dispatch(
    '+', 'a', 'b',
    lhs_class='int', rhs_class='Vec', registry=reg,
)
print(r)
# Fiber(Var(name='_issubclass_Vec_of_int'),
#       [PyObjType(), PyObjType()])

The two fibres correspond to:

1. RHS-first branch — fires when issubclass(Vec, int) holds.
2. Standard branch — fires otherwise; this branch contains the same ConditionalDuckPath as the basic case.

In-Place Operators (+= and friends)

a += b follows a different protocol: Python first looks for __iadd__. If absent, the expression rewrites to a = a + b with the regular dispatch. Deppy uses emit_inplace_op_dispatch:

from deppy.proofs.psdl_op_dispatch import emit_inplace_op_dispatch

print(emit_inplace_op_dispatch('+', 'a', 'b'))
# ConditionalDuckPath(if "hasattr(type(lhs), '__iadd__')": Fiber)

The Operator Dunder Table

OPERATOR_DUNDERS maps Python's binary operators to their forward / reverse dunder pairs:

from deppy.proofs.psdl_op_dispatch import OPERATOR_DUNDERS
for op, (fwd, rev) in list(OPERATOR_DUNDERS.items())[:5]:
    print(op, fwd, rev)

Output:

+ __add__ __radd__
- __sub__ __rsub__
* __mul__ __rmul__
@ __matmul__ __rmatmul__
/ __truediv__ __rtruediv__

Why a Conditional Duck Path?

A plain DuckPath says: "x and y are observationally interchangeable." But operator dispatch is more subtle — the choice depends on whether the operand declares a method. The ConditionalDuckPath carries:

• A condition — a symbolic predicate the kernel evaluates against the type registry.
• A true-branch evidence — proof that the path exists when the condition holds.
• A false-branch evidence — proof that the fallback path exists otherwise.

This shape is exactly what's needed to verify NotImplemented-driven dispatch without requiring the verifier to run the operands.

A Worked Verification

Suppose we want to verify that vec + 0 commutes: i.e. vec + 0 == 0 + vec. The forward dispatch picks vec.__add__(0). The reverse dispatch picks vec.__radd__(0) (because int.__add__ returns NotImplemented on a Vec). If both methods agree on the result, the equation holds.

Deppy compiles the obligation by emitting two ConditionalDuckPaths and checking that the success fibres coincide. When __add__ and __radd__ delegate to the same underlying implementation, the kernel simplifies the path to Refl automatically.

What's Next

Coalgebras: Generators & Async covers yield and await, which use a similar conditional pattern but for suspension events instead of method existence.