One of the most important advantages of functional programming languages is that they allow us to construct programs from specifications by calculation. The expressivity of functional programming enables the formulation of specifications as (usually very inefficient) programs, which can then be optimized by equational reasoning using algebraic identities, in a process reminiscent of high-school mathematics. In this lecture, we will introduce a number of such algebraic identities, and use them in the presentation of a "canonical" example of program calculation: computing a linear-time solution to the maximum segment sum problem.
The prepared lecture material is in Part1.lhs and Part2.lhs. The actual material covered during L14 was bascially the contents of Part1.lhs while the second part is additional reading and a few proofs which did not fit in the time-slot.
Micro-bio: Cezar Ionescu is currently a PostDoc on "Increasingly Correct Scientific Computing" in the FP group at Chalmers. Before that he worked for several years at the Potsdam Institute for Climate Impact Research where he applied AFP in the form of Haskell, C++, Agda and Idris to Computational Vulnarability Assessment, Scientific Computing and Economic Models.
Reading:
- Chapter 6 of "Thinking Functionally with Haskell", Richard Bird, Cambridge University Press, 2014
- Chapter 4 of "Introduction to Functional Programming using Haskell second edition", Richard Bird, Prentice Hall, 1998
- "Algebraic Identities for Program Calculation", Richard Bird, The Computer Journal, Vol. 32, No. 2, 1989, pp 122-126
For reference: