# Correctness of short cut fusion

(Difference between revisions)
 Revision as of 13:29, 7 July 2006 (edit) (finished up)← Previous diff Current revision (04:11, 3 July 2011) (edit) (undo)m (just a small formatting edit) (18 intermediate revisions not shown.) Line 1: Line 1: ==Short cut fusion== ==Short cut fusion== - ''Short cut fusion'' allows elimination of intermediate data structures using rewrite rules that can also be performed automatically during compilation. + [[Short cut fusion]] allows elimination of intermediate data structures using rewrite rules that can also be performed automatically during compilation. The two most popular instances are the foldr/build- and the destroy/unfoldr-rule for Haskell lists. The two most popular instances are the foldr/build- and the destroy/unfoldr-rule for Haskell lists. Line 23: Line 23: - foldr c n (build g) g c n + foldr c n (build g) → g c n Line 48: Line 48: - destroy g (unfoldr p e) g p e + destroy g (unfoldr p e) → g p e Line 113: Line 113: - destroy g (unfoldr p e) $\sqsubseteq$ g p e + destroy g (unfoldr p e) ⊑ g p e What ''is'' known is that semantic equivalence can be recovered here by putting moderate restrictions on p. What ''is'' known is that semantic equivalence can be recovered here by putting moderate restrictions on p. - More precisely, if g does not use seq and p is a strict function that never returns Just $\bot$ (where $\bot$ denotes any kind of failure or nontermination), then indeed: + More precisely, if g does not use seq and p is a strict function that never returns Just ⊥ (where ⊥ denotes any kind of failure or nontermination), then indeed: Line 144: Line 144: - foldr c n (build g) $\sqsupseteq$ g c n + foldr c n (build g) ⊒ g c n Moreover, semantic equivalence can again be recovered by putting restrictions on the involved functions. Moreover, semantic equivalence can again be recovered by putting restrictions on the involved functions. - More precisely, if (c $\bot~\bot)\neq\bot$ and n $\neq\bot$, then even in the presence of seq: + More precisely, if (c ⊥ ⊥) ≠ ⊥ and n ≠ ⊥, then even in the presence of seq: Line 169: Line 169: Conditions for semantic approximation in either direction can be given as follows. Conditions for semantic approximation in either direction can be given as follows. - If p $\neq\bot$ and (p \bot)\in\{\bot,Just $\bot\}$, then: + If p ≠ ⊥ and (p ⊥) ∈ {, Just ⊥}, then: - destroy g (unfoldr p e) $\sqsubseteq$ g p e + destroy g (unfoldr p e) ⊑ g p e - If p is strict and total and never returns Just $\bot$, then: + If p is strict and total and never returns Just ⊥, then: - destroy g (unfoldr p e) $\sqsupseteq$ g p e + destroy g (unfoldr p e) ⊒ g p e Line 186: Line 186: Correctness of short cut fusion is not just an academic issue. Correctness of short cut fusion is not just an academic issue. - There are versions of [[GHC]] (which ones? any officially released ones?) that automatically perform transformations like foldr/build during their optimization pass (also in the disguise of more specialized rules such as head/build). + All recent versions of [[GHC]] (at least 6.0 - 6.6) automatically perform transformations like foldr/build during their optimization pass (also in the disguise of more specialized rules such as head/build). The rules are specified in the GHC.Base and GHC.List modules. - And there has been at least one occasion where, as a result, a safely terminating program was turned into a failing one "in the wild", with a less artificial example than the ones given above. + There has been at least one occasion where, as a result, a safely terminating program was turned into a failing one "in the wild", with a less artificial example than the ones given above. ===foldr/build=== ===foldr/build=== As pointed out above, everything is fine with foldr/build in the absence of seq. As pointed out above, everything is fine with foldr/build in the absence of seq. - If the producer (build g) of the intermediate list may be defined using seq, then the conditions (c $\bot~\bot)\neq\bot$ and n $\neq\bot$ better be satisified, lest the compiler transform a perfectly fine program into a failing one. + If the producer (build g) of the intermediate list may be defined using seq, then the conditions (c ⊥ ⊥) ≠ ⊥ and n ≠ ⊥ better be satisified, lest the compiler transform a perfectly fine program into a failing one. - The mentioned conditions are equivalent to requiring that the consumer (foldr c n) is a total function, that is, maps non-$\bot$ lists to a non-$\bot$ value. + The mentioned conditions are equivalent to requiring that the consumer (foldr c n) is a total function, that is, maps non-⊥ lists to a non-⊥ value. It is thus relatively easy to identify whether a list consumer defined in terms of foldr is eligible for foldr/build-fusion in the presence of seq or not. It is thus relatively easy to identify whether a list consumer defined in terms of foldr is eligible for foldr/build-fusion in the presence of seq or not. For example, the Prelude functions head and sum are generally not, while map is. For example, the Prelude functions head and sum are generally not, while map is. Line 204: Line 204: As above, the compiler cannot figure out automatically whether (and how) a given instance of destroy/unfoldr-fusion will change the semantics of a program. As above, the compiler cannot figure out automatically whether (and how) a given instance of destroy/unfoldr-fusion will change the semantics of a program. - An easy way to get rid of the condition regarding p never returning Just $\bot$ is to slightly change the definitions of the functions involved: + An easy way to get rid of the condition regarding p never returning Just ⊥ is to slightly change the definitions of the functions involved: Line 221: Line 221: - The new type Step a b is almost isomorphic to Maybe (a,b), but avoids the "junk value" Just $\bot$. This change does not affect the expressiveness of unfoldr or unfoldr' with respect to list producers. + The new type Step a b is almost isomorphic to Maybe (a,b), but avoids the "junk value" Just ⊥. This change does not affect the expressiveness of unfoldr or unfoldr' with respect to list producers. But it allows some of the laws above to be simplified a bit. But it allows some of the laws above to be simplified a bit. Line 227: Line 227: - destroy g' (unfoldr' p e) $\sqsubseteq$ g p e + destroy g' (unfoldr' p e) ⊑ g p e Line 236: Line 236: - In the potential presence of seq, if p $\neq\bot$ and p is strict, then: + In the potential presence of seq, if p ≠ ⊥ and p is strict, then: - destroy' g (unfoldr' p e) $\sqsubseteq$ g p e + destroy' g (unfoldr' p e) ⊑ g p e Line 245: Line 245: - destroy' g (unfoldr' p e) $\sqsupseteq$ g p e + destroy' g (unfoldr' p e) ⊒ g p e Line 267: Line 267: - destroy g (unfoldr p e) $\sqsubseteq$ g p e + destroy g (unfoldr p e) ⊑ g p e Line 284: Line 284: Various parts of the above story, and elaborations thereof, are also told in the following papers: Various parts of the above story, and elaborations thereof, are also told in the following papers: - * A. Gill, J. Launchbury, and S.L. Peyton Jones. A short cut to deforestation. Functional Programming Languages and Computer Architecture, Proceedings, pages 223-232, ACM Press, 1993. + * A. Gill, J. Launchbury, and S.L. Peyton Jones. [http://doi.acm.org/10.1145/165180.165214 A short cut to deforestation]. Functional Programming Languages and Computer Architecture, Proceedings, pages 223-232, ACM Press, 1993. - * J. Svenningsson. Shortcut fusion for accumulating parameters & zip-like functions. International Conference on Functional Programming, Proceedings, pages 124-132, ACM Press, 2002. + * J. Svenningsson. [http://doi.acm.org/10.1145/581478.581491 Shortcut fusion for accumulating parameters & zip-like functions]. International Conference on Functional Programming, Proceedings, pages 124-132, ACM Press, 2002. - * P. Johann. On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi. Mathematical Structures in Computer Science, 15:201-229, 2005. + * P. Johann. [http://dx.doi.org/10.1017/S0960129504004578 On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi]. Mathematical Structures in Computer Science, 15:201-229, 2005. - * P. Johann and J. Voigtländer. The impact of seq on free theorems-based program transformations. Fundamenta Informaticae, 69:63-102, 2006. + * P. Johann and J. Voigtländer. [http://iospress.metapress.com/openurl.asp?genre=article&issn=0169-2968&volume=69&issue=1&spage=63 The impact of seq on free theorems-based program transformations]. Fundamenta Informaticae, 69:63-102, 2006. - * J. Voigtländer and P. Johann. Selective strictness and parametricity in structural operational semantics. Technical Report TUD-FI06-02, Technische Universität Dresden, 2006. + * J. Voigtländer and P. Johann. [http://dx.doi.org/10.1016/j.tcs.2007.09.014 Selective strictness and parametricity in structural operational semantics, inequationally]. Theoretical Computer Science, 388:290-318, 2007. + * J. Voigtländer. [http://doi.acm.org/10.1145/1328408.1328412 Proving Correctness via Free Theorems: The Case of the destroy/build-Rule]. Partial Evaluation and Semantics-Based Program Manipulation, Proceedings, pages 13-20, ACM Press, 2008. + * J. Voigtländer. [http://dx.doi.org/10.1007/978-3-540-78969-7_13 Semantics and Pragmatics of New Shortcut Fusion Rules]. Functional and Logic Programming, Proceedings, LNCS 4989:163-179, Springer-Verlag, 2008. + * P. Johann and J. Voigtländer. [http://wwwtcs.inf.tu-dresden.de/~voigt/iandc.pdf A family of syntactic logical relations for the semantics of Haskell-like languages]. Information and Computation, 207:341-368, 2009. + + + + [[Category:Tutorials]] + [[Category:Program transformation]]

## 1 Short cut fusion

Short cut fusion allows elimination of intermediate data structures using rewrite rules that can also be performed automatically during compilation.

The two most popular instances are the
foldr
/
build
- and the
destroy
/
unfoldr

### 1.1 foldr/build

The
foldr
/
build
-rule eliminates intermediate lists produced by
build
and consumed by
foldr
, where these functions are defined as follows:
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 (:) []
Note the rank-2 polymorphic type of
build
. The
foldr
/
build
-rule now means the following replacement for appropriately typed
g
,
c
, and
n
:
foldr c n (build g) → g c n

### 1.2 destroy/unfoldr

The
destroy
/
unfoldr
-rule eliminates intermediate lists produced by
unfoldr
and consumed by
destroy
, where these functions are defined as follows:
destroy :: (forall b. (b -> Maybe (a,b)) -> b -> c) -> [a] -> c
destroy g = g step

step :: [a] -> Maybe (a,[a])
step []     = Nothing
step (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'
Note the rank-2 polymorphic type of
destroy
. The
destroy
/
unfoldr
-rule now means the following replacement for appropriately typed
g
,
p
, and
e
:
destroy g (unfoldr p e) → g p e

## 2 Correctness

If the
foldr
/
build
- and the
destroy
/
unfoldr
-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
g
is defined using
seq
or not.

### 2.1 In the absence of seq

#### 2.1.1 foldr/build

If
g
does not use
seq
, then the
foldr
/
build
-rule really is a semantic equivalence, that is, it holds that
foldr c n (build g) = g c n

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

#### 2.1.2 destroy/unfoldr

The
destroy
/
unfoldr
-rule, however, is not a semantic equivalence.

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

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
Thus, by applying the
destroy
/
unfoldr
-rule, a nonterminating (or otherwise failing) program can be transformed into a safely terminating one.

The obvious questions now are:

1. Can the converse also happen, that is, can a safely terminating program be transformed into a failing one?
2. 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
g
does not use
seq
, then the
destroy
/
unfoldr
-rule is a semantic approximation from left to right, that is, it holds that
destroy g (unfoldr p e) ⊑ g p e

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

More precisely, if
g
does not use
seq
and
p
is a strict function that never returns
Just ⊥
(where ⊥ denotes any kind of failure or nontermination), then indeed:
destroy g (unfoldr p e) = g p e

### 2.2 In the presence of seq

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

Unsurprisingly, it is also the setting in which more can go wrong than above.

#### 2.2.1 foldr/build

In the presence of
seq
, the
foldr
/
build
-rule is not anymore a semantic equivalence.

The instance

g = seq
c = undefined
n = 0
shows, via similar "evaluations" as above, that the right-hand side (
g c n
) can be strictly less defined than the left-hand side (
foldr c n (build g)
).

The converse cannot happen, because the following always holds:

foldr c n (build g) ⊒ g c n

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

More precisely, if
(c ⊥ ⊥) ≠ ⊥
and
n ≠ ⊥
, then even in the presence of
seq
:
foldr c n (build g) = g c n

#### 2.2.2 destroy/unfoldr

Contrary to the situation without
seq
, now also the
destroy
/
unfoldr
-rule may decrease the definedness of a program.

This is witnessed by the following instance:

g = \x y -> seq x 0
p = undefined
e = 0
Here the left-hand side of the rule (
destroy g (unfoldr p e)
) yields
0
, while the right-hand side (
g p e
) yields
undefined
.

Conditions for semantic approximation in either direction can be given as follows.

If
p ≠ ⊥
and
(p ⊥)
∈ {
,
Just ⊥
}, then:
destroy g (unfoldr p e) ⊑ g p e
If
p
is strict and total and never returns
Just ⊥
, then:
destroy g (unfoldr p e) ⊒ g p e

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

## 3 Discussion

Correctness of short cut fusion is not just an academic issue.

All recent versions of GHC (at least 6.0 - 6.6) automatically perform transformations like
foldr
/
build
during their optimization pass (also in the disguise of more specialized rules such as
/
build
). The rules are specified in the GHC.Base and GHC.List modules.

There has been at least one occasion where, as a result, a safely terminating program was turned into a failing one "in the wild", with a less artificial example than the ones given above.

### 3.1 foldr/build

As pointed out above, everything is fine with
foldr
/
build
in the absence of
seq
. If the producer (
build g
) of the intermediate list may be defined using
seq
, then the conditions
(c ⊥ ⊥) ≠ ⊥
and
n ≠ ⊥
better be satisified, lest the compiler transform a perfectly fine program into a failing one. The mentioned conditions are equivalent to requiring that the consumer (
foldr c n
) is a total function, that is, maps non-⊥ lists to a non-⊥ value. It is thus relatively easy to identify whether a list consumer defined in terms of
foldr
is eligible for
foldr
/
build
-fusion in the presence of
seq
or not. For example, the Prelude functions
and
sum
are generally not, while
map
is. There is, however, currently no way to detect automatically, inside the compiler, whether a particular instance of
foldr
/
build
-fusion is safe, i.e., whether the producer avoids
seq
or the consumer is total.

### 3.2 destroy/unfoldr

As above, the compiler cannot figure out automatically whether (and how) a given instance of
destroy
/
unfoldr
-fusion will change the semantics of a program. An easy way to get rid of the condition regarding
p
never returning
Just ⊥
is to slightly change the definitions of the functions involved:
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'
The new type
Step a b
is almost isomorphic to
Maybe (a,b)
, but avoids the "junk value"
Just ⊥
. This change does not affect the expressiveness of
unfoldr
or
unfoldr'
with respect to list producers.

But it allows some of the laws above to be simplified a bit.

We would still have that if
g
does not use
seq
, then:
destroy g' (unfoldr' p e) ⊑ g p e
Moreover, if
g
does not use
seq
and
p
is strict, then even:
destroy' g (unfoldr' p e) = g p e
In the potential presence of
seq
, if
p ≠ ⊥
and
p
is strict, then:
destroy' g (unfoldr' p e) ⊑ g p e
Also without restriction regarding
seq
, if
p
is strict and total, then:
destroy' g (unfoldr' p e) ⊒ g p e

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
seq
, for example with a producer of the form
repeat x = unfoldr (\y -> Just (x,y)) undefined

or

repeat x = unfoldr' (\y -> Yield x y) undefined
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
[]
). The reason is that for any such producer expressed via
unfoldr
or
unfoldr'
the conditions imposed on
p
in the left-to-right approximation laws above are necessarily fulfilled.

A left-to-right approximation as in

destroy g (unfoldr p e) ⊑ g p e

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

For example, the following producer has to be outlawed then:

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

## 4 Literature

Various parts of the above story, and elaborations thereof, are also told in the following papers: