Reasoning about types and code: Talk at SF Scala - October 17, 2019

https://www.meetup.com/SF-Scala/events/265169356/

Talk slides: https://github.com/winitzki/sofp/blob/master/sofp-src/reasoning-types-code-sf-scala.pdf

Talk Summary:

Functional programming is unique among programming paradigms because it allows us to reason rigorously about types and computations before we start writing code. In this way, functional programming is the only paradigm that makes the work of a software developer resemble the work of an engineer. I have been working on 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 directly useful to functional programmers. Typical tasks are to determine whether a function with given type signature can be implemented; to write code for a typeclass method that satisfies the laws; and to transform a data type to an equivalent but simpler form. In this presentation, I show in detail two specific examples of mathematical reasoning using a notation I developed in the book. The first example is to derive the equivalence between three different formulations of the free monad. The second example is a proof (in 5 lines of calculations) that a certain complicated monad transformer satisfies its laws, - a proof that a recent academic paper failed to complete because such calculations are too hard when written in the syntax of code in a programming language.