Scott Fleischman: Agda from Nothing: Order in the Types - λC Winter Retreat 2017

Scott Fleischman teaches Agda from first principles, focusing on implementing correct-by-construction ordered data structures like binary search trees.

In this two-hour workshop we will learn Agda from first principles with a focus on ordered data structures. To get used to Agda we will explore basic types for natural numbers, lists and trees, working toward implementing a binary search tree. We will then try a couple different ways of making the binary search tree correct-by-construction with regard to its ordering invariant. Once we have achieved our goal of creating one ordered container structure, we will make it systematic by creating a universe of all ordered container structures. Within this universe we will see what lists, trees, and our binary search tree looks like. There are minimal prerequisites for this workshop—familiarity with curried functions is perhaps the starting point. The concepts build on one another throughout the talk. The expected takeaway for the first two-thirds is a working experience with binary search trees in a dependently-typed setting. The final third of the workshop ramps up quickly in abstract concepts so the expectation shifts more to exposure to the concepts rather than a detailed understanding of them. The workshop follows the outline of Conor McBride’s paper How to Keep Your Neighbours in Order (2014) [pdf]. The Agda code from the paper is reworked for the needs of the workshop, in particular making the proofs explicit. There will be a mixture of live coding and slides. The key goals for the workshop are to come away with: A working knowledge of the basics of Agda Experience encoding an invariant in a dependently-typed data structure An sense of the advantages of using prescriptive types over descriptive ones Exposure to the concepts of an Agda program of non-trivial size and complexity