A compiler does not always have to do everything in one go.
A compiler pass might take a program, simplify it, lower it to another representation, split a computation between machines, or choose a different representation — and then hand the result to another compiler. The second compiler does another piece of the job, and eventually something produces the final target program. This is the idea behind a partial compiler.
But there is an interesting question that the usual description leaves out:
How do we know that a compiler pass has not introduced an error?
There is a surprisingly simple answer. Put back something that the original definition threw away.
A compiler that leaves the job unfinished
A partial compiler takes a source program and produces a reduced source program. But it also has to remember enough information to put the final answer back together.
Schematically, we can think of a partial compiler as having two parts:
a way to reduce the source;
a way to assemble the final target from the original source and whatever comes back from the next compiler.
The second part is important. If I take something out of a program in the first pass, I may need the original program again when I assemble the final result.
This is exactly the shape studied by Budiu, Galenson and Plotkin in their work on the Compiler Forest. Partial compilers can be composed: one pass hands its reduced program to the next, and the results are assembled in the reverse order. There is already a beautiful mathematical structure here. Partial compilers form a category. And there is an even older mathematical structure hiding underneath.
This looks like Dialectica
In the Dialectica interpretation, an object consists roughly of two kinds of things:
witnesses and counterexamples.
A witness is proposed evidence that something is true. A counterexample is a challenge to that evidence.
A Dialectica morphism has exactly the same two pieces of data as a partial compiler:
something going forward, turning one witness into another;
something going backward, turning a challenge to the output into a challenge to the input.
The backward map is allowed to depend on the original witness. This is precisely what a partial compiler needs when it has to remember the source while reconstructing the target. So a partial compiler is not merely similar to a Dialectica morphism.
It is a Dialectica morphism with one important thing missing: the relation.
This identification is not new. The authors of the Compiler Forest work themselves connect their construction with Dialectica through Blass's questions and answers and Milner's tactics. I also pointed it out in a talk on partial compilers and Dialectica spaces in 2011.
What is interesting and new is what happens when we stop throwing the relation away.
Put the counterexamples back
Suppose that for every source program S and target program T we have a relation saying that T is a bad implementation of S. Then a compiler pass is correct when it respects that relation. What does that mean?
Suppose the pass turns S into a smaller source f(S). Later, another compiler produces a target for f(S), and our pass uses that target to assemble a final target T for S. If T is wrong for S, then the target that came back from the next compiler must already have been wrong for f(S).
In other words: the pass itself has introduced no new errors.
That is exactly the Dialectica morphism condition, once we read the relation as a relation of refutations rather than as a relation saying that something is correct. And this gives a rather pleasant interpretation of the categorical composition.
A stack of compiler passes does not need a new correctness proof for the composite. Instead, take the specification at the end and push it backwards through the passes, one pass at a time. The specification that arrives at one pass tells us exactly what that pass has to guarantee.
This is a weakest-precondition calculation, but with the program running in two directions: witnesses move forward and counterexamples move backward.
Why "counterexample" rather than "correctness"?
There is a small but important subtlety here. One could have defined the relation the other way around: perhaps α(S,T) says that T is a correct implementation of S.
But then the direction of the Dialectica condition is wrong for what we want from a compiler. The useful reading is asymmetric:
the source is what we are trying to implement; the target is what can refute the implementation.
That is why counterexamples travel backwards. There is something rather satisfying about this. Correctness is not extra information that a compiler has to carry around. The compiler already has its two pieces of data.
The relation is a specification against which those pieces can be checked. A compiler either satisfies it or it doesn't.
Something unexpected happens: copying
Once we have the relation back, we can ask questions that are difficult to see in the original compiler description. One of them is:
Can a compiler duplicate its source?
This turns out not to be a question about the source. It is a question about the target type.
To copy something in the Dialectica category, the target has to know how to combine two copies into one. In mathematical language, it needs a suitable commutative monoid structure.
This makes visible the reason for a phenomenon reported in the Compiler Forest work. If compile-time effects are moved inside the construction, one might expect to get another category. But composition is no longer associative.
The Dialectica analysis explains why. The source appears in both the reduction and the generation part of a partial compiler. In effect, it is being used twice. Copying is free in a cartesian world.
It is not free in general.
The target type has to be able to absorb those two copies. A single outer monad can restore the situation because it keeps the effect outside this copying problem. So a categorical question about whether composition is associative turns out to have a very concrete interpretation:
Can this kind of target be copied?
What about cost?
The same construction also lets us replace ordinary truth values by quantitative ones. Instead of saying simply
this target is a counterexample
we can assign a value measuring how bad it is.
For example, the value might represent:
- size,
- running time,
- register pressure,
- or another resource.
The natural example is the Lawvere quantale, where the monoidal operation is addition. Then the Dialectica relation becomes a kind of cost model.
A compiler pass may add cost, but it cannot magically make the cost disappear. And, just as before, specifications can be pushed backwards through a stack of compiler passes.
There is another nice coincidence here.
When a compiler is lifted from individual sources to lists of sources, the specification for a list can be obtained simply by combining the specifications of its elements.
For costs, that means adding them. So the same mathematical operation — the monoidal structure — appears on opposite sides of the relation. On the target side, it describes how targets can be assembled or copied. On the specification side, it describes how costs can be aggregated.
From verified compilers to a type of verified compilers
There is one more step that I find particularly intriguing.
Suppose we do not want to say merely that a compiler has a specification. We want to restrict its source type to the sources for which the specification is actually satisfied. Then we are no longer talking about a class of programs carrying a side condition. We are constructing a new object consisting only of the sources that meet the condition.
In categorical language, this is a comprehension construction, and in the paper it leads to a proposed object of verified partial compilers. The idea is that the verified compilers themselves should form a type. There is even a natural adjunction suggested by this construction: a function-space-like object of verified partial compilers should be right adjoint to product with the source problem.
What I like about this story
The original partial compilers were motivated by a very concrete problem: compiling programs in stages and assembling the pieces later.
The mathematical construction reveals that the same pattern occurs in several places. A problem can be reduced to another problem and a solution can be assembled from a solution of the reduced problem. That is Kolmogorov's interpretation of intuitionistic logic as a calculus of problems. It is also the shape of Milner's tactics: reduce a goal to subgoals, then assemble a proof from their solutions. And it is the shape of a partial compiler.
Dialectica categories provide a common mathematical language for all of these.
The striking point for me is not that we can redescribe compilers categorically. It is that restoring the relation gives us things that were invisible when the relation was discarded:
- correctness,
- a criterion for copying,
- quantitative cost,
- and potentially a type of verified partial compilers.
None of this requires changing the compiler. The passes are the same passes. The composition is the same composition. The extra ingredient is simply the relation that says what counts as a counterexample.
So perhaps the moral is a very small one:
Sometimes the most useful information is precisely the information that was thrown away.
But another useful one is the (not-quite-ready) preprint.
No comments:
Post a Comment