Jim Newton
3/16/2016 4:55:00 PM
Hi Kaz, thanks. My understanding is the same as yours. So certainly there is something wrong with my paraphrasing. I'll type in the paragraphs here from the book. But first a little background.
I don't know whether record types, or join/meet is "normal" terminology for functional language
or whether it is something this author made up.
<: (with the :) means is a subtype of
^ means meet
v means join
{x1:T1, x2:T2 ... xn:Tn} means a record type with fields x1, x2... xn whose types are T1, T2...Tn resp.
{} is the record type with no fields.
If A and B are record types, and if each field of B is also a field of A, then A <: B
(provided the field types match). Consequently every record type is a subtype of {}
Top is the type which is a super type of all types
There is no corresponding Bot type (for reasons I don't yet completely understand)
--- Text from Book ---
Definition: A type J is called a join of a pair of types S and T, written SvT = J,
if S <: J, T <: J, and, for all types U, if S <: U and T <: U, then J <: U.
Similarly, we say that a type M is a meet of S and T, written S^T=M, if M <: S,
M <: T, and, for all types L, if L <: S and L <: T, then L <: M.
Depending on how the subtype relation in a particular language with sub-
typing is defined, it may or may not be the case that every pair of types has a
join. A given subtype relation is said to have joins if, for every S and T, there
is some J that is join of S and T. Similarly, a subtype relation is said to have
meets if, for every S and T, there is some M that is a meet of S and T.
The subtype relation that we are considering in this section has joins, but
not meets. For example, the types {} and Top->Top do not have any common
subtypes at all, so they certainly have no greatest one. However, a slightly
weaker property does hold. A pair of types S and T is said to be bounded
below if there is some type L such that L <: S and L <: T. A given subtype
relation is said to have bounded meets if, for every S and T such that S and T
are bounded below, there is some M that is a meet of S and T.