Yet Another Small Exercise

The following problem description is taken from exercise 7.39 of AoP:

The function takeWhile of functional programming can be specified by

takeWhile p = max R . Λ(list p . prefix)

where R = lengthº . leq . length. In word, takeWhile p x returns the longest prefix of x with the property that all its elements satisfy p. (Question: why the longest here rather than a longest?) Using prefix = cata [nil, cons ∪ nil] and the greedy theorem, derive the standard implementation of takeWhile.

(The answer to the small question is that a prefix of a given length is unique.) My aim, however, is to play with functional derivation. Therefore

The purpose of the first fusion is to transform the generating part into a fold, in hope that the greedy theorem can be applied.

One small property I didn't prove is filter ((t ∧) . p) = (const t → filter p, nil . !), which is a rather straightforward one.

And the second fusion tries to promote max into the generating fold, which is the spirit of the greedy theorem. I didn't formulate the greedy theorem in functional form, though, so I simply do the fusion.

In fact I don't know precisely which part should be called the monotonicity condition. Maybe it will become clear to me after I prove the greedy theorem (by fold fusion) and compare the proof to this derivation and the derivation of maximum prefix sum. Having experience dealing with maximum prefix sum, I guess the following property is an essential one.

This is the fusion condition for (x:) . max ≤ℓ. Applying type functor fusion to max ≤ℓ . map (x:), we would have max ≤ℓ . map (x:) = (x:) . max ≤ℓ, a premise used in the second fusion.

The entire derivation is very similar to maximum prefix sum, which is certainly no surprise. They are both applications of the greedy theorem. I mixed Haskell and AoP syntax as well as curried and uncurried forms. Hope it's not too confusing.

--
Time to study AoP chap. 7!