Editing Correctness of short cut fusion (section)

===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.