[PRL] Type-directed partial evaluation

[Carl Eastlund]

But it does suffer from that problem.  "S" needs to generate a "C", which
it can only do using its first paramter (A -> B -> C), so it also needs an
A and a B.  Which it can only get from its other two arguments, and the
constraints stay the same.

Whether this actually results in a problem in Dave's code and/or theory, I
don't know.

--Carl

On Thu, 8 Jan 2004, Felix S Klock II wrote:

>
> 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
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl
>