Subtyping Parametric and Dependent Types An introduction^{∗}

Gang Chen

School of Comp. and Info. Sci. University of South Australia

The Levels, South Australia 5095 cisgc@cs.unisa.edu.au

Giuseppe Longo

LIENS (CNRS) and Dept. d’informatique Ecole Normale Supérieure 45 rue d’Ulm, 75005 Paris, France longo@dmi.ens.fr

Abstract

A type may be a subtype of another type. The intuition about this should be clear: a type is a type of data, some data then may live in a given type as well as in a larger one, up to a simple “transformation”. The advantage is that those data may be “seen” or used in different contexts. The formal treatment of this intuition, though, is not so obvious, in particular when data may be programs. In Object Oriented Programming, where the issue of “reusing data” is crucial, there has been a long-lasting discussion on “inheritance”. Since early work of Cardelli and Wegner, there has been a large amount of papers developing several possible functional approaches to inheritance, as subtyping. Indeed, functional subtyping captures only one point of view on inheritance, yet this notion largely motivated most of that work. Whether or not inheritance is exactly functional subtyping, this notion raised several problems and many relevant answers. We take the most naive approach, here, and survey two recent approaches and some of their consequences, one for the second order types (variable types), the other for types which may depend on first order variables.

A brief survey of futher recent work is presented in the last part of this paper.

1 Introduction

Sets have subsets. This is an absolutely crucial notion in Set Theory, as a key axiom, Comprehension, in its various forms, “isolates” by a predicate a set, as a subset of a previously given set. Many consider the subset relation as a fundamental link to Logic, as it provides an elementary form of implication (p is q).

∗This paper is based on Longo’s Invited Lecture at “Type Theory and Term Rewriting”, Glasgow, September 1996. It has been revised in 1999 and the last two sections are mainly written by Chen.

Objects of categories have subobjects (i.e. monomorphic embeddings). Subobjects are usually considered less crucial, in general approaches to Category Theory, than subsets for Set Theory. Yet, the notion turns out to be as relevant, when considering the area of Category Theory that more closely relates to Logic: Topos Theory. In this frame subobjects, suitably classified, determine the intended logic of the Topos.

Types have subtypes. This is less clear or more complex, to say the least. In Type Theories, some data then may live in a given type as well as in a larger one, but the intended “inclusion”, either in the set-theoretic sense or in the category-theoretic one (monomorphism) or otherwise, must be determined. The intuition is not so clear, as data may be programs and then one has to compare the type of inputs and that of outputs. This matter will be extensively discussed below.

In Object Oriented Programming, where the issue of “reusing data” is a basic facility, there has been a long-lasting discussion on “inheritance” and ... little agreement. Recently, the notion of “inheritance” has been applied to proof assistants in order to “reuse proofs”. There are several ways to understand and formalize inheritance, which depend on the specific programming environment used. Functional subtyping captures only one point of view on inheritance, yet this notion largely motivated a large amount of work. Whether or not inheritance is exactly functional subtyping, this notion raised several problems and many relevant answers (see, for example, [CW85, Mit88, BL90, BTCG^{+}91, CMMS91, CG92, PS97, Tiu96, TU96, Pie92, PS97, Com94, AC96, CC99, CG97a, Ste97, JLS97, LS99, Che98, DC98, Zwa99, BR00]). We follow this point of view, here, and survey two recent approaches and some of their consequences, one for the second order types (variable types), the other for types which may depend on first order variables (dependent types).

2 System Fc

Our starting point is Girard’s System F [Gir71]. Its language has two kinds of expression, types and terms, defined by the following syntax:

(Types)  σ ::= X | σ → τ | ∀X.σ
(Terms) M ::= x | λx:σ.M | MN | λX.M | Mτ

We will use:

σ, τ, ρ, μ for types  M, N, P, Q, R for terms
X, Y, Z for type variables  x, y, z for term variables

An environment Γ is a set of term variables with their types. We write Γ, x:σ to extend Γ with a new term variable x of type σ, where x must not already occur in Γ.

We use the notation Γ ⊢_{F c} M : σ for type assignment in system Fc, where term equality is defined below. The following rules define valid type assignments.

System Fc

(ax) Γ, x:σ ⊢_{F c} x : σ

(→ intro)  {Γ, x:σ ⊢_{F c} M : τ \atop Γ ⊢_{F c} λx:σ.M : σ → τ}  (→ elim) {Γ ⊢_{F c} M : σ → τ  Γ ⊢_{F c} N : σ \atop Γ ⊢_{F c} MN : τ}

(∀ intro) {Γ ⊢_{F c} M : σ \atop Γ ⊢_{F c} λX.M : ∀X.σ}

∗

for X not free in the type of any free term variable in M

(∀ elim)

{Γ ⊢_{F c} M : ∀X.σ \atop Γ ⊢_{F c} Mτ : [τ/X]σ}

Reduction of terms is defined as usual by the closure of the following rules, where F V (M) stands for the set of free type and term variables in M:

\begin{matrix}(β_{1}) & (λx:σ.M)N =_{β_{1}} [N/x]M & (β_{2}) & (λX.M)τ =_{β_{2}} [τ/X]M \\ (η_{1}) & \begin{matrix}λx:σ.Mx =_{η_{1}} M \\ ∗ & for x ∉ F V (M) \end{matrix} & (η_{2}) & \begin{matrix}λX.MX =_{η_{2}} M \\ ∗ & for X ∉ F V (M) \end{matrix} \end{matrix}

Equality of terms is the intended equality: namely the usual reflexive and transitive closure of the reduction rules above augmented by the following axiom.

(Axiom C) {M : ∀X.σ \atop Mτ_{1} = Mτ_{2}}
∗for X not ; free in σ

It may be fair to call intended this extension as it formalizes an early and relevant remark of J.Y. Girard, in [Gir71]: in System F, there are no type discriminators. Indeed, (Axiom C) forces terms of universally quantified type, whose outputs live in the same type, to be constant; that is, it says that a term cannot discriminate between different types, by giving provably different output (different normal forms in the same type). The very sound idea is that in our constructive framework a type represents possibly infinite information. Thus a finite program, a term, cannot output 0 or 1, say, according to a check on the equality of possibly infinite entities. Note also that all known proper models of F realize (Axiom C), that is all known models except the term model and models of the inconsistent theory Type:Type, see [Lon95]. The extended system, call it Fc, has a decidable term-equality; indeed, it may be obtained by a normalizing and Church-Rosser reduction relation (ongoing work of Bellé).

3 Sets and Propositions

Usually, formalisations are guided by semantic intuition. We then sketch first a path through informal meaning towards a sound theory. Later we will survey the basic ideas of a mathematical model. There exist several alternative interpretations of types, which may suggest different treatment of subtyping. Types may be sets, propositions or objects of categories. We briefly discuss the first two understanding of subtyping and just mention the latter.

3.1 Types as Sets or as Objects

As a type is a type of data, not necessarily a structured one, the first idea is to understand subtypes as subsets and extend System Fc by suitable rules, which mimic the intended properties of subsets. This interpretation is naif, indeed impossible, yet it may guide the first few steps towards a formalization.

Viewed as a set, a type is identically injected into a larger one. As for universal quantification, the core construction of System F, sets provide an immediate intuition and an easy formalization. The intuitive meaning of ∀X.σ is the following: the intersection of all the instances of σ, when X ranges in the intended domain. In this naif interpretation, ∀X.σ is always a subset of σ. Conversely, σ may also be a subset, thus identical to ∀X.σ, in the special case that X does not occur in σ. More formally,

(∀ left, axiom) ∀X.σ ≤ [ρ/X]σ

(∀ right, axiom) σ ≤ ∀X.σ for X not free in σ

In [Mit88] these are two of the formal axioms of the subtyping system. So far so good: sets provide a good intuition and suggest an easy formalization of the crucial inclusion relations, the ones between a type and its universal quantification. This relation is crucial, as the strength of impredicative second order systems is given by the possibility of quantifying over type variables, thus one has to say something on how types and their universal quantifications relate to each other. Note finally that, over sets, the intended inclusion, in each direction, is an injection: indeed, the identical embedding.

The other type constructor of System F(c) is not less relevant: it is the arrow type constructor. Its set-theoretic interpretation poses no problem: (the interpretation of) σ → τ is the set of functions from (the interpretation of) σ to τ. Can we inherit to arrow types the identical injection of a subset into a set? No, there is no way: suppose that σ is a subset of ρ then σ → τ is not a subset, nor a superset of ρ → τ. In the set-theoretic interpretation of the functions in σ → τ as graphs, that is as single-valued subsets of the cartesian product σ × τ, the two function sets are simply incomparable.

Of course, there are maps going from one arrow set to the other (by extending functions, say), but the identical embedding is lost in either case.

Unfortunately, general Category Theory cannot help either for an interpretation: subobjects nicely generalize subsets, but, similarly as for sets, the monomorphic embedding which characterizes subobjects (see any text in Category Theory, such as [AL91], say) is not inherited at higher types, as a monomorphism is an injection in the specific case of the Category of Sets (a recent, though complex, categorical frame for subtyping has been proposed in [Jac95]). In conclusion, both naif Set and Category Theory cannot suggest any sound formalization of inclusion between arrow types. Moreover, even for universal quantification, the suggestion was very informal, as its meaning is far from granted in either approach, as we will mention later.

3.2 Types as Propositions

Even though naif Set Theory suggested a well motivated formalization for subtyping universally quantified types, it did not help us with the arrow types. We are then forced to try another meaning for inclusion and derive a formal treatment from it. The well-known interpretation of types as propositions may turn out to be useful. How can we interpret subtypes as subpropositions? By a blend of logical and naif set-theoretic meaning of inclusion as implication or entailment. A proposition naively determines a set, its set of validity. Then, when the intended set for σ is a subset of the intended one for ρ or σ ≤ ρ, this means that σ implies ρ. Let’s then maintain this interpretation and consider inclusion as a special case of logical implication, when types are viewed as propositions, and forget that this actually originated from looking at propositions as sets. One of the tasks of the formalization will be to determine exactly what kind of implication it is.

We check first inclusion for arrow types, as it caused problems. Since aristotelian logic it is known that if ρ implies σ then σ → τ implies ρ → τ, if → is understood as linguistic implication. Assume σ → τ and that ρ implies σ, then, given ρ, go first to σ and then from σ to τ, by using σ → τ. Thus, σ → τ implies ρ → τ. So far as for the crucial first argument of the → type constructor. The second argument, here as before, does not pose any problem: if ρ implies σ, then τ → ρ trivially implies τ → σ. In conclusion, once inclusion is understood as implication (or entailement), ancient logic suggests the following rule, contravariant in the first argument and covariant in the second.

(→) {σ ≤ τ  ρ ≤ ρ′ \atop τ → ρ ≤ σ → ρ′}

By chance, it happens that this rule has also a clear computational meaning, in the modern terminology, in spite of the lack of set-theoretical and categorical sense. Go back again to the naif interpretation of subtypes as subsets and assume that ρ is “settheoretically” included in σ. A program of type σ → τ can “a fortiori” act on any input of the smaller type ρ. Thus, the programs in σ → τ inhabit also ρ → τ, or σ → τ is included in ρ → τ. The difference with the set-theoretic and the categorical approach should be clear. In this computational perspective, programs are not single-valued settheoretic relations, nor categorical morphisms with intended source and target, but list of symbols, acting on inputs. The understanding is naif, as we are discussing of typed programs and use a type-free understanding of their manipulation of inputs. This is fair though, as it corresponds to the practice of many typed programming languages, the ML family for example, where types are used only at compile time and not at run time, when they are actually fed with inputs. This computational intuition motivated the introduction of the →-rule in [BCDC83] and [CW85].

Let’s now investigate the other key case: the inclusion relation between a type and its universal quantification. No problem here: in logic, ∀X.σ clearly implies [ρ/X]σ for any instantiation of X by ρ in σ. Similarly for the reverse inclusion, when X does not occur in σ, as quantification in this case is dummy. The point though will be to check whether this implication is the special kind of implication that interprets “inclusion” between propositions, some sort of “simple” implication representing the intended identical embedding of sets, within a logic frame. Note that, in order to work out the formal details, Set Theory cannot help, as there is no rigorous set-theoretic interpretation of system F [Rey83]. The miracle happens in a few categories, for example in the original blend of sets and categories provided by the Effective Topos, see [Hyl82], [LM91] and [BL90], an issue to be discussed later.

Before going to the formal description of subtyping as “implication”, entailment to be precise, recall though that naif Set Theory suggested an understanding of inclusion as identical embedding, where possible, in particular from ∀X.σ to [ρ/X]σ. When subtyping is logical implication, do we still have, in general, an injective map which represents the implication from ∀X.σ to [ρ/X]σ? We will discuss this issue in section 6.2. The reader, for the time being, may try to answer the question for exercise ... or, at least, to formalize it in Type Theory (i.e. write the implication which would say that λx:∀X.σ.xρ : ∀X.σ → [ρ/x]σ is injective, for any given σ and ρ).

4 Subtyping as Logical Entailment

We are now in the position to summarize in a unified approach the scattered remarks above on the meaning of subtyping. This Gentzen-style presentation of subtyping as entailment is taken from [LMS95] (see [LMS99] for a full presentation and furher work).

4.1 The Unlabelled System

Here is the core system:

(ax)  σ ⊢ σ  (→)  {σ′ ⊢ σ  τ ⊢ τ′ \atop σ → τ ⊢ σ′ → τ′}

(∀ left) {[ρ/X]σ ⊢ τ \atop ∀X.σ ⊢ τ}  (∀ right) {σ ⊢ τ \atop σ ⊢ ∀X.τ}
∗ for X not ; free in σ

Note that only one premise is allowed in a sequent σ ⊢ τ, as even the swapping of inputs is forbidden: this will help us in determining the exact class of maps representing subtyping as constructive implication. Thus, in order to deal with nested implications, we generalize (∀ right) to:

(∀_{n≥0} right) {σ ⊢ τ_{1} → … (τ_{n} → τ) …) \atop σ ⊢ τ_{1} → … (τ_{n} → ∀X.τ) …)}
∗ for X not ; free in σ nor ; in τ_{1}, …, τ_{n}

(∀_{n} right) is a family of rules indexed by n ≥ 0. Note that, if more than one premise was allowed, (∀_{n} right) would be the curried variant of (∀ right) with n premises.

These four rules are, basically, all we need. The reader may wonder what happened to a fundamental property of subtyping, that is, to transitivity. Indeed, in [LMS95] and [LMS99] it is proven that ⊢ is a partial order, thus, in particular that it is transitive and anti-symmetric. But transitivity is just a (cut) rule:

(cut) {σ ⊢ τ  τ ⊢ ρ \atop σ ⊢ ρ}

The proof of transitivity is then a proof of admissibility for the rule (cut). That is, each time the premises are derivable, then the consequence is derivable too, see below. Or, equivalently, that the system extended with (cut) has the cut-elimination property. Note that the rules above are all derivable in System F. However, the proof that one can “eliminate cuts”, in general, is not inherited to subsystems (a reduction path may lay outside the subsystem). Thus, we cannot use the normalization theorem of System F to prove it (see the complete version of [LMS95] for a direct proof and a detailed discussion).

In summary, the entailment system for subtyping is given by the rules: (ax), (→), (∀ left), (∀_{0≤n} right).

4.2 The Labelled System

Recall now that we are in a constructive frame. That is, proofs are not platonic observation of an outside ontology, but actual constructions; in particular, they are programs that transform proofs as inputs to proofs as outputs. This is the essence of Type Theory as formalized Intuitionistic Logic. Let’s then write the explicit terms as programs in the entailment rules. We consider terms as “labels” of the deduction rules.

System Co^{⊢} (labeled)

(ax)  x:σ ⊢_{co} x : σ

(→)  {x′:σ′ ⊢_{co} M : σ  y:τ ⊢_{co} N : τ′ \atop x:σ → τ ⊢_{co} λx′:σ′ . [xM/y]N : σ′ → τ′}

(∀ left)  {y:[ρ/X]σ ⊢_{co} M : τ \atop x:∀X.σ ⊢_{co} [xρ/y]M : τ}

\begin{matrix}For 0 ≤ k ≤ n \\ (∀_{k,n} ) & {x:σ ⊢_{co} λx_{1} :τ_{1} … λx_{k}:τ_{k}.M : (τ_{1} → … (τ_{n} → τ) …) \atop x:σ ⊢_{co} λx_{1} :τ_{1} … λx_{n}:τ_{n}.λX.Mx_{k+1} … x_{n} : (τ_{1} → … (τ_{n} → ∀X.τ) …)} \end{matrix}

This presentation of the last rule of Co^{⊢} in [LMS95] is taken from [Tiu96].

We already mentioned that the other approach dealing explicitly with the subtyping relation between a type and its universal quantification has been proposed by Mitchell in his seminal paper [Mit88]. The latter is an axiomatic approach, based on seven axioms and rules, which include transitivity among the assumption, and it is essentially equivalent to the one above, see [LMS95]. The advantages of a Gentzen style approach should be clear: we may derive transitivity and we can explicitly construct terms, as our deductions are typing rules, in the usual sense. This will also allow to state and prove a new fact: the coherence of the system, in a categorical sense.

5 Coherence, Completeness and Transitivity

(The results reviewed in this section are all from [LMS95] and [LMS99], unless otherwise stated). The terms given by the typing system above have several strong restrictions. They are clearly terms of System F, in normal form. They are “linear” in the precise and restrictive sense that each “abstrated” variable, that is each variable in the assumption, appears free exactly once in the consequence. Moreover, each sequent has exactly one assumption. We call coercions the typed terms in the systems, with reference to the meaning of this term in the practice of computing.

Are these coercions needed and useful? Note that we are in Type Theory, thus it make no sense to say, when σ is different from τ, that “σ can be identically embedded into τ”: there is no identity of type σ → τ, if σ is different from τ. Naif Set Theory suggested an axiomatization, but then, in the account above, we had to forget the vague hints coming from it, as Set Theory fails to give (even naively) a sound meaning to contravariance of the arrow type in the first argument. We had then to switch to Types as Propositions, where the meaning of a constructive approach is exactly given by the presence of typed terms. Thus coercions are needed, in Type Theory. (Note that also in categories one needs a non-identical morphism to go from σ to τ, if σ is different from τ.) The point is to prove how “simple” these maps are.

Recall now that we are thinking to System Fc, namely to system F extended with the constructive equality given by adding (Axiom C). Up to a “subtyping version” of (Axiom C), it is then possible to make some use of coercions as they may be shown to be unique, if any, between two types. Thus, a type is a subtype of another in “at most one way”; this corresponds also to the intuition of computing, as we only want one way to coerce integers, say, into reals.

Let’s first state the subtyping version of (Axiom C): following an idea for equality in presence of subtyping in [CMMS91], extend (Axiom C) to the following rule.

(eq appl2 co)  {y_{1} : [τ_{1}/X]σ ⊢_{co} N_{1} : μ  y_{2} : [τ_{2}/X]σ ⊢_{co} N_{2} : μ \atop x:∀X.σ ⊢_{co} [xτ_{1}/y_{1}]N_{1} =_{ηco} [xτ_{2}/y_{2}]N_{2} : μ}

Intuitively, (eq appl2 co) says that if two different instances of the same type are coerced to the same type μ, then these coercions equate the two coerced values, in the two instances, of each term in ∀X.σ. (Note that there is an underlining commuting diagram, in the categorical sense of “coherence”). It is easy to observe that, when [τ_{1}/X]σ = μ = [τ_{2}/X]σ, and thus when σ does not contain X free, (eq appl2 co) collapses to (Axiom C), for coercions.

We can then state the Coherence theorem for coercions.

Theorem 1 (Coherence of Co^{⊢} derivations) Consider two derivations x : σ ⊢_{co} M:τ and x:σ ⊢_{co} N:τ. Then, x:σ ⊢_{co} M =_{ηco} N.

In system F extended with subtyping, coherence has been investigated also in [CG92], from a different perspective though.

One may wonder then whether these coercions, which seem so few, are “sufficiently many”, namely whether system Co^{⊢} is enough expressive as to capture all “intended” subtyping relations. How to formalize this? There are two (equivalent) ways: a syntactic and a semantic one.

As for the syntax, what kind of computations should “all” coercions be? We already said that in Type Theory they cannot be identities. There is no doubt though that coercions should make little or no transformation on terms: at most they should update the type of the inputs and, viewed as type-free computations, they should compute like the identity. Indeed, in [Mit88] they are called “retyping” functions. Here comes, of course, the ML-like practice: at run time, when computing, we only want type-free terms.

It is very easy to show that the typable terms in Co^{⊢} erase to the identity. Namely, that, when all type information is inductively erased, one gets type-free terms η-equivalent to the identity. The point is that also the converse holds:

Theorem 2 (Completeness) Let M be a term in β-nf such that x:σ ⊢_{F} M : τ and erase(M) ⟶_{η} x. Then, x:σ ⊢_{co} M : τ.

As for the semantic completeness, this may be obtained by factorizing via Mitchell’s system, [Mit88], where a model-theoretic completeness theorem is given via that provably equivalent system to Co^{⊢}.

Completeness, besides its relevance, has an indirect application: transitivity. We already mentioned that the strength of the Gentzen style approach, as a type assignment system, was going to allow us to derive a key property of partial orders, transitivity, instead of assuming it.

Recall that, in the unlabeled system, transitivity may be written as the fact that the rule:

(cut) {σ ⊢_{co} τ  τ ⊢_{co} ρ \atop σ ⊢_{co} ρ}

is admissible.

At first thinking a labeled version could be the following:

{x:σ ⊢_{co} M : τ y:τ ⊢_{co} N : ρ \atop x:σ ⊢_{co} [M/y]N : ρ}

But the term [M/y]N may not be a coercion; in particular, it may not be in β-nf. However, without making use of the strong normalization property of System F, it is easy to show that, under the assumptions in the rule, [M/y]N normalizes (just use the strong linearity of coercions: coercions contain one lambda-abstraction for the unique occurrence of the unique free variable ...).

The existence and unicity of the β-nf of [M/y]N now motivates the following alternative version of the labeled (cut)-rule, where nf_{β}([M/y]N) means the β-nf of [M/y]N:

(cut)  {x:σ ⊢_{co} M : τ  y:τ ⊢_{co} N : ρ \atop x:σ ⊢_{co} nf_{β}([M/y]N) : ρ}

The theorem below proves than that x: σ ⊢_{co} nf_{β}([M/y]N) : ρ is actually a coercion, that is, derivable in Co^{⊢}; or, in other words, that the rule above is admissible.

Theorem 3 (Transitivity) (cut) is an admissible rule in Co^{⊢}. Proof: (Sketch) Just observe that if the assumptions erase to the identity, then also the consequence erases to the identity. By the completeness theorem we are done.

Definition (Bicoercibility) Two types σ and τ are defined to be bicoercible, written

σ ≅ ; b τ, iff σ ⊢_{co} τ and τ ⊢_{co} σ.

For example, τ ≅ ; b ∀X.τ for X not free in τ. Now, recall that, in general, two objects or types A and B are isomorphic, A ≅ B, if there are maps f : A → B and g: B → A such that g ∘ f = id and f ∘ g = id. Thus the following can be easily shown:

Corollary (Anti-symmetry) If σ ≅ ; b τ then σ ≅ τ in Co^{⊢}.

Note that bicoercibility is strictly stronger than isomorphism. In [Tiu95] it is shown that bicoercibility is decidable, while subtyping is not (see [TU96] and [Wel95]).

As a final remark, note that it is easy to extend Co^{⊢}with base types. Just extend the language of Co^{⊢} with fresh type constants κ_{1}, κ_{2}, κ_{3}, …. For example, these could be base types such as bool, int, real. To assert that a subtyping relation holds between some of these base types, between κ_{i} and κ_{j} say, add a fresh term constant c_{i,j} to the language and add the following Gentzen-style rule asserting that κ_{i} is a subtype of κ_{j} via coercion c_{i,j}:

(κ_{i} ≤ κ_{j}) {x:σ ⊢ M : κ_{i} \atop x:σ ⊢ c_{i,j} M : κ_{j}}

Then Co^{⊢}+ρ may be shown to be a conservative extension of Co^{⊢} , which satisfies (the extended versions of) the Coherence, Completeness and Transitivity Theorems.

6 Models and Parametricity

6.1 Intersection as Product

In the motivating discussion for the entailment system for subtyping above, we started with the issue of “injectivity” of subtypes into types. Indeed, both the set-theoretic identical embedding and the categorical monomorphism represent “injective” maps. And ... this is the reason why both Set Theory and Category Theory failed to provide the right abstract setting for subtyping, even in the propositional case: both forms of injectivity are lost at arrow types. However, consider just the subtyping relation in (∀ left) axiom or rule. It was an easy remark that, over sets, the naif interpretation of “for-all” as intersection yields injective embeddings: just the identity between an intersection of sets and one component of the intersection.

This interpretation of “for-all” as intersection is not sound, though: it could just informally guide the formalization. The technical reasons are given in [Rey83]. The intuition is that the intersection is “too small” or too much information is lost: from an intersection of sets, one cannot reconstruct the sets which gave it (the components of the intersection). Recall instead the constructive meaning of ∀X.σ. A proof-term M:∀X.σ is a computation or function that takes any type ρ to a proof Mρ : [ρ/X]σ. Thus, from the terms M:∀X.σ one can reconstruct the terms Mρ in each of its components [ρ/X]σ. Even in set-theoretic terms, the understanding of such an M as a function f and σ as a functional G in X may find a better representation as ‘indexed product”. Let then G be a function(al) from a set T p of “semantic types” to the category Set. The set-theoretic indexed product is defined as the set or class

∏_{X∈T p} G(X) = { f | f(X) ∈ G(X), for X ∈ T p}

There is a problem though: this is ... “too big”. T p should interpret the set of Types, that is ∀X.σ: T ypes should mean ∏_{X∈T p} G(X) ∈ T p, while there is no non-trivial set T p closed under products indexed over itself.

The solution comes from categorical logic, since the work of Lawvere, where universal quantification is (soundly) interpreted as a dependent or indexed product in suitable Toposes (see [AL91] for details in second order Type Theory, the case we are dealing with). As a matter of fact, in Category Theory, the intended interpretation of “for-all” as product is similar to the set-theoretic one above: categories just add more structure, which reduces the “size” of ∏_{X∈T p} G(X).

The connection between intersection and products is given in Hyland’s Effective Topos, [Hyl82], [Hyl88]. In short, in that specific model, the categorical interpretation of second order universal quantification, as “indexed product” (or adjoint to the diagonal functor), which is formally sound, happens to be (isomorphic to) an intersection, by a non-trivial result, see [LM91]. In a sense, by the validity of a strong proof-principle in that Topos, the Uniformity Principle, the intersection is so informative, or the product is so small, that they can both interpret second order universal quantification. By this, that model is the only known interpretation, up to now, of the subtyping rules for “arrow” and “for all”, see [BL90],[CL91],[LMS95]. The point though is that the embedding in (∀ left) axiom or rule, is not interpreted by an identical injection, since we are in a category and there is no identity between different objects. It is even not a monomorphism. Yet it is “computed” by the identical function, a true coercion in the sense above, indeed the closest we could go to the set-theoretic intuition. The further advantage is that this interpretation is finally sound and it is inherited at arrow types too.

6.2 Effective Parametricity

In the interpretation of Types as Propositions, which motivated our approach to subtyping as entailment, the injectivity of the coercions in the rules left for universal quantification may seem a minor curiosity, in particular because, also when Types are Propositions, injectivity is lost at arrow types. However, it is not so, as that particular injectivity sets an unexpected bridge towards an apparently unrelated topic: Parametricity.

We owe to Strachey, in the sixties, the distinction between “parametric” or uniform and “ad hoc” polymorphism, according to how polymorphic functions depend on their type parameters. Reynolds later proposed a formalization of the early ideas of Strachey: in his (rather complex) approach, parametricity is formalized as a notion of invariance by means of ”relations”. The idea is that the independence of computations w.r.t. (the internal structure of) types is expressed by their invariance w.r.t. arbitrary relations on types. The pivotal result is the “abstraction theorem”, which essentially says that a polymorphic function takes related input types to related output values. This approach has been given a categorical presentation in [MR92] and further developed by many, see for example [ACC93], [Has93].

The first link to our approach is that (Axiom C) can be (easily) derived in Reynolds’ relational extension of system F, see [ACC93], [Lon95].

The other connection is given by an alternative, but related (by (Axiom C)), approach to parametricity. This is given by the injectivity of the intended coercion in (∀ left). Recall the structure of this coercion:

(∀ left) {y:[ρ/X]σ ⊢_{co} M : τ \atop x:∀X.σ ⊢_{co} [xρ/y]M : τ}

Then, for each σ and ρ, the coercion from ∀X.σ to [ρ/X]σ is the following map (just take τ to be [ρ/X]σ in the rule):

x:∀X.σ ⊢_{co} xρ : [ρ/X]σ

Is this injective? And how is this related to parametricity?

The reader was already asked to write, at least, the exact statement of injectivity, for the coercion above. If he/she did so, he/she would now recognize that, by the following theorem, for each σ and ρ, with no restriction on σ nor ρ, the coercion above is injective. But, beyond the (minor) point of injectivity, one should understand the theorem for what it really says about terms parametrized by types (or polymorphic).

Theorem 4 (Genericity) Let Γ ⊢_{F} M : ∀X.σ and Γ ⊢_{F} N : ∀X.σ. Then, if Γ ⊢_{F c} Mρ = Nρ : [ρ/X]σ for some ρ, one has Γ ⊢_{F c} M = N : ∀X.σ.

The proof requires about 15 pages and is given in [LMS93]. It is based in a close proof-theoretic analysis of the derivation of the assumption and in the proof that, in that derivation, types are “generic”; namely, that the “value” of a type appearing in a term is not used in any computation from that term. Note that any term of System F yields a term of universally quantified type and, thus, satisfies an obvious variant of the theorem in terms of substitution.

Is this a form of “parametricity”, in the sense of Strachey? Yes, as it says that polymorphic terms have a “uniform behaviour” w.r.t. input types. Indeed, the meaning (and the strength) of the theorem is the following: if two polymorphic functions of the same type agree on one input, then they agree on all inputs. In other words, any type is generic (or behaves like a variable). In our understanding, the Genericity Theorem says that we cannot use the possibly infinite information carried by a type, as predicate or (structured) set. This corresponds to the effective nature of Intuitionistic Logic: terms may compute only on finite information. Thus, computations deal with types as “black holes”: if two terms compute to the same value on a given black hole, they will compute in the same way on all other black holes. This suggests that Genericity expresses a form of Effective Parametricity. (Or a strong uniformity for polymorphic functions, similar to the one for functions of complex variables: if they are known on the border of a sphere, then they are known everywhere.)

In conclusion, an easy to state injectivity property, which is trivial in Set Theory, false in Category Theory, yields an informative result in Type Theory: the effectiveness and uniformity of the dependence of terms on types. (For a discussion on model theoretic issues, in particular concerning the interpretation of Genericity in the Effective Topos, one should consult [Lon95]; some Proof Theory is discussed in [FL99].)

7 Subtyping first order dependent types

7.1 Motivation

System F extends simply typed λ-calculus, λ_{→}, by adding variable types and in particular, functions which are mappings from types to terms:

λX.M : T ypes ↦ T erms

On the other hand, dependent type systems have functions which give types as outputs. The first-order dependent type system λΠ (also called λP) is an extension of λ_{→} by adding functions which map terms to types:

Λx : ρ.τ : T erms ↦ T ypes

A function of this kind is called a type family, or simply, a family, which lives in the “kind” Πx:ρ.K where K is the kind for τ. There is a special kind ⋆ representing the class of all types. Suppose that a type family L lives in the kind Πx:ρ.⋆, then for y : ρ, Ly : ⋆ is a type. This shows that a type may contain terms with free variables. So an ordinary λ-term may have a π-type instead of an arrow type: λx:ρ.M : πx:ρ.τ, where x may occur free in τ. A notable new feature of dependent types is existence of type reduction:

(Λx : ρ.τ)M →_{β_{2}} τ[x := M]

More generally, we have type conversion σ_{1} =_{β} σ_{2} , where β = β_{1} ∪ β_{2} and β_{1} is the β-reduction on ordinary terms.

Due to the well-known logical interpretation, dependent types are widely used as foundation of proof development systems. Researchers in this area strongly feel the need of combining subtyping with dependent types. The following is an example given by Pfenning [Pfe93]. It is about an economic encoding of logics in logical framework LF. Consider the set (or the type) of well formed formulas in propositional calculus defined by the syntax:

τ ::= Atom | ¬τ | τ ∧ τ | τ ∨ τ | τ ⇒ τ |

A subset of these formulas can be defined as:

τ_{1} ::= Atom | ¬τ_{1} | τ_{1} ∨ τ_{1}

As pointed out by Pfenning, without subtyping, the representation of subsets of formulas like τ_{1} is awkward and will lead to inefficient implementations of proof search procedures. To overcome the problem, he proposed the subsorting relation, which could be viewed as a restricted form of subtyping. In the dependent type theory with subsorting, the above syntax can be represented as:

\begin{matrix}Atom <: τ_{1} & − − Atom is a subsort of the type formula τ_{1} \\ τ_{1} <: τ & − − τ_{1} is a subsort of τ \end{matrix}

¬ : τ → τ  ¬ : τ_{1} → τ_{1}
∧ : τ → τ → τ  ∨ : τ_{1} → τ_{1} → τ_{1}
∨ : τ → τ → τ
⇒ : τ → τ → τ

where τ <: ρ denotes that τ is a subsort of ρ. Assume, for example, that v_{1}, v_{2} are variables of atomic type, then ¬v_{1} ∨ v_{2} is in type τ_{1}, so, by the subsorting relation, it is in the type τ^{1}.

This example demonstrates the advantage of using subtyping. In the following, we concentrate on the meta-theoretic study of subtyping extensions on dependent type systems.

7.2 Subtyping in λP_{≤}

Aspinall and Compagnoni [AC96] have studied λP_{≤}, which is a subtyping extension to the pure dependent type system λΠ. Its subtyping system is as follows:

S-CONV  \frac{Γ ⊢ τ, ρ : K τ =_{β} ρ}{Γ ⊢ τ ≤ ρ}  S-π  \begin{matrix}Γ ⊢ τ′ ≤ τ, Γ, x : τ′ ⊢ ρ ≤ ρ′ \\ Γ ⊢ πx:τ.ρ : ⋆ \\ Γ ⊢ πx:τ.ρ ≤ πx:τ′.ρ′ \end{matrix}

S-Λ  \frac{Γ, x : τ ⊢ ρ ≤ ρ′ Γ ⊢ Λx:τ.ρ : K}{Γ ⊢ Λx:τ.ρ ≤ Λx:τ.ρ′} S-TRANS  \frac{Γ ⊢ τ ≤ ρ Γ ⊢ ρ ≤ σ}{Γ ⊢ τ ≤ σ}

S-VAR  \frac{Γ ⊢ ⋆ α ≤ Γ(α) : K in Γ}{Γ ⊢ α ≤ Γ(α)}  S-APP  \frac{Γ ⊢ τ ≤ ρ Γ ⊢ ρM : K}{Γ ⊢ τM ≤ ρM}

Compared to the case of second order polymorphism, there are several new features in this set of rules:

Kinding condition Kinding requirements, such as Γ ⊢ τ, ρ : K and Γ ⊢ πx:τ.ρ : ⋆, are used to ensure that the types and type families are well-formed in subtyping rules. Without them, we may have undesirable subtyping judgements, e.g. (πx:τ.ρ)M ≤ (πx:τ′.ρ′)M, where the expressions at two sides of ≤ are not well-formed.

The existence of kinding premises in the subtyping rules complicates the prooftheoretic research, because typing, kinding, context formation and subtyping are mutually related.

Conversion rule The analysis of λP_{≤} is challenging, principally because it introduces the conversion rule S-CONV for subtyping based on type convertion, and the rule S-APP for subtyping based on type family application. These rules are responsible for the loss of transitivity elimination (cut-elimination) at type level. In other

\begin{aligned}¬ & : (τ → τ) ∩ (τ_{1} → τ_{1}) \\ ∨ & : (τ → τ → τ) ∩ (τ_{1} → τ_{1} → τ_{1}) \end{aligned}

1There is an implicit use of intersection type in this typing declaration. Formally, the typing of ¬ and ∧ should be written as:

Therefore, a notion of intersection or overloading is also needed. See [CC99] for more details.

words, a derivation using transitivity rule can not always be transformed into a transitivity-free derivation, as it can be seen from the following example:

{σ =_{β} πx:τ.ρ \atop Γ ⊢ σ ≤ πx:τ.ρ} S-CONV \begin{matrix}Γ ⊢ τ′ ≤ τ & Γ, x : τ′ ⊢ ρ ≤ ρ′ \\ Γ ⊢ πx:τ.ρ ≤ πx:τ′.ρ′ \end{matrix} S-π

Γ ⊢ σ ≤ πx:τ′.ρ′ S-TRANS

Type family A type family is a type constructor. Informally, it can be viewed as a function mapping a set of terms to a type. Syntactically, a type family can be a type variable, an Λ-abstraction of the form Λx:τ.ρ, or an application τM. Given two type families τ, ρ of the same kind, say Πx_{1}:τ_{1}...Πx_{n}:τ_{n}.⋆, the notion τ ≤ ρ could be understood as: for all terms M_{1}, ..., M_{n}, τM_{1}...M_{n} is a subtype of ρM_{1}..., M_{n}. The subtyping rules about type family are S-Λ and S-APP.

λP_{≤} has the desired meta-theoretic properties: confluence, strong normalization, subject reduction and decidability of subtyping. One of the main technical contribution of λP_{≤} is its algorithmic subtyping system defined on β_{2}-normalized types. Reflexivity and transitivity are all admissible in this system. The algorithmic system is the key step in the proofs of subject reduction and the decidability.

7.3 Subtyping in λΠ_{≤}

The research of λΠ_{≤}([Che96], also in [CC99] Part II) started with an attempt to investigate two questions about λP_{≤} subtyping rules:

1. Could kinding premises be removed from the subtyping rules?

2. Does there exist a subtyping system with transitivity-elimination at the type level?

λP_{≤} is a pure dependent type system with subtyping. Proofs in λP_{≤} are quite delicate due to the circularity of the subtyping and typing system. For practical applications, it is inevitable to add other type constructions such as inductive types, intersection types, overloaded types etc. A system with complicated proofs is usually difficult to extend. Without kinding premises, subtyping rules would be independent from typing and kinding, allowing a relatively easy study.

Transitivity-elimination is an essential property in the study of subtyping. Proofs of subject reduction and decidability all depend on this property. It would be desirable to lift the transitivity elimination to type level instead of being restricted to normalized expressions.

λΠ_{≤} consists of a set of subtyping rules coming from a modification to the algorithmic subtyping rules of λP_{≤}. The major improvement is that it is capable of handling arbitrary types instead of just normalized types. The λΠ_{≤} subtyping rules are:

S-π  \frac{Γ ⊢ τ′ ≤ τ Γ, x : τ′ ⊢ ρ ≤ ρ′}{Γ ⊢ πx:τ.ρ ≤ πx:τ′.ρ′}  S-Λ  \frac{Γ, x : τ ⊢ ρ ≤ ρ′}{Γ ⊢ Λx:τ.ρ ≤ Λx:τ.ρ′}

S-ApR  \frac{M_{1} =_{β} M′_{1} ⋯ M_{n} =_{β} M′_{n}}{Γ ⊢ αM_{1}..M_{n} ≤ αM′_{1}..M′_{n}}  S-ApT  \frac{Γ ⊢ Γ(α)M_{1}..M_{n} ≤ τ}{Γ ⊢ αM_{1}..M_{n} ≤ τ}

S-ApSL  \frac{Γ ⊢ [M_{1}/x]ρM_{2}..M_{n} ≤ σ}{Γ ⊢ (Λx:τ.ρ)M_{1}..M_{n} ≤ σ}  S-ApSR \frac{Γ ⊢ σ ≤ [M_{1}/x]ρM_{2}..M_{n}}{Γ ⊢ σ ≤ (Λx:τ.ρ)M_{1}..M_{n}}

The main novelty is the addition of last two rules which deal with the subtyping derived from β_{2} conversion. The rules are designed in such a way that they are amenable to transitivity elimination.

This system is equivalent to λP_{≤} in the following sense, where ⊢_{λΠ_{≤}}, ⊢_{λP_{≤}}, ⊢_{λP_{≤}^{alg}} denote judgements in λΠ_{≤}, λP_{≤} and the algorithmic version of λP_{≤} respectively:

Γ ⊢_{λΠ_{≤}} τ ≤ ρ ∧ Γ ⊢ τ, ρ : ⋆ ⇔ Γ ⊢_{λP_{≤}} τ ≤ ρ ⇔ Γ ⊢_{λP_{≤}^{alg}} τ^{β_{2}} ≤ ρ^{β_{2}} ∧ Γ ⊢ τ, ρ : ⋆

This result implies the admissibility of transitivity in λΠ_{≤}. Note that no kinding premise is present in the rules, so the subtyping system is independent from the typing system. These rules can be straightforwardly turned into an ordered rewriting system to check subtyping. As subtyping is defined on types rather than on β_{2} normalized types, the algorithm could be more efficient.

From the equivalence with λP_{≤}, λΠ_{≤} keeps the desired properties like subject reduction, strong normalization and decidability. But we have also provided direct proofs. Apart from the the proof of admissibility of transitivity, another novel part in our proof is the proof of βΓ-strong-normalization, which is a key step of the proof of decidability of subtyping. The proof is more easy and general, it has been adapted to λC_{≤}[Che98], which is a subtyping extension to CC.

The technique used to achieve transitivity elimination will be further discussed in Section 8.

7.4 Semantical Analysis of Subtyping Relation

Recall that the logical interpretation of a subtyping relation Γ ⊢ τ ≤ ρ consists of two points:

1. τ,ρ are logical propositions and τ implies ρ;

2. any proof M of τ is also a proof of ρ in the sense that there is a coercion function c from τ to ρ such that: (a) cM is a proof of ρ; (b) c behaves like an identity function. So a subtyping relation τ ≤ ρ can be understood as an assertion that “any proof of the proposition τ can be used as a proof of ρ with straightforward modifications in the type labels”. If we take τ, ρ as specifications for programs, then the subtyping relation means that any programs satisfying the specification of τ can be straightforwardly adapted for the specification ρ. The latter point gives a restriction to the coercion.

In this subsection, we analyse the subtyping in dependent type system from the logical implication point of view.

In λP_{≤} and λΠ_{≤}, there are subtyping relations between type families. Type families are not types, so they can neither be interpreted as sets nor as formulas. But we use subtyping rules only in the subsumption rule for checking subtyping relations between “true” types, that is, we only want to check Γ ⊢ τ ≤ ρ such that Γ ⊢ τ, ρ : ⋆. In λΠ_{≤}, one can observe that all judgements in the derivation for such “true” subtyping judgement contains only types of kind ⋆. Therefore, subtyping between type families is not directly used, especially the rule S-A of Λ-abstraction can be eliminated.

Now we give a logical interpretation for subtyping rules in λΠ_{≤} except S-Λ.

Conversion-based rules Observe that rules S-ApR, S-ApSL and S-ApSR concern only the β-conversion. In logic, two β-convertible formulas are simply identified. So these rules are easily justified.

Subtyping π-types The logical interpretation of a π type πx:τ.ρ is the first-order universal quantified formula ∀x:τ.ρ. Therefore, the subtyping relation Γ ⊢ πx:τ.ρ ≤ πx:τ′.ρ′ can be understood as the implication between unversal quantified firstorder propositions: Γ ⊢ ∀x:τ.ρ ⇒ ∀x:τ′.ρ′, where the context Γ is used to record the free variables in these formulas.

Primitive subtyping The rule S-ApT is an application of subtyping relation defined in the context. For example, if α ≤ τ : Πx_{1}:τ_{1}...x_{n}:τ_{n}.⋆ is defined in the context, then α and τ represent n-ary predicates such that for any n terms M_{1}, ..., M_{n}

α(M_{1}, ..., M_{n}) ⇒ τ(M_{1}, ..., M_{n})

That is, the relation α ≤ τ in the context can be interpreted as the logical implication

∀x_{1}:τ_{1}...x_{n}:τ_{n}.(α(x_{1}...x_{n}) ⇒ τ(x_{1}...x_{n}))

The rule S-ApT is just a reformulation of this statement in order to preserve the transitivity elimination property.

8 An overview of recent progress in subtyping

The first part of this paper has presented the meta-theoretical properties of Co^{⊢}, including: transitivity elimination; subtyping as logical entailment; coercion as identity; completeness; coherence and anti-symmetry. In this section, we will discuss some recent advances in the studies of these properties in various subtyping systems (with dependent types). Some technical challenges will be analyzed along with the discussion of existing approaches. Further issue, such as subtyping checking and coercion inference, will also be briefly summarized. This brief survey does not attempt to be exhaustive, on the contrary, most technical analysis will be based on work by the first author. Due to the limitation of our knowledge and of space, many valuable results on subtyping may not be discussed or even missed in this paper. Especially, results based on simply typed λ-caluclus are not included in this discussion.

8.1 Transitivity Elimination

From the semantical point of view, a subtyping relation is a set of all “semantically acceptable” subtyping judgements. The subtyping relation should have the transitivity property: if two judgements σ ≤ τ and τ ≤ μ belong to the subtyping relation, then so does σ ≤ μ. Syntactically, such a relation could be represented by different sets of subtyping rules. For the convenience of discussion on transitivity elimination, we shall use the term subtyping system^{2} to describe a set of subtyping rules capable of deriving exactly all “acceptable” subtyping judgements in the subtyping relation. In practice, an “acceptable” subtyping relation could be either semantically characterized, as done in Co^{⊢}, or syntactically determined by a subtyping system incorporating the most intuitive subtyping rules, as done in λP_{≤}.

Although the underlying subtyping relation must be transitive, a subtyping system by itself may not explicitly contain a transitivity rule. We need only to show that the transitivity rule is admissible, as done for Co^{⊢} and λΠ_{≤}. In such a case, we also say that the system enjoys the transitivity elimination property, the term comes from the fact that the proof of admissibility of transitivity is mainly a procedure of elimination of transitivity.

Since the transitivity rule does not have the subformula property, it is hard to perform meta-theoretic studies over a subtyping system without this property. In particular, such difficulties can be seen in the investigations of subtyping checking, proof of subject reduction and that of completeness of subtyping. Therefore, it would be highly desirable if the transitivity rule could be eliminated from the subtyping system in question. Unfortunately, this is not always possible. In such a case, an effective choice is to construct an equivalent subtyping system enjoying transitivity elimination. This is often achieved by looking for those subtyping rules which are responsible for the loss of transitivity elimination, and by replacing them by some “better” rules.

2The term “subtyping system” has been ambiguously used in the literature, sometimes it denotes the set of “semantically acceptable” subtyping judgements, and sometimes one specific syntactical representation(in form of subtyping rules) of such a set. In most cases, the distinction between this two interpretations is unnecessary, because the “semantically acceptable” subtyping judgements are exactly all the derivable judgements of the given set of subtyping rules. But when there are several equivalent sets of subtyping rules, it is necessary to distinguish a specific syntactical representation and the set of “acceptable” subtyping judgements. Under this interpretation, both Mitchell’s system and Co^{⊢} can be view as two subtyping systems for the same subtyping relation, so do λP_{≤} and λΠ_{≤}.

In the history of subtyping, the first such case is in the study of F_{≤}, in which there is a rule for the introduction of primitive subtyping:

{α ≤ σ ∈ Γ \atop Γ ⊢ α ≤ σ}  (1)

Assume that the subtyping context Γ contains two declarations α_{1} ≤ α_{2}, α_{2} ≤ α_{3}. Then the transitivity in the following derivation can not be eliminated when the rule (1) is used as the sole rule for primitive subtyping:

\begin{matrix}Γ ⊢ α_{1} ≤ α_{2} & Γ ⊢ α_{2} ≤ α_{3} \\ Γ ⊢ α_{1} ≤ α_{3} \end{matrix}

This problem was solved by Curien and Ghelli[CG92]. Their method was to reformulate rule (1) into the following one:

\begin{matrix}Γ ⊢ α_{2} ≤ σ & α_{1} ≤ α_{2} ∈ Γ \\ Γ ⊢ α ≤ σ \end{matrix}

This rule has been incorporated into a subtyping system, which is equivalent to the original one and enjoys transitivity elimination. This system was called algorithmic system in their paper.

Another troublesome rule is

∀X.σ ≤ σ[ρ/X]

appeared in the Mitchell’s system (see 3.1). Co^{⊢} did not adopt this rule but the following one:

{σ[ρ/X] ≤ τ \atop ∀X.σ ≤ τ}

which is amenable to transitivity elimination.

The third difficult rule is the one which turns type conversion into subtyping. This rule is used in subtyping systems based on dependent types. Its most natual formulation, as appeared in F_{≤}^{ω}, λP_{≤}, has the form

\begin{matrix}σ =_{β} τ & Γ ⊢ σ, τ : s \\ Γ ⊢ σ ≤ τ \end{matrix}  (2)

The assumption Γ ⊢ σ, τ : s in the rule is called sorting condition, it ensures that σ, τ are well-formed types.

This rule has caused difficulty for the construction of subtyping checking algorithm. One approach to circumvent this problem was to restrict the use of the transitivity rule, e.g.[Bar95, Sai97, Lil97]. An important step in this direction is the approach proposed in F_{≤}^{ω}[PS97, Com94] and λP_{≤}[AC96], where intermediate subtyping systems (often called algorithmic system) are introduced. These systems are defined on normalized types, so that β-conversion can be avoided. Thus, these intermediate systems enjoy the transitivity elimination property. A negative aspect of this approach is that they depend on the analysis of the specific reductions in the system, therefore it is unclear how to apply it to systems with more reductions, such as CC.

The introduction of two rules S-ApSL and S-ApSR shown in the previous section gives a method to reformulate λP_{≤} so that the obtained system enjoys transitivity elimination at type level. The idea comes from the observation that both F_{≤} and Co^{⊢} turned a ”culprit” rule of the form

{⋯ \atop σ ≤ τ}

into a rule of the form

{τ ≤ ρ \atop σ ≤ ρ}

so that they can achieve transitivity elimination.

Thus, a similar rule reformulation is adopted in λΠ_{≤}. The main novelty is that the conversion is handled on both sides. The idea has been successfully extended to systems with more complicated reductions. In [Che97] and Part III of [Che98], the first author has proposed the system λC_{≤}, in which the rule (2) is reformulated as

\begin{aligned}σ =_{β} ρ_{1} & Γ ⊢ ρ_{1} ≤ ρ_{2} & ρ_{2} =_{β} τ & Γ ⊢ σ, ρ_{1}, ρ_{2}, τ : s \\ & Γ ⊢ σ ≤ τ \end{aligned} S-β

It is shown that the proposed subtyping system based on this rule enjoys transitivity elimination. This nice property greatly helps the proof of subject reduction in λC_{≤}. The effectiveness of this technique is not restricted in λC_{≤}: a similar rule also appeared in [Luo99], in which the transitivity elimination for the coercive subtyping system to the logical framework UTT(Universal Type Theory) is proved[JLS97]. UTT is a system more powerful than λC_{≤}, for example, it is capable of defining inductive types. Therefore, its subtyping system is more challenging.

To obtain a subtyping checking algorithm for λC_{≤}, the rule S-β is replaced by S-β′:

\begin{aligned}σ →_{β}^{∗} ρ_{1} & Γ ⊢ ρ_{1} ≤ ρ_{2} & ρ_{2} ←_{β}^{∗} τ \\ & Γ ⊢ σ ≤ τ \end{aligned} S-β′

This rule is obtained from S-β by replacing conversion by reduction and removing sorting condition, so that subtyping checking is independent from type checking.

A specialized form of S-β′ is proposed in [CG97a], where the reduction is the operational semantics. With this formulation, the transitivity elimination for their higher order subtyping system with bounded abstraction operator is proved.

An uncomfortable aspect of the rule S-β is that it contains a sorting condition, the purpose of which is to ensure that all types in a subtyping derivation are well-formed whenever the types in the conclusion of the derivation are well-formed. But this sorting condition complicates the meta-theoretical study, as subtyping and typing are not mutually independent. Furthermore, the adaptation of this method to general pure type systems and systems with bounded types would not be straightforward. Apparently, an alternative approach is to use S-β′. Historically, this was our first choice as it was a natural generalization from S-ApL and S-ApR. But we did not find a direct proof of transitivity elimination with this rule. By that time, it was unclear for us how to transform the following derivation into a transitivity-free one:

\begin{matrix}\begin{aligned}σ →_{β}^{∗} σ′ & σ′ ≤ ρ′ & ρ′ ←_{β}^{∗} ρ \\ & σ ≤ ρ \end{aligned} S-β′ & \begin{aligned}ρ →_{β}^{∗} ρ′′ & ρ′′ ≤ τ′′ & τ′′ ←_{β}^{∗} τ \\ & ρ ≤ τ \end{aligned} S-β′ \\ σ ≤ τ \end{matrix} => ?

This problem was solved by Jan Zwanenburg[Zwa99]. The trick is just to do a further case analysis on how the assumptions of these S-β′ rule are derived. This progress is quite successful and results in a general treatment of transitivity elimination. In fact, his work solves this problem for pure type systems and systems with bounded quantification.

8.2 Completeness of subtyping

A subtyping system is complete iff all “semantically acceptable” subtyping judgements are derivable. According to the semantical interpretation of subtyping in Section 4 and Section 5, a subtyping judgement σ ≤ τ is ”semantically acceptable” iff there is a coercion c : σ → τ such that c behaves like an identity function, more precisely, the erasure of c should be η-reduced to the identity. In general, there are two issues concerning the completeness of subtyping system:

1. how to construct a subtyping system such that each derivable judgement σ ≤ τ can be interpreted as arrow type σ → τ;

2. given a subtyping system, how to prove that it is complete. In this subsection, we discuss recent progress related to these two issues.

Subtyping as logical entailment The principle of subtyping as logical entailment, which lead to Co^{⊢}, is to interpret a subtyping judgement σ ≤ τ as a special case of arrow type σ → τ. Furthermore, the coercion c : σ ≤ τ should be interpreted as a term in σ → τ.

One coercive subtyping rule in accordance with this principle is the following rule for subtyping arrow types:

\begin{matrix}c : ρ ≤ σ & d : τ ≤ μ \\ λf:(σ→τ).λx:ρ.d(f(c(x))) : σ → τ ≤ ρ → μ \end{matrix}

It is easy to verify that

c : ρ → σ ∧ d : τ → μ ⇒ λf:(σ→τ).λx:ρ.d(f(c(x))) : (σ→τ)→(ρ→μ)

A naive generalization from such a rule to a coercive subtyping rule between Π-types would be:

\frac{Γ ⊢ c : ρ ≤ σ Γ, x : ρ ⊢ d : τ ≤ μ}{Γ ⊢ λf:Πx:σ.τ.λx:ρ.d(f(c(x))) : Πx:σ.τ ≤ Πx:ρ.μ}

Unfortunately, the coercion does not live in the expected arrow type:

\begin{aligned}& Γ ⊢ c : ρ → σ ∧ Γ, x : ρ ⊢ d : τ → μ \\ ⇏ & Γ ⊢ λf:Πx:σ.τ.λx:ρ.d(f(c(x))) : Πx:σ.τ→Πx:ρ.μ \end{aligned}

A possible solution to this problem is to change the conclusion of the rule to:

Γ ⊢ λf:(Πx:σ.τ[f(c(x))/x]).λx:ρ.d(f(c(x))) : Πx:σ.τ[f(c(x))/x] ≤ Πx:ρ.μ

Such a rule is neither elegant nor amenable to subtyping checking. Instead, we propose

\begin{matrix}Γ ⊢ c : ρ ≤ σ & Γ, x : ρ ⊢ d : τ[c(x)/x] ≤ μ \\ Γ ⊢ λf:Πx:σ.τ.λx:ρ.d(f(c(x))) : Πx:σ.τ ≤ Πx:ρ.μ \end{matrix} S-Π

The above rule has been adopted in λC_{≤}^{co}[Che98], which extends λC_{≤} by coercions. It is proved that Γ ⊢ c : σ ≤ τ implies Γ ⊢ c : σ → τ.

The property that subtyping as arrow type is also maintained in the coercive subtyping system on UTT in [JLS97].

Proof of completeness of coercive subtyping The key step of the proof of completeness is to analyze the form of a coercion c : A → B, under the condition that the erasure of c will be η-reduced to identity. If c is not in normal form, then the analysis is difficult. Unfortunately, those subtyping systems which derive judgements of form c : σ ≤ τ usually do not ensure that coercions will be in normal form. To see this point, just consider the rule S-Π in the previous subsection. In that rule, if the assumptions are also derived by S-Π, then d and c will be λ-abstractions, so the coercion in the conclusion will contain redexes.

On the other hand, the coercions in Co^{⊢} are always in normal form, where the coercive subtyping judgements are formulated as x : σ ⊢ M : τ. This representation apparently simplifies the proof of completeness. In [Che98], this technique is adapted in the proof of completeness for λC_{≤}^{co}. In this work two equivalent subtyping systems are formulated, one derives subtyping judgement of the form c : σ ≤ τ, another derives judgement of form x : σ ⊢ M : τ. The completeness is first shown for the second system. By means of the equivalence between the two systems, the completeness for the former system is obtained.

8.3 Anti-symmetry and Coherence

The anti-symmetry of subtyping means that if both σ ≤ τ and τ ≤ σ are derivable, then σ and τ are same types (convertible). In a system with dependent types, this property can be formulated as

σ ≤ τ ∧ τ ≤ σ ⇒ σ =_{βη} τ

The coherence of subtyping means that the derivation of subtyping is unique. In coercive subtyping system, this property can be stated as:

c : σ ≤ τ ∧ c′ : σ ≤ τ ⇒ c =_{βη} c′

In subtyping systems like λC_{≤}^{co}, the hard part in the proofs of both properties is to show that

Γ(α)M_{1}..M_{n} ≤ αM_{1}..M_{n}  (3)

is not derivable.

Anti-symmetry At the presence of dependent types, the application of primitive subtyping takes the form αM_{1}..M_{n} ≤ Γ(α)M_{1}..M_{n} where α ≤ Γ(α) is a subtyping declaration in the context, M_{1} ⋯ M_{n} are terms. Note that, if both Γ(α)M_{1}..M_{n} and αM_{1}..M_{n} were not well-formed, then it could be possible that they were convertible. For example, take Γ(α) ≡ λx.αx. In this case, the subtyping declaration α ≤ λx.αx is not a well-formed primitive subtyping declaration, as α should not occur free in Γ(α). Another example, which is adapted from [CG97b], is that Γ(α) ≡ λy.yy and M_{1} ≡ α. Here, the dependent type λy.yy can not have a well-formed kinding.

In [Che98], it is shown that the λC_{≤}^{co} system enjoys anti-symmetry. The key step of the proof is to show that (3) is not derivable if the subtyping judgement is well formed. First, using the result that λC_{≤}^{co} is strongly normalizing, it is shown that Γ(α)M_{1}..M_{n} and αM_{1}..M_{n} are not convertible if they are well-formed. This means that counterexamples like the second one could be excluded. Second, it is proved that any derivation for such a judgement would not contain the rule S-Π(see previous subsection). This result implies that any proof for (3) should take the form:

\begin{matrix}Γ(α)M_{1}..M_{n} →^{⋆}_{βη} α_{1}N_{1}^{1}..N_{k_{1}}^{1} ≤ Γ(α_{1})N_{1}^{1}..N_{k_{1}}^{1} →^{⋆}_{βη} α_{2}N_{1}^{2}..N_{k_{2}}^{2} \\ ≤ ⋯ Γ(α_{m})N_{1}^{m}..N_{k_{m}}^{m} ←^{⋆}_{βη} αM_{1}..M_{n} \end{matrix}

Hence, there should be at least one α_{i} in this sequence such that α_{i} occurs before α in the context Γ. By induction on the position of α in Γ, it is proved that such a sequence can never be constructed. This argument also illustrates why the counter-examples like the first one are impossible.

In [CG97b], Compagnoni and Goguen have proved that the system F_{≤}^{ω}, which is an extension of F^{ω} with bounded quantification, has the anti-symmetry property. The main step in their proof is also to show that (3) is impossible. Their technique is based on the operational semantics.

Coherence In [Che98], it is proved that λC_{≤}^{co} enjoys the coherence. The interesting part of the proof is the special case where types in a subtypng judgement are convertible:

σ =_{βη} τ ∧ Γ ⊢ c : σ ≤ τ ⇒ c =_{βη} λx:A.x

This result again depends on (3).

John, Luo and Soloviev [JLS97] have also proved that the coercive subtyping system on UTT has the coherence property. In their system, the primitive subtyping does not take the form as in λC_{≤}^{co}, besides, its base system UTT is more powerful than λC, so the technique of proof is different.

8.4 Subtyping checking and coercion inference

In this subsection, we list briefly the works in subtyping checking and coercion inference.

Subtyping checking In the study of subtyping checking, the transitivity elimination plays a crucial role. In many cases, if a subtyping system can be reformulated into a system having transitivity elimination property, then the latter system could be turned into a subtyping checking algorithm. But transitivity elimination does not always imply decidable subtyping checking. It is well known that subtyping checking for two second order subtyping systems F_{≤} and Co^{⊢}, both of them enjoy transitivity elimination, are undecidable, see [Pie92] and [TU96] respectively. But, some variants of F_{≤} has decidable subtyping, see a discussion in [PS97]. One decidable variant of F_{≤} has been extended to a subtyping system for F^{ω} and named as F_{≤}^{ω}. This system still enjoys decidable subtyping [PS97, Com94] (the latter reference also contains intersection types). F_{≤}^{ω} with bounded operator abstraction is studied in [CG97a], F_{≤}^{ω} with polarities are studied in [Ste97] and [DC98]. In both systems, subtyping checking are decidable. As we have mentioned in this paper, the system λP_{≤}, which is a subtyping extension to λP, also has decidable subtyping and typing[AC96]. The combination of λ& (an overloaded type system with subtyping) and λP_{≤}, named as λΠ^{&}, contains a subsystem, which has decidable subtyping [CC99]. The system λC_{≤}, which can be viewed as an extension of λP_{≤}(or λΠ_{≤}) to λC, enjoys decidable subtyping and typing [Che97, Che98]. Finally, the subtyping and type checking for the subtyping extension to PTS (Pure Type System) are decidable [Zwa99]. A recent progress in this direction is a subtyping system with inductive types [BR00].

Coercion inference Two coercion inference algorithms have been implemented on proof assistants LEGO [Bai96] and Coq [Sai97] respectively. A formalization of coercion inference problem is presented in [Che98], where it is shown that the coercion inference for λC_{≤}^{co} is decidable. A coercion inference algorithm for the coercive subtyping system on UTT is studied in [JLS97], where the correctness of the algorithm is proved. A notable recent development in this direction is the study of dependent coercions[LS99].

9 Conclusion and Future Work

In this short survey, we have presented subtyping for two type systems: Co^{⊢} for System-F(c) and λP_{≤}, λΠ_{≤} for λΠ.

There are several common features in these studies. From the syntactic point of view, both in Co^{⊢} and λΠ_{≤} transitivity is admissible. From the semantical side, the interpretation of subtyping as logical entailment with coherent coercions has been first developed in the study of Co^{⊢} and then applied to λΠ_{≤}.

In the last part of this paper, we discussed recent works on subtyping with a focus on the issues related to Co^{⊢}. Many aspects of subtyping have not been covered in this analysis, especially the practical motivations of different subtyping rules. For more information, we refer the interested reader to relevant research papers[Pie92, PS97, Com94, AC96, CC99, CG97a, Ste97, JLS97, LS99, Che98, DC98, Zwa99, BR00].

Acknowledgements. Giuseppe Longo would like to thank Kathleen Milsted and Sergei Soloviev for the long lasting and stimulating collaboration; part of his early work on this topic was supported by Digital Equipment Corporation, by a generous consulting contract. Gang Chen is grateful for the discussions with David Aspinall, Adriana Compagnoni, Zhaohui Luo, Sergei Soloviev and Martin Steffen; his work in Paris was supported by Programme PRA M4, Association Franco-Chinoise pour la Recherche Scientifique et Technique, and Bourse du Ministère des Affaires Etrangères du Gouvernement Français.

References

[AC96] David Aspinall and Adriana Compagnoni. Subtyping dependent types, 1996. In LICS96.

[ACC93] M. Abadi, L. Cardelli, and P.-L. Curien. Formal parametric polymorphism. In Dezani, Ronchi, and Venturini, editors, Böhm Festschrift, Special issue of Theoretical Computer Science, 1993.

[AL91] Andrea Asperti and Giuseppe Longo. Categories, Types and Structures: an introduction to Category Theory for the working computer scientist. M.I.T.- Press, 1991. (pp. 1–300).

[Bai96] Anthony Bailey. Lego with implicit coercions, 1996. draft.

[Bar95] Gilles Barthe. Implicit coercions in type systems. In S. Berardi and M. Coppo, editors, Proceedings of Types’95, LNCS 1128, pp 1–15., 1995.

[Bar92] Henk Barendregt. Lambda calculi with types. In Handbook of Logic in Computer Science. Oxford University Press, 1992.

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

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

[BM92] Kim Bruce and John Mitchell. PER models of subtyping, recursive types and higher-order polymorphism. In Proceedings of the Nineteenth ACM Symposium on Principles of Programming Languages, Albequerque, NM, January 1992.

[BR00] Gilles Barthe and Femke van Raamsdonk Constructor subtyping in the Calculus of Inductive Constructions In Foundations of Software Science and Computation Structures, Berlin, Germany, March 2000.

[BTCG^{+}91] V. Breazu-Tannen, T. Coquand, C.A. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and Computation, 93:172–221, 1991. Part of this work appeared in the Proc. of the 4th International Workshop on Database Programming Languages, Wordkshop in Computing series, Springer Verlag.

[C^{+}86] Robert L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.

[Car87] Luca Cardelli. Typechecking dependent types and subtypes, December 1987.

[Cas97] G. Castagna. Object-Oriented Programming: A Unified Foundation. Progress in Theoretical Computer Science. Birkäuser, Boston, 1997. ISBN 3-7643-3905-5.

[CC99] Giuseppe Castagna and Gang Chen. An extension of dependent type with overloading and subtyping. to appear in Information and Computation.

[CG92] P. L. Curien and G. Ghelli. Coherence of subsumption, minimum typing and the type checking in F_{≤}. Mathematical Structures in Computer Science, 2(1), 1992.

[CG97a] A.Compagnoni and H. Goguen. Typed Operational Semantics for Higher Order Subtyping. Revised version of University of Edinburgh, LFCS report ECS-LFCS-97-361. April 1997. To appear in Information and Computation.

[CG97b] A.Compagnoni and H. Goguen. Anti-Symmetry of Higher-Order Subtyping. in CSL’99.

[CGL95] Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded functions with subtyping. Information and Computation, 117(1):115–135, 15 February 1995.

[Pie92] Benjamin C. Pierce. Bounded Quantification is Undecidable. Information and Computation, 112(1):131–165, July 1994,

[Che96] Gang Chen. Dependent type system with subtyping. Technical Report LIENS-96-27, Laboratoire d’Informatique, Ecole Normale Supérieure - Paris, 12 1996.

[Che97] Gang Chen. Subtyping calculus of construction (extended abstract). In The 22nd International Symposium on Mathematical Foundation of Computer Science, volume 1295. Springer-Verlag LNCS, August 1997. Bratislava, Slovakia.

[Che98] Gang Chen. Subtyping, type conversions and elimination of transitivity. PhD thesis, Université Paris 7, 1998.

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

[CMMS91] L. Cardelli, S. Martini, J.C. Mitchell, and A. Scedrov. An extension of system F with subtyping. In T. Ito and A.R. Meyer, editors, Theoretical Aspects of Computer Software, pages 750–771. Springer-Verlag, September 1991. LNCS 526.

[CNSvS94] Thierry Coquand, Bengt Nordström, Jan M. Smith, and Björn von Sydow. Type theory and programming. Bulletin of the European Association for Theoretical Computer Science, 52:203–228, February 1994.

[Com94] Adriana B. Compagnoni. Decidability of higher-order subtyping with intersection types. In Proceedings of the Annual Conference of the European Association for Computer Science Logic, CSL’94, Kazimierz, Poland, LNCS 933, Springer-Verlag, June 1995.

[Coq92] Thierry Coquand. Pattern matching with dependent types. In Proceedings on Types for Proofs and Programs, pages 71–83, 1992.

[Cou95] Judicaelë Courant. Rapport de magistère, Novembre 1995.

[DC98] Dominic Duggan and Adriana Compagnoni Subtyping for Object Type Constructors. FOOL 6, Oct. 1998.

[CW85] L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471–522, December 1985.

[DFH^{+}93] Gilles Dowek, Amy Felty, Hugo Herbelin, Gérard Huet, Chet Murthy, Catherine Parent, Christine Paulin-Mohring, and Benjamin Werner. The Coq proof assistant user’s guide. Rapport Techniques 154, INRIA, Rocquencourt, France, 1993. Version 5.8.

[FL99] T. Fruchart and G. Longo. Carnap’s remarks on impredicativity and the genericity theorem, In Logic and Foundations of Mathematics (Cantini et al. eds). Kluwer Academic Publishers, 1999.

[Gir71] Girard, J.-Y. Une Extension de l’Interprétation de Gödel à l’Analyse, et son Application à l’Élimination des Coupures dans l’Analyse et la Théorie des Types. In Jens Erik Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 63–92, Amsterdam, 1971. North-Holland.

[Has93] Ryu Hasegawa. Categorical data types in parametric polymorphism. 1993.

[HHP93] Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, January 1993.

[Hic95] Jason J. Hickey. Formal abstract data types, December 1995. Unpublished draft.

[Hyl82] J.M.E. Hyland. The effective topos. In A.S.Troelstra and D.S. van Dalen, editors, The L. E. J. Brouwer Centenary Symposium, pages 165–216. North-Holland, Amsterdam, 1982.

[Hyl88] J.M.E. Hyland. A small complete category. Annals of Pure and Applied Logic, 40, 1988.

[Jac95] B. Jacobs. Subtyping and bounded quantification from a fibred perspective. In Conference on Mathematical Foundations of Programming Semantics. New Orleans, U.S.A, 1995.

[JLS97] Alex Jones, Zhaohui Luo, and Sergei Soloviev. Some algorithmic and proof-theoretical aspects of coercive subtyping. (eds.) E. Gimenez and C. Paulin-Mohring, LNCS 1512.

[Lil97] Mark Lillibridge. Translucent Sums: A Foundation for Higher-Order Module Systems. PhD thesis, CMU, May 1997. CMU-CS-97-122.

[LM91] G. Longo and E. Moggi. Constructive natural deduction and its ω-set interpretation. Mathematical Structures in Computer Science, 1(2):215– 253, 1991.

[LMS93] Giuseppe Longo, Kathleen Milsted, and Sergei Soloviev. The Genericity Theorem and effective Parametricity in Polymorphic lambda-calculus. Theoretical Computer Science, 121:323–349, 1993.

[LMS95] Giuseppe Longo, Kathleen Milsted, and Sergei Soloviev. A Logic of Subtyping, extended abstract. In Logic in Computer Science, LICS’95, San Diego, June 1995. Complete version available on ftp.ens.fr/pub/dmi/users/longo/.

[LMS99] Giuseppe Longo, Kathleen Milsted, and Sergei Soloviev. Coherence and transitivity of subtyping as entailment. Journal of Logic and Computation, vol. 10, no. 96/53, pp. 1 - 35, 2000, available on ftp.ens.fr/pub/dmi/users/longo/.

[Lon95] Giuseppe Longo. Parametric and type-dependent polymorphism. Fundamenta Informaticae, 22(1-2):69–92, 1995.

[LP92] Zhaohui Luo and Robert Pollack. The LEGO proof development system: A user’s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, May 1992.

[Luo96] Zhaohui Luo. Coercive subtyping in type theory. In CSL’96, the 1996 Annual Conference of the European Association for Computer Science Logic, Utrecht, volume 1258, 1996.

[Luo99] Zhaohui Luo. Coercive subtyping. In Journal of Logic and Computation., Vol. 9, No. 1. 1999.

[LS99] Z. Luo and S. Soloviev. Dependent coercions. In Proc of the 8th Inter. Conf. on Category Theory in Computer Science (CTCS’99), Edinburgh, 1999.

[Mit88] J.C. Mitchell. Polymorphic type inference and containment. Information and Computation, 76:211–249, 1988.

[MR92] Q. Ma and J.C. Reynolds. Types, abstraction, and parametric polymorphism, part 2. In S. Brookes et al., editor, Mathematical Fundations of Programming Semantics, volume 598, pages 1–40. 1992.

[Pfe89] Frank Pfenning. Elf: A language for logic definition and verified metaprogramming. In Fourth Annual Symposium on Logic in Computer Science, pages 313–322, Pacific Grove, California, June 1989. IEEE Computer Society Press.

[Pfe93] Frank Pfenning. Refinement types for logical frameworks. In Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, May 1993.

[PS97] Benjamin Pierce and Martin Steffen. Higher-order subtyping. In Theoretical Computer Science, vol. 176, no. 1–2, pp. 235–282, 1997 (with a corrigendum in TCS vol. 184 (1997), p. 247).

[Rey83] J.C. Reynolds. Types, abstractions and parametric polymorphism. In R.E.A. Mason, editor, Information Processing ’83, pages 513–523. North-Holland, 1983.

[Sai97] Amokrance Saibi. Typing algorithm in type theory with inheritance. In the 24th Annual SIGPLAN-SIGACT Symposium on principles of Programming Languages, January 1997. Paris, France.

[Ste97] Polarized Higher-Order Subtyping PhD thesis, Technische Fakultt, Universitt Erlangen, 1997.

[Tiu95] J. Tiuryn. Equational axiomatization of bicoercibility for polymorphic types. In Proc. 15th Conference Foundations of software Technology and Theoretical Computer Science, LNCS, pages 166–179. Springer-Verlag, 1995.

[Tiu96] J. Tiuryn. A sequent calculus for subtyping polymorphic types. LNCS 1113, 1996.

[TU96] J. Tiuryn and P. Urzyczyn. The subtyping problem for second-order types is undecidable. In Proc. LICS 96, 1996.

[Wel95] J. Wells. The undecidability of mitchell’s subtyping relation. Technical report, Dept., Boston University, December 1995.

[Zwa99] Jan Zwanenburg. Pure Type Systems with Subtyping. In TLCA’99 LNCS 1581, May 1999.