constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A thunk-force category is a category that models call-by-value? programming languages with effects. More commonly, terms in a call-by-value language are modelled as morphisms in the Kleisli category of a strong monad. A thunk-force category axiomatizes the Kleisli category directly and is also called an abstract Kleisli category1. The original category can be recovered from this category if it satisfies certain properties.
The name derives from programming terminology. A thunk means a value that represents an unevaluated computation, which can later be forced to be evaluated and perform its side effects. This is represented by the object which could be read as a “thunk of ” or a “lazy ”. The thunking arrow embeds a value as a trivial thunk, and the force forces the evaluation of its thunked input.
The type constructor and associated thunk and force don’t normally appear as a standalone feature in a call-by-value language, but if the language supports first-class functions, they can be implemented in the usual way as a function of unit input. On the model side, this corresponds to the fact that if a thunk-force category is premonoidal closed, then is equivalent to and can be defined using this structure.
The opposite of a thunk-force category is sometimes called a category equipped with a runnable monad. (Thus, a thunk-force structure could be called a “(co)runnable comonad”, while a runnable monad could be called a “co-thunk-force category”.) Just as a thunk-force category models call-by-value programming, a runnable monad models call-by-name? programming.
A thunk-force category Führmann 99 consists of
such that
These conditions on the data can also be rephrased as
The second of these axioms states that and that , while the first states that is natural and (plus two other properties that follow from the second axiom).
The definition can be extended to monoidal closed thunk-force category to model a context and strong monad Führmann 99.
A morphism represents an effectful program. The presence of the thunk allows us to make the distinction between the “pure”/“trivially effectful” programs and those that have non-trivial effects. A morphism in a thunk-force category is thunkable if , i.e., is “natural with respect to ”. Note that the condition in the definition says precisely that is thunkable.
The presence of non-thunkable morphisms makes fail to be natural overall; naturality of is exactly the same as saying all morphisms are thunkable. This is the case for the Kleisli category of the identity monad. On the other hand, most monads produce many non-thunkable morphisms. For example in the Kleisli category of the maybe monad, which is equivalent to the category of sets and partial functions, the thunkable morphisms are the total functions. As discussed below, most monads on a category used in denotational semantics satisfy an equalizing requirement which means the thunkable morphisms are in one-to-one correspondence to the morphisms of the original category .
Let be a monad on a category . The Kleisli category of is a thunk-force category. Let denote the adjunction between and the Kleisli category . Define and the counit of the comonad. To define , take and, using the fact that is an identity-on-objects functor (or at least bijective on objects), treat it as an unnatural transformation from . Then it follows immediately by naturality that every morphism in the image of is thunkable.
More explicitly, using the “Kleisli arrow” definition of the Kleisli category, is just , is the identity, and .
In the opposite direction, starting with a thunk-force category , we can define the (non-full) subcategory of thunkable morphisms . Since is natural, the image of lands in this subcategory, and is right adjoint to the inclusion. Then there is a monad induced on by this adjunction. Furthermore, the thunk-force category generated by the Kleisli category of the monad is equivalent to .
These constructions exhibit the category of thunk-force categories as a reflective subcategory of the category of monads. The subcategory can be characterized as the monads satisfying the “equalizing requirement”, that the unit of the monad is an equalizer in the following diagram:
Which is in practice often satisfied for monads used in denotational semantics. The definition of the category of morphism of thunk-force categories and proof of this theorem are in Führmann 99 section 5.
Since the thunk is a comonad, the Kleisli category of the comonad is a model of a call-by-name? language. This is a semantic counterpart of the “thunking translation” of call-by-name into call-by-value (described for example in Hatcliff-Danvy 97.
Thunk-force categories were introduced (under the name “abstract Kleisli categories” in
See also:
We prefer the term thunk-force category since it is ambiguous whether Kleisli category refers to the Kleisli category of a monad or a comonad. ↩
Last revised on November 3, 2023 at 13:27:34. See the history of this page for a list of all contributions to it.