# Correctness of short cut fusion

### From HaskellWiki

(Difference between revisions)

(wrote new page) |
(commit additions) |

## Revision as of 14:41, 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.

foldr

build

destroy

unfoldr

### 1.1 foldr/build

The foldr

build

foldr

build

build

foldr

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

build

foldr

build

g

c

n

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

### 1.2 destroy/unfoldr

The destroy

unfoldr

destroy

unfoldr

unfoldr

destroy

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

destroy

unfoldr

g

p

e

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

## 2 Correctness

If thefoldr

build

destroy

unfoldr

*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 whetherg

seq

### 2.1 In absence of seq

If seq

g

seq

foldr

build

foldr c n (build g) = g c n

The two sides are semantically interchangeable.

Thedestroy

unfoldr

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

unfoldr

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

destroy

unfoldr

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

g

seq

destroy

unfoldr

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.

g

seq

p

Just <math>\bot</math>

destroy g (unfoldr p e) = g p e

### 2.2 In presence of seq

This is the more interesting setting, given that in Haskell there is no way to retrict the use of seq

seq

g

foldr

build

destroy

unfoldr

seq