Review: Practical Foundations for Programming Languages

A lot of my work revolves around various problems encountered when one tries to automate the production of hardware from a description of the behaviour the hardware is supposed to exhibit when in use. This problem has a long history, most recently going by the name “High Level Synthesis”. A natural question, but one that is oddly rarely asked in computer-aided design, is “what kind of description?”

Of course not only hardware designers need to specify behaviour. The most common kind of formal description is that of a programming language, so it seems natural to ask what the active community of programming language specialists have to say. I am  fortunate enough to be an investigator on a multidisciplinary EPSRC project with my friend and colleague Dan Ghica, specifically aimed at bringing together these two communities, and I thought it was time to undertake sufficient reading to help me bridge some gaps in terminology between our fields.

With this is mind, I recently read Bob Harper‘s Practical Foundations for Programming Languages. For an outsider to the field, this seems to be a fairly encyclopaedic book describing a broad range of theory in a fairly accessible way, although it did become less readily accessible to me as the book progressed. My colleague Andy Pitts is quoted on the back cover as saying that this book “reveals the theory of programming languages as a coherent scientific subject,” so with no further recommendation required, I jumped in!

I like the structure of this book because as a non-specialist I find this material heavy going: Harper has split a 500 page book into fully 50 chapters, which suits me very well. Each chapter has an introduction and a “notes” section and – for the parts in which I’m not very interested – I can read these bits to still get the gist of the material. Moreover, there is a common structure to these chapters, where each feature is typically first described in terms of its statics and then its dynamics. The 50 chapters are divided into 15 “parts”, to provide further structure to the material.

The early parts of the book are interesting, but not of immediate practical relevance to me as someone who wants to find a use for these ideas rather than study them in their own right. It is nice, however, to see many of the practical concepts I use in the rare occasions I get to write my own code, shown in their theoretical depth – function types, product types, sum types, polymorphism, classes and methods, etc. Part V, “Infinite Data Types” is of greater interest to me just because anything infinite seems to be of interest to me (and, more seriously, because one of the most significant issues I deal with in my work is mapping of algorithms conceptually defined over infinite structures into finite implementations).

Where things really get interesting for me is in Part XI, “Types as Propositions”. (I also love Harper’s distinction between constructive and classical logic as “logic as if people matter” versus “the logic of the mind of God”, and I wonder whether anyone has explored the connections between the constructive / classical logic dichotomy and the philosophical idealist / materialist one?) This left me wanting more, though, and in particular I am determined to get around to reading more about Martin-Löf type theory, which is not covered in this text.

Part XIV, Laziness, is also interesting for someone who has only played with laziness in the context of streams (in both Haskell and Scala, which take quite different philosophical approaches). Harper argues strongly in favour of allowing the programmer to make evaluation choices (lazy / strict, etc.).

Part XV, Parallelism, starts with the construction of a cost dynamics, which is fairly straight forward. The second chapter in this part looks at a concept called futures and their use in pipelining; while pipelining is my bread and butter in hardware design, the idea of a future was new to me. Part XVI, Concurrency, is also relevant to hardware design, of course. Chapter 43 makes an unexpected (for me!) link between the type system of a distributed concurrent language with modal logics, another area in which I am personally interested for epistemological reasons, but know little.

After discussing modularity, the book finishes off with a discussion of notions of equivalence.

I found this to be an enlightening read, and would recommend it to others with an interest in programming languages, an appetite for theoretical concerns, but a lack of exposure to the topics explored in programming language research.

2 thoughts on “Review: Practical Foundations for Programming Languages

  1. Very nice review! Indeed, Practical Foundations is a very good, down-to-earth yet not superficial book. And I guarantee you will find Martin-Lof type theory very exciting. I suggest a hands-on approach, e.g. follow an Agda tutorial.


    1. I’ve had a brief look at Agda in the past, but found limited support for newcomers. Is there a reason you’d choose Agda over Coq or Idris?


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s