Editing Correctness of short cut fusion (section)

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

As above, the compiler cannot figure out automatically whether (and how) a given instance of <hask>destroy</hask>/<hask>unfoldr</hask>-fusion will change the semantics of a program.

An easy way to get rid of the condition regarding <hask>p</hask> never returning <hask>Just ⊥</hask> is to slightly change the definitions of the functions involved:

<haskell>
data Step a b = Done | Yield a b

destroy' :: (forall b. (b -> Step a b) -> b -> c) -> [a] -> c
destroy' g = g step'

step' :: [a] -> Step a [a]
step' []     = Done 
step' (x:xs) = Yield x xs

unfoldr' :: (b -> Step a b) -> b -> [a]
unfoldr' p e = case p e of Done       -> []
                           Yield x e' -> x:unfoldr' p e'
</haskell>

The new type <hask>Step a b</hask> is almost isomorphic to <hask>Maybe (a,b)</hask>, but avoids the "junk value" <hask>Just ⊥</hask>. This change does not affect the expressiveness of <hask>unfoldr</hask> or <hask>unfoldr'</hask> with respect to list producers.
But it allows some of the laws above to be simplified a bit.

We would still have that if <hask>g</hask> does not use <hask>seq</hask>, then:

<haskell>
destroy g' (unfoldr' p e) ⊑ g p e
</haskell>

Moreover, if <hask>g</hask> does not use <hask>seq</hask> and <hask>p</hask> is strict, then even:

<haskell>
destroy' g (unfoldr' p e) = g p e
</haskell>

In the potential presence of <hask>seq</hask>, if <hask>p ≠ ⊥</hask> and <hask>p</hask> is strict, then: 

<haskell>
destroy' g (unfoldr' p e) ⊑ g p e
</haskell>

Also without restriction regarding <hask>seq</hask>, if <hask>p</hask> is strict and total, then:

<haskell>
destroy' g (unfoldr' p e) ⊒ g p e
</haskell>

The worst change in program behavior from a complier user's point of view is when, through application of "optimization" rules, a safely terminating program is transformed into a failing one or one delivering a different result.
This can happen in the presence of <hask>seq</hask>, for example with a producer of the form

<haskell>
repeat x = unfoldr (\y -> Just (x,y)) undefined
</haskell>

or 

<haskell>
repeat x = unfoldr' (\y -> Yield x y) undefined
</haskell>

Fortunately, it cannot happen for any producer of a nonempty, spine-total list (i.e., one that contains at least one element and ends with <hask>[]</hask>).
The reason is that for any such producer expressed via <hask>unfoldr</hask> or <hask>unfoldr'</hask> the conditions imposed on <hask>p</hask> in the left-to-right approximation laws above are necessarily fulfilled.

A left-to-right approximation as in 

<haskell>
destroy g (unfoldr p e) ⊑ g p e
</haskell>

under suitable preconditions might be acceptable in practice.
After all, it only means that the transformed program may be "more terminating" than the original one, but not less so.

If one insists on semantic equivalence rather than approximation, then the conditions imposed on the producer of the intermediate list become quite severe, in particular in the potential presence of <hask>seq</hask>.
For example, the following producer has to be outlawed then: 

<haskell>
enumFromTo n m = unfoldr (\i -> if i>m then Nothing else Just (i,i+1)) n
</haskell>