A Compilation Method for ML-Style Polymorphic Record Calculi^{∗}

Atsushi Ohori

Oki Electric Industry, Kansai Laboratory Crystal Tower, 1-2-27 Shiromi Chuo-ku, Osaka 540 Japan

email: ohori@kansai.oki.co.jp

Abstract

Polymorphic record calculi have recently attracted much attention as a typed foundation for objectoriented programming. This is based on the fact that a function that selects a field l of a record can be given a polymorphic type that enables it to be applied to various records containing a field l. Recent studies have established techniques to develop an ML-style type inference algorithm for such a polymorphic type system. There seems to be, however, no established method to compile an ML-style polymorphic record calculus into efficient code. The purpose of this paper is to present one such method. We define a polymorphic record calculus as an extension of Damas and Milner’s proof system for ML. For this calculus, we define an implementation calculus where records are represented as arrays of (references to) values and field selection is performed by direct indexing. To represent polymorphic field selection, the implementation calculus contains an abstraction mechanism over indexes. We then develop an algorithm to translate the polymorphic record calculus into the implementation calculus by refining a type inference algorithm; it simultaneously computes a principal type scheme in the polymorphic record calculus and a correct implementation term in the implementation calculus. The type inference is shown to be sound and complete in the sense of Damas-Milner’s algorithm for ML. Moreover, the polymorphic type system is shown to be sound with respect to an operational semantics of the translated terms in the implementation calculus.

1 Introduction

The investigation of a polymorphic type discipline for labeled records was initiated by Cardelli [Car88], who defined a typed functional calculus with records and showed that certain aspects of method inheritance can be represented in a static type system. This is based on the observation that a subtype relation can be used to capture the polymorphic nature of functions involving field selection such as

function wealthy(x : {Name : string, Salary : int}) = x·Salary > 100000

where x·Salary selects the Salary field from a record. This function can be applied to all the subtypes of {Name : string, Salary : int}, i.e. those record types that may contain more fields. [CW85] extended this calculus to a second-order type system by combining the subtyping and the type system of the second-order lambda calculus [Gir71, Rey74]. A similar idea was presented in [Mit84]. More powerful second-order calculi for records were proposed in [CM89, HP91].

Wand [Wan87, Wan88] observed that the above form of method inheritance can properly be represented in an ML style polymorphic type system when it is extended to records (and variants). This idea was further developed in a number of type inference systems [Sta88, JM88, OB88, Rém89, Wan89, Rém90] that include a combination of type inference and data abstraction with multiple inheritance [OB89]. In these type systems, a most general polymorphic type scheme is inferred for any typable untyped term containing operations on records. By appropriate instantiation of the inferred type scheme, an untyped term can safely be used as values of various types. This approach not only captures the polymorphic nature of functions on records but also integrates a record calculus and ML-style type inference, which relieves the programmer from complicated type declarations required in explicit second-order calculi. We therefore hope that this approach will provide a basis for designing practical programming languages for object-oriented programming and other data intensive applications, such as database programming [AB87], for which records are an essential data structure.

∗Appeared in Proc. ACM POPL Symposium, pages 154–165, 1992 (a few minor errors corrected.)

To implement a practical programming language embodying such a polymorphic type inference system, we need to develop a method to compile (typable) untyped polymorphic expressions involving operations on records into efficient code. In this paper, we attempt to provide one such method. As a first step, we only consider field selection and field modification (update) as operations on records. They are the basis of all record calculi so far proposed, and are also the operations commonly found in conventional programming languages. We hope that the method presented here can be extended to various other operations on records such as those to extend a record with an additional field [Wan87, JM88, Rém89, CM89, Rém90], various forms of record concatenation [Wan89, HP91, Rém91] and join [OB88]. We will comment on this issue in Section 6.

For a language with a simple type system, compiling field selection into efficient code is a standard practice that is routinely carried out by a compiler. This is due to the fact that exact type information on parameters is available when compiling a function operating on records. In a polymorphic type system, however, generating efficient code for field selection is far from trivial. Since types of actual parameters may differ, the position (or offset) of a field within a record passed as a parameter cannot be statically computed when compiling the body of a function operating on records. One naive approach is to implement directly the intended semantics of field selection and field modification by dynamically searching for the required label in a record represented as an association list of labels and values. An obvious drawback to such an approach is inefficiency in run-time execution. Since field selection is a basic operation that is frequently invoked, such a method is unacceptable for serious practical applications. Another approach might be to predetermine the offsets of all the possible labels and to represent a record as a potentially very large structure with many empty slots. A recent work by Cardelli [Car91] used this approach to represent records in a pure calculus of subtyping. While this approach is useful for studying formal properties of record polymorphism, it is unrealistic in practice.

For a polymorphic record calculus to become a basis of practical programming languages, we must develop a compilation method that achieves both compactness in representation of records and efficiency in execution of field selection and field modification. Connar, Deale, Morrisoan and Brown [CDMB89] considered this problem in the context of an explicitly typed language with subtyping and suggested a solution. However, they did not establish a systematic method to deal with arbitrary expressions, nor did they consider a type inference system. To the author’s knowledge, there has been no proposal that establishes a method to compile an ML-style implicitly typed polymorphic language with records into efficient code. The purpose of this paper is to present such a compilation method and to establish that the compilation achieves the intended operational behavior of a polymorphic record calculus. This requires a formulation of type inference for records with ML’s let binding and a precise definition of “efficient implementation” for a record calculus.

Our strategy is to translate a polymorphic record calculus into an implementation calculus, where a record is represented as an array of (references to) values and field selection and field modification are performed by direct indexing. To deal with polymorphic field selection, the implementation calculus contains index variables and index abstraction. For example, from the untyped term of the form

let wealthy = λx. x·Salary > 100000

in ⋯ (wealthy R) ⋯ end

the translation algorithm produces the following implementation code:

let wealthy = λIλx. x[I] > 100000 in ⋯ ((wealthy I) R) ⋯ end

where I is an index variable, λI. M is index abstraction, x[I] is an index expression and (wealthy I) is index application with an appropriate index value I. This method was suggested in [CDMB89]. The major technical contribution of the present paper is to establish an inference algorithm that always constructs a correct implementation term for any type correct raw term of a polymorphic record calculus and to prove that the polymorphic type discipline is sound with respect to the translation. We achieve this by refining a polymorphic type inference algorithm for a record calculus.

In Section 2 we define a polymorphic record calculus λ^{let,·} with field selection and field modification operations. Here we refine the mechanism of conditional type schemes that we proposed in [OB88] as kinded type schemes. This refinement allows us to extend a number of known formal properties of ML polymorphism to record structures. Examples include Damas and Milner’s formal account [DM82] for let polymorphism and Mitchell and Harper’s analysis [MH88] on ML polymorphism. Section 3 defines an implementation calculus λ^{let,[ ]}. In order to establish the soundness of the compilation algorithm, we present the calculus as a typed functional calculus and prove the soundness of the type system with respect to an operational semantics. In Section 4 we simultaneously develop a type inference algorithm for λ^{let,·} and a compilation algorithm from λ^{let,·} to λ^{let,[ ]}. We then establish that the compilation algorithm preserves typings. This result, together with the soundness of the type system of λ^{let,[ ]}, establishes the soundness of the polymorphic type system of λ^{let,·} with respect to the semantics achieved by the compilation.

In our calculus, the polymorphic nature of field selection is obtained not by subtyping but by polymorphic instantiation of type schemes. Since the same problem arises in compiling a language with subtyping, it would be nice if we could also develop a similar compilation algorithm for record calculi based on subtyping. However, there exists some difficulty that seems to be inherent in calculi with subtyping. We will discuss this issue in Section 5.

2 The Record Calculus λ^{let, ·}

The set of raw terms (ranged over by e) of λ^{let,·} is given by the syntax:

e ::= c^{τ} | x | λx. e | e e | {l = e, …, l = e} | e·l | modify(e, l, e) | let x = e in e end

where c^{τ} stands for constants of type τ. For the simplicity of presentation we assume that τ in c^{τ} is a ground type not containing any type variables. It is not hard to extend our formal development to constants having a polymorphic type. {l_{1} = e_{1}, …, l_{n} = e_{n}} is the syntax for labeled records where l_{1}, …, l_{n} are pairwise distinct labels and the order of their appearance is insignificant. e·l is field selection and modify(e_{1}, l, e_{2}) is field modification, which creates a new record from e_{1} by changing the value of the l field to e_{2}. let x = e in e end is ML’s let construct.

Following Damas and Milner’s formal account [DM82] for let polymorphism, the set of types is divided into the set of monotypes and the set of polytypes. The set of monotypes (ranged over by τ) is given by the syntax:

τ ::= t | b | τ → τ | {l : τ, …, l : τ}

where t stands for type variables and b for base types. To represent polymorphic field selection, we need to refine type quantification in Damas-Milner polytypes. Instead of using row variables [Wan87], we use kinded type quantification of the form ∀t :: k. τ, which denotes quantification over the subset of monotypes represented by the kind k. This is a refinement of conditional type schemes we proposed in [OB88], and is also similar to bounded quantification [CW85]. It should be noted, however, that we do not use any notion of subtyping. The set of polytypes (ranged over by σ) and the set of kinds (ranged over by k) are given as:

σ ::= τ | ∀t::k. σ k ::= U | ⟨l : τ, …, l : τ⟩ U denotes the set of all monotypes and ⟨l_{1} : τ_{1}, …, l_{n} : τ_{n}⟩ is a record kind intuitively denoting the subset of monotypes that are record types containing the fields l_{1} : τ_{1}, …, l_{n} : τ_{n}.

In our calculus, every type variable must be kinded by a kind assignment K, which is a function from a finite set of type variables to kinds. A monotype τ has a kind k under a kind assignment K, denoted by K ⊢ τ :: k, if it is derivable by the following set of kinding rules:

K ⊢ τ :: U for all τ
K ⊢ t :: ⟨l_{1} : τ_{1}, …, l_{n} : τ_{n}⟩

if t ∈ dom(K), K(t) = ⟨l_{1} : τ_{1}, …, l_{n} : τ_{n}, …⟩ K ⊢ {l_{1} : τ_{1}, …, l_{n} : τ_{n}, …} :: ⟨l_{1} : τ_{1}, …, l_{n} : τ_{n}⟩

Let T be a type assignment, which is a function from a finite set of variables to polytypes. Typing judgments in our calculus are formulae of the form K, T ⊢ e : σ such that all free type variables in T and σ are contained in the domain of K. For a function f, we write f{x ↦ v} for the function f′ such that dom(f′) = dom(f) ∪ {x}, f′(x) = v and f′(y) = f(y) for all y ∈ dom(f), y ≠ x. We also write σ[τ/t] for the type obtained from σ by substituting all the free occurrences of t with τ. Figure 1 gives the set of typing rules for λ^{let,·}. Note that kindings in rules dot and modify represent the exact conditions on record types. This allows us to integrate these rules with those for let construct (rules gen and inst). Since let construct is the source of ML polymorphism, this formal treatment is essential to develop a systematic compilation method.

2.1 Properties of λ^{let,·}

The above treatment of let binding in our proof system allows us to analyze various formal properties of let polymorphism with records. Indeed, most of the known results of ML polymorphism seems to extend to our calculus. Examples include Mitchell and Harper’s analysis [MH88] of Damas and Milner’s proof system for ML through a limited form of explicit calculus called XML. The explicit calculus corresponding to our calculus is defined by changing the term e in the conclusion of the rules abs, gen, inst and let to λx : τ_{1}. e_{1}, λt:: k. e, e τ and let x : σ = e_{1} in e_{2} end, respectively. Let E be an explicitly typed term and erase(E) be the raw term obtained from E by erasing type specification, type abstraction and type application. We can show the following property, which is an extension of a result shown in [MH88].

Proposition 1 If K, T ⊢ E : σ is a typing in the explicit calculus, then K, T ⊢ erase(E) : σ is a typing in λ^{let,·}. Conversely, if K, T ⊢ e : σ is a typing in

const K, T ⊢ c^{τ} : τ
var  K, T ⊢ x : σ  if x ∈ dom(T ), T (x) = σ
abs  \frac{K, T \{x ↦ τ_{1}\} ⊢ e_{1} : τ_{2}}{K, T ⊢ λx. e_{1} : τ_{1} → τ_{2}}
app  \frac{K, T ⊢ e_{1} : τ_{1} → τ_{2} K, T ⊢ e_{2} : τ_{1}}{K, T ⊢ e_{1} e_{2} : τ_{2}}
record  \frac{K, T ⊢ e_{i} : τ_{i} (1 ≤ i ≤ n)}{K, T ⊢ \{l_{1} = e_{1}, …, l_{n} = e_{n}\} : \{l : τ_{1}, …, l_{n} : τ_{n}\}}
dot  \frac{K, T ⊢ e : τ_{1} K ⊢ τ_{1} :: ⟨l : τ_{2}⟩}{K, T ⊢ e·l : τ_{2}}
modify  \frac{K, T ⊢ e_{1} : τ_{1} K, T ⊢ e_{2} : τ_{2} K ⊢ τ_{1} :: ⟨l : τ_{2}⟩}{K, T ⊢ modify(e_{1}, l, e_{2}) : τ_{1}}
gen  \frac{K\{t ↦ k\}, T ⊢ e : σ}{K, T ⊢ e : ∀t::k. σ}  t not free in T
inst  \frac{K, T ⊢ e : ∀t::k. σ K ⊢ τ :: k}{K, T ⊢ e : σ[τ/t]}
let  \frac{K, T ⊢ e_{1} : σ K, T \{x ↦ σ\} ⊢ e_{2} : τ}{K, T ⊢ let x = e_{1} in e_{2} end : τ}

Figure 1: Typing rules of the polymorphic record calculus

λ^{let,·}, then there is an explicitly typed term E such that erase(E) = e and K, T ⊢ E : σ is a typing in the explicit calculus.

This result allows us to transfer various analyses presented in [MH88] to our calculus.

Rémy’s recent work [Rém90] also provide a formal treatment of let and unbounded labeled records. It seems to be fairly obvious that other proposals for type inference systems of (unbounded) labeled records [Wan87, Sta88, JM88, Wan89] can deal with let binding by properly renaming types and row variables. It is, however, not immediately obvious that various formal properties underlying let polymorphism such as above can be extended to those proposals.

2.2 An alternative proof system of λ^{let,·}

The existence of polytypes in the presentation of λ^{let,·}, however, complicates the presentation of a type inference algorithm and a compilation algorithm we shall develop below. Fortunately there is a simpler proof system that is equivalent to λ^{let,·}. This is based on simpler accounts for let polymorphism presented in [Oho89a, Mit90]. The simpler proof system is obtained by (1) restricting the set of types to be monotypes, (2) removing the rules gen and inst, and (3) replacing the rule let with the following rule:

let’  \frac{K, T ⊢ e_{1} : τ_{1} K, T ⊢ e_{2}[e_{1}/x] : τ_{2}}{K, T ⊢ let x = e_{1} in e_{2} end : τ_{2}}

where τ_{1} may be any monotype and the notation e_{2}[e_{1}/x] denotes the term obtained from e_{2} by substituting all the free occurrences of x in e_{2} by e_{1} with necessary bound variable renaming.

Since e_{2}[e_{1}/x] in the above rule is not a subterm of let x = e_{1} in e_{2} end, some care must be taken in proving various properties of this proof system. In particular, we cannot use induction on the size of raw terms. We can, however, define a complexity measure of raw terms in such a way that, in any rule in this proof system, the complexity of the raw term in the conclusion is strictly greater than those of the raw terms in its premises. Based on this, we can prove properties of this proof system by usual case analysis in terms of the structure of raw terms. Here we omit a rather lengthy definition of the complexity measure of raw terms. One definition can be found in [Oho89b]. For closed raw terms, this proof system is equivalent

to the original one.

Proposition 2 Let e be a closed raw term. It has a typing in λ^{let,·} if and only if it has a typing in the simpler proof system.

Another advantage of this simpler proof system is that it has a simple denotational semantics as exploited in [Oho89a].

We use this alternative proof system in what follows.

3 The Implementation Calculus λ^{let,[ ]}

This section defines a calculus λ^{let,[ ]} where field selection and field modification are executed efficiently. In order to establish the correctness of the compilation algorithm given in Section 4, we define λ^{let,[ ]} as a typed functional calculus and show the soundness of the type system in terms of an operational semantics.

We assume that there is a linear order ≤ on the set of labels and that a labeled record {l_{1} = v_{1}, …, l_{n} = v_{n}} is represented as an array of values such that the field l_{i} = v_{i} is the jth entry of the array where j is the size of the set {l|l ∈ {l_{1}, …, l_{n}}, l ≤ l_{i}}. Selecting the l_{i} field can then be performed by the simple indexing operation {l_{1} = v_{1}, …, l_{n} = v_{n}}[j]. In an actual implementation, records may be presented by references (or “pointers”) to values and field selection is implemented by indexing followed by de-referencing. In examples below, we use lexicographical ordering on strings for ≤. For example, Age ≤ Name and the record {Name = ”Joe”, Age = 21} is represented by an array of two entries whose first entry is Age = 21 and whose second entry is Name = ”Joe”. Selecting Name field from this record is performed by the index expression {Name = ”Joe”, Age = 21}[2].

Since the required index values are not always available when compiling field selection, we introduce index variables (ranged over by I) and an abstraction mechanism over indexes (ranged over by I). An index is either a natural number or an index variable. The set of raw terms (ranged over by M) of the implementation calculus is given as:

M ::= c^{τ} | x | λx. M | M M | {l = M, …, l = M} | M[I] | modify(M, I, M) | λI. M | M I | let x = M in M end

In order to assign a type to raw terms involving index variables, we introduce index types of the form index(l, τ) denoting the index value corresponding to field l in type τ. The set of types of the implementation calculus is given by the syntax:

τ ::= t | b | τ → τ | {l : τ, …, l : τ} | index(l, τ) ⇒ τ

where index(l, τ) ⇒ τ is a type of terms that are abstracted over indexes. The set of kinds and the kinding rules are the same as before. In order for index types of the form index(l, τ) to be meaningful, we require τ to have an appropriate record kind: an index type index(l, τ) is well formed under a kind assignment K if K ⊢ τ :: ⟨l, τ′⟩ for some τ′. This condition guarantees that an index type denotes a position of a field in a record type. In particular, a well formed ground index type (under any kind assignment) must be of the form index(l_{i}, {l_{1} : τ_{1}, …, l_{n} : τ_{n}}), l_{i} ∈ {l_{1}, …, l_{n}} and it denotes the natural number equal to the size of the set {l|l ∈ {l_{1}, …, l_{n}}, l ≤ l_{i}}.

Typings are presented relative to an index assignment (ranged over by L), which is a function from a finite set of index variables to index types. An index assignment L is well formed under a kind assignment K if all the index types appearing in L are well formed under K. An index value I has an index type index(l, τ) under an index assignment L, denoted by L ⊢ I : index(l, τ), if either I = I, L(I) = index(l, τ) or I is the natural number denoted by index(l, τ). Typing judgments in λ^{let,[ ]} are formulae of the form K, T , L ⊢ M : τ such that L is well formed under K. Figure 2 gives the typing rules of λ^{let,[ ]}.

3.1 Operational semantics and the soundness of the type system

To show the soundness of the type system, we define an operational semantics of λ^{let,[ ]} in the style of [Tof88] by giving a set of rules of the form

E, L ⊢ M ⟹ v

where v is a canonical value defined below, E is a variable environment, which is a function from a finite set of variables to values, and L is an index environment, which is a function from a finite set of index variables to natural numbers. The set of canonical values is given by the syntax:

v ::= c^{τ} | {l_{1} = v_{1}, …, l_{n} = v_{n}} | fun(E, L, x, M) | lab(E, L, I, M) | wrong

where {l_{1} = v_{1}, …, l_{n} = v_{n}} stands for canonical values for record expressions. For the purpose of pure evaluation, it is not necessary to keep record labels in canonical values of record expressions; however, they should be useful, for example, for a printing utility. fun(E, L, x, M) stands for function closures, lab(E, L, I, M) for closures corresponding to index abstraction and wrong represents run-time error. Figure 3 gives the set of reduction rules. Note that although the above rules suggest associative lookup for lambda variables and index variables, standard techniques for compiling programming languages can be used to determine the actual address (e.g. the offset to an activation record) of each variable.

A value v has a ground type τ, denoted by ⊧ v : τ, if it is derivable from the following set of rules:

• ⊧ c^{τ} : τ for any c^{τ}. const K, T , L ⊢ c^{τ} : τ var K, T , L ⊢ x : τ if x ∈ dom(T ), T (x) = τ

abs  \frac{K, T \{x ↦ τ_{1}\}, L ⊢ M_{1} : τ_{2}}{K, T , L ⊢ λx. M_{1} : τ_{1} → τ_{2}}
app  \frac{K, T , L ⊢ M_{1} : τ_{1} → τ_{2}  K, T , L ⊢ M_{2} : τ_{1}}{K, T , L ⊢ M_{1} M_{2} : τ_{2}}
record  \frac{K, T , L ⊢ M_{i} : τ_{i} (1 ≤ i ≤ n)}{K, T , L ⊢ \{l_{1} = M_{1}, …, l_{n} = M_{n}\} : \{l : τ_{1}, …, l_{n} : τ_{n}\}}
index  \frac{K, T , L ⊢ M : τ_{1}  K ⊢ τ_{1} :: ⟨l : τ_{2}⟩  L ⊢ I : index(l, τ_{1})}{K, T , L ⊢ M[I] : τ_{2}}
modify  \frac{K, T , L ⊢ M_{1} : τ_{1} K, T , L ⊢ M_{2} : τ_{2} K ⊢ τ_{1} :: ⟨l : τ_{2}⟩ L ⊢ I : index(l, τ_{1})}{K, T ⊢ modify(M_{1}, I, M_{2}) : τ_{1}}
iabs  \frac{K, T , L\{I ↦ index(l, τ_{1})\} ⊢ M : τ_{2}}{K, T , L ⊢ λI. M : index(l, τ_{1}) ⇒ τ_{2}}
iapp  \frac{K, T , L ⊢ M : index(l, τ_{1}) ⇒ τ_{2}  L ⊢ I : index(l, τ_{1})}{K, T , L ⊢ M I : τ_{2}}
let’  \frac{K, T , L ⊢ M_{1} : τ_{1}  K, T , L ⊢ M_{2}[M_{1}/x] : τ_{2}}{K, T , L ⊢ let x = M_{1} in M_{2} end : τ_{2}}

Figure 2: The typing rules of the implementation calculus

E, L ⊢ c^{τ} ⟹ c^{τ} E, L ⊢ x ⟹ v if x ∈ dom(E) and v = E(x) E, L ⊢ λx. M ⟹ fun(E, L, x, M)

\frac{E_{1}, L_{1} ⊢ M_{1} ⟹ fun(E_{2}, L_{2}, x, M_{2}) E_{1}, L_{1} ⊢ M_{3} ⟹ v_{1} E_{2}\{x ↦ v_{1}\}, L_{2} ⊢ M_{2} ⟹ v_{2}}{E_{1}, L_{1} ⊢ M_{1} M_{3} ⟹ v_{2}}

\frac{E, L ⊢ M_{i} ⟹ v_{i} (1 ≤ i ≤ n)}{E, L ⊢ \{l_{1} = M_{1}, …, l_{n} = M_{n}\} ⟹ \{l_{1} = v_{1}, …, l_{n} = v_{n}\}}

\frac{E, L ⊢ M ⟹ \{l_{1} = v_{1}, …, l_{n} = v_{n}\}}{E, L ⊢ M[I] ⟹ v_{i}} if I = i or I = I, L(I) = i (1 ≤ i ≤ n)

\frac{E, L ⊢ M_{1} ⟹ \{l_{1} = v_{1}, …, l_{n} = v_{n}\} E, L ⊢ M_{2} ⟹ v}{E, L ⊢ modify(M_{1}, I, M_{2}) ⟹ \{l_{1} = v_{1}, …, l_{i} = v, …, l_{n} = v_{n}\}} if I = i or I = I, L(I) = i

E, L ⊢ λI. M ⟹ lab(E, L, I, M)

\frac{E_{1}, L_{1} ⊢ M_{1} ⟹ lab(E_{2}, L_{2}, I, M_{2}) E_{2}, L_{2}\{I ↦ i\} ⊢ M_{2} ⟹ v_{2}}{E_{1}, L_{1} ⊢ M_{1} I ⟹ v_{2}} if I = i or I = I, L(I) = i

\frac{E_{1}, L_{1} ⊢ M_{1} ⟹ v_{1} E_{1}\{x ↦ v_{1}\}, L_{1} ⊢ M_{2} ⟹ v_{2}}{E_{1}, L_{1} ⊢ let x = M_{1} in M_{2} end ⟹ v_{2}}

Cases yielding wrong are omitted. Figure 3: Operational Semantics of the Implementation Calculus • ⊧ {l_{1} = v_{1}, …, l_{n} = v_{n}} : {l_{1} : τ_{1}, …, l_{n} : τ_{n}}

if ⊧ v_{i} : τ_{i} for all 1 ≤ i ≤ n.

• ⊧ fun(E, L, x, M) : τ_{1} → τ_{2} if ∀v, v′ if ⊧ v : τ_{1} and E{x ↦ v}, L ⊢ M ⟹ v′ then ⊧ v′ : τ_{2}.

• ⊧ lab(E, L, I, M) : α ⇒ τ if ∀v if E, L{I ↦ i} ⊢ M ⟹ v then ⊧ v : τ where i is the natural number denoted by α.

In the last rule, since α is a well formed ground index type, it always denotes a natural number. A substitution S is a function from type variables to types. We write [t_{1} ↦ τ_{1}, …, t_{n} ↦ τ_{n}] for the substitution S such that S(t_{i}) = τ_{i} (1 ≤ i ≤ n), S(t) = t (t ∉ {t_{1}, …, t_{n}}). A substitution extends to monotypes and other structures containing monotypes. We identify a substitution and its extension. The composition S_{1} ∘ S_{2} of two substitutions S_{1} and S_{2} is defined as S_{1} ∘ S_{2}(t) = S_{1}(S_{2}(t)). A substitution is ground if its range does not contain type variables. A ground substitution S respects a kind assignment K if, for all t ∈ dom(K), ∅ ⊢ S(t) :: S(K(t)) is a derivable kinding. A variable environment E respects a ground type assignment T if dom(T ) = dom(E) and for all x ∈ dom(E), ⊧ E(x) : T (x). An index environment respects a ground index assignment L if dom(L) = dom(L) and for all I ∈ dom(L), L(I) is the natural number denoted by L(I). We then have the following soundness theorem for λ^{let,[ ]}.

Theorem 1 If K, T , L ⊢ M : τ, then for any ground substitution S, if S respects K, E respects S(T ), L respects S(L) and E, L ⊢ M ⟹ v, then ⊧ v : τ.

Proof: It is easily checked that typings in λ^{let,[ ]} are preserved by kind respecting ground substitutions, i.e. if K, T , L ⊢ M : τ is a typing in λ^{let,[ ]} and S is a ground substitution that respects K, then ∅, S(T ), S(L) ⊢ M : S(τ) is also a typing. It is then enough to prove the property:

if ∅, T , L ⊢ M : τ is a ground typing, E respects T , L respects L and E, L ⊢ M ⟹ v, then ⊧ v : τ

To prove this property by induction, we use the operational semantics obtained from the one defined in Figure 3 by replacing the last rule for let expressions with the following rule:

\frac{E_{1}, L_{1} ⊢ M_{1} ⟹ v_{1} E_{1}, L_{1} ⊢ M_{2}[M_{1}/x] ⟹ v_{2}}{E_{1}, L_{1} ⊢ let x = M_{1} in M_{2} end ⟹ v_{2}}

It can be shown that the resulting operational semantics is equivalent to the original one. The desired property is then proved by induction on the complexity of raw terms we mentioned earlier. Proof proceeds by cases. The case for let follows from the induction hypothesis. Cases other than M[I], λI. M and M I are similar to the corresponding proof in [Tof88]. Here we only give the cases for λI. M and leave the cases for M[I] and M I to the reader.

Suppose ∅, T , L ⊢ λI. M : index(l, τ_{1}) ⇒ τ_{2}, E respects T , L respects L and E, L ⊢ λI. M ⟹ lab(E, L, I, M). By the definitions of typing rules, we must have ∅, T , L{I ↦ index(l, τ_{1})} ⊢ M : τ_{2}. Since index(l, τ_{1}) is a well formed ground index type, this denotes a natural number. Let this number be i. Then L{I ↦ i} respects L{I ↦ index(l, τ_{1})}. By induction hypothesis, for any v, if E, L{I ↦ i} ⊢ M ⟹ v, then ⊧ v : τ_{2}. By the definition of the typing rule for lab(E, L, I, M), we have ⊧ lab(E, L, I, M) : index(l, τ_{1}) ⇒ τ_{2}.

Later we use this result to establish the soundness of our compilation.

4 Type Inference and Compilation

In order to compile λ^{let,·} into λ^{let,[ ]}, we need to maintain information about type instantiations and to insert appropriate code for index abstraction and index application. We use the technique of type inference to achieve this. For this purpose, we first refine a unification algorithm to kinded unification.

4.1 Kinded unification

A kinded substitution is a pair consisting of a kind assignment and a substitution. A kinded substitution (K_{1}, S) respects a kind assignment K_{2} if, for all t ∈ dom(K_{2}), K_{1} ⊢ S(t) :: S(K_{2}(t)) is a derivable kinding. A kinded substitution (K_{1}, S_{1}) is more general than (K_{2}, S_{2}) if S_{2} = S_{3} ∘ S_{1} for some S_{3} such that (K_{2}, S_{3}) respects K_{1}. A kinded set of equations is a pair consisting of a kind assignment and a set of pairs of types. A kinded substitution (K_{1}, S) is a unifier of a kinded set of equations (K_{2}, E) if it respects K_{2} and S(τ_{1}) = S(τ_{2}) for all (τ_{1}, τ_{2}) ∈ E.

Theorem 2 There is an algorithm U which, given any kinded set of equations, computes a most general unifier if one exists and reports failure otherwise.

Proof: We define the algorithm U in the style of [GS89] by a set of transformation rules on triples (K, E, S) consisting of a kind assignment K, a set E of type equations and a set S of “solved” type equations of the form (t, τ) such that t ∉ F T V (τ). Let F range over functions from a finite set of labels to types. We write {F } and ⟨F ⟩ to denote the record type identified by F and the record kind identified by F, respectively. Figure 4 gives the set of transformation rules. Let u-i (K, E ∪ {(τ, τ)}, S) ⟹ (K, E, S)

u-ii (K ∪ {t ↦ U}, E ∪ {(t, τ)}, S) ⟹ ([t ↦ τ](K), [t ↦ τ](E), {(t, τ)} ∪ [t ↦ τ](S)) if t ∉ F T V (τ)

u-iii (K ∪ {t_{1} ↦ ⟨F_{1}⟩, t_{2} ↦ ⟨F_{2}⟩}, E ∪ {(t_{1}, t_{2})}, S) ⟹ ([t_{1} ↦ t_{2}](K ∪ {t_{2} ↦ ⟨F ⟩}), [t_{1} ↦ t_{2}](E ∪ {(F_{1}(l), F_{2}(l))|l ∈ dom(F_{1}) ∩ dom(F_{2})}),

{(t_{1}, t_{2})} ∪ [t_{1} ↦ t_{2}](S))
where F = {(l, τ_{l})|l ∈ dom(F_{1}) ∪ dom(F_{2}), τ_{l} = F_{1}(l) if l ∈ dom(F_{1}) otherwise τ_{l} = F_{2}(l)}
if t_{1} does not appear in F_{2} and t_{2} does not appear in F_{1}

u-iv (K ∪ {t_{1} ↦ ⟨F_{1}⟩}, E ∪ {(t_{1}, {F_{2}})}, S) ⟹ ([t_{1} ↦ {F_{2}}](K), [t_{1} ↦ {F_{2}}](E ∪ {(F_{1}(l), F_{2}(l))|l ∈ dom(F_{1}) ∩ dom(F_{2})}), {(t_{1}, {F_{2}})} ∪ [t_{1} ↦ {F_{2}}](S)

if dom(F_{1}) ⊆ dom(F_{2}) and t ∉ F T V ({F_{2}})

u-v (K, E ∪ {(τ_{1}^{1} → τ_{1}^{2}, τ_{2}^{1} → τ_{2}^{2})}, S) ⟹ (K, E ∪ {(τ_{1}^{1}, τ_{2}^{1}), (τ_{1}^{2}, τ_{2}^{2})}, S)

u-vi (K, E ∪ {({F_{1}}, {F_{2}})}, S) ⟹ (K, E ∪ {(F_{1}(l), F_{2}(l))|l ∈ dom(F_{1})}, S) if dom(F_{1}) = dom(F_{2})

Figure 4: Transformation Rules for Unification

(K, E) be a given kinded set of equations. The algorithm U first transforms (K, E, ∅) to (K′, E′, S′) until no more rules can apply. It then returns (K′, S′) if E′ is empty; otherwise it reports failure. The correctness of the algorithm is proved by showing that each transformation rule preserves the following property:

If (K_{1}, E_{1}, S_{1}) ⟹ (K_{2}, E_{2}, S_{2}) then a kinded
substitution is a unifier of (K_{1}, E_{1}∪S_{1}) if and
only if it is a unifier of (K_{2}, E_{2} ∪ S_{2}).

Cases other than u-iii and u-iv are same as in [GS89]. Here we show the case of the rule u-iii. The rule u-iv is simpler.

Suppose (K, σ) is a unifier of (K ∪ {t_{1} ↦ ⟨F_{1}⟩, t_{2} ↦ ⟨F_{2}⟩}, E ∪ {(t_{1}, t_{2})}, S). Then K ⊢ σ(t_{1}) :: σ(⟨F_{1}⟩), K ⊢ σ(t_{2}) :: σ(⟨F_{2}⟩), and σ(t_{1}) = σ(t_{2}). By the definition of kindings, we have σ(F_{1}(l)) = σ(F_{2}(l)) for all l ∈ dom(F_{1}) ∩ dom(F_{2}). Therefore K ⊢ σ(t_{2}) :: σ(⟨F ⟩). Since σ(t_{1}) = σ(t_{2}), σ([t_{1} ↦ t_{2}](E)) = σ(E) and σ([t_{1} ↦ t_{2}](S)) = σ(S). Thus (K, σ) is also a unifier of (K ∪ {t_{2} ↦ ⟨F ⟩}, [t_{1} ↦ t_{2}](E ∪ {(F_{1}(l), F_{2}(l))|l ∈ dom(F_{1}) ∩ dom(F_{2})}), {(t_{1}, t_{2})} ∪ [t_{1} ↦ t_{2}](S)). Conversely, suppose (K, σ) is a unifier of (K ∪ {t_{2} ↦ ⟨F ⟩}, [t_{1} ↦ t_{2}](E ∪ {(F_{1}(l), F_{2}(l))|l ∈ dom(F_{1}) ∩ dom(F_{2})}), {(t_{1}, t_{2})} ∪ [t_{1} ↦ t_{2}](S)). Then K ⊢ σ(t_{2}) :: σ(⟨F ⟩), σ([t_{1} ↦ t_{2}](F_{1}(l))) = σ([t_{1} ↦ t_{2}](F_{2}(l))) for all l ∈ dom(F_{1}) ∩ dom(F_{2}), and σ(t_{1}) = σ(t_{2}). By the definition of kindings, this implies that K ⊢ σ(t_{1}) :: σ(⟨F_{1}⟩) K ⊢ σ(t_{2}) :: σ(⟨F_{2}⟩). Since σ(t_{1}) = σ(t_{2}), σ([t_{1} ↦ t_{2}](E)) = σ(E) and σ([t_{1} ↦ t_{2}](S)) = σ(S). Thus (K, σ) is also a unifier of (K ∪ {t_{1} ↦ ⟨F_{1}⟩, t_{2} ↦ ⟨F_{2}⟩}, E ∪ {(t_{1}, t_{2})}, S). The termination can be proved by showing that each transformation rule decreases the termination measure of the lexicographical pair consisting of the number of type variables in E and the total size of E.

If the transformation terminates with (K, ∅, S), then it is obvious that (K, S) is a most general unifier of (K, ∅, S). It is also easily checked that if the transformation terminates with non empty E then E has no unifier.

4.2 The algorithm for compilation and type inference

We now give an algorithm that simultaneously computes a principal type scheme and a compiled implementation term.

A typing K_{1}, T_{1} ⊢ e : τ_{1} is more general than K_{2}, T_{2} ⊢ e : τ_{2} if dom(T_{1}) ⊆ dom(T_{2}), and there is a substitution S such that the kinded substitution (K_{2}, S) respects K_{1}, T_{2}(t) = S(T_{1}(t)) for all t ∈ dom(T_{1}), and τ_{2} = S(τ_{1}). A typing K, T ⊢ e : τ is principal if it is more general than all the derivable typings for e. We then have the following theorem.

Theorem 3 There is an algorithm C which takes a raw term and returns either (K, T , L, M, τ) or failure such that if it returns (K, T , L, M, τ), then K, T ⊢ e : τ is a principal typing in λ^{let,·} and K, T , L ⊢ M : τ is a typing in λ^{let,[ ]}; otherwise e has no typing in λ^{let,·}.

Proof: We follow [Mit90] and present C as

C(e) = Comp(e, ∅)

where Comp is an algorithm which takes a raw term and an environment A which maps a finite set of variables to tuples of the form (K, T , τ). The purpose of the environment A is to maintain a principal typing of let bound variables.

A complete definition of Comp is given in Figure 5. Since the treatment of let bound variables through

an auxiliary parameter A to Comp is the same as the proof of the corresponding theorem in [Mit90], the correctness of the treatment of let expressions is shown similarly. It is therefore enough to show that (1) the cases other than let bound variables and let expressions preserve the principal typing property of e, and (2) each case yields a provable typing of M in λ^{let,[ ]}.

Here we sketch below the proof of the property (1) for the case of e·l. The case for modify(e_{1}, l, e_{2}) is similar and all the other cases are essentially the same as in [Mit90].

By the definition of typing rules of λ^{let,·}, e_{1}·l has a typing of the form K, T ⊢ e_{1}·l : τ iff e_{1} has a typing of the form K, T ⊢ e_{1} : τ′ and K ⊢ τ′ :: ⟨l : τ⟩. By induction hypothesis, e_{1} has a typing K, T ⊢ e_{1} : τ′ iff (K_{1}, T_{1}, L_{1}, M_{1}, τ_{1}) = Comp(e_{1}, A) and K_{1}, T_{1} ⊢ e : τ_{1} is a more general than K, T ⊢ e_{1} : τ′. Under the fact that K ⊢ τ′ :: ⟨l : τ⟩, the later proposition of the previous sentence implies that (K_{1} ∪{t_{1} ↦ U, t_{2} ↦ ⟨l : t_{1}⟩}, {(τ_{1}, t_{2})}) (t_{1}, t_{2} fresh) has a unifier. The desired property then follows from that of U.

The property of (2) can be shown by cases. The cases of let and let bound variables can be shown by using the following two properties of λ^{let,[ ]}: (1) K, T , L{I ↦ index(l, τ_{1})} ⊢ M : τ_{2} is a derivable typing in λ^{let,[ ]} iff so is K, T , L ⊢ λI. M : index(l, τ_{1}) ⇒ τ_{2}, and (2) K, T , L{I ↦ index(l, τ_{1})} ⊢ M I : τ_{2} is a derivable typing in λ^{let,[ ]} iff so is K, T , L ⊢ M : index(l, τ_{1}) ⇒ τ_{2}. Other cases can be show by simple inductive reasoning.

Since we have shown the soundness of the type system of λ^{let,[ ]}, the above theorem implies the following soundness property of the type system of λ^{let,·} with respect to the evaluation through the compilation.

Corollary 1 If C(e) = (K, T , L, M, τ), E is a value environment respecting T and L is an index environment respecting L, and E, L ⊢ M ⟹ v, then ⊧ v : τ.

We end this section by showing some examples of the compilation.

C(λx. x·l)

=({t_{1} ↦ U, t_{2} ↦ ⟨l : t_{1}⟩}, ∅, {I ↦ index(l, t_{2})}, λx. x[I], t_{2} → t_{1})

C(let name = λx. x·Name in

name {Name = ”Joe”, Age = 21} end) = (∅, ∅, ∅, let name = λI. λx. x[I] in

(name 2) {Name = ”Joe”, Age = 21}
end, string)

The following shows an examples of compiling an ML-style type inference session. We write let x = e; for let x = e in x end and the subsequent expressions of the form e′; are regarded as shorthand for let x = e in e′. For the following type inference session:

(* to move a point-shape object horizontally *) let inc X = λp. modify(p, X, p·X + 1); → : ∀t::⟨X : int⟩. t → t

let salary = λx. x·Salary;

→ : ∀t_{1} ::U. ∀t_{2} ::⟨Salary : t_{1}⟩. t_{2} → t_{1}

salary {Name = ”Susan”, Age = 21,

Salary = 34000};

→ : int

let wealthy = λx. (salary x) > 100000;

→ : ∀t::⟨Salary : int⟩. t → bool

wealthy {Name = ”Susan”, Age = 21,

Salary = 34000};

→ : bool

the compilation algorithm produces the following code:

let inc X = λIλp. modify(p, I, p[I] + 1); → :∀t :: ⟨X : int⟩. index(X, t) ⇒ t → t

let salary = λIλx. x[I];

→ :∀t_{1} ::U∀t_{2} :: ⟨Salary : t_{1}⟩.

index(Salary, t_{2}) ⇒ t_{2} → t_{1}

(salary 3) {Name = ”Susan”, Age = 21,

Salary = 34000};

→ : int

let wealthy = λI. λx. ((salary I) x) > 100000; → :∀t::⟨Salary : int⟩.

index(Salary, t) ⇒ t → bool

(wealthy 3){Name = ”Susan”, Age = 21,

Salary = 34000};

→ : bool

5 Calculi with Subtyping

One might want to develop a similar compilation algorithm for a polymorphic record calculus with subtyping. As we mentioned in the introduction, however, Comp(x, A) = if x ∈ dom(A) then

let (K_{1}, T_{1}, τ_{1}) = A(x) (with all type variables renamed with fresh names) (α_{1} ⇒ ⋯ ⇒ α_{n} ⇒ τ′_{1}) = τ_{1} (0 ≤ n and τ′_{1} does not contain ⇒) I_{i} = (if α_{i} ≡ index(l, t) then I_{i} (fresh) else the integer denoted by α_{i}) L_{1} = {I_{i} ↦ α_{i}| for new I_{i} introduced above},

in (K_{1}, T_{1}, L_{1}, ((⋯ (x I_{1}) ⋯) I_{n}), τ′_{1}) else ({t ↦ U}, {x ↦ t}, ∅, x, t)

Comp(c^{τ} , A) = (∅, ∅, ∅, c^{τ} , τ)

Comp(λx. e_{1}, A) = let (K_{1}, T_{1}, L_{1}, M_{1}, τ_{1}) = Comp(e_{1}, A)

in if x ∈ dom(T_{1}) then (K_{1}, T_{1}↑^{dom(T_{1})\{x}}, L_{1}, λx. M_{1}, T_{1}(x) → τ_{1})

else (K_{1}{t ↦ U}, T_{1}, L_{1}, λx. M_{1}, t → τ_{1}) (t fresh)

Comp(e_{1} e_{2}, A) =

let (K_{1}, T_{1}, L_{1}, M_{1}, τ_{1}) = Comp(e_{1}, A)

(K_{2}, T_{2}, L_{2}, M_{2}, τ_{2}) = Comp(e_{2}, A) (K_{3}, S) = U(K_{1} ∪ K_{2} ∪ {t ↦ U}, {(T_{1}(x), T_{2}(x))|x ∈ dom(T_{1}) ∩ dom(T_{2})} ∪ {(τ_{2} → t, τ_{1})}) (t fresh)

in (K_{3}, S(T_{1} ∪ T_{2}), S(L_{1} ∪ L_{2}), M_{1} M_{2}, S(t))

Comp({l_{1} = e_{1}, …, l_{n} = e_{n}}, A) =

let (K_{i}, T_{i}, L_{i}, M_{i}, τ_{i}) = Comp(e_{i}, A) (1 ≤ i ≤ n)

T′_{i} =T_{i}{x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}}

where {x_{1}, …, x_{n}} = (⋃_{1≤j≤n} dom(T_{j})) \ dom(T_{i}) and {t_{1}, …, t_{n}} are all fresh (K, S) = U(K_{1} ∪ ⋯ ∪ K_{n} ∪ {t_{i} ↦ U|1 ≤ i ≤ n}, {(T′_{i}(x), T′_{i+1}(x))|x ∈ dom(T′_{1}), 1 ≤ i ≤ n − 1})

in (K, S(T_{1}), S(L_{1} ∪ ⋯ ∪ L_{n}), {l_{1} = M_{1}, …, l_{n} = M_{n}}, S({l_{1} : τ_{1}, …, l_{n} : τ_{n}}))

Comp(e_{1}·l, A) = let (K_{1}, T_{1}, L_{1}, M_{1}, τ_{1}) = Comp(e_{1}, A)

(K, S) = U(K_{1} ∪ {t_{1} ↦ U, t_{2} ↦ ⟨l : t_{1}⟩}, {(τ_{1}, t_{2})}) (t_{1}, t_{2} fresh)

in if S(t_{2}) = {l_{1} : τ_{1}^{1}, …, l_{n} : τ_{n}^{1}} then

(K, S(T_{1}), S(L_{1}), M[j], S(t_{1})) where j = Size({l|l ∈ {l_{1}, …, l_{n}}, l ≤ l_{i}}) else (K, S(T_{1}), S(L_{1}) ∪ {I ↦ index(l, S(t_{2}))}, M[I], S(t_{1}))

Comp(modify(e_{1}, l, e_{2}), A) =

let (K_{1}, T_{1}, L_{1}, M_{1}, τ_{1}) = Comp(e_{1}, A)

(K_{2}, T_{2}, L_{2}, M_{2}, τ_{2}) = Comp(e_{2}, A) (K_{3}, S) = U(K_{1} ∪ K_{2} ∪ {t_{1} ↦ U, t_{2} ↦ ⟨l : t_{1}⟩},

{(T_{1}(x), T_{2}(x))|x ∈ dom(T_{1}) ∩ dom(T_{2})} ∪ {(τ_{2}, t_{1}), (τ_{1}, t_{2})}) (t_{1}, t_{2} fresh)

in if S(t_{2}) = {l_{1} : τ_{1}^{1}, …, l_{n} : τ_{n}^{1}} then

(K_{3}, S(T_{1} ∪ T_{2}), S(L_{1} ∪ L_{2}), modify(M_{1}, j, M_{2}), S(t_{2})) where j = Size({l|l ∈ {l_{1}, …, l_{n}}, l ≤ l_{i}}) else (K_{3}, S(T_{1} ∪ T_{2}), S(L_{1} ∪ L_{2}) ∪ {I ↦ index(l, S(t_{2}))}, modify(M_{1}, I, M_{2}), S(t_{2}))

Comp(let x = e_{1} in e_{2} end, A) =

let (K_{1}, T_{1}, L_{1}, M_{1}, τ_{1}) = Comp(e_{1}, A)

{I_{1} ↦ α_{1}, …, I_{n} ↦ α_{n}, I′_{1} ↦ α′_{1}, …, I′_{m} ↦ α′_{m}} = L_{1} (α_{i} not ground, α′_{i} ground) A′ = A{x ↦ (K_{1}, T_{1}, α_{1} ⇒ ⋯ ⇒ α_{n} ⇒ τ_{1})} (K_{2}, T_{2}, L_{2}, M_{2}, τ_{2}) = Comp(e_{2}, A′) (K, S) = U(K_{1} ∪ K_{2}, {(T_{1}(x), T_{2}(x))|x ∈ dom(T_{1}) ∩ dom(T_{2})}) M′_{1} be the term obtained from M_{1} by replacing occurrences of I′_{i} with the natural number denoted by α′_{i}

in (K, S(T_{1} ∪ T_{2}), S(L_{2}), let x = λI_{1}. · · · λI_{n}. M_{1} in M_{2} end, S(τ_{2}))

Figure 5: The Compilation Algorithm some difficulty seems to be inherent in any record calculus containing the familiar subsumption rule of the form:

sub  \frac{⊢ e : τ_{1} τ_{1} ≤ τ_{2}}{⊢ e : τ_{2}}

To see the difficulty, consider the expression:

e ≡ if e_{1} then {A = ”abc”, B = true} else {B = true, C = ”abc”}

With the existence of the subsumption rule, this expression has the type {B : bool}. However, the actual set of labels of the value denoted by e depends on the value denoted by e_{1} and therefore the offset of the label B can not be statically determined. It is therefore impossible to compile an expression such as (λx. x·B) e into the implementation calculus. A similar problem arises in combination of bulk data types such as list or set types. This observation shows that in a record calculus with the subsumption rule, it is in general impossible to statically compute offsets of labels. This property is related to loss of type information – the phenomenon first observed in [CW85]. With the subsumption rule, a typing judgment of the form ⊢ e : {l_{1} : τ_{1}, …, l_{n} : τ_{n}} no longer implies that e denotes a record value having the exact type {l_{1} : τ_{1}, …, l_{n} : τ_{n}}.

As we have discussed in [BTBO89], this property is also problematic in dealing with operations such as equality and database join, which require the exact type information of their parameters. It remains to be investigated whether there is some interesting subset of a polymorphic record calculus with subtyping that does not suffer from this problem and allow efficient compilation. Another possibility of overcoming this difficulty would be to enrich a calculus with a new form of judgments for exact typing.

6 Conclusions

We have established a compilation method for a polymorphic type inference system with labeled records. The method always yields code that deals with field selection and field modification by a few machine instructions. The polymorphic type discipline for records is shown to be sound with respect to the compilation.

The presented algorithm can readily be incorporated in existing ML-style polymorphic programming languages with records. For example, Standard ML [MTH90] contains records and monomorphic field selection. By refining its type system to incorporate kinded abstraction and incorporating its compiler with our compilation algorithm, the language can be refined to support polymorphic field selection and its efficient execution without altering its language syntax.

As we mentioned in the introduction, one important extension to the work presented here is to include more powerful operations on records such as concatenation and join. To represent these operations, the polymorphic type system must be extended. One approach is to introduce constraints on instantiation of type variables of the form

t = τ_{1}∗τ_{2}

which denotes the requirement that the instantiation of t is restricted to those S(t) such that S(t) is a record type equal to S(τ_{1})∗S(τ_{2}), where ∗ is an appropriate operator on record types representing join or concatenation. Typing mechanism incorporating this idea have been developed in [OB88, Wan89] for type inference systems and in [CM89, HP91] for second-order type systems. However, eliminating time consuming run-time scan of the fields of two records seems to require a substantial extension of the implementation calculus and the compilation strategy.

References

[AB87] M.P. Atkinson and O.P. Buneman. Types and persistence in database programming languages. ACM Computing Surveys, 1987.

[BTBO89] V. Breazu-Tannen, P. Buneman, and A. Ohori. Can object-oriented databases be statically typed? In Proc. 2^{nd} International Workshop on Database Programming Languages, pages 226 – 237, 1989. Morgan Kaufmann Publishers.

[Car88] L. Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988. (Special issue devoted to Symp. on Semantics of Data Types, 1984).

[Car91] L. Cardelli. Extensible records in a pure calculus of subtyping. Technical report, DEC Systems Research Center, 1991.

[CDMB89] R. Connor, A. Dearle, R. Morrison, and F. Brown. An object addressing mechanism for statically typed languages with multiple inheritance. In Proc. ACM OOP-SLA Conference, pages 279–285, 1989.

[CM89] L. Cardelli and J. Mitchell. Operations on records. In Proc. Masematical Foundation of Programming Semantics, Lecture Notes in Computer Science 442, pages 22– 52, 1989.

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

[DM82] L. Damas and R. Milner. Principal type-schemes for functional programs. In Proc. ACM Symposium on Principles of Programming Languages, pages 207–212, 1982.

[Gir71] J.-Y.

Girard. Une extension de l’interpretation de gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et théorie des types. In Second Scandinavian Logic Symposium. North-Holland, 1971.

[GS89] J. Gallier and W. Snyder. Complete sets of transformations for general E-unification. Theoretical Computer Science, 67(2):203– 260, 1989.

[HP91] R. Harper and B. Pierce. A record calculus based on symmetric concatenation. In Proc. ACM Symp. on Principles of Programming Languages, 1991.

[JM88] L. A. Jategaonkar and J.C. Mitchell. ML with extended pattern matching and subtypes. In Proc. ACM Conference on LISP and Functional Programming, pages 198– 211, 1988.

[MH88] J. C. Mitchell and R. Harper. The essence of ML. In Proc. 15th ACM Symposium on Principles of Programming Languages, pages 28–46, 1988.

[Mit84] J.C. Mitchell. Coercion and type inference. In Proc. ACM Symposium on Principles of Programming Languages, pages 175–185, 1984.

[Mit90] J.C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 8, pages 365–458. MIT Press/Elsevier, 1990.

[MTH90] R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1990.

[OB88] A. Ohori and P. Buneman. Type inference in a database programming language. In Proc. ACM Conference on LISP and Functional Programming, pages 174–183, 1988.

[OB89] A. Ohori and P. Buneman. Static type inference for parametric classes. In Proc. ACM OOPSLA Conference, pages 445– 456, 1989.

[Oho89a] A. Ohori. A simple semantics for ML polymorphism. In Proc. ACM/IFIP Conference on Functional Programming Languages and Computer Architecture, pages 281–292, 1989.

[Oho89b] A. Ohori. A Study of Types, Semantics and Languages for Databases and Objectoriented Programming. PhD thesis, University of Pennsylvania, 1989.

[Rém89] D. Rémy. Typechecking records and variants in a natural extension of ML. In ACM Conference on Principles of Programming Languages, pages 242–249, 1989.

[Rém90] D. Rémy. Typechecking records in a natural extension of ML. Technical report, INRIA–Rocquencourt, Le Chesnay Cedex, France, 1990.

[Rém91] D. Rémy. Typing record concatenation for free. Technical report, INRIA–Rocquencourt, Le Chesnay Cedex, France., 1991.

[Rey74] J.C. Reynolds. Towards a theory of type structure. In Paris Colloq. on Programming, pages 408–425. Springer-Verlag, 1974.

[Sta88] R. Stansifer. Type inference with subtypes. In Proc. ACM Symposium on Principles of Programming Languages, pages 88–97, 1988.

[Tof88] M. Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, Department of Computer Science, University of Edinburgh, 1988.

[Wan87] M. Wand. Complete type inference for simple objects. In Proc. IEEE Symposium on Logic in Computer Science, pages 37– 44, 1987.

[Wan88] M. Wand. Corrigendum : Complete type inference for simple object. In Proc. IEEE Symposium on Logic in Computer Science, 1988.

[Wan89] M. Wand. Type inference for records concatenation and simple objects. In Proc. IEEE Symposim on Logic in Computer Science, pages 92–97, 1989.