Suppose we have two (immutable)
record types,
and
, with
. In order for elements of
to
masquerade as elements of
, expressions of type
need to
support all of the operations applicable to expressions of type
.
The only operation available on a record is to extract a labeled
field. For
to masquerade as
,then, for each field
of
,
must also contain a field
. Moreover the type of that field must be a subtype of the
corresponding field in
, since if
then
must be usable in any context in which the same field selection of an
element of type
makes sense.
In Figure 1 we show a record
masquerading as
a record of type
.
Notice that the result of extracting the
field of
must be
able to be treated as being of type
.Notice also that type
may have more
labeled fields than
(since the extra fields don't get in the way of
any of the operations applicable to
).
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:
For example, if , then