[PRL] Type-directed partial evaluation

[Matthias Felleisen]

Take PCF instead of Scheme. Take good(tm) domains instead of 
target-machine code (and read some of Mitch's old papers from the early 
80s). Then I can create source text for all infinite computable
"compiled codes" using call/cc. Though I have to admit that the 
algorithm is burried in two papers
and I only know the one for finite computable "codes" reasonable well 
to do it on the spot.

-- Matthias


On Thursday, January 8, 2004, at 02: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))
>
> Decompiling a value of ground type or a pair is easy. The trick to 
> decompiling a function is eta-expansion: although you can't inspect a 
> function, you can always apply it. By applying it in the body of a new 
> function, you can generate a dynamic (i.e., uncompiled) function that 
> is eta-equivalent to the original (compiled) function. However, the 
> new variable in the eta-expanded function is dynamic, and the compiled 
> function is static. So the variable has to be converted to a static 
> value before it can be passed to the compiled function. For this we 
> need a complementary `reflect' operation which takes dynamic 
> expressions to static values.
>
>     ;; reify : type static-value -> dynamic-expression
>     ;; reifies a static value into a dynamic program based on the 
> specified type
>     (define (reify t v)
>       (match t
>         [`(,t1 * ,t2)
>          `(cons ,(reify t1 (car v))
>                 ,(reify t2 (cdr v)))]
>         [`(,t1 -> ,t2)
>          (let ([x1 (gensym!)])
>            `(lambda (,x1)
>               ,(reify t2 (v (reflect t1 x1)))))]
>         [_ v]))
>
>     ;; reflect : type dynamic-expression -> static-value
>     ;; reflects a program into a static value based on the specified 
> type
>     (define (reflect t e)
>       (match t
>         [`(,t1 * ,t2)
>          (cons (reflect t1 `(car ,e))
>                (reflect t2 `(cdr ,e)))]
>         [`(,t1 -> ,t2)
>          (lambda (v1)
>            (reflect t2 `(,e ,(reify t1 v1))))]
>         [_ e]))
>
>     ;; residualize : any type -> program
>     ;; decompiles a program
>     (define (residualize v t)
>       (reset-gensym!)
>       (reify (parse-type t) v))
>
> [The parse-type function curries a type expression (e.g., '(A -> B -> 
> C) becomes '(A -> (B -> C))).]
>
> Cool, huh?
>
> Dave
>
> [1] Olivier Danvy: Type-directed partial evaluation. POPL '96.
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl