The Coherence of Languages with Intersection Types

John C. Reynolds^{∗} School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213-3890, USA

                 john.reynolds@cs.cmu.edu

Abstract

When a programming language has a sufficiently rich type structure, there can be more than one proof of the same typing judgement; potentially this can lead to semantic ambiguity since the semantics of a typed language is a function of such proofs. When no such ambiguity arises, we say that the language is coherent. In this paper we prove the coherence of a class of lambda-calculus-based languages that use the intersection type discipline, including both a purely functional programming language and the Algol-like programming language Forsythe.

1 Introduction

As the type structure of programming languages has become richer, the problem of avoiding semantic ambiguity has become more difficult. In [5], this problem was resolved for first-order languages with implicit conversions (i.e. subtypes) and generic operators. In the present paper, we consider the more general case of higher-order languages with implicit conversions and intersection types [2]. For such languages, we will find that the usual kind of semantic equations give meaning, not to phrases of the language itself, but rather to proofs of typing judgements about such phrases. Thus to insure against semantic ambiguity, we must prove that distinct proofs of the same typing judgement possess the same meaning. Following [1] (which treats a closely related problem for a language with implicit conversions and polymorphism), we call this property coherence.

∗This research was sponsored in part by National Science Foundation Grant CCR-8922109 and in part by the Avionics Lab, Wright Research and Development Center, Aeronautical Systems Division (AFSC), U.S. Air Force, Wright-Patterson AFB, OH 45433-6543 under Contract F33615-90-C-1465, Arpa Order No. 7597. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. Government.

The kind of language for which we will prove coherence is a lambda calculus extended to include object manipulation, fixed points, and conditionals. More precisely, our results hold for a class of such languages obtained by varying such entities as primitive types, constants, and semantic categories, subject to appropriate constraints.

Two particular cases of importance are a purely functional language (albeit without recursively defined types), and a syntactically desugared version of the Algol-like language Forsythe [7]. Certain aspects of the general treatment, notably the inclusion of operations for object construction, field selection, merging, and conditional branching, are specifically motivated by the desire to encompass Forsythe.

Our results depend upon some basic properties of intersection types (also called conjunctive types) that are proved in [6] and summarized in the following section.

2 Types and Their Semantics

We consider the set of types defined by the abstract grammar

θ ::= ρ | θ → θ | ι: θ | ns | θ & θ

where the metavariable ι ranges over identifiers, and the metavariable ρ ranges over primitive types. Here → is the usual operator for constructing types of procedures (or, in an applicative language, functions), & is the binary intersection operator, and ns (called ω in [2]) denotes the intersection of zero types. The construction ι: θ is meant to denote a type that is isomorphic to θ, but (in an intuitive sense) disjoint from θ. (In programming terminology, one can regard ι: θ as the type of objects or records with a single field named ι ranging over the type θ.)

We write θ ≤ θ′ to indicate that θ is a subtype of θ′. The subtype relation ≤ is the least preorder on the set of types such that

θ ≤ ns  θ_{1} & θ_{2} ≤ θ_{1}  θ_{1} & θ_{2} ≤ θ_{2}
If θ ≤ θ_{1} and θ ≤ θ_{2} then θ ≤ θ_{1} & θ_{2} .
If ρ ≤_{prim} ρ′ then ρ ≤ ρ′ . If θ ≤ θ′ then ι: θ ≤ ι: θ′ .
If θ′_{1} ≤ θ_{1} and θ_{2} ≤ θ′_{2} then θ_{1} → θ_{2} ≤ θ′_{1} → θ′_{2} .
ι: θ_{1} & ι: θ_{2} ≤ ι: (θ_{1} & θ_{2})
(θ → θ_{1}) & (θ → θ_{2}) ≤ θ → (θ_{1} & θ_{2})
ns ≤ ι: ns ns ≤ θ → ns

where ≤_{prim} is a given subtype preorder for primitive types. We write θ ≃ θ′ when θ and θ′ are equivalent, i.e. when θ ≤ θ′ and θ′ ≤ θ.

The first four of the above relationships establish that ns is a greatest type and that θ_{1} & θ_{2} is a greatest lower bound of θ_{1} and θ_{2}. Note that we say “a” rather than “the”; since we have a preorder rather than a partial order, greatest types and greatest lower bounds are unique only to within equivalence.

The specific choice of the primitive types and their subtype relation is not relevant to the coherence property. However, we will impose two requirements: First, the preordered set of primitive types must be pairwise bounded complete, i.e. every pair of primitive types with an upper bound must have a least upper bound. Second (so that we can introduce conditionals), there must be a particular primitive type bool.

Under the first of these assumptions, it is shown in [6] that

Proposition 1 If θ_{1} & θ_{2} ≤ θ′ then there are θ′_{1} and θ′_{2} such that θ_{1} ≤ θ′_{1}, θ_{2} ≤ θ′_{2}, and θ′ ≃ θ′_{1} & θ′_{2}.

Proposition 2 Every pair of types has a least upper bound. In particular, there is a function ⊔ mapping pairs of types into types such that θ_{1} ⊔ θ_{2} is a least upper bound of θ_{1} and θ_{2}, and

θ ⊔ ns ≃ ns
θ_{1} ⊔ (θ_{2} & θ_{3}) ≃ (θ_{1} ⊔ θ_{2}) & (θ_{1} ⊔ θ_{3})
ρ ⊔ ι: θ ≃ ns
ρ ⊔ (θ_{1} → θ_{2}) ≃ ns
ι: θ_{1} ⊔ (θ_{2} → θ_{3}) ≃ ns
ρ_{1} ⊔ ρ_{2} ≃ ρ_{1} ⊔_{prim} ρ_{2} when ρ_{1} ⊔_{prim} ρ_{2} exists
ρ_{1} ⊔ ρ_{2} ≃ ns when ρ_{1} ⊔_{prim} ρ_{2} does not exist
ι: θ_{1} ⊔ ι: θ_{2} ≃ ι: (θ_{1} ⊔ θ_{2})
ι_{1}: θ_{1} ⊔ ι_{2}: θ_{2} ≃ ns when ι_{1} ≠ ι_{2}
(θ_{1} → θ′_{1}) ⊔ (θ_{2} → θ′_{2}) ≃ (θ_{1} & θ_{2}) → (θ′_{1} ⊔ θ′_{2}) .

(As with greatest lower bounds, least upper bounds are unique only to within an equivalence. Note, by the way, that the function ⊔, unlike &, is not a type constructor.)

In proving coherence, we will assume that the semantics of our language is based upon a category K with the following properties:

1. The category K is Cartesian closed.

2. There is a subcategory S of K such that every finite diagram in S has a limit in S that is also a limit in K. (In particular, we assume that S and K have the same distinguished product.)

3. There is a functor ⟹_{S} from S^{op}×S to S that is a restriction of the exponentiation functor ⟹_{K} from K^{op} × K to K. (This does not imply that S is Cartesian closed, since it need not contain application and abstraction morphisms.) For each object k of S, the functor k ⟹_{S} − preserves limits in S.

4. There is a functor [[−]]_{prim} from the preordered set of primitive types (viewed as a category) to S that assigns meanings to the primitive types ρ and implicit conversions to the morphisms ρ ≤_{prim} ρ′ of the primitive subtype relation.

For a purely functional language, for example, K is the category CPO whose objects are complete partial orders with least elements and whose morphisms are continuous functions, and S is the subcategory whose morphisms are strict. For Forsythe, on the other hand, both K and S are subcategories of the functor category CPO^{Σ} used by F. Oles to describe the semantics of Algol-like languages [3, 4]. Specifically, K is the full subcategory whose objects are functors that map morphisms into strict functions, S is the further subcategory whose morphisms are natural transformations that map objects into strict functions, and Σ is an appropriate category of “store shapes”.

In [6], it is shown from the above general properties of K that one can define a semantic functor [[−]] characterized as follows:

Proposition 3 There is a “semantic” functor [[−]] from the preordered set of types (viewed as a category) to S that satisfies

1. [[−]] is an extension of [[−]]_{prim}.

2. [[θ_{1} → θ_{2}]] = [[θ_{1}]] ⟹_{S} [[θ_{2}]] and [[θ_{1} → θ_{2} ≤ θ′_{1} → θ′_{2}]] = [[θ′_{1} ≤ θ_{1}]] ⟹_{S} [[θ_{2} ≤ θ′_{2}]].

3. [[ι: θ]] = [[θ]] and [[ι: θ ≤ ι: θ′]] = [[θ ≤ θ′]].

4. [[ns]] is a terminal object.

5. [[θ_{1} & θ_{2}]], along with the implicit conversions [[θ_{1} & θ_{2} ≤ θ_{1}]] and [[θ_{1} & θ_{2} ≤ θ_{2}]], is a pullback of [[θ_{1}]], [[θ_{2}]], and [[θ_{1} ⊔ θ_{2}]]:

[figure: [[θ_{1} & θ_{2}]]; [[θ_{1}]]; [[θ_{2}]]; [[θ_{1} ⊔ θ_{2}]]]

(As illustrated by this diagram, we adopt the convention that an unlabeled arrow from [[θ]] to [[θ′]] denotes the implicit conversion [[θ ≤ θ′]]. Later, we will also use this convention for products of implicit conversions.)

Actually, the functor constructed in [6] only gives isomorphisms, such as [[θ_{1} → θ_{2}]] ≃ [[θ_{1}]] ⟹_{S} [[θ_{2}]] and [[ι: θ]] ≃ [[θ]]. Without any loss of generality, however, we can make the present exposition far more concise by assuming that these isomorphisms are equalities.

Notice that, because of the last part of the above proposition, the semantics of types is not compositional in the conventional sense, since the meaning [[θ_{1} & θ_{2}]] of θ_{1} & θ_{2} depends, not only upon the meanings of θ_{1} and θ_{2}, but also upon the meaning of θ_{1}⊔θ_{2} and the implicit conversions among these meanings.

A type assignment π is a mapping from a finite set of identifiers into types; the appropriate preordering is that π ≤ π′ whenever dom π′ ⊆ dom π and, for all ι ^{∈} dom π′, πι ≤ π′ι. We write [[−]]^{∗} for the functor from the preordered set of type assignments (viewed as a category) to S, such that

[[π]]^{∗} =^{def} \begin{matrix}∏ & S \\ ι^{∈}dom π \end{matrix}[[πι]] ,

and [[π ≤ π′]]^{∗} is the unique morphism making the diagram

[figure: \begin{matrix}∏ & S \\ ι^{∈}dom π \end{matrix}[[πι]]; \begin{matrix}∏ & S \\ ι^{∈}dom π′ \end{matrix}[[π′ι]]; [[πι]]; [[π′ι]]; [[π ≤ π′]]^{∗}; p; p′]

(where p and p′ denote projection morphisms) commute in S for every ι ^{∈} dom π′.

3 Phrases and their Semantics

We write π ⊢ p : θ for the judgement that a phrase p has type θ under the type assignment π, and P_{πθ} for the set of phrases p for which π ⊢ p : θ is a valid typing judgement. The valid typing judgements of our language are those that are provable from a certain set of inference rules. At the outset, it is important to note that some of these rules, such as the rule for subtypes:

\frac{π ⊢ p : θ_{1}}{π ⊢ p : θ} when θ_{1} ≤ θ

are not syntax-directed, since they allow one to infer a judgement about a phrase from a previous judgement about the same phrase.

The semantics of phrases (or more precisely of typing judgements, since a phrase satisfying several judgements will have several meanings) is given by a family of semantic functions

μ_{πθ} ^{∈} P_{πθ} → ([[π]]^{∗} ⟶_{K} [[θ]]) .

Conventionally, one would expect to define these functions by a collection of semantic equations, one for each “reason” that a phrase belongs to one of the P_{πθ}, i.e. for each inference rule. But as soon as one tries to write a semantic equation for a non-syntax-directed rule, such as the intuitively obvious rule

μ_{πθ}[ p] = μ_{πθ_{1}}[ p] ; [[θ_{1} ≤ θ]] when π ⊢ p : θ_{1} and θ_{1} ≤ θ

for subtypes, it becomes clear that something is awry: Since conventional semantic equations are cases of a definition by induction on the size of phrases, they should not define the meaning of a phrase in terms of another meaning of the same phrase. (Note, by the way, that we use a semicolon to denote composition in diagrammatic order.)

In fact, instead of defining the meaning of phrases, the semantic equations for our language define the meaning of proofs that such phrases satisfy typing judgements. They actually define a function μ (distinguished from μ_{πθ} by the absence of subscripts) that maps each proof P of a judgement π ⊢ p : θ into a morphism in [[π]]^{∗} ⟶_{K} [[θ]]. The definition is by induction on the size of the proof, with a case analysis on the rule used at the main step of the proof.

For each inference rule

\frac{J_{1} J_{2} … J_{n}}{J}

the corresponding semantic equation gives the meaning of the proofs that use the rule at their main step, as a function of the meanings of the subproofs of the judgements that are premisses of the rule. In stating the semantic equation, we will write P for the proof of J whose meaning is being defined and P_{i} for the subproof of the premiss J_{i}. For example, the semantic equation for the subtype rule is

μ[P] = μ[P_{1}] ; [[θ_{1} ≤ θ]] .

The property of coherence bridges the gap between the function μ that is actually defined by the semantic equations and the functions μ_{πθ} that give meanings to typing judgements independently of their proofs. We say that μ is coherent iff μ[P_{1}] = μ[P_{2}] whenever P_{1} and P_{2} both prove the same typing judgement. This is exactly the property needed to make the obvious definition

μ_{πθ}[ p] =^{def} μ[P] for any P proving π ⊢ p : θ

unambiguous.

4 Inference Rules and Semantic Equations

In this section we give the inference rules and semantic equations for the class of languages for which we will prove coherence. The first three of these rules are the only ones that are not syntax-directed.

• Subtypes

\frac{π ⊢ p : θ_{1}}{π ⊢ p : θ} when θ_{1} ≤ θ μ[P] = μ[P_{1}] ; [[θ_{1} ≤ θ]] .

• Nonsense

\overline{π ⊢ p : ns} μ[P] = u_{π} ,

where u_{π} is the unique morphism from [[π]]^{∗} to the terminal element [[ns]].

• Intersections

\frac{π ⊢ p : θ_{1} π ⊢ p : θ_{2}}{π ⊢ p : θ_{1} & θ_{2}} μ[P] = β ,

where β is the unique mediating morphism into the pullback:

[figure: [[π]]^{∗}; [[θ_{1} & θ_{2}]]; [[θ_{1}]]; [[θ_{2}]]; [[θ_{1} ⊔ θ_{2}]]; μ[P_{1}]; β; μ[P_{2}]]

This semantic equation only makes sense if the perimeter of the above diagram commutes. In the next section, as part of the proof of coherence, we will establish that this condition is always met.

• Identifiers

\overline{π ⊢ ι : π(ι)} when ι ^{∈} dom π μ[P] = p ,

where p is the projection morphism from [[π]]^{∗} = \begin{matrix}∏ & S \\ ι^{∈}dom π \end{matrix}[[πι]] to [[πι]].

• Constants

\overline{π ⊢ c : θ_{c}} μ[P] = u_{π} ; μ_{c} .

Here θ_{c} is the type of the constant c, μ_{c} is its meaning, which must be a morphism from the terminal element [[ns]] to [[θ_{c}]], and u_{π} is the unique morphism from [[π]]^{∗} to the terminal element.

We will not specify any particular constants. It should be noted, however, that when θ_{c} is an intersection of procedural types, e.g. (θ_{1} → θ′_{1}) & (θ_{2} → θ′_{2}), the requirement that μ_{c} must be a morphism from [[ns]] to [[θ_{c}]] is a nontrivial constraint that has the same effect as the naturality constraints on generic operators in [5].

The semantics of the next two rules relies upon the Cartesian closed nature of K. For all objects B and C there is an exponentiation object B ⇒ C and an application morphism ap ^{∈} (B ⇒ C) × B → C such that, for all objects A and morphisms ρ ^{∈} A × B → C, there is exactly one abstraction morphism ab ρ ^{∈} A → (B ⇒ C) making

[figure: A × B; (B ⇒ C) × B; C; ρ; ap; ab ρ × I_{B}]

commute in K. Moreover, the exponentiation operator ⇒ extends to a functor from K^{op} × K to K with the following action on morphisms: if ϕ ^{∈} B′ → B and ψ ^{∈} C → C′ then ϕ ⇒ ψ is the unique morphism in (B ⇒ C) → (B′ ⇒ C′) making

[figure: (B ⇒ C) × B′; (B ⇒ C) × B; C; (B′ ⇒ C′) × B′; C′; I_{B⇒C} × ϕ; ap; (ϕ ⇒ ψ) × I_{B′}; ψ; ^{ap′}]

commute in K. Note that the subcategory S is assumed to be closed under products and exponentiations of both objects and morphisms.

• Applications

\frac{π ⊢ p_{1} : θ_{1} → θ π ⊢ p_{2} : θ_{1}}{π ⊢ p_{1} p_{2} : θ} μ[P] = ⟨μ[P_{1}], μ[P_{2}]⟩; ap ,

where ⟨μ[P_{1}], μ[P_{2}]⟩ is the mediating morphism from the object [[π]]^{∗} to the product ([[θ_{1}]] ⟹_{K} [[θ]]) × [[θ_{1}]], and ap is the application morphism from this product to [[θ]].

• Abstractions

\frac{[ π | ι: θ_{1} ] ⊢ p_{1} : θ_{2}}{π ⊢ λι. p_{1} : θ_{1} → θ_{2}} μ[P] = ab(¶; μ[P_{1}]) .

Here [ π | ι: θ_{1} ] denotes the type assignment with domain dom π ∪ {ι} that maps ι into θ_{1} and all other ι′ in its domain into πι′, while ¶ denotes the unique morphism making

[figure: [[π]]^{∗} × [[θ_{1}]]; _{[[[ π | ι: θ_{1} ]]]_{∗}}; [[θ_{1}]]; ¶; and; [[π]]^{∗} × [[θ_{1}]]; _{[[[ π | ι: θ_{1} ]]]_{∗}}; [[π]]^{∗}; [[πι′]]; ¶]

commute, the latter for all ι′ ^{∈} dom π − {ι}. (The unlabeled arrows in these diagrams denote the evident projection morphisms.)

Notice that abstractions do not contain type information, so that our inference rules describe an implicitly typed language. Of course, in practice one must use an explicitly typed language, since there is no type-inference decision procedure for intersection types [2]. But explicit type information is not needed to establish coherence; indeed the property of coherence is stronger when formulated for the implicitly typed case, since it implies that changing explicit type information cannot change semantics.

The next two cases deal with operations for constructing objects and extracting their fields (which are central to the object-oriented capabilities of Forsythe). Intuitively, ι ≡ p constructs an object with a single field whose name is ι and whose value is p, while p.ι extracts the value of the field named ι from the object p. In the actual semantics, however, [[ι: θ]] = [[θ]], i.e. single-field objects are identical to their field values, so that the semantic equations are trivial.

• Object Construction

\frac{π ⊢ p_{1} : θ_{1}}{π ⊢ (ι ≡ p_{1}) : (ι: θ_{1})} μ[P] = μ[P_{1}] .

• Field Selection

\frac{π ⊢ p_{1} : (ι: θ)}{π ⊢ p_{1}.ι : θ} μ[P] = μ[P_{1}] .

The next four rules describe the Forsythe “merging” operation. The essential idea is that a phrase p_{1}, p_{2} should take on the meanings of both p_{1} and p_{2}. However, to avoid ambiguity, the phrase p_{2} is required to be either a lambda expression or an object constructor, whose meaning “overwrites” the corresponding type of meaning of p_{1}. (The object-constructor case provides a limited kind of object concatenation that is much simpler than, for example, the approach of [8].)

• Merging

\frac{π ⊢ λι. p_{2} : θ_{1} → θ_{2}}{π ⊢ (p_{1}, λι. p_{2}) : θ_{1} → θ_{2}}  μ[P] = μ[P_{1}]

\frac{π ⊢ p_{1} : θ}{π ⊢ (p_{1}, λι. p_{2}) : θ} when θ is a primitive type

or has the form ι: θ_{1}

μ[P] = μ[P_{1}]

\frac{π ⊢ ι ≡ p_{2} : (ι: θ_{1})}{π ⊢ (p_{1}, ι ≡ p_{2}) : (ι: θ_{1})}  μ[P] = μ[P_{1}]

\frac{π ⊢ p_{1} : θ}{π ⊢ (p_{1}, ι ≡ p_{2}) : θ}

when θ is a primitive type or has the form θ_{1} → θ_{2} or ι′: θ_{1} where ι′ ≠ ι

μ[P] = μ[P_{1}] .

Finally, we give rules for fixed-point and conditional constructions. In these cases we cannot give an explicit semantics without specifying a particular semantic category; for example, the semantics are different for Forsythe than for a purely functional langauge. So we state the semantic equations in terms of unspecified entities Y_{k} and cd_{θ} for which we can give sufficient conditions to ensure coherence.

• Fixed Points

\frac{π ⊢ p_{1} : θ → θ}{π ⊢ rec p_{1} : θ} μ[P] = μ[P_{1}] ; Y_{[[θ]]} .

Here Y_{k} ^{∈} (k ⇒ k) → k is an object-indexed family of morphisms in K that satisfies the following condition: If p, ρ, ρ′ is a pullback in S of

[figure: p; k; k′; k′′; ρ; ρ′; ϕ; ϕ′]

and if the diagram

[figure: k̂; k ⇒ k; k′ ⇒ k′; p ⇒ k′′; α; α′; ρ ⇒ ϕ; ρ′ ⇒ ϕ′]

commutes in K then

commutes in K.

• Conditionals

\frac{π ⊢ p_{1} : bool π ⊢ p_{2} : θ π ⊢ p_{3} : θ}{π ⊢ if p_{1} then p_{2} else p_{3} : θ} μ[P] = ⟨μ[P_{1}], μ[P_{2}], μ[P_{3}]⟩;cd_{θ},

[figure: k̂; k ⇒ k; k′ ⇒ k′; α; α′; k; k′; k′′; ϕ; ϕ′; Y_{k}; Y_{k′}]

where ⟨μ[P_{1}], μ[P_{2}], μ[P_{3}]⟩ is the mediating morphism from [[π]]^{∗} to [[bool]] × [[θ]] × [[θ]]. Here cd_{θ} is a type-indexed family of morphisms in K that is required to be a natural transformation from the functor [[bool]] × [[−]] × [[−]] to the functor [[−]] (regarded as functors from the preordered set of types to K). (See Appendix.)

The reader who is familiar with [7] will notice that we have omitted a number of inference rules for various constructions in Forsythe. However, in an implicitly typed version of this language these constructions can all be defined as syntactic sugar, i.e. as abbreviations for phrases in the more basic language described above (with the inclusion of extra constants, such as add, that do not actually occur in Forsythe).

5 A Proof of Coherence

We will now prove that the inference rules and semantic equations in the previous section define a semantic function μ that is coherent. In fact, we will prove a stronger property of μ:

Proposition 4 Suppose P proves π ⊢ p : θ, P′ proves π′ ⊢ p : θ′, π′′ ≤ π, π′′ ≤ π′, θ ≤ θ′′, and θ′ ≤ θ′′. Then

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[θ]]; [[θ′]]; [[θ′′]]; μ[P]; μ[P′]]

commutes in K.

The special case where π = π′ = π′′ and θ = θ′ = θ′′ gives the coherence property. (Also, the special case where π = π′ = π′′ and θ′′ = θ ⊔ θ′ will be needed to show that the function μ is well-defined in the case of intersections.)

Proof : The proof is by induction on the sum of the sizes of the proofs P and P′.

(1a) If the main step of P is

\frac{π ⊢ p : θ_{1}}{π ⊢ p : θ} when θ_{1} ≤ θ

then μ[P] = μ[P_{1}] ; [[θ_{1} ≤ θ]]. In the diagram

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[θ]]; [[θ′]]; [[θ′′]]; [[θ_{1}]]; μ[P]; μ[P′]; μ[P_{1}]]

the inner hexagon commutes by the induction hypothesis, the leftmost triangle by the semantic equation, and the rightmost triangle since [[−]] is a functor. Thus the outer hexagon commutes.

(1b) If the main step of P′ is the rule for subtypes, then an argument symmetric to that of (1a) applies.

(2a) If the main step of P is

\overline{π ⊢ p : ns}

then μ[P] is the unique morphism from [[π]]^{∗} to [[ns]]. Then θ is ns, so that θ′′ ≃ ns, and since [[−]] is a functor, [[θ′′]] is isomorphic to [[ns]], which is a terminal object. Thus [[θ′′]] is also terminal, so that the hexagon commutes.

(2b) If the main step of P′ is the rule for nonsense, then an argument symmetric to that of (2a) applies.

(3a) If the main step of P is

\frac{π ⊢ p : θ_{1} π ⊢ p : θ_{2}}{π ⊢ p : θ_{1} & θ_{2}}

then μ[P] is the unique mediating morphism into the pullback:

[figure: [[π]]^{∗}; [[θ_{1} & θ_{2}]]; [[θ_{1}]]; [[θ_{2}]]; [[θ_{1} ⊔ θ_{2}]]; μ[P_{1}]; μ[P]; μ[P_{2}]]

This semantic equation only makes sense if the perimeter of the diagram commutes, but this condition is insured by the induction hypothesis, applied to P_{1} and P_{2}.

Since θ = θ_{1} &θ_{2} ≤ θ′′, Proposition 1 shows that there are θ′′_{1} and θ′′_{2} such that θ_{1} ≤ θ′′_{1}, θ_{2} ≤ θ′′_{2}, and θ′′ ≃ θ′′_{1} & θ′′_{2}. Thus everything in

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[θ_{1} & θ_{2}]]; [[θ_{1}]]; [[θ_{2}]]; [[θ′′]]; [[θ′′_{1}]]; [[θ′′_{2}]]; [[θ′′_{1} ⊔ θ′′_{2}]]; μ[P_{1}]; μ[P]; μ[P_{2}]]

commutes, and [[θ′′]] is a pullback of [[θ′′_{1}]], [[θ′′_{2}]], and [[θ′′_{1} ⊔ θ′′_{2}]].

It follows that the outside paths in

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π]]^{∗}; [[π]]^{∗}; [[θ_{1} & θ_{2}]]; [[θ_{1}]]; [[θ_{2}]]; [[θ′′]]; [[θ′′_{1}]]; [[θ′′_{2}]]; μ[P_{1}]; μ[P]; μ[P_{2}]]

are a cone for this pullback and, since the inner polygons commute, the middle path is a mediating morphism. But, by two applications of the induction hypothesis, to P_{1} and P′ and to P_{2} and P′ respectively, the inner polygons in

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[θ′]]; [[θ_{1}]]; [[θ_{2}]]; [[θ′′]]; [[θ′′_{1}]]; [[θ′′_{2}]]; μ[P_{1}]; μ[P′]; μ[P_{2}]]

also commute, so that the middle path here is also a mediating morphism. Then the equality of the mediating morphisms gives the desired result.

(3b) If the main step of P′ is the rule for intersections, then an argument symmetric to that of (3a) applies.

At this stage, we have considered all of the cases where the main step of P or P′ is a non-syntax-directed rule. In the remaining cases, since both P and P′ prove judgements about the same phrase p, their main steps must be syntax-directed rules for the same syntactic construction. Except in the case of the merging constructions, there is exactly one rule, which must be used as the main step of both proofs, for each construction.

(4) If p is an identifier ι, then the main steps of P and P′ must be

\overline{π ⊢ ι : π(ι)}  and  \overline{π′ ⊢ ι : π′(ι)}

where ι belongs to both dom π and dom π′, and μ[P] and μ[P′] must be projection morphisms. Then the definition of [[π′′ ≤ π]]^{∗} and [[π′′ ≤ π′]]^{∗} insures that the two parallelograms on the left of

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[θ]] = [[πι]]; [[θ′]] = [[π′ι]]; [[θ′′]]; [[π′′ι]]; μ[P] = p; μ[P′] = p′; p′′]

commute, while the functoriality of [[−]] insures that the diamond on the right commutes.

(5) If p is a constant c, then the main steps of P and P′ must be

\overline{π ⊢ c : θ_{c}}  and  \overline{π′ ⊢ c : θ_{c}}

with μ[P] = u_{π} ; μ_{c} and μ[P′] = u′_{π} ; μ_{c}. Then the triangles in

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[θ]] = [[θ_{c}]]; [[θ′]] = [[θ_{c}]]; [[θ′′]]; [[ns]]; u_{π}; u_{π′}; μ_{c}; μ_{c}; μ[P]; μ[P′]]

commute, the left diamond commutes since [[ns]] is terminal, and the right diamond commutes trivially.

(6) If p is an application p_{1} p_{2}, then the main steps of P and P′ must be

\frac{π ⊢ p_{1} : θ_{1} → θ π ⊢ p_{2} : θ_{1}}{π ⊢ p_{1} p_{2} : θ}  and  \frac{π′ ⊢ p_{1} : θ′_{1} → θ′ π′ ⊢ p_{2} : θ′_{1}}{π′ ⊢ p_{1} p_{2} : θ′}

with μ[P] = ⟨μ[P_{1}], μ[P_{2}]⟩; ap and μ[P′] = ⟨μ[P′_{1}], μ[P′_{2}]⟩; ap′. Since both θ_{1} → θ and θ′_{1} → θ′ are subtypes of (θ_{1} & θ′_{1}) → θ′′, the application of the induction hypothesis to P_{1} and P′_{1} shows that

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[θ_{1} → θ]]; [[θ′_{1} → θ′]]; [[(θ_{1} & θ′_{1}) → θ′′]]; μ[P_{1}]; μ[P′_{1}]]  (1)

commutes. On the other hand, since θ_{1} and θ′_{1} are both subtypes of θ_{1} ⊔ θ′_{1}, the application of the induction hypothesis to P_{2} and P′_{2} shows that the perimeter of

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[θ_{1}]]; [[θ′_{1}]]; [[θ_{1} ⊔ θ′_{1}]]; [[θ_{1} & θ′_{1}]]; μ[P_{2}]; μ[P′_{2}]; β]  (2)

commutes, so that the definition of intersection as a pullback establishes that there is a unique morphism β making the two parallelograms commute. Now consider the diagram

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[θ_{1} → θ]] × [[θ_{1} & θ′_{1}]]; [[θ′_{1} → θ′]] × [[θ_{1} & θ′_{1}]]; [[θ_{1} → θ]] × [[θ_{1}]]; [[(θ_{1} & θ′_{1}) → θ′′]] × [[θ_{1} & θ′_{1}]]; [[θ′_{1} → θ′]] × [[θ′_{1}]]; [[θ]]; [[θ′]]; [[θ′′]]; ⟨[[π′′ ≤ π]]^{∗} ; μ[P_{1}], β⟩; ⟨[[π′′ ≤ π′]]^{∗} ; μ[P′_{1}], β⟩; ⟨μ[P_{1}], μ[P_{2}]⟩; ⟨μ[P′_{1}], μ[P′_{2}]⟩; ap; ^{ap′′}; _{ap_{′}}]

From the commutativity of Diagram 1 and elementary properties of products, the central quadrilateral commutes. From the commutativity of the parallelograms in Diagram 2 and elementary properties of products, the quadrilaterals at the upper and lower left commute. Finally, since Proposition 3 gives

[[θ_{1} → θ ≤ (θ_{1} & θ′_{1}) → θ′′]] = [[(θ_{1} & θ′_{1}) ≤ θ_{1}]] ⇒ [[θ ≤ θ′′]]

(and similarly for θ′_{1} → θ′), the definition of ⇒ on morphisms implies that the pentagons at the upper (and lower) right commute. The desired result follows from the semantic equations.

(7) If p is an abstraction λι. p_{1}, then the main steps of P and P′ must be

\frac{[ π | ι: θ_{1} ] ⊢ p_{1} : θ_{2}}{π ⊢ λι. p_{1} : θ_{1} → θ_{2}}  and  \frac{[ π′ | ι: θ′_{1} ] ⊢ p_{1} : θ′_{2}}{π′ ⊢ λι. p_{1} : θ′_{1} → θ′_{2}}

with μ[P] = ab(¶; μ[P_{1}]) and μ[P′] = ab(¶′; μ[P′_{1}]). Let θ′′_{1} = θ_{1} & θ′_{1} and θ′′_{2} = θ_{2} ⊔ θ′_{2}, and consider the diagram

[figure: [[π′′]]^{∗} × [[θ′′_{1}]]; [[[ π′′ | ι: θ′′_{1} ]]]^{∗}; [[θ′′_{2}]]; (1); [[π]]^{∗} × [[θ_{1}]]; ^{[[[ π | ι: θ_{1} ]]]^{∗}}; [[θ_{2}]]; [[π]]^{∗} × [[θ′′_{1}]]; [[θ_{1} → θ_{2}]] × [[θ′′_{1}]]; [[θ_{1} → θ_{2}]] × [[θ_{1}]]; [[θ′′_{1} → θ′′_{2}]] × [[θ′′_{1}]]; μ[P] × I; ap; ^{ap′′}; [[π′]]^{∗} × [[θ′_{1}]]; [[θ′_{1} → θ′_{2}]] × [[θ′_{1}]]; μ[P′] × I; ^{¶′′}; ¶; μ[P_{1}]; μ[P] × I; (2); (3); (4); (5); _{[[[ π′ | ι: θ′_{1} ]]]_{∗}}; [[θ′_{2}]]; [[π′]]^{∗} × [[θ′′_{1}]]; [[θ′_{1} → θ′_{2}]] × [[θ′′_{1}]]; [[θ′′_{1} → θ′′_{2}]] × [[θ′′_{1}]]; _{ap_{′}}; _{ap_{′′}}; _{¶_{′}}; μ[P′_{1}]; μ[P′] × I; (2); (3); (4); (5)]

The commutativity of (1) is established by the induction hypothesis, that of (2) by the definition of ¶ and properties of products, that of (3) by the semantic equation and the property of Cartesian closure, that of (4) by properties of products, and that of (5) by Proposition 3 and the definition of ⇒ on morphisms.

From the commutativity of the perimeter, using properties of products again, we get

(([[π′′ ≤ π]]^{∗} ; μ[P] ; [[θ_{1} → θ_{2} ≤ θ′′_{1} → θ′′_{2}]]) × I_{[[θ′′_{1}]]}); ap′′ =
(([[π′′ ≤ π′]]^{∗} ; μ[P′] ; [[θ′_{1} → θ′_{2} ≤ θ′′_{1} → θ′′_{2}]]) × I_{[[θ′′_{1}]]}); ap′′ .

Then the uniqueness of abstraction morphisms establishes the commutativity of the inner hexagon in

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[θ_{1} → θ_{2}]]; [[θ′_{1} → θ′_{2}]]; [[θ′′_{1} → θ′′_{2}]]; [[θ′′]]; μ[P]; μ[P′]]

The rest of the diagram is justified by the fact that θ′′_{1} → θ′′_{2} = (θ_{1} & θ′_{1}) → (θ_{2} ⊔ θ′_{2}) is a least upper bound of θ = θ_{1} → θ_{2} and θ′ = θ′_{1} → θ′_{2}, and thus a subtype of θ′′.

(8) If p is an object constructor ι ≡ p_{1}, then the main steps of P and P′ must be

\frac{π ⊢ p_{1} : θ_{1}}{π ⊢ (ι ≡ p_{1}) : (ι: θ_{1})}  and  \frac{π′ ⊢ p_{1} : θ′_{1}}{π′ ⊢ (ι ≡ p_{1}) : (ι: θ′_{1})}

with μ[P] = μ[P_{1}] and μ[P′] = μ[P′_{1}]. The induction hypothesis gives the commutativity of so that, by the semantic equation and Proposition 3,

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[θ_{1}]]; [[θ′_{1}]]; [[θ_{1} ⊔ θ′_{1}]]; μ[P_{1}]; μ[P′_{1}]]

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[ι: θ_{1}]]; [[ι: θ′_{1}]]; [[ι: (θ_{1} ⊔ θ′_{1})]]; μ[P]; μ[P′]]

commutes. Then, as in the previous case, the desired result follows from the fact that ι: (θ_{1} ⊔ θ′_{1}) is a least upper bound of θ = ι: θ_{1} and θ′ = ι: θ′_{1}, and thus a subtype of θ′′.

(9) If p is a selection operation p_{1}.ι, then the main steps of P and P′ must be

\frac{π ⊢ p_{1} : (ι: θ)}{π ⊢ p_{1}.ι : θ}  and  \frac{π′ ⊢ p_{1} : (ι: θ′)}{π′ ⊢ p_{1}.ι : θ′}

with μ[P] = μ[P_{1}] and μ[P′] = μ[P′_{1}]. The argument here is essentially the same as in the previous case.

(10) If p is a merging operation p_{1}, λι. p_{2}, the the main steps of P and P′ must be

π ⊢ λι. p_{2} : θ_{1} → θ_{2} π ⊢ (p_{1}, λι. p_{2}) : θ_{1} → θ_{2} or π ⊢ p_{1} : θ π ⊢ (p_{1}, λι. p_{2}) : θ when θ is a primitive

type or has the form ι: θ_{1}

and

π′ ⊢ λι. p_{2} : θ′_{1} → θ′_{2} π′ ⊢ (p_{1}, λι. p_{2}) : θ′_{1} → θ′_{2} or π′ ⊢ p_{1} : θ′ π′ ⊢ (p_{1}, λι. p_{2}) : θ′ when θ′ is a primitive

type or has the form ι: θ′_{1}

with μ[P] = μ[P_{1}] and μ[P′] = μ[P′_{1}]. If the main steps of P and P′ are both rules on the left or both rules on the right, then the induction hypothesis gives the desired result immediately. On the other hand, if one main step is the rule on the left and the other is the rule on the right then, by Proposition 2, ns is a least upper bound of θ and θ′, so that θ′′ ≃ ns. Then the desired result follows since [[θ′′]] is terminal.

(11) If p is a merging operation p_{1}, ι ≡ p_{2}, then the argument is similar to the previous case.

(12) If p is a fixed-point construction rec p_{1}, then the main steps of P and P′ must be

\frac{π ⊢ p_{1} : θ → θ}{π ⊢ rec p_{1} : θ}  and  \frac{π′ ⊢ p_{1} : θ′ → θ′}{π′ ⊢ rec p_{1} : θ′}

with μ[P] = μ[P_{1}] ; Y_{[[θ]]} and μ[P′] = μ[P′_{1}] ; Y_{[[θ′]]}. Since [[θ & θ′]] is a pullback of [[θ]], [[θ′]], and [[θ ⊔ θ′]], and since by the induction hypothesis

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[θ → θ]]; [[θ′ → θ′]]; [[(θ & θ′) → (θ ⊔ θ′)]]; μ[P_{1}]; μ[P′_{1}]]

commutes, the condition satisfied by the Y_{k} implies the commutativity of

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[θ → θ]]; [[θ′ → θ′]]; [[θ]]; [[θ′]]; [[θ ⊔ θ′]]; μ[P_{1}]; μ[P′_{1}]; Y_{[[θ]]}; Y_{[[θ′]]}]

Then the desired result follows from the semantic equations and θ ⊔ θ′ ≤ θ′′.

(13) If p is a conditional construction if p_{1} then p_{2} else p_{3}, then the main steps of P and P′ must be

\frac{π ⊢ p_{1} : bool π ⊢ p_{2} : θ π ⊢ p_{3} : θ}{π ⊢ if p_{1} then p_{2} else p_{3} : θ} \frac{π′ ⊢ p_{1} : bool π′ ⊢ p_{2} : θ′ π′ ⊢ p_{3} : θ′}{π′ ⊢ if p_{1} then p_{2} else p_{3} : θ′}

with μ[P] = ⟨μ[P_{1}], μ[P_{2}], μ[P_{3}]⟩ ; cd_{θ} and μ[P′] = ⟨μ[P′_{1}], μ[P′_{2}], μ[P′_{3}]⟩ ; cd_{θ′}. By the induction hypothesis for each of the three premisses, the perimeters of

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[bool]]; μ[P_{1}]; μ[P′_{1}]; β_{1}; and; [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[θ]]; [[θ′]]; [[θ ⊔ θ′]]; [[θ & θ′]]; μ[P_{2}]; μ[P′_{2}]; β_{2}]

and a similar diagram for P_{3} and P′_{3} must commute. Thus, trivially in the first case and by the definition of θ&θ′ as a pullback in the remaining cases, there are morphisms β_{1}, β_{2}, and β_{3} that make the interior triangles and parallelograms commute. Then the lefthand parallelograms in

[figure: [[π′′]]^{∗}; [[π]]^{∗}; [[π′]]^{∗}; [[bool]] × [[θ & θ′]] × [[θ & θ′]]; [[bool]] × [[θ]] × [[θ]]; [[bool]] × [[θ′]] × [[θ′]]; [[θ & θ′]]; [[θ]]; [[θ′]]; [[θ′′]]; ⟨β_{1}, β_{2}, β_{3}⟩; ⟨μ[P_{1}], μ[P_{2}], μ[P_{3}]⟩; ⟨μ[P′_{1}], μ[P′_{2}], μ[P′_{3}]⟩; ^{cd^{θ&θ′}}; ^{cd^{θ}}; _{cd_{θ′}}]

commute, and the rest of the diagram commutes since cd is natural and [[−]] is a functor. The desired result follows from the semantic equations. (End of Proof )

Acknowledgement

The author wishes to thank Andre Scedrov for convincing him of the importance of coherence.

References

[1] V. Breazu-Tannen, T. Coquand, C. A. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and Computation, 93(1):172–222, July 1991.

[2] M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Z. Math. Logik Grundlagen Math., 27:45–58, 1981.

[3] F. J. Oles. A Category-Theoretic Approach to the Semantics of Programming Languages. Ph. D. dissertation, Syracuse University, August 1982.

[4] F. J. Oles. Type algebras, functor categories, and block structure. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, pages 543–573. Cambridge Univ. Press, Cambridge, England, 1985.

[5] J. C. Reynolds. Using category theory to design implicit conversions and generic operators. In N. D. Jones, editor, Semantics-Directed Compiler Generation, volume 94 of Lect. Notes in Computer Sci., pages 211–258, Berlin, 1980. Springer-Verlag.

[6] J. C. Reynolds. Conjunctive types and Algol-like languages (abstract of invited lecture). In Proc. Symp. on Logic in Computer Science, page 119, 1987. Full text in preparation.

[7] J. C. Reynolds. Preliminary design of the programming language Forsythe. Report CMU-CS-88-159, Carnegie Mellon University, June 21, 1988.

[8] M. Wand. Type inference for record concatenation and multiple inheritance. In Proc. Fourth Annual Symp. on Logic in Computer Science, pages 92–97, 1989.

A Conditionals in Forsythe

To complete the definition of Forsythe and show that it is coherent, we would have to specify the categories K and S, the morphism families Y_{k} and cd_{θ}, and the meaning of various constants, and demonstrate that these entities satisfy the assumptions stated in this paper. For the most part, such a development is beyond the scope of our presentation. In this appendix, however, we consider one aspect that is closely related to the rest of the paper and does not involve the details of functor-category semantics.

In Forsythe, the conditional construction is first defined for primitive types and then defined by induction for all types. Here we show that if the initial definition for primitives is a natural transformation then the inductively defined extension is a natural transformation.

Let B be the functor from the preordered set of types to K such that B(−) = [[bool]]× (−) × (−), and assume that cd is a natural transformation from B[[J(−)]] to [[J(−)]], where J is the injection from primitive types to types. Then we extend cd_{θ} ^{∈} B[[θ]] → [[θ]] to all types θ as follows:

• cd_{θ_{1}→θ_{2}} = ab(Ψ_{[[θ_{1}→θ_{2}]],[[θ_{1}]]} ; B(ap) ; cd_{θ_{2}}),

where Ψ_{k,k′} is the evident morphism from the product ([[bool]] × k × k) × k′ to the product [[bool]] × (k × k′) × (k × k′) that “duplicates its second argument”.

• cd_{ι:θ} = cd_{θ}.

• cd_{ns} is the unique morphism from B[[ns]] to [[ns]].

• cd_{θ_{1}&θ_{2}} is the unique morphism into the pullback:

[figure: B[[θ_{1} & θ_{2}]]; B[[θ_{1}]]; B[[θ_{2}]]; [[θ_{1}]]; [[θ_{2}]]; [[θ_{1} & θ_{2}]]; [[θ_{1} ⊔ θ_{2}]]; ^{cd^{θ_{1}&θ_{2}}}; ^{cd^{θ_{1}}}; _{cd_{θ_{2}}}]

The final case of the definition only makes sense if the perimeter of the diagram commutes, but the following proposition will establish that this condition is always met.

Proposition 5 Suppose θ̂ is a lower bound, and θ′′ is an upper bound, of θ and θ′. Then

[figure: B[[θ̂]]; B[[θ]]; B[[θ′]]; [[θ]]; [[θ′]]; [[θ′′]]; ^{cd^{θ}}; _{cd_{θ′}}]

commutes in K.

Notice that this proposition, in the special case where θ̂ = θ ≤ θ′ = θ′′, implies the naturality of cd. Proof : The proof is by induction on the sum of the sizes of the types θ and θ′. (1a) If θ = ns then θ′′ ≃ ns, so that [[θ′′]] is terminal, and the hexagon commutes. (1b) If θ′ = ns then an argument symmetric to (1a) applies. (2a) If θ = θ_{1} & θ_{2} then cd_{θ} is the unique mediating morphism into the pullback:

[figure: B[[θ]]; B[[θ_{1}]]; B[[θ_{2}]]; [[θ_{1}]]; [[θ_{2}]]; [[θ]]; [[θ_{1} ⊔ θ_{2}]]; ^{cd^{θ}}; ^{cd^{θ_{1}}}; _{cd_{θ_{2}}}]

This only makes sense if the perimeter of this diagram commutes, but this condition is insured by the induction hypothesis, applied to θ_{1} and θ_{2}. Since θ = θ_{1} &θ_{2} ≤ θ′′, Proposition 1 shows that there are θ′′_{1} and θ′′_{2} such that θ_{1} ≤ θ′′_{1}, θ_{2} ≤ θ′′_{2}, and θ′′ ≃ θ′′_{1} & θ′′_{2}. Thus everything in

[figure: B[[θ̂]]; B[[θ]]; B[[θ_{1}]]; B[[θ_{2}]]; [[θ_{1}]]; [[θ_{2}]]; [[θ]]; ^{cd^{θ}}; ^{cd^{θ_{1}}}; _{cd_{θ_{2}}}; [[θ′′]]; [[θ′′_{1}]]; [[θ′′_{2}]]; [[θ′′_{1} ⊔ θ′′_{2}]]]

commutes, and [[θ′′]] is a pullback of [[θ′′_{1}]], [[θ′′_{2}]], and [[θ′′_{1} ⊔ θ′′_{2}]].

It follows that the outside paths in

[figure: B[[θ̂]]; B[[θ]]; B[[θ_{1}]]; B[[θ_{2}]]; [[θ_{1}]]; [[θ_{2}]]; [[θ]]; ^{cd^{θ}}; ^{cd^{θ_{1}}}; _{cd_{θ_{2}}}; [[θ′′]]; [[θ′′_{1}]]; [[θ′′_{2}]]]

are a cone for this pullback and, since the inner polygons commute, the middle path is a mediating morphism. But, by two applications of the induction hypothesis, to θ_{1} and θ′ and to θ_{2} and θ′ respectively, the inner polygons in

[figure: B[[θ̂]]; B[[θ′]]; B[[θ_{1}]]; B[[θ_{2}]]; [[θ_{1}]]; [[θ_{2}]]; [[θ′]]; ^{cd^{θ′}}; ^{cd^{θ_{1}}}; _{cd_{θ_{2}}}; [[θ′′]]; [[θ′′_{1}]]; [[θ′′_{2}]]]

also commute, so that the middle path here is also a mediating morphism. Then the equality of the mediating morphisms gives the desired result.

(2b) If θ′ = θ_{1} & θ_{2} then an argument symmetric to (2a) applies.

(3) In the remaining cases, Proposition 2 shows that ns is a least upper bound of θ and θ′ unless θ and θ′ are both primitive types and have a primitive least upper bound, or both procedural types, or both object types with the same field name. But when ns is a least upper bound, [[θ′′]] must be terminal.

(4) If θ = ρ and θ′ = ρ′ are primitive types with a least upper bound, then the naturality of cd for primitive types gives the commutativity of

[figure: B[[θ̂]]; B[[ρ]]; B[[ρ′]]; [[ρ]]; [[ρ′]]; B[[ρ ⊔ ρ′]]; [[ρ ⊔ ρ′]]; ^{cd^{ρ}}; _{cd_{ρ′}}; ^{cd^{ρ⊔ρ′}}]

and the desired result follows since ρ ⊔ ρ′ = θ ⊔ θ′ ≤ θ′′.

(5) If θ = θ_{1} → θ_{2} and θ′ = θ′_{1} → θ′_{2} then

cd_{θ} = ab(Ψ_{[[θ]],[[θ_{1}]]} ; B(ap) ; cd_{θ_{2}}) and cd_{θ′} = ab(Ψ_{[[θ′]],[[θ′_{1}]]} ; B(ap′) ; cd_{θ′_{2}}) .

Let θ′′_{1} = θ_{1} & θ′_{1} and θ′′_{2} = θ_{2} ⊔ θ′_{2}, and consider the diagram

[figure: [[θ̂]] × [[θ′′_{1}]]; [[θ]] × [[θ′′_{1}]]; [[θ]] × [[θ_{1}]]; [[θ′]] × [[θ′′_{1}]]; [[θ′]] × [[θ′_{1}]]; [[θ′′_{1} → θ′′_{2}]] × [[θ′′_{1}]]; [[θ_{2}]]; [[θ′_{2}]]; [[θ′′_{2}]]; ap; ap′; ap′′]

Since

[[θ ≤ θ′′_{1} → θ′′_{2}]] = [[θ_{1} → θ_{2} ≤ θ′′_{1} → θ′′_{2}]] = [[θ′′_{1} ≤ θ_{1}]] ⇒ [[θ_{2} ≤ θ′′_{2}]] ,

(and similarly for θ′), the definition of ⇒ on morphisms implies that the upper (and lower) pentagons commute. Thus the perimeter commutes, and by the definition of θ_{2} & θ′_{2} as a pullback, there is a unique mediating morphism β that makes the two parallelograms in

[figure: [[θ̂]] × [[θ′′_{1}]]; [[θ]] × [[θ_{1}]]; [[θ′]] × [[θ′_{1}]]; [[θ_{2}]]; [[θ′_{2}]]; [[θ′′_{2}]]; [[θ_{2} & θ′_{2}]]; ap; ap′; β]

commute. Now consider the diagram

[figure: B[[θ̂]] × [[θ′′_{1}]]; B([[θ̂]] × [[θ′′_{1}]]); B[[θ_{2} & θ′_{2}]]; [[θ′′_{2}]]; Ψ′′; Bβ; (1); B[[θ]] × [[θ_{1}]]; B([[θ]] × [[θ_{1}]]); B[[θ_{2}]]; [[θ_{2}]]; B[[θ]] × [[θ′′_{1}]]; [[θ]] × [[θ′′_{1}]]; [[θ]] × [[θ_{1}]]; [[θ′′_{1} → θ′′_{2}]] × [[θ′′_{1}]]; cd_{θ} × I; ap; ^{ap′′}; Ψ; B ap; ^{cd^{θ_{2}}}; cd_{θ} × I; (3); (2); (4); (5); (6); B[[θ′]] × [[θ′_{1}]]; B([[θ′]] × [[θ′_{1}]]); B[[θ′_{2}]]; [[θ′_{2}]]; B[[θ′]] × [[θ′′_{1}]]; [[θ′]] × [[θ′′_{1}]]; [[θ′]] × [[θ′_{1}]]; [[θ′′_{1} → θ′′_{2}]] × [[θ′′_{1}]]; cd_{θ′} × I; _{ap_{′}}; _{ap_{′′}}; Ψ′; B ap′; _{cd_{θ′_{2}}}; cd_{θ′} × I; (3); (2); (4); (5); (6)]

The commutativity of (1) is established by the induction hypothesis, that of (2) by applying B to the previous diagram, that of (3) by properties of products that insure that Ψ is natural, that of (4) by the definition of cd_{θ} and the property of Cartesian closure, that of (5) by properties of products, and that of (6) by Proposition 3 and the definition of ⇒ on morphisms.

From the commutivity of the perimeter, using properties of products again, we get

((B[[θ̂ ≤ θ]] ; cd_{θ} ; [[θ ≤ θ′′_{1} → θ′′_{2}]]) × I_{[[θ′′_{1}]]}); ap′′ =
((B[[θ̂ ≤ θ′]] ; cd_{θ′} ; [[θ′ ≤ θ′′_{1} → θ′′_{2}]]) × I_{[[θ′′_{1}]]}); ap′′ .

Then the uniqueness of abstraction morphisms establishes the commutativity of

[figure: B[[θ̂]]; B[[θ]]; B[[θ′]]; [[θ]]; [[θ′]]; [[θ′′_{1} → θ′′_{2}]]; ^{cd^{θ}}; _{cd_{θ′}}]

and the desired result follows since θ′′_{1} → θ′′_{2} is a least upper bound of θ and θ′, and thus a subtype of θ′′.

(6) If θ = ι: θ_{1} and θ′ = ι: θ′_{1} then the induction hypothesis gives the commutativity of

[figure: B[[θ_{1} & θ′_{1}]]; B[[θ_{1}]]; B[[θ′_{1}]]; [[θ_{1}]]; [[θ′_{1}]]; [[θ_{1} ⊔ θ′_{1}]]; ^{cd^{θ_{1}}}; _{cd_{θ′_{1}}}]

Then since cd_{ι:θ_{1}} = cd_{θ_{1}} and [[ι: θ_{1}]] = [[θ_{1}]], and similarly for θ′_{1}, θ_{1} & θ′_{1}, θ_{1} ⊔ θ′_{1},

[figure: B[[ι: (θ_{1} & θ′_{1})]]; B[[ι: θ_{1}]]; B[[ι: θ′_{1}]]; [[ι: θ_{1}]]; [[ι: θ′_{1}]]; [[ι: (θ_{1} ⊔ θ′_{1})]]; ^{cd^{ι:θ_{1}}}; _{cd_{ι:θ′_{1}}}]

commutes. The desired result follows since θ̂ ≤ ι: θ_{1}&ι: θ′_{1} ≤ ι: (θ_{1}&θ′_{1}) and ι: (θ_{1}⊔θ′_{1}) ≃ ι: θ_{1} ⊔ ι: θ′_{1} ≤ θ′′. (End of Proof )