Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 4 / d / Solution

First define argument reversal, with its most general polymorphic type signature:

flip :: (a -> b -> c) -> b -> a -> c
flip f y x = f x y

Use concat = foldr (++) []. In the right-fold fusion law, choose f = foldr fn e, g = (++), a = [], b = e, and h = flip (foldr fn). The base-image condition follows from foldr fn e [] = e; strictness follows because a right fold inspects its input spine. Part (c) supplies exactly the compatibility condition:

f (xs ++ ys)
  = foldr fn (foldr fn e ys) xs
  = flip (foldr fn) xs (f ys)
  = h xs (f ys)

Consequently,The accumulator argument of foldr fn comes before the inner list, whereas the outer right fold supplies the inner list first; flip reconciles those orders. The proof uses fusion and the already proved concatenation identity, without a further induction.