A new chapter on type refinements has been added, complementing previous chapters on dynamic typing and on sub-typing.

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).

The parallel abstract machine was revised to correct an implied extension that would have been impossible to carry out.

Numerous corrections and improvements were made throughout, including memorable and pronounceable names for languages.

Exercises were added to the end of each chapter (but the last). Solutions are available separately.

The index was revised and expanded, and some conventions systematized.

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.

This entry was posted on Monday, April 11th, 2016 at 10:26 pm and is filed under Programming, Research, Teaching. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.

11 Responses to Practical Foundations for Programming Languages, Second Edition

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

and

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

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.

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
end
type key = KEY.t
type val
type t
val find, ins, del…
end

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
end
type t = …
type key = Key.t
type val = string
val find, ins, del…
end

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.

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.

“… 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!

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

and

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.

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

end

type key = KEY.t

type val

type t

val find, ins, del…

end

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

end

type t = …

type key = Key.t

type val = string

val find, ins, del…

end

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.

Exercises! Hurrah!

Does the online preview edition have these improvements?

Yes.

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.

I’ve yet to set up a book web site, working on it.

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

“… 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!