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

[Ben Franksen]

wren ng thornton wrote:
 On 9/16/10 4:59 PM, Ben Franksen wrote:
 even though we always have

(\x -  e) y == let x = y in e

 which means that let can be translated to lambda, the converse is not
 true,
 
 Not exactly. 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.

I meant not possible as in by a source-to-source transformation in a
simple core-ML-like language (such as is used in most introductions to
HM-style type inference). If you translate to a language with mutable state
and/or built-in continuations then things are different, of course.

Do you know a good online introduction to CPS conversion that explains the
kind of duality you mentioned?

Cheers
Ben

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe