Recently in category theory Category

While we're on the topic, here's something that's been bugging me for a few years now.

There are three monad laws in Haskell, and they make a lot of sense, especially when you write them in do-notation form. They're very-well motivated, and they're clean.

Arrows are a very pretty generalisation of "notions of computation" (you can think of them as extending monads to not-just-straight-line computation). However, some of the laws that they obey are much more poorly motivated. I figured that this was because they were based on Freyd categories, which are abstract things which obey silly, technical laws.

I'm happy to report that I was wrong. We hereby motivate some of the arrow laws.

The programming language Haskell (under reasonable conditions) has this cool property, known as parametricity. Intuitively, it means that all functions of a certain type share certain properties.

After Phil Wadler, we refer to any such property as a "free theorem". In the ramblings that follow, I muse on exactly what they mean.