Calculating compilers categorically

Conal Elliott

Draft of July, 2018 (comments please!)


This note revisits the classic exercise of compiling a programming language to a stack-based virtual machine. The main innovation is to factor the exercise into two phases: translation into standard algebraic vocabulary, and a stack-oriented interpretation of that vocabulary. The first phase is independent of stack machines and has already been justified and implemented in a much more general setting. The second phase captures the essential nature of stack-based computation, is independent of the source language, and is calculated from a very simple specification.

The first translation phase converts a typed functional language (here, Haskell) to the vocabulary of categories. All that remains is to specify and calculate a category of stack computations, which is quite easily done as demonstrated below. Other examples of this compiling-to-categories technique include generation of massively parallel implementations on GPUs and FPGAs, incremental evaluation, interval analysis, and automatic differentiation.