[PRL] Type-directed partial evaluation

[Felix S Klock II]

On Jan 8, 2004, at 4:05 PM, Felix S Klock II wrote:

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

Oops, I spoke too soon.  I don't think the first example you gave 
suffers from the problem I described.  Sorry.

-Felix