[PRL] Type-directed partial evaluation

[Felix S Klock II]

On Jan 8, 2004, at 2:43 PM, David Herman wrote:

> And now for the Scheme magic of the day, thanks to Danvy [1]. Assume a 
> mini-Scheme with curried unary functions, atoms and pairs. If you give 
> me a *compiled* mini-Scheme program and its type, I will *decompile* 
> it back to (alpha-beta-eta-equivalent) source, amazingly with only a 
> few dozen LOC. Here's a sample interaction:
>
>     > (define S (lambda (f)
>                  (lambda (g)
>                   (lambda (x)
>                    ((f x) (g x))))))
>     > (residualize S '((A -> B -> C) -> (A -> B) -> A -> C))
>     (lambda (x0) (lambda (x1) (lambda (x2) ((x0 x2) (x1 x2)))))
>     > (define I*K (cons (lambda (x) x)
>                         (lambda (y) (lambda (z) y))))
>     > (residualize I*K '((A -> A) * (B -> C -> B)))
>     (cons (lambda (x0) x0) (lambda (x1) (lambda (x2) x1))

Is it not true that, for these examples, you can figure out the body of 
your code just from the type itself (assuming that those are all type 
variables in there, and that we're only dealing with total functions 
here)?

E.G.

((A -> A) * (B -> C -> B))

A -> A is only populated by id.
B -> C -> B is only populated by  "\ b . \ c . b"

Maybe you've already done this, but it might be good to test out the 
code on Church booleans and Church numbers.

-Felix