Yes! Haskell is a delight for optimization because you can use algebraic reasoning and calculation to derive more efficient code. For example, if I had the following code:
(concat . reverse . map reverse) strs
I could easily replace it with the following code, which is simpler, faster, and reduces memory churn:
(reverse . concat) strs
You can prove that these two implementations produce the same results (see [1] for a step-by-step proof). After you do the proofs for a while, you'll start seeing similar optimizations everywhere – and claiming them.
The rewriting part - if not the comping up with proofs part - is done automatically in quite a few libraries. You can specify the expression rewriting rules in pragmas in your source and GHC will carry them out.
Comments
Yes! Haskell is a delight for optimization because you can use algebraic reasoning and calculation to derive more efficient code. For example, if I had the following code:
I could easily replace it with the following code, which is simpler, faster, and reduces memory churn: You can prove that these two implementations produce the same results (see [1] for a step-by-step proof). After you do the proofs for a while, you'll start seeing similar optimizations everywhere – and claiming them.[1] https://gist.github.com/tmoertel/7968466
If you can derive this and prove it, shouldn't this optimization be done (theoretically) completely automatically by the compiler?
Computers are good at verifying things, but bad at coming up with them.
(An example for something computers can come up with is free theorems, but in this case that wouldn't have helped.)
The rewriting part - if not the comping up with proofs part - is done automatically in quite a few libraries. You can specify the expression rewriting rules in pragmas in your source and GHC will carry them out.