Commit 7ac00e6
authored
feat(stdlib): D17 exactly-once MessageHandle as linear typestate (#279)
## Summary
Ships `stdlib/Stream.eph` — the **D17 exactly-once message handles**
quick-win from this session's DB-theory inventory ("ship-this-month"
cluster).
A linear `MessageHandle!` is constructed by `produce` (publisher) or
`next` (consumer) and **must be consumed exactly once** by `ack`,
`fail`, `retry`, or `drop_with_dlq`. Dropping a handle silently at
region exit is a **static type error** — which IS the no-loss half of
exactly-once delivery. Linearity also blocks duplicate `ack` (a handle
cannot be split), giving the no-duplication half.
## Module surface
- **Types**: `Topic`, `MessageHandle` (LINEAR), `AckResult`, `Consumer`
(LINEAR).
- **Producer**: `produce(t, msg) -> MessageHandle!`.
- **Consumer**: `consumer(t, group) -> Consumer!`, `close(c)`, `next(c)
-> Option<Pair<A, MessageHandle!>>`.
- **Finalisers**: `ack`, `fail(reason)`, `retry(attempts) ->
MessageHandle!`, `drop_with_dlq(dlq)`.
- **Sugar**: `exactly_once(h, body) -> Result<A, E>` for the common
process-and-ack-on-Ok / fail-on-Err arc.
- **Pattern guide**: manual / sugar / retry / DLQ / producer (5 worked
examples in the file).
Mirrors `stdlib/Transactions.eph` (D04, PR #275) shape — linear handle
with consume-or-error semantics; engine integration via
`__intrinsic_stream_*` so the host runtime stays out of the type system.
## Pedigree
- **Lamport, L.** "Time, Clocks, and the Ordering of Events in a
Distributed System." *CACM* 21 (7): 558-565. July 1978.
- **Akidau, T. et al.** "The Dataflow Model: A Practical Approach to
Balancing Correctness, Latency, and Cost in Massive-Scale, Unbounded,
Out-of-Order Data Processing." *PVLDB* 8 (12): 1792-1803. August 2015.
(§3 — what/where/when/how of exactly-once.)
- **Wadler, P.** "Linear types can change the world!" *Programming
Concepts and Methods*. North-Holland, 1990. (Linear-handle-for-resources
pattern.)
## Fit in ephapax
- **L1 region capability** bounds handle lifetime so an unwinding panic
at the region boundary cannot leave a half-processed message unacked.
- **L2 affine + L3 mandatory echo** on `ack` are the structural witness
that "every committed offset is the echo of exactly one processed
handle."
- Prereq **D04 Transactions.eph** landed earlier this session as PR
#275.
## Future work (documented in file, out of scope here)
- **D19** `Window.eph` (windowed aggregation; depends on this module's
`MessageHandle`).
- **D28** `Consensus.eph` (2PC / Paxos / Raft as linear protocols —
extends the protocol-as-type story).
- **D07** `Wal.eph` (durability via Linear Echo; ties `ack` to fsync).
- **D09** provenance threading through `next` / `produce`.
- `formal/Stream.v` Coq mechanisation of (a) linear finalisation, (b)
`exactly_once` soundness.
## Test plan
- [ ] Pre-commit SPDX/owner hook passes (verified locally — `MPL-2.0` +
owner literal present).
- [ ] GPG-signed commit (verified locally — key
`4A03639C1EB1F86C7F0C97A91835A14A2867091E`).
- [ ] CI green or pre-existing red on main only.
- [ ] No other file touched (scope = exactly one new stdlib file).
- [ ] Auto-merge SQUASH armed on landing.1 parent 0327717 commit 7ac00e6
1 file changed
Lines changed: 472 additions & 0 deletions
0 commit comments