16.3 Joins and Meets

< Free Open Study >

Typechecking expressions with multiple result branches, such as conditionals or case expressions, in a language with subtyping requires some additional machinery. For example, recall the declarative typing rule for conditionals.

The rule requires that the types of the two branches be the same, and assigns this type to the whole conditional. But in the presence of subsumption, there may be many ways of giving the two branches the same type. For example,

   if true then {x=true,y=false} else {x=false,z=true};

has type {x:Bool}, since the then part has minimal type {x:Bool,y:Bool}, which can be promoted to {x:Bool} using T-SUB, and similarly the else part has minimal type {x:Bool,z:Bool}, which can also be promoted to {x:Bool}. The same term also has types {x:Top} and {}-in fact, any type that is a supertype of both {x:Bool,y:Bool} and {x:Bool,z:Bool}. The minimal type for the whole conditional is therefore the least type that is a supertype of both {x:Bool,y:Bool} and {x:Bool,z:Bool}-i.e., {x:Bool}. In general, to calculate the minimal type of an arbitrary conditional expression, we need to calculate the minimal types of its then and else branches and then calculate the least common supertype of these. This type is often called the join of the types of the branches, since it corresponds to the usual join of two elements of a partial order.

16.3.1 Definition

A type J is called a join of a pair of types S and T, written S V T = J, if S <: J, T <: J, and, for all types U, if S <: U and T <: U, then J <: U. Similarly, we say that a type M is a meet of S and T, written S ∧ T = M, if M <: S, M <: T, and, for all types L, if L <: S and L <: T, then L <: M.

Depending on how the subtype relation in a particular language with subtyping is defined, it may or may not be the case that every pair of types has a join. A given subtype relation is said to have joins if, for every S and T, there is some J that is a join of S and T. Similarly, a subtype relation is said to have meets if, for every S and T, there is some M that is a meet of S and T.

The subtype relation that we are considering in this section^[2] has joins, but not meets. For example, the types {} and Top→Top do not have any common subtypes at all, so they certainly have no greatest one. However, a slightly weaker property does hold. A pair of types S and T is said to be bounded below if there is some type L such that L <: S and L <: T. A given subtype relation is said to have bounded meets if, for every S and T such that S and T are bounded below, there is some M that is a meet of S and T.

Joins and meets need not be unique. For example, {x:Top,y:Top} and {y:Top,x:Top} are both joins of the pair of types {x:Top,y:Top,z:Top} and {x:Top,y:Top,w:Top}. However, two different joins (or meets) of the same pair of types must each be a subtype of the other.

16.3.2 Proposition [Existence of Joins and Bounded Meets]

For every pair of types S and T, there is some type J such that S V T = J.
For every pair of types S and T with a common subtype, there is some type M such that S ∧ T = M.

Proof: EXERCISE [RECOMMENDED, ⋆⋆⋆].

Using the join operation we can now give an algorithmic rule for the if construct in the presence of subtyping.

16.3.3 Exercise [⋆⋆]

What is the minimal type of if true then false else {}? Is this what we want?

16.3.4 Exercise [⋆⋆⋆]

Is it easy to extend the algorithms for calculating joins and meets to an imperative language with references, as described in §15-5? What about the treatment of references in §15.5, where we refine the invariant Ref with covariant Source and contravariant Sink?

^[2]That is, the relation defined in Figures 15-1 and 15-3, extended with the type Bool. The subtyping behavior of Bool is simple: no rules for it are added to the declarative subtype relation, so its only supertype is Top.

< Free Open Study >