> I find it interesting that correct equational reasoning in this case lead to a correct program, but one with absymal performance.

That's not really an interesting property of Haskell, though. You can always write correct but slow code in any language.

> It'd be interesting to think how one could encode performance characteristics into equations.

I've seen the concept of encoding performance in types played around with, but I can't find actual work (if any) that's been done on it.