Advanced Functional Programming

News: Re-examination subjects available!

Course objectives

After completing the course, the students should be

  • comfortable with standard combinators such as: fold, unfold, fmap, naturality (parametricity);
  • comfortable with monads and monad transformers;
  • comfortable with advanced type system features: GADTs, functional dependencies;
  • able to formulate specifications using dependent types;
  • understand the relationship between dependent types and Haskell extensions.

More general objectives:

  • able to use and appreciate equational reasoning;
  • understand programming by refinement;
  • understand the use of functional programming as a method of specification and conceptual analysis;
  • able to read scientific literature related to advanced functional programming.

Timetable

Lectures every Thursday, 10:00-12:00 in Takustr. 9 SR 049.

Exercises every Wednesday 12:00-14:00 in Arnimallee 6 SR 007/008.

Practice Problems

In the extra exercises session of Monday, July 15th, we worked through an exercise sheet which is similar to the one you will receive in the exam.  I have added one or two extra exercises, and uploaded it here.

The exam exercises.

The re-exam exercises.

Lectures

Summaries of the 12 lectures.  Thanks to everybody who contributed corrections: R. Möhn, C. Horst, N. Botta, T. Richter, N. Geyso, Lusy (?).

Lecture 1 summary.

Paramorphisms.

Lecture 2 summary.

Concatenate as a fold. A summary of the derivation of |(++)| as a |foldr|.

Lecture 3 summary.

Lecture 4 summary.

Lecture 5 summary.

Lecture 6 summary.

Lecture 7 summary .

Lecture 8 summary.

Lecture 9 summary.

Lecture 10 summaries: Part1, Part2, Part3.

Commutativity of plus as seen in the exercises session June 26th, calculational style (Cezar) and proof-tactics style (Edwin).

Lecture 11 was given by Edwin Brady: slides, code.

Lecture 12: Agda code, Idris code (without with, or withless).  Once the with Idris with construct works, there will be a corresponding Idris version here.

 

Coursework

The exercises sheets.

Exercises 1.

Exercises 2.

Exercises 3.

Exercises 4.

Exercises 5.

Exercises 6.

Exercises 7.

Exercises 8.

Exercises 9.

Exercises 10.

Exercises 11.

Exercises 12.

Literature

In the first part of the course, we will make extensive use of Richard Bird's Introduction to Functional Programming using Haskell (Prentice Hall, 1998).

 

Suggestions for further reading.

We have covered almost all the material in Bird's book, but you can still find a lot of interesting examples and exercises (which you should have no problem doing).  In particular, the chapter on monadic parsing should be on your reading list.


The book Pearls of Functional Programming Design (Cambridge University Press, 2010), also by Richard Bird, has a lot more examples of calculating functional programs.  They are longer and certainly more spectacular than what we've been doing in the course, but not more difficult.

 

After being exposed to folds and unfolds in a cottage industry kind of way, you should be well-placed to appreciate the elegant framework provided by category theory.  The first three chapters of The Algebra of Programming (Prentice Hall, 1997) by Richard Bird and Oege de Moor,  are the best presentation I know of for the functional programmer.  And the best preparation for them are Graham Hutton's lecture notes.

Useful links