2 Preface

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

My motivation for wanting to teach from PLFA using Agda are similar to those described by Philip Wadler in the preface to PLFA. If you haven’t done so already, you should read that preface now.

When I first started teaching the theory of programming languages, I used the textbook Types and Programming Languages (TaPL) by Benjamin Pierce (five times now, in CS 442). The proofs there are on paper, written by humans for humans, and it is sometimes difficult to get students to engage with them seriously. Pierce and co-authors went on to develop the online textbook Software Foundations (SF), which uses the Coq proof assistant to formalize some of the proofs in TaPL. I used SF at graduate level (three times, in CS 798), as well as using ideas from it at the undergraduate level (three times, in CS 245E). (The preface to SF is an excellent overview of the motivations for CS 747, and you should also read that as well.)

SF is a great resource, and student reaction to it (and courses I have taught using it) has always been positive. However, I found myself subverting its decision to work nearly always at the top level of abstraction in Coq (proof scripts written using tactics). My subversion consisted of an early exposition of the correspondence between propositions and types (that SF leaves to a late, optional chapter, and PLFA discusses in the first paragraph of the Preface) and by exposing the proof objects (dependently-typed code) that the scripts were manipulating and constructing. In Agda, one works directly with proof objects, so there’s no need for subversion.

Agda and Coq are both dependently-typed programming languages, and have much in common, including some early developers. Coq has a longer history. It is implemented in OCaml, and its syntax resembles OCaml. Agda is implemented in Haskell, and its syntax resembles Haskell. The current version, Agda 2, is largely due to Ulf Norell, and his PhD thesis from 2007 is a good source of information if you really want to know how things work. But both Coq and Agda are under active development, and texts using them often require tweaks after new releases.

In a type system which supports dependent types, the result type of a function can depend on the value of its parameter. It’s not immediately clear why this would be valuable, because most type systems don’t offer this possibility. One big motivation, as the demo showed, is that logical statements behave this way. A theorem like "For all natural numbers \(m\), \(m + 0 = m\)" is used by instantiating it for a particular value of m. For example, we can conclude "\(4 + 0 = 4\)". The theorem can be viewed as a function that consumes a natural number \(m\) and produces a proof that "\(m + 0 = m\)" for that specific value.

In a dependently-typed programming language, types are expressive enough to encode logical statements. The proof of such a statement is a value of that type. This is what Wadler refers to as "propositions as types" in the preface (he has written an expository paper with that title, from which PLFA sometimes quotes). It is also known as the Curry-Howard correspondence between logic and type theory.

This is quite appealing, as it means that to prove something, one gets to write a program. But there are costs. In order to keep the logical system consistent, all functions must be total (no partial functions, no exceptions, no infinite loops) and termination should be relatively obvious (because Agda’s termination checker is fairly simple-minded). Writing code that typechecks becomes harder, so both Coq and Agda offer interactive development, where code is refined with the help of information from the compiler in a very tight feedback loop. This is independently quite appealing.

SF has had more than a decade of development and has been used at many institutions. Despite my considerable respect for it, my differences with its approach were enough to make me reconsider its use. PLFA was first released in early 2019, and has been used in only a few courses. Both books are under active development, just like the languages they use. I will do some things differently from PLFA; these notes should help explain how and why.