> 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 intere

> 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.