A classic case of inefficiency in functional program is things like the reverse function written from specification
import Prelude()
[] ++ ys = ys
(x:xs) ++ ys = x:(xs ++ ys)
reverse [] = []
reverse (x:xs) = (reverse xs) ++ [x]
Using associativity, one can derive an efficient reverse
-------- REWRITE ------
-- RULE : ++ relation (deduced)
-- reverse xs = reverse xs ++ []
-- RULE : [] relation -- case split
-- reverse [] = reverse [] ++ []
-- reverse (x::xs) = reverse (x::xs) ++ []
-- RULE : reverse relation
-- reverse [] = []
-- reverse (x::xs) = (reverse xs ++ [x]) ++ []
-- RULE : ++ relation (deduced)
-- reverse [] = []
-- reverse (x::xs) = reverse xs ++ ([x] ++ [])
-- RULE : ++ relation
-- reverse [] = []
-- reverse (x::xs) = reverse xs ++ (x::[])
-- RULE : (language)
-- reverse' [] _ = []
-- reverse' (x::xs) acc = reverse xs ++ acc
-- reverse xs = reverse' xs []
reverse_eff xs = reverse' xs []
where
reverse' [] ys = ys
reverse' (x:xs) ys = reverse' xs (x:ys)
However, where is the problem coming from in the first place ?
- We instruct a specific order for
++ - Composition as defined by our language defines an order for composition of our
++ - Our language is unaware of laws, derived from the code itself, and is unaware of ideas of efficiency.
What we really meant to do was :
- specify a (functional) relation
++, properly quotiented by all its laws - use relational composition for it, which hides which specific parenthesizing will be used
- at usage site, select one parenthesizing which best fit our access pattern and goal (in the case of
reverse, this means shifting all the parenthesis to match the way the resulting list is constructed)
Are there any language which generates some laws, and searches for the best rewrite according to some metric ?