Posts tagged math

Closure Conversion as CoYoneda

:: Yoneda, coYoneda, category theory, compilers, closure conversion, math, by Max New

The continuation-passing style transform (cps) and closure conversion (cc) are two techniques widely employed by compilers for functional languages, and have been studied extensively in the compiler correctness literature. Interestingly, typed versions of each can be proven to be equivalence preserving using polymorphic types and parametric reasoning, as shown by my advisor Amal Ahmed and Matthias Blume (cps,cc).

In fact, there is something like a duality between the two proofs, cps uses a universal type, closure-conversion uses an existential type and the isomorphism proofs use analogous reasoning. It turns out that both are instances of general theorems in category theory: the polymorphic cps isomorphism can be proven using the Yoneda lemma, and the polymorphic closure-conversion isomorphism can be proven using a less well known theorem often called the *co*Yoneda lemma.

The connection between cps and the Yoneda embedding/lemma is detailed elsewhere in the literature and blogosphere (ncafe, Bartosz), so I’ll focus on closure conversion here. Also, I’ll try to go into some detail in showing how the “usual” version of Yoneda/coYoneda (using the category of sets) relates to the appropriate version for compilers.

I’ll assume some background knowledge on closure conversion and parametricity below. Fortunately, Matt Might has a nice blog post explaining untyped closure conversion.

Understanding Constructive Galois Connections

:: icfp, galois connection, adjunction, category theory, math, by Max New

One of my favorite papers at ICFP 2016 (in lovely Nara, Japan) was Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory by David Darais and David Van Horn. The central technical result is quite interesting, but a little intimidating, so I’d like to share a “de-generalization” of the result that I found helpful to understand.