Cardelli identifies

- objects as records with possibly functional components
- objects as functions that receive a stream of messages and which dispatch on the message to select the appropriate method

A record is a finite association of values to labels, for example

There is a subtype relation on record types, corresponding to the subclass relation in Simula or Smalltalk. A record type T is a subtype of another record type T' (written T <= T') if T has all of the fields of T', and possibly more, and each field of T' has a like-named field in T that is a subtype of it.

Note that for any type T, T<=T, and in particular, int<=int, etc, for all of the basic types.

If a has type T and T<=T', then a also has type T'. For example,

Records can have functions as components; we can use this to model methods. The rule for subtyping among functional types is:

There is a notation for defining a subtype of a record type:

Or we can mask off fields:

We can also have variant types:

We can model private variables (or private functions) using lexical scoping:

The semantics of expressions is given in a domain V of values. V contains all possible values, and is the coalesced sum of the domains of basic values, functions, records, variants, and two special values: bottom and wrong. Bottom is used to model runtime exceptions, such as divide-by-zero or a non-terminating computation. Wrong is used to model type errors.

A "coalesced sum" means that the values in V are "labelled" by the domain from which the value came. This could be modelled, for example, by having V consist of tuples of (domain_name,domain_value).

The idea is that we will define some type rules, which can be checked at compile time. These will guarantee that we will never compute the value 'wrong' at run time.

A type is just a subset of V. (Not every possible subset is a type -- the
subsets must obey certain technical properties. Those subsets are called
*ideals*. (The precise definition of 'ideal' is beyond the scope of
the instructor.) However, all types found in programming languages are
ideals, so this restriction won't get in our way.

The *environment* is a function from identifiers to values.
The semantics of expressions is defined using a *semantic function*
E, which maps expressions to functions from environments to values.
(This should be a script E but I can't get html to do this.)

For example, consider the equation for the meaning of identifiers:

This says that the meaning of an identifier x is simply the result of looking up that identifier in the environment v.

There are also equations that give the meaning of type expressions (page 11). The type inference rules (page 12) let us deduce the types of expressions, given information about e.g. the types of their constituent parts.

There is a typechecking function T, which maps expressions into functions from type environments to type expressions:

The bottom line is the corollary on page 15: