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.