Re: Call-by-value is Dual to Call-by-name

To: Philip Wadler <wadler@research.avayalabs.com>
Subject: Re: Call-by-value is Dual to Call-by-name
From: Paul B Levy <P.B.Levy@cs.bham.ac.uk>
Date: Wed, 2 Jul 2003 17:29:39 +0100 (BST)
cc: types@cis.upenn.edu
In-Reply-To: <200306301759.h5UHxvmW023902@saul.cis.upenn.edu>

Hi Phil

> The rules of classical logic may be formulated in pairs corresponding
> to De Morgan duals: rules about & are dual to rules about \/. A line
> of work, including that of Filinski (1989), Griffin (1990), Parigot
> (1992), Danos, Joinet, and Schellinx (1995), Selinger (1998,2001), and
> Curien and Herbelin (2000), has led to the startling conclusion that

[in the presence of control operators] 

> call-by-value is the de Morgan dual of call-by-name.

I'd say that the main source for the CBV/CBN control duality is one you 
didn't mention, viz.

@Article{StreicherReus:continuations,
  title =        "Classical logic, continuation semantics and abstract
                 machines",
  author =       "Th. Streicher and B. Reus",
  pages =        "543--572",
  journal =      "Journal of Functional Programming",
  month =        nov,
  year =         "1998",
  volume =       "8",
  number =       "6",
}

because that's the one that describes how to interpret CBV and CBN
languages with control in continuation categories that are dual
(developing the earlier work of Hofmann and Streicher).

This paper influenced my work on call-by-push-value, and as I argue in 

@InProceedings{Levy:adjunctions,
  author = 	 {P. B. Levy},
  title = 	 {Adjunction Models For Call-By-Push-Value With Stacks},
  booktitle = 	 {Proceedings of 9th Conference on Category Theory and 
Computer Science, Ottawa, 2002},
  year = 	 2003,
  volume =       {69}
  series =       {Electronic Notes in Theoretical Computer Science},
}

the Streicher-Reus duality is a consequence of a more fundamental duality,
viz. between values and stacks in CBPV, again with control operators.

In general, there is, in CBPV, an adjunction between values and stacks.  
CBV and CBN live in the Kleisli and co-Kleisli (respectively) parts of
that adjunction.  When we add control operators, there is a duality
between values and stacks *as well as* this adjunction, and so the Kleisli
and co-Kleisli categories are dual.

The Streicher-Reus duality is only a duality at the level of *judgements*
(that is to say, the semantic categories are dual).  There is no CBV/CBN
duality at the level of terms, unless one modifies CBN to achieve it, as
Selinger did (and you have done too), by adding a type constructor that he
called "disjunction", which is different from the usual CBN sum type, and
would not be meaningful in the absence of control operators.  (At least, I
don't see any operational meaning in general.  Though I must admit that
 finite coproducts in the stack category do seem to pop up in a lot of
CBPV models, e.g. coalesced sum of pointed cpos.  Why, I have no idea.)

Paul