Types and Programming Languages, by Benjamin Pierce

This is a highly technical book which has the combined styles of a math book and a book on software. There are theorems and proofs. There are many references to works from the 20’s thru the 50’s that were pure mathematics and were seen by few then as relevant to computers which were then somewhat over the horizon. The book has interesting perspectives on commercial computer languages such as Java, C and C++. The book even descends to issues of producing machine language for certain constructs.

The pedagogical plan is for the reader to bring at least an informal understanding of OCaml and to develop a formal understanding of OCaml and several possible extensions thereof.

I find a fair amount of information that is new to me. The book pays close attention to what can be built upon what. I was startled to see that cons, car and cdr can be built from pure lambda. I was amused that conflating true with 1 has roots far older than C.

The following is tentative. I have thought of types as sets of values. A particular formal system would first define values (with an eye towards organizing them into types of course) and then the types. This subtle distinction emerges, I think, in Pierce’s treatment of subtyping. We agree that until subtyping, a value is of exactly one type. (Algol 68 sticks to this and introduces unions which are sets of types. A union is not a type but a mood and variables, fields and parameters can be declared as such.) Pierce says that a language might make the type int a subtype of float. In this case it is not clear to me whether he intends that there remain distinct values 1 and 1.0. Mathematicians are themselves vague and often inconsistent on this point within a short span in a book. [He seems to limit this to values whose machine representations are naturally substitutable.] I grant that this is the important case but in theory subtyping should allow other ‘embeddings’ of one type within another. His motivating example is that a record with field names and corresponding field types should be welcome anywhere that a record with a subset of those names and types is used. In this case the embedding is natural and should be honored. The machine representation may be impacted by this strategy however. The case of embedding integer values within floating point seems different to me somehow. I am not convinced we can limit ourselves to cases where the embedding is ‘natural’.

The integers as a subset of reals (with types as value sets) is an example of a type being a subset as well as a subtype. Types {x: Nat; y: float; ...} as a subtypes of {x: Nat} is an example of a vastly larger sets of values composing a suptypes. Such subtypes seem much different and certainly confusing. The book is sporadically concerned with implementation issues. One use of subtyping is to enable the scenario where:

The goal is that neither producers of subtype values, nor consumers of the supertype values, need pay extra for correct and safe function. It may be possible for the platform (language system) to find a place to put code that transforms any such values after production and before consumption, and that this code need not necessarily run as often as either the producer or consumer. Consider, for instance, a call site that passes an integer value to a routine value that takes a float. The call site can include conversion code. Another way to achieve this efficiency is to find a form of expressing these values so that the transformation is vacuous. This latter is achieved with the vtables of C++ but only by imposing limitations on subtyping. These rules allow the representation of subtypes (a block with a pointer to a vtable) to be interchangeable with representations of the supertype. This is so because the vtable format for the subtype includes the vtable format for the supertype as an initial portion. (Java relaxes these limitations and pays a call cost with their Interface mechanism.) I find this an annoying, yet very useful hack due to its efficiency. I have not understood multiple inheritance in this context but I suppose it is not obviously impossible.

There are many ramifications of subtyping, dependent compilation and independent compilation that escape me. Is the notion of subtyping more or less than C’s conventional notion of coercion of arguments to a subroutine?

Things get clearer to me if we posit that the language designer, not the programmer, determines the subtype relationships. That ints can be used in strong floating contexts (as in C) is an inflexible language feature. This perspective suggests that a Java compiler could produce code to dynamically create a new v-table at a call site where the argument type was a sub-type of the parameter type by virtue of an Interface. This might be faster than the current practice which, I think, is to search on each call and perhaps cache the search result.

I am unconvinced of the utility of the mathematical theory of types. Occasionally Pierce will rephrase some one of his many formulae in plain English and a collection of such sentences would be a valuable addition to the missing OCaml language definition.
Page 53: “Abstract syntax is a much simpler internal representation of programs as labeled trees (called abstract syntax trees or ASTs). The tree representation renders the structure of the terms immediately obvious, making it a natural fit for the complex manipulations involved in both rigorous language definitions (and proofs about them) and the internals of compilers and interpreters.” I agree, but in the quest for simplicity objectively defined, I must recall the 1401 Fortran compiler where linked lists were not used and routines in the compiler comprised about 6000 instructions. For several reasons linked lists or trees were not available as technologies. The first compilers, some of which were simple, predated either the stack or the linked list. These compilers were also confined by the nature of memory technology available then. Several compilers ran in machines where the source code would not fit in RAM at once. The nature of caches today and the foreseeable future suggest that some of these patterns would be necessary should the need arise for processing programs (such as compiling) much more efficiently than we do today. This is not a current problem I believe.

Page 121: “There are a number of situations where ascription can be useful in programming. One common one is documentation. It can sometimes become difficult for a reader to keep track of the types of the subexpressions of a large compound expression. Judicious use of ascription can make such programs much easier to follow.”
There is another point here. There is a covenant between the compiler and the reader that the compiler agrees with the claim. The ascription does not modify the meaning of the code. In this context it is clear that ascription is a compile time check. I think that the OCaml manual is unclear on this.

Page 191: I find Pierce’s reasons to avoid including the type Bot a bit vague. I agree that it is not much needed and it is empty; there are no values of that type, which he notes. I suppose that the type expression “bot ref” would be awkward. I am a bit surprised that the book takes expressions in the language as the most fundament value to reason about. Some values, such as the fix operator have not denotation in the languages that he studies, except as an identifier defined in some invisible primal environ.

Page 207: Pierce says that languages with union types lack case statements. Algol 68 has the construct:

N t = 6;
print(CASE t IN (INT i): i+1, (REAL x): x-1.0 ESAC)
which yields “+7”.

Book’s site
At the beginning of each chapter there is a footnote with a name of one of these folders where the collected sources for the chapter may be found. Note related *.tar.gz files towards the bottom. In each expanded folder it suffices to type “make” and then “./f test.f” to run the code.
Some code from the book


I wish that Pierce had mentioned the notion that references might be more orthogonal. Algol 68 arrays (called ‘row’s) are primitively immutable like other types. As in OCaml a value of type REF ROW is a mutable array Ditto structures. This cost some complex theoretical shenanigans to explain what ordinary programmers had been doing with real mutable arrays for years. Immutable arrays are useful in Algol 68. I also wish that the notion of a sub-type of reference that supported dereferencing but not assignment had been mentioned. He hints at this as he mentions the language Forsyth on page 199. ------- P 207