[gsg]

Interesting if somewhat opaque. I'm familiar with defunctionalisation as an alternative to closure conversion in whole program compilers and as a description of how data types are derived from the lambda calculus - never seen a category theory take on the idea. I don't seem to be able to understand the category theory part though.

The suggestion to use a combination of CPS + defunctionalisation to serialise closures is notable, since that pair of transformations gives a fairly close correspondence between a subset of the lambda calculus (plus some primitives) and abstract machine code. Some of the old-school Scheme compilers used CPS as a low-level IR for that reason.