CBPV splits evaluation into value vs computation, offering a powerful foundation that:
1. Unifies CBV/CBN under one semantics-preserving translation,
2. Supports both syntax-level and semantics-level reasoning,
3. Admits a clear categorical interpretation
4. Enhances clarity in handling effects and evaluation order.
CBPV vs Algebraic Effects
CBPV:
• Encodes effects explicitly via separation of values and computations.
• Effects live in the F A (computation) types.
• Uses a monad (or algebraic theory) to model sequencing, effects, etc.
• thunk and force structure define an adjunction: U \dashv F : \mathcal{C} \leftrightarrows \mathcal{V}
Algebraic Effects:
• Treat effects as operations with laws—e.g. get, put, print, choose, etc.
• Combine effects via free algebras, effect handlers, and their corresponding Lawvere theories.
• The computation category C can be built from the free model of an algebraic theory, i.e. it’s the Kleisli category of a monad arising from algebraic operations.
• CBPV doesn’t enforce how the monad arises—so you can plug in any algebraic theory of effects.
• CBPV generalizes and supports algebraic effects seamlessly
One language that uses CBPV is Forsp: https://news.ycombinator.com/item?id=40633003
Is there an FP/Lambda calculus cogniscenti willing to translate this into ordinary humanese?
CBPV splits evaluation into value vs computation, offering a powerful foundation that:
CBPV vs Algebraic EffectsCBPV:
• Encodes effects explicitly via separation of values and computations.
• Effects live in the F A (computation) types.
• Uses a monad (or algebraic theory) to model sequencing, effects, etc.
• thunk and force structure define an adjunction: U \dashv F : \mathcal{C} \leftrightarrows \mathcal{V}
Algebraic Effects:
• Treat effects as operations with laws—e.g. get, put, print, choose, etc.
• Combine effects via free algebras, effect handlers, and their corresponding Lawvere theories.
• Expressed categorically as:
• Effect signatures = operations,
• Algebra = model of those operations.
CBPV naturally supports algebraic effects because:
• The computation category C can be built from the free model of an algebraic theory, i.e. it’s the Kleisli category of a monad arising from algebraic operations.
• CBPV doesn’t enforce how the monad arises—so you can plug in any algebraic theory of effects.
• CBPV generalizes and supports algebraic effects seamlessly
It looks like a lambda calculus with effectful computations that can model imperative programming. I hadn't heard of it before either.
https://en.wikipedia.org/wiki/Call-by-push-value