Defunctionalization and Freyd’s Theorem | Hacker News Reader

Defunctionalization and Freyd’s Theorem

bartoszmilewski.com

36 pointsingve15 comments

These posts always seem so damn interesting, but I get lost very early on. In this case it was at "Product is functorial in both arguments so, in particular, we can define a functor".

Any suggestions for introductory material that might help me appreciate Milewski's writings?

His own introduction to category theory for programmers is good:

https://bartoszmilewski.com/2014/10/28/category-theory-for-p...

This feels like the category theory version of the Feynman Lectures.

Not bad! Looks like I've found my next 20%-time project! :)

Steve Awodey's "Category Theory" is an excellent book to learn the basics, and there are no requirements to know beforehand topology or higher abstract algebra in order to follow it.

Aaaaaaaand purchased! Thanks!

I've read it once, so feel free to contact me if you need any help!

To be super clear, the quoted sentence continues, including the typeset formula below it. (It's an academic convention that I'm not a particular fan of.)

> Product is functorial in both arguments so, in particular, we can define a functor L_a(c) = c * a.

Bartosz is saying that we can fix one side of the product, giving us a one-argument specialization that is a functor. In this case, we're fixing `a` (subscript binds tighter than parameters, in some sense) and letting `c` vary. That's what it means to be functorial in both arguments: fix either one and you get a functor.

The same phenomenon shows up in other fields where you have n-ary functions. Bilinear maps (in linear algebra) are linear in each argument. You could come up with something similar involving continuity in each argument for a binary function in real analysis (although I think that would actually be a weaker property than claiming the binary function is continuous...)

Yup, I had gleaned that much from context. My issue is taht I don't know what a functor is!

Sure, I could look it up, but my problem is that I spend all my time looking things up. At some point, this gets in the way of proper understanding. It's a strong signal that I'm missing some foundational knowledge.

(Your reply is most appreciated, though!)

Fair! Sorry for belaboring an unnecessary point ^_^;

Not at all!

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.

> When you’re implementing a function, you are, in a sense, telling apply what to do with it – what code to execute. You’re implementing individual chunks of apply. These chunks are usually scattered all over your program, sometimes anonymously in the form of lambdas.

I feel like this is a much deeper philosophical point worth pausing and pondering. (It's also very suggestive as to the whole point of defunctionalization -- nice foreshadowing!)

I’ll need to reread some of his posts, but I don’t find this particularly enlightening. Apply has always been pure variable substitution in my mind. From this point of view, of course apply is dependent on the code snippet you’re supplying, it’s the code that’s getting “modified” by the substitution.

The point I took from it is that "apply" is normally given by your programming system, and its cases are spread out over your whole program. but there's no reason you can't build your own "apply" on your own function-like type. (The `Expr = Lit Int | Add Expr Expr` type is probably the best-known example.)

Functions happen to be things that your PL provides natively. Defunctionalization is all about capturing a piece of the global `apply` for functions, and translating it into an `apply` on a custom data type.

Reply on news.ycombinator.com