Subject: categories: Re: co-exponential question

From: Andrzej Filinski <[email-masked]>
Date: Thu, 22 Jul 1999 22:28:12 +0200 (MET DST)

Paul Levy writes:

> I don't know if this is relevant to your question, but there is an
> example in programming semantics where the dual of a cartesian closed
> category has independent significance, due to Lafont, Streicher, Reus
> and Hofmann.  (Some further work was done by Selinger.)  It is found
> in the following paper:  [Streicher & Reus 1998]

Indeed, co-exponentials are closely tied the semantics of call/cc-like
control operators. This connection is perhaps expressed more directly in
the following (regrettably somewhat unpolished) work:

@MastersThesis{Filinski:89a,
  author =      "Andrzej Filinski",
  title =       "Declarative Continuations and Categorical Duality",
  school =      "Computer Science Department, University of Copenhagen",
  year =        1989,
  month =       Aug, 
  note =        "DIKU Report 89/11",
  URL =         "http://www.brics.dk/~andrzej/papers/DCaCD.ps.gz"
}

@InProceedings{Filinski:89b,
  author =      "Andrzej Filinski",
  title =       "Declarative Continuations: An Investigation of
                 Duality in Programming Language Semantics",
  booktitle =   "Category Theory and Computer Science",
  series =      LNCS,
  number =      389,
  address =     "Manchester, UK",
  month =       Sep,
  pages =       "224-249"
}

Specifically, in the category induced by the types and terms of a
call-by-value language with first-class continuations, the coproduct
functor - + A actually has a left adjoint - x (A -> 0), where 0 is the
empty type.  The operational intuition behind this construction is that
a function f : X -> Y + A returning either a "normal" (Y) or an
"exceptional" (A) result corresponds to a function f' : X x (A -> 0) ->
Y, returning only the normal result, but passing any exceptional results
to an additional, non-returning-function parameter.

(In a purely functional language, the type A -> 0 would of course
contain at most one value; but in the presence of control effects, such
as exceptions, there can be many distinct "functions" of this type. And
with a sufficiently powerful control operator, it actually becomes
possible to define co-application and co-currying with equational
properties exactly mirroring those of CCC exponentials.)

Still, as Paul notes,

> K is certainly an important category, but I wouldn't say that the fact
> that it has coexponentials is significant.  

constructing a categorical semantics of a language with control operators
_directly_ in terms of coexponentials is somewhat awkward, and the
formulation used by Streicher and Reus is almost certainly nicer to work
with in practice.

-- Andrzej

---

From: Peter Selinger <[email-masked]>
Date: Fri, 23 Jul 1999 15:40:52 -0400 (EDT)

> formulation used by Streicher and Reus is almost certainly nicer to work

The _direct_ categorical semantics of languages with control operators
is actually not too unnatural and leads to some interesting category
theory. Let me first clarify the difference between direct and
indirect semantics. To give a direct semantics, one starts with a
class of categories with algebraic structure (for our purposes:
structure that is given by object constructors, morphism constructors,
and equations on morphisms). In the direct interpretation of a
language, types are interpreted as objects, type constructors as
object constructors, and typing judgments as morphisms, in such a way
that the language forms an _internal language_ for the class of
categories at hand. This means, among other things, that one can
construct a syntactic category from a theory of the language. Thus,
all structure of the category (on objects and morhpisms) is denotable
in the language. The usual interpretation of the simply-typed lambda
calculus in a cartesian-closed category is perhaps the best-known
example of a direct semantics. (Direct semantics of higher order can
be given in fibered categories, but this is not necessary for our
purposes here).

In an indirect semantics, one does not interpret the language directly
in a category with algebraic structure, but in a derived auxiliary
category. Moggi's monadic semantics is an example of an indirect
semantics.  Given a category C with a monad T, one interprets the
language (for instance, a call-by-value lambda calculus) in the
Kleisli category of the monad. Notice that the structure of the
Kleisli category, per se, is not necessarily algebraic in the above
sense. The Reus-Streicher-Lafont-Hofmann semantics is indirect; in
fact it is the monadic semantics for the continuations monad
R^(R^(-)).

Indirect semantics are very successful in practise. Among other
things, they have proven excellent tools for reasoning about and
implementing control effects. This point is made convincingly in
Andrzej Filinski's PhD thesis [1]. However, the correspondence between
syntax and semantics is not as close as in the direct case: one cannot
usually speak of internal languages in the context of indirect
semantics.  The reason is that, from a syntactic theory of the
language, one can reconstruct only the Kleisli category of T, but not
the underlying category C or the monad T itself. Thus, direct
semantics might be more satisfying to the theorist, because they
capture the essence of the language precisely, and without resorting
to a translation to a meta-language.

The difference between direct and indirect semantics is explained very
nicely in a recent paper by Carsten Fuhrmann [2], where he also gives
a general method of constructing direct semantics from indirect ones.
It seems that direct semantics are often characterized by the presence
of certain _non-natural_ transformations, and that indirect semantics
are a way of hiding this non-naturality.

The first direct semantics for a call-by-value language with control
effects are the tensor-not categories of Hayo Thielecke [3]. His work
was later extended by me to a language with finite coproducts (this is
where co-exponentials enter the picture) and to the call-by-name case
[4]. I called the resulting class of categories "control
categories". The connection between the direct and indirect semantics
can be established via categorical representation theorems, and such
theorems were shown by Fuhrmann for tensor-not categories [5], and
independently by myself for control categories [4].

It is interesting that a call-by-name language is an internal language
for control categories, and the corresponding call-by-value language
is an internal language for the dual co-control categories. As a
consequence, one obtains a syntactic duality between call-by-name and
call-by-value [4]. Such a duality was conjectured by Streicher and
Reus [6], and certainly anticipated by Filinski's work on the
symmetric lambda calculus [7].

Best wishes, -- Peter

[1] A. Filinski. Controlling effects. PhD Thesis in Computer Science,
Carnegie Mellon University, 1996.

[2] C. F\"uhrmann. Direct models for the computational
lambda-calculus. Technical Report ECS-LFCS-98-400, Edinburgh, 1998.

[3] H. Thielecke. Categorical structure of continuation passing
style. PhD Thesis in Computer Science, Edinburgh, 1997.

[4] P. Selinger. Control categories and duality: on the categorical
semantics of the lambda-mu calculus. Submitted 1999. Available from
Hypatia or http://www.math.lsa.umich.edu/~selinger/papers.html

[5] C. F\"uhrmann. Exponential categories and semantics of
continuations. Presented at MFPS, 1998.

[6] T. Streicher, B. Reus. Classical Logic, continuation semantics and
abstract machines. Journal of Functional Programming 8(6)543-572, 1998.

[7] A. Filinski. Declarative continuations and categorical duality.
Masters Thesis in Computer Science, DIKU, University of Copenhagen,
1989. DIKU Report 89/11.