Direct models for the computational lambda-calculus

Carsten Führmann car@dcs.ed.ac.uk

Technical Report ECS–LFCS–98-400 Department of Computer Science University of Edinburgh

December 2, 1998

Abstract: We give direct categorical models for the computational lambdacalculus. By ‘direct’ I mean that the model consists of one category together with operators on objects and morphisms for modelling type and program constructors, respectively. Moggi’s λ_{C}-models, for example, are not direct, because the category of program denotations is constructed as the Kleisli category of a monad. We call our models ‘direct λ_{C}-models’. The main result is, loosely speaking, that each λ_{C}-model generates a direct λ_{C}-model, and each direct λ_{C}-model arises in this way. We shall make this precise by showing that the category of direct λ_{C}-models is reflective in the category of λ_{C}-models. From this we shall deduce that we can replace λ_{C}-models by direct λ_{C}-models without losing or gaining generality. We shall also see that the category of direct λ_{C}-models is equivalent to the category of λ_{C}-models that fulfil the equalizing requirement. Moreover, we shall see that we can describe our direct λ_{C}-models with universally quantified equations, which helps reasoning about programs and models. Finally, we shall see that direct λ_{C}-models reveal two kinds of well-behaved programs which are not obvious from λ_{C}-models.

1 Introduction

Cartesian-closed categories validate the β-law, which is false for realistic call-by-value programming languages. (For example, if ⊥ is a looping program, then (λx.λy.y) ⊥ 1 ≠ 1 in a call-by-value language.) By contrast, the theory of Moggi’s λ_{C}-models [Mog88], which is called the computational lambda-calculus, has only equations which are operationally true for a range of realistic call-by-value programming languages. A λ_{C}-model is a category C with finite products together with a strong monad T and T -exponentials—that is, for all objects A and B, an exponential of T B by A. Environments Γ and types A of the computational lambda-calculus denote objects [[Γ]] and [[A]], respectively, in the Kleisli category C_{T}. A sequent Γ ⊢ M : A denotes a morphism [[Γ]] ^{}[[A]] in C_{T}, which in C is a morphism [[Γ]] ^{}T [[A]]. There is a simple example with C = Set and a certain monad T such that, for each set A, we have T A = {⊥} ∪ {⌞a⌟ : a ∈ A}. Then C_{T} is isomorphic to the category of sets and partial functions, where ⊥ serves as ‘undefined’. In general, the monad T can be seen as a parameter that depends on the computational effect—there are lifting monads (partiality), state monads, continuations monads, and so on. (You can find the term formation rules and Moggi’s semantics of the computational lambda-calculus in appendix A.)

Cartesian-closed categories are direct models, by which I mean that the objects and morphisms of the cartesian-closed category give the denotations for types and programs, respectively. λ_{C}-models are not direct, because the category of program denotations is constructed as the Kleisli category of a monad.

Another approach to semantics of call-by-value languages are Freyd categories (see [PT98, PT97]). A Freyd category consists of a category C with finite products, a symmetric premonoidal category K, and an identity-on-objects strict symmetric premonoidal functor F : C ^{}K. (I shall explain symmetric premonoidal categories in this article.) The type and program denotations are objects and morphisms, respectively, of K. Freyd categories are not direct because of the auxiliary category C. As we shall see, λ_{C}-models are equivalent to closed Freyd categories [PT98]. A closed Freyd category is a Freyd category F ⊣ G : K ^{}C together with Kleisli exponentials—that is, for each object A an adjunction F (−) ⊗ A ⊣ A ⇒ (−) : K ^{}C. By ‘equivalent’ I mean an equivalence of categories between an obvious category of λ_{C}-models and an obvious category of closed Freyd categories. (Some vital parts of this equivalence occur in the work of John Power and Edmund Robinson, for example [PR97].)

In this article we define direct models for the computational lambda-calculus. We call these direct λ_{C}-models. I found them by analysing Hayo Thielecke’s ⊗¬-categories [Thi97a, Thi97b], which are direct models for call-by-value languages with higher-order types and continuations. (Roughly speaking, continuations bring the power of jumps into functional programming.) As we shall see, ⊗¬-categories are direct λ_{C}-models with extra structure.

Loosely speaking, the main result in this article is that each λ_{C}-model generates a direct λ_{C}-model, and each direct λ_{C}-model arises in this way. We shall make this precise by showing that the category of direct λ_{C}-models is reflective in the category of λ_{C}-models. From this we shall deduce that we can replace λ_{C}-models by direct λ_{C}-models without losing or gaining generality.

The direct λ_{C}-models are algebraic, by which I mean that we can describe them with universally quantified equations. (If this is not clear enough now, it will become clearer later in this article.) This has some benefits, two of which are

• We can do all reasoning by replacing subexpressions along the axioms.

• We have a simple meta-theory—for example, we can form the free model generated by a set of operators and equations, adjoin indeterminates, and so on.

As we shall see in section 5, direct λ_{C}-models reveal two kinds of well-behaved programs which are not obvious from λ_{C}-models: thunkable programs and central programs.

We define the direct λ_{C}-models by giving structure in three steps:

direct λ_{C}-models thunk-force-⊗-categories thunk-force-categories

(I took the names thunk and force, which stand for certain natural transformations, from ⊗¬-categories.) The hierarchy of direct models corresponds to the following hierarchy by means of three reflections, one at each level:

λ_{C}-models

cartesian computational models monads

2 thunk-force-categories

I shall now describe thunk-force-categories and their relation to monads. As we shall see, each monad generates a thunk-force-category, and every thunk-force-category arises in this way. We shall see also that a thunk-force-category has exactly that part of the structure of its generating monad that we need for semantics.

Definition 1. A thunk-force-category is

• A category K

• A functor L : K ^{}K

• A transformation^{1} thunk : Id ^{}L

• A natural transformation force : L ^{·}^{}Id

such that thunkL is a natural transformation L ^{·}^{}L^{2}, and

[figure: Id; thunk; L; Id; thunk; L; L; thunkL; L^{2}]
[figure: id; id]
[figure: L; thunk; thunkL; L^{2}; Lthunk; Id; force; L; Lforce]

Example. The category Pfn of sets and partial functions. For a set A, we define LA = {⊥} ∪ {⌞a⌟ : a ∈ A}. For a partial function f : A ⇀ B, we define Lf : LA ^{}LB as the total function that sends • ⌞a⌟ to ⌞fa⌟ if f is defined for a

1by a transformation from a functor F : C  D to a functor G : C  D, I mean a map that sends each object A of C to an arrow F A GA

• ⌞a⌟ to ⊥ if f is not defined for a

• ⊥ to ⊥

We define thunkx = ⌞x⌟ and force : LA ⇀ A as the partial function that sends ⌞a⌟ to a and is undefined for ⊥. As you can easily check, this is a thunk-force-category.

Note that thunk-force-categories are algebraic. Note also that L forms a comonad on K with thunkL as the comultiplication and force as the counit.

Definition 2. Tf is defined as the obvious category whose objects are the thunk-force-categories, and whose morphisms are functors that strictly preserve L, thunk, and force.

Definition 3. Monad is defined as the obvious category such that an object is a category C together with a monad on C, and a morphism is a functor that strictly preserves the monad data (which are: the endofunctor, the multiplication, and the unit).

So we consider monads as categories with algebraic structure. Now we turn to the main result for monads and thunk-force-categories. To help understanding the result, let’s recall what a reflection is. In [Lan71] on page 87, Mac Lane writes

A left adjoint to an inclusion functor (of a full subcategory) is called a reflection

We adopt the slightly more general definition by Johnstone [Joh92]:

A reflection is an adjunction for which the counit map ε_{B} is an isomorphism for all B. (This is equivalent to saying that [the right adjoint] G is full and faithful… —see [Mac Lane 1971], p. 88, Theorem 1.)

If there is a reflection with a right adjoint C ^{}D, then I write C ⊲ D.

Theorem 4. There is a reflection

Tf ⊲ Monad

To prove the theorem, we define an intermediate category Adj , which is—as we shall see—equivalent to Monad.

Definition 5. A Kleisli adjunction is an adjunction whose left adjoint is the identity on objects. The category Adj is defined as follows. Objects are Kleisli adjunctions. A morphism from F ⊣ G : K ^{}C to F′ ⊣ G′ : K′ ^{}C′ is a pair of functors h : C ^{}C′ and H : K ^{}K′ such that h strictly preserves the unit, H strictly preserves the counit, and

[figure: C; h; C′; C; h; C′; K; F; H; K′; F; ′; K; G; H; K′; G; ′]

You can easily check the following: If the two squares in definition 5 commute, then h preserves the unit if and only if H preserves the counit, and either is equivalent to saying that h and H together strictly preserve the adjunction iso.

Lemma 6. The construction of the Kleisli category extends to an equivalence

Monad ≃ Adj

Proof. For an object C = (C, T) of Monad, the required adjunction is the well-known adjunction F_{T} ⊣ G_{T} : C_{T} ^{}C like in [Lan71]. Thus we get an obvious functor Kleisli : Monad ^{}Adj For a Kleisli adjunction F ⊣ G : K ^{}C of Adj with unit η and counit ε, the required monad has the functor GF : C ^{}C, the unit η and the multiplication GεF. Thus we get an obvious functor X : Adj ^{}Monad Trivially, we have XKleisli = Id_{Monad}. Now we prove that KleisliX ≅ Id_{Adj} . Suppose that F ⊣ G : K ^{}C is a Kleisli adjunction. Applying KleisliX yields F_{T} ⊣ G_{T} : C_{T} ^{}C, where T is the monad induced by the adjunction F ⊣ G. So we have the unique comparison functor ! : C_{T} ^{}K like in [Lan71], page 144, theorem 2, where ! is called L. For all objects A we have !A = A, and for all elements f of C_{T} (A, B), which is equal to C(A, GB), we have !f = f^{♭} where ♭ is the obvious iso C(A, GB) ≅ K(F A, B). Because F is the identity on objects, ! is an isomorphism of categories (proving this is left as an exercise). Let E_{F ⊣G} = (Id_{C},!). As you can easily check, E_{F ⊣G} is an iso from F_{T} ⊣ G_{T} to F ⊣ G. It remains to prove that E is natural in F ⊣ G. This is left as an exercise.

The next definition is the key to proving theorem 4:

Definition 7. A morphism f : A ^{}B of a thunk-force-category K is called thunkable if

A \overline{thunk_{}}LA

[figure: B; f; thunk; LB; Lf]

ΘK is the subcategory of K determined by all objects and the thunkable morphisms.

In Pfn, as you can easily check, the thunkable morphisms are the total functions.

Proof of theorem 4. By lemma 6 it is enough to prove a reflection Tf ⊲ Adj . We shall define a reflection

Tf [figure: i; ⊤; \underline{j}] Adj

First we define i. Suppose that K is a thunk-force-category, and that inc is the inclusion ΘK ^{}K. As you can easily check, we have a Kleisli adjunction

ΘK [figure: inc; ⊥; \underline{L}] K

with unit thunk and counit force. Let iK be this adjunction. Now for the morphism part of i. Suppose that H : K ^{}K′ is a morphism of thunk-force-categories. Because H strictly preserves L and thunk, H preserves thunkable morphisms. So H has a restriction h : ΘK ^{}ΘK′. Let iH = (h, H). This is obviously a morphism of Adj .

Now we define j. Suppose that F ⊣ G : K ^{}C, with unit η and counit ε, is a Kleisli adjunction. Now we define

L =_{def} F G
thunk =_{def} F η
force =_{def} ε

and let j(F ⊣ G) = (K, L, thunk, force). As you can easily check, j(F ⊣ G) is a thunkforce-category. The morphism part of j is obvious.

As you can easily check, ji = Id_{Tf} . Therefore we define the counit ji ^{}Id_{Tf} of the reflection as the identity on Id_{Tf} .

Now for the unit of the reflection. Suppose that F ⊣ G : K ^{}C is a Kleisli adjunction. Then ij(F ⊣ G) is the adjunction inc ⊣ L : K ^{}ΘK. Suppose that f is a morphism of C. Then the square expressing that F f is thunkable is the image of the square f; η = η; GF f under F. So F has a corestriction to ΘK. We define U_{F ⊣G} = (F : C ^{}ΘK, Id_{K}). As you can easily check, U_{F ⊣G} is a morphism from F ⊣ G : K ^{}C to ij(F ⊣ G). As you can check by simple arrow chasing, U_{F ⊣G} is natural in F ⊣ G.

It remains to check the triangular identities of the reflection. Because the counit is the identity, we need to check only that U_{iK} = Id_{iK} and jU_{F ⊣G} = Id_{j(F ⊣G)}. Checking these two equations is straightforward.

We shall now see that Moggi’s semantics of the computational lambda-calculus uses the monad only via the generated L, thunk, and force. Suppose that C is a λ_{C}-model whose monad is T = (T, μ, η). Let K be the thunk-force-category that results from sending C through the right adjoint of the reflection Monad ⊲ Tf . So

K = C_{T}
L = F_{T} G_{T}
thunk = F_{T} η
force_{A} = id_{T A}^{C}

As you can easily check, these for equations translate Moggi’s two semantic rules of the computational lambda-calculus that use only T, μ, and η, into

[[Γ ⊢ M : A]] = f : Γ ^{}A
[[Γ ⊢ [M] : T A]] = Γ ^{thunk}^{}LΓ ^{Lf}^{}LA

[[Γ ⊢ M : T A]] = f : Γ ^{}A
[[Γ ⊢ μ(M) : A]] = Γ ^{f}^{}LA ^{force}^{}A

So thunk-force-categories have all the structure that we need from monads. Moreover, thunk-force-categories don’t have more structure than we need, because L, thunk, and force are denotable. For thunk and force, this is obvious. To see it for L, suppose that x : A ⊢ M : B denotes f : A ^{}B. Then

y : LA ⊢ [let x = μ(y) in M] : LB

denotes Lf, as becomes clear from the semantics of let in the next section. So we can conclude that thunk-force-categories have exactly the structure that we need from a monad.

Because of the reflection Tf ⊲ Monad, thunk-force-categories correspond to a full subcategory of Monad. We shall now see which subcategory.

Definition 8. A monad T with unit η fulfils the equalizing requirement if, for each object A, η_{A} is an equalizer of η_{T A} and T η_{A}. The category Monad_{eq} is defined as the full subcategory of Monad determined by the objects (C, T) such that T fulfils the equalizing requirement.

Theorem 9. There is an equivalence of categories

Monad_{eq} ≃ Tf

To prove this theorem, we use an intermediate category Adj_{eq}.

Definition 10. Adj_{eq} is defined as the full subcategory of Adj determined by the objects F ⊣ G such that, if η stands for the unit, then for each object A, η_{A} is an equalizer of η_{GF A} and GF η_{A}.

Lemma 11. There is an equivalence of categories

Monad_{eq} ≃ Adj_{eq}

This follows directly from lemma 6.

Lemma 12. Suppose that F ⊣ G : K ^{}C is a Kleisli adjunction with defining isomorphism ♯ : K(F A, B) ≅ C(A, GB). Then an element f of K(A, B) is thunkable if and only if

[figure: A; f^{♯}; GF B; GF B; f^{♯}; GF η; GF GB; η]

Proof. We apply the inverse of ♯ to either path of the diagram. As you can easily check, we get

[figure: A; F η; F GA; B; f; F η; F GB; F Gf]

This is the square that states that f is thunkable.

Lemma 13. An object F ⊣ G : K ^{}C of Adj is in Adj_{eq} if and only if F is faithful and every thunkable morphism of K is in the image of F.

Proof. Suppose that F ⊣ G : K ^{}C is a Kleisli adjunction. For the ‘only if’, let F ⊣ G be an object of Adj_{eq}. Suppose that f is a thunkable element of K(A, B). By lemma 12, we have f^{♯}; η_{GF B} = f^{♯}; GF η_{B}. Because η_{B} is an equalizer of η_{GF B} and GF η_{B}, there is a unique g : A ^{}B such that g; η_{B} = f^{♯}. As you can easily check, the inverse ♭ of ♯ sends the equation g; η_{B} = f^{♯} to F g = f. So every thunkable morphism is the image under F of exactly one morphism. Because all morphisms in the image of F are thunkable, F is faithful.

Now for the ‘if’. Because η is natural, we have

η_{B}; η_{GF B} = η_{B}; GF η_{B}

for all objects B. Let g ∈ C(A, T B) such that

g; η_{GF B} = g; GF η_{B}

We need a unique f ∈ C(A, B) such that f; η = g. As you can easily check, ♭ sends the equation f; η = g to F f = g^{♭}. By lemma 12, g^{♭} is thunkable. So there is exactly one solution f.

Proof of theorem 9. By lemma 11 it is enough to prove that Tf ≃ Adj_{eq}. First we prove that i : Tf ^{}Adj has a corestriction to Adj_{eq}. Suppose that K is a thunk-force-category. By definition iK is equal to inc ⊣ L : K ^{}ΘK. This, by lemma 13, is an object of Adj_{eq}. It remains to prove that the unit U of the reflection Tf ⊲ Adj restricts to an iso Id_{Adj_{eq}} ≅ ij. Because U_{F ⊣G:K C} = (F : C ^{}ΘK, Id_{K}), this amounts to proving that F : K ^{}ΘK is an iso. This follows directly from lemma 13.

3 thunk-force-⊗-categories

In this section, we shall define thunk-force-⊗-categories—the direct models that correspond to cartesian computational models. Our definition of thunk-force-⊗-categories depends on symmetric premonoidal categories. The latter generalise symmetric monoidal categories in that the product ⊗ does not have to be a bifunctor, but only a functor in either argument. We shall now introduce symmetric premonoidal categories by means of binoidal categories. (For more on symmetric premonoidal categories, see [PR97].) Definition 14. A binoidal category is

• A category C

• For each object A, a functor A ⊗ (−) : C ^{}C

• For each object B, a functor (−) ⊗ B : C ^{}C such that for all objects A and B

(A ⊗ (−))(B) = ((−) ⊗ B)(A)

For the joint value, we write A ⊗ B, or short AB. Definition 15. A morphism f : A ^{}A′ of a binoidal category is called central if for each g : B ^{}B′

[figure: AB; fB; A′B; AB′; Ag; fB′; A′B′; A′g; AB; fB; A′B; AB′; Ag; fB′; A′B′; A′g]

The centre of a binoidal category is the subcategory of all objects and central morphisms. Definition 16. A symmetric premonoidal category is

• A binoidal category C

• An object I of C

• Four natural isomorphisms A(BC) ≅ (AB)C, IA ≅ A, AI ≅ A, and AB ≅ BA with central components that fulfil the coherence conditions known from symmetric monoidal categories.

The symmetric monoidal categories are the symmetric premonoidal categories that have only central morphisms. As you can easily check, the natural associativity implies that A ⊗ (−) and (−) ⊗ A preserve central morphisms. Therefore Proposition 17. The centre of a symmetric premonoidal category is a symmetric monoidal category.

Definition 18. Suppose that C and D are symmetric premonoidal categories. Then a functor from C to D is strict symmetric premonoidal if it sends central morphisms to such and strictly preserves the multiplication, the unit, and the four structural isomorphisms.

Definition 19. A thunk-force-⊗-category K is

• A thunk-force-category K

• A symmetric premonoidal structure on K

• Finite products on ΘK that agree with the symmetric premonoidal structure.

such that ΘK is a subcategory of the centre.

Example. We continue our example Pfn. Because ΘPfn = Set the finite products are obvious. For f : A ⇀ A′ and g : B ^{}B′ we define f ⊗ g : A ⊗ A′ ^{}B ⊗ B′ as the partial function that sends (a, b) to (f(a), g(b)) if f is defined for a and g is defined for b, and is undefined for (a, b) otherwise.

Obviously a thunk-force-⊗-category is a Freyd category with C = ΘK and the inclusion ΘK ^{}K as F. Now we add three rules to our semantics of λ_{C}-terms, which so far has rules for μ and [−] (let δ be the diagonal of the cartesian product of ΘK):

[[x_{1} : A_{1}, …, x_{n} : A_{n} ⊢ x_{i} : A_{i}]] = π_{i} : A_{1} ⊗ ⋯ ⊗ A_{n}  ^{}A_{i}

[[Γ ⊢ M : A]] = f : Γ ^{}A [[Γ ⊢ N : B]] = g : Γ ^{}B
[[Γ ⊢ (M, N) : A ∗ B]] = [figure: Γ; δ; Γ ⊗ Γ; f ⊗ Γ; A ⊗ Γ; A ⊗ g; A ⊗ B]
[[Γ ⊢ M : A]] = f : Γ ^{}A [[Γ, x : A ⊢ N : B]] = g : Γ ⊗ A ^{}B
[[Γ ⊢ let x = M in N : B]] = [figure: Γ; δ; Γ ⊗ Γ; Γ ⊗ f; Γ ⊗ A; g; B]

We shall now define two useful concepts for thunk-force-⊗-categories. (For an object A of a thunk-force-⊗-category K, let !_{A} : A ^{}I be the unique element of (ΘK)(A, I).)

Definition 20. Suppose that f : A ^{}B is morphism of a thunk-force-⊗-category. f is copyable if,

[figure: A; δ; AA; B; f; δ; BB; f; f]

f is discardable if

[figure: A; !; I; B; f; !; I; id]

The next proposition has two purposes. First, it helps checking that a structure is a thunk-force-⊗-category. Second—as we shall see—it implies that thunk-force-⊗-categories are algebraic.

Proposition 21. Suppose that K is a thunk-force-category together with a binoidal product, an object I, and transformations δ_{A} : A ^{}AA and !_{A} : A ^{}I. Then K determines a thunk-force-⊗-category if and only if

1. The components of thunk are central, and all morphisms of the form Lf are central.

2. All morphisms of the form A⊗thunk, thunk ⊗A, A⊗Lf, and Lf ⊗A are thunkable.

3. The components of thunk, and all morphisms of the form Lf, are copyable and discardable.

4. The components of δ and ! are thunkable.

5. δ and ! determine a comonoid.

6. We have

[figure: AB; δ; (AB)(AB); id; AB; ππ′; where; {; π; =; AB; A!; AI ≅ A; π′; =; AB; !B; IB ≅ B]

Proof. First we check the ‘only if’. Conditions 1, 2 and 3 hold because the components of thunk are in ΘK, and all morphisms of the form Lf are in ΘK. The remaining conditions are obvious.

Now for the ‘if’. Condition 1 implies that all thunkable morphisms are central. To see this, let f ∈ ΘK(A, B). Then for every g ∈ K(A′, B′) we have

A ⊗ g; f ⊗ B′ = A ⊗ g; f ⊗ B′; thunk ⊗ B′; force ⊗ B′
= A ⊗ g; thunk ⊗ B′; Lf ⊗ B′; force ⊗ B′
= thunk ⊗ A′; Lf ⊗ A′; LB ⊗ g; force ⊗ B′
= f ⊗ A′; thunk ⊗ A′; LB ⊗ g; force ⊗ B′
= f ⊗ A′; B ⊗ g; thunk ⊗ B′; force ⊗ B′
= f ⊗ A′; B ⊗ g

Condition 2 implies that ΘK is closed under ⊗. To see this, let f ∈ ΘK(A, B). Then

A ⊗ f; thunk = A ⊗ f; thunk; L(A ⊗ thunk); L(A ⊗ force)
= A ⊗ f; A ⊗ thunk; thunk; L(A ⊗ force)
= A ⊗ thunk; A ⊗ Lf; thunk; L(A ⊗ force)
= A ⊗ thunk; thunk; L(A ⊗ Lf); L(A ⊗ force)
= A ⊗ thunk; thunk; L(A ⊗ force); L(A ⊗ f)
= thunk; L(A ⊗ thunk); L(A ⊗ force); L(A ⊗ f)
= thunk; L(A ⊗ f)

So ΘK and ⊗ together determine a binoidal subcategory of the centre. In particular, ⊗ determines a bifunctor ΘK × ΘK ^{}ΘK. Condition 3 implies that every thunkable morphism is copyable and discardable (the proof is left as an exercise). The remaining conditions imply that ΘK together with ⊗, I, δ, and ! is a category with finite products (the proof is left as an exercise). Every category with finite products determines a symmetric monoidal category (see [Lan71], p. 159). Because the symmetric monoidal product of ΘK agrees with the binoidal product on K, the symmetric monoidal structure on ΘK extends to a symmetric premonoidal structure on K.

You can easily express all conditions in proposition 21 by equations that are all-quantified over hom-sets. So we have the following corollary:

Corollary 22. thunk-force-⊗-categories are algebraic.

Now we turn to generalising theorem 4, which states that there is a reflection Monad ⊲ Tf . We shall define a category Tf ⊗ of thunk-force-⊗-categories, and a category Ccm of computational cartesian models, and prove that there is a reflection Tf ⊗ ⊲ Ccm.

Definition 23. Tf ⊗ is defined as the obvious category formed by the thunk-force-⊗- categories and the functors that strictly preserve all operators.

Note that it is not obvious that morphisms of thunk-force-⊗-categories preserve central maps. For suppose that F : K ^{}K′ is a morphism of thunk-force-⊗-categories, and f is a central morphism of K. That f is central means that f commutes in the sense of definition 15 with all morphisms g of K. Therefore, F f commutes with all morphisms of the form F g. But K′ may have morphisms that are not in the image of F. Fortunately, we have the following proposition:

Proposition 24. Suppose that K is a thunk-force-⊗-category. A morphism f ∈ K(A, A′) is central if for all B ∈ Ob(K)

A ⊗ LB f ⊗ LB^{}A′ ⊗ LB

[figure: A ⊗ B; A ⊗ force_{B}; f ⊗ B; A′ ⊗ B; A′ ⊗ force_{B}]

Proof. Let g ∈ K(B, B′). Then g = thunk; force; g = thunk; Lg; force. Because thunk and Lg are thunkable and therefore central, they commute with f. Because f commutes with force too, f commutes with g.

Because morphisms of thunk-force-⊗-categories preserve force, morphisms of thunk-force- ⊗-categories preserve central morphisms. So we get the following corollary:

Corollary 25. Morphisms of thunk-force-⊗-categories are strict symmetric premonoidal functors.

Definition 26. Ccm is defined as the obvious category formed by cartesian computational models and the morphisms of Monad that strictly preserve the finite products and the strength.

Theorem 27. There is a reflection

Tf ⊗ ⊲ Ccm

To prove this, we use an intermediate category. First we describe its objects.

Definition 28. A I-closed Freyd category consists of a category C with finite products, a symmetric premonoidal category K, and an adjunction F ⊣ G : K ^{}C such that F is an identity-on-objects strict symmetric premonoidal functor.

We call them I-closed Freyd categories because in a Freyd category F : C ^{}K the functor F has a right adjoint if and only if F (−) ⊗ I has a right adjoint, and therefore I-closed Freyd categories herald closed Freyd categories.

Definition 29. The category IcFreyd is defined as follows. The objects are the I-closed Freyd categories. A morphism from F ⊣ G : K ^{}C to F′ ⊣ G′ : K′ ^{}C′ is a pair (h, H) that consists of a functor h : C ^{}C′ that strictly preserves finite products, and a strict symmetric premonoidal functor H : K ^{}K′ such that (h, H) is a morphism of Kleisli adjunctions.

Lemma 30. There is a reflection

Tf ⊗ ⊲ IcFreyd

Proof. We extend the reflection j ⊣ i : Tf ^{}Adj to a reflection j ⊣ i : Tf ⊗

IcFreyd. First we show that i extends to a functor Tf ⊗ ^{}IcFreyd. Let K be a thunk-force-⊗-category. By definition, iK is the adjunction inc ⊣ L : K ^{}ΘK. This is obviously an I-closed Freyd category. For a morphism H : K ^{}K′ of thunkforce-⊗-categories, iH : iK ^{}iK′ is obviously a morphism of I-closed Freyd categories.

Now we show that j extends to a functor IcFreyd ^{}Tf ⊗. Let f ⊣ G : K ^{}C be an I-closed Freyd category, where η is the unit and ε is the counit. By definition, for j(F ⊣ G) is K together with L = F G, thunk = F η, and force = ε. For each object A, let δ_{A} and !_{A} be the images under F of the diagonal A ^{}AA and the unique arrow A ^{}1, respectively. With proposition 21 we prove that the thunk-force-category K together with ⊗, 1, δ, and ! determines a thunk-force-⊗-category. Condition 1 of proposition 21 holds because F, which is a strict symmetric premonoidal functor, preserves central morphisms, and thunk and Lf are in the image of F. Condition 4 holds because all morphisms in the image of F are thunkable, as you can easily check. Condition 2 holds because

A ⊗ thunk = F A ⊗ F η = F (A ⊗ η)
A ⊗ Lf = F A ⊗ F Gf = F (A ⊗ f)

Condition 3 holds because all morphisms in the image of F are copyable and discardable, as you can easily check. Checking the remaining conditions is straightforward—I leave it away here. Checking that j sends morphisms of I-closed Freyd categories to morphisms of thunk-force-⊗-categories is straightforward—I leave it away here.

As you can easily check, we have ji = Id_{Tf ⊗}. We define the counit ji ^{}Id_{Tf ⊗} as the identity. Now for the unit. Let’s recall the unit U of the reflection Tf ⊲ Adj : For a Kleisli adjunction F ⊣ G, we have U_{F ⊣G} = (F : C ^{}ΘK, Id_{K}). It remains to prove that, if F ⊣ G is an I-closed Freyd category, then U_{F ⊣G} forms a morphism of I-closed Freyd categories. This amounts to checking that F : C ^{}ΘK strictly preserves finite products, which is obvious. The naturality of the unit, and the triangular equations, follow from the corresponding results for the reflection Tf ⊲ Adj .

Lemma 31. The construction of the Kleisli category forms an equivalence

Ccm ≃ IcFreyd

Proof. By lemma 6, we have functors Kleisli : Monad ^{}Adj and X : Adj ^{}Monad that form an equivalence. First we extend Kleisli to a functor Ccm ^{}IcFreyd. Let C = (C, T) be a computational cartesian model, where T = (T, μ, η) and t is the strength. We need a symmetric premonoidal structure in C_{T}. For objects A and B, let

A ⊗ B =_{def} A × B

For an object A and element f of C_{T} (B, B′), which is equal to C(B, T B′), let

A ⊗ f =_{def} [figure: A × B; A × f; A × T B′; t; T (A × B′)]

and f ⊗ A symmetrically. Now ⊗ forms a symmetric premonoidal structure on C_{T} such that F_{T} ⊣ G_{T} : C_{T} ^{}C is an I-closed Freyd category (The proof is left as an exercise, as well as the proof that this gives a functor Ccm ^{}IcFreyd).

Now we extend X to a functor X : IcFreyd ^{}Ccm. Let F ⊣ G : K ^{}C be an I-closed Freyd category with iso ♯ : K(F A, B) ≅ C(A, GB) and counit ε. By definition, X takes the I-closed Freyd category to (C, T), where T = (GF, GεF, η). What we still need is the strength t : A × T B ^{}T (A × B). Let

t =_{def} (A ⊗ ε)^{♯}

This gives us a computational cartesian model (the proof is left as an exercise, as well as the proof that this gives a functor X : Ccm ^{}IcFreyd).

To see that the two extended functors are inverse up to natural iso, it is enough to check that the two natural isos in the proof of lemma 6 preserve the new structure. The proof is left as an exercise).

Proof of theorem 27. By composition of the reflections Tf ⊗ ⊲ IcFreyd and IcFreyd ≃ Ccm.

Theorem 32. Moggi’s semantics of the computational lambda-calculus in a λ_{C}-model C agrees with the semantics in the thunk-force-⊗-category generated by C.

Proving this amounts to checking the semantic rules for variables, pairs, and let. Checking this is left as an exercise.

Let Ccm_{eq} be the full subcategory of Ccm determined by the computational cartesian models whose monad fulfils the equalizing requirement. The following theorem follows directly from theorems 9 and 27:

Theorem 33. There is an equivalence of categories

Ccm_{eq} ≃ Tf ⊗

4 Direct λ_{C}-models

Finally, we shall define direct λ_{C}-models—the direct models that correspond to λ_{C}-models.

Definition 34. A direct λ_{C}-model is a thunk-force-⊗-category K together with, for each object A, a functor A ⇒ (−) : K ^{}ΘK and an adjunction

λ : K(B ⊗ A, C) ≅ (ΘK)(B, A ⇒ C)

Example. For Pfn, we define

A ⇒ (−) = Pfn(A, −) : Pfn ^{}Set

(recall that ΘPfn = Set). λ is obvious.

A direct λ_{C}-model K is obviously a closed Freyd category with C = ΘK and F as the inclusion. We write apply for the counit (A ⇒ B) ⊗ A ^{}B of the Kleisli exponentials, and pair for the unit A ^{}B ⇒ (A ⊗ B). Here come the remaining two rules of our semantics of the computational lambda-calculus in direct λ_{C}-models.

{[[Γ, x : A ⊢ M : B]] = f : Γ ⊗ A ^{}B \atop [[Γ ⊢ λx : A.M : A ⇒ B]] = λf : Γ ^{}A ⇒ B}

[[Γ ⊢ M : A ⇒ B]] = f : Γ ^{}A ⇒ B [[Γ ⊢ N : A]] = g : Γ ^{}A
[[Γ ⊢ MN : B]] = [figure: Γ; δ; ΓΓ; fΓ; (A ⇒ B)Γ; (A ⇒ B)g; (A ⇒ B)A; apply; B]

The next proposition helps checking that a structure is a direct λ_{C}-model. We shall need the proposition in later proofs.

Proposition 35. Suppose that K is a thunk-force-⊗-category together with a functor A ⇒ (−) : K ^{}K, a natural transformation apply : (A ⇒ B)A ^{·}^{}B, and a transformation pair : B ^{}A ⇒ (BA). Then for each object A there is an adjunction A ⊗ (−) ⊣ A ⇒ (−) : K ^{}ΘK with unit pair and counit apply if and only if

1. All components of pair are thunkable., and all morphisms of the form A ⇒ f are thunkable.

2. pair is natural for all components of thunk, and for all morphisms of the form Lf.

3. We have

[figure: AB; pairB; (B ⇒ (AB))B; B ⇒ A; pair; B ⇒ ((B ⇒ A)B)]
[figure: id; id]
[figure: AB; apply; B ⇒ A; B ⇒ apply]

Proof. The ‘only if’ is obvious. The non-obvious part of the ‘if’ is to prove that condition 2 implies that pair is natural for all thunkable morphisms. To see this, let f : A ^{}A′ be a thunkable morphism, and B an object for which we consider the adjunction (−) ⊗ B ⊣ B ⇒ (−). Then

f; pair = f; pair; B ⇒ (thunkB); B ⇒ (forceB)
= f; thunk; pair; B ⇒ (forceB)
= thunk; Lf; pair; B ⇒ (forceB)
= pair; B ⇒ (thunkB); B ⇒ ((Lf)B); B ⇒ (forceB)
= pair; B ⇒ (fB); B ⇒ (thunkB); B ⇒ (forceB)
= pair; B ⇒ (fB)

Because thunk-force-⊗-categories are algebraic, and all conditions in proposition 35 are algebraic, we have the following corollary:

Proposition 36. Direct λ_{C}-models are algebraic.

Definition 37. We define three categories as follows:

• Dλ_{C} is defined as the obvious category formed by direct λ_{C}-models and the morphisms of thunk-force-⊗-categories that preserve Kleisli exponentials.

• λ_{C} is defined as the obvious category formed by λ_{C}-models and the morphisms of computational cartesian models that preserve T -exponentials.

• CFreyd is defined as the obvious category formed by closed Freyd categories and morphisms of I-closed Freyd categories that strictly preserve Kleisli exponentials.

Theorem 38. There is a reflection

Dλ_{C} ⊲ CFreyd

Proof. We extend the reflection j ⊣ i : Tf ⊗ ^{}IcFreyd to a reflection j ⊣ i : Dλ_{C} ^{}CFreyd Extending i is obvious: For a direct λ_{C}-model K, iK is inc ⊣ L : K ^{}ΘK. Now for j. Let F ⊣ C : K ^{}C be a closed Freyd category. Let

A ⇒′ (−) =_{def} K ^{A⇒(−)}^{}C ^{F}^{}ΘK
pair′ =_{def} F pair
apply′ =_{def} apply

With proposition 35 we prove that the new data determine the required adjunction. Condition 1 holds because all morphisms of the form F g are thunkable. Condition 2 holds because, as you can easily check, pair′ is natural for all morphisms of the form F g. Checking the remaining conditions of proposition 35 is very easy—I leave it away here.

Obviously we have ji = Id_{Dλ_{C}} . So it remains to check that the unit of the reflection extends. This means checking that for each direct λ_{C}-model F ⊣ G : K ^{}C, the morphism of I-closed Freyd categories (F, Id_{K}) into inc ⊣ L : K ^{}ΘK preserves Kleisli exponentials. Checking this is straightforward and left as an exercise.

Theorem 39. The construction of the Kleisli category forms an equivalence

CFreyd ≃ λ_{C}

Proof. By lemma 31 we have functors Kleisli : Ccm ^{}IcFreyd and X : IcFreyd ^{}Ccm that form an equivalence of categories. First we extend Kleisli to a functor λ_{C} ^{}CFreyd. Let C be a λ_{C}-model whose monad is T = (T, μ, η) and whose T -exponentials are determined by

λ : C(AB, T C) ≅ C(A, (T C)^{B})

Let C′ be the full subcategory of C whose objects are those of the form T A. For f ∈ C′(T A, T A′) and an object B, let

f^{B} =_{def} λ ((T A)^{B} × B ^{ev}^{}T A ^{f}^{}T A′)

As you can easily check, (−)^{A} determines a functor C′ ^{}C. Let

A ⇒ (−) =_{def} (G_{T} (−))^{A}

Now we claim that λ determines a natural iso

λ : C_{T} (F A ⊗ B, C) ≅ C(A, B ⇒ C)

What we must check is the naturality of λ. Checking this is straightforward—I leave it away here.

Now we extend X to a functor CFreyd ^{}λ_{C} . Suppose that F ⊣ G : K ^{}C is a direct λ_{c}-model, and ♯ : K(F A, C) ≅ C(A, GC) is the obvious adjunction iso. By definition, the computational cartesian model X(F ⊣ G) has the monad T = (GF, GεF, η). Let

(T B)^{A} =_{def} A ⇒ B
ev =_{def} apply^{♯}

This determines T -exponentials on C—checking this is left as an exercise. Checking the morphism part of X is straightforward, so I leave it away here.

Obviously XKleisli : λ_{C} ^{}λ_{C} doesn’t change T -exponentials. Therefore XKleisli = Id_{λ_{C}} .

It remains to prove that the components of the natural iso KleisliX ≅ Id_{IcFreyd} preserve Kleisli exponentials. Let F ⊣ G : K ^{}C be a direct λ_{c}-model, and let ♭ : C(A, GB) ≅ K(F A, B) be the obvious natural iso. Applying KleisliX yields the direct λ_{c}-model F_{T} ⊣ G_{T} : C_{T} ^{}C where T = (GF, GεF, η). The component of the iso KleisliX ≅ Id_{IcFreyd} at F ⊣ G is (Id_{C},!) where ! is the unique comparison functor C_{T} ^{}K. Now we prove that (Id_{C},!) preserves Kleisli exponentials. For every object B let B ⇒_{T} (−) and B ⇒ (−) be the Kleisli exponential functors of F_{T} ⊣ G_{T} and F ⊣ G, respectively, and let λ_{T} and λ be the natural isos for the respective Kleisli exponentials. First we prove that

Id_{C}(B ⇒_{T} (−)) = !B ⇒!(−)

For an object A we get

Id_{C}(B ⇒_{T} A) = B ⇒_{T} A = (T A)^{B} = B ⇒ A = !B ⇒!A

For f ∈ C_{T} (A, A′) we have

Id_{C}(B ⇒_{T} f) = (G_{T} f)^{B} = (G(f^{♭}))^{B}
!B ⇒!f = B ⇒ f^{♭}

We prove that (G(f^{♭}))^{B} = B ⇒ f^{♭} by checking

[figure: (T A)^{B} × B; ev; T A; (T A′)^{B} × B; (B ⇒ f^{♭}) × B; ev; T A′; G(f^{♭})]

This is true because

(ev; G(f^{♭}))^{♭} = F (ev; G(f^{♭})); ε = F (apply^{♯}; G(f^{♭})); ε
= F (η; Gapply; G(f^{♭})); ε = F η; F Gapply; F G(f^{♭}); ε
= thunk; Lapply; L(f^{♭}); force = thunk; force; apply; f^{♭}
= apply; f^{♭} = F (B ⇒ f^{♭}) ⊗ B; apply
= F ((B ⇒ f^{♭}) × B); ev^{♭} = F ((B ⇒ f^{♭}) × B); F ev; ε
= F ((B ⇒ f^{♭}) × B; ev); ε = ((B ⇒ f^{♭}) × B; ev)^{♭}

It remains to prove that for each f ∈ C_{T} (A × B, C)

Id_{C}(λ_{T} f) = λ(!f)

We prove this by checking

(T C)^{B} × B \overline{ev^{}}T C
[figure: f]
A × B^{λ(!f) × B }

This is true because

(λ(!f) × B; ev)^{♭} = (λ(f^{♭}) × B; ev)^{♭} = F (λ(f^{♭}) × B); apply = F (λ(f^{♭})) ⊗ B; apply = f^{♭}

By composing the reflections Dλ_{C} ⊲ CFreyd and CFreyd ≃ λ_{C} we get

Theorem 40. There is a reflection

Dλ_{C} ⊲ λ_{C}

Theorem 41. Moggi’s semantics of the computational lambda-calculus in a λ_{C}-model C is equal to the semantics in the direct λ_{C}-model generated by C.

Proving this amounts to checking the semantic rules for lambda abstraction and application. Checking this is left as an exercise.

Let λ_{C}_{eq} be the full subcategory of λ_{C} determined by the λ_{C}-models whose monads fulfil the equalizing requirement. Let CFreyd_{eq} be the subcategory of CFreyd determined by the closed Freyd categories whose induced monads fulfil the equalizing requirement The following theorem follows directly from theorems 9, 38, and 39:

Theorem 42.

Dλ_{C} ≃ CFreyd_{eq} ≃ λ_{C}_{eq}

Proposition 43. Let K be a direct λ_{C}-model. Then L and I ⇒ (−) are naturally isomorphic, and we have

[figure: LA; ≅; I ⇒ A; LA; ≅; I ⇒ A]
[figure: λr]
[figure: A; force; apply; I ⇒ AI; ≅; A; thunk; pair; I ⇒ (AI); ≅]

Proof. As you can easily check, each thunk-force-category K has an adjunction

K(A, B) ≅ (ΘK)(A, LB)

with unit thunk and counit force. So we have a natural iso

(ΘK)(A, LB) ≅ K(A, B) ≅ K(A ⊗ I, B) ≅ (ΘK)(A, I ⇒ B)

Checking the two diagrams is left as an exercise.

Therefore, the program transformation that replaces all occurrences of T A with I ⇒ A, all occurrences of [M] with λx : I.M, and all occurrences of μ(M) with M∗ preserves meaning up to natural isomorphism. So T, μ(−), and [−] are redundant. But we may want to keep the three. To see this, note that we want to consider languages with many computational effects. Therefore we may need models with one thunk-force-structure per computational effect. So the codomain of λ is no longer obvious. In particular, the functor I ⇒ (−) may not be isomorphic to the functor L of any computational effect.

5 Thunkable and central programs

By definition of a thunk-force-⊗-category, every thunkable morphism is central. The converse does not hold: In Pfn, for example, every partial function is central, but only the total functions are thunkable. As we shall see later, in ⊗¬-categories all central morphisms are thunkable, but not all morphisms are central. Let’s see now when the denotation of a program is thunkable and central, respectively. Suppose that K is a direct λ_{C}-model K, and that Γ ⊢ M : A denotes f : Γ ^{}A in K. Then, as you can easily check,

Γ ⊢ let x = M in [y] : LA denotes Γ ^{f}^{}A ^{thunk}^{}LA
Γ ⊢ [M] : LA denotes A ^{thunk}^{}LA ^{Lf}^{}LB

Now suppose that Δ is an environment that doesn’t share variables with Γ, and Δ ⊢ N : B denotes g : Δ ^{}B. Then the two sequents

Γ, Δ ⊢ let x = M in let y = N in (x, y) : A ∗ B
Γ, Δ ⊢ let y = N in let x = M in (x, y) : A ∗ B

denote, respectively,

[figure: Γ ⊗ Δ; f ⊗ Δ; A ⊗ Δ; A ⊗ g; A ⊗ B]
[figure: Γ ⊗ Δ; Γ ⊗ g; Γ ⊗ B; f ⊗ B; A ⊗ B]

This directly implies the ‘only if’-part of the following proposition:

Proposition 44. Suppose that K is a direct λ_{C}-model. The denotation of Γ ⊢ M : A in K is central if and only if for every program Δ ⊢ N : B such that Δ doesn’t share variables with Γ,

Γ, Δ ⊢ let x = M in let y = N in (x, y)
= let y = N in let x = M in (x, y) : A ∗ B

Proof. The proof of the first claim is straightforward. The second claim requires some care. If the denotation of Γ ⊢ M : A is central, then obviously the equation in the statement of the second claim holds. The converse is not obvious, because K may have morphisms that cannot be denoted by any Δ ⊢ N : B. By lemma 24, f is central if it commutes with g = force_{B} for all objects B. And force_{B} is denoted by z : T B ⊢ μ(z) : B.

6 ⊗¬-categories as direct λ_{C}-models

The theory of ⊗¬-categories can be seen as an extension of the theory of direct λ_{C}-models. The only extra operator is a functor

¬ : K^{op} ^{}ΘK

This functor can model a unary type constructor cont like in SML of New Jersey. The axioms for ¬ imply that

x ⇒ y = ¬(x ⊗ ¬y)

For a full definition of ⊗¬-categories, see [Thi97a, Thi97b]. ⊗¬-categories are algebraic, which was observed by Peter Selinger (his control categories and co controlcategories [Sel98] are algebraic, and the latter are ⊗¬-categories together with sums). To my surprise I found that in a ⊗¬-category every central morphism is thunkable (see [Füh98]).

7 A direction for further research

Direct λ_{C}-models may be a good basis for finding direct models for call-by-value programming languages with several computational effects. I would like to keep the theories for several computational effects algebraic, because • We can do all reasoning by replacing subexpressions along the axioms.

• We can cope with changes of language features by simply adding and removing operators and equations, respectively.

• We have a simple meta-theory—for example, we can form the free algebraic theory generated by a set of operators and equations, adjoin indeterminates, and so on.

Acknowledgments. I am indebted to Hayo Thielecke, whose ⊗¬-categories were the main inspiration for my analysis of direct models. Thanks a lot to John Power for explaining to me premonoidal categories and more, and commenting on my work. Thanks to Peter Selinger for many discussions, in particular for making me aware of the algebraicitycriterion for models. Thanks to Stuart Anderson for commenting on several versions of this article. And a historical remark: Recently, Alex Simpson made me aware of his 1993 LFCS Lab-Lunch talk ‘(Not very far) Towards algebraic semantics of programming languages’ [Sim93]. There he sketched what I call direct models. He had already found the essence of my reflection theorem for monads (theorem 4). But there was no way to transfer this to strong monads, because premonoidal categories had not yet emerged.

References

[Füh98] Carsten Führmann. Relating two models of continuations. submitted, November 1998.

[Joh92] Peter T. Johnstone. Stone Spaces. Cambridge studies in advanced mathematics. Cambridge University Press, 1992.

[Lan71] Saunders Mac Lane. Categories for the Working Mathematician. Graduate Texts in Mathematics. Springer-Verlag, 1971.

[Mog88] E. Moggi. Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-66, Edinburgh Univ., Dept. of Comp. Sci., 1988.

[PR97] John Power and Edmund Robinson. Premonoidal categories and notions of computation. Mathematical Structures in Computer Science, 7(5):453–468, October 1997.

[PT97] John Power and Hayo Thielecke. Environments, continuation semantics and indexed categories. In Proceedings TACS’97, volume 1281 of LNCS, pages 391– 414. Springer Verlag, 1997.

[PT98] John Power and Hayo Thielecke. Environments in Freyd categories and κcategories. submitted, 1998.

[Sel98] Peter Selinger. Control categories. http:// www.math.lsa.umich.edu/ ∼selinger/ papers.html, 1998.

[Sim93] Alex Simpson. Towards algebraic semantics of programming languages. Notes for a talk at the LFCS Lab Lunch, March 1993.

[Thi97a] Hayo Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh, 1997.

[Thi97b] Hayo Thielecke. Continuation semantics and self-adjointness. In Proceedings MFPS XIII, Electronic Notes in Theoretical Computer Science. Elsevier, 1997.

A Moggi’s semantics of the λ_{C}-calculus

λ_{C}-calculus  λ_{C}-model
x_{1} : A_{1}, …, x_{n} : A_{n} ⊢ x_{i} : A_{i}  [figure: A_{1} × ⋯ × A_{n}; π_{i}; A_{i}; η; T A_{i}]
Γ ⊢ M : A  Γ \overline{\begin{matrix}f \\  \end{matrix}}T A
Γ ⊢ [M] : T A  [figure: Γ; f; T A; η; T T A]
Γ ⊢ M : T A  Γ \overline{\begin{matrix}f \\  \end{matrix}}T T A
Γ ⊢ μ(M) : A  [figure: Γ; f; T T A; μ; T A]
Γ ⊢ M : A  Γ \overline{\begin{matrix}f \\  \end{matrix}}T A
Γ, x : A ⊢ N : B  Γ × A \overline{\begin{matrix}g \\  \end{matrix}}T B
Γ ⊢ let x = M in N : B  [figure: Γ; ⟨id, f⟩; Γ × T A; t; T (Γ × A); T g; T T B; μ; T B]
Γ ⊢ M : A  Γ \overline{\begin{matrix}f \\  \end{matrix}}T A
Γ ⊢ N : B  Γ \overline{\begin{matrix}g \\  \end{matrix}}T B
Γ ⊢ (M, N) : A ∗ B  [figure: Γ; ⟨f, g⟩; T A × T B; ψ; T (A × B)]
Γ, x : A ⊢ M : B  Γ × A \overline{\begin{matrix}f \\  \end{matrix}}T B
Γ ⊢ λx : A.M : A ⇒ B  [figure: Γ; λf; T B^{A}; η; T ((T B)^{A})]
Γ ⊢ M : A ⇒ B  Γ \overline{\begin{matrix}f \\  \end{matrix}}(T B)^{A}
Γ ⊢ N : A  Γ \overline{\begin{matrix}g \\  \end{matrix}}T A
Γ ⊢ MN : B  [figure: Γ; ⟨f, g⟩; (T B)^{A} × T A; ψ; T ((T B)^{A} × A); T ev; T T B; μ; T B]

B Direct semantics of the λ_{C}-calculus

λ_{C}-calculus  direct λ_{C}-model
x_{1} : A_{1}, …, x_{n} : A_{n} ⊢ x_{i} : A_{i}  A_{1} ⋯ A_{n} π_{i} A_{i}
Γ ⊢ M : A  Γ \overline{\begin{matrix}f \\  \end{matrix}}A
Γ ⊢ [M] : T A  [figure: Γ; thunk; LΓ; Lf; LA]
Γ ⊢ M : T A  Γ \overline{\begin{matrix}f \\  \end{matrix}}LA
Γ ⊢ μ(M) : A  [figure: Γ; f; LA; force; A]
Γ ⊢ M : A  Γ \overline{\begin{matrix}f \\  \end{matrix}}A
Γ, x : A ⊢ N : B  ΓA \overline{\begin{matrix}g \\  \end{matrix}}B
Γ ⊢ let x = M in N : B  [figure: Γ; δ; ΓΓ; Γf; ΓA; g; B]
Γ ⊢ M : A  Γ \overline{\begin{matrix}f \\  \end{matrix}}A
Γ ⊢ N : B  Γ \overline{\begin{matrix}g \\  \end{matrix}}B
Γ ⊢ (M, N) : A ∗ B  [figure: Γ; δ; ΓΓ; fΓ; AΓ; Ag; AB]
Γ, x : A ⊢ M : B  ΓA \overline{\begin{matrix}f \\  \end{matrix}}B
Γ ⊢ λx : A.M : A ⇒ B  Γ\overline{\begin{matrix}λf \\  \end{matrix}}B^{A}
Γ ⊢ M : A ⇒ B  Γ \overline{\begin{matrix}f \\  \end{matrix}}B^{A}
Γ ⊢ N : A  Γ \overline{\begin{matrix}g \\  \end{matrix}}A
Γ ⊢ MN : B  [figure: Γ; δ; ΓΓ; fΓ; B^{A}Γ; B^{A}g; B^{A}A; apply; B]