Coherence and Transitivity of Subtyping as Entailment

Giuseppe Longo

LIENS(CNRS) and DMI Ecole Normale Supérieure

45 rue d’Ulm 75005 Paris, France longo@dmi.ens.fr

Kathleen Milsted

CNET France Télécom 28 chemin du Vieux Chêne BP 98, 38243 Meylan Cedex, France kathleen.milsted@cnet.francetelecom.fr

Sergei Soloviev

IRIT Université de Toulouse-III 118 route de Narbonne 31062 Toulouse, France soloviev@irit.fr

January 31, 2000

Abstract

The relation of inclusion between types has been suggested by the practice of programming as it enriches the polymorphism of functional languages. We propose a simple (and linear) sequent calculus for subtyping as logical entailment. This allows us to derive a complete and coherent approach to subtyping from a few, logically meaningful sequents. In particular, transitivity and anti-symmetry will be derived from elementary logical principles^{1}.

1 Introduction

The word “coercion” occurs in varying contexts. For example, in imperative and object-oriented programming languages such as C and C++, coercions are known as “casting functions”, whereby variables of one datatype (e.g., boolean) are “converted” or “cast” to another datatype (e.g., integer). In some languages, such conversions may actually change the underlying representation of the variable’s contents, in which case the conversion is done at run-time when the contents are known. More semantic interpretations characterise coercions with respect to identity functions, which do not imply a change to underlying representations. Coercions are used in this sense in [Mit88] for example, where they are known as “retyping functions”. In practice, the conversions implied by such coercions are performed statically at compile-time, for type-checking, etc. This paradigm is very relevant in functional programming.

In recent years, several extensions of core functional languages have been proposed to deal with the notion of subtyping; see, for example, [CW85, Mit88, BL90, BCGS91, CMMS91, CG92, PS94, Tiu96, TU96, Che96, Che98, Luo96, JLS98]. These extensions were suggested by the practice of various programming styles. In particular, they were inspired by the notion of inheritance as used in object-oriented programming languages, or by other concrete implementations of the following form of polymorphism: data living in a type σ, which is a subtype of τ, may also be seen as living in type τ, in some suitable sense. So, an integer is also a real, modulo an obvious “almost identical” coercion from integers to reals.

1Journal of Logic and Computation, to appear.

However, subtyping, in the presence of functional arrow → (and second-order universal quantification ∀) presents some semantic and logical problems. In all functional approaches to subtyping, arrow is formalized as being contravariant or antimonotone in the first argument. More formally:

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

where σ ≤ τ is read “σ is a subtype of τ”. The contravariant behavior of → (on the left) intuitively fits with the categorical notion of (contravariant) Hom functor, as well as with the intuitive understanding of programs as transformations acting on inputs: if a program M acts on inputs N in τ, then it can take as input any element in a subtype σ of τ. This is where the challenge arises: is it possible to give a precise mathematical meaning to the (→) rule and universal quantification, in the sense, say, of denotational semantics or of logical calculi?

In this paper, we propose a sequent calculus of subtyping, as a fragment of intuitionistic (linear) second-order propositional calculus. In particular, we focus on the introduction and elimination rules for ∀, which are at the core of second-order systems, and on a “cut-elimination” theorem. This is a relevant property for the partial order of subtyping, as the “cut” rule corresponds to transitivity.

The idea is that one can give an obvious logical (constructive) understanding of “σ is a subtype of τ” as “σ implies τ”, or more precisely, as “σ entails τ” (σ ⊢ τ). Note first that, with this interpretation, the (→) rule makes perfect sense: if σ entails τ and ρ entails ρ′, then τ → ρ entails σ → ρ′. Moreover, if terms in σ may also be in τ, then this embedding should be described by some sort of effective transformation: either the identity or a “suitable” coercion, as an effective map from σ to τ. Thus, by the Curry-Howard isomorphism, subtyping is a special case of intuitionistic implication: a computation from σ to τ is a proof of σ ⊢ τ. But which special case? And how to characterize it?

As we shall see, a characterization in terms of erasure (that is, after erasing all type information, coercions become identity maps in the untyped calculus) also has some semantic flavor.

The main results of this paper (except the part about base types) appeared without proofs in a previously published paper [LMS95] on a calculus for subtyping as logical entailment. The complete proofs related to that presentation may be found in a technical report [LMS96], where normalization for the simple, but impredicative, logical system presented here is dealt with by a direct argument — see the discussion in section 6.4. Those proofs have been deeply revised and simplified in this paper.

Since its publication, the calculus of subtyping in [LMS95] has been studied and developed by several authors (see, for example, [Tiu96, TU96, Che96, Che98]). Another approach to coercive subtyping, where “almost arbitrary” functions may be taken as coercions, was suggested by Zhaohui Luo and further investigated with the participation of one of the authors of the present paper [Luo96, JLS98]; that approach is more general but, because of its generality, it lacks the semantic motivation and the connection between coercions and logical deductions at the heart of the work presented here.

1.1 Subtyping as restricted linear implication

The logical frame we use here is intuitionistic second-order propositional logic. The intended meaning of σ ⊢ τ is that σ is a subtype of τ. An obvious axiom and the contra(co)-variance rule for → are the first requests for a logic of subtyping:

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

Consider now a logical interpretation of second-order ∀. Assume that σ contains X free and that from a specific instance of σ (with ρ substituted for X say), one can deduce τ. Then, from ∀X.σ one can, a fortiori, deduce τ. This is the (∀ left) rule of Gentzen’s sequent calculus. A semantic understanding of this second-order deduction can be given in the PER model of subtyping (see section 6.2 for a discussion and references): informally, if a specific instance of a family of types is a subtype of τ, then, in the model, the intersection of the entire family is a subtype of τ.

(∀ left) {[ρ/X]σ ⊢ τ \atop ∀X.σ ⊢ τ}

where [ρ/X]σ stands for the type resulting from the (capture-avoiding) substitution of type ρ for X in type σ.

Moreover, if σ entails τ, and σ does not contain X free, then σ also entails ∀X.τ. This is Gentzen’s (∀ right) rule. Semantically, if σ is a subtype of τ and σ does not depend on X, then σ is also a subtype of the intersection of all τs over X:

(∀ right) {σ ⊢ τ \atop σ ⊢ ∀X.τ}
∗ for X not ; free in σ

Recall now that the principal idea here is that the embedding of a type into another should be very simple: indeed, as close to the identity as possible in a typed language. Identities are linear maps, to say the least, as our system will be a fragment of the linear sequent calculus. Even more so: we allow only one premise in a sequent σ ⊢ τ, as even the swapping of inputs is forbidden. 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 all we need. Observe that ∀ is introduced to the left and to the right of entailment by two separate rules while → is symmetrically introduced both to the left and to the right of entailment by a single rule, the familiar (→) rule defined previously.

The reader may wonder what happened to a fundamental property of subtyping, that is, to transitivity. Indeed, we will prove that ⊢ is a partial order, thus, in particular that it is transitive and anti-symmetric. But transitivity is just a (cut) rule:

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

Proving transitivity will thus be the proof of admissibility for the rule (cut), that is, each time the premises are derivable, the consequence is derivable too. Or, equivalently, that the system extended with (cut) has the cut-elimination property. Notice that the proof that one can “eliminate cuts” is non-trivial for weak systems (as we will discuss in section 6.4) as, in general, these results and proofs are not inherited by subsystems.

Cut-elimination is a fundamental property in constructive logical systems. It guarantees consistency as it shows that each derivation can be given a “minimal” structure. In the various lambda-calculi, it relates deductions to computations as cut-elimination corresponds to β-reduction. In those systems, (cut) is a non-primitive rule, as it corresponds to the sequential application of (→-introduction) and (→-elimination) rules; moreover, it is usually considered as a (side) consequence of normalization. In contrast to this, for the purposes of subtyping, (cut) is as basic as transitivity.

The seemingly simple logical system above will be shown to be complete and coherent as a logic for deriving subtyping relations. By completeness, we mean that σ ⊢ τ is derivable iff there is a term of type σ → τ that erases to the identity (cf. section 3.1). Such a term is a coercion from σ to τ. By a result in [Mit88], this characterization also guarantees completeness with respect to subtyping in all PER models, in the sense of [BL90].

Coherence will mean that derivability of σ ⊢ τ implies the existence of a unique coercion from σ to τ. One of its consequences will be anti-symmetry. Coherence will be easily shown in the simple four rule system, while it requires cut-elimination if proved in the system extended with (cut).

Once the formal system is fully written down, with proof-terms displayed (see section 2.2), the next thing to be described is term equality. The notion of equality we use here may be viewed as the “generalized dual” of an early result of Girard[Gir71]: in system F, there is no definable term that discriminates between types. Namely, there is no definable term J_{σ} such that J_{σ} applied to type ρ is 1 if σ = ρ, and is 0 if σ ≠ ρ. This idea was taken up in [LMS93] by extending system F with the following axiom:

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

Intuitively, as there are no type discriminators, (Axiom C) forces terms of universally quantified type, whose outputs live in the same type, to be constant. System F extended with (Axiom C) satisfies the Genericity Theorem (see [LMS93]), which states that if two second-order functions (of the same type) coincide on an input type, then they are, in fact, the same function. Equivalently, types are generic inputs to second-order functions.

(Axiom C) was proposed following [Gir71] and independently of [CMMS91]. The latter defines the system F_{≤}, which includes the following inference rule, a generalization of (Axiom C) to subtyping:

(eq appl2) {M : ∀X.σ  [τ_{1}/X]σ ≤ μ  [τ_{2}/X]σ ≤ μ \atop Mτ_{1} = Mτ_{2} : μ}

This rule is sound within a context with Cardelli’s rule of subsumption [CW85]: if N:σ and σ ≤ τ then also N:τ. Observe that M gives outputs in (possibly) different types [τ_{1}/X]σ and [τ_{2}/X]σ. Then, intuitively, (eq appl2) says that if these two types (of outputs) have a common supertype μ, then the outputs are equal when seen as elements of μ. Thus, in particular, if σ does not contain X free, one obtains (Axiom C).

Note that (Axiom C) is valid in all proper models of system F, in particular in all “parametric models” in the sense of Reynolds ([MR92, ACC93]). Moreover, (eq appl2) holds in the only semantic models of system F with subtyping, namely in PER models with the intended coercions (see section 6.2). The relevance of (eq appl2) is that it allows one to prove the (categorical) universality of key definable constructs in System F (binary products, coproducts, existentials, etc.).

However, (eq appl2) relies implicitly on the subsumption rule, i.e., if M : σ and σ ≤ τ, then M : τ. And, as we will discuss in section 6.2, subsumption has neither typetheoretic nor categorical meaning, even though it may have solid practical motivations and intuitive meaning. Subsumption may be avoided in (eq appl2) if coercions are used explicitly along the lines of the following informal rule where the terms N_{1}, N_{2} represent coercions:

{M : ∀X.σ  y_{1} : [τ_{1}/X]σ ⊢ N_{1} : μ  y_{2} : [τ_{2}/X]σ ⊢ N_{2} : μ \atop [Mτ_{1}/y_{1}]N_{1} = [Mτ_{2}/y_{2}]N_{2}}

This will be formalized in our system as as the rule (eq appl2 co)) and that “coercion version” of (eq appl2) will be used in our type-theory as an interplay between subtyping and equality.

In conclusion then, our logic of subtyping will be based on the simple four rule sequent calculus presented previously, and the proof terms will satisfy the usual equational rules plus a coercion version of (eq appl2).

The paper is organised as follows. In section 2.1, we recall System F and describe our logic of subtyping, referred to as System Co^{⊢} (where “co” stands for coercions). We also prove in this section some lemmas about derivations in F and Co^{⊢} to help establish the relationship between these two systems, and notably that Co^{⊢} can be regarded as a subsystem of System F. Some aspects of the definition of cut (transitivity) in System Co^{⊢} are discussed and some syntactic conventions used in the paper are established.

Section 3 then presents the main results of paper: completeness of System Co^{⊢} with respect to the semantics provided by interpretation in the type-free calculus, admissibility of transitivity, and coherence. We postpone to this section a discussion about equality of coercions since it will be more natural after the completeness result is established. At the end of this section, the consequences for the relation of bicoercibility are also considered.

In section 4, Co^{⊢} is proved equivalent to a system of subtyping formulated by Mitchell [Mit88] in the sense that a subtyping judgement is derivable in Mitchell’s system iff the corresponding entailment is derivable in Co^{⊢} . Section 5 describes system Co^{⊢} extended with base types, and proves relevant properties of the extended system including conservativity, completeness, admissibility of transitivity and coherence. Finally, section 6 describes related work concerning other proof-theoretic analyses and models of subtyping, along with a discussion of equality and a discussion of second-order cut-elimination proofs. Section 7 ends with some conclusions.

2 System F and coercions

2.1 System F

We first recall System F [Gir71]. Then we define a sequent calculus of subtyping Co^{⊢} that may be regarded as a subsystem of System F.

The language of System F has two kinds of expressions, 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} M : σ for type assignment in system F. The following rules define valid type assignments.

System F

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

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

(∀ intro)  {Γ ⊢_{F} M : σ \atop Γ ⊢_{F} λX.M : ∀X.σ}  (∀ elim)  {Γ ⊢_{F} M : ∀X.σ \atop Γ ⊢_{F} Mτ : [τ/X]σ}

∗

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

We write F V (M) for the set of free type and term variables in M, and [N/x] and [σ/X] in prefix position for term and type substitution, respectively, with usual renaming of bound variables to avoid capture. Reduction of terms is defined as usual by the closure of the following rules:

\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}

We will write ⟶_{βη} for the transitive closure of all four reductions, ⟶_{β} for the closure of just β_{1} and β_{2}, and ⟶_{η} for the closure of η_{1} and η_{2}. We will also write “βη-nf” for normal form with respect to all four reduction relations, and “β-nf” or “nf_{β}” for normal form with respect to β_{1} and β_{2}.

Different equality relations on terms are defined by the symmetric, reflexive and transitive closure of the different reduction relations. In particular, we will write M =_{βη} N for equality with respect to ⟶_{βη}, and M =_{η} N for equality with respect to ⟶_{η}. We reserve the notation M ≡ N for syntactic identity of terms up to αconversion, and for types, equality, written σ = τ, is just syntactic identity up to α-conversion.

2.2 System Co^{⊢}

We now define our sequent calculus of subtyping, referred to as System Co^{⊢} or just Co^{⊢}. We will use ⊢_{co} for entailment in this system.

We give two presentations of Co^{⊢}. The first presentation gives only the types involved in each judgment, which are of the form σ ⊢_{co} τ. This presentation emphasizes the intended subtyping relation between types (σ ⊢_{co} τ can be read “σ is a subtype of τ”) but, of course, the calculus may be considered independently of this interpretation by referring just to its logical structure.

System Co^{⊢} (unlabeled)

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

(∀ left) {[ρ/X]σ ⊢_{co} τ \atop ∀X.σ ⊢_{co} τ}  (∀_{n} right) {σ ⊢_{co} τ_{1} → … (τ_{n} → τ) …) \atop σ ⊢_{co} τ_{1} → … (τ_{n} → ∀X.τ) …)}

∗

for 0 ≤ n, X not free in σ nor in τ_{1}, …, τ_{n}

In the second presentation of the system, we label each type with a term, yielding judgments of the form x: σ ⊢_{co} M : τ. We will refer to the first presentation as the “unlabeled” system, to the second as the “labeled” system.

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 : τ}

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

∗

for X not free in σ nor in τ_{1}, …, τ_{n}, M not of the form λy.M′, and x_{k+1}, …, x_{n} fresh

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

∗

for X not free in σ nor in τ_{1}, …, τ_{n}, M not of the form λy.M′ and τ ≡ τ_{n+1} → … (τ_{k} → τ′) …)

The rule ∀_{n}-right has two cases in the labeled system.^{2} In both cases, the premise has exactly the same form but we will shortly see that the two cases are disjoint.

In the rest of the paper, we will refer to judgments of either presentation (labeled and unlabeled) of Co^{⊢} as “sequents”. We will use S for sequents and α, γ for derivations of sequents.

Obviously a sequent σ ⊢ τ is derivable in unlabeled system Co^{⊢} iff σ ⊢ M : τ is derivable in the labeled system for some term M. If only the derivability of subtyping judgements is studied, then it is enough to consider the unlabeled system.

Many of the proofs in this paper are by induction on the size of a derivation. This notion of size is defined as the total number of applications of rules in a derivation.

In this work, a coercion is defined as follows:

Definition 1 (Coercion) A sequent x:σ ⊢_{co} M : τ is a coercion from σ to τ iff it is derivable in Co^{⊢}.

As a linguistic shorthand, we will also refer to the term M as a coercion when the sequent x:σ ⊢_{co} M : τ is derivable.

To illustrate Co^{⊢}, observe that ⊥ = ∀X.X (the empty type) is provably a subtype of all types. The corresponding coercion is obtained from the following derivation:

y:[σ/X]X ⊢_{co} y : σ
(∀ left)
x:∀X.X ⊢_{co} x σ : σ

2Tiuryn, in [Tiu96], presents (∀_{n} right) in another, slightly simpler form.

2.3 Some structural lemmas

Lemma 2 (Structure of coercions) Assume that x: σ ⊢_{co} M : τ. Then, M has exactly one free term variable which is x, and x occurs exactly once in M and always at head position. Furthermore, each bound term variable occurs exactly once in the body of M.

Proof By induction on the size of the derivation of x:σ ⊢_{co} M : τ.

This lemma shows that coercions are linear terms (in the usual sense).

Lemma 3 (Coercions are functions of System F) If x : σ ⊢_{co} M : τ then x:σ ⊢_{F} M : τ.

Proof By induction on the size of the derivation of x:σ ⊢_{co} M : τ.

Lemma 4 (Coercions are in β-nf) If x:σ ⊢_{co} M : τ then M is in β-nf.

Proof By induction on the size of the derivation of x: σ ⊢_{co} M : τ, as no inference rule creates a β-redex.

This lemma shows that the terms labeling the two cases of (∀_{n} right) are unambiguously defined since M, in the assumption, must be in β-nf.

We need the following lemma about subterms in System F to prove two invertibility lemmas below.

Lemma 5 Let Γ ⊢ P : τ. Consider an occurrence of a subterm Q of P. Let Γ_{0} be the environment that consists of all term variables free in Q. (Observe that Γ_{0} includes free variables of P that occur in Q, as well as bound variables of P bound by a λ with scope including this occurrence of Q; the types of these free and bound variables of P are defined by Γ and by the corresponding λ binders). Then:

1. Γ_{0} ⊢_{F} Q : ρ with ρ uniquely determined by Γ_{0} and Q.

2. Let P′ be some term containing at least one free occurrence of y. If P ≡ [Q/y]P′, then, since substitution excludes capture of free variables, Γ_{0} ⊢_{F} Q : ρ and Γ_{1}, y:ρ ⊢_{F} P′ : τ, with Γ_{0} consisting of all free variables of Q, Γ_{1} consisting of all free variables of P′ excluding y, and ρ uniquely determined by Γ_{0} and Q.

Proof By structural induction on some F-derivation of Γ ⊢ P : τ. In some places, we use also the well-known facts of admissibility of weakening and strengthening of F-contexts. Uniqueness of ρ follows from the uniqueness of typing in F. Base case for 1 and 2: axiom Γ, x : ρ ⊢ x : ρ. Then, ρ ≡ τ, Q ≡ P ≡ x, Γ_{0} ≡ x : ρ. Inductive step for 1: If P ≡ Q then Γ_{0} ⊆ Γ, ρ ≡ τ, and we use strengthening of F-contexts. If not, consider the last rule of the derivation.

(i) (→ elim):

{Γ ⊢_{F} M : σ → τ Γ ⊢_{F} N : σ \atop Γ ⊢_{F} MN : τ}

Since we consider a single occurrence of Q, it belongs to M or N. Γ_{0} is not changed. Apply the inductive hypothesis.

(ii) (→ intro):

{Γ, x:σ ⊢_{F} M : τ \atop Γ ⊢_{F} λx:σ.M : σ → τ}

Observe that Γ_{0} is not changed. If x ∈ F V (Q) the reason for its inclusion in Γ_{0} is changed, else it doesn’t belong. Apply the inductive hypothesis. (iii) (∀ intro):

{Γ ⊢_{F} M : σ \atop Γ ⊢_{F} λX.M : ∀X.σ}

∗

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

Q is a subterm of M, Γ_{0} is not changed. Apply the inductive hypothesis. (iv) (∀ elim):

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

Since τ is not a subterm, Q is a subterm of M. Γ_{0} is not changed. Apply the inductive hypothesis. Inductive step for 2: By 1) applied to each occurrence of Q, ρ is determined by Γ_{0}. If P ≡ Q then ρ ≡ τ, P′ ≡ y, and the derivation Γ_{1}, y:ρ ⊢ y : τ is an axiom.

If not, we consider the last rule of the derivation as above.

(i) (→ elim):

{Γ ⊢_{F} M : σ → τ Γ ⊢_{F} N : σ \atop Γ ⊢_{F} MN : τ}

M and N have the structure M ≡ [Q/y]M′, N ≡ [Q/y]N′ and in at least one of two cases, the substitution is not dummy. Γ_{0} is not changed. By inductive hypothesis, we obtain Γ_{0} ⊢_{F} Q : ρ.

Let Σ ⊆ Γ_{1} and Δ ⊆ Γ_{1} be the lists of free variables of M′, N′ respectively. Note that if one of M′, N′ does not contain y, it is identical to M, N, respectively. If y ∈ F V (M′), F V (N′), then by inductive hypothesis, Σ, y : ρ ⊢_{F} M′ : σ → τ, Δ, y:ρ ⊢_{F} N′ : σ. Using weakening and (→ elim), we have Γ_{1}, y:ρ ⊢_{F} M′N′ : τ.

If one of the substitutions M ≡ [Q/y]M′, N ≡ [Q/y]N′ is dummy, we don’t need the inductive hypothesis for this term but for the other, proceed as above. (ii) (→ intro):

{Γ, x:σ ⊢_{F} M : τ \atop Γ ⊢_{F} λx:σ.M : σ → τ}

Observe that Γ_{0} is not changed. In this case, because x cannot belong to F V (P). Apply the inductive hypothesis and proceed as above. (iii) and (iv) (∀ intro) and (∀ elim): proceed as in the previous cases.

The following lemmas show more clearly the relationship between derivations in system F and in Co^{⊢}.

Lemma 6 (F-invertibility with respect to the rules of Co^{⊢}) Let x: σ ⊢ M : τ be a sequent and assume that it is obtained from some other sequent(s) S_{1} ≡ y_{1} :σ_{1} ⊢ M_{1} : τ_{1}, …, S_{n} ≡ y_{n}:σ_{n} ⊢ M_{n} : τ_{n} by application of one of the rules of Co^{⊢}, where y_{i} does occur and is the only free variable of M_{i}. (Note that S_{i} are not necessarily derivable in either Co^{⊢} or F.) Then, if x:σ ⊢ M:τ is derivable in F, then S_{1}, …, S_{n} are also derivable in F.

Proof First, note that if x:σ ⊢ M:τ is derivable in F, then M cannot contain any free variables other than x. Proceed by case analysis of the three System Co^{⊢} rules.

(i) (→):

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

By assumption, the conclusion of this rule is derivable in System F, and thus also the following sequent: x:σ → τ, x′:σ′ ⊢_{F} [xM/y]N : τ′. Apply Lemma 5 to this sequent taking P ≡ [xM/y]N, Q ≡ xM and P′ ≡ N.

Γ_{0} = {x: σ → τ, x′: σ′}, Γ_{1} = ∅ and x: σ → τ, x′: σ′ ⊢_{F} xM : τ, y : τ ⊢_{F} N : τ′. Lemma 5 may be applied again to x: σ → τ, x′: σ′ ⊢_{F} xM : τ taking M as Q. Note that x′:σ′ is the only free variable of M, and we have x′:σ′ ⊢_{F} M : σ. (ii) (∀ left):

{y:[ρ/X]σ ⊢ M : τ \atop x:∀X.σ ⊢ [xρ/y]M : τ}

By assumption, the conclusion of this rule is derivable in System F. Apply Lemma 5 taking P ≡ [xρ/y]M, Q ≡ xρ and P′ ≡ M. Γ_{0} = {x:∀X.σ}, Γ_{1} = ∅ and x:∀X.σ ⊢_{F} xρ:[ρ/X]σ, y:[ρ/X]σ ⊢_{F} M : τ. (iii) (∀ right): it suffices to use properties of λ-introduction in F; Lemma 5 is not needed.

Lemma 7 (One case of invertibility in Co^{⊢}) If x: σ ⊢_{co} λx_{1} : τ_{1} … λx_{k}: τ_{k}.Sρ : τ_{1} → … (τ_{n} → [ρ/Y]τ) …) then x : σ ⊢_{co} λx_{1} : τ_{1} … λx_{k} : τ_{k}.S : τ_{1} → … (τ_{n} → ∀Y.τ) …)

Proof By induction on the Co^{⊢} derivation of the judgement containing Sρ. Base case: since the axiom does not have the form described in the assumption of the lemma, the lemma is vacuously true. Inductive step: analysis of the rules of Co^{⊢} shows that x:σ ⊢_{co} λx_{1} :τ_{1} … λx_{k}:τ_{k}.Sρ : τ_{1} → … (τ_{n} → [ρ/Y]τ) …) cannot be the conclusion of ∀_{n} right.

If it is the conclusion of (→), then its right premise must be of the form y: τ ⊢_{co} λx_{2} : τ_{2} … λx_{k}: τ_{k}.S′ρ : τ_{2} → … (τ_{n} → [ρ/Y]τ) …). Apply the inductive hypothesis and the same rule.

If it is the conclusion of (∀ left), then if S is different from the variable x, apply the inductive hypothesis and the same rule. Suppose S ≡ x. The term λx_{1} :τ_{1} … λx_{k}:τ_{k}.y cannot be obtained by one of the rules of Co^{⊢} if the prefix is non-empty. Thus, the prefix is empty and the premise of (∀ left) is the axiom y:[ρ/X]τ ⊢_{co} y : [ρ/Y]τ. The judgement x:∀X.τ ⊢_{co} x : ∀X.τ is also an axiom. This proves the lemma.

Clearly, Co^{⊢} is strictly weaker than System F. Consider, for example:

x:∀X.X ⊢_{F} x(∀X.X → ∀X.X)x : ∀X.X

but

x:∀X.X ⊬_{co} x(∀X.X → ∀X.X)x : ∀X.X

Even restricting terms to linear ones, and environments to those containing exactly one variable, is not enough to produce a coercion. For example,

x:σ → (τ → ρ) ⊢_{F} λy:τ.λz:σ.(x z y) : τ → (σ → ρ)

is not a coercion. Theorem 19 (completeness) will characterize those System F functions that are coercions.

By the Curry-Howard isomorphism, Co^{⊢} is thus a proper subsystem of intuitionistic (linear) second-order propositional logic. This is only natural since coercions are intended to represent “inclusions” of types. Clearly, there is no reason why arbitrary F-entailment (or even isomorphisms of types) should be interpreted as inclusion.

2.4 Special forms of derivations

Definition 8 (Pure variable derivation) A pure variable derivation is a derivation in which no type variable occurs both free and bound in the same sequent.

This notion of a pure variable derivation is comparable with that used by Kleene (see [Kle67]).

Lemma 9 Every derivation in Co^{⊢} is equal, up to =, to any derivation obtained by safely renaming bound type variables in types and terms, without capturing free type variables.

Proof By induction on the size of the derivation. In the case of (∀ left), use the identity [ρ/X]σ = [ρ/X′]([X′/X]σ) where X′ does not occur free in σ (otherwise X′ would be captured), and in the case of (∀_{n} right), uniformly substitute [X′/X] in the derivation of the premise and then use (∀_{n} right) with X′ instead of X (the side-condition is used). For (→), it is enough to use the induction hypothesis.

Lemma 10 Every derivation in Co^{⊢} is equal, up to =, to a pure variable derivation.

Proof By induction and using the previous lemma (always choosing fresh bound variables).

To illustrate the utility of pure variable derivations, consider the following derivation:

{α_{l} \atop x′:σ′ ⊢_{co} M : σ}  {α_{r} \atop y:τ ⊢_{co} N : τ′} ; (∀_{0} right) ; y:τ ⊢_{co} λX.N : ∀X.τ′
(→)
x:σ → τ ⊢_{co} λx′:σ′ . λX . [xM/y]N : σ′ → ∀X.τ′

By the side-condition on (∀_{0} right), we know that X is not free in τ. Our aim now is to permute the applications of (∀_{0} right) and (→) as follows:

{α_{l} \atop x′:σ′ ⊢_{co} M : σ}  {α_{r} \atop y:τ ⊢_{co} N : τ′}
(→)
x:σ → τ ⊢_{co} λx′:σ′ . [xM/y]N : σ′ → τ′
(∀_{1} right)
x:σ → τ ⊢_{co} λx′:σ′ . λX . [xM/y]N : σ′ → ∀X.τ′

However, this second derivation is only possible if the variable X is not free in σ nor in σ′, as required by (∀_{1} right). This is the case if the first derivation is a pure variable one, for then the X bound in ∀X.τ′ would be fresh.

¿From now on, we will work exclusively with pure variable derivations, referring to them as just “derivations”.

Lemma 11 The following pairs of derivations are equal in Co^{⊢} up to =:

1. \begin{aligned}α \\ & (∀_{n} right) \\ S_{1} \end{aligned} (∀ left) S_{2}  =  \begin{aligned}α \\ & (∀ left) \\ S′_{1} \end{aligned} ; (∀_{n} right) ; S_{2}

2. \begin{aligned}α_{l} & & \begin{aligned}α_{r} \\ & (∀_{n} right) \\ S_{1} \end{aligned} \\ & & (→) \\ & S_{2} \end{aligned}  =  \begin{aligned}α_{l} & & α_{r} \\ & & & (→) \\ & S′_{1} \end{aligned} ; (∀_{n+1} right) ; S_{2}

Proof By simple consideration of the types and terms involved in each sequent. Case 1 applies to any kind of derivation whereas case 2 requires a pure variable derivation. Indeed, the proof of case 2, permuting (∀_{n} right) for n = 0 and (→), is given by the examples of pure variable derivations above. It is checked directly that the terms labeling the end sequents of both the left and right derivations above, are identical (thus, the derivations are equal up to =).

Note that (∀_{n} right) becomes (∀_{n+1} right) when it is permuted downwards with (→). Note also that case 1 applies only when (∀_{n} right) is permuted downwards with (∀ left), not conversely.

Definition 12 (Atomic derivation) An atomic derivation is one in which all axioms are of the form x:X ⊢_{co} x : X.

Lemma 13 Every derivation α in Co^{⊢} is equal, up to =_{η}, to some atomic derivation α′.^{3}

Proof Let α be a derivation of x:σ ⊢_{co} M : τ. If α is not atomic then an axiom of the form x:ρ ⊢_{co} x : ρ where ρ is not a type variable, is used at a leaf. It suffices to prove the thesis for such axioms by induction on the length of types. The base case, when ρ is a type variable, is obvious.

Inductive case: ρ = ∀X.ρ′. Construct the following derivation:

y:[X/X]ρ′ ⊢_{co} y : ρ′
(∀ left)
x:∀X.ρ′ ⊢_{co} xX : ρ′
(∀_{0} right)
x:∀X.ρ′ ⊢_{co} λX.xX : ∀X.ρ′

where λX.xX =_{η} x and apply induction to y:ρ′ ⊢_{co} y : ρ′.

3It will be shown in the next section that coercions are closed under η-conversion.

Inductive case: ρ = ρ_{1} → ρ_{2}. Construct the following derivation:

y:ρ_{1} ⊢_{co} y : ρ_{1} y′:ρ_{2} ⊢_{co} y′ : ρ_{2}
(→)
x:ρ_{1} → ρ_{2} ⊢_{co} λy:ρ_{1}.xy : ρ_{1} → ρ_{2}

where λy:ρ_{1}.xy =_{η} x and apply induction to y:ρ_{1} ⊢_{co} y : ρ_{1} and y′:ρ_{2} ⊢_{co} y′ : ρ_{2}.

In the following lemma, we “transform” atomic derivations to a useful form (for later purposes) by permuting rules as appropriate.

Lemma 14 Let α be an atomic derivation of x : σ ⊢_{co} M : τ_{1} → (… (τ_{n} → ∀X.τ) …). Then, there exists an atomic derivation α′ = α, with α and α′ of equal size, and where (∀_{n} right) is the last rule used in α′.

Proof Proceed by induction on the derivation of α. Clearly, (ax) cannot have been used, and if (∀_{n} right) was used last in α, then we are done. In the other two cases, use Lemma 11 to permute rules as follows:

Case: (∀ left) used last. Apply the induction hypothesis to the premise then permute (∀ left) with (∀_{n} right) (Lemma 11, case 1).

Case: (→) used last. Apply the induction hypothesis to the left premise then permute (→) with (∀_{n−1} right), the latter becoming (∀_{n} right) in the final derivation (Lemma 11, case 2).

Lemma 15 Let α_{1} and α_{2} be two atomic derivations of x:σ ⊢_{co} M:τ and x:σ ⊢_{co} N: τ respectively. Then, there exist atomic derivations α′_{1} = α_{1} and α′_{2} = α_{2} such that α′_{1} and α′_{2} end with the same rule and have the same size as α_{1} and α_{2}, respectively.

Proof If α_{1} and α_{2} end with the same rule, then, trivially, we are done. Otherwise, based on the structure of σ and τ, it is sufficient to consider two cases: either α_{1} ends with (∀_{n} right) and α_{2} with (→), or α_{1} ends with (∀_{n} right) and α_{2} with (∀ left) (the combination of (→) and (∀ left) is structurally impossible).

In the first case, the end sequent in both derivations must be of the form x:σ ⊢_{co} M : τ_{1} → ∀X.τ_{2}. Apply then Lemma 14 to α_{2} yielding a derivation α′_{2} = α_{2} ending with (∀_{n} right) of equal size, and take α′_{1} ≡ α_{1}. The second case is treated likewise. If α_{1} ends with (∀_{n} right), apply Lemma 14 to α_{2} yielding a derivation α′_{2} = α_{2} ending with (∀_{n} right) and of equal size. Take α′_{1} ≡ α_{1}.

2.5 The transitivity problem

In section 3.3, we will show that ⊢_{co} is a transitive relation. That is, in the unlabeled system, the rule:

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

is admissible.

Its labeled version needs some discussion. A “naive” variant would be:

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

But note that the term [M/y]N may not be a coercion; in particular, it may not be in β-nf (cf. Lemma 4). However, without making use of the strong normalization property of System F, we can prove that [M/y]N normalizes:

Lemma 16 Assume that x: σ ⊢_{co} M : τ and y : τ ⊢_{co} N : ρ. Then, there exists a unique, finite path of β-reductions from [M/y]N. Consequently, there exists a unique β-nf of [M/y]N.

Proof By the linearity of coercions (Lemma 2), M and N are linear, and so the term [M/y]N is also linear (remember that the only free term variable of M is x and of N is y). Observe then that, because M and N are in β-nf (Lemma 4), only one β-redex may exist in [M/y]N. And each subsequent β-reduction from [M/y]N preserves linearity and may introduce only one new β-redex. Furthermore, each such β-reduction decreases the number of λs, say n, originally in [M/y]N. Thus, there is a unique path, with at most n steps, of β-reductions from [M/y]N.

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) : ρ}

Our aim will be to show that x:σ ⊢_{co} nf_{β}([M/y]N) : ρ is actually a coercion (i.e., derivable in Co^{⊢}). In other words, that the rule above is admissible.

Note that (cut) is a “cut” rule in the usual sense of sequent calculi. Thus, proving the admissibility of (cut) is equivalent to proving a cut-elimination theorem for the extended system Co^{⊢} plus (cut). Observe too that subject reduction is vacuously true in the extended system: all terms in Co^{⊢} plus (cut) are in β-nf.

3 Completeness, transitivity and coherence

3.1 Completeness of Co^{⊢}

The standard notion of erasure, defined as follows, will serve to characterize coercions.

Definition 17 (Erasure) The erasure of a polymorphic term to a type-free term is defined by: erase(x) ≡ x

erase(λx:σ.M) ≡ λx.erase(M)  erase(MN) ≡ erase(M)erase(N)
erase(λX.M) ≡ erase(M)  erase(Mτ) ≡ erase(M)

By straightforward induction on derivations, one shows that the erasure of a coercion η-reduces to the identity (in the type-free λ-calculus).

Lemma 18 If x:σ ⊢_{co} M:τ then erase(M)⟶_{η} x.

Conversely, we will now show that any System F term in β-nf whose erasure ηreduces to a term variable is a coercion. This will give a complete characterization of coercions. Moreover, it will be a key step in the proof of transitivity of ⊢_{co} and in relating our system to that of Mitchell [Mit88] (section 4). The proof proceeds by syntactic analysis of the normal form.

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

Proof By the assumption that M is in β-nf, M must have the following structure:

M ≡ λY⃗_{1} . λy_{1} :τ_{1} …. λY⃗_{k} . λy_{k}:τ_{k} . λY⃗_{k+1} . x′ρ⃗_{1}M_{1} … ρ⃗_{n}M_{n}ρ⃗_{n+1}

with each subterm M_{i}, for 1 ≤ i ≤ n, in β-nf. Furthermore, the assumption erase(M) ⟶_{η} x implies that x′ ≡ x, k = n and erase(M_{i}) ⟶_{η} y_{i} for 1 ≤ i ≤ n. The fact that erase(M_{i}) ⟶_{η} y_{i} means that y_{i} is the only free term variable in M_{i}. So, by lemma 5: y_{i}: τ_{i} ⊢_{F} M_{i} : σ_{i}. (The concrete form of σ_{i} may be found but we don’t need it.)

We thus have that the subterms M_{i}, 1 ≤ i ≤ n, are in β-nf with erase(M_{i}) ⟶_{η} y_{i} and y_{i}: τ_{i} ⊢_{F} M_{i} : [ρ⃗_{1}/X⃗_{1}, …, ρ⃗_{i}/X⃗_{i}]σ_{i}. The proof now proceeds by induction on the size of M. Base case: M ≡ x is trivial. Inductive step: three cases as follows.

a) Case: at least one of the lists Y⃗_{k} is non-empty. M then has the form

M ≡ λy_{1} :τ_{1} …. λy_{i−1}λY⃗_{i} . λy_{i}:τ_{i} …. λY⃗_{n}.λy_{n} . λY⃗_{n+1} . xρ⃗_{1}M_{1} … ρ⃗_{n}M_{n}ρ⃗_{n+1}

where Y⃗_{i} is the leftmost of such lists. The type τ of M is

τ = (τ_{1} → … → ∀Y⃗_{i}.(τ_{i} → … ∀Y⃗_{n}.(τ_{n} → ∀Y⃗_{n+1}.σ′) …)

Consider the term M′ obtained by erasing only λY⃗_{i} and the type τ′ of M′:

τ′ = (τ_{1} → … → (τ_{i} → … ∀Y⃗_{n}.(τ_{n} → ∀Y⃗_{n+1}.σ′) …)

The judgement x : σ ⊢ M : τ is derivable from the judgement x : σ ⊢ M′ : τ′ by repeated (∀_{i} right). By lemma 6, x: σ ⊢_{F} M : τ implies x: σ ⊢_{F} M′ : τ′. Obviously erase(M′) ≡ erase(M) ⟶_{η} x. Thus, by inductive hypothesis, x : σ ⊢_{co} M′ : τ′. Now, by (∀_{i} right), x:σ ⊢_{co} M : τ.

b) Case: all Y⃗_{i} are empty but ρ⃗_{1} is non-empty. The term M has the structure

M ≡ λy_{1} :τ_{1} … λy_{n} . . xρ⃗_{1}M_{1} … ρ⃗_{n}M_{n}ρ⃗_{n+1}

Notice that x : σ ⊢_{F} xρ⃗_{1} : σ_{0} for certain σ_{0} since xρ⃗_{1} is a subterm of an F-term (lemma 5). Moreover, x:σ ⊢_{co} xρ⃗_{1} : σ_{0} (it may be derived by ∀_{left} in Co^{⊢} ). Let M′ be obtained by replacement of xρ_{1} by a fresh variable z.

The judgement x : σ ⊢_{F} M : τ is derived by (∀ left) from z : σ_{0} ⊢ M′ : τ. By lemma 6, z: σ_{0} ⊢_{F} M′ : τ. Obviously, erase(M′) ⟶_{η} z because erase(M) ⟶_{η} x. By inductive hypothesis, z:σ_{0} ⊢_{co} M′ : τ and by (∀ left), x:σ ⊢_{co} M : τ. c) Case: all Y⃗_{i} are empty and ρ⃗_{1} is empty but n ≥ 0 (else we have the base case). The type τ of M is

τ = (τ_{1} → … → (τ_{n} → σ′) …)

We need also the type τ′

τ′ = (τ_{2} → … → (τ_{n} → σ′) …)

By inductive hypothesis, we may assume that the subterm M_{1} is a coercion: y_{1} :τ_{1} ⊢_{co} M_{1} : σ_{1}.

Consider the term M′ obtained by erasure of λy_{1} and replacement of xM_{1} by a fresh variable z; the type of z is easily derived since xM_{1} is an F-term. The type of x must be some σ ≡ σ_{1} → σ′_{1} and x: σ ⊢_{F} xM_{1} : σ′_{1}. The judgement x: σ ⊢_{F} M : τ is derived by the rule → from z: σ′_{1} ⊢ M′ : τ′. Thus, by lemma 6 z: σ′_{1} ⊢_{F} M′ : τ′. Obviously, erase(M′) ⟶_{η} z. By inductive hypothesis, z: σ′_{1} ⊢_{co} M′ : τ′ and by the rule (→), x:σ ⊢_{co} M : τ.

Since η-reductions and expansions do not affect the property erase(M) ⟶_{η} x, we have the following corollary.

Corollary 20 For M in β-nf, assume that x:σ ⊢_{F} M : τ and M ⟶_{η} M′. Then, x:σ ⊢_{co} M : τ iff x:σ ⊢_{co} M′ : τ.

Since coercions are in β-normal form, this amounts to the subject reduction property for coercions.

3.2 Equality =_{ηco}

Equality of coercions is defined, essentially, by η-equality plus a coercion version of the F_{≤} [CMMS91] rule (eq appl2). Since coercions are in β-normal form, β-equality need not be considered and we showed previously that coercions are closed with respect to η-equality. The corecion version of (eq appl2) is motivated by Mitchell’s system and semantical considerations based for example on PER models (see section 6.3).

Let us write x: σ ⊢_{co} M =_{ηco} N : τ to mean that M and N are equal coercions from σ to τ. This relation is defined as follows.

Definition 21 (Equality of coercions) =_{ηco} is the least equivalence relation generated by α-convertibility and the two rules

(eq η)  {x:σ ⊢_{co} M : τ  x:σ ⊢_{co} M′ : τ  M =_{η} M′ \atop x:σ ⊢_{co} M =_{ηco} M′ : τ}

(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} : μ}

plus two other rules, (eq →) and (eq ∀_{n} right), which state, respectively, that (→) and (∀_{n} right) preserve equality of coercions. (eq →) and (eq ∀_{n} right) are given in full in the appendix.

Note that (eq appl2 co) implies that (∀ left) preserves equality of coercions: given y: [ρ/X]σ ⊢_{co} M =_{ηco} N: τ, apply (eq appl2 co) with τ_{1} ≡ τ_{2} ≡ ρ and N_{1} ≡ M and N_{2} ≡ N to obtain x:∀X.σ ⊢_{co} [xρ/y]M =_{ηco} [xρ/y]N : τ.

The rules (eq →) and (eq ∀_{n} right) are derivable in system F using β-convertibility. Rule (eq appl2 co), on the other hand, is not derivable in system F as it equates terms that are not β-convertible, as shown by the following instance of the rule.

y_{1} : [τ_{1}/X]Y ⊢_{co} y_{1} : Y y_{2} : [τ_{2}/X]Y ⊢_{co} y_{2} : Y

(eq appl2 co)

x:∀X.Y ⊢_{co} [xτ_{1}/y_{1}]y_{1} =_{ηco} [xτ_{2}/y_{2}]y_{2} : Y

Thus, xτ_{1} =_{ηco} xτ_{2} whereas xτ_{1} ≠_{βη} xτ_{2} in general, i.e., they are not equal in System F. Clearly, though, xτ_{1} and xτ_{2} are equal in F_{≤} [CMMS91] using the corresponding “non-coercion” F_{≤} rule (eq appl2); see section 1.1.

Here are two examples to illustrate =_{ηco} (recall that ⊥ = ∀X.X). Note that these equalities are not provable in system F.

Example: x:⊥ ⊢_{co} x =_{ηco} x⊥ : ⊥

y_{1} :[X/X]X ⊢_{co} y_{1} : X  y:[X/X]X ⊢_{co} y : X ; (∀ left) ; y_{2} :[⊥/X]X ⊢_{co} y_{2}X : X

(eq appl2 co)

x:⊥ ⊢_{co} xX =_{ηco} x⊥X : X

(eq ∀_{0} right)
x:⊥ ⊢_{co} λX.xX =_{ηco} λX.x⊥X : ⊥
(eq η)
x:⊥ ⊢_{co} x =_{ηco} x⊥ : ⊥

Example: x:∀X . X → X ⊢_{co} λy:⊥ . λX . xX(yX) =_{ηco} x⊥ : ⊥ → ⊥

\begin{aligned}y′:X ⊢_{co} y′ : X ; (∀ left) ; y:⊥ ⊢_{co} yX : X & x′:X ⊢_{co} x′ : X \\ & (→) \\ y_{1} :X → X ⊢_{co} λy:⊥ . y_{1}(yX) : ⊥ → X \end{aligned} \begin{matrix}y:⊥ ⊢_{co} y : ⊥ & y′:X ⊢_{co} y′ : X ; (∀ left) ; x′:⊥ ⊢_{co} x′X : X \\ (→) \\ y_{2} :⊥ → ⊥ ⊢_{co} λy:⊥ . y_{2}yX : ⊥ → X \end{matrix}

(eq appl2 co)

x:∀X.X → X ⊢_{co} λy:⊥ . xX(yX) =_{ηco} λy:⊥ . x⊥yX : ⊥ → X

(eq ∀_{1} right)

x:∀X.X → X ⊢_{co} λy:⊥ . λX . xX(yX) =_{ηco} λy:⊥ . λX . x⊥yX : ⊥ → ⊥

As well as equality of terms, we will need equality of derivations, defined by the following three relations:

Definition 22 (Equality of derivations) Let α_{1} be a derivation of x: σ ⊢_{co} M : τ and α_{2} a derivation of x:σ ⊢_{co} N : τ. We write:

• α_{1} = α_{2} iff M ≡ N

• α_{1} =_{η} α_{2} iff x:σ ⊢_{co} M =_{η} N
• α_{1} =_{ηco} α_{2} iff x:σ ⊢_{co} M =_{ηco} N.

3.3 Transitivity of ⊢_{co}

We now prove that ⊢_{co} is a transitive relation. More formally, we will prove that:

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

is an admissible rule in Co^{⊢}.

Lemma 23 Assume that x:σ ⊢_{co} M : τ and y:τ ⊢_{co} N : ρ. Then erase (nf_{β} ([M/y]N)) =_{η} nf_{β} (erase ([M/y]N)).

Proof Note first that, by an argument similar to the proof of Lemma 16, there exists a unique β-nf of erase([M/y]N), i.e., nf_{β}(erase([M/y]N)) does indeed exist. The only difference is that there will be no β_{2}-reductions in the path from erase([M/y]N). Next, by Lemma 16 directly, nf_{β}([M/y]N) exists. Finally, the erasure of nf_{β}([M/y]N) is clearly η-equivalent to the unique β-nf of erase([M/y]N).

Theorem 24 (Transitivity) (cut) is an admissible rule in Co^{⊢}.

Proof Assume that x:σ ⊢_{co} M : τ and y:τ ⊢_{co} N : ρ. By Lemma 16, nf_{β}([M/y]N) exists. Since x: σ ⊢_{F} [M/y]N : ρ, then, by subject reduction in System F, x: σ ⊢_{F} nf_{β}([M/y]N) : ρ. Furthermore, since coercions erase to the identity (Lemma 18), erase(M)⟶_{η} x and erase(N)⟶_{η} y. Then:

erase(nf_{β}([M/y]N)) =_{η} nf_{β}(erase([M/y]N))  by Lemma 23
≡ nf_{β}([erase(M)/y]erase(N))
=_{η} x

Finally, by completeness of Co^{⊢} (Theorem 19), x:σ ⊢_{co} nf_{β}([M/y]N) : ρ.

Notice that proving the admissibility of (cut) for the system Co^{⊢} is equivalent to proving a cut-elimination theorem for the extended system Co^{⊢}+(cut). See section 6.4 for a discussion of second-order cut-elimination proofs.

As pointed out in the introduction, if we had taken (cut) as a primitive of the system, then we would have had to eliminate it in any case in order to prove coherence. Moreover, (cut) as primitive would imply that coercions could “compute on themselves” (even without inputs), whereas the coercions provided by Co^{⊢} are guaranteed to be in β-nf. Thus, they only transform an element of a type to a supertype without any other kind of computation.

3.4 Coherence of Co^{⊢}

By coherence, we mean that a coercion from type σ to type τ is independent of its derivation in Co^{⊢}in the sense that, if a coercion from σ to τ exists, then it is unique, up to =_{ηco}.

We are now in a position to prove the coherence of Co^{⊢} derivations. Note that this is where =_{ηco} is used, and thus the strength of the rule (eq appl2 co); we display it first in a lemma.

Lemma 25 Let α_{1} and α_{2} be two derivations of x: σ ⊢_{co} M : τ and x: σ ⊢_{co} N : τ ending with (∀ left). Then, α_{1} =_{ηco} α_{2}.

Proof Let σ ≡ ∀X.σ′, M ≡ [xτ_{1}/y_{1}]N_{1} and N ≡ [xτ_{2}/y_{2}]N_{2}. The final steps in α_{1} and α_{2} are respectively:

{α_{l} \atop y_{1} :[τ_{1}/X]σ′ ⊢_{co} N_{1} :τ} ; (∀ left) ; x:∀X.σ′ ⊢_{co} [xτ_{1}/y_{1}]N_{1} :τ  {α_{r} \atop y_{2} :[τ_{2}/X]σ′ ⊢_{co} N_{2} :τ} ; (∀ left) ; x:∀X.σ′ ⊢_{co} [xτ_{2}/y_{2}]N_{2} :τ

Now, use (eq appl2 co) on both premises:

{α_{l} \atop y_{1} :[τ_{1}/X]σ′ ⊢_{co} N_{1} :τ}  {α_{r} \atop y_{2} :[τ_{2}/X]σ′ ⊢_{co} N_{2} :τ}

(eq appl2 co)

x:∀X.σ′ ⊢_{co} [xτ_{1}/y_{1}]N_{1} =_{ηco} [xτ_{2}/y_{2}]N_{2} : τ

Hence, by definition, α_{1} =_{ηco} α_{2}.

Theorem 26 (Coherence of Co^{⊢} derivations) Let α_{1} and α_{2} be two derivations of x:σ ⊢_{co} M:τ and x:σ ⊢_{co} N:τ respectively. Then, α_{1} =_{ηco} α_{2}.

Proof By Lemma 13, we may assume α_{1} and α_{2} to be atomic derivations, up to =_{η}. The proof then proceeds by induction on n = max{size(α_{1}), size(α_{2})}. By lemma 15, there exist atomic derivations α′_{1} = α_{1}, α′_{2} = α_{2} such that α′_{1} and α′_{2} end with the same rule and have the same size as α_{1} and α_{2} (respect.). Notice that, if the final rule applied is (→) or (∀_{n} right), then the premises in both derivations are the same. Base case, n = 0: Both derivations are atomic axioms (trivial). Inductive step, n ≥ 1: There are three subcases: Case: (∀ left) is used last. Then, lemma 25 suffices. Note that, in this case, we do not need to apply the induction hypothesis. Cases: (→) or (∀_{n} right) are used last, the same in both derivations. Then, the respective premises of the last rule in both derivations coincide. Use then the induction hypothesis on these premises, followed by the equality rules (eq →) or (eq ∀_{n} right). Thus α_{1} =_{ηco} α_{2}.

It will be an easy corollary of coherence and the transitivity of ⊢_{co} (section 3.3) that x: σ ⊢_{co} M : τ and x: τ ⊢_{co} N : σ implies that σ is isomorphic to τ. In other words, ⊢_{co} is anti-symmetric up to isomorphism.

3.5 Bicoercibility

Consider now the term model | Co^{⊢} | of Co^{⊢}, i.e., the structure whose objects are types and arrows are coercions. | Co^{⊢} | is a category. Indeed, by (ax), it contains all identities. By the transitivity of ⊢_{co}, coercions (arrows) compose: just observe that if

x:σ ⊢_{co} M : τ and y:τ ⊢_{co} N : ρ

then there exists P such that x: σ ⊢_{co} P : ρ and P is unique by coherence. As for associativity, this is again given by coherence.

| Co^{⊢} | is even a partial order: by the corollary below, anti-symmetry of ⊢_{co} is a consequence of coherence and transitivity of entailment. Define first the following relation of bicoercibility between types:

Definition 27 (Bicoercibility) Two types σ and τ are bicoercible, written σ ≅ ; b τ, iff σ ⊢_{co} τ and τ ⊢_{co} σ.

For example, τ ≅ ; b ∀X.τ for X not free in τ. Now, recall that, in a category, two objects 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, one can prove the following:

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

Proof By assumption, x : σ ⊢_{co} M : τ and y : τ ⊢_{co} N : σ. By (cut), we obtain x : σ ⊢_{co} nf_{β}([M/y]N) : σ and y : τ ⊢_{co} nf_{β}([N/x]M) : τ, then, by coherence, nf_{β}([M/y]N) =_{ηco} x and nf_{β}([N/x]M) =_{ηco} y.

Note that bicoercibility is strictly stronger than isomorphism: the type σ → (τ → ρ) is isomorphic to τ → (σ → ρ) (see [Sol83, BDL92] for a characterisation) but it is clearly not a subtype, and so not bicoercible. Tiuryn in [Tiu95] has shown that bicoercibility is decidable, while Tiuryn and Urzyczyn [TU96] have shown that coercibility ⊢_{co}, that is, subtyping, is undecidable.

As pointed out, |Co^{⊢} | is a category and a partial order. This allows a preliminary observation on adding base types (int, real, etc.) with axioms introducing ⊢_{co} between these types (e.g., int ⊢_{co} real). In short, one obtains the freely generated partial order, from these base types, by our axioms and rules. A proof-theoretic analysis of this fact will be given in Section 5.

4 Mitchell’s subtyping system

In [Mit88], a “retyping function” is defined as a typed term in System F whose erasure η-reduces to the identity. In [Mit88, Lemma 9], it is then shown that σ is a subtype of τ in all “simple inference models” (as defined in [Mit88, section 4.2]) if and only if there is a retyping function from σ to τ. Thus, our Theorem 19 also yields semantic completeness, in the sense of Mitchell, for Co^{⊢}. In this section, we give a direct comparison of Co^{⊢} to Mitchell’s axiomatic approach to subtyping, presented here in a revised (but clearly equivalent) way.

Mitchell’s Subtyping System

(ax)  σ ≤ σ  (trans)  {σ ≤ τ  τ ≤ ρ \atop σ ≤ ρ}

(→)  {σ′ ≤ σ  τ ≤ τ′ \atop (σ → τ) ≤ (σ′ → τ′)}  (∀ subst) {σ ≤ τ \atop ∀X.σ ≤ ∀X.τ}

(∀ intro)  σ ≤ ∀X.σ  (∀ elim) ∀X.σ ≤ [ρ/X]σ
∗ for X not ; free in σ

(∀→ distr)  ∀X.(σ → τ) ≤ (∀X.σ) → (∀X.τ)

It is not hard to show that the unlabeled system Co^{⊢} and Mitchell’s system are equivalent.

Theorem 29 σ ≤ τ iff σ ⊢_{co} τ.

Proof Clearly, rules (ax) and (→) are identical in the two systems (with ⊢_{co} for ≤). For the implication from left to right, the rule (trans) in Mitchell’s system above corresponds to the Co^{⊢} rule (cut) which, by Theorem 24, is admissible for Co^{⊢}; the other cases in this direction are proven as follows: Case: (∀ intro) is derivable in Co^{⊢} since X is not free in σ

\frac{σ ⊢_{co} σ}{σ ⊢_{co} ∀X.σ} (∀_{0} right)

Case: (∀ elim) is derivable in Co^{⊢}

\frac{[ρ/X]σ ⊢_{co} [ρ/X]σ}{∀X.σ ⊢_{co} [ρ/X]σ} (∀ left)

Case: (∀ subst) is derivable in Co^{⊢}

\frac{[X/X]σ ⊢_{co} τ}{∀X.σ ⊢_{co} τ} (∀ left)
\overline{∀X.σ ⊢_{co} ∀X.τ} (∀_{0} right)

Case: (∀→ distr) is derivable in Co^{⊢}+(cut)

\underline{∀X.σ ⊢_{co} σ  τ ⊢_{co} τ} (→) ∀X.(σ → τ) ⊢_{co} σ → τ  σ → τ ⊢_{co} (∀X.σ) → τ \overline{∀X.(σ → τ) ⊢_{co+cut} (∀X.σ) → τ}  (cut)
\overline{∀X.(σ → τ) ⊢_{co+cut} (∀X.σ) → (∀X.τ)}  (∀_{1} right)

Conversely, the remaining cases of the implication from right to left are proven as follows: Case: (∀ left) is derivable in Mitchell’s system by

∀X.σ ≤ [ρ/X]σ ≤ τ

using (trans) on (∀ elim) and the premise of (∀ left), i.e., [ρ/X]σ ≤ τ. Case: (∀_{n} right) is derivable in Mitchell’s system as follows:

σ ≤ ∀X.σ  by (∀ intro) and (∀_{n} right) side-condition X not free in σ
≤ ∀X.(τ_{1} → … (τ_{n} → τ) …)  by (∀ subst) on (∀_{n} right) premise
≤ (∀X.τ_{1}) → ∀X.(τ_{2} → … (τ_{n} → τ) …)  by (∀→ distr)
≤ (∀X.τ_{1}) → ((∀X.τ_{2}) → ∀X.(τ_{3} → … (τ_{n} → τ) …)by (∀→ distr) and (→)
≤ ⋮
≤ (∀X.τ_{1}) → ((∀X.τ_{2}) → … ((∀X.τ_{n}) → (∀X.τ) …)

by (∀→ distr) and (→)

≤ τ_{1} → (∀X.τ_{2}) → … (∀X.τ_{n}) → (∀X.τ) …)

by (→), (∀ intro) and (∀_{n} right) side-condition X not free in τ_{1}

≤ ⋮
≤ τ_{1} → (τ_{2} → … (τ_{n} → ∀X.τ) …)

by (→), (∀ intro) and (∀_{n} right) side-condition X not free in τ_{n}

5 Coercions and base types

This section extends the results of the previous sections to subtyping systems containing coercions between base types.

5.1 Systems F +B and Co^{⊢}+B

Consider extending the language of Co^{⊢} with type constants κ_{1}, κ_{2}, κ_{3}, ... For example, these could be base types such as bool, int, real. As in the case of Co^{⊢}, the extended system will be considered together with the corresponding extension of System F.

System F +B is obtained by adding to the language of System F type constants κ_{1}, κ_{2}, κ_{3}, ... and term constants c_{i,j} for each i, j such that a subtyping relation holds between κ_{i}, κ_{j}, and adding an axiom (with Γ an arbitrary context)

Γ ⊢_{F +B} c_{i,j} : κ_{i} → κ_{j}

System Co^{⊢}+B is defined in its labeled and unlabeled versions, with the language extended in the same way as for System F. In the labeled Co^{⊢}+B system, the following Gentzen-style rule is added:

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

It is a derivable rule with respect to system F +B. In its unlabeled version, this rule takes the form:

(κ_{i} ≤ κ_{j}) {σ ⊢ κ_{i} \atop σ ⊢ κ_{j}}

Let ⊢_{co+B} denote entailment in this extended system. What happens then to the subtyping partial order and the coherence and transitivity properties of the “pure” calculus Co^{⊢}?

First, observe that the expected subtyping judgment x: κ_{i} ⊢_{co} c_{i,j} x : κ_{j} is easy to derive: just take σ = κ_{i} and M ≡ x in the above rule. Indeed, as we now show, the new constants and rules introduce no new subtyping judgments beyond those expected. In a sense, base coercions act like variables; they do not compute.

Lemma 30 (Conservativity of Co^{⊢}+B with respect to Co^{⊢}) Assume that types σ and τ do not contain occurrences of base types. Consider x:σ ⊢_{co+B} M : τ (in the labeled system). If M contains neither base types nor c_{i,j}, then x: σ ⊢_{co} M : τ. In the unlabeled system, if σ ⊢_{co+B} τ then σ ⊢_{co} τ.

Proof First, let α be a Co^{⊢}+B derivation (labeled or unlabeled) of a sequent S, where S may contain base types. Observe that by uniformly substituting in α, a fresh variable X for all base types κ_{1}, … κ_{n} and omitting the (κ_{i} ≤ κ_{j}) rules, we obtain a Co^{⊢} derivation of [X/κ_{1}, …, X/κ_{n}]S. This is easily shown by induction on Co^{⊢}+B derivations. The lemma then holds as a corollary of this observation.

5.2 Structural lemmas concerning base types

We will require notions of equality on Co^{⊢}+B derivations, defined similarly to the equalities on Co^{⊢} derivations (see section 3.2), and for which we will use the same symbols: =, =_{η}, =_{ηco}. At the moment, we need only =. (Recall that two derivations are = when the proof terms labeling their final sequents are syntactically identical.)

Lemma 31 A (κ_{i} ≤ κ_{j}) rule cannot be applied at any point after an application of either (∀_{n} right) or (→).

Lemma 32 A (κ_{i} ≤ κ_{j}) rule can be permuted with (∀ left) in both directions (the labels are not changed and the size of the new derivation is the same as the original one):

\begin{matrix}\frac{S_{1}}{S_{2}} & (κ_{i} ≤ κ_{j}) \\ \overline{S_{3}} & (∀ left) \end{matrix}  =  \begin{matrix}\frac{S_{1}}{S′_{2}} & (∀ left) \\ \overline{S_{3}} & (κ_{i} ≤ κ_{j}) \end{matrix}

Lemma 33 Assume σ ⊢_{co+B} τ with derivation α.

1) If τ contains neither → nor ∀, then α may contain applications of only (ax), (κ_{i} ≤ κ_{j}), and (∀ left).

2) If σ contains neither → nor ∀, then α may contain applications of only (ax), (κ_{i} ≤ κ_{j}), and (∀_{0} right).

Proof By induction on the size of α in both cases. Note that, in both cases, the derivations have just one branch.

Lemma 34 (Subtypes and supertypes of a base type)

1) Let σ ⊢_{co+B} κ. Then, σ = ∀X_{l} … ∀X_{1}.σ′, for some l ≥ 0 with σ′ either a base type κ′ or a variable X_{i} for i ∈ 1 … l.

2) Let κ ⊢_{co+B} τ. Then, τ = ∀X_{m} … ∀X_{1}.κ′ for some base type κ′ and m ≥ 0.

Proof Consider statement 1). By Lemma 33 case 1, the derivation of σ ⊢_{co+B} κ consists of applications of only (ax), (κ_{i} ≤ κ_{j}), and (∀ left). The derivation is linear, not a tree. The applications of (κ_{i} ≤ κ_{j}) can be permuted by Lemma 32 with the applications of (∀ left), if any. Furthermore, (ax) must be of the form κ′ ⊢_{co+B} κ′. Thus, an equal derivation of σ ⊢_{co+B} κ may be constructed with the following structure:

κ′ ⊢_{co+B} κ′  (ax)
(∀ left)
⋮ ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ′} (∀ left)
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ_{p}} (κ′ ≤ κ_{p})
\overline{⋮}  ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ_{q}}  ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ} (κ_{q} ≤ κ)

where k ≥ 0 is the number of applications of (κ_{i} ≤ κ_{j}) rules, i.e., (κ′ ≤ κ_{p}), …, (κ_{q} ≤ κ), and l′ ≥ 0 is the number of applications of (∀ left). Note that l ≤ l′.

Consider statement 2). By Lemma 33 case 2, the derivation of κ ⊢_{co+B} τ can contain applications of only (ax), (κ_{i} ≤ κ_{j}), and (∀_{0} right). By Lemma 31, all the applications of the (κ_{i} ≤ κ_{j}) rules must appear before those of (∀_{0} right). Furthermore, (ax) must be of the form κ ⊢_{co+B} κ. Hence, the derivation has the following structure:

κ ⊢_{co+B} κ  (ax)
\overline{κ ⊢_{co+B} κ_{p}}  (κ ≤ κ_{p})
⋮
⋮  ⋮ \overline{κ ⊢_{co+B} κ_{q}}  ⋮
\overline{κ ⊢_{co+B} κ′}  (κ_{q} ≤ κ′)
\overline{κ ⊢_{co+B} ∀X_{1}.κ′}  (∀_{0} right)
⋮
⋮ ⋮
\overline{κ ⊢_{co+B} ∀X_{m} … ∀X_{1}.κ′} (∀_{0} right)

where k ≥ 0 is the number of applications of (κ_{i} ≤ κ_{j}) rules, i.e., (κ ≤ κ_{p}), …, (κ_{q} ≤ κ′), and m ≥ 0 is the number of applications of (∀_{0} right).

Corollary 35

1) Let x : σ ⊢_{co+B} M : κ. Then, M ≡ c_{k}(… c_{1}(xρ_{l′} … ρ_{1}) …) where c_{1}, …, c_{k} denote c_{i,j} for corresponding i, j and [ρ_{l′}/X_{l}] (… ([ρ_{1}/X]σ) …) = κ′ ^{4}.

4The number l′ need not be equal to l since the types ρ may themselves contain ∀.

2) Let x:κ ⊢_{co+B} M:τ. Then, M ≡ λX_{m} … λX_{1} . c_{k}(… c_{1}x) …)

Note that the permutations of rules described in the lemma change neither labels nor the size of the derivations.

Lemma 34 shows that adding extra base types and base coercions changes the subtyping partial order in a reasonable way: each base type has only itself, the empty type, or other base types, given by the extra subtyping rules, as its subtypes (up to bicoercibility, of course). Indeed, for case 1 of Lemma 34, σ ≅ ; b κ′ or σ ≅ ; b ∀X.X, while for case 2, τ ≅ ; b κ′.

Modifications to structural lemmas of section 2.3

Adding base types changes little of most of the formulations and proofs of section 2.2. Systems Co^{⊢} and F should be replaced everywhere by Co^{⊢}+B and F +B respectively. Sometimes an extra case should be considered in the proof: for example, lemma 5 for the case when the rule r is a base type rule.

The definition of an atomic derivation (definition 12) is modified as follows:

Definition 36 (Atomic derivation with base types) An atomic derivation is one in which, for any base type κ, all axioms are of the form x: X ⊢_{co+B} x : X or x: κ ⊢_{co+B} x : κ in the labeled system, and of the form X ⊢_{co+B} X or κ ⊢_{co+B} κ in the unlabeled system, respectively.

Only lemma 15 is modified more seriously as follows.

Lemma 37 Let α_{1} and α_{2} be two atomic derivations of x : σ ⊢_{co+B} M : τ and x : σ ⊢_{co+B} N : τ respectively. Then, there exist atomic derivations α′_{1} = α_{1} and α′_{2} = α_{2} such that α′_{1} and α′_{2} have the same size as α_{1} and α_{2}, respectively, and

• either both end with the same rule,

• or at least one ends with a base type rule.

Proof In the case when both derivations end with some rule that is not a base type rule, the modified versions of lemma 11 and lemma 31 should be used instead of lemma 11. If at least one ends with a base type rule, then lemma 34 is applied.

To the modified version of lemma 16 (which asserts that if M, N are Co^{⊢}+B terms, then the β-nf of [M/x]N exists and the reduction is linear), one may add the following obvious observation: if M ≡ c_{i,j}M′ then [M/x]N is β-normal.

5.3 Completeness of Co^{⊢}+B

The definition of erasure (see section 3.1) must also be extended to account for base coercions.

Definition 38 (Erasure of base coercions) erase(c_{i,j} M) ≡ erase(M).

Lemma 39 If x:σ ⊢_{co+B} M:τ then erase(M)⟶_{η} x.

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

Proof Almost identical to the proof of completeness for the pure system Co^{⊢} (Theorem 19). Since c_{i,j} has the type k_{i} → k_{j}, M, in β-nf, has the following general structure:

M ≡ λY⃗_{1} . λy_{1} :τ_{1} … λY⃗_{k} . λy_{k}:τ_{k} . λY⃗_{k+1} . c_{1}(… (c_{l}(xρ⃗_{1}M_{1} … ρ⃗_{n}M_{n}ρ⃗_{n+1})) …)

First the same cases as in theorem 19 are considered (using modified lemmas). Then if none of them apply, lemma 34 and its corollary 35 may be used.

Corollary 20 holds for Co^{⊢}+B (i.e., one has the subject reduction property for Co^{⊢}+B).

5.4 Transitivity

The fact that modified lemma 16 holds for Co^{⊢}+B terms justifies the definition of cut (transitivity) for the labeled system as the following rule:

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

Recall that reduction to normal form is linear.

The proofs of the following lemma and theorem are similar to the proofs of lemma 23 and theorem 24.

Lemma 41 Assume that x:σ ⊢_{co+B} M : τ and y:τ ⊢_{co+B} N : ρ. Then, erase (nf_{β} ([M/y]N)) =_{η} nf_{β} (erase ([M/y]N)).

Theorem 42 (Transitivity of ⊢_{co+B} ) (cut) is an admissible rule in Co^{⊢}+B.

We have thus shown that adding extra base types and coercions preserves the transitivity of entailment, i.e., of subtyping.

Note that, if we had used axioms of the form κ_{i} ⊢_{co+B} κ_{j} to assert subtyping relations between base types instead of Gentzen-style rules (κ_{i} ≤ κ_{j}), it would have been impossible to eliminate cuts. Notice also that, usually, in Gentzen-style systems such as ours, “right” rules are balanced by symmetric “left” rules. In the system Co^{⊢}+B, though, only the rules

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

are added to assert subtyping between base types. However, from the admissibility of (cut) (Theorem 42), we can deduce the admissibility of the “left” analogue of the (κ_{i} ≤ κ_{j}) rules.

(κ_{i} ≤ κ_{j} left){x:κ_{j} ⊢_{co+B} M : σ \atop y:κ_{i} ⊢_{co+B} [c_{i,j} y/x]M : σ}

By the observation following lemma , [c_{i,j} y/x]M is in β-nf.

To see this, assume that x: κ_{j} ⊢_{co+B} M : σ has been proved. Construct the following derivation with (cut):

\begin{matrix}(κ_{i} ≤ κ_{j}) & \underline{y:κ_{i} ⊢_{co+B} y : κ_{i}} \\ y:κ_{i} ⊢_{co+B} c_{i,j} y : κ_{j} & x:κ_{j} ⊢_{co+B} M : σ \\ (cut) & \overline{y:κ_{i} ⊢_{co+B} [c_{i,j} y/x]M : σ} \end{matrix}

where [c_{i,j} y/x]M is the already in β-nf. Since (cut) is admissible, we are done.

5.5 Coherence

Suppose that base types κ_{1}, κ_{2}, κ_{3}, … are given together with some (κ_{i} ≤ κ_{j}) rules, as described previously, but that no other conditions are added; in particular, neither unicity of the constants c_{i,j} for any given i, j, nor compositionality, nor associativity of coercions between base types are asserted.

As regards compositionality, transitivity of ⊢_{co+B} (Theorem 42) guarantees that, once embedded in our Gentzen-style system, base coercions compose.

The questions of unicity (coherence) and associativity may be settled only with respect to an equality stronger than = (in Co^{⊢}, already =_{ηco} was needed). Consider first what happens if we extend to Co^{⊢}+B the equality =_{ηco} defined for Co^{⊢}. This equality is defined exactly as in definition 21 (with Co^{⊢}+B sequents instead of Co^{⊢} sequents).

Let us consider first the case of coercions between the new base types (and their bicoercible images) in the extended system. As pointed out previously (lemma 34, case 1), only types bicoercible to ∀X.X and to base types may be subtypes of a base type in the extended system Co^{⊢}+B. As a weak form of coherence, here is what (eq appl2 co) allows us to prove, without any further conditions or assumptions on base types and rules:

Theorem 43 (Weak coherence of Co^{⊢}+B) Assume that both c_{i,j} and d_{i,j} are coercion constants between base types κ_{i} and κ_{j}. If y : σ ⊢_{co+B} M : κ_{i}, then x:∀X.σ ⊢_{co+B} c_{i,j} ([xX/y]M) =_{ηco} d_{i,j} ([xX/y]M) : κ_{j}.

Proof The assumption means that the following two rules have been added:

{x:σ ⊢_{co+B} M : κ_{i} \atop x:σ ⊢_{co+B} c_{i,j} M : κ_{j}}  {x:σ ⊢_{co+B} M : κ_{i} \atop x:σ ⊢_{co+B} d_{i,j} M : κ_{j}}

Construct then the following derivation:

\frac{y:σ ⊢_{co+B} M : κ_{i}}{y:σ ⊢_{co+B} c_{i,j} M : κ_{j}}  \frac{y:σ ⊢_{co+B} M : κ_{i}}{y:σ ⊢_{co+B} d_{i,j} M : κ_{j}}
\overline{x:∀X.σ ⊢_{co+B} c_{i,j} ([xX/y]M) =_{ηco} d_{i,j} ([xX/y]M) : κ_{j}} (eq appl2 co)

In particular, since x: ∀X.κ_{i} ⊢_{co+B} xX: κ_{i}, this weak coherence theorem implies equality of the composition of c_{i,j} and d_{i,j} with the coercion xX: just take σ = κ_{i} and M ≡ y. Clearly though, the theorem does not imply the equality of c_{i,j} and d_{i,j}.

In order to prove full coherence for Co^{⊢}+B, we need to force unicity of coercions (coherence) on base types. This may be done by adding a rule for equality on base types as follows.

Definition 44 =_{ηcoB} is the least equivalence relation generated by =_{ηco} plus the following rule:

(eq base co) {x:κ_{i} ⊢_{co+B} M : κ_{j}  x:κ_{i} ⊢_{co+B} N : κ_{j} \atop x:κ_{i} ⊢_{co+B} M =_{ηcoB} N : κ_{j}}

Note that, by the corollary to Lemma 34, the terms M and N must have the structure c_{i}(… (c_{1}x) …) and c′_{j}(… (c′_{1}x) …), respectively.

The condition on coercions between base types may be compared with the condition of coherence on basic coercions in [JLS98].

Theorem 45 (Coherence of Co^{⊢}+B) Let α_{1} and α_{2} be two derivations of x : σ ⊢_{co+B} M:τ and x:σ ⊢_{co+B} N:τ respectively. Then, M =_{ηcoB} N.

Proof The proof is similar to the proof of coherence for the pure system Co^{⊢} (Theorem 26) but instead of lemma 15, we have to use its modified version (lemma 37).

An extra case has to be considered: at least one of α_{1}, α_{2} ends with a (base) rule. In this case, τ = κ for some base type κ. By Lemma 33 case 1, both α_{1} and α_{2} may contain applications of only (ax), (κ_{i} ≤ κ_{j}), and (∀ left) rules. Apply Lemma 32 to both derivations, permuting all applications of (κ_{i} ≤ κ_{j}) rules before those of (∀ left), thus obtaining the following two derivations:

κ′ ⊢_{co+B} κ′  (ax)
\overline{κ′ ⊢_{co+B} κ_{p}}  (κ′ ≤ κ_{p})
\overline{⋮}  ⋮
\overline{κ′ ⊢_{co+B} κ_{q}}  ⋮
\overline{x:κ′ ⊢_{co+B} M : κ} (κ_{q} ≤ κ)
(∀ left)
⋮ ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ} (∀ left)

κ′ ⊢_{co+B} κ′  (ax)
\overline{κ′ ⊢_{co+B} κ_{p′}}  (κ′ ≤ κ_{p′})
\overline{⋮}  ⋮
\overline{κ′ ⊢_{co+B} κ_{q′}}  ⋮
\overline{x:κ′ ⊢_{co+B} N : κ}  (κ_{q′} ≤ κ)
(∀ left)
⋮ ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ} (∀ left)

Note that the applications of (∀ left) are the same in both derivations but the applications of (κ_{i} ≤ κ_{j}) rules, and their number, may differ.

Ignore now the applications of (∀ left) and consider the (sub)derivations of x : κ′ ⊢_{co+B} M : κ and x : κ′ ⊢_{co+B} N : κ in each derivation. By simple application of the equality rule (eq base co) above, obtain x: κ′ ⊢_{co+B} M =_{ηcoB} N : κ. Then, since (∀ left) preserves equality of coercions (implied by (eq appl2 co); see remarks section 3.2), we are done.

Corollary 46 Each (κ_{i} ≤ κ_{j}) rule preserves equality of coercions.

Proof Assume that a rule (κ ≤ κ′) has been added to the system, and assume that the equality x:σ ⊢_{co+B} M =_{ηcoB} N : κ has been derived.

The equality implies that x:σ ⊢_{co+B} M : κ and x:σ ⊢_{co+B} N : κ. By application of the rule (κ ≤ κ′), we obtain both x: σ ⊢_{co+B} c_{i,j} M : κ′ and x: σ ⊢_{co+B} c_{i,j} N : κ′ where c_{i,j} is the base coercion given by the rule. Use now the same proof technique as in Theorem 45 to derive x:σ ⊢_{co+B} c_{i,j} M =_{ηcoB} c_{i,j} N : κ′.

Coherence guarantees unicity of coercions on all types. As in the pure system Co^{⊢}, it implies that bicoercible types are isomorphic. And, as in Co^{⊢}, coherence implies the associativity of coercion composition, as given by transitivity of entailment.

6 Related work on subtyping

6.1 Proof-theoretic analyses

In light of the proof-theoretic investigations that the problem of subtyping has stimulated, it is fair to say that “the notion of subtyping is one of the most important concepts introduced recently into the theory of functional languages” [Tiu96].

Let’s quote some relevant papers. [CG92] solves the difficult problems of coherence and minimum typing in a different context. Clearly, if a term belongs to a type and to any larger type, then it has no unique type nor does it code a unique proof (or type derivation). Of course, the contravariant behavior of → (on the left) and second-order quantification complicate the problem. Yet, in [CG92], it is shown that each proof reduces to a unique “normal” one, which also yields the minimum type of its coding term (see also [PS94]). Other extensions of various lambda-calculi further clarified the issue of subtyping at a syntactic level. The approach in [BCGS91] significantly departs from the “intended” meaning in the previous papers: the subtyping relation is interpreted by the existence of a certain definable term (coercion) between type expressions.

Yet another approach may be found in [CMMS91]. This is directly related to Cardelli’s ideas for the programming language Quest and contains its main features as a basis (the Top type, bounded quantification, etc.). In short, a type-inference system is proposed which fully formalizes Quest’s rules and investigates conservativity of typing judgements and some categorical properties in a proof-theoretic frame (e.g., the syntactic isomorphisms between closed terms). Moreover, [CMMS91] suggests the rule (eq appl2) for equality of terms, the coercion version of which, (eq appl2 co), is used in our approach.

Both [BCGS91] and [CMMS91] are “orthogonal” to this paper, as they contain features (a Top type, records, variants, bounded quantification, etc.) that were motivated mostly by the practice of programming and which are not present in our approach. Our perspective stresses the logical (indeed, the “implicative”) nature of subtyping and, for now, it presents only the “pure logic”. It takes care of the introduction and elimination of universal quantification, which are not present in the other approaches except in that of Mitchell [Mit88] and Tiuryn [Tiu96]. In a sense, the present paper (in particular, section 4) may be seen as a proof-theoretic analysis of Mitchell’s Hilbert-style approach. Tiuryn gives two complete logical systems for subtyping, one in natural-deduction style and the other as a full Gentzen-style system; the latter system was inspired by the earlier version of our work here, i.e. by [LMS95].

In [Luo96, JLS98] subtyping in the computational theories specified in a typed logical framework LF has been studied. The main problem considered there was the conservativity of subtyping extensions of underlying type theories.

6.2 Models

As regards the key covariance/contravariance issue, the semantic problem should be clear, that is, the problem of giving a sound interpretation of the rule:

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

Recall that, one may naively interpret “σ is a subtype of τ” as “σ is a subset of τ” or “σ can be identically injected into τ”. This set-theoretic understanding is usually expressed by subsumption: if N has type σ and σ is a subtype of τ, then N also has type τ. However, in Set Theory, the rule (→) is not realized, as there is no way to inject τ → ρ into σ → ρ when σ is a subset of τ. There are, of course, several possible injections (by trivially extending functions) of σ → ρ into τ → ρ, but this is the opposite of what is desired. Even Category Theory, where Hom functors are contravariant on the left, doesn’t help: if “subtype” is interpreted as “subobject”, there is no way to extend a monomorphism m : σ → τ to a monomorphism from C[τ, ρ] to C[σ, ρ] or, in a Cartesian Closed Category, from ρ^{τ} to ρ^{σ}.

An early solution was proposed in [BL90] by constructing a specific categorical interpretation with “set-theoretic features”: the model of Partial Equivalence Relations (PER) accommodates Cartesian Closure as well as subtyping when σ ≤ τ is interpreted as “σ is a subrelation, a subset of pairs, of τ”. As a matter of fact, the PER model also provides an interpretation of higher-order quantification as closure under indexed products. The overall categorical construction of PER, as a model of higherorder lambda-calculus, in particular, Girard’s system F [Gir71], works because it is embedded in a constructive approach to Set Theory (the category of ω-Sets [LM91] or the Effective Topos [Hyl82]); see also [Rey84] and [Pit89].

In PER models, coercions are not arbitrary maps; nor are they identities. Indeed, this makes no sense in typed frameworks: if σ ≤ τ but σ and τ are different, there is no identity from σ to τ. This is so both in models and in theories. Note that PER models are constructed over an underlying model of the type-free lambda calculus. Any model of partial combinatory logic may suffice, see [Hyl88] say, and in particular Kleene’s (ω, .): in this case, n.m stays for the n-th index or Turing Machine applied to m.

Thus, in the PER model, terms are interpreted as equivalence classes of elements of ω. More precisely, define the erasure of a typed term to be the type-free term obtained by erasing all type information. Then, a term is interpreted by the equivalence class of (the interpretation of) its erasure. This allows second-order quantification to be interpreted as intersection, since the intersection is isomorphic to a categorical product (see [LM91]). In short, in the model in [BL90] (more precisely in the variant of it in [CL91], section 4), a coercion c from σ to τ transforms each {n}_{σ} into {n}_{τ}, where {n}_{σ} denotes the equivalence class of n in σ and {n}_{σ} is generally smaller than {n}_{τ}.

Thus, c is computed, in particular, by any index i of the identity function; equivalently, c is represented by {i}_{σ→τ}, since {i}_{σ→τ} .{n}_{σ} = {i.n}_{τ} = {n}_{τ}. Clearly, {i}_{σ→τ} contains many more elements than the indices of the identity function on ω, when σ or τ are different from ω. Using erasures in order to interpret typed terms, then this suggests that syntactic coercions are typed terms, different, in general, from the identity, but whose erasure is equal to the identity λx.x. This idea is nicely used in [Mit88]. It gives the syntactic completeness theorem for our “logic of subtyping”, system Co^{⊢}.

6.3 Semantics of equality, =_{ηco}

The semantics, indeed the consistency, of (eq appl2 co) deserves close attention. The following remarks are likewise intended for the reader familiar with PER models.

Rule (eq appl2 co) is valid in the PER model of subtyping [BL90]. More precisely, it is valid in the interpretation of subtyping with explicit coercions, given in [CL91] for the system Quest_{C}. This can be seen as follows. Recall that, under an environment ξ, the interpretation of M : ρ is given by the equivalence class {[[erase(M)_{ξ}]]}_{ρ}, where, by an abuse of language, we use the same name for both a type ρ and its meaning as a p.e.r.. (See the introduction and [CL91] on how type-free and typed environments are related; in short, a type-free environment ξ “picks out” an element of the equivalence class of the typed ξ′). Assume now that y_{i} : [τ_{i}/X]σ for i = 1, 2, and x : ∀X.σ. If both [τ_{i}/X]σ for i = 1, 2 are subtypes of μ, then the equivalence classes {ξ(y_{i})}_{[τ_{i}/X]σ} are coerced to the (larger) equivalence classes {ξ(y_{i})}_{μ} for i = 1, 2. Note now that, for x : ∀X.σ, one has xτ_{i} : [τ_{i}/X]σ and erase(xτ_{i}) = erase(x) = x. Then, by the interpretation of polymorphic application (see [LM91]), {ξ(x)}_{∀X.σ} . τ_{i} = {ξ(x)}_{[τ_{i}/X]σ}, which is also equal to the interpretation of xτ_{i} : [τ_{i}/X]σ.

The validity of the premises of (eq appl2 co) means that, in the model, N_{i} coerces the meaning of any term in [τ_{i}/X]σ into an equivalence class of μ. In particular, both interpretations {ξ(x)}_{[τ_{i}/X]σ} of xτ_{i} : [τ_{i}/X]σ, i = 1, 2, are coerced by N_{i} to the same equivalence class {ξ(x)}_{μ}, which does not depend on i. This is exactly the validity of the consequence of (eq appl2 co).

As recalled in the introduction, the coercions N_{1}, N_{2} are interpreted by functions computed (also) by indexes of the identity function. In general, though, they are not themselves identities and {ξ(y_{i})}_{[τ_{i}/X]σ} may be strictly smaller than {ξ(y_{i})}_{μ} (and each of the {ξ(x)}_{[τ_{i}/X]σ} may be strictly smaller than {ξ(x)}_{μ}). In [CMMS91], it is said that (eq appl2), which contains no coercions, is valid in PER models. This is correct but only modulo “forgetting” the coercions in the model (as was suggested in [BL90]). However, this does not correspond exactly to the structure of PER models, where coercions are non-identical maps (see [CL91] for a more detailed discussion). Thus, (eq appl2 co) is a more precise formalisation of “truth”, as given in PER models, than (eq appl2).

6.4 Second-order cut elimination proofs

The reader may wonder why the cut-elimination proof (Theorem 24) is so simple for a system which contains higher-order types and/or why we couldn’t just derive it from the proofs of more expressive systems. It is known that impredicative secondorder logic requires powerful tools to yield cut-elimination or normalization proofs ([Gir71, GLT89]). Yet, in [LMS96], we give another direct proof of cut-elimination for Co^{⊢} plus (cut) by a proof that does not rely on completeness: a non-obvious exercise. For the reader interested in the issue, we analyse here the key difficulties of a direct proof and some analogies and differences with respect to other calculi. We use [GLT89] as a reference.

For a first-order system, the proof of cut-elimination considered in Chapter 13 of [GLT89] is divided into two main parts: sections 13.1 and 13.2. The first part is the basis for an induction on the size of derivations: “cuts” are permuted with other rules and, when possible, they are moved up. Among the key cases, there are two crucial ones: cases 6 and 7 (or 8). Case 6 has an arrow as the cut formula, and the point there is that if one “swaps” the cut rule with the right and left-arrow rules, the cut rule is, unlike the preceding cases, NOT moved up, and a straightforward induction would then fail. This is the reason for introducing (in section 13.2) the notion of “degree” δ of a formula and using a combined induction on derivations AND degrees: in case 6, section 13.1, the degree of the cut formula does decrease (not the size of the derivation).

Fortunately, in the first-order case, the notion of degree of a formula does not present any problems (section 13.2): it is preserved under instantiation of a term variable by a term (e.g., δ(A[t/x]) = δ(A)). By this, the degree of the cut formulae in case 7 (and 8) of section 13.1 does not change when moving up the cut rule. And the combined induction goes through.

However, this form of combined induction cannot be used in the presence of higherorder (impredicative) formulae: no degree or measure on formulae is preserved by instantiation in general. Girard and Tait’s proof by “candidates of reducibility” employs a powerful technique to overcome this crucial difficulty of impredicative systems. The heavy inductive loading used (conditions CR 1,2,3 of chapters 6 and 14) requires the intended set of terms (candidates of reducibility) to be closed under reductions and expansions. In our case of a direct proof [LMS96], the difficulties of case 6 (section 13.1 of [GLT89]) are easily handled: that case corresponds to (→) occurring simultaneously on the left and on the right, where an arrow formula is eliminated, by cut. This gives a symmetric situation and allows one to move up the last cut rule, in contrast to case 6 in [GLT89]. Thus, we do not need to introduce an induction on degrees of formulae, which would, in turn, cause problems in an impredicative system, like ours. Moreover, we can neither refer to nor use the candidates of reducibility, even though Co^{⊢} is a subsystem of System F: the terms of our system with the cut rule are not closed under β-expansions (CR3), as pointed out before Lemma 16. Note that, in general, cut-elimination cannot automatically be applied to subsystems: there are easy counter-examples.

In the present approach, we used a simpler technique. The linearity of terms gives an immediate normalization theorem; then the completeness result (Theorem 19: coercions are exactly those F terms that erase to the identity) allows us to avoid a step-by-step cut-elimination and refer to the “evaluation” (nf_{β}) of a term’s erasure (cf. recent results on “normalization-by-evaluation” [BS91]).

7 Conclusions

The purpose of the calculus Co^{⊢} presented in this paper is to give a coherent logical meaning to the notion of subtyping: σ is a subtype of τ if σ implies (entails) τ. This meaning is the most obvious relation between logical implication and naive set-theoretic inclusion. The main advantage of our approach is that Co^{⊢} has a sound logical “status”, independently of its intended meaning for subtyping. This is obtained by presenting entailment in the frame of a second-order sequent calculus, where quantification is introduced and eliminated by right and left rules. We could then state and prove relevant properties such as coherence and the admissibility of (cut), which is equivalent to a cut-elimination theorem.

It should be clear why we do not take the (cut) rule as part of the definition of our subtyping system. In order to obtain coherence, we would need to eliminate it anyway. And coherence is used to prove anti-symmetry. Moreover, without (cut), all our proof-terms (definable coercions) are in normal form, as only (cut) may introduce redexes, exactly as in the λ-calculus.

In view of its formal relation to (cut), it may be fair to say that our system of subtyping is the least but still meaningful system for implication that also handles second-order universal quantification. Indeed, what weaker but still meaningful computation is there than “take an input and transform it into an element of a larger type”? And, intuitionistically, logical implications are computations. By our system, we characterized the logical implications which are coercions and explicitly used this characterization in the main results.

In the final section, we extended Co^{⊢} with base types. Transitivity and coherence hold in this extended calculus, which is conservative over Co^{⊢}. In view of the work in [BCGS91, CMMS91, CG92], further extensions can be studied, in particular, with a Top type, records, variants and bounded quantification. Moreover, a joint system F+Co^{⊢} could also be relevant for investigating general polymorphic subtyping.

Acknowledgments

We would like to thank Jerzy Tiuryn and Chen Gang for their close analysis and critical insight into our work. We also acknowledge the comments of an anonymous referee on a previous version of this paper, as well as the referees of the present version.

Sergei Soloviev was supported by a British EPSRC grant GR/K79130 while working at Durham University (1996-98); his work was also funded by HCM Project CHRX-CT93-0046 “Typed Lambda Calculus” (while visiting ENS, Paris) and “CLICS II”. Giuseppe Longo’s work was partially supported by HCM Project CHRX-CT93-0046 “Typed Lambda Calculus”.

Appendix

The following rules complete the definition of =_{ηco} (section 3.2); they just say that rules (→) and (∀_{n} right) preserve equality of coercions:

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

(eq ∀_{0≤k≤n} right)  {x:σ ⊢_{co} \begin{matrix}λx_{1} :τ_{1} … λx_{k}:τ_{k}.M =_{ηco} λx_{1} :τ_{1} … λx_{k}:τ_{k}.N \\ : τ_{1} → … (τ_{n} → τ) …) \end{matrix} \atop x:σ ⊢_{co} \begin{matrix}λx_{1} :τ_{1} … λx_{k}:τ_{k} … λx_{n}:τ_{n}.λX.Mx_{k+1} … x_{n} \\ =_{ηco} λx_{1} :τ_{1} … λx_{k}:τ_{k} … λx_{n}:τ_{n}.λX.Nx_{k+1} … x_{n} \\ : τ_{1} → … (τ_{n} → ∀X.τ) …) \end{matrix}}

∗

for X not free in σ

nor in τ_{1}, …, τ_{n}, for M not of the form λy.M′, for x_{k+1}, …, x_{n} fresh

(eq ∀_{0≤n<k} right)  {x:σ ⊢_{co} \begin{matrix}λx_{1} :τ_{1} … λx_{k}:τ_{k}.M =_{ηco} λx_{1} :τ_{1} … λx_{k}:τ_{k}.N \\ : τ_{1} → … (τ_{n} → τ) …) \end{matrix} \atop x:σ ⊢_{co} \begin{matrix}λx_{1} :τ_{1} … λx_{n}:τ_{n}.λX.λx_{n+1} :τ_{n+1} … λx_{k}:τ_{k}.M \\ =_{ηco} λx_{1} :τ_{1} … λx_{n}:τ_{n}λX.λx_{n+1} :τ_{n+1} … λx_{k}:τ_{k}.N \\ : τ_{1} → … (τ_{n} → ∀X.τ) …) \end{matrix}}

∗

for X not free in σ

nor in τ_{1}, …, τ_{n}, for M not of the form λy.M′ for τ ≡ τ_{n+1} → … (τ_{k} → τ′) …)

References

[ACC93] M. Abadi, L. Cardelli and P.-L. Curien. Formal parametric polymorphism. Theoretical Computer Science 121, pages 9–58, 1993.

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

[BDL92] K. Bruce, R. Di Cosmo, and G. Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science 2:2, pages 231–247, 1992.

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

[BS91] U. Berger and H. Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. Proceedings of the 6th IEEE Symposium on Logic in Computer Science (LICS), pages 203–213, IEEE Computer Society Press, 1991.

[CG92] P.-L. Curien and G. Ghelli. Coherence of subsumption, minimum typing and type-checking in F_{≤}. Mathematical Structures in Computer Science 2, pages 55–92, 1992.

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

[CMMS91] L. Cardelli, S. Martini, J. Mitchell, and A. Scedrov. An extension of system F with subtyping. Information and Computation 94, pages 4–56, 1994. First appeared in the proceedings of the Conference on Theoretical Aspects of Computer Software (Sendai, Japan), T. Ito and R. Meyer, eds., Lecture Notes in Computer Science 526, pages 750–770, Springer, 1991.

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

[Che96] G. Chen. Dependent type system with subtyping. Technical Report LIENS-96-27, Ecole Normale Supérieure, Paris. Revised version to appear in Journal of Computer Science and Technology.

[Che98] G. Chen. Sous-typage, conversion de types et élimination de la transitivité. Doctoral thesis, Laboratoire d’Informatique de l’Ecole Normale Supérieure, Paris. December 1998.

[Gir71] J.-Y. Girard. 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. Proceedings of the 2nd Scandinavian Logic Symposium, J.E. Fenstad, ed., pages 63–92, North-Holland, 1971.

[GLT89] J.-Y. Girard, Y. Lafont and P. Taylor. Proofs and types. Cambridge Tracts in Theoretical Computer Science 7, Cambridge University Press, 1989.

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

[Hyl88] J. Hyland. A small complete category. Annals of Pure and Applied Logic 40, pages 135–165, 1988.

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

[JLS98] A. Jones, Z. Luo and S. Soloviev. Some algorithmic and proof-theoretical aspects of coercive subtyping. Selected papers of the International TYPES’96 Workshop (Aussois, France, December 1996), E. Giménez and C. Paulin-Mohring, eds., Lecture Notes in Computer Science 1512, pages 173–196, Springer, 1998.

[Kle67] S. Kleene. Mathematical logic, Wiley, 1967.

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

[LMS93] G. Longo, K. Milsted, and S. Soloviev. The genericity theorem and the notion of parametricity in the polymorphic λ-calculus. Theoretical Computer Science 121, pages 323–349, 1993.

[LMS95] G. Longo, K. Milsted, and S. Soloviev. A logic of subtyping (Extended Abstract). Proceedings of the 10th IEEE Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, 1995.

[LMS96] G. Longo, K. Milsted, and S. Soloviev. A logic of subtyping. Complete version of the previous paper; available by anonymous ftp from ftp.ens.fr as /pub/dmi/users/longo/logicSubtyping.ps.Z or ... /logicSubtyping.dvi.Z [Luo96] . Zhaohui Luo. Coercive subtyping in type theory. In CSL’96, the 1996 An-

nual Conference of the European Association for Computer Science Logic, Utrecht, Lecture Notes in Computer Science, v. 1258, 1996.

[MR92] Q. Ma and J. Reynolds. Types, abstraction, and parametric polymorphism, part 2. Proceedings of the Conference on Mathematical Foundations of Programming Semantics, S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, eds., Lecture Notes in Computer Science 598, pages 1–40, Springer, 1992.

[Mit88] J. Mitchell. Polymorphic type inference and containment. Information and Computation 76:2-3, pages 211–249, 1988. Also appeared in Logical Foundations of Functional Programming, G. Huet, ed., pages 153–193, Addison-Wesley, 1990.

[PS94] B. Pierce and M. Steffen. Higher-Order subtyping. Theoretical Computer Science 176, pages 235–282, April 1997. A preliminary version appeared in the proceedings of the IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET), June 1994, and as University of Edinburgh technical report ECS-LFCS-94-280 and Universität Erlangen-Nürnberg Interner Bericht IMMD7-01/94, January 1994.

[Pit89] A. Pitts. Non-trivial power types can’t be subtypes of polymorphic types. Proceedings of the 4th IEEE Symposium on Logic in Computer Science (LICS), pages 6–13, IEEE Computer Society Press, 1989.

[Rey84] J. Reynolds. Polymorphism is not set-theoretic. Proceedings of Semantics of Data Types, G. Kahn et al., eds., Lecture Notes in Computer Science 173, pages 145-156, Springer, 1984.

[Sol83] S. Soloviev. The category of finite sets and Cartesian Closed Categories. Journal of Soviet Mathematics 22:3, pages 1387–1400, 1983.

[Tiu95] J. Tiuryn. Equational axiomatization of bicoercibility for polymorphic types. Proceedings of the 15th Conference on the Foundations of Software Technology and Theoretical Computer Science, P.S. Thiagarajan, ed., Lecture Notes in Computer Science 1026, pages 166–179, Springer, 1995.

[Tiu96] J. Tiuryn. A sequent calculus for subtyping polymorphic types. Proceedings of the Conference on Mathematical Foundations of Computer Science, Springer, 1996.

[TU96] J. Tiuryn and P. Urzyczyn. The subtyping problem for second-order types is undecidable. Proceedings of the 11th IEEE Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, 1996.