Editing Correctness of short cut fusion (section)

==Correctness==

If the <hask>foldr</hask>/<hask>build</hask>- and the <hask>destroy</hask>/<hask>unfoldr</hask>-rule are to be automatically performed during compilation, as is possible using [[GHC]]'s ''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 <hask>g</hask> is defined using <hask>seq</hask> or not.

===In the absence of <hask>seq</hask>===

====<hask>foldr</hask>/<hask>build</hask>====

If <hask>g</hask> does not use <hask>seq</hask>, then the <hask>foldr</hask>/<hask>build</hask>-rule really is a semantic equivalence, that is, it holds that 

<haskell>
foldr c n (build g) = g c n
</haskell>

The two sides are interchangeable in any program without affecting semantics.

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

The <hask>destroy</hask>/<hask>unfoldr</hask>-rule, however, is not a semantic equivalence.
To see this, consider the following instance:

<haskell>
g = \x y -> case x y of Just z -> 0
p = \x -> if x==0 then Just undefined else Nothing
e = 0
</haskell>

These values have appropriate types for being used in the <hask>destroy</hask>/<hask>unfoldr</hask>-rule. But with them, that rule's left-hand side "evaluates" as follows:

<haskell>
destroy g (unfoldr p e) = g step (unfoldr p e)
                        = case step (unfoldr p e) of Just z -> 0
                        = case step (case p e of Nothing     -> []
                                                 Just (x,e') -> x:unfoldr p e') of Just z -> 0
                        = case step (case Just undefined of Nothing     -> []
                                                            Just (x,e') -> x:unfoldr p e') of Just z -> 0
                        = undefined
</haskell>

while its right-hand side "evaluates" as follows:

<haskell>
g p e = case p e of Just z -> 0
      = case Just undefined of Just z -> 0
      = 0
</haskell>

Thus, by applying the <hask>destroy</hask>/<hask>unfoldr</hask>-rule, a nonterminating (or otherwise failing) program can be transformed into a safely terminating one.
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 <hask>g</hask> does not use <hask>seq</hask>, then the <hask>destroy</hask>/<hask>unfoldr</hask>-rule is a semantic approximation from left to right, that is, it holds that

<haskell>
destroy g (unfoldr p e) ⊑ g p e
</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 ⊥</hask> (where ⊥ denotes any kind of failure or nontermination), then indeed:

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

===In the presence of <hask>seq</hask>===

This is the more interesting setting, given that in Haskell there is no way to restrict 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>.
Unsurprisingly, it is also the setting in which more can go wrong than above.

====<hask>foldr</hask>/<hask>build</hask>====

In the presence of <hask>seq</hask>, the <hask>foldr</hask>/<hask>build</hask>-rule is not necessarily a semantic equivalence.
The instance

<haskell>
g = seq
c = undefined
n = 0
</haskell>

shows, via similar "evaluations" as above, that the right-hand side (<hask>g c n</hask>) can be strictly less defined than the left-hand side (<hask>foldr c n (build g)</hask>).

The converse cannot happen, because the following always holds:

<haskell>
foldr c n (build g) ⊒ g c n
</haskell>

Moreover, semantic equivalence can again be recovered by putting restrictions on the involved functions.

On the consumption side, if <hask>(c ⊥ ⊥) ≠ ⊥</hask> and <hask>n ≠ ⊥</hask>, then even in the presence of <hask>seq</hask>:

<haskell>
foldr c n (build g) = g c n
</haskell>

On the production side, <hask>seq</hask> can be used safely as long as it is never used to force anything whose type <hask>build</hask> expects to be polymorphic. In particular, the function passed to build must not force either of its arguments, and must not force anything constructed using them. For example, in

<haskell>
f x = build (\c n -> x `seq` (x `c` n))
</haskell>

The usual equivalence holds, regardless of <hask>c</hask> and <hask>n</hask>:

<haskell>
fold c n (f x) = x `seq` (x `c` n)
</haskell>

For a more interesting example, we can define

<haskell>
hyloList f q c n =
  case f q of
    Nothing     -> n
    Just (x,q') -> x `c` hyloList f q' c n

unfoldr f q = build (hyloList f q)
</haskell>

Note that if <hask>f</hask> or <hask>q</hask> uses <hask>seq</hask>, then that will appear in the argument to <hask>build</hask>, but that is still safe because <hask>f</hask> and <hask>q</hask> have no way to get their hands on <hask>c</hask>, <hask>n</hask>, or anything built from them.

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

Contrary to the situation without <hask>seq</hask>, now also the <hask>destroy</hask>/<hask>unfoldr</hask>-rule may decrease the definedness of a program.
This is witnessed by the following instance:

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

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 ≠ ⊥</hask> and <hask>(p ⊥)</hask> ∈ {<hask>⊥</hask>, <hask>Just ⊥</hask>}, then: 

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

If <hask>p</hask> is strict and total and never returns <hask>Just ⊥</hask>, then:

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

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