[PRL] Type-directed partial evaluation

[David Herman]

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.