## Subtyping

• While languages like Java and C# have generics these days, the source of type-system expressiveness most fundamental to object-oriented style is subtype polymorphism, also known as subtyping.

We need a type system, with a form of types for records and typing rules for each of our expressions.

• If e1 has type t1, e2 has type t2, ..., en has type tn, then {f1=e1, f2=e2, ..., fn=en} has type {f1:t1, f2:t2, ..., fn:tn}.
• If e has a record type containing f : t, then e.f has type t (else e.f does not type-check).
• If e1 has a record type containing f : t and e2 has type t,then e1.f = e2 has type t (else e1.f = e2 does not type-check).
• “Width” subtyping: A supertype can have a subset of fields with the same types, i.e., a subtype can have "extra" fields
• “Permutation” subtyping: A supertype can have the same set of fields with the same types in a different order.
• Transitivity: If t1 <: t2 and t2 <: t3, then t1 <: t3.
• Reflexivity: Every type is a subtype of itself: t <: t.