Correctness of short cut fusion
Revision as of 15:14, 6 July 2006
1 Short cut fusion
Short cut fusion allows elimination of intermediate data structures using rewrite rules that can also be performed automatically during compilation.The two most popular instances are the
foldr :: (a -> b -> b) -> b -> [a] -> b foldr c n  = n foldr c n (x:xs) = c x (foldr c n xs) build :: (forall b. (a -> b -> b) -> b -> b) -> [a] build g = g (:) 
foldr c n (build g) <nowiki>→</nowiki> g c n
destroy :: (forall b. (b -> Maybe (a,b)) -> b -> c) -> [a] -> c destroy g = g listpsi listpsi :: [a] -> Maybe (a,[a]) listpsi  = Nothing listpsi (x:xs) = Just (x,xs) unfoldr :: (b -> Maybe (a,b)) -> b -> [a] unfoldr p e = case p e of Nothing ->  Just (x,e') -> x:unfoldr p e'
destroy g (unfoldr p e) <nowiki>→</nowiki> g p e
2 CorrectnessIf the
That is, the left- and right-hand sides should be semantically the same for each instance of either rule. Unfortunately, this is not so in Haskell.We can distinguish two situations, depending on whether
2.1 In the absence of seq
foldr c n (build g) = g c n
The two sides are semantically interchangeable.
To see this, consider the following instance:
g = \x y -> case x y of Just z -> 0 p = \x -> if x==0 then Just undefined else Nothing e = 0
destroy g (unfoldr p e) = g listpsi (unfoldr p e) = case listpsi (unfoldr p e) of Just z -> 0 = case listpsi (case p e of Nothing ->  Just (x,e') -> x:unfoldr p e') of Just z -> 0 = case listpsi (case Just undefined of Nothing ->  Just (x,e') -> x:unfoldr p e') of Just z -> 0 = undefined
while its right-hand side "evaluates" as follows:
g p e = case p e of Just z -> 0 = case Just undefined of Just z -> 0 = 0
The obvious questions now are:
- Can the converse also happen, that is, can a safely terminating program be transformed into a failing one?
- Can a safely terminating program be transformed into another safely terminating one that gives a different value as result?
There is no formal proof yet, but strong evidence supporting the conjecture that the answer to both questions is "No!".The conjecture goes that if
destroy g (unfoldr p e) <math>\sqsubseteq</math> g p e
What is known is that semantic equivalence can be recovered here by putting moderate restrictions on p.More precisely, if
destroy g (unfoldr p e) = g p e
2.2 In the presence of seq
This is the more interesting setting, given that in Haskell there is no way to restrict the use of
Unsurprisingly, it is also the setting in which more can go wrong than above.
In the presence of
g = seq c = undefined n = 0
The converse cannot happen, because the following always holds:
foldr c n (build g) <math>\sqsupseteq</math> g c n
Moreover, semantic equivalence can again be recovered by putting restrictions on the involved functions.More precisely, if
foldr c n (build g) = g c n
Contrary to the situation without
This is witnessed by the following instance:
g = \x y -> seq x 0 p = undefined e = 0