Some remarks on control categories

This paper is a collection of remarks on control categories, including answers to some frequently asked questions. The paper is not self-contained and must be read in conjunction with [3]. We clarify the definition of response categories, and show that most of the conditions can be dropped. In particular, the requirement of having finite sums can be dropped, leading to an interesting new CPS translation of the λµ-calculus. We discuss the choice of left-to-right vs. right-to-left evaluation in the call-by-value lambda calculus, an issue which is sometimes misunderstood because it is a purely syntactical issue which is not reflected semantically. We clarify the relationships between various alternative formulations of disjunction types and conjunction types, which coincide in call-by-value but differ in call-byname. We prove that copyable and discardable maps are not always central, and we characterize those control categories of the form R Set for which copyable and discardable implies central. We prove that any control category with initial object is a preorder. 1 Response categories and sums The central construction of [3] is the construction of a control category from a category with finite products and powers of the form R A, for a single, distinguished object R. This construction is a categorical version of continuation passing style (CPS) semantics of the lambda calculus. In [3], a category C with a distinguished object R is called a response category if it satisfies the following conditions: 1. C has finite products. 2. Exponentials of the form R A exist, for any object A. This means that there is a natural isomorphism of hom-sets (B, R A) ∼ =A (B × A, R). 3. C has finite coproducts (sums). 4. Sums and products distribute, i.e., the canonical morphism d: (A × C) + (B × C) → (A + B) × C is an isomorphism