This is not a pipe

This is a story of how a subtle distinction made a big difference in designing a compiler: The map is not the territory, and compile-time constants are not runtime values.

Comparing floats

While developing the HUGR compiler, there was an ongoing conversation whether a floating point constant should implement the Eq, Ord and Hash traits. In Rust, the floating point types do not implement these traits to comply strictly with the IEEE-754 standard that prescribes that NaN is not equal to itself. This can be circumvented easily (for instance by using the ordered_float crate), but doing so requires dismissing the argument that constants should follow the semantic structure of their domain. If floating point numbers do not have a reflexive equality relation, then why should floating point constants?

However, not being able to compare and hash floating point constants hamstrings the compiler in ways that are hard to justify. We would lose the ability to deduplicate constants via hash-consing: every NaN term would have to be represented by its own entity in the compiler’s memory, since sharing them would imply that they are equal after all. A rewrite rule like NaN * x = NaN would never be triggered since no term can ever match with NaN * x (whether such a rule is wise depends on how much you value the exact bit-patterns of NaNs, but that is besides the point).

This problem dissolves with the realisation that floats and float constants are not the same. The constant NaN term that a compiler manipulates is not a float but a description of how to produce a float. With that semantic distinction in place, it is not a contradiction that a NaN constant is equal to itself while its runtime instantiations are not.

I recognise that this may sound incredibly pedantic and perhaps completely obvious, but it is subtle enough to have tripped up a real team working on an industrial compiler for quantum computers for a while.

Copying qubits

It was surprisingly difficult to argue the significance of this semantic hygiene in the floating point case since it seemed awefully close to philosophical nitpicking. But because HUGR is a quantum compiler, we encountered a case where the distinction between constants and values was even more stark.

Qubits famously can not be copied. Does that mean that a constant in the compiler’s memory should not be copyable either? Is reading a qubit constant a destructive and stochastic operation just like measurement would be on a quantum computer? If I serialise the compiler’s state to disk, copy the bytes, and then deserialise it twice, have I circumvented a law of nature? Do I need a quantum computer to run my compiler?

The consequences of conflating qubits and their descriptions proved sufficiently absurd to make a convincing argument to overhaul the constant system. A qubit constant is not a quantum state, but a description of how to produce a quantum state. This description is classical data and can be freely copied, compared, and serialised to disk.

The quantum case inspired an even stronger position: runtime values are unutterable. A runtime value refers to the state of the machine at the time the program is run. This can be a classical bit, a quantum state, an open network connection, or the device handle of a GPU. The compiler can not refer to runtime values directly at all. The best it can do is talk about blueprints that can be instantiated into runtime values. This philosophy is already helpful for classical compilers, but was essential in clearing up a bunch of difficult questions regarding quantum programs.

Compressed representations

The new constant system enabled some further features that would’ve been weird to conceptualise coherently before. For instance, we noticed that many programs we encountered operated on large classical arrays of numbers. These arrays were initialised from a constant array filled with zeros and that constant was included verbatim in the serialised program, leading to large parts of the binaries being zeros. While this compressed well on disk, the overhead of decompressing and then manipulating many large byte buffers needlessly slowed down the compiler.

There is a more succinct way to describe an array of many zeros than explicitly listing out every zero individually. When we conflate constants and runtime values, this was not something we could do cleanly. If [0, 0, 0, 0, 0] is equal to [0; 5] we can not prefer one over the other. But if they are different, we can not compress the verbatim array to its succinct variant without changing the meaning of the program.

Our updated perspective on constants allows instantiation to be non-injective: We can have many different constants that instantiate to the same runtime value. As constants, [0, 0, 0, 0, 0] and [0; 5] are not the same, but they produce the same runtime array. Therefore we can change the uncompressed to the compressed version, producing an intensionally different program, while the runtime semantics of the program remains unchanged.

As a real-world analogy, there is two ways I could go about ordering a stack of 500 business cards: I could send the same design to a print shop 500 times, or I could send it once with the instruction to print it 500 times. In both cases I would obtain the exact same business cards, but clearly one is preferable to the other since it doesn’t cause an intolerable amount of hassle to everyone involved.

LNL Semantics

The inspiration for the constants-as-blueprints perspective came from the categorical semantics for linear-non-linear logic (LNL). To form a practical IR, we would need to strenghten the LNL setting to its dependently typed variant dLNL, but this restricted variant is sufficient to illustrate the point of constants. I found category theory to be a very useful tool in coming up with coherent designs in programming language theory, but also to be sufficiently scary to many practicing computer scientists as to elicit an immediate defensive reaction; therefore I didn’t advertise the origins of this idea as explicitly as it would have deserved.

In LNL, we have a symmetric monoidal category together with a cartesian monoidal category , connected via a lax monoidal adjunction

In our interpretation of this framework, describes the runtime language of a compiler IR. An object of is a type of runtime values, and morphisms in are programs that run on the target hardware. Because is not required to be cartesian, it can accomodate exotic programming models such as quantum channels. The category describes the language of compile-time parameters. It is cartesian monoidal, allowing parameters to be copied and discarded freely.

The functor takes a type in the runtime language and produces a type in the parameter language. We interpret as the type of constants or blueprints for . Since lives in , any blueprint for can be freely copied even when there is no way to copy values of type at runtime. The counit of the adjunction is a runtime map for every runtime type , which we interpret as instantiating a constant. In HUGR, I gave the functor the name core.const.