Functional programming. Reasoning about types and code (hors série)

I have been writing up my functional programming tutorials as chapters for a new book, "The Science of Functional Programming". This presentation focuses on one of the main themes of the book - the techniques and applications of mathematical reasoning about types and code.

I give examples of type and code reasoning tasks that are useful to practitioners of functional programming. Typical tasks are to determine whether a value of a given type can be computed, to implement a typeclass method that satisfies the laws, and to transform a type constructor to a mathematically equivalent but simpler form.

While working on my functional programming tutorials, I had to work through many derivations that were difficult to perform using the Scala syntax. To make this work easier, I have developed a condensed notation for calculations with types and code, which appears to be well adapted to reasoning tasks. In this presentation, I show the advantages of the condensed notation on two examples. First, I derive the equivalence between three different formulations of the free monad. Second, I prove (in 5 lines of calculations) the monad associativity law for the selector monad transformer, - a proof that a recent academic paper failed to carry out because such calculations are often unmanageable when written in the syntax of a programing language.

In the forthcoming free book, "The Science of Functional Programming", I will present detailed explanations and examples of the available techniques for type and code reasoning. The book's source code and current draft versions are available at https://github.com/winitzki/sofp

The current draft of the book can be downloaded as PDF at https://github.com/winitzki/sofp or purchased on paper at http://www.lulu.com/content/paperback-book/the-science-of-functional-programming/24915714

Slides for this talk: https://github.com/winitzki/sofp/blob/master/sofp-src/reasoning-types-code.pdf