CBPV is structured as a polarized λ-calculus with two main types, "values" (+) and "computations" (-).
[1] Restrictions on interactions between the two types enforce a controlled order of evaluation, similar to monads or CPS.
The calculus can embed computational effects, such as nontermination, mutable state, or nondeterminism.
There are natural semantics-preserving translations from CBV and CBN into CBPV.
Paul Blain Levy formulated and developed CBPV in several papers and his doctoral thesis.
When modelling CBPV in the equational or category theory, such constructs are indispensable.
Levy therefore defines an extended IR, "CBPV with complex values".
[3] Besides modelling, such constructs also make writing programs in CBPV more natural.
Such a decision has no semantic significance because evaluating complex values has no side effects.
Also, it is possible to syntactically convert any computation or closed expression to one of the same type and denotation without complex values.
ADT values are wrapped with return, but force and thunk are also necessary on internal structure.
[2] It is also possible to extend CBPV to model call-by-need, by introducing a M need x. N construct that allows visible sharing.
[8] Egger and Mogelberg justify omitting U on the grounds of streamlined syntax and avoiding the clutter of inferable conversions from computations to values.
This modified calculus is equivalent to a superset of CBPV via a bidirectional semantics-preserving translation.
[7] Ehrhard in contrast omits the F type constructor, making values a subset of computations.
Ehrhard renames computations to "general types" to better reflect their semantics.
[8][9] It can be translated bidirectionally to a subset of a fully-polarized variant of CBPV.