[Haskell-cafe] Re: Re: Re: Do expression definition

[wren ng thornton]

On 9/17/10 4:04 PM, Ben Franksen wrote:
> wren ng thornton wrote:
>> Note that when compilers do CPS conversion, everything is
>> converted into let-binding and continuations (i.e., longjump/goto with
>> value passing). It's just dual to the everything-is-lambda world,
>> nothing special.
>
> Do you know a good online introduction to CPS conversion that explains the
> kind of duality you mentioned?

Not off hand. These papers[1] give a pretty good explanation of CPS 
conversion and the other stages of compilation, from the perspective of 
proving compiler correctness. But they don't say much about the duality 
aspect of it. For the duality side of things, Andrzej Filinski's masters 
thesis[2] is an excellent read; though it doesn't say much about 
compilation IIRC.

Basically the duality comes when decomposing a whole program. When we 
separate a term from its context, which part is in control? Control is 
just a perspective, so you could be outside the function looking in, or 
inside the function looking out. One person's push is another's pull. 
This is the same sort of thing as build/foldr vs unfoldr/destroy forms 
of list fusion: once we separate the F-algebra and F-coalgebra, which 
one should get the recursion?[3]


[1]
@InProceedings{ Chlipala2007:tpc,
     author    = "Adam Chlipala",
     title     = "A Certified Type-Preserving Compiler from Lambda 
Calculus to Assembly Language",
     year      = 2007,
     booktitle = "PLDI",
     url       = {http://adam.chlipala.net/papers/CtpcPLDI07/CtpcPLDI07.pdf}
}
@Article{ Leroy2009:compcert,
     author    = "Xavier Leroy",
     title     = "A Formally-Verified Compiler Back-End",
     year      = 2009,
     journal   = "Journal of Automated Reasoning",
     url       = 
{http://pauillac.inria.fr/~xleroy/publi/compcert-backend.pdf}
}


[2] http://www.diku.dk/~andrzej/papers/DCaCD.ps.gz

[3] http://www.haskell.org/pipermail/haskell-cafe/2010-August/082592.html

-- 
Live well,
~wren