Laws on the cheap

For the record, again, this is the definition of an Arrow:

> class Arrow (~>) where
>     arr :: (a -> b) -> (a ~> b)
>     (>>>) :: (a ~> b) -> (b ~> c) -> (a ~> c)
>     first :: (a ~> b) -> ((a,c) ~> (b,c))

Ignoring first for a moment, the laws are:

• An arrow is a category, with arr id as the identity. That is:

  arr id >>> a = a >>> arr id = a
  (f >>> g) >>> h = f >>> (g >>> h)
  

• An arrow is a functor:

  arr (f . g) = arr g >>> arr f
  

The laws that first satisfies are the tricky ones. Going from Ross Patterson's paper cited above, we have:

• extension

  first (arr f) = arr (f >< id)
  

• functor

  first (f >>> g) = first f >>> first g
  

• exchange

  first f >>> arr (id >< g) = arr (id >< g) >>> first f
  

• unit

  first f >>> arr fst = arr fst >>> f
  

• association

  first (first f) >>> arr assoc = arr assoc >>> first f
  

where we use the following auxiliary definitions:

> (><) :: (a -> b) -> (c -> d) -> (a,c) -> (b,d)
> (f >< g) ~(a,b) = (f a, g b)

> assoc :: ((a,b).c) -> (a,(b,c))

> assoc ~(~(a,b),c) = (a,(b,c))

Now, if you weren't paying attention in the last entry on free theorems, now is the time to rectify that. Go back and read it. All done? Okay.

Arrows are functors, so like Haskell Functors, they should have nice free theorems associated with them. Although we didn't state it explicitly, fmap is a way to construct functor homomorphisms from type substitutions, and the Functor laws guarantee that it behaves.

The situation is the same with arrows. Let (~>) be an arbitrary arrow, and consider the operation:

idA :: a ~> a

We would expect this to have a free theorem that looks a lot like the free theorem for id. And, indeed, it does:

idA >>> f = f >>> idA

What about first? The free theorem, it turns out, is:

If p >>> arr f = arr g >>> q,
then first p >>> arr (f >< h) = arr (g >< h) >>> first q.

We will assume, for the moment, that first is a functor:

first (arr id) = arr id
first f >>> first g = first (f >>> g)

Then, two of the five laws for first fall out as consequences.

The extension law:

    arr f >>> arr id = arr f >>> arr id
= (free theorem for first)
    first f >>> arr (id >< id) = arr (f >< id) >>> first (arr id)
= (arr (id >< id) is just arr id)
    first f = arr (f >< id) >>> first (arr id)
= (first is a functor)
    first f = arr (f >< id)

The exchange law:

    f >>> arr id = arr id >>> f
= (free theorem for first)
    first f >>> arr (id >< g) = arr (id >< g) >>> first f

The remaining two are unit and association. Although these seem to be related, and they look like they should be free theorems, I don't believe that they are. Because there's no guarantee that the arrow behaves like a function (it could be a forgetful functor), the first operation doesn't quite seem constrained enough by its type alone. The unit and association laws, then, define what first actually does.

Incidentally, you can get something very close to the association law by applying the free theorem for first to the unit law. Try it and see.

Now while it's nice to know that you don't need as many axioms as you thought you did, there's actually a serious side to this, and it's to do with the relationship between axioms and theorems as they relate to algebras embedded in Haskell.

If you write a monad, say, you have to guarantee that the three monad laws are obeyed. If you do that, everything works, and a bunch of other theorems are guaranteed to be true (partly from free theorems, partly from unbreakable abstractions). Another way of thinking about this is that axioms are laws that the programmer is required to prove. Theorems are up to the library implementor and.or compiler writer to prove, if they can assume that the axioms are correct.

Changing the number of axioms, or changing which basis axioms to use, does have an effect on programmer workload. Here, we've effectively reduced the number of axioms by two. That's two things you don't have to prove or unit test when you implement an arrow. Instead, it's up to smart people like John Hughes or Ross Patterson to prove them once.

So this is a plea for you academics out there who come up with new, cool abstractions for we lowly Haskell programmers to use: Every time you say the word "axiom", you've delegated responsibility and cost onto everyone who uses your tool. Sure, your time is valuable, too. But if you actually check it, and find that it's actually a theorem, then everyone else gets to benefit.

The theorem may not end up being free, but it will end up being cheaper for everyone.

Update: Thanks to Derek Elkins for correcting a mistake made in something I wrote at 11pm last night. arr is not a contravariant functor.