# Correctness of short cut fusion

### From HaskellWiki

(Difference between revisions)

(wrote new page) |
(commit additions) |
||

Line 23: | Line 23: | ||

<haskell> |
<haskell> |
||

− | foldr c n (build g) => g c n |
+ | foldr c n (build g) <nowiki>→</nowiki> g c n |

</haskell> |
</haskell> |
||

− | |||

===<hask>destroy</hask>/<hask>unfoldr</hask>=== |
===<hask>destroy</hask>/<hask>unfoldr</hask>=== |
||

Line 49: | Line 48: | ||

<haskell> |
<haskell> |
||

− | destroy g (unfoldr p e) => g p e |
+ | destroy g (unfoldr p e) <nowiki>→</nowiki> g p e |

</haskell> |
</haskell> |
||

Line 112: | Line 111: | ||

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

</haskell> |
</haskell> |
||

+ | |||

+ | What ''is'' known is that semantic equivalence can be recovered here by putting moderate restrictions on p. |
||

+ | More precisely, if <hask>g</hask> does not use <hask>seq</hask> and <hask>p</hask> is a strict function that never returns <hask>Just <math>\bot</math></hask> (where <math>\bot</math> denotes any kind of failure or nontermination), then indeed: |
||

+ | |||

+ | <haskell> |
||

+ | destroy g (unfoldr p e) = g p e |
||

+ | </haskell> |
||

+ | |||

+ | ===In presence of <hask>seq</hask>=== |
||

+ | |||

+ | This is the more interesting setting, given that in Haskell there is no way to retrict the use of <hask>seq</hask>, so in any given program we must be prepared for the possibility that the <hask>g</hask> appearing in the <hask>foldr</hask>/<hask>build</hask>- or the <hask>destroy</hask>/<hask>unfoldr</hask>-rule is defined using <hask>seq</hask>. |

## 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