Why $\lambda$‽

The Compiler Forest
M.Budiu, J. Galenson and G. D. Plotkin
ESOP 2013

This paper explores a notion of partial compilers, motivated by the problem of compiling high-level code (e.g. LINQ-style collection-based programs) on different architectures, such as multicore, GPU, or database backends.  If we think of a compiler as a simple function $C : source \to target$, then a partial compiler is a function $PC : source \to source' * (target' \to target)$.  Moreover, we can think of a "compilation problem" $C(source,target)$ as a pair of the source language and target language types.  Then a partial compiler $PC : C(source,target) \mathrel{-\!\!\circ} C(source',target')$ translates one "compilation problem" to another, hopefully simpler one: it takes a $source$ and produces a $source'$ together with a function $target' \to target$ that says how to finish compiling to $target$ once the $source'$ has been compiled to $target'$.

An ordinary compiler is then just a partial compiler that reduces the problem of compiling $source$ to $target$ to the "empty" problem $C(unit,unit)$, since $source \to unit * (unit \to target)$ is isomorphic to $source \to target$.
Read more »

Labels: compilers, programming languages, tactics