Practical Foundations for Programming Languages, Second Edition

Today I received my copies of Practical Foundations for Programming Languages, Second Edition on Cambridge University Press.  The new edition represents a substantial revision and expansion of the first edition, including these:

  1. A new chapter on type refinements has been added, complementing previous chapters on dynamic typing and on sub-typing.
  2. Two old chapters were removed (general pattern matching, polarization), and several chapters were very substantially rewritten (higher kinds, inductive and co-inductive types, concurrent and distributed Algol).
  3. The parallel abstract machine was revised to correct an implied extension that would have been impossible to carry out.
  4. Numerous corrections and improvements were made throughout, including memorable and pronounceable names for languages.
  5. Exercises were added to the end of each chapter (but the last).  Solutions are available separately.
  6. The index was revised and expanded, and some conventions systematized.
  7. An inexcusably missing easter egg was inserted.

I am grateful to many people for their careful reading of the text and their suggestions for correction and improvement.

In writing this book I have attempted to organize a large body of material on programming language concepts, all presented in the unifying framework of type systems and structural operational semantics.  My goal is to give precise definitions that provide a clear basis for discussion and a foundation for both analysis and implementation.  The field needs such a foundation, and I hope to have helped provide one.



11 Responses to Practical Foundations for Programming Languages, Second Edition

  1. stephenbly says:

    Hi Professor Harper. I’ve read all of *Practical Foundations for Programming Languages* and it was eye-opening to say the least. I have a question on modules, which I’ve found to be the most difficult section of the text (I guess that’s why it’s last!). I have two questions:

    I’m having trouble figuring out a concrete example of module hierarchies in the chapter *Hierarchy and Parameterization*. Parameterization corresponds to functors in SML and OCaml (which I have been using to ground the concepts presented in the text), but it doesn’t seem like either of these languages have module hierarchies as defined. Is that true, or am I missing something obvious?

    Second, I don’t understand why binding a sealed module to a variable allows us to safely access its static part. What is the conceptual different between

    (struct type t = int val zero: t = 0 end : sig type t val zero: t end).t


    let val M = struct (struct type t = int val zero: t = 0 end : sig type t val zero: t end) in M.t

    Are modules variables “special” in some way?

    • Thanks, I am glad you benefited from reading it.

      Both SML and OCaml have module hierarchies, under the terminology “substructures”. eg, when I have a substructure for keys in a dictionary. Think of that as Sigma k::KEY.DICT(k), for example.

      Your example is a kind of corner case because the structure is, in fact, a value. In general evaluation of a structure expression can have an effect, and we wish to distinguish two abstract types that are observably different. The conservative thing to do is insist that such types always be distinct, even when we can see in particular cases that they are in fact indistinguishable. This leads to a simple, practical module system without the complications that would be required to do a better job in certain circumstances. OCaml tries to do better (“applicative functors”), but the costs outweigh the benefits, especially for expository purposes in PFPL.

    • stephenbly says:

      OK. I think I’m confused because OCaml also has an `include` keyword. I’m not sure if that fits into the theory you laid out, or if it offers orthogonal functionality.

      From what you said, here is what I believe is a layered signature:

      signature DICT = sig
      signature KEY =
      type t
      val leq: t * t -> bool
      type key = KEY.t
      type val
      type t
      val find, ins, del…

      And then a module implementing the signature could be created as:

      structure Dict: DICT = struct
      structure Key: DICT.KEY =
      type t = int
      val leq a b = a < b
      type t = …
      type key = Key.t
      type val = string
      val find, ins, del…

      Is that correct?

      From what I've seen, it's more common to create DICT as a module *parameterized* by a module of signature KEY, instead of containing a submodule of signature KEY.

    • One of the most important lessons of the ML module system is that parameterization in the sense you suggest does not work in practice. Instead, hierarchical structures tied together by sharing equations is much more convenient.

  2. Nick Barnes says:

    Does the online preview edition have these improvements?

  3. This looks great, I’ll definitely get it. One question: You mention that the solutions to the exercises are available separately but I can’t find anything. It would be great if you could provide a link as I find solutions quite helpful for self study.

  4. Congratulations on the release of the book! Just ordered mine.

  5. Todd Wilson says:

    “… precise definitions that provide a clear basis for discussion and a foundation for both analysis and implementation. The field needs such a foundation, and I hope to have helped provide one.”

    This is a modest understatement of the great value of this book to both students and experts alike. The unified approach developed here not only allows an efficient and comprehensive treatment of many (seemingly) disparate systems, but also makes clear many of the more subtle and complex issues that often go under-appreciated in alternative accounts. It is truly a democratizing and empowering resource, whose importance is most evident when using it in the classroom as the basis of a course and watching students develop from it a rich understanding of the field.

    The changes in the second edition are most welcome, especially the exercises; thanks for the effort you’ve put into both editions!

Leave a Reply

Please log in using one of these methods to post your comment: Logo

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

Twitter picture

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

Facebook photo

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

Google+ photo

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

Connecting to %s

%d bloggers like this: