[PRL] Type-directed partial evaluation
Matthias Felleisen
matthias at ccs.neu.edu
Thu Jan 8 18:03:37 EST 2004
As you pointed out in the old papers, denotations are compiled code.
The denotations in SEQ (the category of domains that I developed with
Curien and Corky) allows a FA semantics for PCF with catch (or a
restricted version of callcc). Inside the FA proof, there is an
algorithm -- not unlike Danvy's -- that resurrects the source code of a
function. You use catch to provide the coroutining that is necessary
between functionals of rank 2 and higher (see my first lecture in 369)
and their arguments. That's the rough idea. I claim it is an algorithm
(even though I only have words right now) because I can do it
systematically and because it always terminates.
Rama extended this to the infinite case in a joint paper that we
presented at some too obscure conference in the Netherlands. SEQ is
thus the only known category that presents finite elements in a
constructive, enumerable manner, allows a FA proof, therefore allows
the textual representation of all finite elements, and allows full
expressiveness of all infinite computable elements in the domain on
top. (Naturally, we can't represent infinite non-computable elements
from the "code basis" aka domains.) I therefore claim that SEQ domains
are far superior to the Abramsky-Hyland clan production. :-)
-- Matthias
On Thursday, January 8, 2004, at 05:58 PM, Mitchell Wand wrote:
>> Take PCF instead of Scheme. Take good(tm) domains instead of
>> target-machine code (and read some of Mitch's old papers from the
>> early
>> 80s). Then I can create source text for all infinite computable
>> "compiled codes" using call/cc. Though I have to admit that the
>> algorithm is burried in two papers
>> and I only know the one for finite computable "codes" reasonable well
>> to do it on the spot.
>
>> -- Matthias
>
> Umm, tell us more?
>
> --Mitch
More information about the PRL
mailing list