For finite lists, use structural induction: establish
P []; then, for arbitrary x and xs, assume P xs and prove P (x:xs). The induction hypothesis must quantify over any other parameters that need to change in the step.For all Haskell list values, finite terminating spines are insufficient: also establish
P undefined, and allow arbitrary, possibly undefined, heads in the cons step. This proves the equation for finite partial lists ending in the bottom value. An infinite lazy list is the limit of these finite approximations. Equations between pure definable computable functions are preserved by those limits, so the equation extends to infinite inputs. This last argument requires that admissibility property; an arbitrary logical property of lists need not have it. The distinction between [] and the bottom value is essential.[ref]Take compatible function types
f :: b -> c, g :: b -> a -> b, and h :: c -> a -> c. The necessary conditions obtained from the two induction base cases are strictness of f and the fusion equationAt zs = [], the desired equation is exactly the displayed fusion equation. At zs = undefined, both left folds diverge because their list argument has no outer constructor; the equation therefore requires f undefined = undefined. This is the strict function condition. If only finite total spines were considered, the first condition would not be necessary.These conditions also support the step. The induction hypothesis must hold for every accumulator and element. For The middle rewrite uses the fusion equation at
z:zs, instantiate that hypothesis at g x y and z:f (foldl g (g x y) (z:zs))
= f (foldl g (g (g x y) z) zs)
= foldl h (h (f (g x y)) z) zs
= foldl h (h (h (f x) y) z) zs
= foldl h (h (f x) y) (z:zs).x,y. For pure computable functions, equality on infinite spines follows from finite approximations as in part (a).Prove the stronger equation, quantified over the accumulator:For Thus structural induction proves the claim for finite and finite partial spines; definable continuity extends it to infinite lazy lists. Pointwise equality is exactly the asserted equality of function compositions. This is the left-fold fusion law.
[], both sides are f a. For the bottom value, both sides are bottom because f is a strict function. For the cons step, the universal induction hypothesis allows the accumulator to become g a x:f (foldl g a (x:xs))
= f (foldl g (g a x) xs)
= foldl h (f (g a x)) xs
= foldl h (h (f a) x) xs
= foldl h (f a) (x:xs).Use a type with distinct values Since
a and n, and let s _ y = y. Suppose a direct right fold with the same result type represented this left fold. The empty list forces k = n. The singleton lists force c n n = n and c a n = a. But thenfoldr c k [a,n] = c a (c n n) = c a n = a,
foldl s n [a,n] = n.a /= n, this is a counterexample. A direct right fold cannot recover whether its tail result n came from the empty list or from the singleton [n]. The obstruction already occurs on finite total inputs, so it also rules out an implementation valid on all lazy lists.Change the right fold's result type to an accumulator-transforming function type:Thus
foldlAsFoldr :: (b -> a -> b) -> b -> [a] -> b
foldlAsFoldr s n xs = foldr c id xs n
where
c x k a = k (s a x)c x k = \a -> k (s a x) and k = id in the question's notation. Here c :: a -> (b -> b) -> (b -> b), and the fold's base value is the identity function, not the initial accumulator n.The recursion invariant is At an undefined spine, applying the undefined folded function also gives the bottom value. The finite-approximation argument then covers infinite lazy lists. This is a continuation representation of a left fold: the result retains the operation still to be performed, avoiding the information loss in part (d).
foldr c id xs a = foldl s a xs for every a. For [], both sides equal a. For a cons:foldr c id (x:xs) a
= c x (foldr c id xs) a
= foldr c id xs (s a x)
= foldl s (s a x) xs
= foldl s a (x:xs). Articles by others on the same topic
There are currently no matching articles.