1 Introduction

Intersection types [20, 43] are a popular language feature for modern languages, such as Microsoft’s TypeScript [4], Redhat’s Ceylon [1], Facebook’s Flow [3] and Scala [37]. In those languages a typical use of intersection types, which has been known for a long time [19], is to model the subtyping aspects of OO-style multiple inheritance. For example, the following Scala declaration:

figure a

says that the class A implements both B and C. The fact that A implements two interfaces/traits is captured by an intersection type between B and C (denoted in Scala by B with C). Unlike a language like Java, where implements (which plays a similar role to with) would be a mere keyword, in Scala intersection types are first class. For example, it is possible to define functions such as:

figure b

taking an argument with an intersection type B with C.

The existence of first-class intersections has led to the discovery of other interesting applications of intersection types. For example, TypeScript’s documentation motivates intersection typesFootnote 1 as follows:

You will mostly see intersection types used for mixins and other concepts that don’t fit in the classic object-oriented mold. (There are a lot of these in JavaScript!)

Two points are worth emphasizing. Firstly, intersection types are being used to model concepts that are not like the classical (class-based) object-oriented programming. Indeed, being a prototype-based language, JavaScript has a much more dynamic notion of object composition compared to class-based languages: objects are composed at run-time, and their types are not necessarily statically known. Secondly, the use of intersection types in TypeScript is inspired by common programming patterns in the (dynamically typed) JavaScript. This hints that intersection types are useful to capture certain programming patterns that are out-of-reach for more conventional type systems without intersection types.

Central to TypeScript’s use of intersection types for modelling such a dynamic form of mixins is the function:

figure c

The name extend is given as an analogy to the extends keyword commonly used in OO languages like Java. The function takes two objects (first and second) and produces an object with the intersection of the types of the original objects. The implementation of extend relies on low-level (and type-unsafe) features of JavaScript. When a method is invoked on the new object resulting from the application of extend, the new object tries to use the first object to answer the method call and, if the method invocation fails, it then uses the second object to answer the method call.

The extend function is essentially an encoding of the merge operator. The merge operator is used on some calculi [17, 24, 38, 47, 48] as an introduction form for intersection types. Similar encodings to those in TypeScript have been proposed for Scala to enable applications where the merge operator also plays a fundamental role [39, 46]. Unfortunately, the merge operator is not directly supported by TypeScript, Scala, Ceylon or Flow. There are two possible reasons for such lack of support. One reason is simply that the merge operator is not well-known: many calculi with intersection types in the literature do not have explicit introduction forms for intersection types. The other reason is that, while powerful, the merge operator is known to introduce (in)coherence problems [24, 47]. If care is not taken, certain programs using the merge operator do not have a unique semantics, which significantly complicates reasoning about programs.

Solutions to the problem of coherence in the presence of a merge operator exist for simply typed calculi [17, 38, 47, 48], but no prior work addresses polymorphism. Most recently, we proposed using disjoint intersection types [38] to guarantee coherence in : a simply typed calculus with intersection types and a merge operator. The key idea is to allow only disjoint types in intersections. If two types are disjoint then there is no ambiguity in selecting a value of the appropriate type from an intersection, guaranteeing coherence.

Combining parametric polymorphism with disjoint intersection types, while retaining enough flexibility for practical applications, is non-trivial. The key issue is that when a type variable occurs in an intersection type it is not statically known whether the instantiated types will be disjoint to other components of the intersection. A naive way to add polymorphism is to forbid type variables in intersections, since they may be instantiated with a type which is not disjoint to other types in an intersection. Unfortunately this is too conservative and prevents many useful programs, including the extend function, which uses an intersection of two type variables T and U.

This paper presents : a core calculus with disjoint intersection types, a variant of parametric polymorphism and a merge operator. The key innovation in the calculus is disjoint polymorphism: a constrained form of parametric polymorphism, which allows programmers to specify disjointness constraints for type variables. With disjoint polymorphism the calculus remains very flexible in terms of programs that can be written with intersection types, while retaining coherence. In the extend function is implemented as follows:

figure d

From the typing point of view, the difference between extend in TypeScript and is that the type variable U now has a disjointness constraint. The notation U * T means that the type variable U can be instantiated to any types that is disjoint to the type T. Unlike TypeScript, the definition of extend is trivial, type-safe and guarantees coherence by using the built-in merge operator (,,).

The applicability of is illustrated with examples using extend ported from TypeScript, and various operations on polymorphic extensible records [29, 31, 34]. The operations on polymorphic extensible records show that can encode various operations of row types [52]. However, in contrast to various existing proposals for row types and extensible records, supports general intersections and not just record operations.

and the proofs of coherence and type-safety are formalized in the Coq theorem prover [2]. The proofs are complete except for a minor (and trivially true) variable renaming lemma used to prove the soundness between two subtyping relations used in the formalization. The problem arizes from the combination of the locally nameless representation of binding [7] and existential quantification, which prevents a Coq proof for that lemma.

In summary, the contributions of this paper are:

  • Disjoint Polymorphism: A novel form of universal quantification where type variables can have disjointness constraints. Disjoint polymorphism enables a flexible combination of intersection types, the merge operator and parametric polymorphism.

  • Coq Formalization of and Proof of Coherence: An elaboration semantics of System into System F is given. Type-soundness and coherence are proved in Coq. The proofs for these properties and all other lemmata found in this paper are available at: https://github.com/jalpuim/disjoint-polymorphism.

  • Applications: We show how provides basic support for dynamic mixins and various operations on polymorphic extensible records.

2 Overview

This section introduces and its support for intersection types, parametric polymorphism and the merge operator. It then discusses the issue of coherence and shows how the notion of disjoint intersection types and disjoint quantification achieves a coherent semantics. This section uses some syntactic sugar, as well as standard programming language features, to illustrate the various concepts in . Although the minimal core language that we formalize in Sect. 4 does not present all such features and syntactic sugar, these are trivial to add.

2.1 Intersection Types and the Merge Operator

Intersection Types. The intersection of type and (denoted by A & B in ) contains exactly those values which can be used as both values of type and of type . For instance, consider the following program in :

figure e

If a value x has type Int & Bool then x can be used anywhere where either a value of type Int or a value of type Bool is expected. This means that, in the program above the functions succ and not – simple functions on integers and booleans, respectively – both accept x as an argument.

Merge Operator. The previous program deliberately omitted the introduction of values of an intersection type. There are many variants of intersection types in the literature. Our work follows a particular formulation, where intersection types are introduced by a merge operator [17, 24, 38, 47, 48]. As Dunfield [24] has argued a merge operator adds considerable expressiveness to a calculus. The merge operator allows two values to be merged in a single intersection type. For example, an implementation of x in is 1,,True. Following Dunfield’s notation the merge of and is denoted by .

2.2 Coherence and Disjointness

Coherence is a desirable property for a semantics. A semantics is coherent if any valid program has exactly one meaning [47] (that is, the semantics is not ambiguous). Unfortunately the implicit nature of elimination for intersection types built with a merge operator can lead to incoherence. This is due to intersections with overlapping types, as in . The result of the program ((1,,2) : Int) can be either 1 or 2, depending on the implementation of the language.

Disjoint Intersection Types. One option to restore coherence is to reject programs which may have multiple meanings. The calculus [38] – a simply-typed calculus with intersection types and a merge operator – solves this problem by using the concept of disjoint intersections. The incoherence problem with the expression happens because there are two overlapping integers in the merge. Generally speaking, if both terms can be assigned some type then both of them can be chosen as the meaning of the merge, which in its turn leads to multiple meanings of a term. Thus a natural option is to forbid such overlapping values of the same type in a merge. In intersections such as Int&Int are forbidden, since the types in the intersection overlap (i.e. they are not disjoint). However an intersection such as Char&Int is ok because the set of characters and integers are disjoint to each other.

2.3 Parametric Polymorphism

Unfortunately, combining parametric polymorphism with disjoint intersection types is non-trivial. Consider the following program (uppercase Latin letters denote type variables):

figure f

The merge3 function takes an argument x of some type (A) and merges x with 3. Thus the return type of the program is A & Int. merge3 is unproblematic for many possible instantiations of A. However, if merge3 instantiates A with a type that overlaps (i.e. is not disjoint) with Int, then incoherence may happen. For example:

figure g

can evaluate to both 2 or 3.

Forbidding Type Variables in Intersections. A naive way to ensure that only programs with disjoint types are accepted is simply to forbid type variables in intersections. That is, an intersection type such as Char&Int would be accepted, but an intersection such as A & Int (where A is some type variable) would be rejected. The reasoning behind this design is that type variables can be instantiated to any types, including those already in the intersection. Thus forbidding type variables in the intersection will prevent invalid intersections arising from instantiations with overlapping types. Such design does guarantee coherence and would prevent merge3 from type-checking. Unfortunately the big drawback is that the design is too conservative and many other (useful) programs would be rejected. In particular, the extend function from Sect. 1 would also be rejected.

Other Approaches. Another option to mitigate the issues of incoherence, without the use of disjoint intersection types, is to allow for a biased choice: multiple values of the same type may exist in an intersection, but an implementation gives preference to one of them. The encodings of merge operators in TypeScript and Scala [39, 46] use such an approach. A first problem with this approach, which has already been pointed out by Dunfield [24], is that the choice of the corresponding value is tied up to a particular choice in the implementation. In other words incoherence still exists at the semantic level, but the implementation makes it predictable which overlapping value will be chosen. From the theoretical point-of-view it would be much better to have a clear, coherent semantics, which is independent from concrete implementations. Another problem is that the interaction between biased choice and polymorphism can lead to counter-intuitive programs, since instantiation of type-variables affects the type-directed lookup of a value in an intersection.

2.4 Disjoint Polymorphism

To avoid being overly conservative, while still retaining coherence in the presence of parametric polymorphism and intersection types, uses disjoint polymorphism. Inspired by bounded quantification [14], where a type variable is constrained by a type bound, disjoint polymorphism allows type variables to be constrained so that they are disjoint to some given types.

With disjoint quantification a variant of the program , which is accepted by , is written as:

figure h

In this variant the type A can be instantiated to any types disjoint to Int. Such restriction is expressed by the notation A * Int, where the left-side of * denotes the type variable being declared (A), and the right-side denotes the disjointness constraint (Int). For example,

figure i

is accepted. However, instantiating A with Int fails to type-check.

Multiple Constraints. Disjoint quantification allows multiple constraints. For example, the following variant of merge3 has an additional boolean in the merge:

figure j

Here the type variable A needs to be disjoint to both Int and Bool. In such constraint is specified using an intersection type Int & Bool. In general, multiple constraints are specified with an intersection of all required constraints.

Type Variable Constraints. Disjoint quantification also allows type variables to be disjoint to previously defined type variables. For example, the following program is accepted by :

figure k

The program has two type variables A and B. A is unconstrained and can be instantiated with any type. However, the type variable B can only be instantiated with types that are disjoint to A. The constraint on B ensures that the intersection type A & B is disjoint for all valid instantiations of and . In other words, only coherent uses of fst will be accepted. For example, the following use of fst:

figure l

is accepted since Int and Char are disjoint, thus satisfying the constraint on the second type parameter of fst. Furthermore, problematic uses of fst, such as:

figure m

are rejected because Int is not disjoint with Int, thus failing to satisfy the disjointness constraint on the second type parameter of fst.

Empty Constraint. The type variable in the fst function has no constraint. In this actually means that should be associated with the empty constraint, which raises the question: which type should be used to represent such empty constraint? Or, in other words, which type is disjoint to every other type? It is obvious that this type should be one of the bounds of the subtyping lattice: either or . The essential intuition here is that the more specific a type in the subtyping relation is, the less types exist that are disjoint to it. For example, is disjoint to all types except the n-ary intersections that contain , and ; while is disjoint to all types that do not contain \(\texttt {Int}\) or , and . This reasoning that should be treated as the empty constraint. Indeed, in , a single type variable is only syntactic sugar for .

3 Applications

is illustrated with two applications. The first application shows how to mimic some of TypeScript’s examples of dynamic mixins in . The second application shows how enables a powerful form of polymorphic extensible records.

3.1 Dynamic Mixins

TypeScript is a language that adds static type checking to JavaScript. Amongst numerous static typing constructs, TypeScript supports a form of intersection types, without a merge operator. However, it is possible to define a function extend that mimics the merge operator:

figure n

In this example, taken from TypeScript’s documentationFootnote 2, an extend function is defined for mixin composition. Two classes Person and ConsoleLogger are also defined. Two instances of those classes are then composed in a variable jim with the type of the intersection of both using extend. It is type-safe to access both the properties from Person and ConsoleLogger in the object jim.

TypeScript’s implementation of extend relies on a biased choice. The function starts by creating a variable result with the type of the intersection. It then iterates through first’s properties and copies them to result. Next, it iterates through second’s properties but it only copies the properties that result does not possess yet (i.e. the ones present in first). This means that the implementation is left-biased, as the properties of left type of the intersection are chosen in favor of the ones in the right. However, in TypeScript this may be a cause of severe problems since that, at the time of writing, intersections at type-level are right-biased! For example, the following code is well-typed:

figure o

There are a few problems here. Firstly both Dog and Person contain a name field, and the use of extend will favour the name field in the first object. This could be surprising for someone unfamiliar with the semantics of extend and, more importantly, it could easily allow unintended name clashes to go undetected. Secondly, note how fool.male is statically bound to a variable of type boolean but, at run-time, it will contain a value of type String! Thus the example shows some run-time type errors can still occur when using extend.

Other problematic issues regarding the semantics of intersection types can include the order of the types in an intersection, or even intersections including repeated types. This motivates the need to define a clear meaning for the practical application of intersection types.

Dynamic Mixins in . In , the merge operator is built-in. Thus extend is simply defined as follows:

figure p

The disjointness constraint on U ensures that no conflicts (such as duplicated fields of the same type) exists when merging the two objects. In practice this approach is quite similar to trait-based OO approaches [50]. If conflicts exist when two objects are composed, then they have to be resolved manually (by dropping fields from some object, for example). Moreover if no existing implementation can be directly reused, a new one must be provided via record extension, analogously to standard method overriding in OO languages.

For the previous TypeScript examples, assuming a straightforward translation from objects to (polymorphic) records, then the composition of person and consoleLogger is well-typed in :

figure q

However, the intersection Dog & Person is not accepted. This is due to both types sharing a field with the same name (name) and the same type (). Note that the name clash between male fields (which have different types) does not impose any problem in this example: allows and keeps duplicated fields whose types are disjoint. This feature of is further illustrated next.

3.2 Extensible Records

can encode polymorphic extensible records. Describing and implementing records within programming languages is certainly not novel and has been extensively studied in the past, including systems with row types [52, 53]; predicates [28,29,30]; flags [45]; conditional constraints [42]; cases [10]; amongst others. However, while most systems have non-trivial built-in constructs to model various aspects of records, specializes the more general notion of intersection types to encode complex records.

Records and Record Operations in . Systems with records usually rely on 3 basic operations: selection, restriction and extension/concatenation. Selection and concatenation (via the merge operator) are built-in in the semantics of . Merges in can be viewed as a generalization of record concatenation. In , following well-known encodings of multi-field records in systems with intersection types and a merge operator [47, 48], there are only three rather simple constructs for records: (1) single field record types; (2) single field records; (3) field accessors. Multi-field records in are encoded with intersections and merges of single field records. An example is already illustrated in Sect. 3.1. The record type Person is the intersection of two single field record types. The record person "Jim" true is built with a merge of two single field records. Finally, jim.name and jim.log illustrates the use of field accessors. Note how, through the use of subtyping, accessors will accept any intersection type that contains the single record with the corresponding field. This resembles systems with record subtyping [15, 41].

Restriction via Subtyping. In contrast to most record systems, restriction is not directly embedded in . Instead, uses subtyping for restriction:

figure r

The function remove drops the field age from the record x.

Polymorphic Extensible Records. Records in can have polymorphic fields, and disjointness enables encoding various operations expressible in systems with polymorphic records. For example, the following variant of remove

figure s

takes a value x which contains a record of type l : A, as well as some extra information of type B. The disjointness constraint on B ensures that values of type B do not contain a record with type l : A. This example shows that one can use disjoint quantification to express negative field information, which is very close to the system described by Harper and Pierce [29]. Note, however, that requires explicitly stating the type of field in the constraint, whereas systems with a lacks (field) predicate only require the name of the field. The generality of disjoint intersection types, which allows one to encode record types, is exactly what forces us to add this extra type in the constraint. However, there is a slight gain with ’s approach: allows B to contain fields with label , as long as the field types are disjoint to . Such fine-grained constraint is not possible to express only with a lacks predicate.

Expressibility. As noted by Leijen [34], systems can typically be categorized into two distinct groups in what concerns extension: strict and free. The former does not allow field overriding when extending a record (i.e. one can only extend a record with a field that is not present in it); while the latter does account for field overriding. Our system can be seen as hybrid of these two kinds of systems.

With lightweight extensible records [31] – a system with strict extension – an example of a function that uses record types is the following:

figure t

The type signature says that any record , containing fields and and some more information (which lacks both fields and ), can be accepted returning an integer. Note how the bounded polymorphism is essential to ensure that does not contain nor .

On the other hand, in Leijen’s [34] system with free extension the more general program would be accepted:

figure u

In this case, if contains either field or field , they would be shadowed by the labels present in the type signature. In other words, in a record with multiple fields, the most recent (i.e. left-most) is used in any function which accesses .

In the following program can written instead:

figure v

Since accepts duplicated fields as long as the types of the overlapping fields are disjoint, more inputs are accepted by this function than in the first system. However, since Leijen’s system accepts duplicated fields even when types are overlapping, accepts less types than . Another major difference between and the two other mentioned systems, is the ability to combine records with arbitrary types. Our system does not account for well-formedness of record types as the other two systems do (i.e. using a special row kind), since our encoding of records piggybacks on the more general notion of disjoint intersection types.

4 The Calculus

This section presents the syntax, subtyping, and typing of : a calculus with intersection types, parametric polymorphism, records and a merge operator. This calculus is an extension of the calculus [38], which is itself inspired by Dunfield’s calculus [24]. extends with (disjoint) polymorphism.

4.1 Syntax

The syntax of (with the differences to highlighted in gray) is:

Types. Metavariables , range over types. Types include all constructs in : a top type ; the type of integers ; function types ; and intersection types . The main novelty are two standard constructs of System used to support polymorphism: type variables and disjoint (universal) quantification . Unlike traditional universal quantification, the disjoint quantification includes a disjointness constraint associated to a type variable . Finally, also includes singleton record types, which consist of a label and an associated type . We will use to denote the capture-avoiding substitution of for inside and for sets of free type variables.

Terms. Metavariables range over terms. Terms include all constructs in : a canonical top value ; integer literals ; variables , lambda abstractions (); applications (); and the merge of terms and denoted as . Terms are extended with two standard constructs in System : abstraction of type variables over terms ; and application of terms to types . The former also includes an extra disjointness constraint tied to the type variable , due to disjoint quantification. Singleton records consists of a label and an associated term . Finally, the accessor for a label in term is denoted as .

Contexts. Typing contexts track bound type variables with disjointness constraints ; and variables with their type . We will use to denote the capture-avoiding substitution of for in the co-domain of where the domain is a type variable (i.e. all disjointness constraints). Throughout this paper, we will assume that all contexts are well-formed. Importantly, besides usual well-formedness conditions, in well-formed contexts type variables must not appear free within its own disjointness constraint.

Syntactic Sugar. In we may quantify a type variable and omit its constraint. This means that its constraint is . For example, the function type is syntactic sugar for . This is discussed in more detail in Sect. 6.

Fig. 1.
figure 1

Subtyping rules of .

Full size image

4.2 Subtyping

The subtyping rules of the form are shown in Fig. 1. At the moment, the reader is advised to ignore the gray-shaded parts, which will be explained later. Some rules are ported from : , , , , and .

Polymorphism and Records. The subtyping rules introduced by refer to polymorphic constructs and records. defines subtyping as a reflexive relation on type variables. In S\(\forall \) a universal quantifier (\(\forall \)) is covariant in its body, and contravariant in its disjointness constraints. The rule says that records are covariant within their fields’ types. The subtyping relation uses an auxiliary unary ordinary relation, which identifies types that are not intersections. The conditions on two of the intersection rules are necessary to produce unique coercions [38]. The relation needs to be extended with respect to . As shown at the top of Fig. 1, the new types it contains are type variables, universal quantifiers and record types.

Properties of Subtyping. The subtyping relation is reflexive and transitive.

Lemma 1

(Subtyping reflexivity). For any type , .

Proof

By structural induction on .\(\Box \)

Lemma 2

(Subtyping transitivity). If and , then .

Proof

By double induction on both derivations.\(\Box \)

4.3 Typing

Well-Formedness. The well-formedness rules are shown in the top part of Fig. 2. The new rules over are and . Their definition is quite straightforward, but note that the constraint in the latter must be well-formed.

Typing Rules. Our typing rules are formulated as a bi-directional type-system. Just as in , this ensures the type-system is not only syntax-directed, but also that there is no type ambiguity: that is, inferred types are unique. The typing rules are shown in the bottom part of Fig. 2. Again, the reader is advised to ignore the gray-shaded parts, as these will be explained later. The typing judgements are of the form: and . They read: “in the typing context , the term can be checked or inferred to type , respectively. The rules ported from are the check rules for , integers , variables , application , merge operator , annotations ; and infer rules for lambda abstractions , and the subsumption rule .

Disjoint Quantification. The new rules, inspired by System , are the infer rules for type application , and for type abstraction . Type abstraction is introduced by the big lambda , eliminated by the usual type application . The disjointness constraint is added to the context in . During a type application, the type system makes sure that the type argument satisfies the disjointness constraint. Type application performs an extra check ensuring that the type to be instantiated is compatible (i.e. disjoint) with the constraint associated with the abstracted variable. This is important, as it will retain the desired coherence of our type-system; and it will be further explained in Sect. 5. For ease of discussion, also in , we require the type variable introduced by the quantifier to be fresh. For programs with type variable shadowing, this requirement can be met straightforwardly by variable renaming.

Records. Finally, and deal with record types. The former infers a type for a record with label if it can infer a type for the inner expression; the latter says if one can infer a record type from an expression , then it is safe to access the field , and inferring type .

Fig. 2.
figure 2

Well-formedness and type system of .

Full size image
Fig. 3.
figure 3

Algorithmic disjointness.

Full size image

5 Disjointness

Section 4 presented a type system with disjoint intersection types and disjoint quantification. In order to prove both type-safety and coherence (in Sect. 6), it is necessary to first introduce a notion of disjointness, considering polymorphism and disjointness quantification. This section presents an algorithmic set of rules for determining whether two types are disjoint. After, it will show a few important properties regarding substitution, which will turn out to be crucial to ensure both type-safety and coherence. Finally, it will discuss the bounds of disjoint quantification and what implications they have on .

5.1 Algorithmic Rules for Disjointness

The rules for the disjointness judgement are shown in Fig. 3, which consists of two judgements.

Main Judgement. The judgement says two types and are disjoint in a context . The rules are inspired in the disjointness algorithm described by . and say that any type is disjoint to . This is a major difference to , where the notion of disjointness explicitly forbids the presence of types in intersections. We will further discuss this difference in Sect. 6.

Type variables are dealt with two rules: is the base rule; and is its twin symmetrical rule. Both rules state that a type variable is disjoint to some type , if contains any subtype of the corresponding disjointness constraint. This rule is a specialization of the more general lemma:

Lemma 3

(Covariance of disjointness). If and , then .

Proof

By double induction, first on the disjointness derivation and then on the subtyping derivation. The first induction case for  does not need the second induction as it is a straightforward application of subtyping transitivity.\(\Box \)

The lemma states that if a type is disjoint to under , then it is also disjoint to any supertype of . Note how these two variable rules would allow one to prove , for any variable . However, under the assumption that contexts are well-formed, such derivation is not possible as cannot occur free in .

The rule for disjoint quantification is the most interesting. To illustrate this rule, consider the following two types:

When are these two types disjoint? In the first type cannot be instantiated with and in the second case cannot be instantiated with . Therefore for both bodies to be disjoint, cannot be instantiated with either or . The rule for disjoint quantification adds a constraint composed of the intersection of both constraints into and checks for disjointness in the bodies under that environment. The reader might notice how this intersection does not necessarily need to be well-formed, in the sense that the types that compose it might not be disjoint. This is not problematic because the intersections present as constraints in the environment do not contribute directly to the (coherent) coercions generated by the type-system. In other words, intersections play two different roles in , as:

  1. 1.

    Types: restricted (i.e. disjoint) intersections are required to ensure coherence.

  2. 2.

    Constraints: arbitrary intersections are sufficient to serve as constraints under polymorphic instantiation.

The rules and define disjointness between two single label records. If the labels coincide, then the records are disjoint whenever their fields’ types are also disjoint; otherwise they are always disjoint. Finally, the remaining rules are identical to the original rules.

Axioms. Axiom rules take care of two types with different language constructs. These rules capture the set of rules is that holds for all two types of different constructs unless any of them is an intersection type, a type variable, or . Note that disjointness with type variables is already captured by and , and disjointness with the type is captured by and .

5.2 Well-Formed Types

In it is important to show that the type-system only produces well-formed types. This is crucial to ensure coherence, as shown in Sect. 6. However, in the presence of both polymorphism and disjoint intersection types, extra effort is needed to show that all types in are well-formed. To achieve this, not only we need to show that a weaker version of the general substitution lemma holds, but also that disjointness between two types is preserved after substitution. To motivate the former (i.e. why general substitution does not hold in ), consider the type . The type variable cannot be substituted by any type: substituting with will lead to the ill-formed type . To motivate the latter, consider the judgement . After the substitution of for on the two types, the sentence is no longer true, since is clearly not disjoint with itself. Generally speaking, a careless substitution can violate the constraints in the context. However, if appropriate disjointness pre-conditions are met, then disjointness can be preserved. More formally, the following lemma holds:

Lemma 4

(Disjointness is stable under substitution). If and and and well-formed context , then .

Proof

By induction on the disjointness derivation of and . Special attention is needed for the variable case, where it is necessary to prove stability of substitution for the subtyping relation. It is also needed to show that, if and do not contain any variable , then it is safe to make a substitution in the co-domain of the environment.\(\Box \)

We can now prove a weaker version of the general substitution lemma:

Lemma 5

(Types are stable under substitution). If and and and and well-formed context , then .

Proof

By induction on the well-formedness derivation of . The intersection case requires the use of Lemma 4. Also, the variable case required proving that if does not occur free in , and it is safe to substitute it in the co-domain of , then it is safe to perform the substitution.\(\Box \)

Now we can finally show that all types produced by the type-system are well-formed and, more specifically, justify that the disjointness premise on is sufficient for that purpose. More formally, we have that:

Lemma 6

(Well-formed typing). We have that:

  • If .

  • If .

Proof

By induction on the derivation and applying Lemma 5 in the case of .\(\Box \)

Even though the meta-theory is consistent, we can still ask: what are the bounds of disjoint quantification? In other words, which type(s) can be used to allow unrestricted instantiation, and which one(s) will completely restrict instantiation? As the reader might expect, the answer is tightly related to subtyping.

5.3 Bounds of Disjoint Quantification

Substitution raises the question of what range of types can be instantiated for a given variable , under a given context . To answer this question, we ask the reader to recall the rule , copied below:

Given that the cardinality of ’s types is infinite, for the sake of this example we will restrict the type universe to a finite number of primitive types (i.e. ), disjoint intersections of these types, and . Now we may ask: how many suitable types are there to instantiate with, depending on ? The rule above tells us that the more super-types has, the more types has to be disjoint with. In other words, the choices for instantiating are inversely proportional to the number of super-types of . It is easy to see that the number of super-types of is directly proportional to the number of intersections in . For example, taking as leads to be either or ; whereas as leaves as either , or . Thus, the choices of are inversely proportional to the number of intersections in . Following the same logic, choosing (i.e. the 0-ary intersection) as constraint leaves with the most options for instantiation; whereas (i.e. the infinite intersection) will deliver the least options. Consequently, we may conclude that is the empty constraint: a variable associated to it can be instantiated to any well-formed type. It is a subtle but very important property, since is a generalization of System . Any type variable quantified in System , can be quantified equivalently in by assigning it a disjointness constraint (as seen in Sect. 2.4).

6 Semantics, Coherence and Type-Safety

This section discusses the elaboration semantics of and proves type-safety and coherence. It will first show how the semantics is described by an elaboration to System . Then, it will discuss the necessary extensions to retain coherence, namely in the coercions of top-like types; coercive subtyping, and bidirectional type-system’s elaboration.

6.1 Target Language

The dynamic semantics of the call-by-value is defined by means of a type-directed translation to an extension of System with pairs. The syntax and typing of our target language is unsurprising:

The highlighted part shows its difference with the standard System . The interested reader can find the formalization of the full target language syntax and typing rules in our Coq development.

Type and Context Translation. Figure 4 defines the type translation function from types to target language types . The notation \(|\cdot |\) is also overloaded for context translation from contexts to target language contexts .

Fig. 4.
figure 4

Type and context translation.

Full size image

6.2 Coercive Subtyping and Coherence

Coercive Subtyping. The judgement present in Fig. 1, extends the subtyping relation with a coercion on the right hand side of . A coercion is just a term in the target language and is ensured to have type (by Lemma 7). For example, , generates a target coercion function with type: .

Rules , , ,, , , and are taken directly from . In rule , the coercion is simply the identity function. Rule elaborates disjoint quantification, reusing only the coercion of subtyping between the bodies of both types. Rule elaborates records by simply reusing the coercion generated between the inner types. Finally, all rules produce type-correct coercions:

Lemma 7

(Subtyping rules produce type-correct coercions). If , then .

Proof

By a straightforward induction on the derivation.\(\Box \)

Unique Coercions. In order to prove the type-system coherent, the subtyping relation also needs to be shown coherent. In the following lemma holds:

Lemma 8

(Unique subtype contributor). If , where and are well-formed types, and is not top-like, then it is not possible that the following holds at the same time:

  1. 1.
  2. 2.

Proof

By double induction: the first on the disjointness derivation (which follows from being well-formed); the second on type . The variable cases and needed to show that, for any two well-formed and disjoint types and , and is not toplike, then cannot be a subtype of .\(\Box \)

Using this lemma, we can show that the coercion of a subtyping relation is uniquely determined. This fact is captured by the following lemma:

Lemma 9

(Unique coercion). If , where and are well-formed types, then .

Proof

By induction on the first derivation and case analysis on the second.\(\Box \)

6.3 Top-Like Types and Their Coercions

Lemma 8, which is fundamental in the proof of coherence of subtyping, holds under the condition that is not a top-like type. Top-like types in include as well as other syntactically different types that behave as (such as ). It is easy to see that the unique subtyping contributor lemma is invalidated if no restriction on top-like types exists. Since every type is a subtype of then, without the restriction, the lemma would never hold.

Rules. ’s definition of top-like types extends that from . The rules that compose this unary relation, denoted as , are presented at the top of Fig. 5. The new rules are and . Both rules say that their constructs are top-like whenever their enclosing expressions are also top-like.

Fig. 5.
figure 5

Top-like types and their coercions.

Full size image

Coercions for Top-Like Types. Coercions for top-like types require special treatment for retaining coherence. Although Lemma 8 does not hold for top-like types, we can still ensure that that any coercions for top-like types are unique, even if multiple derivations exist. The meta-function , shown at the bottom of Fig. 5, defines coercions for top-like types. With respect to the record and \(\forall \) cases are now defined, and there is also a change in the & case (covering types such as ). With this definition, although two derivations exist for type , they both generate the coercion .

Allowing Overlapping Top-Like Types in Intersections. In is a well-formed disjoint intersection type. This may look odd at first, since all other types cannot appear more than once in an intersection. Indeed, in , is not well-formed. However, -types are special in that they have a unique canonical top value, which is translated to the unit value () in the target language. In other words a merge of two -types will always return the same value regardless of which component of the merge is chosen. This is different from merges of non -types, which do not have this property. Thus, one may say that -types are coherent with every other type. This property makes -types perfect candidates for the empty constraint, but such can only be achieved by allowing in intersections. This explains the more liberal treatment of top types when compared to .

6.4 Elaboration of the Type-System and Coherence

In order to prove the coherence result, we refer to the bidirectional type-system introduced in Sect. 4. The bidirectional type-system is elaborating, producing a term in the target language while performing the typing derivation.

Key Idea of the Translation. This translation turns merges into usual pairs, similar to Dunfield’s elaboration approach [24]. It also translates the form of disjoint quantification and disjoint type application into regular (polymorphic) quantification and type application. For example, in will be translated into System ’s .

The Translation Judgement. The translation judgement extends the typing judgement with an elaborated term on the right hand side of . The translation ensures that has type . The two rules for type abstraction and type application generate the expected corresponding coercions in System F. The coercions generated for and simply erase the labels and translate the corresponding underlying term. All the remaining rules are ported from .

Type-Safety. The type-directed translation is type-safe. This property is captured by the following two theorems.

Theorem 1

(Type preservation). We have that:

  • If , then .

  • If , then .

Proof

By structural induction on the term and the respective inference rule.\(\Box \)

Theorem 2

(Type safety). If is a well-typed term, then evaluates to some System value .

Proof

Since we define the dynamic semantics of in terms of the composition of the type-directed translation and the dynamic semantics of System , type safety follows immediately.\(\Box \)

Uniqueness of Type-Inference. An important property of the bidirectional type-checking is that, given an expression , if it is possible to infer a type for it, then has a unique type.

Theorem 3

(Uniqueness of type-inference). If and , then .

Proof

By structural induction on the term and the respective inference rule.\(\Box \)

Coherency of Elaboration. Combining the previous results, we are finally able to show the central theorem:

Theorem 4

(Unique elaboration). We have that:

  • If , then .

  • If , then .

(“\(\equiv \)” means syntactical equality, up to -equality.)

Proof

By induction on the first derivation. The most important case is the subsumption rule:

We need to show that is unique (by Lemma 9), and thus to show that is well-formed (by Lemma 6). Note that this is the place where stability of substitutions (used by Lemma 6) plays a crucial role in guaranteeing coherence. We also need to show that is unique (by Theorem 3). Uniqueness of is needed to apply the induction hypothesis.\(\Box \)

7 Related Work

Intersection Types, Polymorphism and the Merge Operator. To our knowledge no previous work presents a coherent calculus which includes parametric polymorphism, intersection types and a merge operator. Only Pierce’s  [40] supports intersection types, polymorphism and, as an extension, the merge operator (called in ). However, with such extension, is incoherent. Various simply typed systems with intersections types and a merge operator have been studied in the past. The merge operator was first introduced by Reynold’s in the Forsythe [48] language. The merge operator in Forsythe is coherent [47], but it has various restrictions to ensure coherence. For example Forsythe merges cannot contain more than one function. Many of those restrictions are lifted in . Castagna et al. [17] studied a coherent calculus with a special merge operator that works on functions only. The goal was to model function overloading. Unlike Reynold’s operator, multiple functions are allowed in merges, but non-functional types are forbidden. More recently, Dunfield [24] formalised a system with intersection types and a merge operator with a type-directed translation to the simply-typed lambda calculus with pairs. Although Dunfield’s calculus is incoherent, it was the inspiration for the calculus [38], which extends.

solves the coherence problem for a calculus similar to Dunfield’s, by requiring that intersection types can only be composed of disjoint types. uses a specification for disjointness, which says that two types are disjoint if they do not share a common supertype. does not use such specification as its adaptation to polymorphic types would require using unification, making the specification arguably more complex than the algorithmic rules (and defeating the purpose of having a specification). ’s notion of disjointness is based on ’s more general notion of disjointness concerning types, called -disjointness. -disjointness states that two types and are disjoint if two conditions are satisfied:

  1. 1.
  2. 2.

A significant difference between the and , is that -disjointness does not allow in intersections, while allows this. In other words, condition (1) is not imposed by . As a consequence, the set of well-formed top-like types is a superset of ’s. This is covered in greater detail in Sect. 6.3.

Intersection Types and Polymorphism, Without the Merge Operator. Recently, Castagna et al. [18] studied a coherent calculus that has polymorphism and set-theoretic type connectives (such as intersections, unions, and negations). Their calculus is based on a semantic subtyping relation due to their interpretation of intersection types. The difference to , is that their intersections are used between function types, allowing overloading (i.e. branching) of types. For example, they can express a function whose domain is defined on any type, but executes different code depending on that type:

In our system we cannot express some of these intersections, namely the ones that do not have disjoint co-domains. However, accepts other kinds of intersections which are not possible to express in their calculus. For example merges with type are accepted in . Similarly to Castagna et al. previous work [17], their work is focused on combining intersections with functions (but without a merge operator), whereas is concerned with merges between arbitrary types. Nevertheless, both systems need to express negative information about type variables. That is, which types a given variable cannot be instantiated to. In their calculus, difference takes this role (i.e. ); whereas in , one can express it using disjoint quantification (i.e. ).

Going in the direction of higher kinds, Compagnoni and Pierce [19] added intersection types to System and used a new calculus, , to model multiple inheritance. In their system, types include the construct of intersection of types of the same kind . Davies and Pfenning [22] studied the interactions between intersection types and effects in call-by-value languages. They proposed a “value restriction” for intersection types, similar to value restriction on parametric polymorphism. None of these calculi has a merge operator.

Recently, some form of intersection types has been adopted in object-oriented languages such as Scala [37], TypeScript [4], Flow [3], Ceylon [1], and Grace [9]. There is also a foundational calculus for Scala that incorporates intersection types [49]. The most significant difference between and those languages/calculi is that they have no explicit introduction construct like our merge operator. The lack of a native merge operator leads to several ad-hoc solutions for defining a merge operator in those languages, as discussed in Sects. 1 and 3.1.

Extensible Records. The encoding of multi-field records using intersection types and the merge operator first appeared in Forsythe [48]. Castagna et al. [17] propose an alternative encoding for records. Similarly to ’s treatment of elaborating records is Cardelli’s work [13] on translating a calculus with extensible records () to a simpler calculus without records primitives (). However, he does not encode multi-field records as intersections/merges hence his translation is more heavyweight. Crary [21] used intersection types and existential types to address the problem arising from interpreting method dispatch as self-application, but he did not use intersection types to encode multi-field records.

Wand [52] started the work on extensible records and proposed row types [53] for records, together with a concatenation operator, which is used in many calculi with extensible records [29, 35, 42, 44, 51, 53]. Cardelli and Mitchell [15] defined three primitive operations on records that are also standard in type-systems with record types: selection, restriction, and extension. Several calculi are based on these three primitive operators (especially extension) [10, 28, 31, 33, 34, 45]. The merge operator in generalizes the concatenation operator for records, as its components may contain any types (and not just records). Systems with concatenation typically use a set of constraints/filters (such as and ) which are useful to combine several, possibly polymorphic, records [34]. In , constraints on labels are encoded using disjoint quantification and intersections. Although systems with records can model structurally typed OO languages, it is harder to encode nominal objects. One advantage of the generality of intersections and merges is that it is easier to have nominal objects. Unlike systems with records, which have been extensively studied, there is much less work on intersection type systems with a merge operator. An interesting avenue for future work is to see whether some known compilation and type-inference techniques for extensible records can be adapted to disjoint intersections and merges.

Traits and Mixins. Traits [23, 26, 36] and mixins [5, 6, 8, 11, 25, 27] have become very popular in object-oriented languages. They enable restricted forms of multiple inheritance. One of the main differences between traits and mixins are the way in which ambiguity of names is dealt with. Traits reject programs which compose classes with conflicting method implementations, whereas mixins assume a resolution strategy, which is usually language dependent. Our example demonstrated in Sect. 3 suggests that disjointness in enables a model with a philosophy similar to traits: merging multiple values of overlapping types is forbidden. However while our simple encodings of objects work for very dynamic forms of prototype inheritance, the work on type systems for mixins/traits usually builds on more conventional class-based OO models.

Constrained Types. The notion of disjoint quantification is inspired on bounded polymorphism [12, 16]. Such form of polymorphism typically uses types as subtyping bounds, whereas disjoint quantification uses types as disjoint (i.e. coherent) bounds. Another line of work are qualified types [32], which uses predicates on types to express constraints. However, qualified types are only applicable to the class of Hindley-Milner languages and such predicates are only defined over monotypes. falls outside this class of languages, plus its constraints can be expressed using any arbitrary type (and not just monotypes).

8 Conclusion and Future Work

This paper described : a System -based language that combines intersection types, parametric polymorphism and a merge operator. The language is proved to be type-safe and coherent. To ensure coherence the type system accepts only disjoint intersections. To provide flexibility in the presence of parametric polymorphism, universal quantification is extended with disjointness constraints. We believe that disjoint intersection types and disjoint quantification are intuitive, and at the same time flexible enough to enable practical applications.

For the future, we intend to create a prototype-based statically typed source language based on . We are also interested in extending our work to systems with union types and a type. Union types are also widely used in languages such as Ceylon or Flow, but preserving coherence in the presence of union types is challenging. The naive addition of seems to be problematic. The proofs for rely on the invariant that a type variable can never be disjoint to another type that contains . The addition of breaks this invariant, allowing us to derive, for example, . Finally, we could study a similar system with implicit polymorphism. Such system would require some changes in the subtyping and disjointness relations. For instance, subtyping should allow . Consequently, the disjointness relation would have to be modified, since valid statements in such as would no longer hold under the more powerful subtyping relation.