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:
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.
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:
MODE N = UNION(INT, REAL); 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.