CS611 Lecture 37 Subtype Polymorphism / Type Inclusion November 30, 2001Scribe: Michael Brukman and Jeff Hartline Lecturer: Andrew Myers1 IntroductionWe’d like to extend the traditional typed λ-calculus to include object oriented features, such as classes andclass inheritance. We will do this first by defining a structure type, and then a subtype property that canbe used to relate similar structures. The subtype idea extends beyond structures and we will see how it canbe applied to functions and pointers.2 Record TypesWe extend our typed language to included record types and operations:e ::= ... |{l1= e1,l2= e2,...,ln= en}|e.lτ ::= ... |{l1.τ1,l2.τ2,...,ln.τn}Also we add the following derivations:Γ  ei: τ∀i∈1..niΓ {l1= e1,...,ln= en} : {l1.τ1,...,ln.τn}Γ {l1= e1,...,ln= en} : {l1.τ1,...,ln.τn}Γ  e.li: τiNow we want to look at relationships between similar structure types. In some sense, languages like Cand Java only consider name equivalence and their subtyping relation correspondingly relies on explicitdeclarations: class Child extends Parent. We thus consider subclass declarations of these languages tobe assertions of structural conformance. For a compiler to allow the programmer to make such assertions,however, it needs a way to check that the subclass and superclass classes are indeed structurally compatible.Here’s how we define structural equivalence for our structure types.To do this, we introduce a new typing judgement:∆  τ1≤ τ2which means that, given context ∆ we conclude τ1is a subtype of τ2. We also need to specify how subtypingis used in the type checking derivation. Basically, the idea of a subtype is that when a subtype τ is desired,aparenttypeτ is acceptable. This concept is captured formally by the subsumption rule:Γ  e : τ  τ ≤ τ Γ  e : τ Here are some basic properties of the subtype relation: reflexivity and transitivity. Note that the subtyperelation is not necessarily antisymmetric.τ1≤ τ2 τ1≤ τ2 τ2≤ τ3 τ1≤ τ3For record types there are two natural subtype relationships: width subtyping and depth subtyping. Thesetwo derivation steps, in conjunction with reflexivity and transitivity, completely describe the subtype rela-tionship.m ≥ n{l1: τ1,...,lm: τm}≤{l1: τ1,...,ln: τn}τi≤ τ ∀i∈1..ni{l1: τ1,...,ln: τn}≤{l1: τ 1,...,ln: τ n}Observe that the subtyping property on structures is covariant with the structure components. That is, astructure S is a subtype of another structure S if the shared components of S are subtypes of the sharedcomponents of S .13 FunctionsThe rule in Eiffel with regard to method subtyping is not sound. It corresponds to the following subtypingrule on functions: τ1≤ τ 1 τ2≤ τ 2 τ1→ τ2≤ τ 1→ τ 2What we really want is for function subtyping to work as follows: τ 1≤ τ1 τ2≤ τ 2 τ1→ τ2≤ τ 1→ τ 2where the arguments are contravariant and the return type is covariant. The reason for this can be seen asfollows: let’s say we have a function f : τ → τ andwewishtobeabletouseafunctiong : σ → σ in itsplace. What should the restrictions be on types σ and σ if we are to claim that g ≤ f ?First, we should note that the function g should be able to take any types that f can, thus we must haveg’s argument types must be at least as general as f ’s are, ie. τ ≤ σ, so arguments are contravariant. Second,since anything that our function g returns must be acceptable in the context that f would have been used,the return value of g must be a subtype of the value that f would have returned, or σ ≤ τ , so return valuesare covariant.Given our type hierarchy, where Car ≤ Vehicle, we can construct function subtyping that is broken andwill result in a run-time error, but typechecks under Eiffel’s unsound inference rule:fun f (v: Vehicle) = v.wheels() (* f: Vehicle -> int *)fun g (c: Car) = c.passengers() (* g: Car -> int, so by Eiffel’s rule,g is a subtype of f *)let x = Vehicle(...) in(* this code is legal *)let y = f(x) in(* but we can use g in place of f!* this code typechecks because g is a subtype of f, and f can accept a* Vehicle, but g will call the passengers() function on x, which it* does not have. This results in a runtime error. *)g(x)This shows that, albeit counterintuitive at first, the function arguments do need to be contravariant,while return values are covariant, as expected.4PartialorderontypesSince any type is as good as unit, we can say that any type is a subtype of unit. Nontermination (whichwe can denote by 0) gives us less information than a terminating program of any type, and because anon-terminating program will never violate any type constraint – it will never terminate and hence can beassigned any type – we can say that 0 is a subtype of all other types: τ ≤ 1  0 ≤ τ5RefsWe can add refs to our language with the following type annotation:τ ::= ... | τ refand these inference rules:2Γ  e : τΓ  ref e : τ refΓ  e : τ refΓ  !e : τΓ  e1:τ ref Γ  e2: τΓ  e1:= e2:1How would we present subtyping on refs? Intuitively, it should be: τ ≤ τ  τ ref ≤ τ refBut this rule is not sound. Consider the following example, where Car and Truck are subtypes of Vehicle,but not related to each other:let x :Car ref = Car(...) inlet y :Vehicle ref = ref x in(y := ref Truck(...); (!x).passengers()meets with a problem: after assignment y := ref Truck(...) we now have both x and y pointing to a Truck.That may be fine for y which is a Vehicle, but not for x which is a Car,sox is acting like a Car with a Truckobject backing it, which is clearly an error. Hence, a typing rule on refs cannot be covariant.Clearly, the ref typing rule cannot be contravariant either, since that would mean that:Car ≤ Vehicle ⇒ Vehicle ref ≤ Car refwhich will break easily:let x: Vehicle ref = ref Vehicle(...) inlet y: Car ref = ref x in!y.passengers()Hence, subtyping on refsisinvariant, which for object oriented languages such as Java means thatinheriting classes cannot change the type of a mutable field variable, while they may change the types offunctions as we discussed above.It is interesting to note, however, that the original Java spec allowed to change the function return valuescovariantly, but this spec was never implemented in any officially released Java compiler from Sun. Ratherthan implement this useful