Coalgebras: Generators & Async

yield and await as comonad coalgebras — every suspension is an effect-witness, every resumption is a transport.

The Coalgebraic Picture

A function that runs to completion is an algebra: it consumes input and emits an answer. A function that yields, suspends, and resumes is a coalgebra: it consumes nothing in the middle, emits a partial result, and stores its own continuation as state. Generators and coroutines are exactly this — coalgebras of the "value-or-suspension" comonad.

Deppy gives both shapes the same kernel treatment: each suspension becomes an EffectWitness tagged with the current world epoch, and the chain of suspensions composes via PathComp (or Cut, its sequential cousin). Resumptions transport proofs across the suspension's path.

Generators: yield as EffectWitness

Compile a tiny generator and inspect the proof term:

from deppy.proofs.psdl import compile_psdl

src = """
def gen():
    yield 1
    yield 2
    yield 3
"""
res = compile_psdl(src, foundations={})
print(res.term_repr)

Output:

Cut(_psdl_step_2,
    EffectWitness(yield:0@epoch0, Refl),
    Cut(_psdl_step_3,
        EffectWitness(yield:1@epoch0, Refl),
        EffectWitness(yield:2@epoch0, Refl)))

Three observations:

• Each yield x compiles to EffectWitness("yield:N@epoch_M", Refl(value)). The N is the yield index (0, 1, 2, …); epoch_M is the heap epoch at the time of the yield (here always 0 because none of the yields mutate).
• Three yields are chained by two nested Cuts. The shape is a left-to-right list: yield 0 happens, then (yield 1 then yield 2). Composition is associative because Cut is.
• Refl is the trivial path: the yielded value flows unchanged into the resumption. Generators that send a value back use a TransportProof instead.

Direct API: emit_yield_witness

You can build the witness yourself:

from deppy.proofs.psdl_generators import (
    GeneratorRegistry, emit_yield_witness,
)

reg = GeneratorRegistry()
g = reg.declare('myg', line=0)
reg.add_yield_to('myg', '1', line=2, world_epoch=0)
reg.add_yield_to('myg', '2', line=3, world_epoch=0)
print(g.yields)
# [YieldPoint(index=0, value_repr='1', ...), YieldPoint(index=1, ...)]

w = emit_yield_witness('1', 0, world_epoch=0)
print(w)
# EffectWitness(yield:0@epoch0, Refl(Var(name='_yield_0_1')))

Destructors: next(g) and g.send(v)

The dual operation — extracting one yield from a generator — uses emit_advance_witness, which builds a Cut whose lemma is the current yield point and whose body is the resumption (a Refl for plain next; a TransportProof for send, since the resumed value can change).

Async: await as Event-Path

Coroutines are generators whose suspension events are tied to external "future arrivals" rather than caller-driven advancement. The compile shape is similar:

src = """
async def f():
    x = await producer()
    return x + 1
"""
res = compile_psdl(src, foundations={})
print(res.term_repr)

Output:

Cut(_psdl_step_2,
    Cut(x, EffectWitness(await:producer()@epoch0, Refl), Refl),
    Refl)

await producer() is the suspension event; the kernel records it as EffectWitness("await:producer()@epoch0", Refl). The outer Cut(x, …, Refl) binds the resumed value to x — the resumption is itself a witness that the awaited future delivered x.

Multiple awaits compose

src = """
async def f():
    x = await a()
    y = await b()
    return x
"""
res = compile_psdl(src, foundations={})
print(res.term_repr)

Cut(_psdl_step_2,
    Cut(x, EffectWitness(await:a()@epoch0, Refl), Refl),
    Cut(_psdl_step_3,
        Cut(y, EffectWitness(await:b()@epoch0, Refl), Refl),
        Refl))

Each await is its own edge in the world-path. If a() mutates the heap before b() runs, the @epochN tag changes accordingly and any proof reused from before the mutation must transport.

send and Resume Are Both Transport

For a generator, g.send(v) resumes the suspended computation with a new value v that may not equal what was yielded. Deppy models this with a TransportProof along the yield-path: the value flows through, but the path now records that the inhabitant changed at the suspension boundary.

For a coroutine, the same pattern applies: when the awaited future arrives, the new value substitutes into the binding via TransportProof. This is why both shapes feel the same in the kernel — they really are instances of the same coalgebraic pattern.

Generators as State Machines

The Generator dataclass tracks name, yields (the list of YieldPoints), current_index, and exhausted. The registry's advance(name) increments the index. Because Python semantics let you send at any point, every yield-edge is reversible — Sym (path inversion) takes you back to the previous suspension.

Generators That Mutate

A generator that mutates between yields produces an EffectSequence mixing yield and mutate witnesses:

from deppy.proofs.psdl import compile_psdl
res = compile_psdl("""
def stateful_gen(buf):
    yield 1
    buf.append(1)
    yield 2
""", foundations={})
print(res.effect_sequence)

The compiler produces an effect_sequence tracking each mutation between yields. Reading the buffer at later yield points requires TransportProof across the intervening buf.append mutation — the cubical heap from Part 6.1 kicks in automatically.

Why This Encoding?

Treating yield and await as coalgebras has three concrete benefits for verification:

1. Compositionality. Two generators chained by yield from compose by appending their yield-paths; the proof obligations follow the same composition.
2. Heap interleaving. Generator-driven mutation intermixes with the world's epoch counter exactly the way Python executes it; no sequential-vs-parallel mismatch.
3. Cancellation. g.close() as Sym means cancellation is the path inverse, not a special case — the kernel doesn't need a separate "cancelled" state.

What's Next

Part 6's Async / Await chapter builds on this view to verify concurrent code using deppy.async_verify with @async_requires / @async_ensures. Part 5's PSDL chapter shows how generators and coroutines map to the cubical-effect tactic language.