# Correctness of short cut fusion

### From HaskellWiki

Line 166: | Line 166: | ||

Here the left-hand side of the rule (<hask>destroy g (unfoldr p e)</hask>) yields <hask>0</hask>, while the right-hand side (<hask>g p e</hask>) yields <hask>undefined</hask>. | Here the left-hand side of the rule (<hask>destroy g (unfoldr p e)</hask>) yields <hask>0</hask>, while the right-hand side (<hask>g p e</hask>) yields <hask>undefined</hask>. | ||

+ | |||

+ | Conditions for semantic approximation in either direction can be given as follows. | ||

+ | |||

+ | If <hask>p <math>\neq\bot</math></hask> and <hask>(p <math>\bot</math>)<math>\in\{\bot,</math>Just <math>\bot\}</math></hask>, then: | ||

+ | |||

+ | <haskell> | ||

+ | destroy g (unfoldr p e) <math>\sqsubseteq</math> g p e | ||

+ | </haskell> | ||

+ | |||

+ | If <hask>p</hask> is strict and total and never returns <hask>Just <math>\bot</math></hask>, then: | ||

+ | |||

+ | <haskell> | ||

+ | destroy g (unfoldr p e) <math>\sqsupseteq</math> g p e | ||

+ | </haskell> | ||

+ | |||

+ | Of course, conditions for semantic equivalence can be obtained by combining the two laws above. |

## Revision as of 15:21, 6 July 2006

## Contents |

## 1 Short cut fusion

*Short cut fusion* allows elimination of intermediate data structures using rewrite rules that can also be performed automatically during compilation.

### 1.1 foldr/build

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 (:) []

*rank-2 polymorphic*type of

foldr c n (build g) <nowiki>→</nowiki> g c n

### 1.2 destroy/unfoldr

The 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'

*rank-2 polymorphic*type of

destroy g (unfoldr p e) <nowiki>→</nowiki> g p e

## 2 Correctness

If the*RULES pragmas*, we clearly want them to be equivalences.

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

#### 2.1.1 foldr/build

If foldr c n (build g) = g c n

The two sides are semantically interchangeable.

#### 2.1.2 destroy/unfoldr

The 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!**".

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.

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.

#### 2.2.1 foldr/build

In the presence of The instance

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, iffoldr c n (build g) = g c n

#### 2.2.2 destroy/unfoldr

Contrary to the situation without This is witnessed by the following instance:

g = \x y -> seq x 0 p = undefined e = 0

Conditions for semantic approximation in either direction can be given as follows.

Ifdestroy g (unfoldr p e) <math>\sqsubseteq</math> g p e

destroy g (unfoldr p e) <math>\sqsupseteq</math> g p e

Of course, conditions for semantic equivalence can be obtained by combining the two laws above.