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.

Reviews and author responses: we should stop asking for 500-word responses

:: by Gabriel Scherer

This year I reviewed many ICFP submissions, and got to be on the receiving end of equally many author responses (also sometimes called, somewhat combatively, rebuttals). I found that there was a large difference between the official written advice on author responses and what I, as a reviewer reading the responses, found effective. In particular, I now believe that limiting yourself to 500 words should strongly be avoided — we should even stop giving that advice.

Spring 2017 PL Junior Retrospective

:: PL Junior, by Ben Chung, by Milo Davis, by Ming-Ho Yee, by Matt Kolosick, by Dustin Jamner, by Artem Pelenitsyn, by Julia Belyakova, by Sam Caldwell

The PL Junior Seminar is for beginning PhD and interested undergrad and masters students to understand the foundations of programming languages research. It serves to fill in background knowledge and get up to speed with different areas of PL research.

For the spring 2017 instance of PL Junior we chose program synthesis, the sequent calculus, and logic programming as topics we wanted to learn more about. We also did two group paper readings for Luca Cardelli’s Typeful Programming and Alan Kay’s Early History of Smalltalk. At the same time, we changed up the format from the previous semester.