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