[PRL] Type-directed partial evaluation

[John Clements]

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))

1) That's very nice, and thanks for posting it.

2) things go to hell in a handbasket in the presence of primitives and 
set!, right?  This is like parametricity; the result of the function 
can only be one of a few things, and if we pass in a bunch of gensyms, 
we can characterize the output directly.  In the presence of set!, 
there's no way to know whether the function will behave the same way 
the second time.

3) The natural conclusion is that programming with set! is dangerous 
and makes it hard to reason about your programs, which I certainly 
agree with.