jones_optimal_partial_eval_popl18.md

Jens Palsberg: Jones-Optimal Partial Evaluation by Specialization-Safe Normalization

https://popl18.sigplan.org/event/popl-2018-papers-typed-and-jones-optimal-self-applicable-partial-evaluation

Notes.

We can treat unbound or polymorphic variables as unbound variables.

before:

• mixer is beta-normal form

• but not jones optimal

  • means never any slowdown

partial evaluation can cause slowdown.

• the bottom has a duplication of _, which causes the slowdown
• Reducing (\x. e1) e2 can introduce multiple copies of e2.

Specialization safety:

A reduction relation ~> is specialization-safe for _time_
if e1 ~>* e2 implies
time(e2 x) <= time(e1 x) for all x.

not:

• \f. (\x. f x x) (square n2)
• \f. (\x. f x x) (f n2)

safe: \f. (\y. square x) (f n2)

not-safe: (\n. \m. n (plus m) n0) (f n2)

(terms) e ::= x | xo | \x.e | \xo.e | e1 e2

Mogensen's self-interpreter:

\eo. eo (\xo. xo) (\xo. xo)
\y. (\x. times x x) y
\yo. (\x. times x x) yo

Specialization-Safe Reduction relation

• less than full-beta

• Rule 6/7 allow reduction under lambda

• Can't stop there, because in some applications, we need rule-5

  • But there's still no duplication work.

• Specialization-safe reduction preserves well-formed annotations, is confluent, and produces unique normal forms.

• Nice small proof (summary) that i' <= i, using a diagram.

  • So it's specialization safe.

  mix f d ===_B NF_Beta (f d)
  mix p d ===_B erase NF..

• Using their reductions, church encoding, as well as some other encoding, works well for applying their systems.

How to type-check:

kinds, types, terms

type-check representation of terms.

• mapping type of the term to the type of the representation of the term.
• he's not the guy who knows how to write that stuff.
• If <> |- e : T, then <> |- ...

A partial evaluated has polymorphic type:

Jones, .. (1993)
forall A:*. foall B:* . Exp (A -> B) -> A -> Exp B

Carette, .. (2009)
forall A:*. foall B:* . Exp (A -> B) -> Exp A -> Exp B

All compared self-interpreters have at least 10x slowdown.

Tagless-final PHOAS 10-
Mogensen-Scott PHOAS ..
Tagless-final deBruijn 24-118

Show's comparisons of lambda evaluations.

• Mostly speedups (up to 2x), but a couple slowdowns

Similix ('91) is the only other Jones-optimal paper.

• Though he mentioned he kinda doubted it :P

• But they're still the first, when .. added

Linear-lambda-calculus

• Need annotater?