Editing Correctness of short cut fusion (section)

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