[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