Inheritance in type theory

Gilles Barthe^{⋆}

Faculty of Mathematics and Informatics, Katholieke Universiteit Nijmegen, The Netherlands and Department of Computer Science, University of Manchester, United Kingdom

Abstract. We present an extension of pure type systems with inheritance which combines the flexibility of object-oriented languages (a function symbol can be applied to several domains) with the good behavior of strongly typed functional languages (e.g. decidable type-checking). The idea is to extend the syntax of pure type systems so as to consider derivations of the form Δ|Γ ⊢ M : A, where Δ is a set of coercions. This simple extension turns out to be very flexible and powerful; it supports multiple inheritance and can be applied to all type theories with a function space formation (including extensions of pure type systems or other type theories such as local set theories). It is particularily suitable for the formal development of mathematical theories, such as algebra, graph theory or category theory. Moreover, our syntax generalises type classes as used in Haskell by allowing a more general form of coercions and can easily be extended to capture the notion of constructor class as used in Clean and Gofer.

1 Introduction

Over the last twenty years, a new branch of mathematics, computer mathematics, has imposed itself as a powerful mathematical tool used by mathematicians and engineers as an assistant to do complex mathematical manipulations. Mathematical software has been used interactively for purposes as varied as mathematical education, performing large calculations, verifying the correctness of hardware and software… Paradoxically, the growing interest in mathematical software has caused a drift of mainstream mathematics towards mathematical logic and the foundations of mathematics. Before the appearance of mathematical software, formal systems were generally seen both by logicians and mathematicians as safe heavens into which mathematics could theoretically be embedded. With powerful mathematical software, there is now a genuine interest in developing mathematics within a formal system (see e.g. [6, 13]). This radical change in the relationship between mathematics and mathematical logic calls for a new strategy in the design of formal systems. Before computer mathematics, the value of a formal system was assessed on logical criteria:

⋆ Address from the first of October 1995: Department of Software Technology, CWI, Amsterdam,The Netherlands.

- adequacy: a formal system T is adequate if it is possible to formulate and prove all mathematical theorems within T;

- faithfulness: a formal system T is faithful if one cannot prove in T a statement which is not provable in ordinary mathematics.

With computer mathematics, new criteria have appeared ([2, 4]):

- comfort: developing proofs in a formal system should be as user-friendly as possible. This can be achieved by choosing a suitable syntax, reducing the need for encoding…

- efficiency: formal proofs should be as short as possible. This is achieved by making the formal system more powerful, for example by combining different paradigms such as type theory and term-rewriting or by providing powerful methods for solving some basic problems, such as for example arithmetic.

To meet these new criteria, a new generation of formal systems is required which aims at feasible formal mathematics. The ultimate goal is to design formal systems which remain close to the spirit and form of informal mathematics. Despite an early proposal by N.G. de Bruijn ([7]), much remains to be done in this direction. There are still notable differences between formal and informal mathematics:

(i) the level of detail required in formal proofs is much greater than the level of detail in informal proofs; reasoning in a formal system requires every single step to be decomposed in terms of primitive rules. Logicians only allow themselves to overlook a complex reasoning step if they have already checked that such a step can be decomposed in terms of primitive rules, whereas similar shortcuts are used in ordinary mathematics without being justified in the way logic requires.

(ii) the same difference occurs at the level of language; sentences in a formal language must obey a grammar much stricter than the grammar of a natural language. While mathematicians currently write x ∈ G, where G is a group, the expression is not well-formed in most formal languages, because it is required that the expression on the right hand side of ∈ should be a set. The correct statement is x ∈ carr(G), where carr(G) is the underlying set of G.

Much work has been done to solve the first problem: computer scientists in the theorem-proving (and proof-checking) community have developed new tools such as tactics, decision procedures and techniques to automate induction. As for the second problem, it has been a focus point of the functional programming community: several concepts, such as subsumption, inheritance and argument synthesis have been thoroughly investigated in the context of programming languages ([8, 22, 23]). These concepts, that we shall refer to under the generic term of implicit syntax (the name is due to R.Pollack, see [20]), enable formal expressions to be written in a much fluider and more intuitive style than in conventional formal systems. Yet little work has been made to apply these ideas to formal systems used in theorem-proving and proof-checking. The aim of this paper is to initiate a generic treatment of these concepts in type systems, with a view to apply it to theorem-proving and proof-checking. The long-term goals of our research are

1. to capture in a single framework the use of implicit syntax as it occurs in mathematics and computer science;

2. to bring the flexibility of expression in formal languages to a level similar to that of informal mathematics;

3. to develop formal systems for feasible formal mathematics.

Here we focus on one specific aspect of implicit syntax, namely inheritance. By inheritance, we refer to a grammatical convention which allows one to apply a map f : A → B to an element a of A′ because A′ can be seen in some sense as a subset of A. Inheritance plays a fundamental role in programming languages and mathematics. It seems therefore important to formalise it at the right level of abstraction, both to understand its nature and to implement it in a suitable way. Here we introduce the framework of pure type systems with inheritance, an extension of Barendregt’s framework of pure type systems ([3]). The idea is to consider, instead of the traditional judgements Γ ⊢ M : A, judgements of the form Δ|Γ ⊢ M : A where Δ is a set of legal terms, called coercions, which specify which are the arguments that can be omitted in an expression. Indeed, the deductive system is defined in such a way that one can derive i : ℕ → ℤ| ⊢ minus 3 : ℤ from | ⊢ 3 : ℕ and |minus : ℤ → ℤ because one has assumed the implicit coercion i : ℕ → ℤ. Of course, there are suitable rules to introduce coercions in a context (on the left of a |). This simple extension to the system turns out to be extremely powerful and flexible.

This work originates from previous work with Peter Aczel on formalising Galois theory in Lego, a proof-checker based on ECC developed by R. Pollack at Edinburgh ([15]). In absence of a mechanism to handle multiple inheritance, we realised that the syntax was becoming too heavy and the number of identifiers was becoming disproportionate very rapidly. This led us to consider the possibility of implementing classes in Lego; this was done by September 1993 ([1]). I later used this implementation in a formal proof of the unsolvability of the symmetric group of a set with more than four elements ([4]). Inheritance turned out to be extremely useful. On the one hand, it allowed me to use a limited form of overloading; for example, I could use el X to denote the carrier of X, where X could be a set, a monoid or a group. On the other hand, I could use structured reasoning quite naturally, by applying results proved for monoids to groups. This case study suggested the potential of inheritance in proof-checking but also highlighted some problems: first, the implementation only supported single inheritance. Second, inheritance was obtained by an ad hoc technique. The work in this paper is meant to repair these two basic flaws. We have also attached a special importance to coherence: that is, we have formulated the syntax in such a way that all the coercions between two types are essentially equal. Although coherence might not play an important role in applications, we feel it is a crucial concept for a phenomenological explanation of inheritance, especially as it occurs in mathematics.

The paper is organised as follows: in the next section, we give an informal motivation of the syntax of pure type systems with inheritance by giving an abstract definition of implicit syntax. In section 3, we present the syntax for pure type systems with inheritance. In order to look at interesting examples, we consider pure type systems with Σ-types. In section 4, we exemplify the use of our syntax in the formalisation of algebra. In section 5, we study the basic meta-theory of the system and show that pure type systems with inheritance provide a system of implicit syntax for pure type systems. Related work and possible extensions to our work are discussed in section 6.

2 What is implicit syntax?

2.1 An abstract view of implicit syntax

Implicit syntax can be seen as a relaxing of the grammar of a given language: in this sense, we should talk about a language B being an implicit syntax for a language A. The reason to introduce B is that expressing oneself in A might sometimes be cumbersome; yet B should not be more expressive than A. This is a fundamental assumption of implicit syntax: it is meant to improve expressivity, not to increase it. This means that every expression in B should be reducible by some means to an expression in A. Moreover, one would hope this process to be deterministic, i.e. that every expression in B corresponds uniquely to an expression in A. In order to make the description precise, let us work at a very abstract level and consider a language to be a ‘setoid’, i.e. a type with an equivalence relation on it^{2}.

Definition 1 An implicit syntax for a language (A, =_{A}) consists of a language (B, =_{B}) and an map e : B → A such that

- A ⊆ B;

- for every a_{1}, a_{2} ∈ A, a_{1} =_{A} a_{2} ⇔ a_{1} =_{B} a_{2};

- for every a ∈ A, a =_{A} e(a);

- for every b_{1}, b_{2} ∈ B, b_{1} =_{B} b_{2} ⇔ e(b_{1}) =_{A} e(b_{2}).

Note that ((B, =_{B}), e) is an implicit syntax for (A, =_{A}) if and only if e is a retract of setoids. In this paper, we will not only be interested in languages but in formal systems, so we need to extend the idea of implicit syntax to formal system. What is required here is that the extension is conservative and that theorems are preserved under translation. To fix ideas, let us define a formal system as a triple (A, =_{A}, Thm) where (A, =_{A}) is a language and Thm is a relation on A. For the sake of simplicity, we consider Thm to be a binary relation over A^{3}.

2 We need to introduce the notion of equality as part of the language to be able to consider terms modulo an equational theory. For example, the set of pure λ-terms modulo β-equivalence is a language.

3 We can alternatively think about (a, a′) ∈ Thm as a′ is derivable from a or as a is a proof of the proposition a′.

Definition 2 An implicit syntax for a formal system (A, =_{A}, Thm) consists of a formal system (B, =_{B}, Thm′) and a map e : B → A such that

- (B, =_{B}, e) is an implicit syntax for (A, =_{A});

- for every a_{1}, a_{2} ∈ A, (a_{1}, a_{2}) ∈ Thm ⇔ (a_{1}, a_{2}) ∈ Thm′;

- for every b_{1}, b_{2} ∈ B, (b_{1}, b_{2}) ∈ Thm′ ⇔ (e(b_{1}), e(b_{2})) ∈ Thm.

The above definition gives us an abstract characterisation of the concept of implicit syntax. In the next paragraph, we apply these definitions to pure type systems with inheritance.

2.2 Pure type systems with inheritance as implicit syntax

Recall that a pure type system is specified by a quadruple λS = (Sort, Axiom, Rule_{Π}, Rule_{Σ}) where^{4}

- Sort is a set,

- Axiom : Sort ⇀ Sort and Rule_{Π}, Rule_{Σ} : Sort × Sort ⇀ Sort are partial functions.

Similar tuples are used to specify pure type systems with inheritance. Therefore, one has for every pure type system λS a pure type system with inheritance λ_{inh}S with the same specification and vice-versa. Both have the same set of pseudoterms, defined as usual.

Every pure type system induces a collection of formal systems: for every context Γ, we can consider the formal system (Term(Γ), =_{β},:_{Γ}), where Term(Γ) is the set of legal terms in context Γ and :_{Γ} is the relation defined by M :_{Γ} A if Γ ⊢ M : A. Similarly, every pure type system with inheritance induces a collection of formal systems. For every context^{5} Δ|Γ, we can consider the formal system (Term(Δ|Γ), =_{βϵ(Δ)},:_{Δ|Γ}) where Term(Δ|Γ) is the set of legal terms in context Δ|Γ and :_{Δ|Γ} is the relation defined by M :_{Δ|Γ} A if Δ|Γ ⊢ M : A. The equality on terms is given by β-reduction and ϵ(Δ)-reduction; this latter reduction relation is defined relative to a set of pseudo-coercions and makes terms fully explicit by introducing the missing arguments in a term. In the example of Section 1, we will have minus 3 →_{ϵ(i)} minus (i 3). The main result we will prove is:

Main Result. For every pure type system with inheritance λ_{inh}S and context Δ|Γ, the formal system (Term(Δ|Γ), =_{βϵ(Δ)},:_{Δ|Γ}) is an implicit syntax for the formal system of λS, its corresponding pure type system, (Term(Γ′), =_{β},:_{Γ′}), where Γ′ is the ‘ϵ(Δ)-normal form’ or explicitation of Γ.

In particular, the following two conditions are satisified:

4 We only consider functional pure type systems and include Σ-types as a type

constructors. 5 Recall that judgements are of the form Δ|Γ ⊢ M : A.

- coherence condition: if M is a legal term in context Δ|Γ, all its explicitations or ϵ(Δ)-normal forms are β-convertible;

- conservativity condition: if Δ|Γ ⊢ M : A is derivable, then Γ, M and A have explicitations or ϵ(Δ)-normal forms (respectively Γ′, M′ and A′) and Γ′ ⊢ M′ : A′ is derivable in the underlying pure type system.

Note that the introduction of a reduction relation to make terms fully explicit, which seems to be new, serves several purposes:

- by giving a computational interpretation to implicit syntax, we can analyse its interaction with other computational processes, such as β-reduction;

- by extending not only the set of typable terms but also their equational theory, we are able to explain every term of the implicit syntax by a term of the original syntax. In particular, all the representations of a term of the original system into the system with implicit syntax are equivalent.

3 Pure type systems with inheritance

In the previous section, we specified the properties which are required for pure type systems with inheritance. In this section, we give a syntax which meet these requirements. In order to treat interesting examples, we consider an extension of pure type systems with Σ-types. However, our approach to inheritance is independent from type constructors (we only need a function space former) and does not require the presence of Σ-types.

The set of pseudo-terms of a pure type system (with inheritance) λS = (Sort, Axiom, Rule_{Π}, Rule_{Σ}) is given by the following abstract syntax:

T = V |Sort|ΠV : T.T |λV : T.T |T T |ΣV : T.T |pair(T, T)|fst T |snd T

where V is a fixed set of variables. The deductive system for pure type systems with strong sums are the usual ones (see for example [20]). Before giving the deductive system for pure type systems with inheritance, we must formulate the notion of coercion. To avoid circularities, we consider pseudo-coercions.

Definition 3 A pseudo-coercion is a pair of closed pseudo-terms (λx : A.t, A → B). Usually, we write pseudo-coercions as λx : A.t : A → B.

The idea is that λx : A.t is a term of type A → B. Note that we only consider simple coercions, i.e. neither a coercion or its type are allowed to contain free variables. The reason we do not consider a more general form of coercion is the coherence condition; in order to ensure coherence, we must impose some proviso on the introduction rule for coercions:

\frac{Δ_{1}|Γ_{1} ⊢ M_{1} : A_{1} Δ_{2}|Γ_{2} ⊢ M_{2} : A_{2}}{Δ_{1}, M_{2} : A_{2}|Γ_{1} ⊢ M_{1} : A_{1}}

For simple coercions, it is relatively easy to find a proviso which forces coherence and conservativity. For a more general form of coercions, it is unclear what the proviso should be (see section 6.1 for a longer discussion).

To formulate the proviso for the above rule, we introduce the notion of coherent set of pseudo-coercions. This is achieved by defining the closure Δ^{+} of a set Δ of pseudo-coercions: it is the least set such that if, for i = 1, …, n, c_{i} : A_{i} → B_{i} are pseudo-coercions in Δ and A_{i+1} =_{β} B_{i} for i = 1, …, n − 1 then λx : A_{1}.c_{n}(c_{n−1}(… (c_{1}x) …) : A_{1} → B_{n} is an element of Δ^{+}. Note that all elements of Δ^{+} are pseudo-coercions. If Δ is a set of pseudo-coercions, we say that A is Δ-linked to B if there is a pseudo-term t such that t : A′ → B′ belongs to Δ^{+} for some A′ =_{β} A and B′ =_{β} B.

Definition 4 A set Δ of pseudo-coercions is coherent if:

1. for every two pseudo-coercions (i, A → B) and (j, A′ → B′) in Δ^{+}, A =_{β} A′ ∧ B =_{β} B′ ⇒ i x =_{β} j x, where x is a fresh variable;

2. for every pseudo-coercion (i, A → B) in Δ^{+}such that A =_{β} B, we have t x =_{β} x, where x is a fresh variable.

Let Δ be a set of pseudo-coercions. The relation →_{ϵ(Δ)} is defined on pseudoterms as the compatible closure of t u→_{ϵ(Δ)}t (i u), where it is assumed that i ∈ Δ. ↠_{ϵ(Δ)} (resp. =_{ϵ(Δ)}) is defined as the reflexive, transitive (resp. reflexive, symmetric and transitive) closure of →_{ϵ(Δ)}. The rules for derivation are given in Table 1. All the rules except (Entry), (Method) and the conversion rules are straightforward adaptations of the rules for pure type systems.

- The (Method) rule introduces inheritance in the system by allowing to apply f : Πx : A.B to elements of several types (in fact to all the types which are linked to A). Note that the predicate of the conclusion is B[i u/x] rather than B[u/x] because we do not know if the latter is legal. This is not important in practice because the user of a proof-checker does not have to provide the type of an expression.

- The (Entry) rule enables new coercions to be introduced provided the resulting set of coercions is coherent. Note that one could have considered an alternative rule (AxEntry)

\frac{Δ| ⊢ c : s | ⊢ t : A → B}{Δ, t : A → B| ⊢ c : s} if (c, s) ∈ Axiom and Δ ∪ \{t, A → B\} is coherent

The set of derivables judgements remains unchanged if we replace (Entry) by (AxEntry). The proof proceeds by induction on the derivations and uses induction loading: we prove that if Δ|Γ ⊢ M : A is derivable and Δ′ ⊇ Δ is coherent, then Δ′|Γ ⊢ M : A in the system with (AxEntry).

- The conversion rule has been splitted in two: there is one rule for β-conversion and one rule for ϵ-conversion. There are several reasons to chose these rules: on a conceptual level, it seems natural to postpone computations until the term is fully explicit. On a technical level, the combined reduction is not Church-Rosser and subject reduction fails, as shown in the section 5. This prevents us from having a very general conversion rule, such as

(Axiom)  | ⊢ c : s  if (c, s) ∈ Axiom
(Start)  \frac{Δ|Γ ⊢ A : s}{Δ|Γ, x : A ⊢ x : A}  if x ∉ Γ
(Weakening)  \frac{Δ|Γ ⊢ t : A Δ|Γ ⊢ B : s}{Δ|Γ, x : B ⊢ t : A}  if x ∉ Γ
(Product)  \frac{Δ|Γ ⊢ A : s_{1} Δ|Γ, x : A ⊢ B : s_{2}}{Δ|Γ ⊢ Πx : A.B : s_{3}}  if (s_{1}, s_{2}, s_{3}) ∈ Rule_{Π}
(Application)  \frac{Δ|Γ ⊢ t : Πx : A.B Δ|Γ ⊢ u : A}{Δ|Γ ⊢ tu : B[u/x]}
(Abstraction)  \frac{Δ|Γ, x : A ⊢ t : B Δ|Γ ⊢ Πx : A.B : s}{Δ|Γ ⊢ λx : A.t : Πx : A.B}
(Sum)  \frac{Δ|Γ ⊢ A : s_{1} Δ|Γ, x : A ⊢ B : s_{2}}{Δ|Γ ⊢ Σx : A.B : s_{3}}  if (s_{1}, s_{2}, s_{3}) ∈ Rule_{Σ}
(Pairing)  \begin{matrix}Δ|Γ ⊢ t_{1} : A Δ|Γ ⊢ t_{2} : B[t_{1}/x] \\ Δ|Γ ⊢ Σx : A.B : s \\ Δ|Γ ⊢ pair(t_{1}, t_{2}) : Σx : A.B \end{matrix}
(First Projection) \frac{Δ|Γ ⊢ t : Σx : A.B}{Δ|Γ ⊢ fst t : A}
(Second Projection) \frac{Δ|Γ ⊢ t : Σx : A.B}{Δ|Γ ⊢ snd t : B[fst t/x]}
(Entry)  \frac{Δ|Γ ⊢ c : C | ⊢ t : A → B}{Δ, t : A → B|Γ ⊢ c : C}  if Δ ∪ \{t, A → B\} is coherent
(Method)  \frac{Δ|Γ ⊢ t : Πx : A.B Δ|Γ ⊢ u : A′}{Δ|Γ ⊢ tu : B[i u/x]}  if A′ is linked to A by λx : A′′.i
(β-conversion)  \frac{Δ|Γ ⊢ c : C |Γ′ ⊢ C : s |Γ′ ⊢ C′ : s}{Δ|Γ ⊢ c : C′} if C ↓_{β} C′ and Γ →_{ϵ(Δ)} Γ′
(ϵ-conversion)  \frac{Δ|Γ ⊢ c : C Δ|Γ ⊢ C′ : s}{Δ|Γ ⊢ c : C′}  if C ↓_{ϵ(Δ)} C′

Table 1. Rules for derivations in pure type systems with inheritance

\frac{Δ|Γ ⊢ c : C Δ|Γ ⊢ C′ : s}{Δ|Γ ⊢ c : C′} if C =^{βϵ(Δ)} C′

It would also have been possible to replace the conversion rule by an expansion/reduction rule, as done for pure type systems with algebraic rewriting (see for example [5]); the expansion/conversion rule would then be

\frac{Δ|Γ ⊢ c : C Δ|Γ ⊢ C′ : s}{Δ|Γ ⊢ c : C′}

if C →_{ϵ(Δ)} C′, C′ →_{ϵ(Δ)} C, C →_{β} C′ or C′ →_{β} C. All the results of the following section also apply to the syntax obtained by replacing the conversion rules by the expansion/reduction rule.

Note that pure type systems with inheritance extend pure type systems in the obvious way.

Lemma 5 Let λS be a pure type system and λ_{inh}S be its corresponding pure type system with inheritance. Assume Γ ⊢_{λS} M : A. Then Δ|Γ ⊢_{λ_{inh}S} M : A for every coherent set of coercions Δ. Conversely, if |Γ ⊢_{λ_{inh}S} M : A, then Γ ⊢_{λS} M : A.

4 Inheritance at work: formalising algebra in the Calculus of Constructions with inheritance

The proposed syntax is very suited for the development of formal mathematics. As said earlier, we have used an implementation of single inheritance in Lego to develop a formal proof of the unsolvability of the symmetric group over a set with more than four elements ([4]). Inheritance turned out to be an invaluable tool in order to attain a reasonably structured and intuitive structure for the proof. In this section, we exemplify the use of inheritance by formalising basic algebraic notions in the Calculus of Constructions with strong sums CCΣ. Inheritance is equally useful in the formalisation of universal algebra, graph theory or category theory to mention only few examples.

The Calculus of Constructions with strong sums has two sorts, ∗ and □, related by the axiom ∗ : □. The rules for products are (∗, ∗), (□, ∗), (∗, □), (□, □). The rules for sums are (∗, ∗, ∗) and (□, ∗, □). The system is Church-Rosser, strongly normalising, consistent and has decidable type-checking. In CCΣ, it is possible to define several basic algebraic types, such as sets, groupoids, monoids… We give some of these definitions here. For the sake of simplicity, we do not use the standard representation of sets as setoids ([4]) and treat sets as types. So we have Set = ∗. Other types are defined as shown below:

Gpd = ΣT : Set.Σo : T → T → T.AxGpd o
AbGpd = ΣT : Set.Σo : T → T → T.(AxGpd o) ∧ (Comm o)
Mon = ΣT : Set.Σo : T → T → T.Σe : T.AxMon o e
Mon′ = ΣT : Set.Σe : T.Σo : T → T → T.AxMon o e
AbMon = ΣT : Set.Σo : T → T → T.Σe : T.(AxMon o e) ∧ (Comm o)
Grp = ΣT : Set.Σo : T → T → T.Σe : T.Σi : T → T.AxGrp o e i
AbGrp = ΣT : Set.Σo : T → T → T.Σe : T.Σi : T → T.(AxGrp o e i) ∧ (Comm o)

where Comm o is the proposition stating that o is commutative and AxGpd, Ax-Mon and AxGrp respectively state the axioms of groupoids, monoids and groups. There are canonical maps between these types corresponding to projections; for example the canonical map from groupoids to sets is the first projection. These maps are shown in figure 1. These ten maps (in any order) induce a coherent set of (simple) coercions, which can conveniently be used to formalise algebra. For example, if we define Op2 as λT : Set.T → T → T and comp as λG : Gpd.fst (snd G) then we can apply comp to monoids, groups… If G is an abelian group, then comp G is of type Op2 G. Similarly, one can apply unit to G, where unit is defined as λM : Mon.fst (snd (snd M)).

As can be seen from the above example, typical features of our approach include:

Grp ^{AbGrptoGrp}  AbGrp
[figure: GrptoMon; AbGrptoAbMon]
[figure: Mon′; Mon′toMon; \overline{MontoMon′}; Mon; AbMontoMon; AbMon]
[figure: MontoGpd; AbMontoAbGpd]
Gpd ^{AbGpdtoGpd}  AbGpd
GpdtoSet
Set

Fig. 1. Basic coercions for algebra

- multiple inheritance: there can be several coercions maps with the same domain and there might be more than one path between two types. For example, one can have four coercion maps f : A → B, g : B → C, h : A → B′ and i : B′ → C provided g ∘ f and i ∘ h are extensionally equal.

- top-down introduction of coercions: it is possible to introduce a coercion f : A → B and then a coercion g : B → C. In fact, coercions can be introduced in any order. This solves the problem of “supertype” which occurs when coercions are required to be built up in a tree-like manner. In our syntax, there is no problem in defining the natural, then the integers and declaring a coercion from natural to integers, then build the rationals and declare a coercion from integers to rationals…

- splitting a coercion: it is possible to “split” a coercion f : A → B into two coercions g : A → C and h : C → B provided f and h ∘ g are extensionally equal. This allows to postpone the introduction of new notions until they are needed. For example, one does not need to introduce the notion of monoid before the notion of group in order to split the coercion from groups to groupoids into a coercion from groups to monoids and from monoids to groupoids;

- back and forth coercions: it is possible to have two coercions f : A → B and g : B → A provided the maps are mutually inverse. Back and forth coercions allow for equivalent representations of a same mathematical object to be handled elegantly. In our example, we can apply every function defined on Mon to Mon’ and conversely. This is very convenient for re-usability as experience shows that different users chose different but equivalent representations of a same mathematical object.

5 Meta-theory of pure type systems with inheritance

In this section, we establish that type systems with inheritance are systems of implicit syntax for type systems by showing that the conservativity and coherence conditions are satisfied. First, we start with a brief discussion about the meta-theory of these systems.

5.1 Which meta-theory for pure type systems with inheritance?

The two fundamental properties of a type system are confluence and strong normalisation. The first property ensures that programs always give the same result independently of the order in which the computations are performed. The second property ensures that all programs terminate. With systems of implicit syntax, none of these properties is relevant. To start with, local confluence of the combined reduction relation and subject reduction do not hold:

- for confluence, consider the term t = (λx : A.x)x. Then t →_{β} x. Moreover, t →_{ϵ(Δ)} (λx : A.x) (i x) for every non-empty set of pseudo-coercions Δ and i ∈ Δ. In general, one does not have (λx : A.x) (i x) →_{βϵ(Δ)} x.

- for subject reduction, consider Op2 G where G is a group and perform a β-reduction, the result is G → G → G, which is not well-typed.

Intuitively, the reason is that it is not safe to perform β-reduction on a term which is partly implicit. The morale is that one should only perform β-reduction on explicit parts of a term. With this view, reduction is a succession of two processes, explicitation (i.e. ϵ-reduction) and computation (i.e. β-reduction). What is required is that computations should only be performed on redexes in ϵ(Δ)- normal form. Therefore we introduce the mix reduction relation →_{mix(Δ|Γ)} as some form priority rewrite system.

Definition 6 M →_{mix(Δ|Γ)} N if:

- either Δ|Γ ⊢ M, N : A for some A and M →_{ϵ(Δ)} N;

- either M = C[(λx : A.b) a], N = C[b[a/x]] and Δ|Γ ⊢ a : A.

In the sequel, we feel free to write mix(Δ) rather than mix(Δ|Γ) when no confusion is possible.

It is reasonable to ask that the results of unfolding a term M such that Δ|Γ ⊢ M : A w.r.t mix(Δ|Γ)-reduction is independent of the reduction strategy. This will be proved later. One would also hope that all mix-reduction paths terminate. However, this cannot be the case because ϵ-reduction itself is not strongly normalising, due to the presence of back-and-forth coercions. Yet we will show that infinite reductions can only be caused by those back-and-forth coercions.

Remark: the fact that →_{mix} is defined relative to a context Δ|Γ rather than relative to a set of coercions Δ might appear to be rather cumbersome. One possibility to avoid this problem is to consider a variant of pure type systems, called pure type systems with variable labellings, in which every variable is assigned à priori a pseudo-term, to be understood as its potential type. In this framework, there is no need to keep track of contexts, i.e. derivations are of the form ⊢ M : A ([5]). If we consider inheritance for pure type systems with variable labellings, then derivations are of the form Δ ⊢ M : A where Δ is a set of coercions and →_{mix} needs only be defined relative to a set of coercions.

5.2 Basic results

Before proving the coherence and conservativity conditions, we need to establish some basic facts about the meta-theory of type systems with inheritance. We start by a definition of legal reduction path.

Definition 7 Let M be a term such that Δ|Γ ⊢ M : A. A reduction sequence M → M_{1} → ⋯ → M_{n} is legal w.r.t. Δ|Γ provided there exists 1 ≤ i ≤ n such that:

- every reduction step before M_{i} is a ϵ(Δ)-reduction step;

- there exists Γ′ and A′ such that |Γ′ ⊢ M_{i} : A′, Γ ↠_{ϵ(Δ)} Γ′ and A ↠_{ϵ(Δ)} A′;

- every reduction step after M_{i} is a β-reduction step.

We shall write M ↠_{leg(Δ|Γ)} N whenever M reduces to N along a Δ|Γ -legal reduction path. We write M =_{leg(Δ|Γ)} N whenever M and N are convertible via a Δ|Γ -legal path. Legal reduction plays a similar role to inside-out reduction in untyped λ-calculus, as shown by the following result.

Lemma 8 If M ↠_{leg(Δ|Γ)} N, then M ↠_{mix(Δ|Γ)} N. Moreover, if M ↠_{mix(Δ|Γ)} N, then there exists P such that M ↠_{leg(Δ|Γ)} P and N ↠_{mix(Δ|Γ)} P.

It is also important to notice that the two conversion rules of Table 1 are equivalent to the legal conversion rule

\frac{Δ|Γ ⊢ c : C Δ|Γ ⊢ C′ : s}{Δ|Γ ⊢ c : C′} if C =^{leg(Δ|Γ)} C′

This new formulation enables us to give a clear formulation of basic lemmas, such as the generation lemma or the key lemma.

Lemma 9 (Generation lemma) - If Δ|Γ ⊢ s : C, where s is a sort, then

there exists a sort s′ such that (s, s′) ∈ Axiom and C ↠_{leg(Δ|Γ)} s′.

- If Δ|Γ ⊢ x : C, where x is a variable, then there exists a type C′ such that (x : C′) ∈ Γ and C =_{leg(Δ|Γ)} C′.

- If Δ|Γ ⊢ Πx : A.B : C, then there exist three sorts s_{1}, s_{2} and s such that C ↠_{leg(Δ|Γ)} s′, Δ|Γ ⊢ A : s_{1}, Δ|Γ, x : A ⊢ B : s_{2} and (s_{1}, s_{2}, s) ∈ Rule_{Π}.

- If Δ|Γ ⊢ Σx : A.B : C, then there exist three sorts s_{1}, s_{2} and s such that C ↠_{leg(Δ|Γ)} s′, Δ|Γ ⊢ A : s_{1}, Δ|Γ, x : A ⊢ B : s_{2} and (s_{1}, s_{2}, s) ∈ Rule_{Σ}.

- If Δ|Γ ⊢ λx : A.b : C, then there exist a sort s and a type B such that Δ|Γ ⊢ Πx : A.B : s, C =_{leg(Δ|Γ)} Πx : A.B and Δ|Γ, x : A ⊢ b : B.

- If Δ|Γ ⊢ M N : C then there exists Πx : A.B such that Δ|Γ ⊢ M : Πx : A.B and

- either Δ|Γ ⊢ N : A and C =_{leg(Δ|Γ)} B[N/x];

- either Δ|Γ ⊢ N : A′ and C =_{leg(Δ|Γ)} B[i N/x] for some A′ Δ-linked to

A by i.

- If Δ|Γ ⊢ ⟨M, N⟩ : C, then there exists a sort s and a type Σx : A.B such that Δ|Γ ⊢ Σx : A.B : s, C =_{leg(Δ|Γ)} Σx : A.B, Δ|Γ ⊢ M : A and Δ|Γ ⊢ N : B[M/x].

- If Δ|Γ ⊢ fst M : C, then there exists a type Σx : A.B such that Δ|Γ ⊢ M : Σx : A.B and C =_{leg(Δ|Γ)} A.

- If Δ|Γ ⊢ snd M : C, then there exists a type Σx : A.B such that Δ|Γ ⊢ M : Σx : A.B and C =_{leg(Δ|Γ)} B[fst M/x].

Lemma 10 (Key lemma) Assume Δ|Γ ⊢ Πx : A.B : s and Δ|Γ ⊢ Πx : A′.B′ : s with Πx : A.B =_{leg(Δ|Γ)} Πx : A′.B′. Then A =_{leg(Δ|Γ)A′} and B =_{leg(Δ|Γ,x:A)} B′.

These results enable to establish various closure properties of derivations under reduction and expansion.

Lemma 11 - Assume Δ|Γ ⊢ M : A and M →_{mix(Δ|Γ)} N. Then Δ|Γ ⊢ N : A.

- Assume Δ|Γ ⊢ M : A, Γ ↠_{ϵ(Δ)} Γ′, M′ ↠_{ϵ(Δ)} M and A′ ↠_{ϵ(Δ)} A. Then Δ|Γ′ ⊢ N′ : A′.

5.3 The conservativity and coherence conditions

In this section, we establish that pure type systems with inheritance give an implicit syntax for pure type systems by showing that the conservativity and coherence conditions are satisfied. First, we define the notion of ϵ(Δ)-normal form. Because of possible loops in the graph of coercions, we are forced to consider a slightly weaker notion than usual. First, define M ↠_{ϵ(Δ|Γ)} N if there exists A such that Δ|Γ ⊢ M, N : A and M ↠_{ϵ(Δ)} N.

Definition 12 A term M is in ϵ(Δ|Γ)-normal form if

- there exists A such that Δ|Γ ⊢ M : A;

- if M ↠_{ϵ(Δ|Γ)} P, then there exists N such that P ↠_{ϵ(Δ|Γ)} N and N ↠_{β} M.

We will show that a term is in ϵ(Δ|Γ)-normal form if it is typable in a context without coercions. As usual, we say M has ϵ(Δ)-normal form N if Δ|Γ ⊢ M : A and M ↠_{ϵ(Δ|Γ)} N. The notion of normal form and reduction on contexts is defined recursively. We write, somewhat loosely, Γ, x : A ↠_{ϵ(Δ)} Γ′, x : A′ if Γ ↠_{ϵ(Δ)} Γ′ and A ↠_{ϵ(Δ|Γ)} A′.

The coherence condition can be stated as the condition that a legal term in context Δ|Γ has at most one ϵ(Δ)-normal form up to convertibility.

Proposition 13 (Coherence) Let Δ|Γ ⊢ M : A be a derivable judgement. Let M_{1}, M_{2} be ϵ(Δ|Γ)-normal forms for M. Then M_{1} =_{β} M_{2}.

Proof: the proposition is proved by induction on the structure of the terms. The only interesting case is when M = M_{1}M_{2}. By induction hypothesis, M_{1} and M_{2} have at most one ϵ(Δ|Γ)-normal form up to convertibility. Assume M has two ϵ(Δ|Γ)-normal forms N and P. We show they are β-convertible. First, note that there exist coercions i_{1}, …, i_{n}, j_{1}, …, j_{m} such that N = N_{1} (i_{1} ( … (i_{n} N_{2}) …)) and P = P_{1} (j_{1} ( … (j_{p} P_{2}) …)), where N_{k} and P_{k} are ϵ(Δ|Γ)-normal forms of M_{k} (k = 1, 2). By generation lemma, Δ|Γ ⊢ N′_{1}, P′_{1} : Πx : A.B and Δ|Γ ⊢ N′_{2}, P′_{2} : A′ with A′ linked to A. Again by generation, Δ|x : A′ ⊢ i_{1} ( … (i_{n} x) …) : A′ → A and Δ|x : A′ ⊢ j_{1} ( … (j_{p} x) …) : A′ → A. Both terms have a ϵ(Δ, x : A′)-normal form, say I and J respectively, with Δ|x : A′ ⊢ I, J : A′ → A. By coherence, we know I =_{β} J. Hence I[N′_{2}/x] =_{β} J[P′_{2}/x] and N′_{1} (I[N′_{2}/x]) =_{β} P′_{1} (J[P′_{2}/x]). □ We conclude:

Corollary 14 (Confluence of legal reduction) Let M be a legal term such that Δ|Γ ⊢ M : A. Let N, P be pseudo-terms such that M ↠_{mix(Δ|Γ)} N, P. Then there exists Q such that N, P ↠_{mix(Δ|Γ)} Q.

Proof sketch: first, prove confluence of legal reduction from ϵ-subject expansion, confluence of β-reduction and Proposition 13. Then conclude confluence of mix-reduction from Lemma 8.□ Using a similar induction principle as in Proposition 13, one can prove the existence of ϵ(Δ|Γ)-normal forms.

Proposition 15 Assume Δ|Γ ⊢ M : A. Then there exists an ϵ(Δ|Γ)-normal form N such that M ↠_{ϵ(Δ|Γ)} N.

In view of Proposition 15, the conservativity condition can be stated as the condition that ϵ(Δ|Γ)-normal forms are derivable in a context without coercions. This is proved by induction on the structure of derivations.

Proposition 16 (Conservativity) Assume Δ|Γ ⊢ M : A is a derivable judgement. Then for every ϵ(Δ|Γ)-normal forms Γ′, M′ and A′ of Γ, M and A, the judgement |Γ′ ⊢ M′ : A′ is derivable.

5.4 Decidability of type-checking

We can advocate Proposition 16, Lemmas 5 and 11 to reduce the problem of type-checking in a pure type system with inheritance λ_{inh}S to the problem of type-checking in the corresponding pure type system λS.

Proposition 17 Δ|Γ ⊢_{λ_{inh}S} M : A is derivable iff Δ is a coherent set of coercions and there exist Γ′, M′ and A′ such that Γ′ ⊢_{λS} M′ : A′ is derivable, Γ ↠_{ϵ(Δ)} Γ′, M ↠_{ϵ(Δ)} M′ and A ↠_{ϵ(Δ)} A′.

One strategy to check whether Δ|Γ ⊢ M : A is derivable is therefore to compute all possible legal ϵ(Δ) reductions of Γ, M and A. This is achieved by defining for every term M its set Exp_{Δ}(M) of possible explicitations of M relative to a set of pseudo-coercions Δ. In the sequel, we let Δ^{•} be the smallest subset of Δ^{+} containing:

- all the pseudo-coercions c : A → B of Δ such that A ≠_{β} B;

- all the pseudo-coercions λx : A_{1}.c_{n}(c_{n−1}(… (c_{1}x) …) : A_{1} → B_{n} where for i = 1, …, n, c_{i} : A_{i} → B_{i} are pseudo-coercions in Δ and

- A_{i+1} =_{β} B_{i} for i = 1, …, n − 1,

- A_{i} ≠_{β} B_{j} for i ≤ j.

In other words, Δ^{•} is the set of pseudo-coercions which do not contain any loop. Exp_{Δ}(M) is defined inductively on the structure of the terms:

Exp_{Δ}(x) = {x}
Exp_{Δ}(s) = {s}
Exp_{Δ}(Πx : A.B) = {Πx : A′.B′ | A′ ∈ Exp(A) ∧ B′ ∈ Exp_{Δ}(B)}
Exp_{Δ}(Σx : A.B) = {Σx : A′.B′ | A′ ∈ Exp(A) ∧ B′ ∈ Exp_{Δ}(B)}
Exp_{Δ}(λx : A.b) = {λx : A′.b′ | A′ ∈ Exp(A) ∧ b′ ∈ Exp_{Δ}(b)}
Exp_{Δ}(M N) = {M′(i[N′/x]) | M′ ∈ Exp_{Δ}(M), N′ ∈ Exp_{Δ}(N) and λx : A.i ∈ Δ^{•} for some A}
Exp_{Δ}(⟨a, b⟩) = {⟨a′, b′⟩ | a′ ∈ Exp(a) ∧ b′ ∈ Exp_{Δ}(b)}
Exp_{Δ}(fst M) = {fst M′ | M′ ∈ Exp_{Δ}(M)}
Exp_{Δ}(snd M) = {snd M′ | M′ ∈ Exp_{Δ}(M)}

where it is assumed that x is a variable and s is a sort.

Lemma 18 Δ|Γ ⊢_{λ_{inh}S} M : A is derivable iff Δ is a coherent set of coercions, Γ′ ⊢_{λS} M′ : A′ is derivable for some Γ′ ∈ Exp_{Δ}(Γ), M′ ∈ Exp(M) and A′ ∈ Exp_{Δ}(A).

The lemma follows from the observation that Exp_{Δ}(M) contains all the possible legal reducts of M. As Exp_{Δ}(M) is finite, we have a procedure to check whether a judgement is derivable in λ_{inh}S provided that:

- λS has decidable type-checking;

- it is decidable whether a set Δ of coercions is coherent;

- the closure Δ^{•} of a coherent set of coercions Δ can be computed effectively.

Note that the last two requirements are automatically fulfilled when the domains and codomains of the coercions are normalising.

Theorem 19 A pure type system with inheritance λ_{inh}S has decidable typechecking (and type-synthesis) if its correponding pure type system λS is normalising and has dedicable type-checking (and type-synthesis).

In [21], L.S. van Benthem Jutting has proved that type-checking and typesynthesis are decidable for a normalising pure type system with finitely many sorts. It follows that a pure type system with inheritance λ_{inh}S with inheritance has dedicable type-checking (and type-synthesis) whenever it has finitely many sorts and its underlying pure type system is β-normalising.

Corollary 20 The systems of the λ-cube with inheritance have decidable typechecking and type-synthesis.

5.5 Normalisation

A pure type system with inheritance is normalising provided its corresponding pure type system is. If Δ|Γ ⊢ M : A, a specific normalisation strategy consists in reducing M to ϵ(Δ)-normal form and then reduce this normal form to βnormal form. Note that this reduction strategy only performs mix-reduction steps. This specific strategy is sufficient for type-checking. However, one might wonder whether other reduction strategies terminate.

Proposition 21 Let λ_{inh}S be a pure type system with inheritance whose unerlying pure type system is strongly normalising. Assume Δ|Γ ⊢ M : A is a derivable judgement. Assume Δ ‘does not contain any loop’. Then every reduction sequence M →_{mix(Δ|Γ)} M_{1} →_{mix(Δ|Γ)} … terminates. If Δ ‘contains loops’, then for every infinite reduction sequence reduction sequence M →_{mix(Δ|Γ)} M_{1} →_{mix(Δ|Γ)} …, there exists a natural i s.t. M_{i} is in β and ϵ(Δ|Γ)-normal form.

6 Possible extensions and related work

In this section, we put our work into a more general perspective by looking at some possible extensions of our framework and some related work in this area.

6.1 Polymorphic coercions

In our syntax, coercions correspond to terms of type A → B in the empty context. In some cases, it is natural to define coercions polymorphically. For example, one might want to define a coercion forget which transforms a list of elements of an arbitray set into a multiset by forgetting the ordering. The type of forget is ΠT : Type.List T → Multiset T.

One can adapt our syntax to allow for polymorphic coercions, by defining a pseudo-coercion to be a pair of closed terms (t, Πx_{1} : A_{1}. . . . .Πx_{n} : A_{n}.B → C). However, it becomes difficult to define the notion of coherent set of coercions as we must consider instances of polymorphic coercions. One possibility to overcome the problem is to overlook the coherence problem. In this approach, it is not required that two coercions maps i, j : A → B are extensionally equal. Instead, one defines an order on coercions and use this order to determine which coercion to use to make a term fully explicit. This approach, which might be suited for pratical purposes, has the very strong disadvantage that it contradicts our intuition of inheritance.

6.2 Inheritance by delegation

An alternative approach to inheritance, suggested by P. Aczel, is to give a very syntactic treatment of inheritance. The idea, reminiscent of similar work in object-oriented programming ([16]), is to have special names for types (these names can be thought as classes) and see coercions as maps between those names. Let us exemplify this approach. Assume A is a type and A′ is a name for A. Then if we have a coercion f : A′ → B and a : A′, we will be allowed to write f a but if a : A, the expression will not be well typed. The advantage of this approach is that it simplifies the problem of coherence and type-checking. However, the approach is very intensional and seems to go against the traditional treatment of definitions. Further research is needed to see whether it is possible to obtain a system which combines the advantages of inheritance as presented in this paper and inheritance by delegation.

6.3 Subtyping

In our approach, the type system remains strongly typed in the sense that every term has at most one type (provided the pure type system is functional). One obvious extension to our work is to allow subtyping by replacing the Method rule with a subsumption rule

\frac{Δ|Γ ⊢ M : A}{Δ|Γ ⊢ M : A′} if (t : A → A′) ∈ Δ

Of course, ϵ-reduction has to be adapted in the obvious way. The syntax we thus obtain is closely related to Z. Luo’s coercive subtyping ([14]). Although we have not checked the details, we believe that the coherence and conservativity conditions still hold in a system with subtyping.

6.4 Classes

The original motivation for our work was to enhance proof-checkers with a notion similar to the one of type class as it is used in Clean ([18, 19]), Gofer ([11, 10, 12]) or Haskell ([9]). Although our work shares many motivations with type classes as developed in these languages, there are several differences worth noticing:

- type classes roughly correspond to Σ-types whose first component is a type. In contrast, we do not have any restriction on the domain and codomain of a coercion. This enables us to treat in an identical manner the canonical coercion from naturals to integers and the canonical coercion from groups to sets. In our view, our ability to give an uniform treatment of inheritance contributes to a clear understanding of the phenomenon involved;

- coercions between type classes are given by projections. In our case, coercions are arbitrary maps. There are several examples of coercions between Σ-types which are not projections: one such example is the canonical coercion from partial orders to total equivalence relations as defined in [4].

- one typical feature of type classes is their incremental built up; in contrast, our approach to inheritance does not require any order on the introduction of coercions, which makes the system much more flexible to use.

One possible drawback of our method is efficiency. In our syntax, there is no primitive notion of type class; instead type classes are encoded as Σ-types, which can be very inefficient.

Finally, it is worth noticing that simple coercions as formulated in our framework roughly correspond to type classes, while polymorphic coercions correspond to constructor classes. In fact, we have the following picture, where an arrow from A to B is used to indicate that A is a special case of B:

Simple coercions \underline{}Type classes
[figure]
Polymorphic coercions \underline{}Type Constructors

General coercions

The form of coercions allowed in each case is summarised below.

Type classes The domain and codomain of a coercion are Σ-types and the

coercion maps are projections.

Simple coercions The domain and codomain of a coercion are arbitrary types and

the coercion map is an arbitrary map between them.

Constructor classes Coercions are of type Πx : A.B → C where x is a vector or type variables and B, C are Σ-types. Coercions are polymorphic projections.

Polymorphic classes Coercions are arbitrary maps of type Πx : A.B → C where A, B

and C are arbitrary types.

General classes Coercions are arbitrary maps of type Πx : A.C.

7 Conclusion

In this paper, we have presented a modified syntax for pure type systems which allows for a uniform treatment of multiple inheritance. On a theoretical level, we have shown our syntax to be well-behaved and seen how it generalises the framework of type classes. At a practical level, experiments with an implementation of (single) inheritance in Lego have shown the framework to be particularly suited for formal mathematics: the new syntax gives the user more flexibility to express himself and enables him to use structured reasoning in an intuitive and direct manner.

In the short term, we believe that an implementation of multiple inheritance along the lines suggested in this paper would prove very useful in proof-checking. In a longer term, it seems important to give a neat treatment of polymorphic coercions. More generally, we will need to understand the interaction between inheritance, subtyping and argument synthesis in order to be able to bring the flexibility of expression in formal systems close to the one of informal mathematics. Such a program, if completed, would constitute a definite step towards feasible formal mathematics.

Acknowledgements

I am particularly indebted to Peter Aczel: the work presented here was very much influenced by the discussions we had while I was working in Manchester. He suggested me to implement inheritance in Lego, which was the starting point of this work. This work was partially supported by the Esprit project ‘Types: Types for programs and proofs’.

References

1. P. Aczel and G. Barthe. Classes in type theory. Note, 1993.

2. H. Barendregt. The quest for correctness. Draft, 1995.

3. H.P. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117–309. Oxford Science Publications, 1992.

4. G. Barthe. Formalising algebra in type theory: fundamentals and applications to group theory. Submitted for publication, 1995.

5. G. Barthe and H. Geuvers. Modular properties of algebraic pure type systems. Manuscript. To be presented at HOA’95, 1995.

6. R.L. Constable, S.F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, D.J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, J.T. Sasaki, and S.F. Smith. Implementing Mathematics with the NuPrl Development System. Prentice-Hall, inc., Englewood Cliffs, New Jersey, first edition, 1986.

7. N.G. de Bruijn. The mathematical vernacular, a language for mathematics with typed sets. In Nederpelt et al. [17], pages 865–935.

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

9. P. Hudak, S.L. Peyton Jones, P.L. Wadler, Arvind, B. Boutel, J. Fairbairn, J. Fasel, K. Guzman, K. Hammond, J. Hughes, T. Johnsson, R. Kieburtz, R.S. Nikhil, W. Partain, and J. Peterson. Report on the functional programming language Haskell, version 1.2. Special Issue of SIGPLAN Notices, 27, 1992.

10. M. Jones. Introduction to Gofer. Included as part of the Gofer distribution. Available by anonymous ftp from nebula.cs.yale.edu in the directory

pub/haskell/gofer, 1991.

11. M.P. Jones. Qualified types: theory and practice. PhD thesis, Oxford University, 1992. Appeared as technical monograph PRG-106.

12. M.P. Jones. A system of constructor classes: overloading and implicit higher-order polymorphism. Journal of Functional Programming, pages 1–25, January 1995.

13. Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Number 11 in International Series of Monographs on Computer Science. Oxford University Press, 1994.

14. Z. Luo. Coercive subtyping. Draft, 1995.

15. Z. Luo and R. Pollack. LEGO proof development system: User’s manual. Technical Report ECS-LFCS-92-211, LFCS, Computer Science Dept., University of Edinburgh, May 1992.

16. J. Mitchell and K. Fischer. A delegation-based object calculus with subtyping. In H. Reichel, editor, Proceedings of FCT’95, number 965 in Lecture Notes in Computer Science. Springer-Verlag, 1995.

17. R. Nederpelt, H. Geuvers, and R. de Vrijer, editors. Selected papers on Automath, volume 133 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1994.

18. M.J. Plasmeijer and M.C.J.D. van Eekelen. Functional Programming and Parallel Graph Rewriting. Addison-Wesley Publishing Company, 1993.

19. M.J. Plasmeijer and M.C.J.D. van Eekelen. Clean 1.0 reference manual. Technical report, Department of Computer Science, University of Nijmegen, 1995. In preparation.

20. R. Pollack. Implicit syntax. Informal Proceedings of First Workshop on Logical Frameworks, Antibes, May 1990.

21. L.S. van Benthem Jutting. Typing in Pure Type Sytems. Information and Computation, 105(1):30–41, July 1993.

22. P. Wadler and S.Blott. How to make ad hoc polymorphism less ad hoc. In Proceedings of POPL’89, pages 60–76. ACM Press, 1989.

23. A. Wikström. Functional Progrmmaming using Standard ML. Interntional Series in Computer Science. Prenctice Hall, 1987.

This article was processed using the L^{A}TEX macro package with LLNCS style