nLab
thunk-force category

Thunk-force category

Context

Constructivism, Realizability, Computability

Category theory

Thunk-force category

Idea

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 LAL A which could be read as a “thunk of AA” or a “lazy AA”. The thunking arrow θ A:ALA\theta_A : A \to L A embeds a value as a trivial thunk, and the force ϵ A:LAA\epsilon_A : L A \to A forces the evaluation of its thunked input.

The type constructor LL 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 LAL A is equivalent to IAI \rightharpoonup A and θ,ϵ\theta, \epsilon 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.

Definition

A thunk-force category Führmann 99 consists of

such that

  • (Lθ)θ=(θL)θ(L\theta)\theta = (\theta L)\theta
  • θL\theta L is a natural transformation
  • ϵθ=id\epsilon\theta = \id
  • (Lϵ)(θL)=id(L\epsilon)(\theta L) = \id

These conditions on the data (L,ϵ,θ)(L,\epsilon,\theta) can also be rephrased as

The second of these axioms states that ϵθ=id\epsilon\theta = \id and that (Lθ)θ=(θL)θ(L\theta)\theta = (\theta L)\theta, while the first states that θL\theta L is natural and (Lϵ)(θL)=id(L\epsilon)(\theta L) = \id (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.

Thunkable Morphisms

A morphism f:ABf : A \to B represents an effectful program. The presence of the thunk θ\theta allows us to make the distinction between the “pure”/“trivially effectful” programs and those that have non-trivial effects. A morphism f:ABf : A \to B in a thunk-force category is thunkable if (Lf)θ=θf( L f )\theta = \theta f, i.e., θ\theta is “natural with respect to ff”. Note that the condition (Lθ)θ=(θL)θ(L\theta)\theta = (\theta L)\theta in the definition says precisely that θ\theta is thunkable.

The presence of non-thunkable morphisms makes θ\theta fail to be natural overall; naturality of θ\theta 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 TT on a category CC 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 CC.

Relation to Monads

Let (T,η,μ)(T,\eta,\mu) be a monad on a category CC. The Kleisli category of TT is a thunk-force category. Let FGF \dashv G denote the adjunction between CC and the Kleisli category C TC_T. Define L=FGL = FG and ϵ\epsilon the counit of the comonad. To define θ\theta, take Fη:FFTF\eta : F \to FT and, using the fact that FF is an identity-on-objects functor (or at least bijective on objects), treat it as an unnatural transformation from Id C TLId_{C_T}\to L. Then it follows immediately by naturality that every morphism in the image of FF is thunkable.

More explicitly, using the “Kleisli arrow” definition of the Kleisli category, LL is just TT, ϵ A:TATA\epsilon_A : T A \to T A is the identity, and θ A=η TAη A:AT 2A\theta_A = \eta_{T A} \eta_{A} : A \to T^2 A.

In the opposite direction, starting with a thunk-force category KK, we can define the (non-full) subcategory of thunkable morphisms G θKG_\theta K. Since θL\theta L is natural, the image of LL lands in this subcategory, and is right adjoint to the inclusion. Then there is a monad L θL_\theta induced on G θKG_{\theta}K by this adjunction. Furthermore, the thunk-force category generated by the Kleisli category of the monad is equivalent to KK.

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 η\eta of the monad is an equalizer in the following diagram:

1 CηTηTTηT 2 1_{C}\underset{\quad \eta \quad}{\to}T\underoverset{\quad \eta T \quad}{T \eta}{\rightrightarrows}T^2

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.

Applications

Since the thunk LL 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.

References

Thunk-force categories were introduced (under the name “abstract Kleisli categories” in

See also:


  1. 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 May 22, 2020 at 12:26:54. See the history of this page for a list of all contributions to it.