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.