Record types

The type of a record includes both the labels and types of each field. Thus a record with labels ${\it {l_i}}$ of type ${\it {T_i}}$ for $1 \le i \le n$ has a type which can be written in the form ${\it {\{l_i:T_i\}_{1 \le i \le n}}}$.For example, the record ${\it {\{name = ``jane'',age = 12\}}}$ has type ${\it {\{name: String; age: Integer \}}}$.

Suppose we have two (immutable) record types, ${\it {R'}}$ and ${\it {R}}$, with ${\it {R' {\rm \ <: \ }R}}$. In order for elements of ${\it {R'}}$ to masquerade as elements of ${\it {R}}$, expressions of type ${\it {R'}}$ need to support all of the operations applicable to expressions of type ${\it {R}}$.

The only operation available on a record is to extract a labeled field. For ${\it {R'}}$ to masquerade as ${\it {R}}$,then, for each field ${\it {l}}$ of ${\it {R}}$, ${\it {R'}}$ must also contain a field ${\it {l}}$. Moreover the type of that field must be a subtype of the corresponding field in ${\it {R}}$, since if ${\it {r':\ R'}}$ then ${\it {r'.l}}$must be usable in any context in which the same field selection of an element of type ${\it {R}}$ makes sense. In Figure 1 we show a record ${\it {r':\ \{l_1:T'_1;l_2:T'_2;l_3:T'_3;l_4:T'_4\}}}$ masquerading as a record of type ${\it {\{l_1:T_1;l_2:T_2;l_3:T_3\}}}$. Notice that the result of extracting the ${\it {l_i}}$ field of ${\it {r'}}$ must be able to be treated as being of type ${\it {T_i}}$.Notice also that type ${\it {R'}}$ may have more labeled fields than ${\it {R}}$ (since the extra fields don't get in the way of any of the operations applicable to ${\it {R}}$).

  

Figure 1: A record ${\it {r:\ \{l_1:T_1;l_2:T_2;l_3:T_3\}}}$, and ${\it {r':\ \{l_1:T'_1;l_2:T'_2;l_3:T'_3;l_4:T'_4\}}}$ masquerading as an element of type ${\it {\{l_1:T_1;l_2:T_2;l_3:T_3\}}}$.

Thus a subtype of a record may have labeled fields whose types are a subtype of the original, and may also have more fields than the original record type. We write this formally as follows:

$$\{ {\rm{\it { l_j:T_j'}}}\}_{1 \le j \le n} {\rm \ <: \ }\{ ... ... \le i \le k, {\rm{\it {T_i'}}} {\rm \ <: \ } {\rm{\it {T_i}}}.$$

For example, if ${\it {TropicalFruit {\rm \ <: \ }Fruit}}$, then

$${\rm{\it {\{main: MainDish; dessert: TropicalFruit; drink: Beverage\} {\rm \ <: \ } \{main: MainDish; dessert: Fruit\}}}}.$$