TECHNICAL REPORT 94-5e

On Extensions of F_{≤}: Second-Order Lambda-Calculus

with Subtyping

Daisuke Suzuki

March 1, 1994

�

Department of Information Science Faculty of Science, University of Tokyo

7–3–1 Hongo, Bunkyo-Ku Tokyo, 113 Japan

TECHNICAL REPORT 94-5e

TITLE On Extensions of F_{≤} : Second-Order Lambda-Calculus with Subtyping

AUTHORS Daisuke Suzuki

KEY WORDS AND PHRASES F_{≤} , parametric polymorphism, ad-hoc polymorphism, integration of two kinds of polymorphism

ABSTRACT

F_{≤} was an extension of a second-order λ -calculus F which has parametric polymorphism with subtyping and bounded quantification, introduced by Ghelli to apply second-order λ -calculi to the framework of object-oriented languages. However, it is impossible to know the amount of information of a type-checked term before evaluation since the subsumption rules are included in F_{≤} . To overcome this problem, we provided new calculi cF_{≤}^{+} and cF_{≤}^{++} as extensions of F_{≤} , and investigated their proof-theoretic properties. cF_{≤}^{+} includes a new type Range(X) , and cF_{≤}^{++} includes two new types Range(X) and Inst(X, T) . For example, the type Range(X) is provided for a type variable X whose upper bound is a function type, as a codomain type of X . When a function type S → T is substituted for X , Range(S → T) is reduced to T . For a type variable X whose upper bound is a universal type, the type Inst(X, U) is provided. When a universal type ∀Y ≤S.T is substituted for X , Inst(∀Y ≤S.T, U) is reduced to T [Y := U] . We showed that types are strongly normalizing under these reductions, and this is why, in cF_{≤}^{+} and cF_{≤}^{++} , a typechecked term can only have the minimal possible type in F_{≤} after reductions occurred. We also applied the techniques of these calculi to the other calculus cF_{≤}^{&}+ which integrates parametric polymorphism and ad-hoc polymorphism and investigated its proof-theoretical properties and its applications.

ANY OTHER IDENTIFYING INFORMATION OF THIS REPORT

DISTRIBUTION STATEMENT This technical report is available ONLY via anonymous FTP from ftp.is.s.u-tokyo.ac.jp (di-

rectory /pub/tech-reports).

SUPPLEMENTARY NOTES REPORT DATE March 1, 1994

TOTAL NO. OF PAGES 76 WRITTEN LANGUAGE English

NO. OF REFERENCES 64

DEPARTMENT OF INFORMATION SCIENCE Faculty of Science, University of Tokyo 7-3-1 Hongo, Bunkyo-ku Tokyo, 113 Japan

On Extensions of F_{≤}: Second-Order λ-Calculus with Subtyping

by Daisuke Suzuki

Master Thesis

Submitted to

the Graduate School of the University of Tokyo

in Partial Fulfillment of the Requirements for the Degree of Master of Science in Information Science

on Feb., 1994

Abstract

F_{≤} was an extension of a second-order λ -calculus F which has parametric polymorphism with subtyping and bounded quantification, introduced by Ghelli to apply second-order λ -calculi to the framework of object-oriented languages. However, it is impossible to know the amount of information of a type-checked term before evaluation since the subsumption rules are included in F_{≤} . To overcome this problem, we provided new calculi cF_{≤}^{+} and cF_{≤}^{++} as extensions of F_{≤} , and investigated their proof-theoretic properties. cF_{≤}^{+} includes a new type Range(X) , and cF_{≤}^{++} includes two new types Range(X) and Inst(X, T) . For example, the type Range(X) is provided for a type variable X whose upper bound is a function type, as a codomain type of X . When a function type S → T is substituted for X , Range(S → T) is reduced to T . For a type variable X whose upper bound is a universal type, the type Inst(X, U) is provided. When a universal type ∀Y ≤S.T is substituted for X , Inst(∀Y ≤S.T, U) is reduced to T [Y := U] . We showed that types are strongly normalizing under these reductions, and this is why, in cF_{≤}^{+} and cF_{≤}^{++} , a type-checked term can only have the minimal possible type in F_{≤} after reductions occurred. We also applied the techniques of these calculi to the other calculus cF_{≤}^{&}+ which integrates parametric polymorphism and ad-hoc polymorphism and investigated its proof-theoretical properties and its applications.

Contents

1 Introduction 1 1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.3 Contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.4 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2 Survey of Polymorphism 5 2.1 Polymorphism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Parametric Polymorphism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2.2.1 Second-order Lambda Calculus . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2.2 Application to Object-Oriented Languages . . . . . . . . . . . . . . . . . . . 6

2.3 Ad-hoc Polymorphism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.4 Symbiosis of Parametric and Ad-hoc Polymorphism . . . . . . . . . . . . . . . . . 9

2.4.1 Integrating Intersection Types . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.4.2 Integrating Overloaded Function . . . . . . . . . . . . . . . . . . . . . . . . 9

3 cF_{≤}^{+} —A Type System without Type instantiation 11 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.2 Type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

3.2.1 Type Judgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.2.2 Subtype Relation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

3.3 Term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3.3.1 Term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 3.3.2 Reduction system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

3.4 Strong Normalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.4.1 Outline of the Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.4.2 Untyped Translation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.4.3 Termination of Type-erasure of cF_{≤}^{+} Terms . . . . . . . . . . . . . . . . . . 32 3.4.4 Termination of cF_{≤}^{+} Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

3.5 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

4 cF_{≤}^{++} —A Type System with Type instantiation 41 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 4.2 Kind . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 4.3 Type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

4.3.1 Type Judgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 4.3.2 Subtype Relation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

4.4 Term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 4.4.1 Term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

4.4.2 Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 4.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53

5 Symbiosis of Parametric and Ad-hoc Polymorphisms 55 5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 5.2 Type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 5.3 Term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 5.4 Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 5.5 Example of Applications to Object-Oriented Languages . . . . . . . . . . . . . . . 65 5.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66

6 Conclusion 67 6.1 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 6.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67

List of Figures

2.1 Program in CLOS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2 Program in C++ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 5.1 Example of the Structure of ∩ -closed Set . . . . . . . . . . . . . . . . . . . . . . . 59

Chapter 1

Introduction

1.1 Background

Polymorphism is one of the important tools for increasing programming efficiency and re-usability of programs. Polymorphism has two classifications: “parametric vs ad hoc” (see [Str67]) and “implicit vs explicit”. A parametric polymorphic function is defined uniformly over types. That is, though a parametric polymorphic function behaves as a collection of monomorphic functions, they have the shared procedure written as a single lambda expression. System F [Gir72] enables us to treat parametric polymorphic functions as first-order objects. From the point of view of object-oriented languages which support the notion of subtyping, F_{≤} [Ghe90, CG92, CG93] is presented by Ghelli. F_{≤} is a conservative extension of F , which has the notion of subtyping and allows us to specify bounds on ∀ -types. In addition, there are many studies about characterizing a parametric polymorphic function in model theory and category theory.

1.2 Motivation

However, in F_{≤} , there is a problem because the system F_{≤} has the subsumption rule as follows:

\begin{matrix}Γ ⊢ e:S & Γ ⊢ S ≤ T \\ Γ ⊢ e:T \end{matrix} (Sub) .

To tell the problem easier, we now consider an extension of F_{≤} with records, where a record types is expressed as:

[l_{1}:T_{1}, ⋯, l_{n}:T_{n}],

the subtyping rule of record types is expressed as:

For all i = 1, ⋯, n, Γ ⊢ S_{i} ≤ T_{i} \{ \begin{matrix}Γ ⊢ [l_{1}:S_{1}, ⋯, l_{n}:S_{n}, l_{n+1}:S_{n+1}, ⋯, l_{n+m}:S_{n+m}] \\ ≤ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] \end{matrix} ( ≤ -record) ,

and record terms and their functions are described as:

{l_{1}=m_{1}, ⋯, l_{n}=m_{n}}  record term m · l  record field selection {l_{1}=m_{1}, ⋯, l_{n}=m_{n}} · l_{i} → m_{i} reduction of field selection (i = 1, …, n) .

In the system, a raw term e = ΛX≤[l:T].λx^{X}.x · l can have the type ∀X≤[l:T].X → T because

\begin{matrix}\begin{matrix}{X ≤ [l:T] ⊢ X type \atop X ≤ [l:T] ⊢ x^{X} : X} & X ≤ [l:T] ⊢ X ≤ [l:T] \\ X ≤ [l:T] ⊢ x^{X} : [l:T] \end{matrix} & (Sub) \\ X ≤ [l:T] ⊢ x^{X} · T \end{matrix} ; X ≤ [l:T] ⊢ λx^{X}.x · l : X → T ⊢ ΛX≤[l:T].λx^{X}.x · l : ∀X≤[l:T].X → T .

However, for any T ’s subtype S and any term n of the type S , when e is applied to a type [l:S] and a term {l=n} of the type [l:S] , e{[l:S]}({l=n}) has the type T , not S , because

\begin{matrix}\begin{matrix}⋮ . ; ⊢ e : ∀X≤[l:T].X → T & ⋮ . ; ⊢ S ≤ T ; ⊢ [l:S] ≤ [l:T] \\ ⊢ e[l:S] : [l:S] → T \end{matrix} & ⋮ . ; ⊢ n : S ; ⊢ \{l=n\} : [l:S] \\ ⊢ e[l:S]\{l=n\} : T \end{matrix} .

while n, where

e{[l:S]}({l=n}) → (λx^{[l:S]}.x · l)({l=n}) → {l=n} · l → n,

can have the type S . That is, before reductions occur, we do not know whether we can fully obtain the information the term n of type S has.

1.3 Contribution

To overcome this problem, we provide new calculi cF_{≤}^{+} and cF_{≤}^{++} as extensions of the system cF_{≤} ( F_{≤} where the subsumption rule is replaced with the coercion rule) enriched with two new types Range(X) and Inst(X, T) where X is a type variable. In the case of Range(X) , function types may be substituted for X and when a function type S → U is substituted for X , Range(X) is reduced to the type U . In the case of Inst(X, T) , (bounded) universal types may be substituted for X and a universal type ∀X≤S.U is substituted for X , Inst(X, T) is “reduced” to the type U[X: = T] .

In the system F_{≤} , every term expression can have two or more types and therefore much information may not be obtained. On the contrary, in cF_{≤}^{+} , for each term expression, its type is uniquely determined and the amount of information loss be smaller.

cF_{≤}^{+} has other virtues: In cF_{≤} , which is a variety of F_{≤} where the subsumption rule is replaced with the rule of coercion operator, we can write few terms which can type-check without a coercion operator. For example, in cF_{≤} , e = ΛX≤(S → T).λx^{X}.λy^{S}.xy cannot have its type, while, in F_{≤} , it has its type ∀X≤(S → T).X → (S → T) . In cF_{≤}^{+} , e has a type ∀X≤(S → T).X → (S → Range(X)) . When a type U → V which is a subtype of S → T is applied, e{U → V } has a type (U → V) → (S → V) because Range(U → V) is reduced to V .

We think that cF_{≤}^{+} is more applicable to object-oriented languages than F_{≤} because for each term, its type is uniquely determined in cF_{≤}^{+} , and because cF_{≤}^{+} satisfies Subject Reduction, that is, for each term, its type does not change when any reduction occurs.

1.4 Outline

We describe the contents of the rest of this thesis.

2. In Chapter 2, we give more details of the background of this thesis. We give a survey of parametric polymorphism, ad-hoc polymorphism, and calculi which integrate two kinds of polymorphisms.

3. Chapter 3 is devoted to the study of a calculus cF_{≤}^{+} . cF_{≤}^{+} is a second order λ -calculus with coercion operator and bounded quantification. To let the unicity of type hold in cF_{≤}^{+} , the rules of coercion operator are used, instead of the subsumption rule in F_{≤} . To avoid the problem about the termination of the “reduction” of types, the type instantiation rule Inst(∀X≤.S.T, U) ⇒ T [X: = U] is not used. Instead, we enrich this calculus with records and a new type Sel(X, l) . In Sel(X, l) , record types which have a field of label l will be substituted for X , and when […, l:T, …] is substituted for X , Sel(X, l) is reduced to T which is the type of the field l. Moreover, we show that cF_{≤}^{+} has good proof-theoretical properties: Subject Reduction, Church-Rosser, and Strong Normalization. To prove the Strong Normalization, we use a method of saturated sets, a variation of untyped version of reducibility predicates [Gir72, GLT89]. In cF_{≤}^{+} , e = ΛX≤[l:T].λx^{X}.x · l (which already appeared in Section 1.2) has the type ∀X≤[l:T].X → Sel(X, l) and when e is applied to a type [l:S] where S is a subtype of T , e{[l:S]} has the type [l:S] → S because Sel([l:S], l) is reduced to S . Moreover, when e{[l:S]} is applied to {l=n} of the type [l:S] , e{[l:S]}({l=n}) has the type S and it is reduced to n of the type S .

4. In Chapter 4, we give a calculus cF_{≤}^{++} by adding the type instantiation rule to cF_{≤}^{+} . In cF_{≤}^{++} , we show that the type system of cF_{≤}^{++} is well defined, for example, that the type instantiation rule (like β -reduction in λ -calculi) Inst(∀X≤S.T, U) ⇒ T [X: = U] always terminates. He proves it by attributing types to “kind”. We also shows that cF_{≤}^{++} satisfies the Subject Reduction and the Church-Rosser.

5. Chapter 5 tells about cF_{≤}^{&}+ , another variety of cF_{≤}^{+} which implements symbiosis of parametric polymorphism and (a very restricted version of) ad-hoc polymorphism. In cF_{≤}^{&}+ , the facility of ad-hoc polymorphism is implemented by overloaded functions as in F_{≤}^{&} . An overloaded function is a set of functions whose behaviors are not related to the others. Every function in it has its eigen type, and when the overloaded function is applied to a type, the component function whose eigen type matches the argument type is driven and returns a value. All eigen types in cF_{≤}^{&}+ are restricted to base types and record types whose all elements are base types. In cF_{≤}^{&}+ , type instantiation rules are adopted but permitted only for overloaded types. We also show that cF_{≤}^{&}+ satisfies Church-Rosser and Subject Reduction. Finally we give some examples of applying cF_{≤}^{&}+ to object-oriented languages. The contents of Chapter 5 are not related to those of Chapter 4. So, if you skip Chapter 4 or Chapter 5, no confusion will occur.

6. Finally the conclusion of this thesis is written in Chapter 6. The future works for our research are also described.

Acknowledgements

I wish to express my gratitude to Masami Hagiya and colleagues.

4 CHAPTER 1. INTRODUCTION

Survey of Polymorphism

2.1 Polymorphism

Polymorphism is one of the important tools for increasing programming efficiency and re-usability of programs. Polymorphism has a classification: “parametric vs ad-hoc”. In addition, there are many studies about characterizing a parametric polymorphic function in model theory and category theory. However, in F (and F_{≤} ), a polymorphic function whose behavior on different types is not related cannot be written.

2.2 Parametric Polymorphism

A parametric polymorphic function is a function which is defined uniformly over types. That is, though a parametric polymorphic function behaves as a collection of monomorphic functions, they have the shared procedure written as a single lambda expression.

Example 2.2.1.

PolyId = ΛX.λx^{X}.x is a polymorphic identity function. When it is applied to a type S , (PolyId){S} is a function which receives a value of type S and returns it without any modification. In other words, PolyId behaves as {λx^{S}.x | S : type}, which is a collection of identity functions for all types.

The notion of parametric polymorphism is important and used in many functional programming languages (ML [AM87, AM91], Haskell [HW90], etc.).

Example 2.2.2.

Here are polymorphic functions in ML, hd and tl. hd receives a finite list of some type X and returns its head and tl receives a finite list of some type X and returns it after its head eliminated. The two functions behaves regardless of the type of arguments (int list, string list, int list list). They are polymorphic since they are uniformly defined over all list types.

- fun hd [] = raise Hd
=   | hd (x::_) = x;
val hd = fn : 'a list -> 'a
- fun tl [] = raise Tl
=   | tl (_::y) = y;
val tl = fn : 'a list -> 'a list
- hd [2,3,4,5];

val it = 2 : int
- hd ["aa", "bb"];
val it = "aa" : string
- tl [2,3,4,5];
val it = [3,4,5] : int list
- tl ["aa", "bb"];
val it = ["bb"] : string list
- hd [[2,3,4],[3],[]];
val it = [2,3,4] : int list
- tl [[2,3,4],[3],[]];
val it = [[3],[]] : int list list
-

2.2.1 Second-order Lambda Calculus

System F [Gir72, GLT89, Rey74] enables us to treat parametric polymorphic functions as firstorder objects. A parametric polymorphic function is also characterized in a model as a function which preserves all the relations between all the types. To explain it in more detail, suppose that F (t) → G(t) is a type of a polymorphic function with a type variable t. When there exists a relation R between two types S and T , then we can form a relation F(R) between F (S) and F (T) , and G(R) between G(S) and G(T) . A parametric function is a collection of functions {f(t) : F (t) → G(t) | t : type} indexed by types such that for each relation R between two types S and T , when x ∈ F (S) and y ∈ F (T) are related by F(R) , then f{S}(x) ∈ G(S) and f{T }(y) ∈ G(T) are related by G(R) . Reynolds characterized polymorphism using this in the first order case and gave an idea to extend it to the second order case [Rey83]. This property have been later proved to be a natural condition for a model to have natural categorical properties [Has90, Has91, MR91].

2.2.2 Application to Object-Oriented Languages

From the point of view of object-oriented languages which support the notion of subtyping, F_{≤} [CG92, CG93, Ghe90] is introduced by Ghelli. F_{≤} is an abstract version of the language Fun [CW85]. The language Fun was defined as a formal system to collect some different capabilities, as parametric polymorphism, hierarchical polymorphism, recursion and abstract data types, which can be found in different programming language. F_{≤} is in some way the kernel of the language Fun. F_{≤} is also a conservative extension of F , which allows us to specify bounds on ∀ -function types. F-bounded was also abstracted from Fun by Cook et al. [CCHMO89], where a type variable X has a upper bound which can contain a type variable X . F-bounded is useful for typing object-oriented programs which involve recursive types: it allows quantification over types that are “structurally similar” to the recursive type Rect.F[t] . F-bounded is currently included in many proposals for strongly typed object-oriented languages (e.g. [Bru93, Mit90, KLM94].

However, its proof-theoretical property and semantics are not widely studied because of its complicatedness [Ghe93].

However in F (and F_{≤} and F-bounded ), a polymorphic function whose behavior on different types is not related to each other cannot be written.

2.3 Ad-hoc Polymorphism

Such a polymorphic function is called an ad-hoc polymorphic function. An example of such a function is a function which is written by type case. In other words, it performs a dispatch on a type passed as an argument. Ad-hoc polymorphism can be modeled using generic functions. For example, Common Lisp Object System, or CLOS [DG87, BDGKK88], which is a standard for merging object oriented programming with Common Lisp, implements message passing using generic functions, and in C++[Str88] multiple inheritance is implemented using overloading.

 (defclass secondvec () ((x :initarg :x :reader x) (y :initarg :y :reader y)))
 (defclass thirdvec (secondvec) ((z :initarg :z :reader z)))
 (defgeneric size (secondvec))
 (defmethod size ((s secondvec)) (let ((x (x s)) (y (y s)))
                                   (sqrt (+ (* x x) (* y y)))))
 (defmethod size ((s thirdvec)) (let ((x (x s)) (y (y s)) (z (z s)))
                                  (sqrt (+ (* x x) (* y y) (* z z)))))

Figure 2.1: Program in CLOS

Example 2.3.1.

Here is an example in CLOS in Figure 2.1. The generic function size is a function which receives a vector value and returns its size. When size is applied to {x=1, y=1} of type [x:Int, y:Int] , it returns a value \sqrt{x^{2} + y^{2}} . When size is applied to \{x=1, y=1, z=1\} of type [x:Int, y:Int, z:Int] , it returns a value \sqrt{x^{2} + y^{2} + z^{2}} . size is ad-hoc because it is defined dependently on the type of its argument.

The result of execurion is:

>(size (make-instance 'secondvec :x 1 :y 1))
1.4142135623730951
>(size (make-instance 'thirdvec :x 1 :y 1 :z 1))
1.7320508075688772
>

.

Example 2.3.2.

Here is an example in C++[Str88] in Figure 2.2. In the following program, the class human and its subclass student are defined, where human, id, name, and sex, which are the methods of human, are inherited by student, while print not inherited.

The result of execution is:

% ./a.out
Name = Taro ,sex = male
Name = Hanako ,sex = female, school = U_TOKYO ,year = 1
%

The notion of ad-hoc polymorphism is also important and used in many programming languages. However, ad-hoc polymorphism has not received so much attention as parametric polymorphism. Wadler tried to preset type classes which permit overloading of arithmetic operators in the framework of functional programming language practically [WB89]. In [CGL92], with the definition of the λ& -calculus, Castagna, Ghelli and Longo started a theoretical analysis of ad-hoc polymorphism with the basis of message passing [Ghe91]. In λ& , an overloaded function is represented by a list of ordinary functions. When an overloaded function is applied to an argument, it selects only one function from the component functions according to the type of the argument, and returns the result. Therefore, in λ& , an ad-hoc polymorphic function whose behavior on different argument types is entirely unrelated is easily written as a first-class object. Tsuiki proposed a calculus λ_{m} [Tsu92, Tsu93, Tsu94a], which is a simply typed λ -calculus enriched with subtyping, coercion and merge operator. Merge operator is provided by generalizing from record merge operator of the extension of ML type system with record [OB88, Wan89]. In λ_{m} , the notion of merge to functions is introduced and it is good-natured in the sense that the behavior

#include <stream.h>
#include <strings.h>
class human {
public:
int id;
char name[30];
enum {male , female} sex;
void print();
};
class student:public human
{
public:
char school[20];
int year;
void print();
};
void human::print() {
cout << "Name = " << name << " ,sex = " << ((sex == male) ?
                                           "male" : "female")
     << "\n";
};

void student::print() {
cout << "Name = " << name << " ,sex = " << ((sex == male) ?
                                           "male" : "female")
     << ", school = " << school << " ,year = " << year
     << "\n";
};
main()
{
human a;
student b;
a.id = 1;
strcpy(a.name,"Taro");
a.sex = 0;
a.print();
b.id = 2;
strcpy(b.name,"Hanako");
b.sex = 1;
strcpy(b.school,"U_TOKYO");
b.year = 1;
b.print();
}

Figure 2.2: Program in C++ on a subtype inherits those on its supertypes. A merge of functions activates all of appropriate functions and merges their effects. Therefore, component functions work together to calculate a result; and thus the behavior of a function on each type is closely related. We may say that the merge operator will bridge the gap between parametric and ad-hoc polymorphism. In order to select applicable functions, λ& and λ_{m} use type information at runtime in contrast to the simply typed lambda calculus which ignore type information at runtime. λ&C^{∗} is introduced by Tsuiki [Tsu94] in order to overcome the problem that properties of subject reduction property and strong normalization are satisfied in λ& . In [Tsu94] the method of compiling λ&G, which is a simplification of λ&C^{∗} , to a untyped calculus is provided and therefore type information need not be used at runtime in λ&G.

2.4 Symbiosis of Parametric and Ad-hoc Polymorphism

2.4.1 Integrating Intersection Types

The idea of intersection types consists of enriching the collection of types with a new type σ∧τ for every pair of types σ and τ . This new type is thought of as containing all the elements of σ that are also elements of τ . The most intriguing and potentially useful property of intersection types is their ability to express an essentially unbounded amount of information about the components of a program. Intersection types can also be viewed as a natural type-theoretic analogy of multiple inheritance. Pierce provided a detailed investigation of a (second order) typed λ -calculus F_{∧}

[Pie91] combining intersection types and bounded quantification. In this calculus parametric and finitary (ad-hoc) polymorphisms complement each other. As a joint work with Turner, Pierce recently provided a typed λ -calculus combining intersection types and bounded quantification F_{∧}^{ω} [PT93, PT93a] in the framework of higher-order λ -calculus F_{ω} [Gir72]. However, in this framework, calculi which satisfy the unicity of type are not widely investigated.

2.4.2 Integrating Overloaded Function

Castagna introduced F_{≤}^{&} [Cas93], which integrates parametric polymorphism and “explicit” adhoc polymorphism. In F_{≤}^{&} , a function which performs a dispatch on a type passed as an argument would be written as: ( X means type variables)

ΛX ≤ T_{1}.exp_{1} & ΛX ≤ T_{2}.exp_{2} & ⋯ & ΛX ≤ T_{n}.exp_{n}

When this function is applied to a type V , ΛX ≤ T_{i}.exp_{i} which satisfies T_{i} = min{T_{k} |k = 1, …, n , V ≤ T_{k}}^{1} is selected and returns the value exp_{i}[X := V] . But F_{≤}^{&} includes many mistakes, which will be described in Chapter 5. However, it provides a clue to integrating parametric polymorphism and ad-hoc polymorphism.

1 min is defined over subtyping relation.

10 CHAPTER 2. SURVEY OF POLYMORPHISM

cF_{≤}^{+}—A Type System without

Type instantiation

In this thesis, the notations of λ -calculus is based on the Barendregt’s standard textbook [Bar84].

3.1 Introduction

As in Section 1.2, Because F_{≤} (with records) has the subsumption rule as follows:

\begin{matrix}Γ ⊢ e:S & Γ ⊢ S ≤ T \\ Γ ⊢ e:T \end{matrix} (Sub) ,

a raw term e = ΛX ≤ [l:T]λx^{X}.x · l can only have the type ∀X ≤ [l:T].X → T . However, for any T ’s subtype S and any term n of the type S , when e is applied to the type [l:S] and the term {l=n} (of the type [l:S] ), e{[l:S]}({l=n}) has the type T , not S . However n, where e{[l:S]}({l=n}) →^{∗} n, can have the type S . That is, before reductions occur, we do not know whether we can fully obtain the information the term n of type S has.

To overcome this problem, we provide a new calculus cF_{≤}^{+} as an extension of the system cF_{≤} ( F_{≤} where the subsumption rule is replaced with the coercion rule) with two new types Range(X) and Sel(X, l) where X is a type variable. In cF_{≤}^{+} , e has the type ∀X≤[l:T].X → Sel(X, l) and when e is applied to a type [l:S] , e{[l:S]} has a type [l:S] → S . Moreover, when e{[l:S]} is applied to {l=n} of the type [l:S] , e{[l:S]}({l=n}) has the type S and it is reduced to n of the type S .

In this chapter, we do not consider the type instantiation such that Inst(∀X≤S.T, U) ⇒ T [X := U] like β -reduction in λ -calculus because the termination of the instantiation is not trivially proved. The calculus which includes the type instantiation will be discussed in the next chapter. Instead of the type instantiation, we consider the calculus including records.

3.2 Type

In this section, we describe the type system cF_{≤}^{+} . In this thesis we assume that there is no subtype relation between base types (for example, Int ≤ Real ).

Notation 3.2.1.

We uses these following notations when no specific notation is declared.

12 CHAPTER 3. CF_{≤}^{+} —A TYPE SYSTEM WITHOUT TYPE INSTANTIATION

Notation  Metavariables
Type Environments  Γ, Δ, …
Type Variables  X, Y, …
Type Constants  A, B, …
Non-well-working Type P, Q, …
Type  S, T, U, …
Term Variables  x, y, …
Term Constants  a, b, …
Term  e, f, …

Notation 3.2.2.

We define a countable set of labels for records L

Definition 3.2.3. (Raw Type)

Raw types are defined as follows.

T := P  non-well-working type
| W  working type
P := X  type variable
| Range(P)  range type
| Sel(P, l)  field type (l ∈ L)
W := B  base type
| T → T  function type
| ∀X.T  universal type
| ∀X≤T.T  bounded universal type
| [l_{1} : T, …, l_{n} : T] record type (l_{i} ∈ L (i = 1, …, n))

The definition of raw types is an extension of that of F_{≤} . Raw types are divided into working types and non-well-working types. Working types consist of function types and (bounded) universal types, which are the same as defined in F_{≤} . Non-well-working types consists of type variables, range types, and field types. Range types have the feature Range(P) , where P has a super type that is a function type, and when a function type S → U is substituted for P , Range(P) is reduced to U .

Field types have the feature Sel(P, l_{i}) , where P has a super type that is a record type, and when a record type [l_{1}:U_{1}, ⋯, l_{i}:U_{i}, ⋯, l_{n}:U_{n}] which contains the field l_{i} is substituted for P , Sel(P, l_{i}) is reduced to U_{i} .

Definition 3.2.4. (Normal Form)

We call a raw type P in normal form if P does not contain Range(S → T) or Sel([⋯, l:T, ⋯]) .

Definition 3.2.5.

For a non-well-working type Range(P) (respectively Sel(P, l_{i}) ), a working type S → T ( [l_{1} : T_{1}, ⋯, l_{i} : T_{i}, ⋯, l_{n} : T_{n}] ) is substituted for P . The (raw) type Range(S → T) ( Sel([l_{1} : T_{1}, ⋯, l_{i} : T_{i}, ⋯, l_{n} : T_{n}], l_{i}) ) need to be reduced to a normal form during these rules:

Range(S → T)  ⇒ T
Sel([l_{1} : T_{1}, ⋯, l_{i} : T_{i}, ⋯, l_{n} : T_{n}], l_{i}) ⇒ T_{i} (1 ≤ i ≤ n)

After a finite number of reductions, Range(S → T) (respectively Sel([l_{1} : T_{1}, ⋯, l_{i} : T_{i}, ⋯, l_{n} : T_{n}], l_{i}) ) is reduced to V which need not be reduced, we write down Range(S → T) ≡⟩ V ( Sel([l_{1} : T_{1}, ⋯, l_{i} : T_{i}, ⋯, l_{n} : T_{n}], l_{i}) ≡⟩ V ).

Definition 3.2.6. (Type Environment)

( Γ env ) In cF_{≤}^{+} , a (type) environment is defined as a sequence of free type variables and pairs of free type variables and its “upper bound”. It is mutually defined to that of type-good formarion (in Definition 3.2.11).

ϕ env
Γ env Γ ⊢ T type X ∉ FV(Γ)
Γ, X ≤ T env
Γ env X ∉ FV(Γ)
Γ, X env

Notation 3.2.7.

Under an environment Γ = Δ, X ≤ T, Δ′ , for the type variable X , we call T the least upper bound (l.u.b.) of X . We represent the least upper bound of X as Γ(X) .

We want to extend the notion of l.u.b. to non-well-working types.

Definition 3.2.8.

For each type T , we want to define l.u.b. of T , Γ(T) . Of course, when T is a working type or T = X where Γ = Δ, X, Δ′ , we define Γ(T) ≡ T . Otherwise, that is, when P is a non-well-working type, we define Γ(P) as follows:

Γ(X)  ≡ T (where Γ = Δ, X ≤ T, Δ′)
Γ(Range(P)) ≡ V (where Range(Γ(P), T)≡⟩V)
Γ(Sel(P, l)) ≡ V (where Sel(Γ(P), l)≡⟩V)

Definition 3.2.9.

To obtain the working upper bound of a non working type P , we recursively define the working least upper bound (w.l.u.b.) Γ^{∗}(P) as follows:

Γ^{∗}(T) = T  (T is a working type)
| X  (T is a type variable X and Γ = Δ, X, Δ′)
| Γ^{∗}(V) (T is a non-well-working type and Γ(T)≡⟩V)

Proposition 3.2.10.

The maximum of the size of the recursive definition Γ^{∗} is limited by the size of Γ because of the definition of the type environment Γ .

( Proof ): Because of the definition of the type environment Γ .

3.2.1 Type Judgements

We have three kinds of type judgements: for the type good-formation (Γ ⊢ S type) , for the subtyping relation (Γ ⊢ S ≤ T) and for the type assignment (Γ ⊢ e : S) . We also call the first two kinds of judgements type judgements. All kinds of type judgements are mutually defined.

Definition 3.2.11. (Type good-formation ( Γ ⊢ S type ))

We define the judgement of the type “good-formation”.

{X ∈ F V (Γ) \atop Γ ⊢ X type} (Var)
Γ ⊢ S type Γ ⊢ T type

Γ ⊢ S → T type (→)

Γ, X ⊢ T type

Γ ⊢ ∀X.T type (∀)

Γ ⊢ S type Γ, X ≤ S ⊢ T type
Γ ⊢ ∀X≤S.T type

(bound-∀)

For all i = 1, ⋯, n, Γ ⊢ T_{i} type Γ ⊢ [l_{1} : T_{1}, ⋯, l_{n} : T_{n}] type

(record)

Γ ⊢ P type Γ^{∗}(P) = S → T

Γ ⊢ Range(P) type

(Range)

Γ ⊢ P type Γ^{∗}(P) = [l_{1} : T_{1} ⋯, l_{i} : T_{i}, ⋯, l_{n} : T_{n}]
Γ ⊢ Sel(P, l_{i}) type

(record-Var)

3.2. TYPE 15

3.2.2 Subtype Relation

Definition 3.2.12. (Subtype Relation ( Γ ⊢ S ≤ T ))

The definitions of the subtype relation are listed as follows:

{Γ ⊢ T type \atop Γ ⊢ T ≤ T} (≤-Refl)
\begin{matrix}Γ ⊢ S ≤ T & Γ ⊢ T ≤ U \\ Γ ⊢ S ≤ U \end{matrix} (≤-Trans)
Γ ⊢ P type Γ(P)≡⟩V Γ ⊢ V ≤ T

Γ ⊢ P ≤ T (≤-Taut)

\begin{matrix}Γ ⊢ S′ ≤ S & Γ ⊢ T ≤ T′ \\ Γ ⊢ S → T ≤ S′ → T′ \end{matrix} (≤-→)
\begin{matrix}Γ ⊢ ∀X.T type & Γ, X ⊢ T ≤ T′ \\ Γ ⊢ ∀X.T ≤ ∀X.T′ \end{matrix} (≤-∀)
Γ ⊢ ∀X.T type Γ ⊢ S′ type Γ, X ≤ S′ ⊢ T ≤ T′

Γ ⊢ ∀X.T ≤ ∀X≤S′.T′ (≤-b∀)

Γ ⊢ ∀X≤S.T type Γ ⊢ S′ ≤ S Γ, X ≤ S′ ⊢ T ≤ T′

Γ ⊢ ∀X≤S.T ≤ ∀X≤S′.T′ (≤-bb∀)

For all i = 1, ⋯, n, Γ ⊢ S_{i} ≤ T_{i}

\{ \begin{matrix}Γ ⊢ [l_{1}:S_{1}, ⋯, l_{n}:S_{n}, l_{n+1}:S_{n+1}, ⋯, l_{n+m}:S_{n+m}] \\ ≤ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] \end{matrix}

(≤-record)
Γ ⊢ Range(P) type Γ ⊢ Range(Q) type Γ ⊢ P ≤ Q

Γ ⊢ Range(P) ≤ Range(Q)

(Range)

Γ ⊢ Sel(P, l) type Γ ⊢ Sel(Q, l) type Γ ⊢ P ≤ Q
Γ ⊢ Sel(P, l) ≤ Sel(Q, l)

(Sel)

Definition 3.2.13. (Degree of Type)

Under an environment Γ , for each well-formed type T , we define the size of the type T as follows:

Deg( env)_{{ϕ}}  = 1
Deg( env)_{{Γ,X}}  = Deg( env)_{{Γ}} + 1
Deg( env)_{{Γ,X≤S}}  = Deg( env)_{{Γ}} + Deg(S)_{{Γ}} + 1
Deg(B)_{{Γ}}  = 1

(B is a base type)

Deg(X)_{{Γ}}  = 1

(Γ = Δ, X, Δ′)

Deg(X)_{{Γ}}  = Deg(T)_{{Γ}} + 1

(Γ = Δ, X ≤ T, Δ′)

Deg(Range(P))_{{Γ}}  = Deg(S)_{{Γ}} + Deg(V)_{{Γ}} + 1

( Γ ⊢ Γ(P)≡⟩V)

Deg(S → T)_{{Γ}}  = Deg(S)_{{Γ}} + Deg(T)_{{Γ}} + 1
Deg(∀X≤S.T)_{{Γ}}  = Deg(S)_{{Γ}} + Deg(T)_{{Γ,X≤S}} + 1
Deg([l_{1} : T_{1}, ⋯, l_{n} : T_{n}])_{{Γ}} = Σ_{i=1,···n}(Deg(T_{i})_{{Γ}}) + 1
Deg(S ≤ T)_{{Γ}}  = Deg(S)_{{Γ}} + Deg(T)_{{Γ}} + 1

From these definitions, the following properties are satisfied.

Proposition 3.2.14.

If Γ ⊢ S ≤ T holds, then Γ ⊢ S type and Γ ⊢ T type hold.

( Proof ): Obvious from definitions.

Proposition 3.2.15.

1. The rule ( Range ) and ( Sel ) can be removed from the subtype relation rules.

2. The rule ( ≤ -Trans) can be removed from the subtype relation rules.

( Proof ):

1. To prove Γ ⊢ P ≤ P , we can apply the rule (Refl). To prove Γ ⊢ P ≤ Q, we must apply the rule (Taut) after several ( Range ) or ( Sel ) rules. Therefore we can first apply the rule (Taut) without ( Range ) or ( Sel ). For example,

Γ ⊢ P′ type Γ(P′) ≡⟩ V′ Γ ⊢ V′ ≤ Q′

Γ ⊢ P′ ≤ Q′ (Taut)

⋮ . Applying several ( ≤ - Range ) or ( ≤ - Sel )

Γ ⊢ P ≤ Q

can be replaced with

Γ ⊢ P type Γ(P) ≡⟩ V  Γ ⊢ V′ ≤ Q′ ; ⋮ . ; Γ ⊢ V ≤ Q

Γ ⊢ P ≤ Q (Taut)

2. We prove that

\begin{matrix}Γ ⊢ S ≤ T & Γ ⊢ T ≤ U \\ Γ ⊢ S ≤ U \end{matrix} (Tran)

can be eliminated by induction on the depth of the proof of Γ ⊢ S ≤ U .

(1) ( S , T , and U are → -types.) In this case

\begin{matrix}⋮ . ; Γ ⊢ T ≤ S & ⋮ . ; Γ ⊢ S′ ≤ T′ \\ Γ ⊢ S → S′ ≤ T → T′ \end{matrix} ; Γ ⊢ S → S′ ≤ U → U′  \begin{matrix}⋮ . ; Γ ⊢ U ≤ T & ⋮ . ; Γ ⊢ T′ ≤ U′ \\ Γ ⊢ T → T′ ≤ U → U′ \end{matrix}

Then we can modify the proof:

\begin{matrix}\begin{matrix}⋮ . ; Γ ⊢ U ≤ T & ⋮ . ; Γ ⊢ T ≤ S \\ Γ ⊢ U ≤ S \end{matrix} & \begin{matrix}⋮ . ; Γ ⊢ S′ ≤ T′ & ⋮ . ; Γ ⊢ T′ ≤ U′ \\ Γ ⊢ S′ ≤ U \end{matrix} \\ Γ ⊢ S → S′ ≤ U → U′ \end{matrix}

By induction hypothesis, Γ ⊢ U ≤ S and Γ ⊢ S′ ≤ U can be proved without (Trans).

(2) ( S , T , and U are ∀ -types.)

In this case

\begin{matrix}\begin{matrix}⋮ . ; Γ ⊢ T ≤ S & ⋮ . ; Γ, X ≤ T ⊢ S′ ≤ T′ \\ Γ ⊢ ∀X≤S.S′ ≤ ∀X≤.T′ \end{matrix} & \begin{matrix}⋮ . ; Γ ⊢ U ≤ T & ⋮ . ; Γ, X ≤ U ⊢ T′ ≤ U′ \\ Γ ⊢ ∀X≤T.T′ ≤ ∀X≤U.U′ \end{matrix} \\ Γ ⊢ ∀X≤S.S′ ≤ ∀X≤U.U′ \end{matrix}

Then we can modify the proof:

\begin{matrix}\begin{matrix}⋮ . ; Γ ⊢ U ≤ T & ⋮ . ; Γ ⊢ T ≤ S \\ Γ ⊢ U ≤ S \end{matrix} & \begin{matrix}⋮ . ; Γ, X ≤ U ⊢ S′ ≤ T′ & ⋮ . ; Γ, X ≤ U ⊢ T′ ≤ U′ \\ Γ, X ≤ U ⊢ S′ ≤ U \end{matrix} \\ Γ ⊢ ∀X≤S.S′ ≤ ∀X≤U.U′ \end{matrix}

Since Γ, X ≤ T ⊢ S′ ≤ T′ and Γ ⊢ U ≤ T hold, Γ, X ≤ U ⊢ S′ ≤ T′ can be easily proved because

⋮ . ; Γ ⊢ U ≤ S ; Γ ⊢ X ≤ S (Taut) .

By induction hypothesis, Γ ⊢ U ≤ S and Γ, X ≤ U ⊢ S′ ≤ U can be proved without (Trans).

(3) ( S , T , and U are non-working.) In this case

Γ ⊢ T ≤ T
⋮ . Applying several (Taut)
Γ ⊢ S ≤ T

Γ ⊢ U ≤ U
⋮ . Applying several (Taut)
Γ ⊢ T ≤ U
Γ ⊢ S ≤ U

Then we can modify the proof:

Γ ⊢ U ≤ U
⋮ . Applying several (Taut)
Γ ⊢ T ≤ U
⋮ . Applying several (Taut)
Γ ⊢ S ≤ U

(4) ( S and T are non-working and U is working.) In this case

Γ ⊢ T ≤ T
⋮ . Applying several (Taut)
Γ ⊢ S ≤ T

⋮ .

Γ ⊢ W ≤ U ( W is a working type.)

⋮ . Applying several (Taut)
Γ ⊢ T ≤ U
Γ ⊢ S ≤ U

Then we can modify the proof:

⋮ . ; Γ ⊢ W ≤ U

⋮ . Applying several (Taut)

Γ ⊢ T ≤ U

⋮ . Applying several (Taut)

Γ ⊢ S ≤ U

(5) ( S is non-working and T and U are working.) In this case

⋮ .

Γ ⊢ W ≤ T ( W is a working type.)

⋮ . Applying several (Taut)
Γ ⊢ S ≤ T

⋮ . ; Γ ⊢ T ≤ U

Γ ⊢ S ≤ U

Then we can modify the proof.

\begin{matrix}⋮ . ; Γ ⊢ W ≤ T & ⋮ . ; Γ ⊢ T ≤ U \\ Γ ⊢ W ≤ U \end{matrix} ⋮ . Applying several (Taut) Γ ⊢ S ≤ U .

Since W is also working. Γ ⊢ W ≤ U can be proved without (Trans).

Notation 3.2.16.

Assume Δ ≡ X_{1} ≤ T_{1}, …, X_{n} ≤ T_{n} , X ∉ {X_{1}, …, X_{n}} and for every Y ∈ FV(U) , Y ∉ {X_{1}, …, X_{n}} hold.

We notate as follows:

Δ[X := U] ≡ X_{1} ≤ T_{1}[X := U], …, X_{n} ≤ T_{n}[X := U]

For all i ∈ 1, … n, T_{i}[X := U] ≡⟩ T′_{i} holds, we write Δ[X := U] ≡⟩ Δ′ , where

Δ′ ≡ X_{1} ≤ T′_{1}, …, X_{n} ≤ T′_{n}

Proposition 3.2.17. (Substitution Lemma about Types)

1. Assume Γ ⊢ U type , and Δ[X := U] ≡⟩ Δ′ hold,

(1) If Γ, X, Δ ⊢ T type and T [X := U] ≡⟩ T′ hold, then Γ, Δ′ ⊢ T′ type .

(2) If Γ, X, Δ ⊢ T ≤ V type , T [X := U] ≡⟩ T′ and V [X := U] ≡⟩ V′ hold, then Γ, Δ′ ⊢ T′ ≤ V′ .

2. Assume Γ ⊢ U ≤ S holds,

(1) If Γ, X ≤ S, Δ ⊢ T type and Δ[X := U] ≡⟩ Δ′ hold, then Γ, Δ′ ⊢ T′ type .

(2) If Γ, X ≤ S, Δ ⊢ T ≤ V type , T [X := U] ≡⟩ T′ and V [X := U] ≡⟩ V′ hold, then Γ, Δ′ ⊢ T′ ≤ V′ .

( Proof ): We prove only the second case by induction on Deg(T)_{{Γ,X≤S,Δ}}

1. Case ( T = X .)

Obvious.

Case ( T = Y (Y ≠ X) .) Obvious.

Case ( T = V → W .) By induction hypothesis , we can assume that V [X := U] ≡⟩ V′ , W [X := U] ≡⟩ W′ , Γ, Δ′ ⊢ V′ type and Γ, Δ′ ⊢ W′ type . Since (V → W)[X := U] ≡⟩ V′ → W′ . From assumptions,

⋮ . ; Γ, Δ′ ⊢ V′ type  ⋮ . ; Γ, Δ′ ⊢ W′ type
Γ, Δ′ ⊢ V′ → W′ type

Case ( T = ∀Y ≤V.W .) By induction hypothesis , we can assume that V [X := U] ≡⟩ V′ , W [X := U] ≡⟩ W′ , Γ, Δ ⊢′ V′ type and Γ, Δ, Y ≤ V′ ⊢ W′ type . Since (∀Y ≤V.W)[X := U] ≡⟩ ∀Y ≤V′.W′ . From assumptions,

⋮ . ; Γ, Δ′ ⊢ V′ type  ⋮ . ; Γ, Δ′, Y ≤ V′ ⊢ W′ type
Γ, Δ′ ⊢ ∀Y ≤V′.W′ type

Case ( T = Range(P) .) We consider two subcases:

(1) ( P [X := U] ≡⟩ M → N )

Since by induction hypothesis, Range(P)[X := U] ≡⟩ N and Γ ⊢ N type hold, we have Γ ⊢ N type .

⋮ . ; Γ, Δ′ ⊢ N type

(2) ( P [X := U] ≡⟩ Q)

Obvious by induction hypothesis, we have:

⋮ . ; Γ, Δ′ ⊢ Q type

Γ, Δ′ ⊢ Range(Q) type

2. By Subtype Relation Rules:

Case ( Γ, X ≤ S, Δ ⊢ X ≤ X .) Since Γ ⊢ U ≤ U holds, then Γ, Δ′ ⊢ U ≤ U also holds.

Case ( Γ, X ≤ S, Δ ⊢ Y ≤ Y .) Obvious.

Case ( Γ, X ≤ S, Δ ⊢ X ≤ T .) Since S = S[X := U] holds,

⋮ . ; Γ, Δ′ ⊢ S ≤ T′ ; Γ, Δ′ ⊢ U ≤ T′

Case ( Γ, X ≤ S, Δ ⊢ Range(P) ≤ T .)

(1) ( P [X := U] ≡⟩ M → N )

We have Γ(P)[X := U] ≡⟩ M′ → N′ . Then, by induction hypothesis, we have:

\begin{matrix}Γ ⊢ M′ ≤ M & Γ ⊢ N ≤ N′ \\ Γ ⊢ M → N ≤ M′ → N′ \end{matrix}

Since Range(P)[X := U] ≡⟩ N and Γ(Range(P))[X := U] ≡⟩ N′ , we have Γ ⊢ N ≤ N′ and Γ ⊢ N′ ≤ T . Then we have:

⋮ . ; Γ, Δ′ ⊢ N ≤ T′

(2) ( P [X := U] ≡⟩ Q) Obvious from induction hypothesis, we have:

⋮ . ; Γ, Δ′ ⊢ R ≤ T′ Range((Γ, Δ′)(Q)) ≡⟩ R
Γ, Δ′ ⊢ Range(Q) ≤ T′

Case ( Γ, X ≤ S, Δ ⊢ V → T ≤ V_{0} → T_{0} .)

\begin{matrix}⋮ . ; Γ, Δ′ ⊢ V′_{0} ≤ V′ & ⋮ . ; Γ, Δ′ ⊢ T′ ≤ T′_{0} \\ Γ, Δ′ ⊢ V′ → T′ ≤ V′_{0} → T′_{0} \end{matrix}

Case ( Γ, X ≤ S, Δ ⊢ ∀Y ≤V.T ≤ ∀Y ≤V_{0}.T_{0} .)

\begin{matrix}⋮ . ; Γ, Δ′ ⊢ V′_{0} ≤ V′ & ⋮ . ; Γ, Δ′, Y ≤ V′_{0} ⊢ T′ ≤ T′_{0} \\ Γ, Δ′ ⊢ ∀Y ≤V′.T′ ≤ ∀Y ≤V′_{0}.T′_{0} \end{matrix}

Case ( Γ, X ≤ S, Δ ⊢ Range(P) ≤ Range(Q) .)

(1) ( P [X := U] ≡⟩ M → N , Q[X := U] ≡⟩ M′ → N′ ) Since, by induction hypothesis, Γ, Δ′ ⊢ M → N ≤ M′ → N′ holds, we have Γ ⊢ N ≤ N′

(2) ( P [X := U] ≡⟩ P′, Q[X := U] ≡⟩ M′ → N′ )

From induction hypothesis,

⋮ . ; Γ, Δ′ ⊢ P′ ≤ M′ → N′

Γ, Δ′ ⊢ Range(P′) ≤ N′

(3) ( P [X := U] ≡⟩ P′, Q[X := U] ≡⟩ Q′

⋮ . ; Γ, Δ′ ⊢ P′ ≤ Q′

Γ, Δ′ ⊢ Range(P′) ≤ Range(Q′)

3.3 Term

In this section, we describe the terms of cF_{≤}^{+} . We start by the definition of raw terms, among which we distinguish the terms, i.e. those raw terms possessing types. Raw terms are divided into several classes: variables, constants, function terms (functions), ∀ -function terms, record terms, record selection terms, and coerced terms. Coercion is introduced to hold the properties of unicity of type and subject reduction.

Definition 3.3.1. (Raw Term)

e := x^{T}  (term) variable
| c^{T}  constant
| λx^{T} .w  λ-abs
| ee  λ-apl
| ΛX.e  Λ-abs
| ΛX≤T.e  bound Λ-abs
| e{T }  Λ-apl
| {l_{1} = e, ⋯, l_{n} = e} record-const (l_{i} ∈ L)
| e · l  record-select (l ∈ L)
| e|_{T}  coerced term

Types which stick to variables or constants are sometimes omitted.

We need to define the reduction of types ( ≡⟩ ) which stick to terms because these sorts of types must be in normal form.

Definition 3.3.2.

x^{T}  ≡⟩ x^{T′}  where T ≡⟩T′
λx^{T} .e  ≡⟩ λx^{T′}.e′  where T ≡⟩T′ and e≡⟩e′
ef  ≡⟩ e′f′  where e≡⟩e′ and f≡⟩f′
ΛX.e  ≡⟩ ΛX.e′  where e≡⟩e′
ΛX≤S.e  ≡⟩ ΛX≤S′.e′  where S≡⟩S′ and e≡⟩e′
e{T }  ≡⟩ e′{T′}  where T ≡⟩T′ and e≡⟩e′
e|_{T}  ≡⟩ e′|_{T′}  where T ≡⟩T′ and e≡⟩e′
{l_{i}=e_{i}}_{i=1,...,n} ≡⟩ {l_{i}=e′_{i}}_{i=1,...,n} where e_{i}≡⟩e′_{i} (i = 1, …, n)

3.3.1 Term

Definition 3.3.3. (Type assignment ( Γ ⊢ e : S ))

Type assignment ( Γ ⊢ e : S )

Terms are selected by the rules below; since term variables are indexed by their type, the rules do not needed assumptions of the term (x : T) :

{Γ ⊢ T type \atop Γ ⊢ x^{T} : T} (var)

{Γ ⊢ e : T \atop Γ ⊢ (λx^{S}.e) : S → T} (λ-ab)

\begin{aligned}Γ ⊢ e : S → T & Γ ⊢ f : U & Γ ⊢ U ≤ S \\ & Γ ⊢ ef : T \end{aligned} (λ-ap)
Γ ⊢ e : P Γ ⊢ f : U Γ^{∗}(P) = S → T Γ ⊢ U ≤ S
Γ ⊢ ef : Range(P)

(λ-Range)
Γ, X ⊢ f : T no free variable whose type is X does not occur in f

Γ ⊢ (ΛX.f) : ∀X.T (Λ-ab)

Γ, X ≤ S ⊢ e : T no free variable whose type is X does not occur in f

Γ ⊢ (ΛX≤S.e) : ∀X≤S.T

(bound-Λ-ab)

\begin{aligned}Γ ⊢ e : ∀X.T & Γ ⊢ U type & T [X := U]≡⟩T′ \\ & Γ ⊢ e\{U\} : T′ \end{aligned} (Λ-ap-w)

\begin{aligned}Γ ⊢ e : ∀X≤S.T & Γ ⊢ U ≤ S & T [X := U]≡⟩T′ \\ & Γ ⊢ e\{U\} : T′ \end{aligned} (bound-Λ-ap-w)
For all i = 1, ⋯, n, Γ ⊢ e_{i} : T_{i}

Γ ⊢ {l_{1} = e_{1}, ⋯, l_{n} = e_{n}} : [l_{1} : T_{1}, ⋯, l_{n} : T_{n}] (record-const)

{Γ ⊢ e : [⋯, l:T, ⋯] \atop Γ ⊢ e · l : T} (record-select)
Γ ⊢ e : P Γ ⊢ Sel(P, l) type
Γ ⊢ e · l : Sel(P, l)

(record-Sel)

\begin{matrix}Γ ⊢ e : S & Γ ⊢ S ≤ T \\ Γ ⊢ e|_{T} : T \end{matrix} (coer)

λx^{S}.e is a function abstraction and ef is a function application. When e has a function type S → T , ef has the type T of e ’s “output”. When e has a non-well-working type P , ef also has a non-well-working type including P .

ΛX≤S.e is a ∀ -function abstraction and e{S} is a ∀ -function application. When e has a universal type ∀X(≤ U).T , e{S} has the type T [X := S] of e ’s “output”. Note that, in ΛX≤S.e, no free variable of type X occurs in e.

{l_{1}=e_{1}, ⋯, l_{n}=e_{n}} is a record term and e · l is a record field selection term. When e has a record type [l_{1}:T_{1}, ⋯, l_{i}:T_{i}, ⋯, l_{n}:T_{n}] , e · l_{i} has the type T_{i} of the content of the field l_{i} . When e is a non-well-working type P , e · l also has a non-well-working type Sel(P, l) .

e|_{T} is a coerced term, where though e has the type S which is T ’s subtype, e|_{T} has the type T .

Because this system does not contain the subsumption rule, the following good properties are satisfied.

Theorem 3.3.4.

If Γ ⊢ e : S then Γ ⊢ S type

Proposition 3.3.5. (Unicity of Types)

For each expression e, if Γ ⊢ e : S and Γ ⊢ e : T hold, then both of S and T are in normal form and S = T holds.

3.3.2 Reduction system

From these definitions, the following properties are satisfied.

Proposition 3.3.6. (Substitution Lemma)

1. If Γ ⊢ e : S holds, e includes x^{T} , and Γ ⊢ f : T holds, then Γ ⊢ e[x^{T} := f] : S holds.

2. If Γ, X ≤ S, Δ ⊢ e : T (respectively Γ, X, Δ ⊢ e : T ), Γ ⊢ U ≤ S ( Γ ⊢ U type ), Δ[X := U] ≡⟩ Δ′ , e[X := U] ≡⟩ e′ and T [X := U] ≡⟩ T′ hold, then Γ, Δ′ ⊢ e′ : T′ holds.

( Proof ):

1. We can prove it by replacing

⋮ . ; Γ ⊢ T type ; Γ ⊢ x^{T} : T

with

⋮ . ; Γ ⊢ f : T

2. Induction on the structure of the proof of Γ ⊢ e : S . We prove in some cases:

(1) ( Γ, X ≤ S, Δ ⊢ x^{X} : X )

⋮ . ; Γ, Δ′ ⊢ U type ; Γ ⊢ x^{U} : U

(2) ( Γ, X ≤ S, Δ ⊢ ΛY ≤V.e : ∀Y ≤V.T )

⋮ . ; Γ, Δ′Y ≤ V′ ⊢ e′ : T′ ; Γ, Δ′ ⊢ ΛY ≤e′ : ∀Y ≤V′.T′

(3) ( Γ, X ≤ S, Δ ⊢ ef : Range(P) )

We only consider the case that Γ, X ≤ S, Δ ⊢ e : P and Γ, X ≤ S, Δ ⊢ f : M hold.

(i) ( P [X := U] ≡⟩ V → W )

⋮ . ; Γ, Δ′ ⊢ e′ : V → W  ⋮ . ; Γ, Δ′ ⊢ f′ : M′  ⋮ . ; Γ, Δ′ ⊢ M′ ≤ V
Γ, Δ′ ⊢ e′f′ : W

(ii) ( P [X := U] ≡⟩ P )

⋮ . ; Γ, Δ′ ⊢ e′ : P′  ⋮ . ; Γ, Δ′ ⊢ f′ : M′
Γ, Δ′ ⊢ e′f′ : Range(P′)
(4) ( Γ, X ≤ S, Δ ⊢ e{T } : V′ )

\begin{aligned}⋮ . ; Γ, Δ′ ⊢ ΛY ≤T′_{0}.e : ∀Y ≤T′_{0}.V′ & ⋮ . ; Γ, Δ′ ⊢ T′ ≤ T′_{0} & e[X := U] ≡⟩ e′ & V′[Y := T′] ≡⟩ V′′ \\ & Γ, Δ′ ⊢ (e′\{T′\}) : V′′ \end{aligned}

Definition 3.3.7. (Reduction)

The reduction rules in cF_{≤}^{+} are listed as follows:

Γ ⊢ (λx^{S}.e)f → e[x := f|_{S}] (β)

{e[X := S]≡⟩e′ \atop Γ ⊢ (ΛX.e)\{S\} → e′} (β2)

{e[X := T]≡⟩e′ \atop Γ ⊢ (ΛX≤S.e)\{T \} → e′} (bound β2)
Γ ⊢ {l_{1} = e_{1}, ⋯, l_{i} = e_{i}, ⋯, l_{n} = e_{n}} · l_{i} → e_{i} (Sel)

\begin{matrix}Γ ⊢ f : T & Range(S)≡⟩V \\ Γ ⊢ (e|_{S})f → (ef)|_{V} \end{matrix} (coer)

\begin{matrix}Γ ⊢ e : ∀X≤V.W & T [X := U]≡⟩T′ \\ Γ ⊢ (e|_{∀X≤S.T})\{U\} → (e\{U\})|_{T′} \end{matrix} (coer2)

{Sel(S, l)≡⟩V \atop Γ ⊢ (e|_{S}) · l → (e · l)|_{V}} (coerSel)
Γ ⊢ e is in normal form S is a base type.
Γ ⊢ e|_{S} → e

(coerconst)

( β ) is the rule of function application. From this rule, the coercion operator occurs after reduction

((bounded-) β 2) is the β -reduction rule for ∀ terms but the slightly complicated substitution about types occurs after reduction.

(coer) means that when the function term e is coerced, after we apply e to the argument f , ef is coerced to a proper type.

(coer2) means that when the ∀ -function term e is coerced, after we apply e to the argument T , e{U} is coerced to a proper type.

(coerconst) meant that, for each term e, when e is coerced to a (constant) base type S , the information that e has is not lost at all.

cF_{≤}^{+} satisfies some good properties as follows:

Theorem 3.3.8. (Subject Reduction)

For each expression e, if Γ ⊢ e : T and Γ ⊢ e → e′ hold, then Γ ⊢ e′ : T holds.

( Proof ): From the reduction rules:

Case ( ( β ).)

From substitution lemma (Proposition 3.3.6).

Case ( ( β2 , bound- β2 ).)

From substitution lemma (Proposition 3.3.6).

Case ( ( Sel ).)

\begin{matrix}⋯ & {⋮ . Π_{i} \atop Γ ⊢ e_{i} : T_{i}} & ⋯ \\ Γ ⊢ \{l_{1} = e_{1}, ⋯, l_{i} = e_{i}, ⋯, l_{n} = e_{n}\} : [l_{1}:T_{1}, ⋯, l_{i}:T_{i}, ⋯, l_{n}:T_{n}] \end{matrix} ; Γ ⊢ \{l_{1} = e_{1}, ⋯, l_{i} = e_{i}, ⋯, l_{n} = e_{n}\} · l_{i} : T_{i}

⇓

{⋮ . Π_{i} \atop Γ ⊢ e_{i} : T_{i}}

Case ( (coer).)

1. ( S = S_{1} → S_{2} , Γ ⊢ e : U_{1} → U_{2} ) Range(S_{1} → S_{2}) ≡⟩ S_{2} holds, then

{⋮ . Π_{1} \atop Γ ⊢ e : U_{1} → U_{2}} \begin{matrix}{⋮ . Σ_{1} \atop Γ ⊢ S_{1} ≤ U_{1}} & {⋮ . Σ_{2} \atop Γ ⊢ U_{2} ≤ S_{2}} \\ Γ ⊢ U_{1} → U_{2} ≤ S_{1} → S_{2} \end{matrix}
Γ ⊢ e|_{S_{1}→S_{2}} : S_{1} → S_{2}

{⋮ . Π_{2} \atop Γ ⊢ f : T} {⋮ . Σ_{3} \atop Γ ⊢ T ≤ S_{1}}

Γ ⊢ (e|_{S_{1}→S_{2}})f : S_{2}
⇓

{⋮ . Π_{1} \atop Γ ⊢ e : U_{1} → U_{2}} {⋮ . Π_{2} \atop Γ ⊢ f : T} \begin{matrix}{⋮ . Σ_{3} \atop Γ ⊢ T ≤ S_{1}} & {⋮ . Σ_{1} \atop Γ ⊢ S_{1} ≤ U_{1}} \\ Γ ⊢ T ≤ U_{1} \end{matrix}
Γ ⊢ ef : U_{2}

{⋮ . Σ_{2} \atop Γ ⊢ U_{2} ≤ S_{2}}

Γ ⊢ (ef)|_{S_{2}} : S_{2}

2. ( S = S_{1} → S_{2} , Γ ⊢ e : P )

Range(S_{1} → S_{2}) ≡⟩ S_{2} holds, then

\begin{matrix}{⋮ . Π_{1} \atop Γ ⊢ e : P} & {⋮ . Σ_{1} \atop Γ ⊢ P ≤ S_{1} → S_{2}} \\ Γ ⊢ e|_{S_{1}→S_{2}} : S_{1} → S_{2} \end{matrix} {⋮ . Π_{2} \atop Γ ⊢ f : T} {⋮ . Σ_{2} \atop Γ ⊢ T ≤ S_{1}}
Γ ⊢ (e|_{S_{1}→S_{2}})f : S_{2}
⇓

{⋮ . Π_{1} \atop Γ ⊢ e : P} {⋮ . Π_{2} \atop Γ ⊢ f : T} {⋮ . Σ_{1} \atop Γ ⊢ P ≤ S_{1} → S_{2}} {⋮ . Σ_{2} \atop Γ ⊢ T ≤ S_{1}}
Γ ⊢ ef : Range(P)

{⋮ . Σ_{1} \atop Γ ⊢ P ≤ S_{1} → S_{2}}

Γ ⊢ Range(P) ≤ S_{2}

Γ ⊢ (ef)|_{S_{2}} : S_{2}

In this case we can replace Γ^{∗}(P) ≡ S_{1} → S_{2} with Γ ⊢ P ≤ S_{1} → S_{2} . In the following cases, for instance, we also replace Γ^{∗}(P) ≡ S → T with Γ ⊢ S → T .

3. ( S = Q, Γ ⊢ e : P )

\begin{matrix}{⋮ . Π_{1} \atop Γ ⊢ e : P} & {⋮ . Σ_{1} \atop ⊢ P ≤ Q} \\ Γ ⊢ e|_{Q} : Q \end{matrix}  {⋮ . Π_{2} \atop Γ ⊢ f : T}  {⋮ . Σ_{2} \atop Γ ⊢ Q ≤ U → V}  {⋮ . Σ_{3} \atop Γ ⊢ U ≤ T}
Γ ⊢ (e|_{Q})f : Range(Q)

⇓

I

{⋮ . Σ_{1} \atop Q ≤ P}

Γ ⊢ Range(Q) ≤ Range(P) Γ ⊢ (ef)|_{Range(Q)} : Range(Q)

where I is

{⋮ . Π_{1} \atop Γ ⊢ e : P}

{⋮ . Π_{2} \atop Γ ⊢ f : T}

⋮ . (From Proposition 3.2.15)
Γ ⊢ P ≤ U → V

{⋮ . Σ_{3} \atop Γ ⊢ U ≤ T}

Γ ⊢ ef : Range(P)

Case ( (coer2).)

{⋮ . Π_{1} \atop Γ ⊢ e : ∀X≤V.W}  \begin{matrix}{⋮ . Σ_{1} \atop Γ ⊢ S ≤ V} & {⋮ . Σ_{2} \atop Γ, X ≤ S ⊢ W ≤ T} \\ Γ ⊢ ∀X≤V.W ≤ ∀X≤S.T \end{matrix}
Γ ⊢ e|_{∀X≤S.T} : ∀X≤S.T

{⋮ . Σ_{3} \atop Γ ⊢ U ≤ S}

T [X := U] ≡⟩ T′
Γ ⊢ (e|_{∀X≤S.T}){U} : T′

⇓

3.3. TERM 27 I

{⋮ . Σ_{2} \atop Γ, X ≤ S ⊢ W ≤ T}  {⋮ . Σ_{3} \atop Γ ⊢ U ≤ S}
⋮ . (From Subst. Lemma)
Γ ⊢ W′ ≤ T′
Γ ⊢ (e{U})|_{T′} : T′

where I is:

{⋮ . Π_{1} \atop Γ ⊢ e : ∀X≤V.W} \begin{matrix}{⋮ . Σ_{3} \atop Γ ⊢ U ≤ S} & {⋮ . Σ_{1} \atop Γ ⊢ S ≤ V} \\ Γ ⊢ U ≤ V \end{matrix} W [X := U] ≡⟩ W′
Γ ⊢ e{U} : W′

Case ( (coer Sel ).)

1. S = [⋯, l:T, ⋯] , Γ ⊢ e : [⋯, l:U, ⋯]

\begin{matrix}{⋮ . Π_{1} \atop Γ ⊢ e : [⋯, l:U, ⋯]} & \begin{matrix}⋯ & {⋮ . Σ_{1} \atop Γ ⊢ U ≤ T} & ⋯ \\ Γ ⊢ [⋯, l:U, ⋯] ≤ [⋯, l:T, ⋯] \end{matrix} \\ Γ ⊢ (e|_{[···,l:T,···]}) : [⋯, l:T, ⋯] \end{matrix} ; Γ ⊢ (e|_{[···,l:T,···]}) · l : T

⇓

\begin{matrix}{⋮ . Π_{1} \atop Γ ⊢ e : [⋯, l:U, ⋯]} ; Γ ⊢ e · l : U & {⋮ . Σ_{1} \atop Γ ⊢ U ≤ T} \\ Γ ⊢ (e · l)|_{T} \end{matrix}

2. ( S = [⋯, l:T, ⋯] , Γ ⊢ e : P )

{⋮ . Π_{1} \atop Γ ⊢ e : P}

\begin{matrix}⋯ & {⋮ . Σ_{1} \atop Γ ⊢ S ≤ T} & ⋯ \\ Γ ⊢ [⋯, l:S, ⋯] ≤ [⋯, l:T, ⋯] \end{matrix}

⋮ . Applying (Taut)
Γ ⊢ P ≤ [⋯, l:T, ⋯]

Γ ⊢ (e|_{[···,l:T,···]}) : [⋯, l:T, ⋯] Γ ⊢ (e|_{[···,l:T,···]}) · l : T

⇓

{⋮ . Π_{1} \atop Γ ⊢ e : P} Sel([⋯, l:S, ⋯])≡⟩S {⋮ . Σ_{1} \atop Γ ⊢ S ≤ T} ; ⋮ .

Γ ⊢ Sel(P, l) ≤ T
Γ ⊢ e · l : Sel(P, l)
Γ ⊢ (e · l)|_{T}

3. ( S = Q, Γ ⊢ e : P )

\begin{matrix}{⋮ . Π_{1} \atop Γ ⊢ e : P} & {⋮ . Σ_{1} \atop Γ ⊢ P ≤ Q} \\ Γ ⊢ (e|_{Q}) : Q \end{matrix}  {⋮ . Σ_{2} \atop Γ ⊢ Q ≤ [ ⋯, l:T, ⋯]}
Γ ⊢ (e|_{Q}) · l : Sel(Q, l)

⇓

I

{⋮ . Σ_{1} \atop Γ ⊢ P ≤ Q} {⋮ . Σ_{2} \atop Γ ⊢ Q ≤ [⋯, l:T, ⋯]}

Γ ⊢ Sel(Q, l) type

Γ ⊢ Sel(P, l) ≤ Sel(Q, l)

Γ ⊢ (e · l)|_{Sel(P,l)} : Sel(P, l)

where I is

{⋮ . Π_{1} \atop Γ ⊢ e : P} \begin{matrix}{⋮ . Σ_{1} \atop Γ ⊢ P ≤ Q} & {⋮ . Σ_{2} \atop Γ ⊢ Q ≤ [ ⋯, l:T, ⋯]} \\ Γ ⊢ P ≤ [⋯, l:T, ⋯] \end{matrix}

Γ ⊢ Sel(P, l) type

Γ ⊢ e · l : Sel(P, l)

Theorem 3.3.9. (Chrch-Rosser)

For each well-typed expression e, if Γ ⊢ e →^{∗} e′ and Γ ⊢ e →^{∗} e′′ , there exists an expression f where Γ ⊢ e′ →^{∗} f and Γ ⊢ e′′ →^{∗} f are satisfied.

( Proof ): Easily proved from those substitution lemmas using parallel reduction[Tak92].

Γ ⊢ x^{T} > x^{T} (PFVar)
Γ ⊢ c^{T} > c^{T} (PFConst)
{Γ ⊢ e > e′ \atop Γ ⊢ λx^{T} .e > λx^{T} .e′} (PFλab)
\begin{matrix}Γ ⊢ e > e′ & Γ ⊢ f > f′ \\ Γ ⊢ ef > e′f′ \end{matrix} (PFλap)
{Γ, X ≤ T ⊢ e > e′ \atop Γ ⊢ ΛX≤T.e > ΛX≤T.e′} (PFΛab)
{Γ ⊢ e > e′ \atop Γ ⊢ e\{T \} > e′\{T \}} (PFΛap)
\begin{matrix}Γ ⊢ e_{1} > e′_{1} & ⋯ & Γ ⊢ e_{n} > e′_{n} \\ Γ ⊢ \{l_{1}=e_{1}, ⋯, l_{n}=e_{n}\} > \{l_{1}=e′_{1}, ⋯, l_{n}=e′_{n}\} \end{matrix} (PFRecordConst)
{Γ ⊢ e > e′ \atop Γ ⊢ e · l > e′ · l} (PFRecordSel)
{Γ ⊢ e > e′ \atop Γ ⊢ e|_{T} > e′|_{T}} (PFCoerce)

\begin{matrix}Γ ⊢ e > e′ & Γ ⊢ f > f \\ Γ ⊢ (λx^{S}.e)f > e′[x = f′|_{S}] \end{matrix} (PRβ)
\begin{matrix}Γ, X ⊢ e > e′ & e′[X := S]≡⟩e′′ \\ Γ ⊢ (ΛX.e)\{S\} > e′′ \end{matrix} (PRβ2)
\begin{matrix}Γ, X ≤ S ⊢ e > e′ & e′[X := T]≡⟩e′′ \\ Γ ⊢ (ΛX≤S.e)\{T \} > e′′ \end{matrix} (PRboundβ2)
{Γ ⊢ \{l_{1}=e_{1}, ⋯, l_{i}=e_{i}, ⋯, l_{n}=e_{n}\} > \{l_{1}=e′_{1}, ⋯, l_{i}=e′_{i}, ⋯, l_{n}=e′_{n}\} \atop Γ ⊢ \{l_{1}=e_{1}, ⋯, l_{i}=e_{i}, ⋯, l_{n}=e_{n}\} · l_{i} > e′_{i}} (PRSel)
Γ ⊢ f : T Range(S)≡⟩V Γ ⊢ e > e′ Γ ⊢ f > f′

Γ ⊢ (e|_{S})f > (e′f′)|_{V} (PRcoer)

\begin{matrix}Γ ⊢ e : ∀X≤V.W & Γ ⊢ e > e′ & T [X := U]≡⟩T′ \\ Γ ⊢ (e|_{∀X≤S.T})\{U\} > (e′\{U\})|_{T′} \end{matrix} (PRcoer2)
\begin{matrix}Sel(S, l)≡⟩V & Γ ⊢ e > e′ \\ Γ ⊢ (e|_{S}) · l > (e′ · l)|_{V} \end{matrix} (PRcoerSel)
Γ ⊢ e is in normal form S is a base type.

Γ ⊢ e|_{S} > e

(PRcoerconst)

Lemma 3.3.10.

1. Γ ⊢ e > e

2. If Γ ⊢ e → e′ , then Γ ⊢ e > e′ .

3. If Γ ⊢ e > e′ , then Γ ⊢ e →^{∗} e′ .

4. If Γ ⊢ e > e′ , Γ ⊢ f > f′ , and Γ ⊢ f : S then Γ ⊢ e[x^{S} := f] > e′[x^{S} := f′] .

5. If Γ, X ≤ S ⊢ e >e′ , Γ ⊢ T ≤ S , e[X := T] ≡⟩ f and e′[X := T] ≡⟩ f′ hold,then Γ ⊢ f >f′ .

( Proof ):

• (1,2,3) Obvious.

• (4,5) From substitution lemmas.

Lemma 3.3.11.

Under an environment Γ , for a term g, we define g^{∗} to be the term constructed by applying the rules of the name (P-R*) when possible, and the rules of the name (P-F*) when no (P-R*) can be applied. g^{∗} is uniquely determined and if Γ ⊢ g > g′ , then Γ ⊢ g′ > g^{∗} .

( Proof ): g^{∗} is uniquely determined because none of the (P-R*) rules overlap. The reset of the theorem is proved using structural induction on the form of the term g.

Case ( x.)

Obvious

Case ( λx^{S}.e.)

Then g has the form λx^{S}.e. Then g′ has the form λx^{S}.e′ for some e′ to which Γ ⊢ e > e′ . By induction hypothesis, Γ ⊢ e′ > e^{∗} . Therefore Γ ⊢ λx^{S}.e′ > λx^{S}.e^{∗} = (λx^{S}.e)^{∗}

Case ( ΛX≤S.e.)

Then g has the form ΛX≤S.e. Then g′ has the form ΛX≤S.e′ for some e′ to which Γ, X ≤ S ⊢ e > e′ . By induction hypothesis, Γ, X ≤ S ⊢ e′ > e^{∗} . Therefore Γ ⊢ ΛX≤S.e′ > ΛX≤S.e^{∗} = (ΛX≤S.e)^{∗}

Case ( e_{0}f .)

g has the form e_{0}f . Then there are two subcases.

1. g has the form (λx^{S}.e)f . Then g^{∗} is e^{∗}[x^{S} := f^{∗}|_{S}] .

• g′ has the form (λx^{S}.e′)f′ . Then from induction, Γ ⊢ e′ >e^{∗} and Γ ⊢ f′ >f^{∗} . Thus from definition, (λx^{S}.e′)f′ > e^{∗}[x^{S} := f^{∗}|_{S}] .

• g′ has the form e′[x^{S} := f′|_{S}] . Then from induction, Γ ⊢ e′ > e^{∗} and Γ ⊢ f′ > f^{∗} , which implies Γ ⊢ f′|_{S} > f^{∗}|_{S} Thus from definition and Proposition 3.3.6, e′[x^{S} := f′|_{S}] > e^{∗}[x^{S} := f^{∗}|_{S}] .

2. g has the form (e|_{P})f . Then g^{∗} is (e^{∗}f^{∗})|_{V} where Range(P) ≡⟩ V . The proof is similar to previous cases.

Case ( e_{0}{T }.)

g has the form e_{0}{T }. Then there are two subcases.

1. g has the form (ΛX≤S.e){T }. Then g^{∗} is f^{∗} where e ≡⟩ e^{∗} and e^{∗}[X := T] ≡⟩ f^{∗} .

• g′ has the form (ΛX≤S.e′){T }. Then from induction, Γ, X ≤ S ⊢ e′ > e^{∗} . Thus from definition, (ΛX^{S}.e′){T } > f^{∗} .

• g′ has the form f′ where e′[X := T] ≡⟩ f′ . Then from induction, Γ, X ≤ S ⊢ e′ > e^{∗} . Thus from definition and Proposition 3.3.6, f′ > f^{∗} .

2. g has the form (e|_{∀X≤S′.U′}){T } where Γ ⊢ e : ∀X≤S.U ≤ ∀X≤S′.U′ . Then g^{∗} is (e^{∗}[X := T])|_{U′[X:=T]} . The proof is similar.

Case ( e_{0}|_{S} .)

Similarly to (Case ( e_{0}f ))

Then we have that cF_{≤}^{+} satisfies the Church-Rosser property.

Theorem 3.3.12. (Strong Normalization)

All type-checked terms in cF_{≤}^{+} is strongly normalizing.

The proof of this theorem is too long and discussed in Section 3.4.

In cF_{≤}^{+} , under an environment Γ when f has type S , functions f and f|_{S} are expected to be the same function because the coercion function from S to S is identity. However, there is no reduction rule which reduces f|_{S} to f , or f to f|_{S} . Actually, we do not expect that cF_{≤}^{+} is extensional from the beginning bacause we did not even have the η -reduction.

Thouth f and f|_{S} are not equal, we expect that thery behave equally. For the same reason, we expect that coercion are transitive. That is f|_{G}|_{U} and f|_{U} behave equally. For this purpose, we define a notion of equivaence between terms, which is sometimes called applicable congruence [Blo90, Plo77, Mil77].

Definition 3.3.13. (Applicable Congruence)

Two closed terms e and f of the same type are applicably congruent (e =AP f) if for every sequent of applications and slot selections g_{1}, …, g_{n} ( g_{i} can be a term or a type) deriving e and f to base types, eg_{1} … g_{n} reduces to a normal form c iff fg_{1} … g_{n} reduces to c.

From this proposition and the Chrch-Rosser theorem, every closed expression of a base type is reduced to a unique constant, or do not have a normal form. This justifies the above definition of equality between terms.

Theorem 3.3.14.

1. When Γ ⊢ f : S holds and f is closed, then f and f|_{S} are applicably congruent.

2. When Γ ⊢ f : S , Γ ⊢ S ≤ T , and Γ ⊢ T ≤ U hold and f is closed, then f|_{T} |_{U} and f|_{U} are applicably congruent.

( Proof ): (1,2) Easily proved by induction on the degree of S .

3.4 Strong Normalization

We here show the proof of the strong normalizability of cF_{≤}^{+} (see Theorem 3.3.12).

3.4.1 Outline of the Proof

We discuss about the proof of the strong normalizability of cF_{≤}^{+} . First, we prove the strong normalization of all type-erasure of cF_{≤}^{+} terms, using the notion of saturated sets which are given in [Gal90, Tai75]. Saturated sets are like candidates of reducibility which are used in the proof of the termination of F terms, and they also give semantics of cF_{≤}^{+} . We will provide a modified method using in [Ghe90]. After the strong normalization of all type-erasure of cF_{≤}^{+} terms, we prove the strong normalization of cF_{≤}^{+} terms.

3.4.2 Untyped Translation

Definition 3.4.1.

We define a target of untyped λ -terms+record Λrec .

e ::= x  (x ∈ X, X is a set of all variables)
| c  (constant)
| λx.e  (λ-abstraction)
| ee′  (λ-application)
| {l_{1}=e_{1}, ⋯, l_{n}=e_{n}}  (record: which can be abbreviated)
{l_{i}=e_{i}}_{i=1,...,n})
(l_{i} ∈ L and for all i ≠ j, then l_{i} ≠ l_{j})
| e · l  (record-field selection)

We define reduction rules:

(β) (λx.e)f  ⇒ e[x := f]
(Sel) {l_{i}=e_{i}}_{i=1,...,n} · l_{k} ⇒ e_{k}
(where k = 1, …, n)

Notation 3.4.2.

In this section el where ( e is a term and l ( ∈ L) a label of record) means e · l because sometimes we do not want to distinguish between record selection and term application.

Definition 3.4.3.

We define a translation Erase(e) from cF_{≤}^{+} to untyped λ -term Λrec .

Erase(x^{T})  = x
Erase(c^{T})  = c
Erase(λx^{T} .e)  = λx.Erase(e)
Erase(ΛX ≤ T.e)  = Erase(e)
Erase(ef)  = Erase(e)Erase(f)
Erase(e{S})  = Erase(e)
Erase({l_{i}=e_{i}}_{i=1,...,n}) = {l_{i}=Erase(e_{i})}_{i=1,...,n}
Erase(e · l)  = Erase(e) · l
Erase(e|_{T})  = Erase(e)

3.4.3 Termination of Type-erasure of cF_{≤}^{+} Terms

We prove the strong normalization property of translated terms of Λrec from cF_{≤}^{+} terms. We call them type erasures.

Definition 3.4.4.

(Space Constructor)

[S → T] = {e ∈ Λrec | ∀f ∈ S ⇒ ef ∈ T }

Definition 3.4.5.

• (Application Constructor)

AP(P, U) = {e_{0}f|e_{0} ∈ P and f ∈ U}

• (Selection Constructor)

SEL(P, l) = {e_{0} · l|e_{0} ∈ P }

Notation 3.4.6.

For every term e of Λrec which is strongly normalizing, we denote the maximum of length of reduction chain of e as ν(e) . For every label l ∈ L, we consider that ν(l) = 0 .

Definition 3.4.7.

Let SN be a set of Λrec -terms which are strongly normalizing. A subset C ⊆ SN is saturated iff the following conditions hold:

(S0) If e ∈ C and e → f hold, then f ∈ C . (S1) For every variable x ∈ X , for all n ≥ 0 and all f_{1}, …, f_{n} ∈ SN ∪ L, xf_{1} … f_{n} ∈ C (S2) For all e, f ∈ SN , for all n ≥ 0 and all f_{1}, …, f_{n} ∈ SN ∪ L, if e[x := f]f_{1} … f_{n} ∈ C , then

(λx.e)ff_{1} … f_{n} ∈ C (S3) For all e ∈ SN , for all n, m ≥ 0 , all f_{1}, …, f_{n} ∈ SN∪L, all e_{1}, …, e_{m} ∈ SN , if ef_{1} … f_{n} ∈

C , then {l_{1}=e_{1}, …, l_{i}=e_{i}, l=e, l_{i+1}=e_{i=1}, ⋯ l_{m}=e_{m}} · lff_{1} … f_{n} ∈ C

SAT is the set of all saturated sets.

Lemma 3.4.8.

SN ∈ SAT

( Proof ):

(S0) Obvious. (S1) By induction on the sum of ν(f_{i}) . Consider any reduction chain starting with xf_{1} … f_{n} :

xf_{1} … f_{i} … f_{n} ⇒ xf_{1} … f′_{i} … f_{n} where f_{i} ⇒ f′_{i} and so it is strongly normalizing, but its depth is strictly smaller than ν(f_{i}) . Then we can apply induction to f_{1}, …, f′_{i}, …, f_{n} obtaining that xf_{1} … f′_{i} … f_{n} is strongly normalizing, and so is xf_{1} … f_{i} … f_{n} .

(S2) By induction on the sum of ν(e[x := f]f_{1} … f_{m}) and ν(f) . Suppose e[x := f]f_{1} … f_{m} ∈ SN and consider any reduction chain starting with (λx.e)ff_{1} … f_{m} ; we must prove that this chain is finite. We have the following possibilities for the first step of this chain:

1. (λx.e)ff_{1} … f_{m}  ⇒ e[x := f]f_{1} … f_{m}
2. (λx.e)ff_{1} … f_{m} ⇒ (λx.e′)ff_{1} … f_{m} e ⇒ e′
3. (λx.e)ff_{1} … f_{i} … f_{m} ⇒ (λx.e)ff_{1} … f′_{i} … f_{m} f_{i} ⇒ f′_{i} (i = 1, …, m)
4. (λx.e)ff_{1} … f_{m}  ⇒ (λx.e)f′f_{1} … f_{m}  f ⇒ f′

We show that in all the four cases the reduced term is in SN . In case 1 the reduced term belongs to SN by hypothesis. In case 2, observe e′[x := f]f_{1} … f_{m} is a reduct of e[x := f]f_{1} … f_{m} , and then belongs to SN . But ν(e′[x := f]f_{1} … f_{m}) is smaller than ν(e[x := f]f_{1} … f_{m}) ; then we can apply to it the induction hypothesis and obtain that (λx.e′)ff_{1} … f_{m} ∈ SN . The same reasoning holds for case 3. In case 4, e[x := f′]f_{1} … f_{m} is a reduct of e[x := f]f_{1} … f_{m} . The induction measure ν(e[x := f]f_{1} … f_{m}) + ν(f) is strictly decreased whether x is free in e or not, and the inductive hypothesis can be applied as in the preceding cases, obtaining (λx.e)f′f_{1} … f_{m} ∈ SN .

(S3) Similar to (S2).

Definition 3.4.9.

The interpretation of environments and types is defined by mutual induction.

[[ϕ]]  = SAT^{0}(a singleton set)
[[Γ, X]]  = {⟨R⃗, C⟩ | R⃗ ∈ [[Γ]], C ∈ SN}
[[Γ, X ≤ T]] = {⟨R⃗, C⟩ | R⃗ ∈ [[Γ]], C ∈ SAT, C ⊆ [[Γ ⊢ T]]R⃗}

The interpretation of types is defined by induction on their size; we will avoid environments Γ and quantifications ∀R⃗ ∈ [[Γ]] , when not necessary, to make the notation less cumbersome:

[[Γ ⊢ X_{i}]]R⃗  = R_{i}
[[Γ ⊢ B]]R⃗  = ⋂_{C∈SAT,C⊆D} C

where D = {Erase(e) | Γ ⊢ e : B and e is terminating.}

[[S → T]]R⃗  = [[[S]]R⃗ → [[T]]R⃗]
[[Γ ⊢ ∀Y ≤S.T]]R⃗  = ⋂_{C∈SAT C⊆[[Γ⊢S]]R⃗}[[Γ, Y ≤ S ⊢ T]](R⃗, Y := C)
[[ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] ]]R⃗ = {e |For every i = 1, …, n, e · l_{i} ∈ [[T_{i}]]R⃗}
[[Γ ⊢ Range(P)]]R⃗  = ⋂_{C∈SAT, C⊇AP([[P]]R⃗,[[S]]R⃗)} C

where Γ^{∗}(Range(P)) = S → T

[[Sel(P, l)]]R⃗  = ⋂_{C∈SAT, C⊇SEL([[P]]R⃗,l)} C

Type variables are interpreted by the type environment. A functional type is simply the type of all terms which is applied to a term of the domain give a term of the codomain. A bounded quantified type is interpreted by a bounded intersection. The substitution-like notation (R⃗, Y := C) means simply ⟨R⃗, C⟩, but should be more suggestive about the fact that we extend the environment R⃗ with an interpretation C for the type variable Y . The definition is well formed because (R⃗, Y := C) ∈ [[Γ, Y ≤ S]] follows immediately by the interpretation of type environments. A Range type is interpreted by a minimum saturated set which contains all terms which are given by applying a term of the contents of Range to its argument.

Firstly we must prove that for every type, its interpretation is saturated.

Lemma 3.4.10.

For any subset C ⊆ SAT , ⋂_{C∈C} C ∈ SAT holds.

( Proof ): Obvious from Definition 3.4.7.

Lemma 3.4.11.

For every type, its interpretation in Definition 3.4.9 is saturated.

( Proof ): Induction on the structures of the proof of the type good-formatiom. We prove only the four cases: function type, record type, ∀ -type, and Range -type.

Case ( T → U .)

(S0) Assume that e ∈ [[T → U]]R⃗ and e → e′ hold. For every f ∈ [[T]]R⃗, ef ∈ [[U]]R⃗ holds.

Since ef → e′f , we have e′f ∈ [[U]]R⃗. Then we have e′ ∈ [[T → U]]R⃗. (S1) For every variable x and for all m ≥ 0 and e ∈ SN and e_{1}, …, e_{m} ∈ SN ∪ L, we have

xe_{1} ⋯ e_{m}e ∈ [[U]]R⃗. Since this holds for every e ∈ [[S]]R⃗, we have xe_{1} ⋯ e_{m} ∈ [[T → U]]R⃗ (S2) For every f, e ∈ SN ,all m ≥ 0 and e_{1}, …, e_{m} ∈ SN ∪ L Assume that e[x := f]e_{1} … e_{m} ∈

[[T → U]]R⃗. This means that, for every g ∈ [[T]]R⃗, e[x := f]e_{1} … e_{m}g ∈ [[U]]R⃗ holds. Since [[U]]R⃗ is saturated, by (S2) (λx.e)fe_{1} … e_{m}g ∈ [[U]]R⃗, and this is true for every g, we have (λx.e)fe_{1} … e_{m} ∈ [[T → U]]R⃗.

(S3) For every e ∈ SN ,all m ≥ 0 , e_{1}, …, e_{m} ∈ SN ∪ L, n ≥ 0 , and e′_{1}, …, e′_{n} ∈ SN . Assume that ee_{1} … e_{m} ∈ [[T → U]]R⃗. This means for every g ∈ [[T]]R⃗, ee_{1} … e_{m}g ∈ [[U]]R⃗. Since [[U]]R⃗ is saturated, by (S3) ({l_{1}=e′_{1}, …, l_{i}=e′_{i}, l=e, l_{i+1}:e′_{i+1}, …, l_{n}=e′_{n}}·l)e_{1} … e_{m}g ∈ [[U]]R⃗, and this is true for every g ∈ [[T]]R⃗, we have ({⋯, l=e, ⋯}·l)e_{1} … e_{m} ∈ [[T → U]]R⃗.

Case ( [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] .)

(S0) Similar to the case of function type. (S1) For every variable x and for all m ≥ 0 , e_{1}, …, e_{m} ∈ SN ∪ L, and i = 1, …, n, we

have (xe_{1} ⋯ e_{m}) · l_{i} ∈ [[T_{i}]]R⃗. Then, from definition of [[ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] ]]R⃗, we have xe_{1} ⋯ e_{m} ∈ [[ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] ]]R⃗

(S2) For every f, e ∈ SN , all m ≥ 0 and e_{1}, …, e_{m} ∈ SN ∪ L, assume that e[x := f]e_{1} … e_{m} ∈ [[ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] ]]R⃗. This means that, for every i = 1, …, n, (e[x := f]e_{1} … e_{m}) · l_{i} ∈ [[T_{i}]]R⃗. Since [[T_{i}]]R⃗ is saturated, by (S2) ((λx.e)fe_{1} … e_{m}) · l_{i} ∈ [[T_{i}]]R⃗, and this is true for every i, we have (λx.e)fe_{1} … e_{m} ∈ [[ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] ]]R⃗.

(S3) For every e ∈ SN , all m ≥ 0 and e_{1}, …, e_{m} ∈ SN ∪ L, and all n′ ≥ 0 and e′_{1}, …, e′_{n′} ∈ SN ∪ L, assume that ee_{1} … e_{m} ∈ [[ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] ]]R⃗ holds. This means that, for every i = 1, …, n, (ee_{1} … e_{m}) · l_{i} ∈ [[T_{i}]]R⃗. Since [[T_{i}]]R⃗ is saturated, by (S2) (({l_{1}=e′_{1}, …, l_{j}=e′_{j}, l=e, l_{j+1}=e′_{j+1}, …, l_{n}=e′_{n′}} · l)e_{1} … e_{n}) · l_{i} ∈ [[T_{i}]]R⃗, and this is true for every i, we have ({l_{1}=e′_{1}, …, l_{j}=e′_{j}, l=e, l_{j+1}=e′_{j+1}, …, l_{n}=e′_{n′}} · l)e_{1} … e_{m} ∈ [[ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] ]]R⃗.

Case ( ∀Y ≤S.T .)

(S0) Assume e ∈ [[Γ ⊢ ∀X≤S.T]]R⃗ and e → e′ hold. Then for every C ⊆ [[Γ ⊢ S]]R⃗ such that C ∈ SAT holds, e ∈ [[Γ, Y ≤ S ⊢ T]](R⃗, Y := C) . By induction hypothesis, we have e′ ∈ [[Γ, Y ≤ S ⊢ T]](R⃗, Y := C) . Then e′ ∈ [[Γ, Y ≤ S ⊢ T]](R⃗, Y := C) holds.

(S1) Assume that [[Γ ⊢ S]]R⃗ ∈ SAT holds. For every variable x and for all m ≥ 0 and e_{1}, …, e_{m} ∈ SN ∪ L, and C ⊆ [[Γ ⊢ S]]R⃗ such that C ∈ SAT holds, we have xe_{1} ⋯ e_{m}e ∈ [[Γ, Y ≤ S ⊢ T]](R⃗, Y := C) . From the definition, xe_{1} ⋯ e_{m}e ∈ ⋂_{V}^{C⊆[[Γ⊢S]]R⃗,C∈SAT}[[Γ, Y ≤ S ⊢ T]](R⃗, Y := C) ≡ [[Γ ⊢ ∀X≤S.T]]R⃗.

(S2) For every f, e ∈ SN ,all m ≥ 0 and e_{1}, …, e_{m} ∈ SN ∪ L Assume that e[x := f]e_{1} … e_{n} ∈ [[Γ ⊢ ∀X≤S.T]]R⃗. This means for every C ⊆ [[Γ ⊢ S]]R⃗ such that C ∈ SAT holds, e[x := f]e_{1} … e_{n} ∈ [[Γ, Y ≤ S ⊢ T]](R⃗, Y := C) . Since [[Γ, Y ≤ S ⊢ T]](R⃗, Y := C) is saturated, by (S2) (λx.e)fe_{1} … e_{n} ∈ [[Γ, Y ≤ S ⊢ T]](R⃗, Y := C) , and this is true for every C , we have (λx.e)fe_{1} … e_{n} ∈ [[Γ ⊢ ∀X≤S.T)]] .

(S3) Similar to (S2)

Case ( Range(P) .)

Assume that Γ^{∗}(P) = S → T . Since Γ ⊢ P ≤ S → T , we have [[P]]R⃗ ⊆ [[S → T]]R⃗. Then AP([[P]]R⃗, [[S]]R⃗) ⊆ [[T]]R⃗ And (S0) � (S3) are trivial from Lemma 3.4.10.

Secondly, we show the soundness of the interpretation via subtype relation.

Lemma 3.4.12.

For every proof of subtype relation Γ ⊢ S ≤ T , [[Γ ⊢ S]]R⃗ ⊆ [[Γ ⊢ T]]R⃗ holds.

( Proof ): Induction on the structure of the proof of the subtype relation.

Case ( ≤ -Refl.)

Trivial.

Case ( ≤ -Trans.)

Obvious from assumptions.

Case ( ≤ -Taut.)

We only need to prove [[P]]R⃗ ≤ [[Γ(P)]]R⃗ holds.

We can consider three cases.

1. In the case that P = X and (X ≤ T) ∈ Γ hold, it is proved from Definition 3.4.9.

2. In the case that P = Range(P′) and Γ(P′) = S → T hold, we have Γ(P) = Γ^{∗}(P) = T . Then, by induction hypothesis, we have [[P′]]R⃗ ⊆ [[S → T]]R⃗. Since AP([[P′]]R⃗, [[S]]R⃗) ⊆ [[T]]R⃗ and [[T]]R⃗ ∈ SAT hold, we have [[Range(P′)]]R⃗ ⊆ [[T]]R⃗.

3. In the case where P = Range(P′) and Γ(P′) = Q′ hold, we have Γ^{∗}(P′) = Γ^{∗}(Q′) . Then we have easily [[Range(P′)]]R⃗ ⊆ [[Range(Q′)]]R⃗.

Case ( ≤ - →.)

\begin{matrix}Γ ⊢ S′ ≤ S & Γ ⊢ T ≤ T′ \\ Γ ⊢ S → T ≤ S′ → T′ \end{matrix} ( ≤ - →)

From assumptions, [[S′]]R⃗ ⊆ [[Γ ⊢ S]]R⃗ and [[T]]R⃗ ⊆ [[T′]]R⃗ hold. For every f ∈ [[S → T]]R⃗ and e ∈ [[S′]]R⃗, e ∈ [[S]]R⃗ holds, and therefore, fe ∈ [[T]]R⃗ ⊆ [[T′]]R⃗ holds. Hence, f ∈ [[S′ → T′]]R⃗ holds.

Case ( ( ≤ -(bb) ∀).)

Γ ⊢ ∀Y ≤S.T type Γ ⊢ S′ ≤ S Γ, X ≤ S′ ⊢ T ≤ T′

Γ ⊢ ∀Y ≤S.T ≤ ∀Y ≤S′.T′ ( ≤ -bb ∀)

From assumptions, [[Γ ⊢ S′]]R⃗ ⊆ [[Γ ⊢ S]]R⃗ and for every C ⊆ [[Γ ⊢ S′]]R⃗ such that C ∈ SAT holds, [[Γ, Y ≤ S′ ⊢ T]](R⃗, Y := C) ⊆ [[Γ, Y ≤ S′ ⊢ T′]](R⃗, Y := C) holds. For every e ∈ [[Γ ⊢ ∀Y ≤S.T]]R⃗, for every C ⊆ [[Γ ⊢ S]]R⃗ such that C ∈ SAT holds, e ∈ [[Γ, Y ≤ S′ ⊢ T]](R⃗, Y := C) , then since Γ ⊢ S′ ≤ S , for every C ⊆ [[Γ ⊢ S′]]R⃗ such that C ∈ SAT holds, e ∈ [[Γ, Y ≤ S′ ⊢ T]](R⃗, Y := C) ⊆ [[Γ, Y ≤ S ⊢ T′]](R⃗, Y := C) = [[Γ, Y ≤ S′ ⊢ T′]](R⃗, Y := C) holds, and therefore e ∈ [[Γ ⊢ ∀Y ≤S′.T′]]R⃗ holds.

Case ( ≤ -record.)

For all i = 1, ⋯, n, Γ ⊢ S_{i} ≤ T_{i}
\{ \begin{matrix}Γ ⊢ [l_{1}:S_{1}, ⋯, l_{n}:S_{n}, l_{n+1}:S_{n+1}, ⋯, l_{n+m}:S_{n+m}] \\ ≤ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] \end{matrix}

( ≤ -record)

Assume e ∈ [[ [l_{1}:S_{1}, ⋯, l_{n}:S_{n}, l_{n+1}:S_{n+1}, ⋯, l_{n+m}:S_{n+m}] ]]R⃗. By definition of [[ ]] , for all i = 1, … n, e · l_{i} ∈ [[S_{i}]]R⃗ holds. By induction hypothesis, we have e · l_{i} ∈ [[T_{i}]]R⃗. Therefore we have e ∈ [[ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] ]]R⃗.

Case ( Range .)

Γ ⊢ Range(P) type Γ ⊢ Range(Q) type Γ ⊢ P ≤ Q

Γ ⊢ Range(P) ≤ Range(Q)

( Range )

Because Range can be derived from ( ≤ -Taut) by Proposition 3.2.15, we can prove it similarly.

Case ( Sel .)

Γ ⊢ Sel(P, l) type Γ ⊢ Sel(Q, l) type Γ ⊢ P ≤ Q
Γ ⊢ Sel(P, l) ≤ Sel(Q, l)

( Sel )

Immediate from [[P]]R⃗ ⊆ [[Q]]R⃗ from definitions.

Lemma 3.4.13.

1. [[Range(S → T)]]R⃗ ≡ [[T]]R⃗

2. [[Sel([…, l:T, …], l)]]R⃗ ≡ [[T]]R⃗

( Proof ): We prove only the first case. The proof of ⊂ is easy. We prove ⊃. For every e ∈ [[T]]R⃗, x ∉ FV(e) , and every f ∈ [[S]]R⃗, we have e[x := f] = e ∈ [[T]]R⃗. Therefore (λx.e)f ∈ [[T]]R⃗ from (S2) and we have λx.e ∈ [[S → T]]R⃗. We can provide a new variable y such that x ≠ y and y ∉ FV(e) hold, and from (S1) y ∈ [[S]]R⃗. Then we have (λx.e)y ∈ [[Range(S → T)]]R⃗, and therefore from (S0), we have also e ∈ [[Range(S → T)]]R⃗.

Finnally we must show that if Γ ⊢ e : T holds, then we have for every interpretation R⃗ ∈ [[Γ]] , Erase(e) ∈ [[Γ ⊢ T]]R⃗. (Therefore Erase(e) is always strongly normalizing.)

Lemma 3.4.14.

For every proof Γ ⊢ e : S , if for every type substitution ϕ : FV(e) → Λ , if ϕ(x) ∈ [[Γ ⊢ T]]R⃗ for every x^{T} ∈ FV(e) , then ϕ(Erase(e)) ∈ [[Γ ⊢ S]]R⃗.

Notation 3.4.15.

For every type substitution ϕ, we define the type substitution ϕ[x := e] as follows:

\begin{aligned}ϕ[x := e](x) & = & e \\ ϕ[x := e](y) & = & ϕ(y) & (y ≠ x) \end{aligned}

( Proof ):

Induction on the structure of the proof of the type-assignment.

Case ( var.)

Obvious from definitions.

Case ( λ -ap.)

\begin{aligned}Γ ⊢ e : S → T & Γ ⊢ f : U & Γ ⊢ U ≤ S \\ & Γ ⊢ ef : T \end{aligned} ( λ -ap)

By induction hypothesis, we have ϕ(Erase(e)) ∈ [[S → T]]R⃗ and ϕ(Erase(f)) ∈ [[U]]R⃗ ⊆ [[S]]R⃗. By definition of [[S → T]]R⃗, we have (Erase(e))(Erase(f)) ∈ [[T]]R⃗

Case ( λ - Range .)

Γ ⊢ e : P Γ ⊢ f : U Γ^{∗}(P) = S → T Γ ⊢ U ≤ S
Γ ⊢ ef : Range(P)

( λ - Range )

By induction hypothesis, we have ϕ(Erase(e)) ∈ [[P]]R⃗ and ϕ(Erase(f)) ∈ [[U]]R⃗ ⊆ [[S]]R⃗. By definition of [[Range(P)]]R⃗, since Erase(ef) = Erase(e)Erase(f) ∈ AP([[P]]R⃗, [[S]]R⃗) holds, we have Erase(ef) ∈ [[Range(P)]]R⃗.

Case ( λ -ab.)

{Γ ⊢ f : T \atop Γ ⊢ (λx^{S}.f) : S → T} ( λ -ab)

We have FV(λx^{S}.f) = FV(f)−{x}. Let ϕ be any substitution with domain FV(f)−{x}, let e be any term in [[S]]R⃗.By α -conversion, we always assume that FV(e) is disjoint from FV(f) . Then, we form the subsumption ϕ[x := e] with domain FV(f) . By induction hypothesis, we have ϕ[x := e](Erase(f)) ∈ [[T]]R⃗. Then by choosing x = e, we have Erase(f) ∈ [[T]]R⃗. Note that ϕ[x := e](Erase(f)) = ϕ(Erase(f))[x := e] . Thus ϕ(Erase(f))[x := e] ∈ [[T]]R⃗. We can apply (S2), and then we have (λx.Erase(f))e ∈ [[T]]R⃗. By the definition of [[S → T]] , we have ϕ(Erase(λx^{S}.f)) = λx.(Erase(f)) ∈ [[S → T]]R⃗

Case ( (bound-) Λ -ap-w.)

\begin{aligned}Γ ⊢ e : ∀Y ≤S.T & Γ ⊢ V ≤ S & T [X := V] ≡⟩ T′ \\ & Γ ⊢ e\{V \} : T′ \end{aligned} (bound- Λ -ap-w)

By induction hypothesis, ϕ(Erase(e)) ∈ [[∀Y ≤S.T]]R⃗. Since the definition of [[∀Y ≤S.T]]R⃗, we have Erase(e{V }) ∈ [[Γ, Y ≤ S ⊢ T]](R⃗, Y := [[Γ ⊢ V]]R⃗) . Therefore ϕ(e{V }) = ϕ(e) ∈ [[Γ ⊢ T [Y := V]]]R⃗.

By Lemma 3.4.13 , we have [[Γ ⊢ T [Y := V]]]R⃗ = [[Γ ⊢ T′]] . So we have ϕ(e{V }) ∈ [[Γ ⊢ T′]]R⃗.

Case ( bound- Λ -ab.)

{Γ, Y ≤ S ⊢ f : T \atop Γ ⊢ (ΛY ≤S.f) : ∀Y ≤S.T} (bound- Λ -ab)

In this rule, no free variable of type Y occurs in f .

By induction hypothesis, for every C ∈ SAT such that C ⊆ [[Γ ⊢ S]]R⃗, ϕ(Erase(f)) ∈ [[Γ, Y ≤ S ⊢ T]](R⃗, Y := C) , that is, Erase(ΛY ≤S.f) = Erase(f) ∈ ⋂_{C∈SAT, C⊆[[Γ⊢S]]R⃗}[[Γ, Y ≤ S ⊢ T]](R⃗, Y := C) = [[Γ ⊢ ∀X≤S.T]]R⃗.

Case ( record.)

For all i = 1, ⋯, n, Γ ⊢ T_{i} type
Γ ⊢ [l_{1} : T_{1}, ⋯, l_{n} : T_{n}] type

(record)

For all i = 1, ⋯, n, assume e_{i} ∈ [[T_{i}]]R⃗.

By induction hypothesis, we have Erase(e_{i}) ∈ [[T_{i}]]R⃗. Applying (S3), we have {l_{1}=e_{1}, ⋯, l_{i}=e_{i}, ⋯, l_{n}=e_{n}} · l_{i} ∈ [[T_{i}]]R⃗. By definition of [[ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] ]]R⃗, we have Erase({l_{1}=e_{1}, ⋯, l_{n}=e_{n}}) ∈ [[ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] ]]R⃗

Case ( recordsel.)

By induction hypothesis, we have ϕ(Erase(e)) ∈ [[ [l_{1} : T_{1}, ⋯, l_{n} : T_{n}] ]]R⃗. By definition of [[ [l_{1} : T_{1}, ⋯, l_{n} : T_{n}] ]]R⃗, we have Erase(e · l_{i}) = (Erase(e)) · l_{i} ∈ [[T_{i}]]R⃗

Case ( record- Sel .)

Γ ⊢ e : P Γ ⊢ Sel(P, l) type
Γ ⊢ e · l : Sel(P, l)

(record- Sel )

Similarly to Case ( λ - Range ).

Case ( (coer).)

\begin{matrix}Γ ⊢ e : S & Γ ⊢ S ≤ T \\ Γ ⊢ e|_{T} : T \end{matrix} (coer)

By induction hypothesis, Erase(e) ∈ [[S]]R⃗. Since [[S]]R⃗ ⊆ [[T]]R⃗, Erase(e|_{T}) = Erase(e) ∈ [[T]]R⃗

From these discussions, the main theorem of this section is proved:

Theorem 3.4.16.

For every raw term e if e type-checks, then Erase(e) ∈ SN

( Proof ): We now apply Lemma 3.4.14 to any assignment (for example, the constant assignment with value SN ) and to the identity substitution, which is legitimate since by (S1), every variable belongs to every saturated set.

3.4.4 Termination of cF_{≤}^{+} Terms

In this section we prove that if the type erasure of an cF_{≤}^{+} term is strongly normalizing then the term itself is strongly normalizing.

We consider the term e and its type erasure Erase(e) .

We prove it by assuming that a typed-term e is not strongly normalizing and Erase(e) is strongly normalizing and deriving contradictions.

Consider an infinite reduction chain in cF_{≤}^{+} . It consists of segments of (β) reduction intermixed with segments of (β2) and (coer*) reductions. Consider the chain of all the type erasures of the elements of the cF_{≤}^{+} chain. To each (β) step in the original chain the same step corresponds in the erased chain, while to each pairs of terms related by a (β2) or (coer*) step in the cF_{≤}^{+} chain two identical terms correspond in the erased chain. This means that collapsing all sequences of identical terms, in the erased chain, into one element, we still obtain a reduction in the type erased cF_{≤}^{+} . But each (β2) reduction deletes a Λrec symbol from the cF_{≤}^{+} term, and then any segment of (β2) reductions has a finite length. Moreover every coercion operator appears and is duplicated only when (β) reduction occurs, and it can move only rightward. when (coer) or (coer2) reduction occurs, and disappear when (coerconst) occurs. So collapsing all segments of (β2) and (coer*) reductions into one term transforms an infinite chain into another infinite chain. This proves that to any infinite reduction chain in cF_{≤}^{+} , an infinite reduction in type erased cF_{≤}^{+} corresponds, and so termination for type-erased cF_{≤}^{+} terms implies termination for cF_{≤}^{+} terms.

Then we conclude that every cF_{≤}^{+} term which can type-check is strongly normalizing.

3.5 Example

We discuss the re-usability of programs in cF_{≤}^{+} and the relation between object-oriented languages and cF_{≤}^{+} more deeply.

cF_{≤}^{+} , instead of F_{≤} , fits our intuition that every term has its exact type in a pragmatic programming languages [OBBT89] because in cF_{≤}^{+} every term has its exact type while in F_{≤} not. Moreover, we show, from some examples, that we can develop the programming efficiency and the re-usability of programs in cF_{≤}^{+} better than F_{≤} Example 3.5.1.

m = ΛX≤[l:T].λx^{X}.x · l

can have the type ∀X≤[l:T].X → T and its super types in F_{≤} because of subsumption rule. However, in cF_{≤} , m cannot have its type. But, in cF_{≤}^{+} , m ’s type is uniquely determined as

\begin{matrix}X ≤ [l:T] ⊢ x : X & (X ≤ [l:T])^{∗}(X) ≡ [l:T] \\ X ≤ [l:T] ⊢ x · l : Sel(X, l) \end{matrix} ; X ≤ [l:T] ⊢ λx^{X}.x · l : X → Sel(X, l)

Γ ⊢ ΛX≤[l:T].λx^{X}.x · l : ∀X≤[l:T].X → Sel(X, l)

Example 3.5.2.

In the system cF_{≤}^{+} , under an environment Γ , for a term m in Example 3.5.1, a type [l:S] where Γ ⊢ S ≤ T holds, and a term {l=n} of the type [l:S] which have been described in section 1, (m{[l:S]})({l=n}) has the type S , while, in F_{≤} , (m{[l:S]})({l=n}) ’s minimal type is no more than T though

(λx^{[l:S]}.x · l){l=n}

can have the type S both of in F_{≤} and in cF_{≤}^{+} .

3.6 Conclusion

In this chapter, we introduced the calculus cF_{≤}^{+} , which is a second order λ -calculus with records, coercion operator and bounded quantification including new types Range(X) and Sel(X, l) . We also proved that cF_{≤}^{+} has good properties (unicity of type, Subject Reduction, Church-Rosser, and Strong Normalization) and showed some applications of cF_{≤}^{+} to object-oriented languages.

cF_{≤}^{++}—A Type System with Type

instantiation

4.1 Introduction

In the previous chapter, cF_{≤}^{+} is introduced to overcome the problem discussed in Section 1.2. However, cF_{≤}^{+} cannot completely solve it because cF_{≤}^{+} does not include the type instantiation (as already discussed in Section 3.1).

In this chapter, we give a calculus cF_{≤}^{++} by adding the type instantiation to cF_{≤}^{+} . In cF_{≤}^{++} , we show that the type system of cF_{≤}^{++} is well defined, for example, that, under the type instantiation rule Inst(∀X≤S.T, U) ⇒ T [X := U] , every well-defined type always terminates. We proved it by attributing a “kind” to type. In cF_{≤}^{++} , the treatments of subtype relation are different from that in cF_{≤}^{+} . It is treated only as a binary relation and their meanings are not considered. So the treatments of l.u.b and w.l.u.b. are also different.

4.2 Kind

In this section we describe the kind system of cF_{≤}^{++} , which is a classification of types. Note that the notion of Kind introduced in this chapter is different from that defined in higher-order λ -calculus, F_{ω} [Gir72]. Kind is introduced only to prove the termination of the “reduction” of the type system of cF_{≤}^{++} and the existence of working least upper bound, and is not related to properties of terms.

Notation 4.2.1.

We do not use only the notations defined in Notation 3.2.1 but also this following notation when no specific notation is declared.

Notation Metavariable
Kind  K, L, …

We firstly define the Kind, its subtype relation, and its degree.

42 CHAPTER 4. CF_{≤}^{++} —A TYPE SYSTEM WITH TYPE INSTANTIATION

Definition 4.2.2. (Kind)

K ::= ∗  (kind for base types)
| Arr(K) (kind for →-types)
| K_{1} → K_{2} (kind for ∀-types)
| Ω  (kind for arbitrary types)

Subkind

K ≤ Ω (Ω)

{K ≤ L \atop Arr(K) ≤ Arr(L)} (Arr)

\begin{matrix}L_{1} ≤ K_{1} & K_{2} ≤ L_{2} \\ K_{1} → K_{2} ≤ L_{1} → L_{2} \end{matrix} (→)

Degree of Kind

\begin{aligned}| ∗ | & = & 1 \\ |Ω| & = & 1 \\ |Arr(K)| & = & |K| + 1 \\ |K → L| & = & |K| + |L| + 1 \end{aligned}

4.3 Type

In this section we describe the type system cF_{≤}^{++} . We also assume that there is no subtype relation between base types.

Definition 4.3.1. ( Raw Type)

Raw types are defined as follows.

T := X  type variable
| B  base type
| Top  Top
| T → T  function type
| ∀X≤T.T  (bounded) universal type
| Range(T) range type
| Inst(T_{1}, T_{1}) instantiation type
| Domain(T) domain type
| Upper(T) (upper) bound type

The definition of raw types is an extension of that of F_{≤} . Raw types are divided into working types and non-well-working types. Working types consist of base types, function types, (bounded) universal types, which are the same as defined in F_{≤} , and Top . Top is the only supertype of all types. Non-well-working types consists of type variables, range types, and instantiation types.

Range types have the feature Range(P) , where P has a super type that is a function type, and when a function type S → U is substituted for P , Range(P) is reduced to U . Instantiation types have the feature Inst(P, T) , where P has a super type that is a universal type, and when a universal type ∀X≤S.U is substituted for P , Inst(P, T) is reduced to U[X := T] . Domain types have the feature Domain(P) , where P has a super type that is a function type, and when a function type S → U is substituted for P , Domain(P) is reduced to S . Bound types have the feature Upper(P) , where P has a super type that is a universal type, and when a universal type ∀X≤S.U is substituted for P , Upper(P) is reduced to S .

Both domain types and bound types are only used to prove the termination of reduction rules of types, and we do not consider the subtype relation and the type assignment to terms of the types Domain(P) or Upper(P) .

Definition 4.3.2. (Normal Form)

We call a raw type P in normal form if P satisfies these conditions:

• P does not contain Range(S → T) or Inst(∀X≤S.T, U) .

• P does not contain Domain , or Upper .

If a raw type P is in normal form and there exist S and T where P = S → T or P = ∀X≤S.T holds, we call P a working type. Otherwise we call P a non-well-working type.

Definition 4.3.3. (Type Environment)

In cF_{≤}^{++} , a (type) environment is defined as a sequence of pairs of a free type variable and its “upper bound”. It is also defined mutually to definition of type good-formation in Definition 4.3.6.

ϕ env
Γ env Γ ⊢ T : Ω X ∉ FV(Γ)
Γ, X:K, X ≤ T env

Definition 4.3.4.

For a non-well-working type Range(P) and Domain(P) (respectively Inst(P, U) and Upper(P) ), a working type S → T ( ∀X≤S.T ) is substituted for P . The (raw) type Range(S → T) and Domain(S → T) ( Inst(∀X≤S.T, U) and Upper(∀X≤S.T) ) need to be reduced to a “normal form”.

Range(S → T) ⇒ T
Inst(∀X ≤ S.T, U) ⇒ T [X := U]
Domain(S → T) ⇒ S
Upper(∀X ≤ S.T, U) ⇒ S

Especially, we call the rule Inst(∀X ≤ S.T, U) ⇒ T [X := U] the type instantiation. When, after a finite number of reductions, a type T which is not in normal form, is reduced to V which is in normal form, we write down T ≡⟩ V .

Definition 4.3.5.

For each type T , we want to define the l.u.b. (least upper bound) of T , Γ(T) . Of course, when T is a working type, we define Γ(T) = T , Otherwise, that is, when P is a non-well-working type, we define Γ(P) as follows:

Γ(X)  ⇒ T (where (X ≤ T) ∈ Γ)
Γ(Range(P)) ⇒ V (where Range(Γ(P))≡⟩V)
Γ(Inst(P, T)) ⇒ V (where Inst(Γ(P), T)≡⟩V)

We have three kinds of type judgements: for the type good-formation (Γ ⊢ S : K) , for the subtype relation (Γ ⊢ S ≤ T : K) and for the type assignment (Γ ⊢ e : S) . We also call the first two kinds of judgements type judgements. All kinds of type judgements are mutually defined.

4.3.1 Type Judgements

Definition 4.3.6. (Type good-formation ( Γ ⊢ S : K ))

Type good-formation ( Γ ⊢ S : K )

We define the judgement of the type “good-formation”, which assigns types to kinds.

{X:K ∈ Γ \atop Γ ⊢ X : K} (Var)
Γ ⊢ Top : Ω (Top)

\begin{matrix}Γ ⊢ S : Ω & Γ ⊢ T : L \\ Γ ⊢ S → T : Arr(L) \end{matrix} (→)

\begin{matrix}Γ ⊢ S : Ω & Γ, X:K, X ≤ S ⊢ T : L \\ Γ ⊢ ∀X≤S.T : K → L \end{matrix} (bound-∀)
Γ ⊢ P : Arr(L)
Γ ⊢ Range(P) : L

(Range)

\begin{matrix}Γ ⊢ P : K → L & Γ ⊢ U : K \\ Γ ⊢ Inst(P, U) : L \end{matrix} (Inst)

Γ ⊢ P : Arr(K) Γ ⊢ Domain(P) : Ω

(Domain)

Γ ⊢ P : K → L
Γ ⊢ Upper(P) : Ω

(Upper)

\begin{matrix}Γ ⊢ T : K & K ≤ L \\ Γ ⊢ T : L \end{matrix} (kind-subsumption)

Proposition 4.3.7. (Subject Reduction of type )

For a pretype T , if Γ ⊢ T : K and T ⇒ T′ , then Γ ⊢ T′ : K holds.

( Proof ): We need only to prove the type instantiation.

Inst(∀X≤S.T.U) ⇒ T [X := U]

{⋮ . Π \atop Γ, X:K, X ≤ S ⊢ T : L} ; Γ ⊢ ∀X≤ S.T : K → L ⋮ . ; Γ ⊢ U : K
Γ ⊢ Inst(∀X≤S.T.U) : L
⇓

(Substitute Γ ⊢ X : K for Γ ⊢ U : K in Π.) Γ ⊢ T [X := U]

Note that X ≤ S is never used in Π .

4.3.2 Subtype Relation

In this section we define the rules of the subtype relation. In cF_{≤}^{++} , this subtype relation is only the binary relation between the types and we need not consider its intuitive semantics.

Definition 4.3.8. (Subtype Relation ( Γ ⊢ S ≤ T : K ))

Subtype Relation ( Γ ⊢ S ≤ T : K )

The definitions of the subtype relation are listed as below:

{Γ ⊢ T : K \atop Γ ⊢ T ≤ T : K} (≤-Refl)

\begin{aligned}Γ ⊢ X : K & Γ ⊢ T : K & (X ≤ T) ∈ Γ \\ & Γ ⊢ X ≤ T : K \end{aligned} (≤-Taut)

\begin{matrix}Γ ⊢ S ≤ T : K & Γ ⊢ T ≤ U : K \\ Γ ⊢ S ≤ U : K \end{matrix} (≤-Trans)

\begin{matrix}Γ ⊢ S ≤ T : K & K ≤ L \\ Γ ⊢ S ≤ T : L \end{matrix} (kind-subsumption)

\begin{matrix}Γ ⊢ S : K & S ⇒ T \\ Γ ⊢ S ≤ T : K \end{matrix} (kind-reduction1)

\begin{matrix}Γ ⊢ S : K & S ⇒ T \\ Γ ⊢ T ≤ S : K \end{matrix} (kind-reduction2)

\begin{matrix}Γ ⊢ S′ ≤ S : Ω & Γ ⊢ T ≤ T′ : L \\ Γ ⊢ S → T ≤ S′ → T′ : Arr(L) \end{matrix} (≤-→)

\begin{matrix}Γ ⊢ ∀X≤S.T : K → L & Γ ⊢ S′ ≤ S : Ω & Γ, X:K, X ≤ S′ ⊢ T ≤ T′ : L \\ Γ ⊢ ∀X≤S.T ≤ ∀X≤S′.T′ : K → L \end{matrix} (≤-bb∀)
Γ ⊢ P ≤ Q : Arr(L)

Γ ⊢ Range(P) ≤ Range(Q) : L

(Range)

Γ ⊢ U : K Γ ⊢ P ≤ Q : K → L
Γ ⊢ Inst(P, U) ≤ Inst(Q, U) : L

(Inst)

Remark 4.3.9.

When all types and subtype relations are already assigned to kinds, we can have the algorithm of judgement of subtype relation. However, if they are not, it will be difficult to get an algorithm of the judgement.

From the definitions the following properties are satisfied.

Proposition 4.3.10.

If Γ ⊢ S ≤ T : K then Γ ⊢ S : K and Γ ⊢ T : K hold.

( Proof ): Obvious.

Proposition 4.3.11. (Termination of Type)

1. Under an environment Γ , for every type expression T which is well-formed, T is strongly normalizing under the reduction rules defined in Definition 4.3.3.

2. If (X_{i} ≤ T_{i}) ∈ Γ ( i = 1, …, n) , we add X_{1} ⇒ T_{1}, …, X_{n} ⇒ T_{n} to “reduction rules” defined in Definition 4.3.3. Then for every well-formed type T , T is strongly normalizing under these reduction rules..

( Proof ): The proof is similar to that of strong normalization of simply typed λ - calculus[GLT89].

Induction on the size of Γ . For every kind K , we define the candidate of reducibility Red_{K}

Definition 4.3.12.

Red_{∗}  = {T : Γ ⊢ T : ∗ and terminating}
Red_{Arr(L)} = {T : Domain(T) ∈ Red_{Ω}, Range(T) ∈ Red_{L}}
Red_{K→L} = {T : Upper(T) ∈ Red_{Ω}
and for every U ∈ Red_{K},Inst(T, U) ∈ Red_{L} holds.}
Red_{Ω}  = {T : Γ ⊢ T : Ω and terminating}

Notation 4.3.13.

We denote ν(T) as a number which bounds the length of every normalization sequence beginning with T .

Definition 4.3.14.

The type T is neutral if T has a shape such as, B (base type), X (type variable), Domain(S) , Range(P) , Upper(P) and Inst(P, U) .

Lemma 4.3.15.

1. All types in Red_{K} is terminating.

2. If T ∈ Red_{K} and T ⇒ T′ , T′ ∈ Red_{K} .

3. T is neutral and for all T′ such that T ⇒ T′ , T′ ∈ Red_{K} holds, then T ∈ Red_{K} .

( Proof ): Induction of degrees of kinds:

Case ( Base type, and Ω .)

Obvious.

Case ( Arr(K) .)

Similar to the case K → L. So we omit.

Case ( K → L.)

1. Assume T ∈ Red_{K→L} . Since Upper(T) ∈ Red_{Ω} holds, Upper(T) is terminating. For a (fresh) type variable X : K , X is a normal form, then Inst(T, X) ∈ Red_{L} . Then we have ν(T) ≤ ν(Inst(T, X)) , and therefore T is terminating.

2. T ∈ Red_{K→L} , and assume T ⇒ T′ . By induction hypothesis, Upper(T) ∈ Red_{Ω} so, Upper(T′) ∈ Red_{Ω} . For every U ∈ Red_{K} , from assumptions, Inst(T′, U) ∈ Red_{L} because Inst(T, U) ⇒ Inst(T′, U) holds. So we have T′ ∈ Red_{K→L} .

3. Assume that T is neutral and that for every T′ such that T ⇒ T′ holds, T′ ∈ Red_{K→L} holds. Since Upper(T) cannot be a redex, and Upper(T′) ∈ Red_{Ω} , since T′ ∈ Red_{K→L} holds. So, by induction hypothesis, Upper(T) ∈ Red_{Ω} holds. Provide that U ∈ Red_{K} . By induction for K , we know that U is terminating; so we can reason about Inst(T, U) by induction on ν(U) .

• Inst(T′, U) with T ⇒ T′ ; but T′ ∈ Red_{K→L} , so Inst(T′, U) ∈ Red_{L} .

• Inst(T, U′) with U ⇒ U′ , U′ ∈ Red_{K} by induction hypothesis for K , and ν(U′) <

ν(U) ; so Inst(T, U′) ∈ Red_{L} .

We conclude that Inst(T, U) ∈ Red_{L} , and so T ∈ Red_{K→L} .

Proposition 4.3.16.

If T ∈ Red_{K} and K ≤ L hold, then T ∈ Red_{L}

( Proof ): We prove these four cases of subkind relation.

Case ( K ≤ Ω .)

If T ∈ Red_{K} , then T is terminating.

Case ( Arr(K) ≤ Arr(L) .)

Similar to the following case.

Case ( K_{1} → K_{2} ≤ L_{1} → L_{2} .)

Assume that T ∈ Red_{K_{1}→K_{2}} , for every U ∈ Red_{L_{1}} . Since U ∈ Red_{K_{1}} holds from hypothesis about L_{1} ≤ K_{1} , Inst(T, U) ∈ Red_{K_{2}} and therefore by hypothesis about K_{2} ≤ L_{2} , Inst(T, U) ∈ Red_{L_{2}} are satisfied.

Lemma 4.3.17.

1. If for a S ∈ Red_{Ω} and for all U ∈ Red_{K} , T [X := U] ∈ Red_{L} holds, then ∀X≤S.T ∈

Red_{K→L}

( Proof ): We want to show that Inst(∀X≤S.T, U) ∈ Red_{K→L} holds for all U ∈ Red_{K} . We reason by induction on ν(S) + ν(T) + ν(U) . Obviously Upper(∀X≤S.T) ∈ Red_{Ω} holds. The type Inst(∀X≤S.T, U) is reduced to

• ( T [X := U] ∈ Red_{L} ) From assumptions,

• ( Inst(∀X≤S′.T, U) with S ⇒ S′ ) By induction hypothesis,

• ( Inst(∀X≤S.T′, U) with T ⇒ T′ ) By induction hypothesis,

• ( Inst(∀X≤S.T, U′) with U ⇒ U′ ) By induction hypothesis,

it is easily proved.

Notation 4.3.18.

We consider the case where, when X ≤ T is included in Γ , X ⇒ T is included in reduction rules defined in Definition 4.3.4.

Lemma 4.3.19.

Assume Γ ⊢ X ≤ T : K . If T ∈ Red_{K} , then X ∈ Red_{K}

( Proof ): We prove only the case that K → L. Firstly we show that Upper(X) ∈ Red_{Ω} holds. The type Upper(X) is reduced to Upper(T) ∈ Red_{K} . Therefore since Upper(X) is neutral, Upper(X) ∈ Red_{Ω} .

Secondly we want to show that Inst(X, U) ∈ Red_{L} holds for all U ∈ Red_{K} . Since Inst(X, U) is neutral, we reason by induction on ν(T) + ν(U) . The type Inst(X, U) is reduced to

• ( Inst(T, U) ∈ Red_{L} ) From assumption,

• ( Inst(X, U) with U ⇒ U′ ) By hypothesis,

it is easily proved.

Then we completely proved Proposition 4.3.11.

From that proposition, this property is easily proved.

Proposition 4.3.20.

For T be any type, and suppose all the free type variables of T are among X_{1} ≤ T_{1}, …, X_{n} ≤ T_{n} of kind K_{1}, …, K_{n} . If U_{i} ∈ Red_{K_{i}} ( Γ ⊢ U_{i} ≤ T_{i} i = 1, …, n) then T [X⃗ := U⃗] ∈ Red_{L}

These properties are needed to prove the subject reduction of cF_{≤}^{++} .

Proposition 4.3.21.

Assume Γ ⊢ U ≤ S : K holds,

1. If Γ, X:K, X ≤ S, Δ ⊢ T : L, T [X := U] = T′ and Δ[X := U] = Δ′ hold, then Γ, Δ′ ⊢ T′ : L.

2. If Γ, X:K, X ≤ S, Δ ⊢ T ≤ V : L, T [X := U] = T′ , V [X := U] = V′ and Δ[X := U] = Δ′ hold, then Γ, Δ′ ⊢ T′ ≤ V′ : L.

( Proof ): From Proposition 4.3.10, we have Γ ⊢ S : K . Both two cases are easily proved by replacing X : K and X ≤ S : K with S : K and U ≤ S : K in the original proofs, respectively.

From Proposition 4.3.11, by applying (kind-reduction 1) and (kind-reduction 2), the following properties are easily proved.

Proposition 4.3.22. (Substitution Lemma)

Assume Γ ⊢ U ≤ S : K holds,

1. If Γ, X:K, X ≤ S, Δ ⊢ T : L, T [X := U] ≡⟩ T′ and Δ[X := U] ≡⟩ Δ′ hold, then Γ, Δ′ ⊢ T′ : L.

2. If Γ, X:K, X ≤ S, Δ ⊢ T ≤ V : L, T [X := U] ≡⟩ T′ , V [X := U] ≡⟩ V′ and Δ[X := U] ≡⟩ Δ′ hold, then Γ, Δ′ ⊢ T′ ≤ V′ : L.

4.4 Term

In the last section, we show that every type which has its kind ( = well-defined type ) is terminating under the reduction rules defined in Definition 4.3.4. So, in this section, we omit kinds for simplicity. For example, we replace Γ ⊢ T : K and Γ ⊢ S ≤ T : K with Γ ⊢ T type and Γ ⊢ S ≤ T , respectively. Before discussions, we define working least upper bounds as in Chapter 3.

Definition 4.4.1.

We need to obtain upper bound which is working for all non working type, because we want to know conditions which enable applications. To obtain the working upper bound of non working type P , we recursively define the working least upper bound (w.l.u.b.) Wlub_{Γ}(P) as follows:

Wlub_{Γ}(T) ≡ T  (T is a working type)
| Wlub_{Γ}(V) (T is a non-well-working type and Γ(T)≡⟩V)

From Proposition 4.3.11, these properties are satisfied:

Proposition 4.4.2.

1. Under an environment Γ , for all non working type P , the w.l.u.b. of P Wlub_{Γ}(P) always exists.

2. For two non-well working types P and Q, if Γ ⊢ P ≤ Q holds, then Wlub_{Γ}(P) ≡ Wlub_{Γ}(Q)

In this section, we describe the terms of cF_{≤}^{++} . We start by the definition of raw terms, among which we distinguish the terms, i.e. those raw terms possessing types. Raw terms are divided into several classes: variables, constants, function terms (functions), ∀ -terms, record terms, record selection terms, and coerced terms. Coercion is introduced to hold the properties of unicity of type and subject reduction.

Definition 4.4.3.

Before considering the term system, we re-consider the definition of type environment, range types and instantiation types, and subtype relation between them.

Type Environment

Γ env Γ ⊢ T type T is in normal form X ∉ FV(Γ)
Γ, X ≤ T env

Type Good-Formation

Γ ⊢ P type Wlub_{Γ}(P) ≡ S → T

Γ ⊢ Range(P) type

(Range)

Γ ⊢ P type Wlub_{Γ}(P) ≡ ∀X≤S.T Γ ⊢ U ≤ S

Γ ⊢ Inst(P, U) type

(Inst)

Subtype Relation

Γ ⊢ Range(P) type Γ ⊢ Range(Q) type Γ ⊢ P ≤ Q

Γ ⊢ Range(P) ≤ Range(Q)

(≤-Range)
Γ ⊢ Inst(P, U) type Γ ⊢ Inst(Q, U) type Γ ⊢ P ≤ Q

Γ ⊢ Inst(P, U) ≤ Inst(Q, U)

(≤-Inst)

The definition of (Inst) is valid because P and ∀X≤S.T share a kind under Γ .

4.4.1 Term

We define the raw terms and their type-assignment rules:

Definition 4.4.4. (Raw Terms)

e := x^{T}  (term) variable
| c^{T}  constant
| λx^{T} .e  λ-abs
| ee  λ-apl
| ΛX≤T.e (bounded) Λ-abs
| e{T }  Λ-apl
| e|_{T}  coerced term

We need to define the reduction of types ( ≡⟩ ) which stick to terms because these sorts of types must be in normal form.

Definition 4.4.5.

x^{T}  ≡⟩ x^{T′}  where T ≡⟩T
λx^{T} .e  ≡⟩ λx^{T′}.e′  where T ≡⟩T′ and e≡⟩e′
ef  ≡⟩ e′f′  where e≡⟩e′ and f≡⟩f′
ΛX≤S.e ≡⟩ ΛX≤S′.e′ where S≡⟩S′ and e≡⟩e′
e{T }  ≡⟩ e′{T′}  where T ≡⟩T′ and e≡⟩e′
e|_{T}  ≡⟩ e′|_{T′}  where T ≡⟩T′ and e≡⟩e′

Definition 4.4.6. (Type assignment ( Γ ⊢ e : S ))

Terms are selected by the rules below; since term variables are indexed by their type, the rules do not needed assumptions of the term (x : T) :

Γ ⊢ T type T is in normal form.

Γ ⊢ x^{T} : T (var)

Γ ⊢ e : T S is in normal form

Γ ⊢ (λx^{S}.e) : S → T (λ-ab)

\begin{aligned}Γ ⊢ e : S → T & Γ ⊢ f : U & Γ ⊢ U ≤ S \\ & Γ ⊢ ef : T \end{aligned} (λ-ap)
\{ \begin{matrix}Γ ⊢ e : P & Γ ⊢ f : U & Γ ⊢ P type \\ Wlub_{Γ}(P) ≡ (S → T) & Γ ⊢ U ≤ S \end{matrix}
Γ ⊢ ef : Range(P)

(λ-Range)

\{ \begin{matrix}Γ, X ≤ S ⊢ e : T S is in a normal form \\ no free variable whose type is X does not occur in e \end{matrix}
Γ ⊢ ΛX≤S.e : ∀X≤S.T

(bound-Λ-ab)

\{ \begin{matrix}Γ ⊢ e : ∀X≤S.T Γ ⊢ U ≤ S \\ U is in normal form \\ T [X := U]≡⟩T′ \end{matrix}
Γ ⊢ e{U} : T′

(bound-Λ-ap-w)

\{ \begin{matrix}Γ ⊢ e : P U is in normal form \\ Wlub_{Γ}(P) ≡ ∀X≤S.T \\ Γ ⊢ U ≤ S \end{matrix}
Γ ⊢ e{U} : Inst(P, U)

(Λ-ap-nw)

Γ ⊢ e : S Γ ⊢ S ≤ T T is in normal form

Γ ⊢ e|_{T} : T (coer)

From these definitions, the following property holds.

Proposition 4.4.7.

If Γ ⊢ e : T holds, T is in normal form.

4.4.2 Reduction

From Proposition 4.3.22, these properties hold:

Proposition 4.4.8. (Substitution Lemma)

1. If Γ ⊢ e : S and Γ ⊢ f : T hold, then Γ ⊢ e[x^{T} := f] : S holds.

2. If Γ, X ≤ S, Δ ⊢ e : T , and Γ ⊢ U ≤ S hold, then Γ, Δ′ ⊢ e′ : T′ holds where e[X := U] ≡⟩ e′ , T [X := U] ≡⟩ T′ , Δ[X := U] ≡⟩ Δ′ .

Now we define reduction rules ( →).

Definition 4.4.9. (Reduction)

We replace (coer2) with (coer2’), which is obtained by relaxing restrictions of (coer2).

The reduction rules in cF_{≤}^{++} are listed as follows:

Γ ⊢ (λx^{S}.e)f → e[x := f|_{S}] (β)

{e[X := S]≡⟩e′ \atop Γ ⊢ (ΛX≤S.e)\{T \} → e′} (bound β2)

{Range(S)≡⟩V \atop Γ ⊢ (e|_{S})f → (ef)|_{V}} (coer)

{Inst(P, U)≡⟩V \atop Γ ⊢ (e|_{P})\{U\} → (e\{U\})|_{V}} (coer2’)
Γ ⊢ e is in normal form S is a base type.
Γ ⊢ e|_{S} → e

(coerconst)

The reduction rules of cF_{≤}^{&}+ have good properties: Subject Reduction and Church-Rosser:

Theorem 4.4.10. (Subject Reduction)

For each expression e, if Γ ⊢ e : T and Γ ⊢ e → e′ hold, then Γ ⊢ e′ : T holds.

( Proof ): We prove only the case (coer2’). The other cases are proved similarly to Chapter 3. We replace, for example, “ Wlub_{Γ}(P) ≡ S → T ” with “ Γ ⊢ P ≤ S → T ”.

Case ( (coer2’).)

1. (working) We first consider the case both P and Q are working, i.e., P = ∀X≤V.W and Q = ∀X≤S.T .

\begin{aligned}I & {⋮ . Σ_{1} \atop Γ ⊢ U ≤ S} & T [X := U] ≡⟩ T′ \\ & Γ ⊢ (e|_{∀X≤S.T})\{U\} : T′ \end{aligned}

where I is

{⋮ . Π_{1} \atop Γ ⊢ e : ∀X≤V.W} {⋮ . Σ_{2} \atop Γ ⊢ ∀X≤V.W type}  {⋮ . Σ_{3} \atop Γ ⊢ S ≤ V}  {⋮ . Σ_{4} \atop Γ, X ≤ S ⊢ W ≤ T}

Γ ⊢ ∀X≤V.W ≤ ∀X≤S.T
Γ ⊢ e|_{∀X≤S.T} : ∀X≤ S.T

⇓

I’

{⋮ . Σ_{4} \atop Γ, X ≤ S ⊢ W ≤ T}  {⋮ . Σ_{1} \atop Γ ⊢ U ≤ S}
⋮ . (Subst. Lemma)
Γ ⊢ W′ ≤ T′
Γ ⊢ (e{U})|_{T′} : T′

where I’ is

{⋮ . Π_{1} \atop Γ ⊢ e : ∀X≤V.W}  {⋮ . Σ_{2} \atop Γ ⊢ ∀X≤V.W type}  \begin{matrix}{⋮ . Σ_{1} \atop Γ ⊢ U ≤ S} & {⋮ . Σ_{3} \atop Γ ⊢ S ≤ V} \\ Γ ⊢ U ≤ V \end{matrix}  W [X := U] ≡⟩ W′
Γ ⊢ e{U} : W′

2. (non working and working) Secondly, we consider the case that P is non working and Q = ∀X≤S.T

\begin{matrix}\begin{matrix}{⋮ . Π_{1} \atop Γ ⊢ e : P} & I \\ Γ ⊢ e|_{∀X≤S.T} : ∀X≤S.T \end{matrix} & {⋮ . Σ_{5} \atop Γ ⊢ U ≤ S} & T [X := U] ≡⟩ T′ \\ Γ ⊢ (e|_{∀X≤S.T})\{U\} : T′ \end{matrix}

where I is

{⋮ . Σ_{1} \atop Γ ⊢ P ≤ ∀X≤V.W (w.l.u.b)} {⋮ . Σ_{2} \atop Γ ⊢ ∀X≤ V .W type} {⋮ . Σ_{3} \atop Γ ⊢ S ≤ V} {⋮ . Σ_{4} \atop Γ, X ≤ S ⊢ W ≤ T}

Γ ⊢ ∀X≤V.W ≤ ∀X≤S.T
Γ ⊢ P ≤ ∀X≤S.T

⇓

I’  \begin{matrix}II & T [X := U] ≡⟩ T′ \\ Γ ⊢ Inst(P, U) ≤ T′ \end{matrix}
Γ ⊢ (e{U})|_{T′} : T′

where I’ is:

{⋮ . Π_{1} \atop Γ ⊢ e : P}  {⋮ . Σ_{1} \atop Γ ⊢ P ≤ ∀X≤V.W}  \begin{matrix}{⋮ . Σ_{5} \atop Γ ⊢ U ≤ S} & {⋮ . Σ_{3} \atop Γ ⊢ S ≤ V} \\ Γ ⊢ U ≤ V \end{matrix}
Γ ⊢ e{U} : Inst(P, U)

and II is:

{⋮ . Σ_{1} \atop Γ ⊢ P ≤ ∀X≤S.T} ⋮ .

Γ ⊢ Inst(P, U) type

⋮ .
Γ ⊢ Inst(∀X≤S.T, U) type

Γ ⊢ Inst(P, U) ≤ Inst(∀X≤S.T, U)

3. (non working and non working) Third, we consider the case both P and Q are non-working.

\begin{matrix}{⋮ . Π_{1} \atop Γ ⊢ e : P} & {⋮ . Σ_{1} \atop Γ ⊢ P ≤ Q} \\ Γ ⊢ e|_{Q} : Q \end{matrix}  {⋮ . Σ_{2} \atop Γ ⊢ Q ≤ ∀X≤S.T (w.l.u.b.)}  {⋮ . Σ_{3} \atop Γ ⊢ U ≤ S}

Γ ⊢ (e|_{Q}){U} : Inst(Q, U)

⇓

I’

{⋮ . Σ_{1} \atop Γ ⊢ P ≤ Q} ⋮ .

Γ ⊢ Inst(P, U) type

⋮ .

Γ ⊢ Inst(P, U) type

Γ ⊢ Inst(P, U) ≤ Inst(Q, U)

Γ ⊢ (e{U})|_{Inst(Q,U)} : Inst(Q, U)

where I’ is

{⋮ . Π_{1} \atop Γ ⊢ e : P}  \begin{matrix}{⋮ . Σ_{1} \atop Γ ⊢ P ≤ Q} & {⋮ . Σ_{2} \atop Γ ⊢ Q ≤ ∀X≤S.T} \\ Γ ⊢ P ≤ ∀X≤S.T \end{matrix}  {⋮ . Σ_{3} \atop Γ ⊢ U ≤ S}
Γ ⊢ e{U} : Inst(P, U)

In the proofs of Γ ⊢ Inst(⋯, U) are very easy and omitted.

Theorem 4.4.11.

cF_{≤}^{++} satisfies Church-Rosser property.

( Proof ): We can easily proved as in Chapter 3 using parallel reduction.

4.5 Conclusion

In this chapter, we proposed the calculus cF_{≤}^{++} by adding the type instantiation rule to cF_{≤}^{+} . We showed that, if the type instantiation rule is added, the reduction of type is always terminating. Thus, cF_{≤}^{++} is a sound extension of cF_{≤} and, in cF_{≤}^{++} , many terms which cannot type-check in cF_{≤} but can do in F_{≤} can have its type. For example, ΛX≤(∀Y ≤S.S).λx^{X}.x{S} cannot have its type in cF_{≤} but have the type ∀X≤(∀Y ≤S.S).X → S in F_{≤} . In cF_{≤}^{++} it has the type ∀X≤(∀Y ≤S.S).X → Inst(X, S) .

54 CHAPTER 4. CF_{≤}^{++} —A TYPE SYSTEM WITH TYPE INSTANTIATION

Symbiosis of Parametric and

Ad-hoc Polymorphisms

In this chapter we introduce cF_{≤}^{&}+ a calculus integrating parametric polymorphism and ad-hoc polymorphism by correcting mistakes of F_{≤}^{&} and using the techniques of cF_{≤}^{+} and cF_{≤}^{++} . Among this thesis, we use some informal judgements: for examples Γ ⊢ S ≡ T stands for “ Γ ⊢ S ≤ T and Γ ⊢ T ≤ S ”, and A_{h} = min_{i∈I}{A_{i} | Γ ⊢ A ≤ A_{i}} stands for “ Γ ⊢ A ≤ A_{h} and for every A_{i} such that Γ ⊢ A ≤ A_{i} holds, (Γ ⊢)A_{h} ≤ A_{i} holds”.

5.1 Introduction

F_{≤}^{&} [Cas93] seems the first calculus that integrates parametric polymorphism and ad-hoc polymorphism. As in [Cas93], in a programming language a function which performs a dispatch on a type passed as an argument would be probably written as:

Fun(X:*) =>
   if X<T1 then exp.1 else if X<T2 then exp.2 ... else if X<Tn then exp.n

This function executes exp_{1} if we pass to it a type less than or equal to T_{1} , and so on. If there is more than one candidate we select among them the branch with the least bound. In F_{≤}^{&} this function is denoted by:

ΛX≤T_{1}.exp_{1}&ΛX≤T_{2}.exp_{2}& … &ΛX≤T_{n}.exp_{n}

and its type is ∀X{T_{1}.S_{1}, T_{2}.S_{2}, …, T_{n}.S_{n}} where ( X ≤ T_{i} ⊢ exp_{i} : S_{i} ). However this type is a rough approximation yet. Indeed, to obtain a coherent and expressive system, we need strong restriction on the T_{i} ’s and S_{i} ’s.

First of all note that the selected branch may change during the computation. For example take a function f of type ∀X.{T_{1}.S_{1}, T_{2}.S_{2}} with T_{2} ≤ T_{1} . Consider now the expression (∀Y ≤ T_{1}.f[Y]) . Since Y ≤ T_{1} we guess that this expression will be ∀X≤T_{1}.S_{1} . But if we pass T_{2} subtype to the function , then, as Y is bound to T_{2} , the selected branch will be the second one and the result will have type S_{2} . If we want reductions to preserve the type in F_{≤}^{&} , we must require S_{2} to be the same type as S_{1} , which seems to be too strong a restriction. In F_{≤}^{&} , to ease this restriction, the constraint which is imposed on F_{≤}^{&} is that ⊢ T_{i} ≤ T_{j} then X ≤ T_{i} ⊢ S_{i} ≤ S_{j} (we call it the covariance condition ), not X ≤ T_{i} ⊢ S_{j} ≤ S_{i} (we call it the contravariance condition ). However, in this calculus the substitution property of the type system does not hold because, in F_{≤}^{&} , overloaded types does not satisfy contravariance of the left argument in the subtype relation.

For example,

\underline{X} ≤ Real ⊢ ∀Y.\{\underline{X}.Int, Real.Real\} type

is a valid type in F_{≤}^{&} . However, when Real is substituted for X , we have to prove

⊢ ∀Y.\{\underline{Real}.Int, Real.Real\} type,

only to fail.

To overcome this mistake, we must impose contravariance (as well as covariance) of the left argument in the subtype relation on overloaded types of the new calculus cF_{≤}^{&}+ .

We limit our study to the case where the bounds of an overloaded function range over basic types and record types all fields of which are base types. Indeed, the use of arrow types in the bounds posses many non-trivial and complicated problems to solve, due to the covariance and contravariance of the left argument in the subtype relation and the definition of ∩ -closed.

Definition 5.1.1.

Let Γ an environment. Given a set of base types or record types whose all fields are base types^{1} {A_{i}}_{i∈I} we write Γ ⊢ {A_{i}}_{i∈I} ∩ -closed iff for all i, j ∈ I if A_{i} and A_{j} have a common lower bound, then there exists h ∈ I where under Γ , A_{h} is the g.l.b. (abbreviation of “greatest lower bound”) of A_{i} and A_{j} . We write it as Γ ⊢ A_{h} = A_{i} ∩ A_{j} .

Note that ∩ -closure is quite a draconian restriction. Indeed ∩ -closed sets of bounds have a very preside form : they are partial downward semi-lattices, i.e. formed by disjoint unions of downward semi-lattices.

5.2 Type

In this section we describe the type system. We first define the pretypes.

Definition 5.2.1. (PreType)

T := P  non-well-working type
| W  working type
P := X  type variable
| Range(P)  range type
| Sel(P, l)  field type
| Inst(P, B)  instantiation type
W := B  base type
| T → T  function type
| [l_{i}:T_{i}]_{i=1,...,n}  record type
| ∀X.T  universal type
| ∀X≤T.T  bounded universal type
| ∀X{A_{1}.T_{1}, ⋯, A_{n}.T_{n}}  overloaded type
also denoted by ∀X{A_{i}.T_{i}}_{i=1,···,n}

We call a (pre)type A a hereditary basic type if A is a base type or a record type whose all fields are hereditary basic types, i.e.,

A = B  base type
| [l_{1}:A_{1}, …, l_{n}:A_{n}] record type whose all fields are hereditary basic types

1In cF_{≤}^{&}+ , the subtype relation between base types is not considered, while it is in F_{≤}^{&}

A type ∀X{A_{i}.T_{i}}_{i=1,...,n} represents a overloaded type. Overloaded types ∀X{A_{i}.T_{i}}_{i=1,...,n} must:

1. have bounds ranging over hereditary basic types.

2. have a ∩ -closed set of bounds.

3. satisfy covariance and contravariance, i.e., if A_{i} ≤ A_{j} then X ≤ A_{i} ⊢ T_{i} = T_{j} .

Definition 5.2.2.

For a non-well-working type Range(P) (respectively Sel(P, l_{i}) ) , a working type S → T ( [l_{1} : T_{1}, ⋯, l_{i} : T_{i}, ⋯, l_{n} : T_{n}] ) is substituted for P . The (raw) type Range(S → T) ( Sel([l_{1} : T_{1}, ⋯, l_{i} : T_{i}, ⋯, l_{n} : T_{n}], l_{i}) ) need to be reduced to a “normal form”.

Γ ⊢ Range(S → T)  ⇒ T
Γ ⊢ Sel([l_{i}:T_{i}]_{i∈I}, l_{j})  ⇒ T_{j}
Γ ⊢ Inst(∀X.{A_{i}.T_{i}}_{i∈I}, A) ⇒ T_{h}[X := A]
where Γ ⊢ A_{h} = min_{i∈I}{A_{i} | Γ ⊢ A ≤ A_{i}}

Definition 5.2.3. (Type)

We mutually define the type environment and the type good-formation:

ϕ env
Γ env X ∉ FV(()Γ)
Γ, X env
Γ env Γ ⊢ S type X ∉ FV(Γ)
Γ, X ≤ S env

{X ∈ F V (Γ) \atop Γ ⊢ X type} (Var)
Γ ⊢ S type Γ ⊢ T type

Γ ⊢ S → T type (→)

Γ, X ⊢ T type

Γ ⊢ ∀X.T type (∀)

Γ ⊢ S type Γ, X ≤ S ⊢ T type
Γ ⊢ ∀X≤S.T type

(bound-∀)

For all i = 1, ⋯, n, Γ ⊢ T_{i} type Γ ⊢ [l_{1} : T_{1}, ⋯, l_{n} : T_{n}] type

(record)

\{ \begin{matrix}Γ ⊢ ∀X≤A_{i}.T_{i} type \\ \{A_{i}\}_{i∈I} ∩-closed \\ If Γ ⊢ A_{i} ≤ A_{j}, then Γ, X ≤ A_{i} ⊢ T_{i} = T_{j} \end{matrix} \}

Γ ⊢ ∀X.{A_{i}.T_{i}}_{i∈I} type {}

Γ ⊢ P type Γ^{∗}(P) = S → T

Γ ⊢ Range(P) type

(Range)

Γ ⊢ P type Γ^{∗}(P) = [l_{1} : T_{1} ⋯, l_{i} : T_{i}, ⋯, l_{n} : T_{n}]
Γ ⊢ Sel(P, l_{i}) type

(record-Var)

Γ ⊢ P type Γ^{∗}(P) = ∀X.{A_{i}.T_{i}}_{i∈I} there is h ∈ I s.t. Γ ⊢ U ≤ A_{h}

Γ ⊢ Inst(P, U) type (Inst)

Definition 5.2.4. (Subtype Relation)

The rules of the subtype relation are listed as follows:

{Γ ⊢ T type \atop Γ ⊢ T ≤ T} (≤-Refl)

\begin{matrix}Γ ⊢ S ≤ T & Γ ⊢ T ≤ U \\ Γ ⊢ S ≤ U \end{matrix} (≤-Trans)
Γ ⊢ P type Γ(P)≡⟩V Γ ⊢ V ≤ T

Γ ⊢ P ≤ T (≤-Taut)

\begin{matrix}Γ ⊢ S′ ≤ S & Γ ⊢ T ≤ T′ \\ Γ ⊢ S → T ≤ S′ → T′ \end{matrix} (≤-→)

\begin{matrix}Γ ⊢ ∀X.T type & Γ, X ⊢ T ≤ T′ \\ Γ ⊢ ∀X.T ≤ ∀X.T′ \end{matrix} (≤-∀)
Γ ⊢ ∀X.T type Γ ⊢ S′ type Γ, X ≤ S′ ⊢ T ≤ T′

Γ ⊢ ∀X.T ≤ ∀X≤S′.T′ (≤-b∀)

ptΓ ⊢ ∀X≤S.T type Γ ⊢ S′ ≤ S Γ, X ≤ S′ ⊢ T ≤ T′ Γ ⊢ ∀X≤S.T ≤ ∀X≤S′.T′ (≤-bb∀)

\{ \begin{matrix}Γ ⊢ ∀X.\{A_{i}.S_{i}\}_{i∈I} type  Γ ⊢ ∀X.\{B_{i}.T_{i}\}_{j∈J} type \\ For all j ∈ J, there exists i ∈ I s.t.Γ ⊢ B_{j} ≤ A_{i} and Γ, X ≤ B_{j} ⊢ S_{i} ≤ T_{j} \end{matrix}

Γ ⊢ Γ ⊢ ∀X.{A_{i}.S_{i}}_{i∈I} ≤ ∀X.{B_{j}.T_{j}}_{j∈J} (≤-{})

For all i = 1, ⋯, n, Γ ⊢ S_{i} ≤ T_{i}

\{ \begin{matrix}Γ ⊢ [l_{1}:S_{1}, ⋯, l_{n}:S_{n}, l_{n+1}:S_{n+1}, ⋯, l_{n+m}:S_{n+m}] \\ ≤ [l_{1}:T_{1}, ⋯, l_{n}:T_{n}] \end{matrix}

(≤-record)

Γ ⊢ Range(P) type Γ ⊢ Range(Q) type Γ ⊢ P ≤ Q

Γ ⊢ Range(P) ≤ Range(Q)

(≤-Range)
Γ ⊢ Sel(P, l) type Γ ⊢ Sel(Q, l) type Γ ⊢ P ≤ Q

Γ ⊢ Sel(P, l) ≤ Sel(Q, l)

(≤-Sel)
Γ ⊢ Inst(P, U) type Γ ⊢ Inst(Q, U) type Γ ⊢ P ≤ Q

Γ ⊢ Inst(P, U) ≤ Inst(Q, U)

(≤-Inst)

The type system of cF_{≤}^{&}+ satisfies the following property.

Proposition 5.2.5.

Assume Γ ⊢ U ≤ S holds, then Γ ⊢ U type and Γ ⊢ S type hold.

( Proof ): Obvious.

Remark 5.2.6.

From these definitions, a set of hereditary basic types has a partial downward semi-latice structure. An example of the structure of ∩ -closed set is written in Figure 5.2.6.

Proposition 5.2.7. (Substitution Lemma)

[figure: [l_{2}:Str]; [l_{1}:Int]; [l_{1}:Int, l_{2}:Str]; [l_{1}:Str, l_{2}:Str]; [l_{1}:Int, l_{3}:Bool]; [l_{1}:Int, l_{2}:Str, l_{3}:Bool]; SubType; SuperType]

Figure 5.1: Example of the Structure of ∩ -closed Set

1. Assume Γ ⊢ U type , Γ ⊢ T [X := U] ≡⟩ T′ , Γ ⊢ V [X := U] ≡⟩ V′ and Γ ⊢ Δ[X := U] ≡⟩ Δ′ hold,

(1) If Γ, X, Δ ⊢ T type holds, then Γ, Δ′ ⊢ T′ type .

(2) If Γ, X, Δ ⊢ T ≤ V type holds, then Γ, Δ′ ⊢ T′ ≤ V′ .

2. Assume Γ ⊢ U ≤ S , Γ ⊢ T [X := U] ≡⟩ T′ , Γ ⊢ V [X := U] ≡⟩ V′ and Γ ⊢ Δ[X := U] ≡⟩ Δ′ hold,

(1) If Γ, X ≤ S, Δ ⊢ T type holds, then Γ, Δ′ ⊢ T′ type .

(2) If Γ, X ≤ S, Δ ⊢ T ≤ V type holds, then Γ, Δ′ ⊢ T′ ≤ V′ .

(Remark) Assume Δ ≡ Y_{1} ≤ S_{1}, …, Y_{n} ≤ S_{n} . If Γ ⊢ S_{1}[X := U] ≡⟩ S′_{1} , Γ, Y_{1} ≤ S′_{1} ⊢ S_{2}[X := U] ≡⟩ S′_{2} , …, and Γ, Y_{1} ≤ S′_{1}, …, Y_{n−1} ≤ S′_{n−1} ⊢ S_{n}[X := U] ≡⟩ S′_{n} hold, we define Δ′ ≡ Y_{1} ≤ S′_{1}, …, Y_{n−1} ≤ S′_{n−1}, Y_{n} ≤ S′_{n} and write down Γ ⊢ Δ[X := U] ≡⟩ Δ′ .

( Proof ): We prove only the second case:

1. Induction on the structure of the proof of ( Γ, X ≤ S, Δ ⊢ T type ) and the size of Δ . We prove only two cases: the first is

Case ( Γ, X ≤ S, Δ ⊢ ∀Y.{A_{i}.T_{i}}_{i∈I} type .)

\{ \begin{matrix}Γ, X ≤ S, Δ ⊢ ∀Y ≤A_{i}.T_{i} type \\ \{A_{i}\}_{i∈I} ∩-closed \\ Γ, X ≤ S, Δ ⊢ A_{i} ≤ A_{j} ⇒ Γ, X ≤ S, Δ, Y ≤ A_{i} ⊢ T_{i} = T_{j} \end{matrix} \}

Γ, X ≤ S, Δ ⊢ ∀Y.{A_{i}.T_{i}}_{i∈I} type {}

Because A_{i} is closed, i.e., A_{i} includes no type variable, if Γ, X ≤ S, Δ ⊢ A_{i} ≤ A_{j} holds, then Γ, Δ′ ⊢ A_{i} ≤ A_{j} holds. The rest of this proof is quote similar to that in Chapter 3.

Case ( Γ ⊢ Inst(P, W) type .)

Γ ⊢ P type Γ^{∗}(P) = ∀Y.{A_{i}.T_{i}}_{i∈I} there is h ∈ I s.t. Γ ⊢ W ≤ A_{h}

Γ ⊢ Inst(P, W) type

( Inst )

We consider two subcases:

(1) ( P [X := U] ≡⟩ ∀Y.{A′_{j}.T′_{j}}_{j∈J} )

Assume W [X := U] ≡⟩ W′ . By ,induction hypothesis Inst(P, W)[X := U] ≡⟩ T′′_{h} where Γ, Δ′ ⊢ A′_{h} = min_{j∈J}{A′_{j} | Γ, Δ′ ⊢ W′ ≤ A′_{j}} and T′_{h}[Y := W′] ≡⟩ T′′_{h} . Such h exists because Wlub_{Γ}(P) ≡ ∀Y.{B_{i}.S_{i}}_{i∈I} holds and k exists such that Γ, X ≤ U, Δ ⊢ W ≤ B_{k} and therefore we have Γ, Δ′ ⊢ W′ ≤ B′_{k} where B_{k}[X := U] ≡⟩ B′_{k} . Then we have from substitution lemma:

⋮ . ; Γ, Δ′, Y ≤ A′_{h} ⊢ T′_{h} type  ⋮ . ; Γ, Δ′ ⊢ W′ ≤ A′_{h} T′_{h}[Y := W′] ≡⟩ T′′_{h}
⋮ . (By induction hypothesis,)
Γ, Δ′ ⊢ T′′_{h} type

(2) ( P [X := U] ≡⟩ Q)

Easy.

Other cases are proved similarly to Chapter 3.

2. Induction on the structure of the proof of Γ, X ≤ S, Δ ⊢ T ≤ V and the size of Δ . In this chapter we show the proof of two cases:

Case ( Γ, X ≤ S, Δ ⊢ Inst(P, W) ≤ T .)

(1) ( P [X := W] ≡⟩ ∀Y.{A_{j}.T_{j}}_{j∈J} )

We have Γ(P)[X := U] ≡⟩ ∀Y.{B_{i}.S_{i}}_{i∈I} by induction hypothesis and the rules of the subtype relation. Assuming W [X := U] ≡⟩ W′ , we have Inst(P, W)[X := U] ≡⟩ T′_{h} where A_{h} = min{A_{j} | Γ, X ≤ S, Δ ⊢ W ≤ A_{j}} and T_{h}[X := U] ≡⟩ T′_{h} . Such h exists because, from induction hypothesis, there exists k such that B_{k} = min{B_{i} | Γ, X ≤ S, Δ ⊢ W ≤ B_{i}} holds. Therefore we have:

⋮ . ; Γ, Δ′ ⊢ T′′_{h} ≤ T′

(2) ( P [X := W] ≡⟩ Q) Assume W [X := U] ≡⟩ W′ . Obvious from induction hypothesis, we have

⋮ . ; Γ, Δ′ ⊢ Q′ ≤ T′ Inst((Γ, Δ′)(Q), W′) ≡⟩ Q′
Γ, Δ′ ⊢ Inst(Q, W) ≤ T′

Case ( Γ, X ≤ S, Δ ⊢ Inst(P, W) ≤ Inst(Q, W) .) Assume that W [X := U] ≡⟩ W′ .

(1) ( P [X := U] ≡⟩ ∀Y.{A_{j}.T_{j}}_{j∈J} , Q[X := U] ≡⟩ ∀Y.{B_{i}.S_{i}}_{i∈I} )

Since, by induction hypothesis, Γ, Δ′ ⊢ ∀Y.{A_{j}.T_{j}}_{j∈J} ≤ ∀Y.{B_{i}.S_{i}}_{i∈I} holds, we have that for all i ∈ I there exists j ∈ J such that Γ, Δ′ ⊢ B_{i} ≤ A_{j} and Γ, Δ′, Y ≤ B_{i} ⊢ T_{j} ≤ S_{i} hold. Then by induction hypothesis and the definition of overloaded types, there exist j_{0} and i_{0} such that Γ, Δ′ ⊢ B_{i_{0}} ≤ A_{j_{0}} , Γ, Δ′, Y ≤ B_{i_{0}} ⊢ T_{j_{0}} ≤ S_{i_{0}} , B_{i_{0}} = min{B_{i} | Γ, Δ′ ⊢ W′ ≤ B_{i}} and A_{j_{0}} = min{A_{j} | Γ, Δ′ ⊢ W′ ≤ A_{j}} hold.

Therefore by induction hypothesis, Γ, Δ′ ⊢ T′_{j_{0}} ≤ S′_{i_{0}} holds where T_{j_{0}}[Y := W′] ≡⟩ T′_{j_{0}} and S_{i_{0}}[Y := W′] ≡⟩ S′_{i_{0}} hold.

(2) ( P [X := U] ≡⟩ P′ and Q[X := U] ≡⟩ ∀Y.{B_{i}.S_{i}}_{i∈I} ) By induction hypothesis, there exists i_{0} such that B_{i_{0}} = min{B_{i} | Γ, Δ′ ⊢ W′ ≤ B_{i}} holds. Therefore we have Γ, Δ′ ⊢ Inst(P′, W′) ≤ B′_{i_{0}} where B_{i_{0}}[Y := W′] ≡⟩ B′_{i_{0}} holds.

(3) ( P [X := U] ≡⟩ P′ and Q[X := U] ≡⟩ Q′ )

Obvious.

The other cases are proved similarly to Chapter 3.

5.3 Term

In this section we describe the terms of the language. We start by the definition of the preterms, among which we distinguish the terms, i.e. those preterms that possess a type. Roughly speaking, (pre)terms are defined in three classes: terms of the simply typed λ -calculus, terms for parametric polymorphism ( cF_{≤}^{+} ) and terms for overloading^{2}. Overloaded functions are built in a list fashion, starting by an empty overloaded function ϵ and concatenating new branches by & .

Definition 5.3.1. (PreTerm)

e := x^{T} | c^{T} | λx^{T} .e | ee  simply-typed λ-calculi
| {l_{1} = e, ⋯, l_{n} = e} | e · l record calculi
| ΛX.e | ΛX≤T.e | e{T } cF_{≤}^{+}
| ϵ | e&f | e[A]  overloading
| e|_{T}  coerced term

It is required that the bounds of an overloaded function range over hereditary basic types Therefore, the argument of an overloaded function can be restricted to be a basic hereditary basic types.

Definition 5.3.2. (Term)

{Γ ⊢ T type \atop Γ ⊢ x^{T} : T} (var)

{Γ ⊢ e : T \atop Γ ⊢ λx^{S}.e : S → T} (λ-ab)

\begin{aligned}Γ ⊢ e : S → T & Γ ⊢ f : U & Γ ⊢ U ≤ S \\ & Γ ⊢ ef : T \end{aligned} (λ-ap)
Γ ⊢ e : P Γ ⊢ f : U Γ^{∗}(P) = S → T Γ ⊢ U ≤ S
Γ ⊢ ef : Range(P)

(λ-Range)

{Γ, X ⊢ e : T \atop Γ ⊢ ΛX.e : ∀X.T} (Λ-ab)

{Γ, X ≤ S ⊢ e : T \atop Γ ⊢ ΛX≤S.e : ∀X≤S.T} (bound-Λ-ab)

\begin{aligned}Γ ⊢ e : ∀X≤S.T & Γ ⊢ U ≤ S & T [X := U]≡⟩T′ \\ & Γ ⊢ e\{U\} : T′ \end{aligned} (bound-Λ-ap-w)

2and records and coercion.

Γ ⊢ ϵ : ∀X.{} (overloaded-ϵ)
\{ \begin{matrix}Γ ⊢ e : ∀X.\{A_{i}.T_{i}\}_{i=1,...,n−1} Γ ⊢ f : ∀X≤A_{n}.T_{n} \\ Γ ⊢ ∀X.\{A_{i}.T_{i}\}_{i=1,...,n} type \end{matrix}

Γ ⊢ e&f : ∀X.{A_{i}.T_{i}}_{i=1,...,n} (overloaded-Λ-ab)

\begin{aligned}\{ & \begin{matrix}Γ ⊢ e : ∀X.\{A_{i}.T_{i}\}_{i=1,...,n} \\ A_{h} = min_{i=1,...,n}\{A_{i} | Γ ⊢ U ≤ A_{i}\} \\ T_{h}[X := U]≡⟩T′_{h} \end{matrix} \\ & Γ ⊢ e[U] : T′_{h} \end{aligned} (overloaded-Λ-ap-w)
Γ ⊢ e : P Γ ⊢ Inst(P, U) type
Γ ⊢ e[U] : Inst(P, U)

(Λ-ap-nw)

For all i = 1, ⋯, n, Γ ⊢ e_{i} : T_{i}

Γ ⊢ {l_{1} = e_{1}, ⋯, l_{n} = e_{n}} : [l_{1} : T_{1}, ⋯, l_{n} : T_{n}] (record-const)

{Γ ⊢ e : [⋯, l:T, ⋯] \atop Γ ⊢ e · l : T} (record-select)
Γ ⊢ e : P Γ ⊢ Sel(P, l) type
Γ ⊢ e · l : Sel(P, l)

(record-Sel)

\begin{matrix}Γ ⊢ e : S & Γ ⊢ S ≤ T \\ Γ ⊢ e|_{T} : T \end{matrix} (coer)

Proposition 5.3.3.

Assume Γ ⊢ U ≤ S , Γ ⊢ T [X := U] ≡⟩ T′ , Γ ⊢ e[X := U] ≡⟩ e′ and Γ ⊢ Δ[X := U] ≡⟩ Δ′ hold, If Γ, X ≤ S, Δ ⊢ e : T holds, then Γ, Δ′ ⊢ e′ : T′ .

( Proof ): Induction on the structure of the proof of ( Γ, X ≤ S, Δ ⊢ e : T ).

We prove (overloaded- Λ -ap-w) and from Proposition 5.2.7, the other cases are proved similarly to Chapter 3.

\{ \begin{matrix}Γ, X ≤ S, Δ ⊢ e : ∀Y.\{A_{i}.T_{i}\}_{i=1,...,n} \\ A_{h} = min_{i=1,...,n}\{A_{i} | Γ, X ≤ S, Δ ⊢ V ≤ A_{i}\} \\ T_{h}[Y := V]≡⟩T′_{h} \end{matrix}
Γ, X ≤ S, Δ ⊢ e[V] : T′_{h}

When Γ, X ≤ S, Δ ⊢ A_{h} = min_{i=1,...,n}{A_{i} | Γ, X ≤ S, Δ ⊢ V′ ≤ A_{i}} holds, then there is some j ∈ I such that Γ, Δ′ ⊢ A_{j} = min_{i=1,...,n}{A_{i} | Γ, Δ′ ⊢ V′ ≤ A_{i}} holds where V [X := U] ≡⟩ V′ . By induction hypothesis, ⊢ A_{j} ≤ A_{h} holds, and therefore we have Γ, X ≤ S, Δ, Y ≤ A_{j} ⊢ T_{h} ≡ T_{j} holds. Hence Γ, Δ, Y ≤ A ⊢ T′_{h} ≡ T′_{j} holds where T_{i}[X := U] ≡⟩ T′_{i} ( i = 1, …, n). Then we have Γ, Δ ⊢ T′′_{h} ≡ T′′_{j} where T′_{i}[Y := V′] ≡⟩ T′′_{i} ( i = 1, …, n).

5.4 Reduction

In this section we give the equational theory of the terms of cF_{≤}^{&}+ . We present it under the form of reduction rules.

Definition 5.4.1.

Assume we have global type environment Γ . We call a type T closed if no type variable is included in T .

Definition 5.4.2. (Reduction)

Γ ⊢ (λx^{S}.e)f → e[x := f|_{S}] (β)

{Γ ⊢ e[X := U]≡⟩e′ \atop Γ ⊢ (ΛX.e)\{T \} → e′} (β2)

{Γ ⊢ e[X := U]≡⟩e′ \atop Γ ⊢ (ΛX≤S.e)\{T \} → e′} (bound β2)
\{ \begin{matrix}A is closed. Γ ⊢ e&f : ∀X.\{A_{i}.T_{i}\}_{i=1,...,n} \\ n = max\{h | A_{h} = min_{i=1,...,n}\{A_{i} | Γ ⊢ A ≤ A_{i}\}\} \end{matrix}
Γ ⊢ (e&f)[A] → f{A}

(β-overload1)

\{ \begin{matrix}A is closed. Γ ⊢ e&f : ∀X.\{A_{i}.T_{i}\}_{i=1,...,n} \\ n ≠ max\{h | A_{h} = min_{i=1,...,n}\{A_{i} | Γ ⊢ A ≤ A_{i}\}\} \end{matrix}
Γ ⊢ (e&f)[A] → e[A]

(β-overload2)

\begin{matrix}Γ ⊢ f : T & Range(S)≡⟩V \\ Γ ⊢ (e|_{S})f → (ef)|_{V} \end{matrix} (coer)

\begin{matrix}Γ ⊢ e : ∀X≤V.W & T [X := U]≡⟩T′ \\ Γ ⊢ (e|_{∀X≤S.T})\{U\} → (e\{U\})|_{T′} \end{matrix} (coer2)

{ΓInst(P, A)≡⟩P′) \atop Γ ⊢ (e|_{P})[A] → (e[A])|_{P′}} (coerInst)
e is in normal form. S is a base type.
Γ ⊢ e|_{S} ⇒ e

(coerconst)

Besides these rules there are the usual rules for the context closure; among these the only one that deserves a note is the rule for Λ . For what it concerns the rules, note that in ( β -overload1) and ( β -overload2) we require that the types involved in the selection of a branch are closed. In this way we always select the most precise branch. In this chapter, we impose the restriction on the reduction rule ( β -overload1) and ( β -overload2) because we want cF_{≤}^{&}+ to satisfy Church-Rosser. However, this restriction is based on the global type environment, and so and, in future, we will have to consider the specific reduction strategy like λv -calculus [Plo75].

cF_{≤}^{&}+ has there good properties:

Proposition 5.4.3.

1. cF_{≤}^{&}+ satisfies Subject Reduction.

2. cF_{≤}^{&}+ satisfies Church-Rosser.

( Proof ):

1. (Subject Reduction)

We prove only the case ( β -overload1) and ( β -overload2). The other cases are trivial or proved similarly as in Chapter 3 and 4.

Case ( β -overload1.)

I  … {⋮ . Π_{2} \atop Γ ⊢ A ≤ A_{n}} …; ⋮ . ; A_{n} = min_{i=1,...,n}\{A_{i} | Γ ⊢ A ≤ A_{i}\} T_{n}[X := A] ≡⟩ T′_{n}
Γ ⊢ (e&f)[A] : T′_{n}

where I is

{⋮ . Σ_{1} \atop Γ ⊢ e : ∀X\{A_{i}.T_{i}\}_{i=1,...n−1}}  {⋮ . Σ_{2} \atop Γ ⊢ f : ∀X≤A_{n}.T_{n}}  {⋮ . Π_{1} \atop Γ ⊢ ∀X.\{A_{i}.T_{i}\}_{i=1,...,n} type}
Γ ⊢ e&f : ∀X.{A_{i}.T_{i}}_{i=1,...,n}

⇓

\begin{aligned}{⋮ . Σ_{2} \atop Γ ⊢ f : ∀X≤A_{n}.T_{n}} & {⋮ . Π_{2} \atop Γ ⊢ A ≤ A_{n}} & T_{n}[X := A] ≡⟩ T′_{n} \\ & Γ ⊢ f\{A\} : T′_{n} \end{aligned}

Case ( β -overload2.)

\begin{aligned}I & {⋮ . Π(j < n) \atop A_{j} = min_{i=1,...,n}\{A_{i} | Γ ⊢ A ≤ A_{i}\}} & T_{j}[X := A] ≡⟩ T′_{j} \\ & Γ ⊢ (e&f)[A] : T′_{n} \end{aligned}

where I is

{⋮ . Σ_{1} \atop Γ ⊢ e : ∀X\{A_{i}.T_{i}\}_{i=1,...n−1}}  {⋮ . Σ_{2} \atop Γ ⊢ f : ∀X≤A_{n}.T_{n}}  {⋮ . Π_{1} \atop Γ ⊢ ∀X.\{A_{i}.T_{i}\}_{i=1,...,n} type}
Γ ⊢ e&f : ∀X.{A_{i}.T_{i}}_{i=1,...,n}

⇓

{⋮ . Σ_{1} \atop Γ ⊢ e : ∀X\{A_{i}.T_{i}\}_{i=1,...n−1}}  {⋮ . Π(j ≤ n − 1) \atop A_{j} = min_{i=1,...,n−1}\{A_{i} | Γ ⊢ A ≤ A_{i}\}} T_{j}[X := A] ≡⟩ T′_{j}
Γ ⊢ e[A] : T′_{j}

2. (Church-Rosser) Use parallel reduction as in Chapter 3 and 4. What to take care of is the reduction ( β -overload). Consider a rule the parallel reduction derived from ( β -overload1) and ( β - overload2):

\{ \begin{matrix}A is closed.  e > e′  f > f′ \\ Γ ⊢ e : ∀X.\{A_{i}.T_{i}\}_{i=1,...,n−1}  Γ ⊢ f : ∀Y ≤A_{n}.T_{n} \\ n = max\{h | A_{h} = min_{i=1,...,n}\{A_{i} | Γ ⊢ A ≤ A_{i}\}\} \end{matrix}
Γ ⊢ (e&f)[A] > f′{A}

(PRβ-overload1)

\{ \begin{matrix}A is closed.  e > e′  f > f′ \\ Γ ⊢ e : ∀X.\{A_{i}.T_{i}\}_{i=1,...,n−1}  Γ ⊢ f : ∀Y ≤A_{n}.T_{n} \\ n ≠ max\{h | A_{h} = min_{i=1,...,n}\{A_{i} | Γ ⊢ A ≤ A_{i}\}\} \end{matrix}
Γ ⊢ (e&f)[A] > e′[A]

(PRβ-overload2)

However, because A is closed, such m in (PR β -overload1) and (PR β -overload2) need to be fixed, the Church-Rosser of cF_{≤}^{&}+ is easily proved by parallel reduction.

5.5 Example of Applications to Object-Oriented Lan-

guages

We discuss about the re-usability of programs in cF_{≤}^{&}+ and the relation between object-oriented languages and cF_{≤}^{&}+ more deeply.

Example 5.5.1.

Classes are subset of a set of all objects, and, because, in this framework, we place objects and terms in the same category, we can regard classes as types. Then a message is (an identifier of) a overloaded function whose branches are the methods associated to that message. The methods to be executed are selected according to the type (the class-name) passed as an argument.

We will provide an example, and, in this section, we assume that there is no type variable, i.e., the environment is ϕ (empty).

Let these types defined as follows using record types:

point1D  = [x:Int]
point2D  = [x:Int ; y:Int]
point3D  = [x:Int ; y:Int ; z:Int]
color  = [c:Str]
(point1D+color) = [x:Int ; c:Str]
(point2D+color) = [x:Int ; y:Int ; c:Str]
(point3D+color) = [x:Int ; y:Int ; z:Int ; c:Str]

From these definitions, for example, ⊢ point3D ≤ point2D , and ⊢ (point1D+color) ≤ point1D hold. We can define a message Norm working on these types

Norm ≡ (ΛMytype ≤ point1D.λself Mytype. max{(self |point1D).x} &(ΛMytype ≤ point2D.λself Mytype. max{self |point2D).x, (self |point2D).y} &(ΛMytype ≤ point3D.λself Mytype. max{(self |point3D).x, (self |point3D).y, (self |point3D).z} .

The type of this message is

S = ∀Mytype.{point1D.[Mytype → Int], point2D.[Mytype → Int], point3D.[Mytype → Int]} .

We have used the variable self to denote the receiver of the message, and, following the notation of [Bru92], the type variable Mytype to denote the type of the receiver.

In the next example, we consider the type which includes type instantiation about overloaded type.

Example 5.5.2.

e = ΛX≤(∀Z.{[l_{1}:Int].Z → Int}).λx^{X}.ΛY ≤[l_{1}:Int].λy^{Y} .x{Y }y

is a function which applies an ad-hoc polymorphic function to an argument and its type is derived as follows:

I

Y ∈ FV(Γ) ; Γ ⊢ Y type
Γ ⊢ y^{Y} : Y Γ^{∗}(Inst(X, Y)) ≡ Y → Int

Y ∈ FV(Γ) ; Γ ⊢ Y type
Γ ⊢ Y ≤ Y
Γ ⊢ x^{X}{Y }y^{Y} : Range(Inst(X, Y))
Γ ⊢ λy^{Y} .x^{X}{Y }y : Y → Range(Inst(X, Y))
\{ \begin{matrix}X≤(∀Z.\{[l_{1}:Int].Z → Int\}) ⊢ ΛY ≤[l_{1}:Int].λy^{Y} .x^{X}\{Y \}y \\ : ∀Y ≤[l_{1} : Int].Y → Range(Inst(X, Y)) \end{matrix}
\{ \begin{matrix}X≤(∀Z.\{[l_{1}:Int].Z → Int\}) ⊢ λx^{X}.ΛY ≤[l_{1}:Int].λy^{Y} .x\{Y \}y \\ : X → (∀Y ≤[l_{1} : Int].Y → Range(Inst(X, Y))) \end{matrix}
\{ \begin{matrix}⊢ ΛX≤(∀Z.\{[l_{1}:Int].Z → Int\}).λx^{X}.ΛY ≤[l_{1}:Int].λy^{Y} .x\{Y \}y \\ : ∀X≤(∀Z.\{[l_{1}:Int].Z → Int\}).X → (∀Y ≤[l_{1} : Int].Y → Range(Inst(X, Y))) \end{matrix}

where I is

X ∈ FV(Γ) ; Γ ⊢ X type
Γ ⊢ x^{X}

Γ^{∗}(X) ≡ (∀Z.{[l_{1}:Int].Z → Int})

(Y ≤[l_{1}:Int]) ∈ Γ
Γ ⊢ Y ≤[l_{1}:Int]

Γ ⊢ Inst(X, Y) type

Γ ⊢ x^{X}{Y } : Inst(X, Y)

In the proof tree above, we write

Γ ≡ X≤(∀Z.{[l_{1}:Int].Z → Int}), Y ≤ [l_{1}:Int].

When e is applied to a type S and Norm of the type S in Example 5.5.1, f = e{S}Norm has the type ∀Mytype≤[l_{1}:Int].Mytype → Int because, under an environment Mytype ≤ [l_{1}:Int] , Range(Inst(S, Mytype)) is reduced to Range(Mytype → Int) and moreover, to Int .

5.6 Conclusion

In this section, by extending cF_{≤}^{+} , we proposed the calculus cF_{≤}^{&}+ integrating symbiosis of parametric polymorphism and a kind of ad-hoc polymorphism and satisfying the property of unicity of type^{3}. We also proved that it satisfies the properties of Subject Reduction and Church-Rosser, and provided its applications to object-oriented languages. However, the facility of ad-hoc polymorphism in cF_{≤}^{&}+ is strictly restricted, and We will have to relax this restriction. The directions of this relaxation will be discussed in Chapter 6.

3We think that cF_{≤}^{&}+ is the first calculus that satisfies unicity of type and Subject reduction and that integrates the two kinds of polymorphisms.

Conclusion

6.1 Conclusion

In this thesis, by modifying and extending F_{≤} , [Ghe90], we first introduced new calculi cF_{≤}^{+} and cF_{≤}^{++} , where, for each term expression, its type is uniquely determined and its information is lost only at the coercion operator. In Chapter 3, we introduced the calculus cF_{≤}^{+} , which is a second order λ -calculus with records, coercion operator and bounded quantification including new types Range(X) and Sel(X, l) . For a type Range(X) , function types may be substituted for X and when a function type S → U is substituted for X , Range(S → U) is reduced to the type U . For a type Sel(X, l) , record types which include field of label l will be substituted for X and when a record type […, l:T, …] is substituted for X , Sel([…, l:T, …], l) is reduced to T . We also proved that cF_{≤}^{+} has good properties (unicity of type, Subject Reduction, Church-Rosser, and Strong Normalization) and showed some applications of cF_{≤}^{+} to object-oriented languages.

In Chapter 4, we proposed the calculus cF_{≤}^{++} by adding the type Inst(X, U) . For a type Inst(X, U) , bounded universal types may be substituted for X and when a universal type ∀Y ≤S.T is substituted for X , Inst(∀Y ≤S.T, U) is reduced to T [X := U] . We called this reduction the type instantiation and proved its termination. We also showed that cF_{≤}^{++} satisfies Subject Reduction and Church-Rosser.

By improving F_{≤}^{&} , we also provided a calculus cF_{≤}^{&}+ based on cF_{≤}^{+} which realizes symbiosis of parametric polymorphism and ad-hoc polymorphism in Chapter 5. It also satisfies good properties such as Subject Reduction and Church-Rosser. In addition, we proposed their applications to object-oriented languages.

6.2 Future Work

We think that the techniques described in this thesis can be applied to calculi integrating intersection types [Pie91, Pie93] and calculi including recursive types and subtyping [CCHMO89]. We also need think how we modify the rules of cF_{≤}^{+} so that some decidable type checking algorithms exist as in the case of F_{≤} [Pie92, KS92, CP94]. We also plan to study the interaction between parametricity and subtyping in the system cF_{≤}^{++} as in [PAC93], for example, by modelling fibration in category theory [Pho92].

The main future work of this thesis is to construct the general framework of calculi which integrate parametric and ad-hoc polymorphisms by extending the notions given in this thesis. There will be two ways to do it. The first way is to extend the notion of Kind introduced in Chapter 4 such that every kind can include types as in [PT93a] to categorize the type of ad-hoc polymorphic functions. Because, if a calculus included the rule of coercion operator, not the subsumption rule, many terms could not type-check in it, most of calculi integrating parametric and ad-hoc polymorphism include the subsumption rule, not the coercion operator. Therefore they cannot satisfy the property of unicity of type. By using the technique in this thesis, we may be able to overcome the problem (see Section 1.3). The second way is to distinguish equations for ordinary expressions and equations for whole programs as in Plotkin’s λv -calculus [Plo75]. Without this kind of distinction, we must restrict ad-hoc polymorphic functions to satisfy Subject Reduction and Church-Rosser property in the framework of second-order λ -calculi. So we must consider the evaluation context to relax the restrictions on ad-hoc polymorphism. We will try extending the cF_{≤}^{++} to integrate two kinds of polymorphisms, where ad-hoc polymorphic functions will be implemented by overloading [CGL92, Tsu94], merge operator [Tsu92, Tsu93, Tsu94a], or generalizations of extensible records [Car92].

Bibliography

[AM87] Appel, A. W., and D. B. MacQueen. A Standard ML compiler. In Functional Programming Languages and Computer Architecture, Lecture Notes in Computer Science 274, pp. 301–324, 1987.

[AM91] Appel, A. W., and D. B. MacQueen. Standard ML of New Jersey. In Third Inter. Symp. on Prog. Lang. Implementation and Logic Programming, Springer-Verlag, 1991.

[Bar84] Barendregt, H. P., The Lambda Calculus — Its Syntax and Semantics. North Holland, 1984. Revised edition.

[Blo90] Bloom, B., Can LCF be topped?, flat lattice models of typed λ -calculus. Information and Computation, Vol. 87, pp. 264-301, 1990.

[Bru92] Bruce, K. B., A paradigmatic object-oriented programming language: Design, static typing and semantics. Technical Report CS-92-01, Williams College, 1992.

[Bru93] Bruce, K. B., Safe type checking in a statically typed object-oriented language. In Proc., ACM Conference on Principles of Programming Languages, 1993.

[BDGKK88] Bobrow, D., L. DiMichel, R. Gabriel, S Keene, et al., Common lisp object system specification: X3j13 document 88-002r. SIGPLAN Notices, vol. 87, pp. 264–301.

[BTGS90] Breazu-Tannen, C., A Gunter, and A. Scedrov, Computing with coercions. In Proceedings, ACM Conference on Lisp and Functional Programming, pp. 44–59, 1990.

[BTGS91] Breazu-Tannen, C., A Gunter, and A. Scedrov, Inheritance as implicit coercion. Information and Computation, Vol 93, pp. 172–221, 1991.

[Car88] Cardelli, L., A semantics of multiple inheritance. Information and Computation, vol. 76, pp. 148–164, 1988.

[Car92] Cardelli, L., Extensible records in a pure calculus of subtyping, Research report 81, DEC Systems Research Center, 1992. Also in [GM93].

[Cas93] Castagna, G., F_{≤}^{&} : integrating parametric and “ad hoc” second order polymorphism, Proc., the 4th International Workshop on Database Programming Languages, 1993. Full version titled ‘Integration of parametric and “ad hoc” second order polymorphism in a calculus with subtyping’ is submitted.

[Cas93a] Castagna, G., Surcharge, Sour-Typage et Liaison Tardive: Fondements Fonctionnels de la Programmation Orientée Objects (in English). Thèse d’Informatique, Université Paris VII, 1993.

[CCHMO89] Canning, P., W. Cook, W. Vool, W. Hill, J. C. Mitchell, and W. Olthoff, F-bounded quantification for object-oriented programming, in Functional Programming and Computer Architecture, pp. 273–280, 1989.

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

[CG93] Curien, P. L., and G. Ghelli, Confluence and decidability of βηtop ≤ reduction in F_{≤} . Information and Computation, To appear.

[CGL92] Castagna, G.,G. Ghelli, and G. Longo, A calculus for overloaded functions with subtyping,Proc., ACM Conference on Lisp and Functional Programming, pp. 182–192,1992. Full version will appear in Information and Computation.

[CGL93] Castagna, G.,G. Ghelli, and G. Longo, A semantics for λ& -early: a calculus with overloading and early binding. In International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, 664, 1993.

[CMMS91] Cardelli, L., S. Martini, J. C. Mitchell, and A. Scedrov, An extension of system F with subtyping, in Theoretical Aspects of Computer Software, Lecture Notes on Computer Science, 526, 1991.

[CP94] Castagna, G., and B. Pierce, Decidable Bounded Quantification, To appear in Proc., ACM Conference on Principles of Programming Languages, 1994.

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

[DG87] DeMichiel, L. G., and R. P. Gabriel. Common lisp object system overview. Proc., European Conference on Object Oriented Programming, 1987.

[Gal90] Gallier, J. H., On Girard’s “Candidates de Reductibilité”, in P. Odifreddi ed., Logic and Computer Science, Academic Press, pp. 123–204, 1990

[Ghe90] Ghelli, G., Proof Theoretic Studies about a Minimal Type System Integrating Inclusion and Parametric Polymorphism, PhD Thesis, Dipartimento di Informatica, Università di Pisa, 1990. Tech. Rep. TD-6/90.

[Ghe91] Ghelli, G., A static type system for message passing. In Proc. of Object Oriented Programming, System, and Application ’91, 1991.

[Ghe93] Ghelli, G., Termination of system F -bounded, Manuscript, 1993.

[Gir72] Girard, J. Y., Interprétation Fonctionnelle et Élimination des Coupures de L’arithmétique D’ordre Supérieur. Thèse d’Etat, Université Paris VII (1972).

[GLT89] Girard, J. Y., Y. Lafont, and P. Taylor. Proof and Types. Cambridge University Press, 1989.

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

[Has90] Hasegawa, R., Categorical Data Types in Parametric Polymorphism. Mathematical Structures in Computer Science. To appear.

[Has91] Hasegawa, R., Parametricity of extensionally collapsed term models of polymorphism and their categorical properties, in Theoretical Aspects of Computer Software. Lecture Notes in Computer Science 526, pp.495–512. 1991.

[HW90] Hudak, P., and P. Wadler (ed.) Report on the Programming Language Haskell, 1990.

[KLM94] Katiyar, D., D. Luckham, and J. C. Mitchell, A type system for prototyping languages. In Proc., ACM Conference on Principles of Programming Languages, 1994.

[KS92] Katiyar, D., and S. Sankar, Completely bounded quantification is decidable. In Proc., ACM Workshop on ML and its applications, pp. 68–77, 1992.

[Mil77] Milner, R., Fully abstract models of typed λ -calculus. Theoretical Computer Science, Vol. 4, pp. 1–22, 1977.

[Mit90] Mitchell, J. C., Towards a typed foundation for method specialization and inheritance. In Proc., ACM Conference on Principles of Programming Languages, 1990.

[MR91] Ma, Q. M., and J. C. Reynolds, Types, Abstraction, and Parametric Polymorphism, Part 2, in Proc. of the Mathematical Foundations of Programming Semantics Conference. Lecture Notes in Computer Science, 1991.

[OB88] Ohori, A., and P. Buneman, Static type inference for parametric classes, ACM conference on Object Oriented Programming Systems,Languages, and Applications, pp. 445–455, 1989.

[OBBT89] Ohori, A., P. Buneman, and V. Breazu- Tannen, Database programming in Machiavelli — a polymorphic language with static type inference. Proc. of ACM SIGMOD Conference, pp. 46–67, Portlang, Oregon, 1989.

[Pho92] Phoa, W., Using fibration to understand subtypes. In Applications of Categories in Computer Science, vol. 177 of L.M.S., pp. 239–254, 1992.

[Pie91] Pierce, B., Programming with Intersection Types and Bounded Polymorphism. PhD. Thesis, Computer Science, CMU, 1991, Available as School of Computer Science tech. rep. CMU-CS-91-205.

[Pie92] Pierce, B., Bounded quantification is undecidable, In Proc., ACM Conference on Principles of Programming Languages, 1992.

[Pie93] Pierce, B., Intersection Types and Bounded Polymorphism, In International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, 664, 1993.

[Plo75] Plotkin, G., Call-by-name, call-by-value, and the λ -calculus. Theoretical Computer Science, vol. 1., pp. 125–157, 1975.

[Plo77] Plotkin, G., LCF considered as a programming language. Theoretical Computer Science, vol. 5., pp. 223-255, 1977.

[PAC93] Plotkin, G., M. Abadi, and L. Cardelli, Subtyping and Parametricity. 1993.

[PT93] Pierce, B., and D. N. Turner, Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming. To appear.

[PT93a] Pierce, B., and D. N. Turner, Statically Typed Friendly Functions via Partially Abstract Types. University of Edinburgh technical report ECS-LFCS-93-256 and INRIA-Rocquencourt Rapport de Recherche No. 1899., 1993.

[Rey74] Reynolds, J. C., Towards a theory of type structures. Lecture Notes in Computer Science, 19, pp. 408–425, 1974.

[Rey83] Reynolds, J. C., Types, abstraction, and parametric polymorphism., In Information Processing 83, pp. 513–523, 1983.

[Str67] Strachey, C., Fundamental concepts in programming languages, Lecture notes for International Summer School in Computer Programming, Copenhagen, 1967.

[Str88] Stroustrup, B., The C++ Programming Language, Addison-Wesley, Reading, Mass., 1988.

[Tai75] Tait, W. W., A realizability interpretation of the theory of species, In Logic Colloquium, Lecture Notes in Computer Science No. 453, pp. 240–251, 1975.

[Tak89] Takahashi, M., Parallel reductions in λ -calculus. Journal of Symbolic Computation, Vol. 7, pp. 113-123, 1989.

[Tak92] Takahashi, M. H., Parallel reductions in λ -calculus. Tech. Rept. C-103, Tokyo Institute of Technology (Revised version of [Tak89]).

[Tsu92] Tsuiki, H., A Record Calculus with a Merge Operator. PhD Thesis, Keio University, 1992.

[Tsu93] Tsuiki, H., A record calculus with a merge operator (in Japanese). Journal of Information Processing Society, vol. 34, No. 5, pp. 954–962, 1993.

[Tsu94] Tsuiki, H. A normalizing calculus with subtyping and overloading. To appear in Theoretical Aspects of Computer Software 94, 1994.

[Tsu94a] Tsuiki, H. A calculus of parametric generic functions. Manuscript, 1994.

[WB89] Wadler, P., and S. Blott. How to make “ad-hoc” polymorphism less “ad-hoc”. In Proc., ACM Conference on Principles of Programming Languages,pp. 60–76, 1989.

[Wan89] Wand, M., Type inference for record concatenation and multiple inheritance, Proc, Fourth IEEE Annal Symposium on Logic in Computer Science, pp. 92–97, 1989.