A tutorial on the universality and expressiveness of fold

This paper by Graham Hutton (http://www.cs.nott.ac.uk/~pszgmh/fold.pdf) provides a great introduction to reasoning with functional programs through the humble 'fold' operator. It gives an insight into how functional programs can be correct by construction and how functional programs can be programatically transformed. The audience is not expected to know functional programming... To help with understanding, I will express concretely many of the points covered in the paper in Haskell. Thanks!