A case study of typechecking with constrained types: Typing record concatenation

Draft of December 26, 1996

Didier Rémy INRIA-Rocquencourt^{∗}

Abstract

We study static type-soundness of type systems with non-atomic-subtyping based on constrained types for first-order lambda-calculus (no Let) with one-field records given with a call-by-value reduction semantics. We then extend the language with general records with concatenation. This case study shows the flexibility of type inference with constrained types. We extend the constrained types with type operators in order to type-check record concatenation in the presence of subtyping. This method should provide wrappers to object-oriented languages based on the object-as-record-of-methods paradigm. We do not address the practical issues of type inference here.

1 Introduction

Presented as a case study of typechecking with constrained types [EST95], the main result of this work is a type system for typechecking record concatenation. The interest of the result is also its possible application to other similar extensions. In particular, objectoriented languages following the “object as record of methods” paradigm, such as [EST], could benefit a lot from wrappers (wrappers solve most examples that motivated multiple inheritance while avoiding the problems of multiple inheritance itself). The flexibility and robustness of type inference with constrained types is also illustrated though this case study. In the proof of type soundness, we make a clear connection between propagation rules at the level of types and the reduction rules at the level of values; we also show how consistency rules guarantee the correspondence between the shape of values and their types. Then, it becomes easy to extend the formalism to new constructions. Our main contribution to the formalism is the introduction of type operators that delay propagation of complex constraints until enough of the shape of the types is known.

The main difficulty in typing record concatenation is its inconsistency with subtyping. The concatenation of two records a_{1} equal to {ℓ_{1} = v_{1}, ℓ_{2} = v_{2}} and a_{2} equal to {ℓ_{2} = v′_{2}, ℓ_{3} = v_{3}} is the record {ℓ_{1} = v_{1}, ℓ_{2} = v′_{2}, ℓ_{3} = v_{3}}. Therefore if a_{1} and a_{2} have types {ℓ_{1} : τ_{1}, ℓ_{2} : τ_{2}} and {ℓ_{2} : τ′_{2}, ℓ_{3} : τ_{3}}, respectively, then the result of their concatenation should have type {ℓ_{1} : τ_{1}, ℓ_{2} : τ′_{2}, ℓ_{3} : τ_{3}}. However, by subtyping a_{2} also has type {ℓ_{3} : τ_{3}}, in which case the result of their concatenation should have type {ℓ_{1},: τ_{1}, ℓ_{2} : τ_{2}, ℓ_{3}, τ_{3}}, which is clearly erroneous. The problem is that, in order to deduce the shape of the record a_{2} from its type, and therefore the type of a_{1} @ a_{2} from the types of τ_{1} and τ_{2}, the exact type of a_{2} is required. We solve this problem keeping subtyping by introducing two forms of record types: rigid and flexible. The idea is that a record is first assigned a rigid record type that exactly describes its structure. For instance, a value a_{0} of the form {ℓ_{1} = a_{1}, ℓ_{2} = 2} has type ⟨ℓ_{1} : τ_{1}, ℓ_{2} : τ_{2}⟩ provided a_{1} and a_{2} have types τ_{1} and τ_{2}. Fields cannot be forgotten in rigid types. In particular, a_{0} does not have type ⟨ℓ_{1} : τ_{1}⟩. However, rigid types can be coerced to flexible types, after which fields may be forgotten. For instance, a_{0} has type {ℓ_{1} : τ_{1}, ℓ_{2} : τ_{2}} and also {ℓ_{1} : τ_{1}}. More generally, the concatenation of two values of type ⟨ℓ_{i} : τ_{i}, i ∈ I⟩ and ⟨ℓ_{i} : τ′_{i}, i ∈ I′⟩ has type ⟨ℓ_{i} : τ_{i}, i ∈ I \I′, ℓ_{i} : τ′_{i}, i ∈ I′⟩. As described above, it is essential that the second type is a rigid type, otherwise it would not guarantee that fields ℓ_{i} for i ∈ I \ I′ are undefined in the second argument.

∗Author’s address: INRIA-Rocquencourt, B.P. 105, F-78153 Le Chesnay Cedex. Email:

Didier.Remy@inria.fr

Typing the function fun x → fun y → x @ y raises another problem: the type of x @ y is determined from the shape of the type τ_{1} and τ_{2} of x and y, and therefore cannot be described more precisely as long as τ_{1} and τ_{2} are variables. One way to handle this problem is to delay types of concatenations of records until enough structure is known about the types of the records. We introduce a type operator @ and allow new constraints of the form τ_{1} @ τ_{2} ▷ τ_{3} that will induce further constraints as soon as enough of the shape of τ_{1} and τ_{2} will be known (see propagation rules below).

We reuse the framework of [EST95] for a small language with one-field records described in section 2.1. We establish the soundness of the static type system with respect to a reduction semantics. There is no new result in this section, but a reformulation of [EST95] emphasizing the modularity of the approach. We extend the language to extensible records and study their concatenation on section 4 and treat the case of multiple-field records in section 5. In the last section we summarize the results and briefly discuss other possible use of constrained types.

2 The language

2.1 The core language

We consider a simply typed language (no Let), since our focus is understanding the basis of both typechecking with constrained types and typechecking record concatenation. Adding ML polymorphism to the language is not a problem in theory. In practice, however, it is a considerable extension that requires trickier algorithms as soon as one begins to consider efficiency issues. Since we have disclaimed from the beginning any consideration for efficiency in this work, we leave the addition of ML polymorphism as an orthogonal issue that should be studied in detail elsewhere.

The syntax of expressions and types

a ::= u | x | a a | b  expressions
u ::= fun x → a | c  value forms
b ::= get a  primitive applications
c ::= abs | pre a  constructor forms
τ ::= α | τ → τ | Pre τ | Abs  types

We write T the set of types. We have intendedly distinguished three classes of subexpressions. The constructions pre and abs should be seen as value constructors, while expressions get are primitive operations. The syntactic class of values v can be automatically generated: its recursive definition is obtained from the definition of u by replacing in c all occurrences of a by v. That is, after c has been expanded:

v ::= fun x → a

                                  | abs | pre v

The evaluation contexts can also be generated in a systematic way by treating all constructions of u and c as applications.

\begin{matrix}E ::= & [] | E a | v E \\ | & get E | pre E \end{matrix}

On the second line we have added one possibility for each occurrence of a. For a left-to-right evaluation order, all occurrences of a appearing on the left of the evaluation context E are replaced by v’s (as for the application), which enforces deterministic application of rule R-context given below. The reduction relation is defined by:

(fun x → a) v ⟶ a[v/x]  (R-β)
get (pre v) ⟶ v  (R-Get)
E[a_{1}] ⟶ E[a_{2}] if a_{1} ⟶ a_{1}  (R-Context)

2.2 Constrained types

Our typechecking is based on constrained types. Constrained types have been introduced by Curtis in his PhD thesis [Cur90], but type soundness was not proved. A general presentation, including type soundness, was done by Aiken and Wimmers [AW93]. A restriction of their formalism was then used for type inference for an object-oriented language in [EST95]. An alternative approach, which has now be proved equivalent was initially done for type inference for primitive objects by Palsberg[Pal94]. The formalism we are using here is taken from [EST95]. Most of the results about constrained types that are presented here were already in [EST95], although the presentation and some proofs have been structured slightly differently, mainly for sake of modularity.

Constraints are pairs of types written τ_{1} ▷ τ_{2}. A set of constraints C can also be seen as a binary relation ▷_{C}, and we drop the subscript when there is no ambiguity. Therefore we indifferently write τ_{1} ▷ τ_{2} ∈ C or τ_{1} ▷_{C} τ_{2} or τ_{1} ▷ τ_{2} in short. The closure of a set of constraints C is the smallest superset Ĉ closed by • transitivity, and

τ_{1} ▷ τ_{2} ∧ τ_{2} ▷ τ_{3} ⟹ τ_{1} ▷ τ_{3}  (P-Trans)

• structural propagation.

τ_{1} → τ_{2} ▷ τ′_{1} → τ′_{2} ⟹ τ_{2} ▷ τ′_{2} ∧ τ′_{1} ▷ τ_{1}  (P-Arrow)
Pre τ ▷ Pre τ′ ⟹ τ ▷ τ′  (P-Pre)

For simplicity of notation, we introduce type patterns t̃, which are types where all variables are replaced by an otherwise character “ ”. We write Top (τ_{1}, τ̃_{2}) and respectively Top (τ_{1}, T) where T is a set of τ̃, to mean that either τ is a variable or that it matches τ_{2} (respectively one of the τ in T). A set of constraints C is consistent, and we write ⊢ C if its closure satisfies the following properties:

τ ▷ τ_{1} → τ_{2} ⟹ Top (τ, → )  (C-Arrow)
τ ▷ Pre τ_{1} ⟹ Top (τ, Pre )  (C-Pre)

It is the case here, and in all extensions in this paper that reflexive constraints are always consistent.

An essential definition is the entailment relation on set of constraints, which we note C_{1} ⊢ C_{2}. In [EST95], the implicit entailment relation is defined as:

C_{1} ⊢_{0} C_{2} =^{def} Ĉ_{2} ⊂ Ĉ_{1} ∪ {τ ▷ τ, τ ∈ T }

In particular, C_{1} ⊢_{0} C_{2} implies that for any set of constraints C, if C_{1} ∩ C is consistent, then so is C_{2} ∩ C. This allows to safely replace C_{1} by C_{2}, i.e. without introducing any further inconsistencies. The converse is not true, i.e. there are set of constraints C_{1}and C_{2} such that

∀C, ( ⊢ C_{1} ∪ C ⟹ ⊢ C_{2} ∪ C)

although C_{1} ⊢_{0} C_{2} does not hold. In [Pot95] it appears that the relation ⊢_{0} prevents too many simplifications. A natural extension of this relation would be:

C_{1} ⊢_{+} C_{2} =^{def} ∀C, ( ⊢ C_{1} ∪ C) ⟹ ( ⊢ C_{2} ∪ C)

Clearly, ⊢_{0} ⊂ ⊢_{+}. However, the relation ⊢_{+} strongly depends on the notion of consistency, which will not facilitate further extensions. Moreover, it is not clear whether the relation ⊢_{+} is decidable. In order to leave flexibility in the choice of the containment relation, we will take any transitive relation ⊢ that contains ⊢_{0} and satisfies

C_{1} ⊢ C_{2} ⟹ ∀C, C_{1} ∪ C ⊢ C_{2} ∪ C  ( ⊢-Extension)

Although non complusory, and sometime misleading, it is also convenience to consider constrained types, i.e. pairs, written τ | C, of a type and a consistent set of constraints. We define an ordering on constrained types: we write τ_{1} | C_{1} ≤ τ_{2} | C_{2} for C_{2} ⊢ C_{1} ∪ {τ_{1} ▷ τ_{2}}. The relation ≤ is transitive (since the relation ⊢ is). Most of the properties of ⊢ induce similar properties on ≤, in particular

τ_{1} | C_{1} ≤ τ_{2} | C_{2} ⟹ ∀C, (τ_{1} | C_{1} ∪ C) ≤ (τ_{2} | C_{2} ∪ C)  (≤-Extension)

2.3 Typing rules

Typing judgements are of the form A ⊢ a : τ | C where C is a consistent set of constraints. The typing rules are:

(Abs) ; \overline{A ⊢ abs : Abs}

(Pre)

\frac{A ⊢ a : τ | C}{A ⊢ pre a : Pre τ | C}

(Get)

\frac{A ⊢ a : Pre τ | C}{A ⊢ get a : τ | C}

(Sub) ; \frac{A ⊢ a : τ_{1} | C_{1} τ_{1} | C_{1} ≤ τ_{2} | C_{2}}{A ⊢ a : τ_{2} | C_{2}}  (Var) ; \frac{x : τ ∈ A}{A ⊢ x : τ | C}  (Fun) ; \frac{A ⊕ (x ↦ τ_{2}) ⊢ a : τ_{1} | C}{A ⊢ fun x → a : τ_{2} → τ_{1} | C}

(App) ; \frac{A ⊢ a_{1} : τ_{2} → τ_{1} | C_{1} A ⊢ a_{2} : τ_{2} | C_{2}}{A ⊢ a_{1} a_{2} : τ_{1} | C_{1} ∪ C_{2}}

The intuition of the Sub rule is that it factorizes the two simpler rules:

(Sub-Type) ; \frac{A ⊢ a : τ | C C ⊢ τ ▷ τ′}{A ⊢ a : τ′ | C} (Sub-Constraint)

\frac{A ⊢ a : τ | C C ⊢ C′}{A ⊢ a : τ | C′}

Lemma 1 (Canonical proofs) Any derivation can be rewritten so that no instance of Sub has an instance of Sub as an antecedent.

\underline{Proof}: This follows immediately from the transitivity of ≤.

3 A syntactic proof of semantic soundness

The correction of the above semantics is guaranteed by two lemmas. Theorem 1 (subject reduction) says that typings are preserved by reduction. Theorem 2 says that well-typed irreducible programs are values. The combination of the two lemmas means that evaluation of well-typed programs cannot go wrong.

A typing for an expression a is a tripple (A, τ, C) such that A ⊢ a : τ | C. The inclusion of typings induce a relation ⊂ on terms. We write a_{1} ⊂ a_{2} to say that all typings of a_{1} are also typings of a_{2}. Then subject reduction is simply the conservation of typings during reduction.

Theorem 1 (subject reduction) The reduction is a sub-relation of ⊂, i.e. if a_{1} ⟶ a_{2}, then a_{1} ⊂ a_{2}

The proof is simplified by using the following lemmas.

Lemma 2 The relation ⊂ is increasing, i.e. if a_{1} ⊂ a_{2}, then E[a_{1}] ⊂ E[a_{2}].

\underline{Proof}: By structural induction on E. In each case we build a derivation of E[a_{2}] from a canonical derivation of E[a_{1}].

Cas E is []: There is nothing to show,

Cas E is E_{0} a: Then a canonical derivation of E[a_{1}] is of the form

A ⊢ E_{0}[a_{1}] : τ → τ_{0} | C_{0} A ⊢ a : τ | C (App)

A ⊢ E[a_{1}] a : τ | C_{0} ∪ C (Sub)

A ⊢ E[a_{1}] a : τ′ | C′

By induction hypothesis, we can replace a_{1} by a_{2} in the premise and apply the same rules to conclude.

Cas E is v E_{0}: Similar to previous case.

Other cases E is get E_{0} or Pre E_{0}: are also similar to the application case.

Lemma 3 If A⊕(x ↦ τ_{0}) ⊢ a : τ | C (1) and A ⊢ v : τ_{0} | C_{0} (2) and if C ∪C_{0} is consistent, then we have A ⊢ a[v/x] : τ | C ∪ C_{0} (3).

\underline{Proof}: The proof is by structural induction on the expression a. We write A_{0} for A⊕(x ↦ τ_{0}).

In each case, we first consider a canonical derivation of (1) that does not end with a Sub rule, and show that we can deduce a derivation (3). Now, if the canonical derivation of (1) ends with a Sub rule, we have a derivation A ⊕ (x ↦ τ_{0}) ⊢ a : τ′ | C′ that does not end with a Sub rule, and such that τ′′ | C′′ ≤ τ | C. By ≤-extension we have τ′′ | C′′ ∪ C_{0} ≤ τ | C ∪ C_{0} (4). Since C ∪ C_{0} is consistent, so is C′′ ∪ C_{0}. Therefore, by induction hypothesis, we have a derivation of A ⊢ a[v/x] : τ′′ | C′′ ∪ C_{0}. We conclude using a Sub rule derived from (4).

Cas a is x or a is abs: The terms a[v/x] and v are equal.

Cas a is z and z ≠ x: The termes a[v/x] and a are equal and x is not free in them. The conclusion is by context extension.

Cas a is pre a_{1}: The canonical derivation of (1) must end with:

\frac{A ⊢ a_{1} : τ_{1} | C}{A ⊢ pre a_{1} : Pre τ_{1} | C}

By induction hypothesis followed by the same rule.

Cas a is get a_{1}: Similar.

Cas a is fun y → a_{1}: The canonical derivation of (1) must end with:

\frac{A_{0} ⊕ (y ↦ τ_{2}) ⊢ a_{1} : τ_{1} | C (4)}{A_{0} ⊢ fun y → a_{1} : τ_{2} → τ_{1} | C}

where τ is τ_{2} → τ_{1}. By rearranging the context of (4), we have A ⊕ (y ↦ τ_{2}) ⊕ (x ↦ τ_{0}) ⊢ a_{1} : τ_{1} | C (5). By extending the context of (2), we have A ⊕ (y ↦ τ_{2}) ⊢ v : τ_{0} | C_{0} (6) By applying the induction hypothesis to (5) and (6), we get A⊕(y ↦ τ_{2}) ⊢ a_{1}[v/x] : τ_{1} | C ∪C_{0}. We obtain the conclusion by applying a Fun rule.

Cas a is a_{1} a_{2}: The canonical derivation of (1) must end with:

\frac{A_{0} ⊢ a_{1} : τ_{1} → τ | C_{1} (1) A_{0} ⊢ a_{2} : τ_{2} | C_{2} (2)}{A_{0} ⊢ a_{1} a_{2} : τ | C_{1} ∪ C_{2} ∪ \{τ_{2} ▷ τ_{1}\}}

where C is C_{1} ∪ C_{2}. By applying the induction hypothesis to both premises, we get A ⊢ a_{1}[v/x] : τ_{0} → τ | C_{1} ∪ C_{0} (4) and A ⊢ a_{2}[v/x] : τ_{2} | C_{2} ∪ C_{0} (5). Since C_{1} ∪ C_{2} ∪ {τ_{2} ▷ τ_{1}} ∪ C_{0} is consistent, so are C_{1} ∪ C_{0} and C_{2} ∪ C_{0}. We obtain the conclusion by applying an App rule.

\underline{Proof}: [of subject reduction] Using the lemma 2, it is enough to show subject reduction for redexes. Each case can be shown independently. The lemma can be first shown for typings whose canonical derivations do not end with a Sub rule. The general case immediately follows by reduction to the simpler case combined with the application of a Sub rule.

Cas a_{1} is (fun x → a) v: The canonical derivation ends with:

A ⊕ (x ↦ τ′_{0}) ⊢ a : τ′ | C′ (1) (Fun) A ⊢ fun x → a : τ′_{0} → τ′ | C′ (Sub) A ⊢ fun x → a : τ_{0} → τ | C A ⊢ v : τ_{0} | C_{0} (2) (App)

A ⊢ (fun x → a) v : τ | C ∪ C_{0}

where τ′_{0} → τ′ | C′ ≤ τ_{0} → τ | C. By structural propagation, we have τ′ | C′ ≤ τ | C and τ_{0} | C′ ≤ τ′_{0} | C (3). Applying a Sub rule to (1) and the first inequality of (3), we get A ⊕ (x ↦ τ′_{0}) ⊢ a : τ | C (4). From (3), we also have τ_{0} ≤ τ′_{0} | C, and by ≤-Extension, we have τ_{0} | C_{0} ≤ τ′_{0} | C ∪ C_{0}. From (2), we deduce A ⊢ v : τ′_{0} | C ∪ C_{0} (5). Applying the lemma 3 to (4) and (5) leads to the conclusion.

Cas a is get (pre v): The canonical derivation ends with:

A ⊢ v : τ_{1} | C_{1} (1) (Pre)

A ⊢ pre v : Pre τ_{1} | C_{1}

(Sub)

A ⊢ pre v : Pre τ_{2} | C_{2}

(Get)

A ⊢ get (pre v) : τ_{2} | C_{2}

We know that Pre τ_{1} | C_{1} ≤ Pre τ_{2} | C_{2}. By structural propagation, we have τ_{1} | C_{1} ≤ τ_{2} | C_{2}. We conclude A ⊢ v : τ_{2} | C_{2} from (1) by a Sub-rule.

Theorem 2 (irreducible terms) Irreducible well-typed terms are values.

\underline{Proof}: The difficulty is to show that the shape of values correspond to the shape of their types. This clearly relies on consistency of constrained types. We first see that for any canonical derivation of ⊢ v : τ | C that does not end with a Sub rule,

• If v is a function then τ is τ_{1} → τ_{2},

• If v is of the form pre v_{1} then τ is Pre τ_{1},

• If v is abs then τ is Abs.

Moreover, τ is never a variable. Since all top symbols of types are distinct, the implications can be reversed:

• If τ is τ_{1} → τ_{2} then v is a function,

• If τ is Pre τ_{1} then v is of the form pre v_{1},

• If τ is Abs then v is abs.

If the canonical derivation of ⊢ v : τ | C ends with a Sub rule, there is a derivation ⊢ v : τ′ | C′ that does not end with a Sub rule and such that τ′ | C′ ≤ τ | C, i.e. C ⊢ C′ ∪ {τ′ ▷ τ}. Since τ′ cannot be a variable, by consistency:

• If τ is τ_{1} → τ_{2} then τ′ is of the form τ′_{1} → τ′_{2}, and so v is a function.

• If τ is Pre τ_{1} then τ′ is of the form Pre τ′_{1}, and so v is of the form pre v_{1}.

We can now prove the theorem, i.e. that any well-typed irreducible term a is a value. The proof is by structural induction on a. We consider a canonical derivation of a typing of a. After possibly removing the last derivation rule of this derivation if it is an instance of a Sub rule, we have a derivation ⊢ a : τ | C (1) that does not end with a sub rule.

Cas a is x: is not possible since a must be closed.

Cas a is abs or fun x → a_{1}: then a is a value.

Cas a is an application a_{1} a_{2}: The canonical derivation of (1) ends with:

\frac{⊢ a_{1} : τ_{2} → τ_{1} | C_{1} ⊢ a_{2} : τ_{2} | C_{2}}{⊢ a_{1} a_{2} : τ_{1} | C_{1} ∪ C_{2}}

Therefore by induction hypothesis, a_{1} is a value. Since it has a functional type, it is a function. Therefore a could be reduced.

Cas a is pre a_{1}: The canonical derivation of (1) ends with:

A ⊢ a_{1} : τ | C (Pre)

A ⊢ pre a_{1} : Pre τ | C

By induction hypothesis a_{1} must be a value, therefore a is a value.

Cas a is get a_{1}: The canonical derivation of (1) ends with:

A ⊢ a_{1} : Pre τ | C (Get)

A ⊢ get a_{1} : τ | C

By induction hypothesis a_{1} must be a value. Since it has a typing of the form Pre τ | C, it must be a value of the form pre v, and therefore a could be reduced.

Remarks and variations

A few points of the above proofs must be emphasized. Propagation rules are used in subject reduction while consistency rules are used only to proof that irreducible terms are values. In particular, it is possible to give stronger consistency rules. For instance, one could add

τ ▷ Abs ⟹ Top (τ, {Pre , Abs})  (C-Abs-Pre)

The connection with propagation and consistency rules will appear even more clearly in the other extensions below. With rule C-Abs-Pre, it would also be guaranteed that values of type Abs are either abs or of the form pre . Since, if ⊢ v : Abs then there is also a derivation ⊢ v : τ′ not ending with a Sub rule such that τ′ is Abs or of the form Pre τ′_{1}.

A much more restrictive rule:

τ ▷ Abs ⟹ Top (τ, Abs)  (C-Abs)

would prevent coercion from present into absent fields. With this rule, the program

let p = if true then (Pre 1, Abs) else (Pre 1, Pre 2) in get (fst p)

would not be typable anymore. The analogy is a type system with records but no subtyping. The C-Abs rule implies that the only value of type Abs is abs. In fact, in the earlier version (consistency rule C-Pre alone) the type symbol Abs played the role of a top for all types, since the coercion τ ▷ Abs is, in this case, consistent for any τ. With rule C-Abs-Pre, Abs becomes the top of Abs and Pre types only.

Both views can be joined in a better solution where Abs and Pre are incompatible but have a top element Either:

τ ::= … | Either

                                                Either

[figure]

                                           Abs         Pre

Propagation rules are unchanged. Consistency rule may be only C-Abs, but optionally, the following consistency rule could be added:

τ ▷ Either ⟹ Top (τ, {Pre , Abs, Either})  (C-Either)

This would force Either to be the top type of Abs and Pre rather than a general top type. That is, a value of type Either is only one of the two forms abs or pre .

4 Concatenation of one-field records

We first consider the simpler case of extensible one-field records.

4.1 Extensible one-field records

We add a new primitive to the language:

b ::= … | a with a

with the following reduction rule:

                            v_{1} with v_{2} ⟶ pre v_{2}

and typing rule:

(C-With)

\frac{A ⊢ a_{1} : τ_{1} | C_{1} A ⊢ a_{2} : τ_{2} | C_{2}}{A ⊢ a_{1} with a_{2} : Pre τ_{2} | C_{1} ∪ C_{2}}

Since no values nor types have been added, there is no propagation nor consistency rules to be added either.

We could check semantic soundness by extending the proofs of for the core language. However, in this special case of one-field records, the primitive with is nothing else but fun x → fun y → Pre y. Clearly, it can be encoded in the language, and the typing rule C-Width is the one derived from the encoding. This guarantees the soundness of the extension. It also means that the power of record extension only comes from the multiplicity of fields, which we will study later.

4.2 Concatenation of one-field records

In this section we study the concatenation of one-field records. We extend the language of section 2 with a new primitive.

b ::= … | a @ a

There are different possibilities for the semantics of concatenation. Clearly, when both records are abs, their concatenation is abs. If one of them is pre v and the other one is abs, their concatenation must be pre v. The problem is what should happen when both fields are present. One obvious solution is to reject this case, and consider it to be an ill-formed program. However, many uses of concatenation show that this is a useful case, and that concatenation should be asymmetric and, for instance, return right side values by priority. This gives the following reduction rules:

v_{1} @ pre v_{2} ⟶ pre v_{2}
v_{1} @ abs ⟶ v_{1}

To get the semantics for symmetric concatenation, replace v_{1} by abs in the first rule

4.3 Concatenation without subtyping

For sake of simplification, we first study concatenation without subtyping. That is, we add rule C-Abs to the consistency rules.

As for record extension, we should not introduce new types since we have not added new values. However, the type of the concatenation of two records cannot be determined unless the types of the arguments are known themselves. We need to delay the computation of the resulting type of the concatenation of two records. This can be formalized by adding type operators (not to be confused with type constructors):

τ̄ ::= τ @ τ

These expressions are not types; they cannot occur inside type expressions but only inside (actually as the left part of) type constraints:

C ::= {} | {τ ▷ τ} | τ̄ ▷ τ | C ∪ C

We can write the following typing rule for concatenation:

(Concat) ; \frac{A ⊢ a_{1} : τ_{1} | C_{1} A ⊢ a_{2} : τ_{2} | C_{2}}{A ⊢ a_{1} @ a_{2} : τ_{3} | C_{1} ∪ C_{2} ∪ \{τ_{1} @ τ_{2} ▷ τ_{3}\}}

Delegating the difficulty to the new propagation rules:

τ_{1} @ Pre τ_{0} ▷ τ ⟹ Pre τ_{0} ▷ τ  (P-Concat-Pre)
τ_{1} @ Abs ▷ τ ⟹ τ_{1} ▷ τ  (P-Concat-Abs)
τ_{2} ▷ τ′_{2} ∧ τ_{1} @ τ′_{2} ▷ τ_{3} ⟹ τ_{1} @ τ_{2} ▷ τ_{3}  (P-Concat-R)

The two first typing rules describe the operator @. The last one, is a generalization of transitive relation for the operator, so that more precise information can be brought into the operator and propagated. It follows from the propagation rules that:

{Pre τ_{0} ▷ τ_{2}, τ_{1} @ τ_{2} ▷ τ_{3}} ⊢ Pre τ_{0} ▷ τ_{3}

and

{Abs ▷ τ_{2}, τ_{1} @ τ_{2} ▷ τ_{3}} ⊢ τ_{1} ▷ τ_{3}

The following consistency rule must also be added:

τ_{1} @ τ_{2} ▷ τ ⟹ Top (τ_{2}, {Pre , Abs})  (C-Concat-R)

Left propagation and left consistency could be defined by symmetry

τ_{1} ▷ τ′_{1} ∧ τ′_{1} @ τ_{2} ▷ τ_{3} ⟹ τ_{1} @ τ_{2} ▷ τ_{3}
τ_{1} @ τ_{2} ▷ τ ⟹ Top (τ_{1}, {Pre , Abs})  (C-Concat-L)

These rules are not mandatory, because one-field concatenation, as defined, does not require its left argument to be a one-field record. For instance, fun x → x @ abs ⟶ fun x → x. Otherwise, both rule C-Concat-L would be required would be required. In any case, they are harmeless; they could safely be added, which would only rejected a few uninteresting programs.

We show the semantics soundness of this extension by extending the proofs of section 3.

In lemma 2: there are two new cases: E is E @ a or v @ E. Each of them is treated as the App cases.

In lemma 3: the new case to consider is when a is a_{1} @ a_{2}; it is similar to the application case. More precisely, a canonical proof of (1) ends either with a Sub rule or with:

(Concat) ; \frac{A ⊢ a_{1} : τ_{1} | C_{1} A ⊢ a_{2} : τ_{2} | C_{2}}{A ⊢ a_{1} @ a_{2} : τ_{3} | C_{1} ∪ C_{2} ∪ \{τ_{1} @ τ_{2} ▷ τ_{3}\}}

where C is C_{1} ∪ C_{2} ∪ {τ_{1} @ τ_{2} ▷ τ_{3}}. By applying the induction hypothesis to both premises, we get A ⊢ a_{1}[v/x] : τ_{1} | C_{1} ∪ C_{0} (4) and A ⊢ a_{2}[v/x] : τ_{2} | C_{2} ∪ C_{0} ∪ {τ_{1} @ τ_{2} ▷ τ_{3}} (5). Since C_{1} ∪ C_{2} ∪ C_{0} is consistent, so are C_{1} ∪ C_{0} and C_{2} ∪ C_{0}. We obtain the conclusion by applying rule Concat.

In theorem 1: the new cases to consider are the following

Sous-cas a is v_{1} @ pre v_{2}: The canonical derivation ends with:

⊢ v_{1} : τ_{1} | C_{1}  ⊢ v_{2} : τ_{0} | C_{0} (Pre) ⊢ pre v_{2} : Pre τ_{0} | C_{0} (2) (Sub) ⊢ pre v_{2} : τ_{2} | C_{2}

(Concat)

⊢ v_{1} @ pre v_{2} : τ_{3} | C_{1} ∪ C_{2} ∪ {τ_{1} @ τ_{2} ▷ τ_{3}}

Where Pre τ_{0} | C_{0} ≤ τ_{2} | C_{2}, i.e. C_{2} ⊢ C_{0} ∪ {Pre τ_{0} ▷ τ_{2}}. Therefore C_{2} ∪ C_{1} ∪ {τ_{1} @ τ_{2} ▷ τ_{3}} ⊢ C_{0} ∪ {Pre τ_{0} ▷ τ_{2}, τ_{1} @ τ_{2} ▷ τ_{3}}. By transitivity and propagation, C_{2} ∪ C_{1} ∪ {τ_{1} @ τ_{2} ▷ τ_{3}} ⊢ C_{0} ∪ {Pre τ_{0} ▷ τ_{3}}. Therefore Pre τ_{0} | C_{0} ≤ τ_{3} | C_{1} ∪ C_{2} ∪ {τ_{1} @ τ_{2} ▷ τ_{3}} and we conclude from (2) with a Sub rule.

Sous-cas a is v_{1} @ abs: The canonical derivation ends with:

⊢ v_{1} : τ_{1} | C_{1} (1) \begin{matrix}⊢ abs : Abs | C_{0} \\ & (Sub) \\ ⊢ abs : τ_{2} | C_{2} \end{matrix}

(Concat)

⊢ v_{1} @ abs : τ_{1} @ τ_{2} | C_{1} ∪ C_{2}

where Abs | C_{0} ≤ τ_{2} | C_{2}, i.e. C_{2} ⊢ C_{0} ∪ {Abs ▷ τ_{2}}. By transitivity and propagation, we get C_{2} ∪ C_{1} ∪ {τ_{1} @ τ_{2} ▷ τ_{3}} ⊢ C_{0} ∪ {τ_{1} ▷ τ_{3}}. Therefore, τ_{1} | C_{0} ≤ τ_{3} | C_{1} ∪ C_{2} ∪ {τ_{1} @ t_{2} ▷ τ_{3}} and we conclude from (1) with a Sub rule.

In theorem 2: The first two parts of the theorem are unchanged.

In the last part, we must consider the case where a is a_{1} @ a_{2}. The canonical derivation of ⊢ a : τ | C ends with

A ⊢ a_{1} : τ_{1} | C_{1} A ⊢ a_{2} : τ_{2} | C_{2} (Concat)

A ⊢ a_{1} @ a_{2} : τ_{3} | C_{1} ∪ C_{2} ∪ {τ_{1} @ τ_{2} ▷ τ_{3}}

By induction hypothesis, a_{2} must be a value. Therefore there is a derivation A ⊢ a_{2} : τ′_{2} | C′_{2} that does not end with a Sub rule such that C_{2} ⊢ τ′_{2} ▷ τ_{2} and τ′_{2} is not a variable. Therefore τ_{1} @ τ′_{2} ▷τ_{3} is consistent. Since it is not a variable, it must be either Abs or of the form Pre . Therefore, a_{2} is either abs or of the form pre , and a can be reduced.

Variation

The above formalism requires a special transitivity rule. This can be avoided by noticing that coercions τ_{1} @ τ_{2}▷τ_{3} are in fact frozen until enough information on τ_{2} is known. Instead, these delayed coercions could be written τ_{2} ▷ τ_{1} @^{−1} τ_{3}, with the following propagation rules

Pre τ_{0} ▷ τ_{1} @^{−1} τ ⟹ Pre τ_{0} ▷ τ  (P-@^{−1}-Pre)
Abs ▷ τ_{1} @^{−1} τ ⟹ τ_{1} ▷ τ  (P-@^{−1}-Abs)

and the consistency rule:

τ ▷ τ_{1} @^{−1} τ_{3} ⟹ Top (τ, {Abs, Pre })  (C-@^{−1})

Type operators τ̄ now appear on the right instead of the left of constraints. In this case, the regular transitive closure is sufficient to bring supertypes of τ_{2} close to the @^{−1} operator so that further propagations may happen. The two systems are clearly equivalent.

4.4 Concatenation in the presence of subtyping

The inclusion Pre τ_{0} ▷ Abs does not combine well with concatenation. The problem is that the shape pre or abs that drives the reduction rules for @ cannot be predicted by the types since a value of type Abs may be of either shape. Consequently, it would be no more possible to tell the type of a value resulting from concatenation from the type of their arguments arguments.

This says that concatenation can only be typed if the type of the arguments have not lost any information yet. Thus, we have to distinguish between fields that are really absent and those that have been forgotten. We naturally reintroduce the type constructor Either together with its consistency rule C-Either.

It is not be difficult to check that type soundness still hold. The proofs are almost unchanged from previous section.

At the beginning of this section, we argued that type operators are used to delay propagation of concatenation constraints until enough of the shape is known to determined what branch of the concatenation will be chosen. In fact, both branches of the concatenation may be possible. For instance, consider the program:

{a = 1} @ (if true then {} else {a = t})

The question is whether the field a of the result will be taken from the left or the right argument. We may intuitively think tat this type should be rejected since the right component should be typed with Either, but Either cannot occur in the right branch of an @ operator. In fact, the program above can be typed with

α | {Pre (I) @ α′ ▷ α ∧ Abs ▷ α′ ∧ Pre (B) ▷ α}

This set is consitent. By propagation, both we have to conisder Pre (I) @ Abs ▷ α and Pre (I) @ Pre (B) ▷ α, and thus both Pre (I) ▷ α and Pre (B) ▷ α must be added in the closure. But none of this rule is inconsistent, even though the value on the field a will never be used. It is indeed correct to accept this example. Actually, it was already typable in the earlier version without Either.

If one really want to reject such pathological programs, one possibility is to had the following propagation rule:

Pre (τ) ▷ τ′ ∧ Abs ▷ τ′ ⟹ Either ▷ τ′  (P-Either-Top)

This rule says that Either is the least upper bound of Abs and Pre. Its combination with C-Concat will reject the above example as inconsistent.

5 Multiple-field records

We now solve concatenation of multiple-field records with subtyping. We assume given a denumerable collection of labels. The modification to the syntax of the language is:

\begin{matrix}b ::= & a @ a | a.ℓ \\ c ::= & \{ℓ_{i} = a_{i} ^{i∈I}\} \end{matrix}

Here, the operation a @ a means concatenation of records rather that concatenation of fields. The operation get a has been replaced by extraction a.ℓ of field ℓ from record a.

The reduction rules are

{ℓ_{i} : v_{i} ^{i∈I}}.ℓ_{i} ⟶ v_{i}, ∀i ∈ I  (R-Extract)
{ℓ_{i} : v_{i}^{1} ^{i∈I_{1}}} @ {ℓ_{i} : v_{i}^{2} ^{i∈I_{2}}} ⟶ {l_{i} : v_{i}^{1} ^{i∈I_{1}\I_{2}}, l_{i} : v_{i}^{1} ^{i∈I_{2}}}  (R-Concat)

We distinguish two kinds of record types.

τ ::= α | τ → τ
| ⟨ℓ_{i} = τ_{i} ^{i∈I}⟩  Rigid record type
| {ℓ_{i} = τ_{i} ^{i∈I}}  Flexible record type
τ̄ ::= τ @ τ

Types ⟨ℓ_{i} = τ_{i} ^{i∈I}⟩ means that no information has been forgotten yet, while {ℓ_{i} = τ_{i} ^{i∈I}} types are the usual record types.

Typing rules for records are the following:

(Record) ; \frac{A ⊢ a : τ_{i} | C_{i}}{A ⊢ \{ℓ = a\} : ⟨ℓ_{i} : τ_{i} ^{i∈I}⟩ | ⋃_{i∈I} C_{i}}  (Extract) ; \frac{A ⊢ a : \{ℓ : τ\} | C}{A ⊢ a.ℓ : τ | C}

(Concat) ; \frac{A ⊢ a_{1} : τ_{1} | C_{1} A ⊢ a_{2} : τ_{2} | C_{2}}{A ⊢ a_{1} @ a_{2} : τ_{3} | C_{1} ∪ C_{2} ∪ \{τ_{1} @ τ_{2} ▷ τ_{3}\}}

The whole set of propagation rules is P-Trans and P-Arrow plus the following ones:

⟨ℓ_{i} : τ_{i}^{1} ^{i∈I_{1}}⟩ @ ⟨ℓ_{i} : τ_{i}^{2} ^{i∈I_{2}}⟩ ▷ τ_{3} ⟹ ⟨ℓ_{i} : τ_{i}^{1} ^{i∈I_{1}\I_{2}}, ℓ_{i} : τ_{i}^{2} ^{i∈I_{2}}⟩  (P-@)
τ′_{1} ▷ τ_{1} ∧ τ_{1} @ τ_{2} ▷ τ_{3} ⟹ τ′_{1} @ τ_{2} ▷ τ_{3}  (P-@-L)
τ′_{2} ▷ τ_{2} ∧ τ_{1} @ τ_{2} ▷ τ_{3} ⟹ τ_{1} @ τ′_{2} ▷ τ_{3}  (P-@-R)
⟨ℓ_{i} : τ_{i}^{1} ^{i∈I}⟩ ▷ ⟨ℓ_{i} : τ_{i}^{2} ^{i∈I}⟩ ⟹ τ_{i}^{1} ▷ τ_{i}^{2}  (P-⟨⟩) ∀i ∈ I,
⟨ℓ_{i} : τ_{i}^{1} ^{i∈I}⟩ ▷ {ℓ_{i} : τ_{i}^{2} ^{i∈I}} ⟹ τ_{i}^{1} ▷ τ_{i}^{2}  (P-⟨⟩-{}) ∀i ∈ I,
{ℓ_{i} : τ_{i}^{1} ^{i∈I_{1}}} ▷ {ℓ_{i} : τ_{i}^{2} ^{i∈I_{2}}} ⟹ τ_{i}^{1} ▷ τ_{i}^{2}  (P-⟨⟩) ∀i ∈ I_{1} ∩ I_{2},

Consistency rules are C-Arrow plus:

τ_{1} @ τ_{2} ▷ τ ⟹ Top (τ_{1}, ⟨ ⟩) ∧ Top (τ_{2}, ⟨ ⟩)  (C-@)
τ ▷ ⟨ℓ_{i} : τ_{i} ^{i∈I}⟩ ⟹ Top (τ, ⟨ℓ_{i} : ^{i∈I}⟩)  (C-⟨⟩)
τ ▷ {ℓ_{i} : τ_{i} ^{i∈I}} ⟹ Top (τ, {ℓ_{i} : ^{i∈I∪J}}) ∨ Top (τ, ⟨ℓ_{i} : ^{i∈I}⟩)  (C-{})

Theorem 3 Typechecking is sound with respect to the reduction semantics. More precisely, both theorem 1 (subject reduction) and theorem 2 (irreducible terms) hold for this extension.

\underline{Proof}: The proof of semantic soundness has the same structure as in section 3. We complete the proofs with the new cases.

In lemma 2: there are four new cases: E @ a or v @ E, {ℓ = E} and E.ℓ. Each of them are treated as the App cases.

In lemma 3: the new cases to consider are where a is a_{1} @ a_{2}, {ℓ = a_{1}} or a_{1}.ℓ. Each of them is similar to case where a is a_{1} a_{2}.

Cas a is {ℓ_{i} : v_{i} ^{i∈I}}.ℓ_{i} where i ∈ I: The canonical derivation ends with:

A ⊢ v_{i} : τ_{i}^{0} | C_{i} ∀i ∈ I (i) (Record)

A ⊢ {ℓ_{i} : v_{i} ^{i∈I}} : ⟨ℓ_{i} : τ_{i}^{0} ^{i∈I}⟩ | ⋃_{i∈I} C_{i} (Sub)

A ⊢ {ℓ_{i} : v_{i} ^{i∈I}} : {ℓ_{i} : τ_{i}} | C \overline{(Extract)}

A ⊢ a : τ_{i} | C

where ⟨ℓ_{i} : τ_{i}^{0} ^{i∈I}⟩ | ⋃_{i∈I} C_{i} ≤ {ℓ_{i} : τ_{i}} | C. Therefore C ⊢ C_{i} ∪ {⟨ℓ_{i} : τ_{i}^{0} ^{i} ∈ I⟩ ▷ {ℓ_{i} : τ_{i}}}, and by propagation C ⊢ C_{i} ∪ {τ_{i}^{0} ▷ τ_{i}}. The conclusion follows by applying a Sub rule to the premise (i).

Cas a is {ℓ_{i} : v_{i}^{1} ^{i∈I_{1}}} @ {ℓ_{i} : v_{i}^{2} ^{i∈I_{2}}}: The canonical derivation ends with:

A ⊢ v_{i} : τ_{i}^{1} | C_{i} ∀i ∈ I_{1} (Record)

A ⊢ {ℓ_{i} : v_{i} ^{i∈I_{1}}} : ⟨ℓ_{i} : τ_{i}^{1} ^{i∈I_{1}}⟩ | ⋃_{i∈I_{1}} C_{i} (Sub)

A ⊢ {ℓ_{i} : v_{i} ^{i∈I}} : τ_{1} | C_{1}

· ; · ; · ; · ; · ; · ; ·

A ⊢ v_{i} : τ_{i}^{2} | C_{i} ∀i ∈ I_{2} \overline{(Record)}

A ⊢ {ℓ_{i} : v_{i} ^{i∈I_{2}}} : ⟨ℓ_{i} : τ_{i}^{2} ^{i∈I_{2}}⟩ | ⋃_{i∈I_{2}} C_{i} \overline{(Sub)}

A ⊢ {ℓ_{i} : v_{i} ^{i∈I}} : τ_{2} | C_{2}

[Concat]A ⊢ a : τ_{3} | C_{1} ∪ C_{2} ∪ {τ_{1} @ τ_{2} ▷ τ} (Concat)

By subtyping hypothesis and propagation, we can easily show that:

C_{1} ∪ C_{2} ⊢ ⋃_{i∈I} C_{i}^{1} ∪ ⋃_{i∈I} C_{i}^{2} ∪ {ℓ_{i} : τ_{i}^{1} ^{i∈I_{2}\I_{1}}, ℓ_{i} : τ_{i}^{2} ^{i∈I_{2}}}

Then we conclude with a record construction followed by a Sub rule.

In theorem 2: since values and types are not changed, the first two parts of the theorem are straightforward. In particular:

• if a value has type ⟨ℓ_{i} : τ, i ∈ I⟩ | C, then it is a record value with exactly fields ℓ_{i} for i in I.

• if a value has type {ℓ_{i} : τ_{i} ^{i} ∈ I} | C, then it is a record value with at least fields l_{i} for i in I.

In the last part, we must consider the following cases

Cas a is a_{1}.ℓ: The canonical derivation of A ⊢ a : τ | C ends with

A ⊢ a_{1} : {ℓ : τ} | C (Extract)

A ⊢ a : τ | C

Therefore a_{1} is a record value with at least field ℓ, and a could be reduced.

Cas a is a_{1} @ a_{2}: The canonical derivation of A ⊢ a : τ | C ends with

A ⊢ a_{1} : τ_{1} | C_{1} A ⊢ a_{2} : τ_{2} | C_{2} (Concat)

A ⊢ a_{1} @ a_{2} : τ_{3} | C_{1} ∪ C_{2} ∪ {τ_{1} @ τ_{2} ▷ τ_{3}}

By induction hypothesis, a_{2} must be a value. Therefore there is a derivation A ⊢ a_{2} : τ′_{2} | C′_{2} that does not end with a Sub rule such that C_{2} ⊢ τ′_{2} ▷ τ_{2} and τ′_{2} is not a variable. Therefore τ_{1} @ τ′_{2} ▷ τ_{3} is consistent. Since it is not a variable, it is a non flexible record type. Thus a_{2} is a record value. Similarly, a_{1} must also be a record value. Therefore a could be reduced.

The extension of record a_{1} on field ℓ with an expression a_{2} can be considered as syntactic sugar for the concatenation of a_{1} with the one field record {ℓ = a_{2}}. However, our typing rules give a weaker type than usual to record extension, since it is then only possible to extend a value of rigid type, i.e. knowing the exact information on all fields. In practice, such a restriction might be useful, since it would allow more compilation optimizations. But it is a restriction, and actually it can be removed. In record concatenation there is no reason not to allow the left argument to have a flexible type, provided the right argument has a rigid type; then the resulting record has a flexible type. This typing rule is incomparable with the one we described, since for instance with this only rule, concatenated records could not be concatenated to other records. A more general solution would include the the two rules together. This is obtained by adding the propagation rule:

{ℓ_{i} : τ_{i}^{1} ^{i∈I_{1}}} @ ⟨ℓ_{i} : τ_{i}^{2} ^{i∈I_{2}}⟩ ▷ τ_{3} ⟹ {ℓ_{i} : τ_{i}^{1} ^{i∈I_{1}\I_{2}}, ℓ_{i} : τ_{i}^{2} ^{i∈I_{2}}} ▷ τ_{3}  (P-@-{})

and change the consistency rule to:

τ_{1} @ τ_{2} ▷ τ ⟹ Top (τ_{1}, {⟨ ⟩, { }}) ∧ Top (τ_{2}, ⟨ ⟩)  (C-@)

Yet, the most general solution is a field-by-field approach to concatenation as described below.

Records as flexible products of fields

One may wonder why we did not reuse the formalism of section 4.4 for multiple field records. This leads to a more atomic presentation of record types. Moreover, it would allow to type more programs. For instance, the program

let a = {a = 1} and bc = {b = 2, c = 3} and bd = {b = 2, d = 4} in (a @ (if true then bc else bd)).b

is not typable in the previous version. The reason is that the if-expression forces to forget fields c and d in recrods bc and bd, which assigns them a flexible type. But this expression should have a rigid record type since it occurs on the right of a concatention operator.

We use the language of section 4.2, but with the following types:

τ ::= α | τ → τ | Abs | Pre τ | Either | {ℓ_{i} = τ_{i} ^{i∈I}; τ}
τ̄ ::= τ | {ℓ_{i} = τ̄_{i} ^{i∈I}; τ̄} | τ̄ @ τ̄

Types {ℓ_{i} = τ_{i} ^{i∈I}; τ} stand for records whose type of fields (including their status) is given by τ_{i} for fields ℓ_{i}’s, or τ otherwise. Moreover, we restict τ_{i} to satisfy Top (τ, {Abs, Either, Pre } and τ to be either Abs or Either. In particular, τ may not be a varibale. We identify {ℓ_{i} : τ_{i} ^{i∈I}; τ} and {ℓ_{i} : τ_{i} ^{i∈I}, ℓ : τ; τ} whenever ℓ is not one of the ℓ_{i}’s. Flexible and rigid types are recovered by taking Either or Abs for τ.

Typing rules for records are the following:

(Record)

\frac{A ⊢ a : τ_{i} | C_{i}}{A ⊢ \{ℓ = a\} : \{ℓ_{i} : Pre τ_{i} ^{i∈I}; Abs\} | ⋃_{i∈I} C_{i}}

(Extract)

\frac{A ⊢ a : \{ℓ : Pre τ; Either\} | C}{A ⊢ a.ℓ : τ | C}

(Concat) ; \frac{A ⊢ a_{1} : τ_{1} | C_{1} A ⊢ a_{2} : τ_{2} | C_{2}}{A ⊢ a_{1} @ a_{2} : τ_{3} | τ_{1} @ τ_{2} ▷ τ_{3} ∪ C_{1} ∪ C_{2}}

Propagation rules:

Pre τ_{1} ▷ Pre τ_{2} ⟹ τ_{1} ▷ τ_{2}
τ_{1} @ Pre τ_{0} ▷ τ_{3} ⟹ Pre τ_{0} ▷ τ_{3}
τ_{1} @ Abs ▷ τ_{3} ⟹ τ_{1} ▷ τ_{3}
τ′_{1} ▷ τ_{1} ∧ τ_{1} @ τ_{2} ▷ τ_{3} ⟹ τ′_{1} @ τ_{2} ▷ τ_{3}
τ′_{2} ▷ τ_{2} ∧ τ_{1} @ τ_{2} ▷ τ_{3} ⟹ τ_{1} @ τ′_{2} ▷ τ_{3}
{ℓ_{i} : τ_{i}^{1} ^{i∈I}; τ_{1}} ▷ {ℓ_{i} : τ_{i}^{2} ^{i∈I}; τ_{2}} ⟹ τ_{i}^{1} ▷ τ_{i}^{2}, i ∈ I ∧ τ_{1} ▷ τ_{2}
{ℓ_{i} : τ_{i}^{1} ^{i} ∈ I; τ_{1}} @ {ℓ_{i} : τ_{i}^{2} ^{i∈I}; τ_{2}} ▷ τ_{3} ⟹ {ℓ_{i} : τ_{i}^{1} @ τ_{i}^{2} ^{i} ∈ I; τ_{1} @ τ_{2}} ▷ τ_{3}

and consistency rules are:

τ_{1} @ τ_{2} ▷ Pre τ ⟹ Top (τ_{2}, {Abs, Pre })
τ_{1} @ τ_{2} ▷ {ℓ_{i} : τ_{i} ^{i} ∈ I; τ} ⟹ Top (τ_{1}, { }) ∧ Top (τ_{2}, { })
τ ▷ Pre τ ⟹ Top (τ, Pre )
τ ▷ Abs ⟹ Top (τ, Abs)

                         τ ▷ Either ⟹ Top (τ, {Either, Abs, Pre })

The operator @ has been overloaded, since it applies both to records and to fields, and we could have used two different operators.

Clearly, the example that we gave at the begenning of this section can now be typed.

6 Concatenation has an intersection type

A more general alternative to the @ operators is to use a restricted form of intersection types. The two reduction rules for concatenation of one field records suggests the following type for fun y → fun x → x @ y has the type (we inverted the arguments so that the significant argument comes first):

Pre τ_{2} → τ_{1} → Pre τ_{2} ∩ Abs → τ_{1} → τ_{1}

Toplevel intersection types of exclusively arrow types of incompatible domains may be solved in a general way.

The idea is to allow constraints of the form τ ▷ τ̄ where τ̄ is ⋂_{i∈I}(τ_{i} → τ′_{i}) # τ′. Such constraints can be understood

⋂_{i∈I}(τ_{i} → τ′_{i}) ▷ τ → τ′

resulting from taking an instance of an overloaded operator. The intuition is that this constraints should propagate into

τ ▷ τ_{i}[τ]′_{i} ▷ τ′

after selection of the correct branch i. However, this seltection must be delayed until enough of the structure of τ is revealed. In order to prevent several branch from beeing selected simultaneously, we restrict the formation of intersection types such that τ_{i}’s are two by two incompatible in any intersection type ⋂_{i∈I}(τ_{i} → τ′_{i}).

For instance, the concatenation function fun x, y → x @ y has the following well-formed intersection type:

⋂_{{n∈IN \atop ℓ_{i}∈L,∀i∈[1,n]}}\{ℓ_{i} : τ_{i}; i ∈ [1, n]; τ\} × \{ℓ_{i} : Pre τ′_{i}, i ∈ [1, n]; Abs\} → \{ℓ_{i} : Pre τ′_{i}, i ∈ [1, n]; τ\}

We write τ∧∨τ′ when τ and τ′ are compatible, i.e. there exits an instance of in a subtype relation with an instance the other. The propagation rule for intersection type

τ ▷ ⋂_{i∈I}(τ_{i} → τ′_{i}) # τ ⟹ τ ▷ τ′_{i} ∧ τ′_{i} ▷ τ′ (∗)  (P-∩)

fires when τ is incompatible with all τ_{j}’s but τ_{i}. The consistency rule must guarantee that the top of the structure of τ will enable selection of one branch and consequently the propagation of constraints.

τ ▷ ⋂_{i∈I}(τ_{i} → τ′_{i}) # τ′ ⟹ ∃i ∈ I, τ∧∨τ_{i}

In other words, it implies that propagation will happen soon enough so that potential errors will be detected statically (i.e. before the erroneous evaluation may happen). This phnomenom is obvious in the case of record concatenation of one field records: the two δ-rules for concatenation requires the argument (first argument after we returned them) to be a value of either shape pre v or abs. By consistency, we know that such values can have either type Pre τ or Abs. Thus, the constraints have been propagated in the corresponding branch. The consistency rule above prevents applying the @ outside of its domain, and for instance to a non record type, which would result in a non-evaluated normal form.

If σ denotes well-formed functional intersection types, the following typing rule may be added:

(Overload)

\frac{x : σ ∈ A}{A ⊢ x : α → α′ | \{α ▷ σ # α′\}}

Pre-defined operators such as @ could be turned into a language construction that would allow (some) user-defined Let-bound overloaded functions. This might be a direction to provide a type system for Castagna’s λ&-calculus [Cas94] into the contrained type framework.

The same pathological cases as discussed in section 4.4 happen here, and similarly, we may force multiple coercions to the same type to be replaced by the coercion of their least upper bound. Greatest lower bounds also play an essential role in [Cas94]

Call-by-name vs Call-by-value

The proof of semantics soundness is correct even for strategies that allow reduction under lambdas. Lemma 3 can be extended to cope with deeper reductions, but the proof becomes slightly more difficult. Record concatenation delays its evaluation until its arguments are known. Thus, it might not be equivalent to replace all functions by overloaded functions. For instance, fun y → (not (succ y)) is not well-typed. While if succ is were an overloaded function of type I → I, ithe same program would be typed with

α_{y} → B | {α_{y} ▷ I → I # α, α ▷ B}

These constraints are consistent. With a true function, the coercion α_{y} ▷I → I # α would be propagated into I ▷α before α_{y} is known to be of type I, revealing some hidden inconsistency in the constraints.

7 Discussion

We have shown the flexibility of constrained types by considering different versions of record calculi, and showing how propagation and consistency rules could be easily adapted, and in an almost systematic way Consistency rules are strongly related to the shape of values. While propagation rules are more related to reduction rules.

We could classify the reduction rules into two categories.

• Destruction rules. For instance, R-β and R-Get. The shape of input values is always known. At the level of types, the constraints can be described uniformly: the type of the result is a component of the type of the arguments.

• Reconstruction rules. This is the case of R-Concat. Input values are pattern matched and a new output value is rebuilt from them according to their shapes. It is no more possible to describe the type of the result uniformly in the type of the arguments. Conversely, its shape strongly depends on the shape of the type of the arguments.

Record concatenation is an operation of the later kind. We have used a type operator delaying the propagation of the type of the arguments until enough of their shape is known. We have also shown a connection between such type operators and simple forms of intersection types.

These simple forms of intersection types might be general enough to treat non ambiguous overloading of functions. In particular, this could applied to objects in the methods as overloaded functions paradigm. However, it is not clear yet how more general intersection types could be incorporated in the formalism, in particular as first-class types. Further research in this direction should be considered, and in particular it may help closing the gap between [EST95] and [AW93].

We have also presented a type system for concatenable records with type inference. The main idea was to enrich the lattice of types, and distinct between rigid record types that contain full type information from flexible record types that may have lost some type information. The enrichment of the lattice of types is also useful in other contexts and is studied on its own in [?]. The delaying effect of constrained types is just what is needed to prevent the combinatorial explosion that happened in [Wan89]. Compare with [Rém93b], the solution we have presented here is a direct approach; it avoids the complicated and asymmetric functionalization of record types in [Rém93b], and some related limitations. Another difference is that record types presented here are “classical” while [Rém93b] as well as [Rém93a] used a more sophiscated sorted equational theory on types and the so-called “row variables”.

The distinction between rigid and flexible types is not only essential for typing record concatenation, but also in other circumstances. For instance, the rigid type of a record gives a precise definition of its shape, which might allow compilation optimizations that would not be possible otherwise. All nods of a programs could be decorated with their best type annotations, so that inclusion on records would be used only when required, and other records treated as rigid records. This idea is not specific to records, and it could probably be applied with any subtyping structure, in particular object and variant types.

Simple variant types are known to be dual of record types (although complex pattern matching involving deeper variants make them more difficult than record types). The dual of record concatenation is concatenation of switch-functions for variants.

This study does not give any hint, however, with respect to the practice of type inference with constrained types. In particular, both the readability of types and type-error messages and the efficiency aspects of type inference, which are all related, need to be studied in more details.

Least upper bounds have appeared quite naturally in the type operators. The might also be very useful in practice by factorizing some of the computations.

References

[AW93] Alexander Aiken and Edward L. Wimmers. Type inclusion constraints and type inference. In Conference on Functional Programming Languages and Computer Architecture, pages 31–41. ACM press, 1993.

[Cas94] Giuseppe Castagna. Surcharge, Sous-typage et liaison tardive: Fondements fonctionnels de la programmation orientée objects. Doctoral dissertation (in French) Thèse de doctorat, Université de Paris 7, 1994.

[Cur90] Pavel Curtis. Constrained quantification in polymorphic type analysis. Technical Report CSL-90-1, Xerox Palo Alto Research Center, February 1990.

[EST] J. Eifrig, S. Smith, and V. Trifonov. Sound polymorphic type inference for objects. To appear in OOPSLA 1995.

[EST95] J. Eifrig, S. Smith, and V. Trifonov. Type inference for recursively constrained types and its application to OOP. In Mathematical Foundations of Programming Semantics, New Orleans, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier, 1995. To Appear. Currently available as

         ftp://ftp.cs.jhu.edu/pub/scott/ooinfer.ps.Z.

[Pal94] Jens Palsberg. Efficient type inference of object types. In Ninth Annual IEEE Symposium on Logic in Computer Science, pages 186–195, Paris, France, July 1994. IEEE Computer Society Press. To appear in Information and Computation.

[Pot95] François Pottier. Simplifying constrained types. Draft, August 1995.

[Rém93a] Didier Rémy. Type inference for records in a natural extension of ML. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1993.

[Rém93b] Didier Rémy. Typing record concatenation for free. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1993.

[Wan89] Mitchell Wand. Type inference for record concatenation and multiple inheritance. In Fourth Annual IEEE Symposium on Logic in Computer Science, pages 92–97, Pacific Grove, CA, June 1989.