Skip to content
Weltenwanderer Weltenwanderer

ADR-005: Evolve as F-Algebra with Catamorphism Fold

Context

The evolve function in event sourcing applies events to state: (State, Event) → State. Over an event stream, this is a left-fold. The question is whether to treat evolve as an arbitrary function or to model it with a formal algebraic structure.

Treating evolve as arbitrary means postcondition verification requires runtime testing. A formal model opens the possibility of static verification.

Decision

Model evolve as an F-algebra. Given the functor F(X) = State × Event → X, the fold over an event stream is the catamorphism — the unique homomorphism from the initial algebra to the evolve algebra.

This choice is justified by three properties the structure provides:

1. Initiality Two evolve definitions that produce identical state transitions for all inputs are provably equal. This enables semantic equivalence checking without runtime comparison.

2. Banana-split theorem Two independent folds over the same event stream fuse into a single pass. This is the formal basis for projection optimization when multiple read models consume the same stream.

3. Fusion law h . cata(f) = cata(g) when h is an algebra homomorphism. The ensure postcondition layer uses this law: a postcondition P on the final state is derivable from evolve if and only if P can be expressed as an algebra homomorphism from the evolve algebra. This reduces postcondition verification to a structural check on expressions.

Formal specification: specs/theory.allium, rule Th-1 (F-Algebra section).

For finite algebraic state types, the catamorphism yields a finite automaton, and all properties over its traces are decidable (Gelade, Marquardt, Schwentick 2012).

Consequences

Positive

  • Postcondition verification (ensure) reduces to a compile-time fusion law check rather than runtime property testing.
  • Projection optimization has a formal foundation that is checkable by the compiler.
  • Equivalence between two evolve definitions is decidable for finite state types.

Negative

  • Fusion law checking requires expression analysis; this is blocked until the operator-precedence expression grammar is fully implemented (landed in commit d5d7b17).
  • Team members unfamiliar with category theory require onboarding on F-algebras and catamorphisms before contributing to the postcondition verification pass.
  • The decidability guarantee holds only for finite algebraic state types; recursive or infinite state types fall outside the verified fragment.