In a similar vein, see[0] which talks about rewrite systems from a more formal viewpoint. On the practice side, GHC performs rewrite rules[1], an example of whi

In a similar vein, see[0] which talks about rewrite systems from a more formal viewpoint. On the practice side, GHC performs rewrite rules[1], an example of which is "map/map" forall f g xs. map f (map g xs) = map (f.g) xs Combining two calls to map into one. While this seems silly, terms like this can arise as a result of other compiler optimizations. GHC can even remove intermediate data structures[2] entirely, so writing factorial as factorial n = product [1..n] would result in an efficient first-order program without the list at all. Another example of where rewrite rules come in handy is linting[3]. It does seem that a lot of these rewrites are possible only in a pure language, otherwise the compiler would have to resort to analyzing side-effects. [0] www.cs.tau.ac.il/~nachum/papers/taste-fixed.pdf [1] https://downloads.haskell.org/~ghc/7.0.3/docs/html/users_guide/rewrite-rules.html https://downloads.haskell.org/~ghc/7.0.3/docs/html/users_gui... [2] https://users.cs.northwestern.edu/~robby/courses/395-495-2017-winter/deforestation-short-cut.pdf https://users.cs.northwestern.edu/~robby/courses/395-495-201... [3] https://github.com/ndmitchell/hlint https://github.com/ndmitchell/hlint