Paper(s) of the day: Bananas

Okay, so as I said I would I ended up reading Bananas, Envelopes, and Barbed Wire as well as Bananas In Space.

Wow, so I don't think the original paper has aged well in some ways. The notation and equations are very different than any other way I've seen the material presented, and it's no wonder I feel like I didn't get much out of this paper five years ago when I was just learning category theory and knew essentially no computer science ("Oh, so you know computer science now?" "Stop that, Caylee!"). So, I read Freyd's papers on fixed points of functors a lot more recently and I think they're clearer if much harder to find. I've never found them available on the Interwebz, but I grabbed copies from my university library. There's no category theorists at Portland State, but we have copies of the category theory journals. Go figure!

So, anyway, the original paper is cute from a historic perspective as it shows how natural fusion laws from the category of sets and functions can be extended to the the categoy of cpos with some strictness side conditions. It basically says, but doesn't show with commuting diagrams, that these laws come from universal mapping properties of limits and colimits.

The Bananas in Space paper is really cute though because it shows how to describe these constructions as Haskell (well, Gofer...) code. The punchline is giving a demonstration of Freyd's difunctors as code. Which, honestly, makes sense if you think of Haskell programs as existing in some subcategory of CPO that's clearly going to be enriched in the ways that Freyd's work needs. I mean, clearly, that's not really rigorous math but it's a really cute example of the construction.

So what did I really gleen from these papers? Well, I guess I didn't pick up stuff that I hadn't already known about. I suppose one thing I'm wondering about is why I haven't seen more systems for reasoning about programming languages using equational methods like these. I have seen papers talking about how you can do it, but I haven't seen many mechanized systems for doing the work and proving serious properties of programs. I've wondered before if that's because most of the languages we'd want to reason about don't have a formal semantics.

I think I just made an argument for why I need to get back to working on a semantics for Habit...*scurry scurry*

Tomorrow will be reviewing Plotkin's generalization of the D-infinity construction as well as Pitt's original paper on logical relations.