Anti-Symmetry of Higher-Order Subtyping

Adriana Compagnoni^{∗}

                          abc@dcs.ed.ac.uk

Healfdene Goguen^{†}

                                                     hhg@sage.att.com

December 14, 1998

Abstract

This paper shows that the subtyping relation of a higher-order lambda calculus, F_{≤}^{ω}, is antisymmetric. It exhibits the first such proof, establishing in the process that the subtyping relation is a partial order—reflexive, transitive and anti-symmetric. While a subtyping relation is reflexive and transitive by definition, anti-symmetry is a derived property. This property has been conjectured by many researchers in the community but never proved. The result, which may seem obvious to the non-expert, is technically challenging, and had been an open problem for almost a decade. In this context, typed operational semantics for subtyping offers a powerful new technology to solve the problem.

1 Introduction

During the last decade, object-oriented programming languages such as Smalltalk, C++, Modula 3, and Java have become popular because they encourage and facilitate software reuse and abstract design. One attempt to give a theoretical understanding of these object-oriented programming languages has been to introduce type systems with features to model constructs from object-oriented programming languages [8, 10], for example bounded quantification [20] and recursive types [2].

Metatheoretic properties of the type systems are important to justify the programming languages being modeled. One important property of a type system is subject reduction or type preservation, which states that evaluation of programs preserves their type. This is one of the central results of an earlier paper [15], which also showed the correctness of the algorithms for type-formation and subtyping. Another important property for type systems is the decidability of type-checking and subtyping: a compiler should be able to process basic type information reliably without help from the programmer in order to prevent basic programming errors. Decidability of type-checking ensures that this will always be possible, and decidability of subtyping is a crucial step to proving this. This result was proved in [14].

The subtyping relation has been extensively researched because of its importance in applications to programming languages [26, 1, 6, 21], proof assistants [27, 3, 24], and metatheoretical studies [18, 4, 7, 10, 5, 19, 16, 23, 31, 15, 14], to name a few. However, none of these studies has established the antisymmetry of the subtyping relation for a higher-order calculus. In some cases it has been conjectured, as in [32]. In other cases, equality has been defined using subtyping: A = B is defined as A ≤ B and B ≤ A. Steffen [30] has showed the simpler property, in the presence of polarized subtyping, that A ≤ B and B ≤ A, where both derivations are without uses of promotion, if and only if A = B.

∗Stevens Institute of Technology, Castle Point on Hudson, Hoboken, NJ 07030, USA. Tel:201-216-5328.

†AT&T Labs, 180 Park Ave., Florham Park NJ 07030 USA.

Anti-symmetry has been demonstrated for F_{≤} [20]. However, the problem there is considerably easier, because there is no notion of computation on types, and in particular no β-reduction.

The remainder of the paper is structured as follows. In the following sections of the introduction we discuss technical points relating to typed operational semantics and anti-symmetry of subtyping. In Section 2 we introduce the basic language of F_{≤}^{ω}. In Section 3 we introduce the typed operational semantics, which as explained above plays a central role in our proof of anti-symmetry by providing a powerful induction principle. Section 4 outlines the proof of anti-symmetry using the typed operational semantics. Section 5 outlines the results that we use from our earlier development of typed operational semantics for F_{≤}^{ω}. In Section 6 we give a sketch of the metatheory of a new presentation of F_{≤}^{ω} without judgemental equality or conversion. Finally, we draw conclusions in Section 7.

Typed Operational Semantics

Our proof of anti-symmetry of higher-order subtyping relies on our understanding of subtyping built up using typed operational semantics. Typed operational semantics gives an alternative induction principle for type theories, by presenting type theory operationally rather than declaratively. The typed operational semantics has judgements for reduction to weak-head and normal form for types, and for subtyping comparison between types in weak-head normal form and arbitrary types. Because the system is presented from the perspective of computation, many properties about the relationship between reduction and typing are particularly easy to show by induction on derivations of the typed operational semantics. This topic is dealt with extensively in an earlier publication [15].

The difficulty with showing anti-symmetry for higher-order subtyping has been in showing one particular lemma, the underivability of Γ(X)(A_{1}, …, A_{n}) ≤ X(A_{1}, …, A_{n}). Otherwise, the proof is straightforward, as we demonstrate in Section 4.

The particular property that drives our proof of this lemma is that the typing rule in the typed operational semantics for variables applied to a sequence of terms has a subderivation stating the wellformedness of the type resulting from the replacement of the variable with its bound. This rule of inference is justified by our earlier proofs of Soundness and Completeness of the typed operational semantics for the usual rules of inference, published elsewhere [15]. The development of the full metatheory of typed operational semantics is quite complex, and in particular the proof of Soundness is similar to proofs of strong normalization and relies on logical relations.

However, once we have this equivalence in place, we can define a simple measure, from derivations to natural numbers, that counts the number of uses of promotion (replacing a variable by its bound) before reaching Top. Clearly, the number of uses of the variable rule in a derivation of X(A_{1}, …, A_{n}) ≤ T must be greater than the number of uses in a derivation of Γ(X)(A_{1}, …, A_{n}) ≤ T. On the other hand, we can also show that if A ≤ B then the number of uses of the variable rule in A ≤ T is greater than or equal to the number in B ≤ T. Hence, if we have a derivation of Γ(X)(A_{1}, …, A_{n}) ≤ X(A_{1}, …, A_{n}) then we can derive a contradiction.

Induced Equivalence Relations

The equivalence relation induced by A ≤ B and B ≤ A may be stronger than the usual intensional equality associated with type theory, syntactic equivalence on normal forms. One such case is [29], where the types ∀(X <: Bot)X→X and ∀(X <: Bot)Bot→Bot are “equivalent in the subtype relation^{1}, even though they are not syntactically identical.” A similar situation appears in intersection types disciplines, where ⊤ = A→⊤ and also A→⊤ ≤ ⊤ and ⊤ ≤ A→⊤. A final example is extensible records [11], where the extension operator is associative and commutative in the subtyping relation. Such equivalence relations have models in existing frameworks, for example game semantics [13] or PER models [17].

1A and B are equivalent in the subtyping relation if A ≤ B and B ≤ A.

Such equivalences can be interesting in the context of programming languages. For example, consider object types with a private section and a public interface, where two object types O_{1} and O_{2} may satisfy O_{1} ≤ O_{2} and O_{2} ≤ O_{1}, but differ in their private section. The equivalence relation that only considers the public interface will be more interesting to the programmer than intensional equality, because it is more permissive.

In our current work on F_{≤}^{ω}, we only consider a very basic subtyping relation. Hence, the resulting equivalence relation is simply the usual notion of β-equality at the type level.

Metatheoretic Consequences of Anti-Symmetry

In addition to providing the answer to a long-standing open problem, our work has several consequences in the development of the metatheory of type systems with subtyping. First, in the presence of antisymmetry for subtyping, we can eliminate the equality relation as a basic judgement of the type system. This means that the proof of soundness for model constructions, such as that for proofs of strong normalization or PER models, can be more concise. We give a sketch of a new presentation of F_{≤}^{ω}, without judgemental equality or conversion, and discuss how the development of the metatheory proceeds for this system. The lack of a notion of equality may also have consequences for the implementation of type theories with subtyping.

Another consequence of this result is that we can now prove the Minimum Types Property, as opposed to the Minimal Types Property which is normally proved. Each term could have many minimal types, and an algorithm would find one of them. We can now state clearly the relation between all the minimal types of a given term: before we knew that any two minimal types were subtypes of each other, and we now know that they are β-equal.

2 Syntax

We now introduce the basic language of F_{≤}^{ω}. A complete development of its meta-theory can be found in [15].

The kinds of F_{≤}^{ω} are the kind ⋆ of proper types and the kinds ΠX≤A:K_{1}.K_{2} of functions on types, or type operators.

The language of types of F_{≤}^{ω} is a straightforward higher-order extension of F_{≤}, where we allow bounds on the abstraction ΛX≤A:K_{1}.B. The capture-avoiding substitution of A for X in B is written B[X←A]. We identify types that differ only in the names of bound variables. We shall write A(B_{1}, …, B_{n}) for ((A B_{1}) … B_{n}).

The language of terms is the same as that for F_{≤}, with bounded type abstraction ΛX≤A:K.M. As in F_{≤}, each type variable is given an upper bound at the point where it is introduced.

The operational semantics of F_{≤}^{ω} is given by the usual β-reduction rules on terms and types, and is extended to a compatible relation with respect to term or type formation. We write ↠_{β} for the transitive and reflexive closure of →_{β} and =_{β} for the least equivalence relation containing →_{β} and closed under α-equivalence.

Contexts are defined as usual, where the empty context is written ∅, term variable bindings have the form x:A, and type variable bindings have the form X≤A:K. We write dom(Γ) for the set of term and type variables defined in a context Γ. The sets of free term and type variables occurring in terms, types, kinds, contexts or judgements are written FV(—) and FTV(—). Since we are careful to ensure that no variable is bound more than once, we sometimes consider contexts as finite functions: Γ(X) yields the bound of X in Γ, where X ∈ dom(Γ) is implicitly asserted.

The system F_{≤}^{ω} is presented as simultaneously defined inductive relations with the following judgement forms:

Γ ⊢ ok  well-formed context
Γ ⊢ K  well-formed kind
Γ ⊢ K =_{β} K′  kind equality
Γ ⊢ A : K  well-kinded type
Γ ⊢ A =_{β} B : K type equality
Γ ⊢ A ≤ B : K subtype
Γ ⊢ M : A  well-typed term.

We sometimes use the metavariable J to range over statements (right-hand sides of judgements) of any of these judgement forms.

We now give an overview of the rules of inference for F_{≤}^{ω}. The context formation rules are as usual in F_{<:}^{ω}. Kind formation differs by incorporating information about the bounds in Π:

\frac{Γ, X≤A:K_{1} ⊢ K_{2}}{Γ ⊢ ΠX≤A:K_{1}.K_{2}}  (K-Π)

The rules of inference for kind equality simply define a typed equivalence relation compatible with respect to the kind formers.

The rules for type formation similarly need to be adjusted for bounded operator abstraction:

\frac{Γ, X≤A_{1}:K_{1} ⊢ A_{2} : K_{2}}{Γ ⊢ ΛX≤A_{1}:K_{1}.A_{2} : ΠX≤A_{1}:K_{1}.K_{2}}  (T-TAbs)

\frac{Γ ⊢ A : ΠX≤B:K_{1}.K_{2} Γ ⊢ C≤B : K_{1}}{Γ ⊢ A C : K_{2}[X←C]}  (T-TApp)

\frac{Γ ⊢ A ≤ B : K  Γ ⊢ K =_{β} K′}{Γ ⊢ A ≤ B : K′}  (T-Conv)

Type equality is defined as the typed equivalence relation compatible with respect to the type formers and closed under β-reduction for types.

\frac{Γ, X≤A_{1}:K_{1} ⊢ A_{2} : K_{2}  Γ ⊢ C ≤ A_{1} : K_{1}}{Γ ⊢ (ΛX≤A_{1}:K_{1}.A_{2}) C =_{β} A_{2}[X←C] : K_{2}[X←C]}  (T-Eq-Beta)

The Type Equality rules appear in Appendix A.

The subtyping rules are again those of F_{<:}^{ω} [9, 10, 25], except for those dealing with bounded type abstraction and type application and the rule for subtyping the quantifier. We chose Cardelli and Wegner’s kernel Fun rule for quantifiers with equal bounds [12], because the contravariant rule for quantifiers renders the system undecidable [28]. Furthermore, transitivity elimination in the presence of such a rule in the higher-order case remains an open problem. Type equality is included in subtyping.

\frac{Γ ⊢ A =_{β} B : K}{Γ ⊢ A ≤ B : K}  (S-Conv)

The Subtyping rules also appear in Appendix A. Our goal is to prove that this relation is Anti-Symmetric.

The term formation rules are standard. We remind the reader that the subtyping relation on ⋆ induces an inclusion over types.

\frac{Γ ⊢ M : A  Γ ⊢ A ≤ B : ⋆}{Γ ⊢ M : B}  (t-Sub)

3 The Typed Operational Semantics

The typed operational semantics for F_{≤}^{ω} is organized in five judgement forms:

Γ ⊢_{S} ok  well-formed context
Γ ⊢_{S} K ↠_{n} K′  kind normalization
Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K type reduction
Γ ⊢_{S} A ≤_{W} B : K  weak-head subtyping
Γ ⊢_{S} A ≤ B : K  subtyping.

This system can be understood informally as a particularly informative algorithm for kinding and subtyping in F_{≤}^{ω}. The first judgement simply represents well-formed contexts. The second and third judgements represent normalization of kinds and types, where the formulation of the rules of inference ensures strong normalization, Church–Rosser and other good metatheoretic properties. The last two judgements represent an algorithm for subtyping that first reduces the left and right-hand sides to weak-head normal forms and then compares these.

For technical reasons relating to the model construction, we need to consider a slightly stronger notion of weak-head normal form.

Definition 3.1 (Weak-Head Normal) T_{⋆}, A_{1}→A_{2}, ∀X≤A:K.B, and ΛX≤A:K.B are weak-head normal. X(A_{1}, …, A_{m}) is weak-head normal if A_{1}, …, A_{m} are in normal form.

We use various notations that omit unnecessary components of the judgement. For example, we write Γ ⊢_{S} K for Γ ⊢_{S} K ↠_{n} K′ for some K′, and similarly for types, Γ ⊢_{S} A ↠_{w} B : K for Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K for some C, and Γ ⊢_{S} A _{w}↠_{n} B : K for Γ ⊢_{S} A ↠_{w} A ↠_{n} B : K. We also write Γ ⊢_{S} K, K′ ↠_{n} K′′ when Γ ⊢_{S} K ↠_{n} K′′ and Γ ⊢_{S} K′ ↠_{n} K′′, and similarly for types.

We now present the rules of inference. The context formation and kind normalization rules are modifications of the corresponding rules for F_{≤}^{ω}. The rules for type reduction combine kinding information and computational behavior in the form of weak-head and β-normal forms. For example, the rule for arrow types says how to obtain the weak-head and β-normal forms of (A_{1}→A_{2}) in ⋆ from those for A_{1} and A_{2} in ⋆.

\frac{Γ ⊢_{S} K_{1} ↠_{n} K′_{1}  Γ ⊢_{S} A ↠_{n} B : K′_{1} Γ, X≤A : K_{1} ⊢_{S} K_{2} ↠_{n} K′_{2}}{Γ ⊢_{S} ΠX≤A:K_{1}.K_{2} ↠_{n} ΠX≤B:K′_{1}.K′_{2}}  (SK-Π)

If A is of the form X(B_{1}, …, B_{n}) then A has head variable X. We write HV(—) for the partial function returning the head variable of a term. We also extend the top type T_{⋆} to any kind K by defining inductively T_{ΠX≤A:K_{1}.K_{2}} = ΛX≤A:K_{1}.T_{K_{2}}. The rules for Type Reduction are in Appendix B.

The beta rule, besides uncovering the outermost redex of the application B C and contracting it, finds the weak-head normal form E and the normal form F. The premise Γ ⊢_{S} K_{2}[X←C] ↠_{w} K ensures that E and F have β-equal kinds, and the subtyping premise Γ ⊢_{S} C ≤ A : K_{1}′ enforces the well-formation of B C.

\frac{Γ ⊢_{S} B ↠_{w} ΛX≤A:K_{1}.D : ΠX≤A′:K′_{1}.K_{2} Γ ⊢_{S} D[X←C] ↠_{w} E _{w}↠_{n} F : K Γ ⊢_{S} K_{2}[X←C] ↠_{n} K  Γ ⊢_{S} C ≤ A : K′_{1}}{Γ ⊢_{S} B C ↠_{w} E _{w}↠_{n} F : K}  (ST-Beta)

The weak-head subtyping rules are motivated by the algorithmic rules in [16]. The rules SWS-Arrow, SWS-All, and SWS-TAbs are structural. The rule SWS-TApp implicitly uses transitivity, reducing the problem of a variable being less than another type to the problem of the bound of the variable being less than that type. The side condition ensures determinism. The rules for weak-head subtyping are in Appendix B.

Finally, full subtyping is defined by reference to the weak-head subtyping relation.

\frac{Γ ⊢_{S} A ↠_{w} C : K Γ ⊢_{S} B ↠_{w} D : K Γ ⊢_{S} C ≤_{W} D : K}{Γ ⊢_{S} A ≤ B : K}  (SS-Inc)

4 Anti-Symmetry

Our goal is to prove the following result:

If Γ ⊢ A ≤ B : K and Γ ⊢ B ≤ A : K then Γ ⊢ A =_{β} B : K.

We obtain it as a consequence of the corresponding property in the typed operational semantics using Soundness (Theorem 5.7) and Completeness (Proposition 5.6). In the semantics, the way to say that two types are equal is that they have the same normal form.

Proposition 4.1 (Anti-Symmetry of TOS)

1. If Γ ⊢_{S} A ≤ B : K and Γ ⊢_{S} B ≤ A : K then Γ ⊢_{S} A, B ↠_{n} C : K.

2. If Γ ⊢_{S} A ≤_{W} B : K and Γ ⊢_{S} B ≤_{W} A : K then Γ ⊢_{S} A, B ↠_{n} C : K.

The proof of Proposition 4.1 follows by simultaneous induction on derivations. The main difficulty appears when A is of the form X(A_{1}, …, A_{m}). Intuitively, in this case B can only be X(A_{1}, …, A_{m}). To discard the possibility that B could be other than A, we need to prove that

Γ ⊢_{S} Γ(X)(A_{1}, …, A_{m}) ≤ X(A_{1}, …, A_{m}) : K is impossible.

Observe that the base case is: Γ ⊢_{S} Γ(X) ≤ X : K is impossible, which can be read as: the bound of X cannot be a subtype of X. The complication in the general case is that X may appear in some A_{i}. So it is not obvious that Γ(X)(A_{1}, …, A_{m}) may not β-reduce to X(A_{1}, …, A_{m}), for example. This negative result, Lemma 4.7, although intuitive and believable, is the challenge of our development. The definitions and results that follow are used in its proof.

Remember that the typed operational semantics is deterministic (Lemma 5.3): therefore there is only one derivation for each judgement, and we can invert the rules deriving premises from conclusions. We sometimes use this fact without mentioning it.

Intuitively, the next lemma says that if A has normal form B then A C and B C have the same normal form.

Lemma 4.2 If Γ ⊢_{S} A ↠_{n} B : ΠX≤E:K_{1}.K_{2} and Γ ⊢_{S} C ≤ E : K_{1} and Γ ⊢_{S} K_{2}[X←C] ↠_{n} K′_{2}. Then Γ ⊢_{S} A C ↠_{n} F : K′_{2} and Γ ⊢_{S} B C ↠_{n} F : K′_{2}.

Proof: By Completeness, Γ ⊢ A C =_{β} B C : K_{2}[X←C], Γ ⊢ C : K_{1}, Γ ⊢ C ≤ E : K_{1} and Γ ⊢ K_{2}[X←C] =_{β} K′_{2}. By T-Eq-Refl Γ ⊢ C =_{β} C : K_{1}. Then, by T-Eq-TApp Γ ⊢ A C =_{β} B C : K_{2}[X←C]. Finally, by Soundness, Γ ⊢_{S} A C ↠_{n} F : K′_{2} and Γ ⊢_{S} B C ↠_{n} F : K′_{2}. □

A consequence of this lemma is that there exists B such that Γ ⊢_{S} Γ(X)(A_{1}, …, A_{m}) ↠_{n} B : K and Γ ⊢_{S} Γ(X)nf(A_{1}, …, A_{m}) ↠_{n} B : K, where Γ ⊢_{S} Γ(X) ↠_{n} Γ(X)nf : K′, for some K′.

4.1 An impossible judgement

In this section we show that the judgement Γ ⊢_{S} Γ(X)(A_{1} … A_{m}) ≤ X(A_{1} … A_{m}) : K is underivable.

We introduce a function from derivations in the typed operational semantics to numbers, informally capturing the number of uses of the rule of inference that a variable is less than its bound. We do not have a good notation for defining a function on derivations because such definitions do not occur commonly in the literature. We therefore use the following abbreviations in our definition of the length function:

• Γ(X) for the subderivation of the bound of X in Γ for the case ST-TVar,

• Γ(X)nf(A_{1}, …, A_{m}) for the subderivation of the normal form of the bound applied to the arguments of X for the case ST-TApp, and

• β for a derivation of B C using ST-Beta and reduct for the subderivation of the β-reduct of B C.

Definition 4.3 We define ♯(−), from derivations of Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K to numbers, by induction on derivations:

ST-Top  ♯(T_{⋆}) = 0
ST-TVar ♯(X) = ♯(Γ(X)) + 1
ST-TApp ♯(X(A_{1}, …, A_{m})) = ♯(Γ(X)nf(A_{1}, …, A_{m})) + 1
ST-Arrow ♯(A_{1}→A_{2}) = 0
ST-All  ♯(∀X≤A_{1}:K.A_{2}) = 0
ST-TAbs ♯(ΛX≤A_{1}:K.A_{2}) = 0
ST-Beta ♯(β) = ♯(reduct)

We now show that this length function is invariant with respect to well-formed types or type-operators that have the same normal form. This lemma justifies our later informality in writing types or typeoperators in place of their derivations of well-formedness.

Lemma 4.4 If D is a derivation of Γ ⊢_{S} A ↠_{w} C _{w}↠_{n} E : K and D′ is a derivation of Γ ⊢_{S} B ↠_{w} D _{w}↠_{n} E : K then ♯(D) = ♯(D′).

Proof: By induction on derivations D.

In each case where E is a type constructor or a variable, we perform a nested induction on D′, and there are two interesting cases. The first is when the nested case is the same rule as for the outermost induction. In this case the lengths are equal by assumption for rules ST-Top, ST-Arrow, ST-All and ST-TAbs. For ST-TVar and ST-TApp, we know Γ(X) is a function, so the result follows by Determinacy and the induction hypothesis. In the case ST-TApp we have that Γ ⊢_{S} A′_{1} A′_{2} ↠_{w} X(A_{1}, …, A_{m}, F) w↠_{n} X(A_{1}, …, A_{m}, F) : K and Γ ⊢_{S} B_{1} B_{2} ↠_{w} X(A_{1}, …, A_{m}, F) _{w}↠_{n} X(A_{1}, …, A_{m}, F) : K. Then D and D′ have the same subderivation Γ ⊢_{S} D(A_{1}, …, A_{m}, F) : K. Hence, by the definition of ♯(−), ♯(D) = ♯(D(A_{1}, …, A_{m})) + 1 = ♯(D′).

The second interesting case in the nested inductions is ST-Beta, where the result follows by the induction hypothesis. All of the other nested cases contradict the assumption that the normal forms are the same.

The final outermost case is ST-Beta, which follows by the induction hypothesis. □ Then, if Γ ⊢_{S} X(A_{1}, …, A_{m}) : K we have

♯(X(A_{1}, …, A_{m})) = ♯(Γ(X)nf(A_{1}, …, A_{m})) + 1
= ♯(Γ(X)(A_{1}, …, A_{m})) + 1
> ♯(Γ(X)(A_{1}, …, A_{m})),

where, by Lemma 4.2, there is a B such that Γ ⊢_{S} Γ(X)nf(A_{1}, …, A_{m}) ↠_{n} B : K and Γ ⊢_{S} Γ(X)(A_{1}, …, A_{m}) ↠_{n} B : K, and by Lemma 4.4, they have the same length.

Our final preparation is a simple lemma saying that ♯(−) is well-defined on the subjects of a subtyping statement:

Lemma 4.5 If Γ ⊢_{S} A ≤ B : K then ♯(A) and ♯(B) are well-defined.

Proof: By Lemma 5.9, if Γ ⊢_{S} A ≤ B : K then Γ ⊢_{S} A : K and Γ ⊢_{S} B : K. Hence ♯(A) and ♯(B) are defined. □

Now, we come to the main lemma about ♯(A):

Lemma 4.6

1. If Γ ⊢_{S} A ≤ B : K then ♯(A) ≥ ♯(B).

2. If Γ ⊢_{S} A ≤_{W} B : K then ♯(A) ≥ ♯(B).

Proof: By induction on derivations that Γ ⊢_{S} A ≤ B : K:

1. The only possible rule for Γ ⊢_{S} A ≤ B : K is SS-Inc, which follows by Determinacy, Lemma 4.4, and the induction hypothesis.

2. SWS-Top Then ♯(A) ≥ 0 = ♯(T_{⋆}) by definition of ≥.

SWS-TApp By the induction hypothesis ♯(E) ≥ ♯(A), so ♯(X((A_{1}, …, A_{m})) = ♯(Γ(X)nf(A_{1}, …, A_{m}))+ 1 = ♯(E) + 1 > ♯(E) ≥ ♯(A) where we know that ♯(Γ(X)nf(A_{1}, …, A_{m})) = ♯(E) by Determinacy.

SWS-Refl Then ♯(X(A_{1}, …, A_{m})) ≥ ♯(X(A_{1}, …, A_{m})).
SWS-Arrow Then ♯(A_{1}→A_{2}) = 0 ≥ 0 = ♯(B_{1}→B_{2}).
SWS-All Then ♯(∀X≤A_{1}:K.A_{2}) = 0 ≥ 0 = ♯(∀X≤B_{1}:K′.B_{2}).

SWS-TAbs Then ♯(ΛX≤A_{1}:K_{1}.A_{2}) = 0 ≥ 0 = ♯(ΛX≤B_{1}:K′_{1}.B_{2}). □

Lemma 4.7 There can be no derivation of Γ ⊢_{S} Γ(X)(A_{1}, …, A_{m}) ≤ X(A_{1}, …, A_{m}) : K.

Proof: Suppose that there were a derivation of Γ ⊢_{S} Γ(X)(A_{1}, …, A_{m}) ≤ X(A_{1}, …, A_{m}) : K. By Lemma 4.6 we would have ♯(Γ(X)(A_{1}, …, A_{m})) ≥ ♯(X(A_{1}, …, A_{m})), contradicting the fact that ♯(X(A_{1}, …, A_{m})) > ♯(Γ(X)(A_{1}, …, A_{m})). □

4.2 Anti-Symmetry

Before proving our main result we establish some auxiliary lemmas.

This lemma says that a type variable applied to a list of arguments has the same kind as its bound applied to the same list. It also says that if a type variable applied to a list of arguments is a subtype of (but not equal to) a given type, then its bound applied to the same list is also a subtype of that given type.

Lemma 4.8 (Upper Bound)

1. If Γ ⊢_{S} X(A_{1}, …, A_{m}) : K then Γ ⊢_{S} Γ(X)(A_{1}, …, A_{m}) : K.

2. If Γ ⊢_{S} X(A_{1}, …, A_{m}) ≤ B : K and B ≢ X(A_{1}, …, A_{m}) then Γ ⊢_{S} Γ(X)(A_{1}, …, A_{m}) ≤ B : K.

3. If Γ ⊢_{S} X(A_{1}, …, A_{m}) ≤_{W} B : K and B ≢ X(A_{1}, …, A_{m}) then Γ ⊢_{S} Γ(X)(A_{1}, …, A_{m}) ≤ B : K.

Proof: Cases 2 and 3 follow by simultaneous induction on derivations.

1. By Soundness and Completeness from Lemma 5.8, because Γ ⊢_{S} K ↠_{n} K.

2. The only rule to derive the assumption is SS-Inc. By Determinism, the premises are Γ ⊢_{S} B ↠_{w} D _{w}↠_{n} E : K, Γ ⊢_{S} X(A_{1}, …, A_{m}) ↠_{w} C : K and Γ ⊢_{S} C ≤_{W} D. By inversion of ST-TApp, C ≡ X(A′_{1}, …, A′_{m}), where Γ ⊢_{S} A_{i} ↠_{n} A′_{i} : K_{i} for some K_{i} and i ∈ {1..m}. By Adequacy, A_{i} ↠_{β} A′_{i}, and by definition of β-reduction Γ(X)(A_{1}, …, A_{m}) ↠_{β} Γ(X)(A′_{1}, …, A′_{m}). By Upper Bound, Γ ⊢_{S} Γ(X)(A_{1}, …, A_{m}) ↠_{n} F : K, By Subject Reduction, Γ ⊢_{S} Γ(X)(A′_{1}, …, A′_{m}) ↠_{n} F : K, By the induction hypothesis, Γ ⊢_{S} Γ(X)(A′_{1}, …, A′_{m}) ≤_{W} D : K. By Lemma 4.9, Γ ⊢_{S} D ↠_{w} D _{w}↠_{n} E : K and, by Subtyping Conversion, Γ ⊢_{S} Γ(X)(A′_{1}, …, A′_{m}) ≤_{W} B : K and then Γ ⊢_{S} Γ(X)(A_{1}, …, A_{m}) ≤_{W} B : K.

3. There are only two rules to derive Γ ⊢_{S} X(A_{1}, …, A_{m}) ≤_{W} B : K. Case SWS-Top follows by Case 1 and SWS-Top. Case SWS-TApp By Adequacy, Γ(X) ↠_{β} D and D(A_{1}, …, A_{m}) ↠_{β} E, and by definition of β-reduction, Γ(X)(A_{1}, …, A_{m}) ↠_{β} E. By Case 1, Γ ⊢_{S} Γ(X)(A_{1}, …, A_{m}) ↠_{n} C : K, and Γ ⊢_{S} E, ↠_{n} C : K, by Subject Reduction. Γ ⊢_{S} E ≤_{W} B : K is a premise, from which the result follows by Subtyping Conversion. □

Lemma 4.9 1. If Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K then Γ ⊢_{S} B ↠_{w} B _{w}↠_{n} C : K and Γ ⊢_{S} C ↠_{w} C _{w}↠_{n} C : K.

2. If Γ ⊢_{S} K ↠_{n} K′ then Γ ⊢_{S} K′ ↠_{n} K′.

Proof: By simultaneous induction on derivations. Most cases are immediate, some follow directly by the induction hypothesis, as ST-Beta. The interesting case is ST-TApp in Case 1 and Case 2. By the induction hypothesis Case 1 and Case 2, Γ ⊢_{S} X(A_{1}, …, A_{m}) ↠_{w} X(A_{1}, …, A_{m}) : ΠX≤C:K_{1}.K_{2}, Γ ⊢_{S} E ↠_{w} E _{w}↠_{n} F : K_{1} and Γ ⊢_{S} F ↠_{w} F _{w}↠_{n} F : K_{1}. By Subtyping Conversion (Lemma 5.5), Γ ⊢_{S} F ≤_{W} C : K_{1}. Then, Γ ⊢_{S} X(A_{1}, …, A_{m}, F) ↠_{w} X(A_{1}, …, A_{m}, F) _{w}↠_{n} X(A_{1}, …, A_{m}, F) : K, by ST-TApp. □

We can now prove our main result. Proof of Proposition 4.1 Anti-Symmetry of TOS. The argument is by simultaneous induction on derivations.

1. The only rule to derive both assumptions is SS-Inc. By Determinacy, the premises are Γ ⊢_{S} A ↠_{w} C _{w}↠_{n} E : K, Γ ⊢_{S} B ↠_{w} D _{w}↠_{n} F : K, Γ ⊢_{S} C ≤_{W} D : K, and Γ ⊢_{S} D ≤_{W} C : K. By Lemma 4.9, Γ ⊢_{S} C ↠_{w} C _{w}↠_{n} E : K, Γ ⊢_{S} D ↠_{w} D _{w}↠_{n} F : K. By the induction hypothesis, Γ ⊢_{S} C _{w}↠_{n} G : K, Γ ⊢_{S} D _{w}↠_{n} G : K. Finally, by Determinacy, E ≡ F ≡ G.

2. The proof is by induction on the derivation of Γ ⊢_{S} A ≤_{W} B : K.

SWS-Top Then B ≡ T_{⋆}, and HV(A) undefined, which means that A is not a type application or a type variable. Therefore the only rule to derive Γ ⊢_{S} T_{⋆} ≤_{W} A : K is SWS-Top, which means that A ≡ T_{⋆}. By Lemma 5.9 and Determinacy, Γ ⊢_{S} T_{⋆} ↠_{w} T_{⋆} _{w}↠_{n} T_{⋆} : ⋆.

SWS-TApp We are going to show that this case is not possible. Assume that it is. We have that A ≡ X(A_{1}, …, A_{m}) and B ≢ X(A_{1}, …, A_{m}). By Upper Bound Lemma 4.8, Γ ⊢_{S} Γ(X)(A_{1}, …, A_{m}) ≤ B : K, and by transitivity Γ ⊢_{S} Γ(X)(A_{1}, …, A_{m}) ≤ X(A_{1}, …, A_{m}) : K, which is a contradiction, by Lemma 4.7.

SWS-Refl By the premise.

SWS-Arrow The only rule to derive Γ ⊢_{S} B ≤_{W} A : K is also SWS-Arrow, then, by the induction hypothesis and ST-Arrow, the result follows.

SWS-All The only rule to derive Γ ⊢_{S} B ≤_{W} A : K is also SWS-All. The premises are, Γ, X≤A_{1}:K ⊢_{S} A_{2} ≤ B_{2} : ⋆, Γ, X≤B_{1}:K′ ⊢_{S} B_{2} ≤ A_{2} : ⋆, Γ ⊢_{S} A_{1}, B_{1} ↠_{n} C_{1} : K′′, and Γ ⊢_{S} K, K′ ↠_{n} K′′. By Context Conversion Lemma 5.2, Γ, X≤A_{1}:K ⊢_{S} B_{2} ≤ A_{2} : ⋆. We can now apply the induction hypothesis to obtain, Γ, X≤A_{1}:K ⊢_{S} A_{2}, B_{2} ↠_{n} C_{2} : ⋆. Finally, Γ ⊢_{S} (∀X≤A_{1}:K.A_{2}), (∀X≤B_{1}:K′.B_{2}) ↠_{n} ∀X≤C_{1}:K′′.C_{2} : ⋆, by ST-All.

SWS-TAbs Similar to case SWS-All. □

Proposition 4.10 (Anti-Symmetry) If Γ ⊢ A ≤ B : K and Γ ⊢ B ≤ A : K then Γ ⊢ A =_{β} B : K.

Proof: By Soundness (Theorem 5.7), Γ ⊢_{S} A ≤ B : K′, Γ ⊢_{S} B ≤ A : K′, and Γ ⊢_{S} K ↠_{n} K′. By Proposition 4.1, Γ ⊢_{S} A, B ↠_{n} C : K′. By Completeness and symmetry of kind equality Γ ⊢ K′ =_{β} K. By Completeness Γ ⊢ A =_{β} C : K′ and Γ ⊢ B =_{β} C : K′ Finally, by T-Eq-Sym, T-Eq-Trans, and S-K-Conv, Γ ⊢ A =_{β} B : K. □

5 Results from [15]

Lemma 5.1 (Adequacy)

• If Γ ⊢_{S} K ↠_{n} K′ then K ↠_{β} K′.

• If Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K then A ↠_{β} B ↠_{β} C.

Lemma 5.2 (Context Conversion) If Γ ⊢_{S} K ↠_{n} K′ and Γ ⊢_{S} A ↠_{n} A′ : K′ and Γ, X≤A:K ⊢_{S} J then Γ, X≤A′:K′ ⊢_{S} J.

Lemma 5.3 (Determinacy)

1. If Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K and Γ ⊢_{S} A ↠_{w} D _{w}↠_{n} E : K′ then B ≡ D, C ≡ E and K ≡ K′.

2. If Γ ⊢_{S} K ↠_{n} K′ and Γ ⊢_{S} K ↠_{n} K′′ then K′ ≡ K′′.

Lemma 5.4 (Subject Reduction) Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K and A →_{β} A′ imply there is a B′ such that B ↠_{β} B′ and Γ ⊢_{S} A′ ↠_{w} B′ _{w}↠_{n} C : K. Lemma 5.5 (Subtyping Conversion) Suppose that Γ ⊢_{S} A ≤_{W} B : K. Then:

• If Γ ⊢_{S} A, A′ _{w}↠_{n} C : K then Γ ⊢_{S} A′ ≤_{W} B : K.

• If Γ ⊢_{S} B, B′ _{w}↠_{n} C : K then Γ ⊢_{S} A ≤_{W} B′ : K. Similarly for Γ ⊢_{S} A ≤ B : K. Proposition 5.6 (Completeness)

1. Γ ⊢_{S} K ↠_{n} K′ implies Γ ⊢ K and Γ ⊢ K =_{β} K′.

2. Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K implies Γ ⊢ A : K, Γ ⊢ A =_{β} B : K and Γ ⊢ A =_{β} C : K.

3. Γ ⊢_{S} A ≤_{W} B : K implies Γ ⊢ A ≤ B : K.

4. Γ ⊢_{S} A ≤ B : K implies Γ ⊢ A, B : K and Γ ⊢ A ≤ B : K. Theorem 5.7 (Soundness)

1. If Γ ⊢ K then there is a K′ such that Γ ⊢_{S} K ↠_{n} K′; if Γ ⊢ K =_{β} K′ then there is a K′′ such that Γ ⊢_{S} K ↠_{n} K′′ and Γ ⊢_{S} K′ ↠_{n} K′′.

2. If Γ ⊢ A : K then there are K′, B and C such that Γ ⊢_{S} K ↠_{n} K′ and Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K′; if Γ ⊢ A =_{β} B : K then there are C and K′ such that Γ ⊢_{S} K ↠_{n} K′, Γ ⊢_{S} A ↠_{n} C : K′ and Γ ⊢_{S} B ↠_{n} C : K′.

3. If Γ ⊢ A ≤ B : K then there is a K′ such that Γ ⊢_{S} K ↠_{n} K′ and Γ ⊢_{S} A ≤ B : K′. Lemma 5.8 (Upper Bound) If Γ ⊢ X(A_{1}, …, A_{m}) : K then Γ ⊢ Γ(X)(A_{1}, …, A_{m}) : K. Lemma 5.9 If Γ ⊢_{S} A ≤ B : K then Γ ⊢_{S} A : K and Γ ⊢_{S} B : K.

6 Replacing Equality with Subtyping

In this section we sketch a presentation of F_{≤}^{ω} without judgemental equality or conversion. This leads to simplifications in the proof of soundness for models of the system, because we remove equality and all of the rules of inference that rely on it.

We shall write Γ ⊢_{A} J for judgements derived in the system without an equality judgement, and Γ ⊢_{A} A ≶ B : K if Γ ⊢_{A} A ≤ B : K and Γ ⊢_{A} B ≤ A : K.

6.1 Modifications to Inference Rules

The system requires several changes in order to accommodate the removal of equality. First, the inclusion of the equality relation in subtyping, and in particular reflexivity and the rule for β-equality, needs to be recovered in the rules for subtyping itself:

\frac{Γ ⊢_{A} A : K}{Γ ⊢_{A} A ≤ A : K}  (SE-Refl)

\frac{\begin{matrix}Γ, X≤A_{1}:K_{1} ⊢_{A} A_{2} : K_{2}  Γ ⊢_{A} C ≤ A_{1} : K_{1} \\ Γ ⊢_{A} A_{2}[X←C] ≤ D : K_{2}[X←C] \end{matrix}}{Γ ⊢_{A} (ΛX≤A_{1}:K_{1}.A_{2}) C ≤ D : K_{2}[X←C]}  (SE-BetaL)

\frac{\begin{matrix}Γ, X≤A_{1}:K_{1} ⊢_{A} A_{2} : K_{2}  Γ ⊢_{A} C ≤ A_{1} : K_{1} \\ Γ ⊢_{A} D ≤ A_{2}[X←C] : K_{2}[X←C] \end{matrix}}{Γ ⊢_{A} D ≤ (ΛX≤A_{1}:K_{1}.A_{2}) C : K_{2}[X←C]}  (SE-BetaR)

Next, the rule for subtyping applications does not allow the argument to vary. This restriction is for a good reason: allowing subtyping in the argument is unsound. However, we need to recapture the behavior of equality in allowing equal types on the right-hand side of an application:

\frac{Γ ⊢_{A} A ≤ B : ΠX≤E:K_{1}.K_{2}  Γ ⊢_{A} C ≶ D : K_{1} Γ ⊢_{A} C ≤ E : K_{1}  Γ ⊢_{A} D ≤ E : K_{1}}{Γ ⊢_{A} A C ≤ B D : K_{2}[X←C]}  (SE-TApp)

Finally, we still need an equivalence relation on kinds in order to allow the kinded judgements to vary with respect to equal kinds. We simply lift the equivalence induced by subtyping to kinds:

\frac{Γ ⊢_{A} ok}{Γ ⊢_{A} ⋆ ≶ ⋆}  (KE-Type)

\frac{\begin{matrix}Γ ⊢_{A} K_{1} ≶ K′_{1}  Γ ⊢_{A} A ≶ B : K_{1} \\ Γ, X ≤ A:K_{1} ⊢_{A} K_{2} ≶ K′_{2} \end{matrix}}{Γ ⊢_{A} ΠX≤A:K_{1}.K_{2} ≶ ΠX≤B:K′_{1}.K′_{2}}  (KE-Π)

6.2 Changes to Metatheory

We can now show several basic results relating the old presentation with judgemental equality and the new one without it.

First, we can show that equality can be captured by the equivalence relation induced by subtyping.

Definition 6.1 Let Γ ⊢_{A} A = B : K be defined using the same rules of inference as judgemental equality for Γ ⊢ A = B : K, but replacing uses of Γ ⊢ A : K, Γ ⊢ A ≤ B : K, and so on by their corresponding judgement Γ ⊢_{A} A : K, Γ ⊢_{A} A ≤ B : K and so on.

Lemma 6.2 If Γ ⊢_{A} A = B : K then Γ ⊢_{A} A ≶ B : K.

Proof: By a simple induction on derivations.

This lemma, plus some minor modifications to the original proof, lead to a proof of Completeness of the typed operational semantics with respect to the new system Γ ⊢_{A} J.

Proposition 6.3 (Completeness)

1. Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K implies Γ ⊢_{A} A : K, Γ ⊢_{A} A =_{β} B : K and Γ ⊢_{A} A =_{β} C : K.

2. Γ ⊢_{S} A ≤ B : K implies Γ ⊢_{A} A, B : K and Γ ⊢_{A} A ≤ B : K.

We now consider Soundness for Γ ⊢_{A} J.

Theorem 6.4 (Soundness)

1. If Γ ⊢_{A} A : K then there are K′, B and C such that Γ ⊢_{S} K ↠_{n} K′ and Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K′.

2. If Γ ⊢_{A} A =_{β} B : K then there are C and K′ such that Γ ⊢_{S} K ↠_{n} K′, Γ ⊢_{S} A ↠_{n} C : K′ and Γ ⊢_{S} B ↠_{n} C : K′.

3. If Γ ⊢_{A} A ≤ B : K then there is a K′ such that Γ ⊢_{S} K ↠_{n} K′ and Γ ⊢_{S} A ≤ B : K′.

7 Conclusions

We have solved a long-standing open problem, giving a general approach to showing the anti-symmetry of higher-order subtyping. To our knowledge, this is the first proof of anti-symmetry for higher-order subtyping: even for systems like F_{<:}^{ω} the result was unknown. We have also showed this result for the subtyping relation of F_{≤}^{ω}, a higher-order lambda calculus with bounded operator abstraction.

This result has several consequences for the metatheory of type systems with subtyping. First, it implies that we can now prove the Minimum Types Property, as opposed to the Minimal Types Property which is normally proved. We can now say what is the relation between all the minimal types of a given term; before we knew that any two minimal types were subtypes of each other, we can now say that they are β-equal. Secondly, we can simplify the basic judgements of type systems with subtyping by eliminating either judgemental equality or conversion.

Acknowledgments

We would like to thank Benjamin Pierce and Juliusz Chroboczek for interesting discussions about type equality and anti-symmetry, and Giorgio Ghelli for the reference about anti-symmetry for F_{≤}.

References

[1] M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag, 1996.

[2] R. M. Amadio and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, 1993.

[3] D. Aspinall and A. Compagnoni. Subtyping dependent types. To appear in Theoretical Computer Science, July 1995.

[4] H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940, 1983.

[5] V. Breazu-Tannen, T. Coquand, C. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and Computation, 93:172–221, 1991.

[6] K. B. Bruce. Typing in object-oriented languages: Achieving expressiveness and safety. Unpublished, June 1996.

[7] K. B. Bruce and G. Longo. A modest model of records, inheritance, and bounded quantification. Information and Computation, 87:196–240, 1990.

[8] L. Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988.

[9] L. Cardelli. Notes about F_{<:}^{ω}. Unpublished manuscript, Oct. 1990.

[10] L. Cardelli and G. Longo. A semantic basis for Quest. Journal of Functional Programming, 1(4):417–458, Oct. 1991.

[11] L. Cardelli and J. Mitchell. Operations on records. Mathematical Structures in Computer Science, 1:3–48, 1991. Also in [22], and available as DEC Systems Research Center Research Report #48, August, 1989, and in the proceedings of MFPS ’89, Springer LNCS volume 442.

[12] L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4), Dec. 1985.

[13] J. Chroboczek. Forthcomming Thesis. PhD thesis, University of Edinburgh. Supervisor: Prof. S. Abramsky.

[14] A. Compagnoni and H. Goguen. Decidability of higher-order subtyping via logical relations, Dec. 1997.

[15] A. Compagnoni and H. Goguen. Typed operational semantics for higher order subtyping, Dec. 1997. Available

at http://www.dcs.ed.ac.uk/home/abc/toshos.dvi.gz. Submitted to Information and Computation.

[16] A. B. Compagnoni. Higher-Order Subtyping with Intersection Types. PhD thesis, University of Nijmegen, The Netherlands, Jan. 1995. Supervisor: Prof. Barendregt. ISBN 90-9007860-6.

[17] A. B. Compagnoni and B. C. Pierce. Higher-order intersection types and multiple inheritance. Mathematical Structures in Computer Science, 6:469–501, 1996.

[18] M. Coppo and M. Dezani-Ciancaglini. A new type-assignment for λ-terms. Archiv. Math. Logik, 19:139–156, 1978.

[19] P.-L. Curien and G. Ghelli. Subtyping + extensionality: Confluence of βη-reductions in F_{≤}. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software (Sendai, Japan), number 526 in Lecture Notes in Computer Science, pages 731–749. Springer-Verlag, Sept. 1991.

[20] P.-L. Curien and G. Ghelli. Coherence of subsumption: Minimum typing and type-checking in F_{≤}. Mathematical Structures in Computer Science, 2:55–91, 1992.

[21] D. Duggan and A. Compagnoni. Subtyping for object type constructors. In Foundations of Object-Oriented Languages (FOOL 6). 1999. To appear.

[22] C. A. Gunter and J. C. Mitchell. Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. The MIT Press, 1994.

[23] M. Hofmann and B. Pierce. Positive subtyping. Information and Computation, 126(1), 1996.

[24] A. Jones, Z. Luo, and S. Soloviev. Some algorithmic and proof-theoretical aspects of coercive subtyping. In Proceedings of TYPES’96, Lecture Notes in Computer Science, 1996.

[25] J. C. Mitchell. Toward a typed foundation for method specialization and inheritance. In Proceedings of the 17th ACM Symposium on Principles of Programming Languages, pages 109–124, Jan. 1990.

[26] J. C. Mitchell, F. Honsell, and K. Fisher. A lambda calculus of objects and method specialization. In 1993 IEEE Symposium on Logic in Computer Science, June 1993.

[27] F. Pfenning. Refinement types for logical frameworks. In Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, pages 315–328, May 1993.

[28] B. C. Pierce. Bounded quantification is undecidable. Information and Computation, 1993.

[29] B. C. Pierce. Bounded quantification with bottom. Technical Report 492, Computer Science Department, Indiana University, 1997.

[30] M. Steffen. Polarized Higher-Order Subtyping. PhD thesis, Lehrstuhl für Informatik VII, Friedrich Alexander Universität Erlangen-Nürnberg, 1998.

[31] M. Steffen and B. Pierce. Higher-order subtyping. Theoretical Computer Science, 176(1–2):235–282, 1997. corrigendum in TCS vol. 184 (1997), p. 247.

[32] J. Zwanenburg. Forthcomming Thesis. PhD thesis, Eindhoven University of Technology. Supervisor: Prof. Hemerik.

A Rules for F_{≤}^{ω}

Equality Rules

\frac{Γ, X≤A_{1}:K_{1} ⊢ A_{2} : K_{2}  Γ ⊢ C ≤ A_{1} : K_{1}}{Γ ⊢ (ΛX≤A_{1}:K_{1}.A_{2}) C =_{β} A_{2}[X←C] : K_{2}[X←C]}  (T-Eq-Beta)
\frac{Γ ⊢ A : K}{Γ ⊢ A =_{β} A : K}  (T-Eq-Refl)
\frac{Γ ⊢ A =_{β} B : K}{Γ ⊢ B =_{β} A : K}  (T-Eq-Sym)
\frac{Γ ⊢ A =_{β} B : K  Γ ⊢ B =_{β} C : K}{Γ ⊢ A =_{β} C : K}  (T-Eq-Trans)
\frac{Γ ⊢ A_{1} =_{β} B_{1} : ⋆  Γ ⊢ A_{2} =_{β} B_{2} : ⋆}{Γ ⊢ A_{1}→A_{2} =_{β} B_{1}→B_{2} : ⋆}  (T-Eq-Arr)

\frac{\begin{matrix}Γ ⊢ A_{1} =_{β} B_{1} : K \\ Γ, X≤A_{1}:K ⊢ A_{2} =_{β} B_{2} : ⋆ \\ Γ ⊢ K =_{β} K′ \end{matrix}}{Γ ⊢ ∀X≤A_{1}:K.A_{2} =_{β} ∀X≤B_{1}:K′.B_{2} : ⋆}  (T-Eq-All)

\frac{\begin{matrix}Γ ⊢ A_{1} =_{β} B_{1} : K_{1} \\ Γ, X≤A_{1}:K_{1} ⊢ A_{2} =_{β} B_{2} : K_{2} \\ Γ ⊢ K_{1} =_{β} K′_{1} \end{matrix}}{Γ ⊢ ΛX≤A_{1}:K_{1}.A_{2} =_{β} ΛX≤B_{1}:K′_{1}.B_{2} : ΠX≤A_{1}:K_{1}.K_{2}}  (T-Eq-TAbs)

\frac{\begin{matrix}Γ ⊢ A =_{β} B : ΠX≤E:K_{1}.K_{2} \\ Γ ⊢ C =_{β} D : K_{1} \\ Γ ⊢ C ≤ E : K_{1} \end{matrix}}{Γ ⊢ A C =_{β} B D : K_{2}[X←C]}  (T-Eq-TApp)
\frac{Γ ⊢ A =_{β} B : K  Γ ⊢ K =_{β} K′}{Γ ⊢ A =_{β} B : K′}  (T-Eq-Conv)

Subtyping Rules

\frac{Γ ⊢ A : K}{Γ ⊢ A ≤ T_{K} : K}  (S-Top)
\frac{Γ ⊢ A =_{β} B : K}{Γ ⊢ A ≤ B : K}  (S-Conv)
\frac{Γ ⊢ A ≤ B : K  Γ ⊢ B ≤ C : K}{Γ ⊢ A ≤ C : K}  (S-Trans)
\frac{Γ_{1}, X≤A:K, Γ_{2} ⊢ ok}{Γ_{1}, X≤A:K, Γ_{2} ⊢ X ≤ A : K}  (S-TVar)
\frac{Γ ⊢ B_{1} ≤ A_{1} : ⋆  Γ ⊢ A_{2} ≤ B_{2} : ⋆}{Γ ⊢ A_{1}→A_{2} ≤ B_{1}→B_{2} : ⋆}  (S-Arrow)

\frac{Γ, X≤C:K ⊢ A ≤ B : ⋆}{Γ ⊢ ∀X≤C:K.A ≤ ∀X≤C:K.B : ⋆}  (S-All)
\frac{Γ, X≤C:K_{1} ⊢ A ≤ B : K_{2}}{Γ ⊢ ΛX≤C:K_{1}.A ≤ ΛX≤C:K_{1}.B : ΠX≤C:K_{1}.K_{2}}  (S-TAbs)
\frac{Γ ⊢ A ≤ B : ΠX≤D:K_{1}.K_{2}  Γ ⊢ C ≤ D : K_{1}}{Γ ⊢ A C ≤ B C : K_{2}[X←C]}  (S-TApp)
\frac{Γ ⊢ A ≤ B : K  Γ ⊢ K =_{β} K′}{Γ ⊢ A ≤ B : K′}  (S-K-Conv)

B Rules for the Typed Operational Semantics

Type Reduction Rules

\frac{Γ ⊢_{S} ok}{Γ ⊢_{S} T_{⋆} ↠_{w} T_{⋆} _{w}↠_{n} T_{⋆} : ⋆}  (ST-Top)
\frac{Γ ⊢_{S} A : K′  Γ ⊢_{S} K ↠_{n} K′  (X≤A : K) ∈ Γ}{Γ ⊢_{S} X ↠_{w} X _{w}↠_{n} X : K′}  (ST-TVar)

\frac{Γ ⊢_{S} A ↠_{w} X(A_{1}, …, A_{m}) : ΠX≤C:K_{1}.K_{2} Γ ⊢_{S} Γ(X) ↠_{n} D : K′ Γ ⊢_{S} D(A_{1}, …, A_{m}, F) : K Γ ⊢_{S} B ↠_{w} E _{w}↠_{n} F : K_{1} Γ ⊢_{S} E ≤_{W} C : K_{1}  Γ ⊢_{S} K_{2}[X←B] ↠_{n} K}{Γ ⊢_{S} A B ↠_{w} X(A_{1}, …, A_{m}, F) _{w}↠_{n} X(A_{1}, …, A_{m}, F) : K}  (ST-TApp)
\frac{Γ ⊢_{S} A_{1} ↠_{n} B_{1} : ⋆  Γ ⊢_{S} A_{2} ↠_{n} B_{2} : ⋆}{Γ ⊢_{S} (A_{1}→A_{2}) ↠_{w} (A_{1}→A_{2}) _{w}↠_{n} (B_{1}→B_{2}) : ⋆}  (ST-Arrow)

\frac{Γ ⊢_{S} A ↠_{n} C : K′ Γ, X≤A:K ⊢_{S} B ↠_{n} D : ⋆ Γ ⊢_{S} K ↠_{n} K′}{Γ ⊢_{S} ∀X≤A:K.B ↠_{w} ∀X≤A:K.B _{w}↠_{n} ∀X≤C:K′.D : ⋆}  (ST-All)

\frac{Γ ⊢_{S} K_{1} ↠_{n} K′_{1} Γ ⊢_{S} A ↠_{n} C : K′_{1} Γ, X≤A:K_{1} ⊢_{S} B ↠_{n} D : K_{2}}{Γ ⊢_{S} ΛX≤A:K_{1}.B ↠_{w} ΛX≤A:K_{1}.B _{w}↠_{n} ΛX≤C:K′_{1}.D : ΠX≤C:K′_{1}.K_{2}}  (ST-TAbs)

\frac{Γ ⊢_{S} B ↠_{w} ΛX≤A:K_{1}.D : ΠX≤A′:K′_{1}.K_{2} Γ ⊢_{S} D[X←C] ↠_{w} E _{w}↠_{n} F : K Γ ⊢_{S} K_{2}[X←C] ↠_{n} K Γ ⊢_{S} C ≤ A : K′_{1}}{Γ ⊢_{S} B C ↠_{w} E _{w}↠_{n} F : K}  (ST-Beta)

Weak-Head Subtyping

\frac{Γ ⊢_{S} A _{w}↠_{n} B : ⋆  HV(A) undefined}{Γ ⊢_{S} A ≤_{W} T_{⋆} : ⋆}  (SWS-Top)

\frac{Γ ⊢_{S} X(A_{1}, …, A_{m}) _{w}↠_{n} C : K Γ ⊢_{S} Γ(X) ↠_{n} B : K′ Γ ⊢_{S} B(A_{1}, …, A_{m}) ↠_{w} E : KΓ ⊢_{S} E ≤_{W} A : K A ≢ X(A_{1}, …, A_{m})}{Γ ⊢_{S} X(A_{1}, …, A_{m}) ≤_{W} A : K}  (SWS-TApp)

\frac{Γ ⊢_{S} X(A_{1}, …, A_{m}) _{w}↠_{n} B : K}{Γ ⊢_{S} X(A_{1}, …, A_{m}) ≤_{W} X(A_{1}, …, A_{m}) : K}  (SWS-Refl)

\frac{Γ ⊢_{S} B_{1} ≤ A_{1} : ⋆  Γ ⊢_{S} A_{2} ≤ B_{2} : ⋆}{Γ ⊢_{S} A_{1}→A_{2} ≤_{W} B_{1}→B_{2} : ⋆}  (SWS-Arrow)

\frac{Γ, X≤A_{1}:K ⊢_{S} A_{2} ≤ B_{2} : ⋆ Γ ⊢_{S} A_{1}, B_{1} ↠_{n} C : K′′Γ ⊢_{S} K, K′ ↠_{n} K′′}{Γ ⊢_{S} ∀X≤A_{1}:K.A_{2} ≤_{W} ∀X≤B_{1}:K′.B_{2} : ⋆}  (SWS-All)

\frac{Γ, X≤A_{1}:K_{1} ⊢_{S} A_{2} ≤ B_{2} : K_{2} Γ ⊢_{S} K_{1}, K′_{1} ↠_{n} K′′_{1} Γ ⊢_{S} A_{1}, B_{1} ↠_{n} C : K′′_{1}}{Γ ⊢_{S} ΛX≤A_{1}:K_{1}.A_{2} ≤_{W} ΛX≤B_{1}:K′_{1}.B_{2} : ΠX≤C:K′′_{1}.K_{2}}  (SWS-TAbs)