Jones-Optimal Partial Evaluation by Specialization-Safe Normalization

Speedup tests compare the runtime of two terms on some input(s). Each test declares a term pgm and a Tagless-final HOAS representation rep. The expectation is that the β-normal form of rep represents a program equivalent to pgm. The test runner normalizes rep and recovers the represented term. Then it compares the runtime of that term with pgm, when applied to some arguments also specified in the test file.

Here is a typical example of a specialization test that measures specialization speedup. The code is from speedupTest-ssrmix-bbint-compile-fact-1.fw, one of the tests we use to experimentally demonstrate Jones-optimality of our partial evaluator:

load "BB";
load "SSRMix";
load "BBUnquote";
load "Church";

decl pgm : Nat → Nat =
  fact
;

decl rep : Exp (Nat → Nat) =
  mix (Exp (Nat → Nat)) (Nat → Nat)
    [unquote (Nat → Nat)]
    [[fact]]
;

decl arg1 : Nat = one;

This test computes the speedup obtained by "compiling" the factorial function fact, when run with input one (the Church encoding of 1). Compilation is done by specializing the Tagless-final HOAS (Boehm-Berarducci) interpreter unquote to the representation of the factorial function fact.

We also use specialization tests to measure interpretational overhead. Here's an example taken from speedupTest-bbint-overhead-fact-1.fw:

load "BB";
load "BBUnquote";
load "Church";

decl pgm : Nat → Nat =
  fact
;

decl rep : Exp (Nat → Nat) =
  [unquote (Nat → Nat) [fact]]
;

decl arg1 : Nat = one;

This test compares the runtime of fact with that of unquote (Nat → Nat) [fact] on input one. Because rep is a representation, it is already a β-normal form, so the test runner simply extracts the represented term and runs it.

To run this test, invoke the runSpeedupTest program:

$ stack exec runSpeedupTest CBV 1 fomega/speedupTest-bbint-overhead-fact-1.fw

The `stack exec runSpeedupTest` part tells the Haskell build tool stack to execute the Haskell program runSpeedupTest. The remaining arguments are passed on to runSpeedupTest. The argument CBV specifies to count steps of call-by-value reduction to a value. The parameter 1 indicates that pgm and the program represented by rep should be run on one argument, namely arg1. Running this produces the following output:

$ stack exec runSpeedupTest CBV 1 fomega/speedupTest-bbint-overhead-fact-1.fw
Running pgm
Computing specialized pgm
Running specialized pgm
fomega/speedupTest-bbint-overhead-fact-1.fw,PASSED,34,463,0.07

The last line is in CSV format with columns Filename,Check,pgm Steps,rep Steps,Speedup. The Filename column indicates the test file. The Check column indicates whether the outputs from pgm and the program represented by rep are β-equivalent on the input(s). The pgm Steps column contains the number of steps pgm takes on the input(s). The rep Steps column contains the number of steps the program represented by rep takes on the input(s). For CBV and SimpleCBV, the steps are to a value; for NormalOrder and MemoNormalOrder they are steps to a β-normal form. The last column, Speedup, is \(\frac{\tt{pgm\ steps}}{\tt{rep\ steps}}\) (see the Wikipedia article on speedup for details). A speedup greater than 1 indicates that the program represented by rep runs faster (i.e. in fewer steps) than pgm on the given input(s). A speedup less than 1 means pgm is faster. In this case we are measuring the interpretational overhead, so rep represents the interpretation of pgm and we get a slowdown. In this case we are not interested in speedup but in the overhead, which is \(\frac{\tt{rep\ steps}\ -\ \tt{pgm\ steps}}{\tt{pgm\ steps}} * 100\) or \((\tt{speedup}^{-1}-1)*100\).

An example of a failing (not β-equivalent) speedup test is fomega/speedupTest-not-equivalent.fw, which compares plus one and plus two on input one:

load "Church";
load "BB";

decl pgm : Nat → Nat =
  plus one
;

decl rep : Exp (Nat → Nat) =
  [plus two]
;

decl arg1 : Nat =
  one
;

When we run this test, we see that runSpeedupTest reports that the β-equivalence check failed:

$ stack exec runSpeedupTest CBV 1 fomega/speedupTest-not-equivalent.fw
Running pgm
Computing specialized pgm
Running specialized pgm
fomega/speedupTest-not-equivalent.fw,FAILED,5,6,0.83

Typecheck tests which check if a program typechecks successfully. In particular, it tests that the final term and its transitive dependencies all typecheck. A type error lurking in an unused declaration will not be detected. Examples:

$ stack exec runTypecheckTest fomega/typecheckTestSuccess.fw
Succeeded.
$ stack exec runTypecheckTest fomega/typecheckTestFailure.fw 
Failed.
expected arrow type: 
l = x0
ty l = A0

The second example attempts to typecheck the term \A:*. \x:A. x x, which fails. This demonstrates that the test runner does in fact detect and report type errors (i.e. it doesn't simply output "Succeeded." for all inputs). It also demonstrates that our type errors are not user-friendly. Our results do not rely on these error messages. We use typecheck tests only to determine whether a program type checks.

Equivalence tests check if the normal forms of two terms or types are α-equivalent. The terms are given in a Church pair. The runner extracts each component, normalizes them, and tests that the normal forms are α-equivalent. These tests are run with runEquivTest.

$ stack exec runEquivTest NormalOrder fomega/equivTestSuccess.fw
normalized fst in 6 steps
normalized snd in 13 steps
Succeeded.
$ stack exec runEquivTest NormalOrder fomega/equivTestFailure.fw
normalized fst in 0 steps
normalized snd in 3 steps
Failed.
Not alpha-equivalent: 
   λs9024:*. λz9025:*. z9025...
   λs9026:*. λz9027:*. s9026 z9027...
Diff:
   x9031
...
   x9028 x9031
...

Again, the second test demonstrates that our equivalence test runner does catch and report failures when the two terms are not equivalent (though it doesn't provide very informative error messages). In this case, it fails because the encoding of 0 is not equivalent to the encoding of 1. Again, our results do not rely upon these error messages.

We can use runEquivTest to demonstrate the difference between the two call-by-value evaluators. The file fomega/equivTestSimpleCBVFailure.fw compares two values that are β-equivalent but not β-normal. The SimpleCBV evaluator reduces both terms to values in 0 steps and then the α-equivalence check fails.

$ stack exec runEquivTest SimpleCBV fomega/equivTestSimpleCBVFailure.fw
normalized fst in 0 steps
normalized snd in 0 steps
Failed.
...

The CBV evaluator reports that the terms reduce to values in 0 steps. However, it continues reducing to β-normal form, so the α-equivalence check succeeds.

normalized fst in 0 steps
normalized snd in 0 steps
Succeeded.

As mentioned above, we implement two call-by-name evaluators. One is simple and quite standard, but takes a very long time on large benchmarks like the fourth Futamura projection. The other is more efficient, but reduces to beta normal form instead of a value. However it only counts the number of call-by-value reduction steps to reach the value form, and the subsequent normalization work is not counted.

Our first test compares the counts reported by these two evaluators on our suite of first Futamura projection tests. We run the entire suite with each evaluator, and compare that the outputs are identical.

$ ./testCBVEvaluator.sh
PASSED

To inspect the output manually, you can use the show parameter. You will see output of the following form:

$ ./testCBVEvaluator.sh show
Output from CBV
...
Output from SimpleCBV
...

Table 2 measures the average overhead of interpreting a suite of programs with each of our interpreters. The script interpretationalOverhead.sh performs these measurements.

$ interpretationalOverhead.sh

Table 3 demonstrates Jones optimality of our partial evaluator based on specialization-safe normalization. We specialize our self-interpreters to the cube, fact, and ackermann functions on Church numerals, and measure speedups on a range of inputs for each. To perform these measurements, run JonesOptimality.sh with the argument ssr, specifying to use the Jones optimal partial evaluator based on specialization-safe normalization.

$ ./JonesOptimality.sh ssr

Table 4 demonstrates that specialization by beta-normalization is not Jones optimal. It reports speedups obtained by the same specializations as in Table 3, but using a beta-normalizer as the partial evaluator. To perform these measurements, run JonesOptimality.sh with the argument beta.

$ ./JonesOptimality.sh beta

Tables 5 through 7 show our speedups for the second, third, and fourth Futamura projections (Table 3 on Jones optimality covers the first projection). Run Futamura.sh with argument 2, 3 or 4 to perform the measurements for the second, third, or fourth projection, respectively.

$ ./Futamura.sh 2
...
$ ./Futamura.sh 3
...
$ ./Futamura.sh 4
...