Making a Type Difference
Subtraction on Intersection Types as Generalized Record Operations

HAN XU∗ , Peking University, China
XUEJING HUANG and BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, China
In programming languages with records, objects, or traits, it is common to have operators that allow dropping,
updating or renaming some components. These operators are useful for programmers to explicitly deal withconflicts and override or update some components. While such operators have been studied for record types,
little work has been done to generalize and study their theory for other types.
This paper shows that, given subtyping and disjointness relations, we can specify and derive algorithmic
implementations for a general type difference operator that works for other types, including function types,
record types and intersection types. When defined in this way, the type difference algebra has many desired
properties that are expected from a subtraction operator. Together with a generic merge operator, using
type difference we can generalize many operations on records formalized in the literature. To illustrate theusefulness of type difference we create an intermediate calculus with a rich set of operators on expressions ofarbitrary type, and demonstrate applications of these operators in CP, a prototype language for Compositional
Programming. The semantics of the calculus is given by elaborating into a calculus with disjoint intersection
types and a merge operator. We have implemented type difference and all the operators in the CP language.
Moreover, all the calculi and related proofs are mechanically formalized in the Coq theorem prover.
CCS Concepts: • Theory of computation → Type theory.
ACM Reference Format:
Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira. 2023. Making a Type Difference: Subtraction on Intersection
Types as Generalized Record Operations. Proc. ACM Program. Lang. 7, POPL, Article 31 (January 2023), 28 pages.
https://doi.org/10.1145/3571224

1

INTRODUCTION

In programming languages with records, objects, or traits [Schärli et al. 2003], it is common to haverestriction operators and other derived operators that allow dropping or updating some components.
Cardelli and Mitchell [1991] did a comprehensive study of operations on records, identifying a varietyof record operators in a calculus with records, subtyping and bounded quantification [Cardelli et al.
1994]. Record operators have also been extensively studied in various calculi with row polymorphism [Wand 1989], though typically in settings without subtyping. Several existing functional
programming languages, including Haskell and OCaml, include some of these record operators.
Moreover, object-oriented languages with traits or mixins, such as the Pharo language [Tesone
et al. 2020] and the Jigsaw framework [Bracha 1992; Lagorio et al. 2009], also include operations
for renaming and removing methods to aid with the resolution of conflicts.
∗ The work was conducted as part of a research internship funded by The University of Hong Kong.

Authors’ addresses: Han Xu, Peking University, China, 1800012917@pku.edu.cn; Xuejing Huang, xjhuang@cs.hku.hk;
Bruno C. d. S. Oliveira, bruno@cs.hku.hk, The University of Hong Kong, Hong Kong, China.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2023 Copyright held by the owner/author(s).
2475-1421/2023/1-ART31
https://doi.org/10.1145/3571224

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31

31:2

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

While for records and record types such operators are widely studied, there is little work on
generalizing and studying the theory of such operators for other types. Nonetheless there are twolines of work that support some form of operators that deal with types other than records. In thefield of semantic subtyping [Castagna and Frisch 2005; Frisch et al. 2008] there is a related notionthat arises from set difference: we can interpret two type 𝐴 and 𝐵 as the sets of values that havetype 𝐴 and 𝐵. Thus, under such interpretation, we can obtain a new set of values by employing
set difference 𝐴\𝐵. The resulting set denotes a type with the values which are in 𝐴 but not in 𝐵.
However the semantics of set difference is not what we want: set difference does not generalize
record restriction and it has different applications. Shields and Meijer [2001] studied a calculus
with type-indexed rows, where types are used instead of labels for indexing. The calculus supports a
simple restriction operation, but lacks some desirable properties and does not have subtyping.
This paper studies a general notion of type difference, which enables a generalization of record
restriction. Although type difference is a partial function that could fail in some cases, it posesno restriction on types that can be subtracted in general. If type difference computes a result, a
number of useful properties are guaranteed, allowing values of the result type to be safely mergedwith other values. Type difference is specified by an intuitive definition based on subtyping anddisjointness relations, resulting in a general type difference operator that works for function types,
record types and intersection types. When defined in this way, type difference has a rich algebrawith many useful properties that are expected from a subtraction operator.
Together with a generic disjoint merge operator [Oliveira et al. 2016], using type difference we
can generalize many record operators in the literature. There are two main primitive operations
that can be defined with type difference. The expression 𝑒\𝐴 means that the information of type
𝐴 is dropped from the expression 𝑒. The related expression 𝑒 1 \𝑒 2 means that the information in
the minimal type of 𝑒 2 is dropped from 𝑒 1 . With those two primitive forms of expressions, several
operators can be defined as syntactic sugar. These operators include updates, biased merges, as well
as renaming operators (for the particular case of records). We show that all the record operators
proposed by Cardelli and Mitchell are encodable with type difference and a merge operator.
To illustrate the usefulness of type difference we create an intermediate polymorphic calculus,
called F𝑖∖ , with a rich set operators on types. The key feature of F𝑖∖ is a type-difference operation
between two types. The semantics of the calculus is given by an elaboration (a type-directedtranslation) into a calculus with disjoint intersection types [Oliveira et al. 2016] with a symmetricmerge operator. The elaboration is proved to be deterministic and type-safe. The elaboration also
illustrates that, although type difference is convenient and enables encodings of many operators,
all the uses of type difference are encodable in terms of merges and explicit type annotations.
An important point to provide the correct intuition for type difference in our work is that theinterpretation of subtyping in calculi with the merge operator and disjoint intersection types is
coercive [Luo 1999; Reynolds 1991], rather than set-theoretic. Assume that the set of values that
inhabit type A is denoted by ⟦A⟧. In semantic subtyping and the set-theoretic interpretation,
subtyping is interpreted as set inclusion: A is a subtype of B means that ⟦A⟧ is a subset of ⟦B⟧.
So it considers a subtype to be smaller than its supertype. Differently, in a coercive interpretationof subtyping, A ≤ B implies the existence of a monomorphism from ⟦A⟧ to ⟦B⟧, and leads to an
injective coercion function to convert values. From any value of a subtype, a value of its supertype
can be obtained. Therefore, we consider a subtype larger than its supertype. For instance, in the
set-theoretic interpretation for the top type, ⟦⊤⟧ is the set of all possible values. In contrast, in thecoercive interpretation, ⟦⊤⟧ is the set with a single value. In other words, ⊤ is interpreted as theunit type, instead of the type that can be assigned to all values. Since a value of the type 𝐴\𝐵 canbe obtained from any value of 𝐴, we expect 𝐴 <: 𝐴\𝐵. In the coercive interpretation, the type 𝐴\𝐵contains less information than 𝐴, justifying its interpretation as a form of difference.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

Making a Type Difference

31:3

We have implemented type difference and all the operators presented in this paper in the CP
language. In CP type difference is useful for implementing a variety of operations on traits, whichallow for conflict resolution when inheriting from multiple traits and for renaming componentsof traits. We also illustrate that in CP the generalized version of the operators works even whenthe expression being updated has a non-record type. In particular, the generalized operators areuseful to update overloaded functions. All the calculi and proofs in this paper are mechanicallyformalized in the Coq theorem prover. In summary, our contributions are:• Type difference: We formalize the idea of information difference on types in terms of subtyping
and type disjointness. Type difference enables operators that erase portions of a value that overlap
with some type. Type difference works in calculi that include a general merge operator [Dunfield
2014; Oliveira et al. 2016], and generalizes record restriction [Cardelli and Mitchell 1991].
• Algorithmic type difference: We study two concrete formulations of type difference for
languages with intersection types. The simpler formulation is for the subtyping of Barendregt,
Coppo, and Dezani-Ciancaglini (BCD), extended with bottom and record types. The second
formulation considers a richer subtyping relation with disjoint polymorphism [Alpuim et al. 2017].
Our two algorithmic formulations of type difference are sound and complete with respect to our
specification of type difference.
• Encodings for a rich set of operators: We show that with type difference we can define two
primitive operations 𝑒\𝐴 and 𝑒 1 \𝑒 2 . These enable encoding a variety of generic operators that
include updates, biased merges, as well as renaming operators (for the particular case of records).
All of Cardelli and Mitchell’s record operators are encodable with our operators.
• The F𝑖∖ calculus: an intermediate calculus with disjoint polymorphism and a rich set of operators.
The F𝑖∖ calculus is defined by a type-safe elaboration semantics into F𝑖+ [Bi et al. 2019; Fan et al.
2022]. The elaboration shows that the set of operators in F𝑖∖ is essentially a sophisticated form of(type-directed) syntactic sugar via type difference in terms of the primitive merge operator in F𝑖+ .
• Mechanical formalization and implementation: We modified the CP language (https://plground.org) to implement all the features of the F𝑖∖ calculus and we use CP to illustrateapplications of type difference and various operators in this paper (online demonstration athttps://plground.org/typediff/cipher). The F𝑖∖ calculus, its elaboration to F𝑖+ , and all the properties
for type difference described in this paper are formalized in Coq. The Coq development and theappendix of this paper are included in the companion artifact [Xu et al. 2022].
2

OVERVIEWThis section covers background on the merge operator, disjoint intersection types and CP. We
motivate type difference using CP examples, discuss why our work is beyond the scope of existing
approaches and describe our key ideas. Formal definitions are deferred to Sections 3 and 4.
2.1

BackgroundA general type difference makes sense in calculi with a generic merge operator [Dunfield 2014]
that merges two arbitrary expressions together. Thus we first review calculi with such a merge
operator, and the CP language which is designed on top of such calculi.
Disjoint Intersection Types and the Merge Operator. Intersection types were introduced in theseventies in Curry-style lambda calculi [Barendregt et al. 1983; Coppo and Dezani-Ciancaglini 1978;
Coppo et al. 1981; Pottinger 1980]. By composing two types with the constructor & , an intersection
type A & B specifies terms that have both type A and B. Although the type is not parametric, it ispolymorphic, providing a way to refine the characterization of terms. A corresponding term-level
constructor merge ( ,, ) was proposed by Reynolds [1988, 1997] for the language Forsythe, and later
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31:4

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

refined by Dunfield [2014]. When two terms e1 and e2 of type A1 and A2 are merged, the whole term
e1 ,, e2 has an intersection type A1 & A2 . For example, a function of type Int & Bool → Bool & Int is:
𝜆x : Int & Bool. (not x) ,, (x + 1)
In such settings, the merge construct is similar to pairs, and intersection types play a role similar
to product types. However, to extract a component from a pair, we need to use explicit projections,while with merge values components are implicitly extracted using types, such as in (not x) above.
The convenience afforded by implicit extraction using types has its costs. The language designer
has to resolve conflicts when two branches of a merge overlap. We follow the design of 𝜆𝑖 which
imposes a disjointness restriction on intersection types [Oliveira et al. 2016]. Two disjoint types
have their least upper bound equivalent to the top type. This restriction prevents, for example, twodifferent booleans, or functions of the same type but different implementations, to appear in one
merge. Therefore merges always have deterministic behavior when guided by a type. For instance,
here are one well-typed and one ill-typed expression.
✓

True ,, (1 ,, not)Bool is disjoint to Int & (Bool → Bool)✗

True ,, (1 ,, False)

Bool is not disjoint to Int & Bool

A merge operator with a disjointness restriction is an unbiased binary term constructor. It composes
expressions to form a tree structure. All the leaves on the tree are in an equal position. They can beviewed as unordered and can be rearranged when needed. The basic elements in merges include
single-field records and any term of primitive types. Here we have a nested merge with threeelements. The nested merge is wrapped by an annotation, which triggers an upcast. The wholeexpression then evaluates to a value that fits the shape of the type annotation.
({l = 1} ,, 2 + 3 ,, not) : Int & {l : Int} ↩→∗ 5 ,, {l = 1}
As we can see, types direct the runtime reduction of expressions. In the F𝑖+ calculus [Bi et al. 2019;
Fan et al. 2022], which we use in our work, merges of functions and merges of universally quantified
abstractions can be applied to an argument or a type argument simultaneously.
(not ,, (𝜆x. x + 1 : Int → Int)) (1 ,, False) ↩→∗ True ,, 2
If we replace the function not by a function of type Bool → Int, the whole expression will berejected during typing because Bool → Int is not disjoint to Int → Int. For two function types tobe disjoint, their return types must be hereditarily disjoint.
Traits and the CP Language. Disjoint intersection types with the merge operator serve as thetheoretical foundation of Compositional Programming [Zhang et al. 2021]: a recently proposed
programming paradigm. The language CP supports first-class traits [Bi and Oliveira 2018]. With
traits as basic reusable units, CP programs can be very modular and extensible. For this paper we
focus on basic uses of traits, but CP’s traits are useful to solve challenging modularity problems
such as the Expression Problem [Wadler 1998]. For further details on CP and its applications, werefer the readers to the original paper by Zhang, Sun, and Oliveira.
Below is a simple trait defaultCipher, which defines two methods encrypt and decrypt that bothtake a String and return a String. It also contains a field that indicates its name. Here we use an
identity function for both encryption and decryption.
type Cipher = { encrypt: String→String; decrypt: String→String; name: String };id = ΛA . \(x:A) → x;
defaultCipher = trait implements Cipher ⇒ {encrypt = id @String;
decrypt = id @String;
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

Making a Type Difference
name

31:5

= "Null Cipher";};A trait is elaborated into a function that returns a record in CP’s core calculus F𝑖+ . For instance thetrait above would be elaborated to a function of type Cipher → Cipher. To model traits, CP uses thesemantics of inheritance introduced by Cook and Palsberg [1989] where a class is seen as a function
from a record of methods to a record of methods. The function argument denotes the self reference.
The argument of the function resulting in the elaboration of a trait denotes the self-reference (i.e.,
this in conventional OOP languages). To create an object (typically via the use of new), we take thefixpoint of the function, fixing the self-reference. As these functions can be merged and act likeone function, traits in CP are compositional. In the following example, we use , (the notation formerges in CP) to safely merge two traits defaultCipher and defaultHelp.
defaultHelp = trait [self: Cipher] ⇒ {showHelp = "Encrypt using " ++ name;test (s:String) = "After encryption and decryption the text is " ++ decrypt (encrypt s);};simpleCipher = defaultCipher , defaultHelp;(new simpleCipher).showHelp --> "Encrypt using Null Cipher"

Note that in the defaultHelp trait the notation [self: Cipher] allows us to specify the name and thetype of the self-reference, similarly to Scala’s self-type annotations [Scala Community 2022]. While
the self-reference is always available in every trait, the self type annotation is optional. The self
type annotation allows us to call the name, decrypt and encrypt methods, which are not implemented
in the trait. Later, to instantiate the trait, we must compose it with another trait that implements
the missing methods (such as defaultCipher). The unbiased merge (,) brings an extra safety checkin compilation via its disjointness restriction, and leads to a static error when two traits being
composed have conflicts. For instance, consider the following definitions:caesarCipher (shift: Int) = trait inherits defaultCipher implements Cipher ⇒ {override encrypt = ... ;override decrypt = ... ;override name = "Caesar Cipher with a shift of " ++ toString shift;
showHelp = "Caesar Cipher is a substitution encryption technique"};new (caesarCipher 3 , defaultHelp) --> type error!

The trait caesarCipher inherits the methods in defaultCipher. However, when trying to compose
caesarCipher with defaultHelp we get a type error, since both traits have a showHelp method.
Trait conflicts. To resolve conflicts, one option is to remove the method showHelp from one of
the traits in advance. One way to do this in CP is to add type annotations to cast traits. Like thefollowing example demonstrates, we can choose what to keep from the two conflicting methods.
dropL = new (caesarCipher 3 : Trait<Cipher>) , defaultHelp;
dropR = new caesarCipher 3 , (defaultHelp: Trait<Cipher⇒{test:String→String}>);dropL.showHelp ++ ". " ++ dropR.showHelp --> "Encrypt using Caesar Cipher with a shift of 3.
Caesar Cipher is a substitution encryption technique"

Here dropL drops the showHelp from caesarCipher, while dropR drops showHelp from defaultHelp. However, removing methods in this way is quite cumbersome. For instance, in dropR a programmer has to
explicitly annotate all the methods that should be preserved (the annotation {test: String→String}).
If there are several methods to be preserved this will lead to a lot of boilerplate and manual work.
In essence the programmer is manually computing a type difference on types here. Therefore bettermechanisms to deal with conflicts are desirable, which is where type difference will come in handy.
Next we will show how type difference and other operators can enhance the flexibility of trait
composition and reduce the burden of manual annotation for programmers.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31:6

2.2

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

Operations on Traits and Merges

The type difference operator that we propose subtracts one type from the other by removing all
the common parts. It is denoted with A \ B. Take two record types for instance. Type difference
does not affect the fields that only appear in the first type.
{count : Int; check : String → Bool} \ {num : Int; check : String → Bool} = {count : Int}
Our type difference deals with types other than records. In particular, it can deal with function
types too. Even when they are nested in other constructs, functions can be partially subtracted.
{check : String → Int & Bool} \ {num : Int; check : String → Bool} = {check : String → Int}
Therefore, type difference can be applied to trait types (which are function types returning records inthe core calculus) to remove some of their methods. We make use of type difference to automaticallyresolve conflicts, rename components, and manually restrict traits in CP, as we shall see next.
Biased merges. In the example in Section 2.1, we use Trait<Cipher> to cast the trait (caesarCipher 3).
This type is the subtraction result of the type of two traits: (caesarCipher 3) and defaultHelp. We
can simplify the conflict resolution process by defining biased merge operators, which use type
difference to calculate the type annotation before merging two terms. There are two variants: +,prioritizes the left part while ,+ prioritizes the right part. The following code has the same effect as
the previous example with no explicit type annotations written.
dropLAlt' = new caesarCipher 3 ,+ defaultHelp;

dropRAlt' = new caesarCipher 3 +, defaultHelp;

The biased merge operators can be used with multiple inheritance as well. In the following example,
we define a trait simpleCompression to compress and decompress data. The trait efficientCipher
inherits the test method from simpleCipher, but its name field comes from caesarCipher. Besides, it
inherits compress and decompress from the simpleCompression trait and makes use of them to refine theencrypt and decrypt methods it inherits from caesarCipher.
type Compression = {compressRatio: Int; compress: String→String; decompress:String→String};
simpleCompression = trait implements Compression ⇒ { ... };efficientCipher (shift: Int) = trait [self: Cipher&Compression] inherits simpleCipher ,+caesarCipher shift ,+ simpleCompression implements Cipher & Compression ⇒ {override encrypt (s:String) = super.encrypt (compress s);override decrypt (s:String) = decompress (super.decrypt s);};(new efficientCipher 2).name --> "Caesar Cipher with a shift of 2"

Renaming. Now assume that we have another more advanced compression method, which
deserves a name. We want to combine this trait with the previously defined trait efficientCipher.
This time we choose to keep both of the conflicting fields (name) and rename them (as cipherName andcompressionName). The rename operator is also encoded by type difference, as we will discuss later.
advancedCompression = trait inherits simpleCompression ⇒ {name = "A Lossless Compression";...};
betterCipher = (efficientCipher 3) [ name <- cipherName ] ,+ advancedCompression [ name <compressionName ];(new betterCipher).cipherName --> "Caesar Cipher with a shift of 3"(new betterCipher).compressionName --> "A Lossless Compression""

Restriction operator. Another way to resolve conflicts is to use restriction on traits directly. We
use type difference to define restriction operators on traits: t\l means the remainder of trait t after
removing method l if it exists; t\\A means the remainder of trait t after removing every method intype A. Suppose that we get a SecretCipher from somewhere. We can use restriction on traits to add
a compression feature, and cover the cipher’s name with a confidentiality note:
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

Making a Type Difference

31:7

secretCipher = trait inherits defaultCipher implements Cipher ⇒ { ... };note = trait ⇒ { cipherName = "Confidential" ; helpInfo = ... };hiddenCipher = ( secretCipher \ name ) , ( betterCipher \\ Cipher ) ,+ note;

We first remove name from SecretCipher, and merge it with betterCipher with its Cipher part removed.
Then we add note to the whole composed trait via a biased merge. Note that this is a typical example
where biased operators alone are limiting. When we need to remove methods from both traits wecannot use a biased operator. But, in CP, we can use explicit restriction operators instead.
2.3

Existing Work on Record Operations and Set Difference

Before introducing the technical details of our work, it is useful to review existing related notions.
Operations on records. Extensible records, or rows, provide a flexible and type-safe way to compose
data dynamically. A record may contain multiple fields with distinct labels. Existing record calculi
vary in the operations that they support [Harper and Pierce 1991a; Ohori 1995; Rémy 1990]. We areparticularly interested in calculi that support subtyping. Therefore we use Cardelli and Mitchell[1991]’s (CM) proposal to demonstrate common operations in a record calculus with subtyping:⟨⟨l1 = True; l2 = 1⟩ | l3 = not⟩• Extension: add a field of some label to a record, knowing↩→∗ ⟨l1 = True; l2 = 1; l3 = not⟩that the record does not contain the same label.

⟨l1 = True; l2 = 1⟩ \ l2

• Restriction: remove a field from a record.

↩→∗ ⟨l1 = True⟩

It does nothing if the given field label is absent.

⟨l1 = True; l2 = 1⟩.l1• Extraction: extract the field associated with the given label.

∗↩→ True

The following two operations are implemented by the above three.

⟨l1 = True; l2 = 1⟩ [l2 ← l3 ]• Renaming: change the label name of a record field.

∗↩→ ⟨l1 = True; l3 = 1⟩

The record must contain the given label.

⟨⟨l1 = True; l2 = 1⟩ ← l2 = 2⟩↩→∗ ⟨l1 = True; l2 = 2⟩

• Overriding: replace a field of the given label if it exists,
otherwise extend the record.

The type system of CM reasons about both positive information and negative information, where
positive information means the record labels are present in the type, and negative informationmeans the record labels are absent in the type. A value of type ⟨l1 : Int⟩ \ l2 must have a field of Int
under name l1 , and can contain any fields except for l2 . The positive information is used in extraction
to guarantee the existence of the wanted field. The negative information, expressed through thespecial type constructor \ similar to our type difference, guards the safety of every record extension.
The subtyping of CM is complicated by the two kinds of information. Our type difference is afunction on types. In A \ B the part of A that matches with B is canceled and the whole type canbe converted into a form that does not contain the difference operator. So {l1 : Int; l2 : Int} \ l2evaluates to {l1 : Int}. However, in CM’s record calculus, ⟨l1 : Int; l2 : Int⟩ \ l2 is equivalent to theempty type because it excludes and contains the same label l2 . Besides, not all negative information
can be eliminated. For example, ⟨⟩ \ l is the type of all records that lacks field l, which cannot be
expressed without the restriction operator. The operations in CM only work for records and takefields as the basic units. They cannot deal with some of our intended applications, like the examples
in Section 2.2, where traits are not modelled as records, but as functions that return records.
Set difference in semantic subtyping. Semantic subtyping [Frisch et al. 2008], and its later extensions to polymorphism [Castagna et al. 2015, 2014, 2016; Castagna and Xu 2011], defines subtyping
via a set-theoretic model. It supports intersection and union types with distributivity. Under theinterpretation that types are sets of values inhabited in it, the subtyping relation is derived from
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31:8

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

the subset relation of values. For example, because A & B stands for the set intersection of A and B,
we directly know that A & B is a subtype of A (or B).
Type difference in semantic subtyping is an abbreviation for A & ¬B, defined via the type complement ¬B. It can be applied to any form of types, but despite the syntactic similarity, this definition
in semantic subtyping has a completely different meaning to our type difference. Roughly, we wantan operation that inverts intersection, so that (A & B) \ B gives us A. But in semantic subtyping,(A & B) & (¬B) is always equivalent to the empty type ⊥: no term of type A & B satisfies ¬B. We
cannot use set difference to cancel a field in a type, which is a typical use case for record restriction.
The next two examples compare the two forms of difference on two record types:{l1 : Int; l2 : Bool} & ¬{l1 : Int}= ⊥{l1 : Int; l2 : Bool} \ {l1 : Int}= {l2 : Bool}semantic subtyping
our calculus

As discussed in Section 1, the semantics of subtyping in the set-theoretical model differs fromours. The intersection of any two inhabited types is inhabited in our work thanks to the merge
operator. This matches up well with a coercive interpretation since the set of values in a subtype
should be larger than the set of values in a supertype. For example, we can actually take any Int andBool to compose a value of type Int & Bool, like 1 ,, True. In other words, intersection types in ourwork should be interpreted as a form of product types, rather than as some form of set intersection.
In semantic subtyping, with no term-level constructors for composition, an intersection such as
Int & Bool, becomes uninhabited, as expected from an intersection of disjoint sets. In calculi with amerge operator, from any value of a subtype, a value of its supertype can be obtained. For example,
if we drop the boolean part in 1 ,, True, the resulting value has type Int.
Type-indexed rows. Shields and Meijer [2001] proposed type-indexed rows to index each field ina record by their types (which have to be distinct) instead of labels. 𝜆𝑇 𝐼𝑅 does not have a restriction
operator, but we can implement one using a function. Consider the examples in 𝜆𝑇 𝐼𝑅 (on the left)
and in our work (on the right):
𝑙𝑒𝑡 𝑓: ∀𝛼 ∗ (Bool → Bool). (𝛼 & (Bool → Bool) → 𝛼)

The following expressions all evaluate to 1

= 𝜆(𝑥 ,, _). 𝑥✓ f (1 ,, not) ↩→∗ 1✓ (1 ,, not) \ (Bool → Bool)✗ f1✓ 1 \ (Bool → Bool)✗ f (1 ,, (𝜆(𝑥 ,, _). 𝑥) : Bool & Int → Bool)✓ (1 ,, (𝜆x. x) : Bool & Int → Bool) \ (Bool → Bool)In 𝜆𝑇 𝐼𝑅 we use 𝑓 to remove the Bool → Bool function from its input row. For better comparison, we
write the expressions in a syntax that is close to ours. The quantification 𝛼 ∗ (Bool → Bool) heremeans type 𝛼 is disjoint with Bool → Bool. This function takes a record that has type 𝛼 & (Bool →Bool) and matches the pattern (𝑥 ,, _). It then returns 𝑥, which corresponds 𝛼, the first part of theargument type, and therefore drops the Bool → Bool part, like e \ (Bool → Bool) on the right. We
use three cases to examine the function and our restriction operator. In the first one, a function
not of Bool → Bool is present, and can be successfully removed by 𝑓 . The last two expressions
raise type errors as the function 𝑓 requires the argument to contain a part exactly corresponding
to the type to remove. In particular, 𝜆𝑇 𝐼𝑅 does not match (𝜆(𝑥 ,, _). 𝑥) : Bool & Int → Bool with
Bool → Bool because it does not support subtyping. For the same reason, the type of the remaining
part of restriction may not be disjoint to Bool → Bool according to our definition of disjointness,
which breaks desirable properties.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

Making a Type Difference

2.4

31:9

Key Ideas

A specification for type difference. Let A \ B denote A minus B. To reuse standard terminology
from subtractions, we say that A is the minuend and B is the subtrahend of the subtraction or type
difference. We want the function to satisfy the following three properties:(1) A \ B is a supertype of A.
(2) A \ B is compatible (disjoint) with B, denoted by (A \ B) ∗ B.
(3) (A \ B) & B is a subtype of A.
Consider a typical case where e1 has type A, e2 has type B and C is the difference of A and B.
(e1 : C ,, e2 ) : A
Expressions of this kind typically arise during updates, such as those that we illustrated at the endof Section 2.1. The first property ensures that e1 : C is valid, because e1 is of type A and it is cast
to a supertype C. The second property guarantees that the merge is safe and compatible. The lastproperty justifies the outermost annotation. We can imagine that A and B are two sets (here atomic
types such as 𝐼𝑛𝑡 or 𝐵𝑜𝑜𝑙 are the elements of the sets). Then the set difference of A and B is theset of elements that are in A (which corresponds to the first property), and are not in B (whichcorresponds to the second property). The set difference includes all elements that fulfill these two
conditions, and it is the relative complement of B with respect to A. This corresponds to the third
property. Formally, we use A \𝑠 B ≡ C to represent that C is the type difference of A and B. The
relational specification combines the three properties above:
Definition 2.1 (Type difference specification). A \𝑠 B ≡ C ≜ A ≤ C ∧ B ∗ C ∧ B & C ≤ A.
Note that we use ≡ in later text to mean the equivalence relation defined on subtyping, i.e., A ≡ B
if and only if they are mutual subtypes. An important complication, which type difference has
to deal with, is that different types can be related by subtyping. Therefore we cannot simply use
equality of two types to decide whether or not to remove a type component from the minuend.
Take ⊤ → Bool and Bool → Bool as an example. The former is a subtype of the latter as it can
accept any argument that the latter accepts (⊤ accepts all legal terms). From the point of view ofsets, we can say that the subtype ⊤ → Bool includes supertype Bool → Bool.
(Int & (Bool → Bool)) \ (⊤ → Bool) ≡ Int
We can always use a subtype to remove a supertype component in the minuend. They cannot bedisjoint unless the supertype is equivalent to ⊤. So, only after ⊤ → Bool is removed, the result
satisfies property (2).
Partiality of type difference. Having subtyping as a partial order also means that we cannot define
a total subtraction operation that satisfies all three properties. What is the difference of ⊥ (theinfinite intersection of all types) and Int? More generally, what should the remaining part be when
we subtract a supertype from a subtype that cannot be further split? Take the previous two types
for example, and consider the following (incorrect) results for type difference:(⊤ → Bool) \ (Bool → Bool) ≡ ⊤ → Boolviolates property (2)(⊤ → Bool) \ (Bool → Bool) ≡ ⊤violates property (3)According to property (1), the result is a supertype of ⊤ → Bool. So the candidates are restricted toa function type, or a top-like type such as ⊤, or an intersection of both. For instance we could try
to pick a function type, such as ⊤ → Bool itself, or ⊤ for the result. But both types will violate atleast one property, and other similar types would be equally problematic. We say that the two types
above are not subtractable. Later, in the formal development, we will discuss how to determine
whether two types are subtractable in detail.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31:10

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

Extension/concatenation

e1 ,, e2

Encoded directly by the merge operator

Restriction (minus a type)

e\APrimitive operation in F𝑖∖

Restriction (minus a term)

e1 \ e2

Primitive operation in F𝑖∖

Restriction (minus a label)e \𝑙≜ e \ {l : ⊥}Extractione.l

Encoded directly by projection

Renaming

𝑒 [𝑙 1 ← 𝑙 2 ]≜ e \ l1 ,, {l2 = e.l1 }Right-biased merge

e1 ,+ e2≜ (e1 \ e2 ) ,, e2

Left-biased mergee1 +, e2

≜ e1 ,, (e2 \ e1 )Table 1. Operations supported via type difference. Two primitive operations and syntactic sugar.

On the other hand, given two subtractable types A and B, these three properties already limit
their type difference A \ B to a class of equivalent types. That is to say, all the types that fulfill theproperties are mutual subtypes. Property (1) allows A \ B to be as large as A. But if the type contains
too many elements, it breaks property (2) because it may contain type components present in B.
On the contrary, if it has too few elements, it loses property (3).
Encoding operations with type difference. Instead of demanding users to annotate terms explicitly,
type difference provides a more direct way to model various desirable operations. As we haveshown in CP, it facilitates updating trait methods, renaming trait components and so on. Here, we
demonstrate how these operations are encoded with the help of type difference.
A first class of operations is restriction operations, which we have seen on traits. For expressions
in the core calculus, we use e \ A and e1 \ e2 corresponding to \\ in CP. These operations can beapplied to any terms, not only to records. Here are some simple examples.
1 \ Int= {}{} stands for the top value, a merge of no element

1\2

= {}

To subtract a term is to subtract its type

(1 ,, True) \ Int= TrueThe part of merge that does not match the subtrahend type remains

1 \ Char=1

If the subtrahend does not overlap with the minuend, it cancels no term

Table 1 shows a summary and description of the operations that we support.
Type difference for overloaded functions. Besides traits, type difference of functions has otherapplications. For instance, we can use type difference to update implementations of an overloadedfunction. In the following example, inspired by Haskell’s read and an example due to Marntirosian
et al. [2020], we use a biased merge to override the conflicting part of a function.
readInt: String → Int
readChar: String → Char
readString : String → String
myNewReadChar : String → Charlet read : (String→Int) & (String→Char) & (String→String)= readInt ,, readChar ,, readStringin newRead = read ,+ myNewReadChar

In this example we have an overloaded read function that can parse a string as either an integer ora character or a string. To obtain a variant of read that uses a different function to read characters
we can update the implementation of the corresponding type as shown in newRead.
Algorithms for type difference, disjointness and subtyping. We will present an algorithmic definition
for type difference, which does not rely on disjointness and subtyping. As disjointness and subtyping
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

Making a Type Difference

31:11

can be encoded by type difference, we can derive disjointness and subtyping algorithms once wehave algorithmic type difference. A formal specification of disjointness is:Definition 2.2 (Disjointness). A ∗ B ≜ ∀ 𝐶, if A ≤ C and B ≤ C then C ≡ ⊤.
According to the specification of type difference, we can conclude A ∗ B from A \ B ≡ A. Via thespecification of disjointness we know that the other direction also holds. Therefore we have:A∗B ↔ A \ B ≡ A
Similarly, we have thatA ≤ B↔B\A≡⊤
The fact that we can derive subtyping from type difference is a natural consequence of its algebraic
properties. Our specification of type difference satisfies the three axioms for being a subtraction
algebra [Jun et al. 2004; Schein 1992], which is known to determine an order relation, guaranteeing agood correspondence between the type difference and subtyping. We have the order ≤ representingthat the left side (subtype) contains more information than the right side (supertype).
A \ (B \ A) ≡ A
A \ (A \ B) ≡ B \ (B \ A)
(A \ B) \ C ≡ (A \ C) \ B
Distributivity and disjoint polymorphism. We add universal quantified types to the subtyping
relation by Barendregt et al. [1983]. Like other type constructors, universal quantifiers distributeover intersections. We make use of the idea of splittable types [Huang et al. 2021]: all types that
contain intersections in positive positions can be split into smaller elements. Splittable types
enable us to deal with distributive subtyping. Furthermore, using splittable types we can subtract afunction partially, even when it is nested in other constructors, as we have shown at the beginningof Section 2.2. In addition, we support disjoint polymorphism, which allows a disjointness constraint
to be specified for type abstractions.
(Λ(𝛼 ∗ Int). 𝜆x : 𝛼 . x ,, 1) : ∀𝛼 ∗ Int. 𝛼 → 𝛼 & Int
This is an expression that takes a type and a term. 𝛼 ∗ Int enforces a restriction to the type argument,
and ensures that the parameter x of type 𝛼 can be merged with 1. Our type difference not only cansubtract a function from another, but can also handle universally quantified types and variables.
Disjoint quantification also allows us to encode the type restriction in the CM calculus.
CM :𝑙𝑒𝑡 𝑓 (𝑅 <: ⟨l1 : Int⟩ \ l2 ) (𝑟 : 𝑅) : ⟨R|l2 : Int⟩ = ⟨⟨r ← l1 = r.l1 + 1⟩ | l2 = 0⟩Us :Λ(𝛼 ∗ {l2 : ⊥}). 𝜆x : 𝛼 & {l1 : Int}. x ,+ {l1 = x.l1 + 1; l2 = 0}

The example above is from CM’s paper. Function 𝑓 expects a type parameter that is a subtype of⟨l1 : Int⟩ \ l2 , and a value parameter of such type, i.e., it must contain a field of l1 and lack a fieldof l2 . The function increments the integer value of l1 and extends the input with a l2 field. The
remaining fields remain unchanged. Our implementation in the second line does the same thing.
3

DERIVING A TYPE DIFFERENCE

This section shows how to derive a type difference algorithm from the specification that was given
in Section 2. We present a type difference algorithm for the subtyping relation of Barendregt et al.
[1983] (BCD) extended with record types, and prove its soundness, completeness and decidability
with respect to the specification. Importantly, note that while the subtyping relations presented in
our work are extensions of BCD subtyping, our typing relation and semantics for the calculi in ourwork (presented in Section 4) are very different from those in Barendregt et al.’s work.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31:12

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

𝐴≤𝐵(BCD subtyping)

S-arr
S-refl

S-bot

S-top

S-topArr

S-topRcd

A2 ≤ A1

A≤A

⊥≤A

A≤⊤

⊤ ≤⊤→⊤⊤ ≤ {l : ⊤}A1 → A3 ≤ A2 → A4

A3 ≤ A4

S-rcd
A≤B{l : A} ≤ {l : B}

S-distArr

S-distRcd(A → B) & (A → C) ≤ A → B & C{l : A} & {l : B} ≤ {l : A & B}

S-trans
A≤B

S-and
B≤C

A≤C

S-andlS-andrA&B ≤ A

A&B ≤ BA≤B

A≤CA ≤ B&C

Fig. 1. BCD subtyping.

3.1

Syntax and Subtyping
𝐴, 𝐵, 𝐶 F Int | ⊤ | ⊥ | A & B | A → B | {l : A}

Types
Ordinary types

𝐴◦, 𝐵 ◦, 𝐶 ◦ F Int | ⊤ | ⊥ | A → 𝐵 ◦ | {l : 𝐴◦ }Types. BCD subtyping [Barendregt et al. 1983] is a widely used subtyping relation for intersection
types. The most important feature of BCD-style subtyping is that it allows function types to
distribute over intersection types, like in rule S-distArr. We have all the types in the original BCD
type system, extended with a bottom type and a record type. Ordinary types [Davies and Pfenning2000], are types that do not contain top-level intersection types. However, in BCD subtyping, arrow
types such as A → B & C may behave like intersection types due to distributivity. Following theapproach by Huang et al. [2021], we restrict the notion of ordinary types to exclude such types.
Subtyping. The subtyping rules, presented in Figure 1, extend BCD subtyping [Barendregt et al.
1983] with rules for record types and the bottom type. Terms of an intersection type must satisfy
both parts of the intersection as A & B is the greatest lower bound of type A and B. The key
feature of BCD subtyping is that other type constructors distribute over intersections. For example,
A → B & C is a subtype of (A → B) & (A → C). ⊤ is the supertype of all types, but there is a groupof types equivalent to ⊤, such as ⊤ & ⊤ or A → ⊤.
Notation. Note that A ≡ B denotes the equivalence defined via subtyping (A ≤ B and B ≤ A) and= is used for syntactic identity, i.e., A = B means that A and B are exactly the same type. We needthis notation because intersection types and distributivity introduce a lot of semantically equivalent
types that are not syntactically equivalent such as Int, Int & Int, Int & Int & Int... In particular, we
use top-like types to describe types that are equivalent to ⊤.
3.2

Deterministic Type Difference

The specification (A \𝑠 B ≡ C) in Definition 2.1 is neither algorithmic nor deterministic. It only
restricts the result of type difference to a semantically equivalent class of types. Next we will givean intermediate definition in Fig 2, which is explained in detail over this section. This definition
will be helpful to derive an algorithmic version of type difference. Unlike the specification of type
difference, the new definition is deterministic: there can only be a unique type for such intermediatetype difference. We prove that the definition is sound and complete to the specification.
Equivalence results for type difference. The type difference specification does not distinguish two
semantically equivalent types, as it is defined by subtyping and disjointness, both of which are notsensitive to the syntactic form of types. The following lemma expresses this property:
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

Making a Type Difference

31:13

A \𝑑 B = C(Deterministic Type Difference)
TD-BCD

TD-disjointA∗B

TD-subtype
B≤A

A \𝑑 B = A

A \𝑑 B = A⊤A1 \𝑑 B = C1

A1  A  A2
A2 \𝑑 B = C2
A \𝑑 B = C

A ⊢ C1  C  C2

Fig. 2. Deterministic definition of type difference, considering different three cases.

Lemma 3.1 (Type Difference Specification Safety). If A\𝑠 B ≡ C0 and C0 ≡ C1 , then A\𝑠 B ≡ C1 .
Take the type difference of Int and Int for example. According to the specification, all the types
equivalent to ⊤ fit Int \𝑠 Int. Such types include ⊤, ⊤ & ⊤, and Int → ⊤. On the other hand, thetype difference specification is precise enough to restrict the result to an equivalence class of types.
We prove the coherence of the type difference specification using the covariance of disjointness
property. With Lemmas 3.1 and 3.3, show the specification forms an equivalence relation.
Lemma 3.2 (Covariance of Disjointness). If A ∗ B and B ≤ C, then A ∗ C.
Lemma 3.3 (Coherence of Type Difference). If A \𝑠 B ≡ C1 and A \𝑠 B ≡ C2 then C1 ≡ C2 .
Two special cases for type difference. We next show two special cases of how the specification
behaves, to help us better understand the first two rules TD-disjoint and TD-subtype of deterministic type difference. Firstly, we have the case where A ∗ B. Since the two types do not share any
nontrivial supertypes other than ⊤, we should remove no part from the minuend A.
Lemma 3.4 (Disjoint Type Subtraction). If A ∗ B, then A \𝑠 B ≡ A.
The second case is when B ≤ A. In this case any part of A is a supertype of B. To find a resultthat is disjoint to B, we have to discard all the components of A.
Lemma 3.5 (Subtype Subtraction). If B ≤ A, then A \𝑠 B ≡ ⊤.
Zero type. While the first rule TD-disjoint directly follows Lemma 3.4, in the second rule we
use a notion of zero type, defined at the right bottom of Figure 3. The zero type function helps thesecond rule TD-subtype to return the same result when it overlaps with the first rule. It computes
a top-like type based on any given type. Notice that ⊤ is not only the supertype of every type, butalso disjoint to every type. For a minuend type A equivalent to ⊤, such as Int → ⊤, A \ B always
matches both of the first two rules regardless of B. To make these two rules consistent, we choose
to preserve the original structure of the minuend as much as possible. For the concrete example(Int → ⊤) \ B, the result is Int → ⊤ rather than ⊤, which is equal to (Int → ⊤) ⊤ . Generally, thezero type function maintains the structure of its input and erases all the meaningful components inpositive positions by using the ⊤ type instead. It does not change the input if it is already top-like.
Lemma 3.6 (Completeness of Zero Type). A⊤ ≡ ⊤.
Lemma 3.7 (Soundness of Zero Type). If A ≡ ⊤, then A⊤ = A.
The general case for type difference. In general, the subtrahend type is neither disjoint with
nor a subtype of the minuend. Suppose that we have an intersection of two functions: (Bool →Bool) & (Int → Int), and we want to remove the function on integers, which is (Bool → Bool) &(Int → Int) \ (Int → Int). In this case, the first two rules cannot apply. Only after the minuend
is separated, (Bool → Bool) \ (Int → Int) matches the first rule and (Int → Int) \ (Int → Int)
matches the second. By composing the two results, we obtain the type difference of the originalminuend and subtrahend (Bool → Bool) & (Int → ⊤), i.e., (Bool → Bool). From the specification,
we can prove the correctness of the splitting and composition.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31:14

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

BAC(Type Splitting)A  A&B  B

A ⊢ B1  C  B2

C1  B  C2

A → C1  A → B  A → C2(Type Merging)A⊤ ≡ BC1  B  C2

{l : C1 }  {l : B}  {l : C2 }(Zero Type Function)⊤⊤ = ⊤

A1 & A2 ⊢ B1  B1 & B2  B2
A ⊢ B1  C  B2

𝐷 → A ⊢ 𝐷 → B1  𝐷 → C  𝐷 → B2
A ⊢ B1  C  B2⊥⊤ = ⊤
Int⊤ = ⊤(A & B) ⊤ = A⊤ & B⊤
(A → B) ⊤ = A → B⊤{l : B}⊤ = {l : B⊤ }{l : A} ⊢ {l : B1 }  {l : C }  {l : B2 }Fig. 3. The auxiliary meta functions used in the deterministic type difference.

Lemma 3.8 (Composition). If A1 \𝑠 B ≡ C1 and A2 \𝑠 B ≡ C2 , then (A1 & A2 ) \𝑠 B ≡ C1 & C2 .
Splittable and mergeable types. The last rule in Figure 2 deals with more than just intersection
types. It is very similar to the last lemma if we replace A1  A  A2 and A ⊢ C1  C  C2 by
A = A1 & A2 and C = C1 & C2 . Actually, these two relations generalize the splitting and merging ofintersection types by taking distributivity into consideration.
For the last rule TD-BCD of type difference, we need to introduce the concept of splittable
and mergeable types. Splittable types were first introduced by Huang et al. [2021] to promote a
subtyping algorithm for BCD subtyping. The idea of splittable types is to specify the distributivity
brought by rules S-distArr and S-distRcd explicitly so that we can eliminate the use of thetransitivity rule S-trans in the subtyping deduction. We need the notion of splittable types because
in the general case of type difference, the intersection may hide deeply inside certain types like
Int → Int & Bool. Subtracting components like Int → Int from them would be impossible if weonly look at top-level intersections. Under such cases, we need the rules for splittable types definedat the top of Figure 3 to help us analyze these intersection-like types.
Mergeable types are new and they are designed to complement splittable types. Merging isdefined at the left bottom part of Figure 3 as a reverse operation of splitting. A ⊢ B1  C  B2 means
merging two types B1 and B2 according to the shape of the type A will result in a type C. We need
the shape of A as a reference because splitting is not an injective function. Thus merging two types
like B1 → B2 and B1 → B3 could result in either B1 → B2 & B3 or (B1 → B2 ) & (B1 → B3 ). The
shape of A ensures the determinism of such merging process. We have the following results toensure the reversibility and determinism of the splittable and mergeable relations.
Lemma 3.9 (Split Determinism). If B1  A  B2 and C1  A  C2 , then B1 = C1 and B2 = C2 .

Lemma 3.10 (Determinism of Merging). If A ⊢ B1  C  B2 and A ⊢ B1  C ′  B2 , then C = C ′.

Lemma 3.11 (Reversibility of Merging and Splitting). If A1  A  A2 , then A ⊢ A1  A  A2 ;if B ⊢ A1  A  A2 , then A1  A  A2 .
3.3 Algorithmic Type Difference
Deterministic type difference depends on subtyping and disjointness. While having algorithmic
formulations of disjointness and subtyping would enable us to obtain an algorithm for deterministic
type difference, in this section we will show an algorithmic formulation of type difference which
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

Making a Type Difference

31:15

A \𝑎 B = A(if A ≡ ⊤)B \𝑎 A = B
A \𝑎 ⊥ = A(if A ≡ ⊤)⊤Int \𝑎 (A → B) = Int
Int \𝑎 {l : A} = Int{l : A} \𝑎 (B → C) = {l : A}{l : A} \𝑎 Int = {l : A}
(A → B) \𝑎 Int = A → B(A → B) \𝑎 {l : C} = A → B
Int \𝑎 Int = ⊤{l1 : A} \𝑎 {l2 : B} = {l1 : A}
A1 → A2 \𝑎 B1 → B2 = A1 → (A2 \𝑎 B2 )(if l1 ≠ l2 )(if A2 \𝑎 B2 = A2 or B1 \𝑎 A1 = B1 ⊤ ){l : A} \𝑎 {l : B} = {l : A \𝑎 B}
A \𝑎 (B1 & B2 ) = (A \𝑎 B1 ) \𝑎 B2(if A1  A  A2 and A ⊢ (A1 \𝑎 B)  C  (A2 \𝑎 B))

A \𝑎 (B1 & B2 ) = (A \𝑎 B2 ) \𝑎 B1(if A \𝑎 B2 is defined )A \𝑎 B = C(if A \𝑎 B1 is defined )Fig. 4. Algorithmic type difference.

does not depend on subtyping and disjointness. In turn, using this algorithmic formulation we cangive an algorithm for subtyping and disjointness as well, since both of these relations are definable
as special cases of type difference.
Design. The rules of algorithmic type difference, presented in Figure 4, can be divided into three
categories, which follow the three cases in deterministic type difference. The first set of rules is for
dealing with disjointness, such as Int \𝑎 (A → B) = Int. The second set of rules is for dealing with
subtyping, such as Int \𝑎 Int = ⊤ and {l : A} \𝑎 {l : B} = {l : A \𝑎 B} . The last set of rules only
contains the last three rules in Figure 4. They are used for dealing with mixed cases, where thesubtrahend or minuend behave like intersection types.
Disjointness. Most of the rules in this category simply return the minuend if the rule operates
on two disjoint types. How to judge type disjointness from the type difference is given by thefollowing lemma. From it we directly obtain an algorithm for disjointness, that is calculating A \𝑎 B
to see whether it results in A or not.
Lemma 3.12 (Disjoint Type Difference). A ∗ B if and only if A \𝑎 B = A.
For most rules such as Int \𝑎 (A → B) = Int, we can directly find the disjointness relation fromthe structure of the two types. There are also rules which involve substructures of types, such as(A1 → A2 ) \𝑎 (B1 → B2 ) = A1 → A2 (if A2 \𝑎 B2 = A2 ). Besides, if a type is equivalent to ⊤, thenit is disjoint to every type, which is the case of the first and the second rule in Figure 4. We givean algorithm for judging whether a type is top-like in the Appendix. We will also introduce analgorithm for judging a top-like type extended with polymorphism in Section 4.
Subtyping Rules. Most of the rules in this category simply return the zero type of the minuend if
the rule finds a subtyping relation between two types. The correctness of this behaviour is ensured
by the following lemmas.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31:16

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

Lemma 3.13 (Zero Type Difference). A⊤ = C if and only if A \𝑎 A = C.
Lemma 3.14 (Subtyping Type Difference). B ≤ A if and only if A \𝑎 B = A⊤ .
For example, the rule Int \𝑎 Int = ⊤ finds that Int is a subtype of Int, thus we return the zerotype of Int, which is ⊤. For two record types or two function types, there is no special rules forthe case that the subtrahend is a subtype of the minuend. Such rules are subsumed by the two
structural rules {l : A} \𝑎 {l : B} = {l : A \𝑎 B} and A1 → A2 \𝑎 B1 → B2 = A1 → (A2 \𝑎 B2 ) (ifB1 \𝑎 A1 = B1 ⊤ ). Note that with the lemmas above, we can give an algorithm for B ≤ A by checking
A \𝑎 B = A⊤ .
Intersections. The last three rules in Figure 4 are used to deal with intersection or intersection-liketypes. The first rule is just the same as deterministic type difference. The rule A \𝑎 (B1 & B2 ) =(A \𝑎 B1 ) \𝑎 B2 says that if a type is subtracted by an intersection type, you can first subtract its
left component then subtract its right component. The rule A \𝑎 (B1 & B2 ) = (A \𝑎 B2 ) \𝑎 B1 is thecommutative version. We need these two rules because type difference is not total. Recall the totality
counterexample in the Section 2. Similarly to the counterexample we have that (Int → Int) → Int
is not subtractable by (Int → Int). Next we consider a type difference A \𝑎 B when A = (Int →Int) → Int and B = (Int → Int) & (Int → Int) → Int. By the rule A \𝑎 (B1 & B2 ) = (A \𝑎 B1 ) \𝑎 B2
alone, we will first need the calculate (Int → Int) → Int \𝑎 (Int → Int), which is not subtractable.
But B is a subtype of A, and according to rule TD-subtype we expect A \𝑎 B to be subtractable.
Therefore, we need a commutative rule A \𝑎 (B1 & B2 ) = (A \𝑎 B2 ) \𝑎 B1 to get through such cases.
Note that the 3 last cases overlap. We have proved that the first rule can always be applied first in
an implementation without loss of expressive power. For the commutative rules we proved that
their relative order does not matter: we can apply either one in any order.
3.4

Theorems

In this section we demonstrate some properties about type difference. We will prove the determinismof type difference, the equivalence between the three type differences (A \𝑠 B ≡ C, A \𝑑 B = C,A \𝑎 B = C) and the decidability of type difference.
Equivalence and Determinism. Using a lemma of deterministic type difference, we can prove theequivalence of the algorithmic type difference with a direct induction.
Lemma 3.15 (Type Difference Concatenation). If A1 \𝑑 B1 = A2 and A2 \𝑑 B2 = A3 , thenA1 \𝑑 (B1 & B2 ) = A3 .
Lemma 3.16 (Type Difference Eqivalence). A \𝑑 B = C if and only if A \𝑎 B = C.
By the Lemmas 3.9 and 3.10 showing the determinism of splittable and mergeable types, we candirectly show that deterministic type difference is indeed deterministic.
Theorem 3.17 (Determinism of Type Difference). If A \𝑑 B = C1 and A \𝑑 B = C2 , then C1 = C2 .
Completeness. Completeness means that deterministic type difference and algorithmic type
difference satisfy the specification of type difference. Similarly to Lemmas 3.12 and 3.14, we canobtain the following two properties.
Lemma 3.18 (Completeness of Subtyping). If A \𝑑 B = C, then A ≤ C.
Lemma 3.19 (Completeness of Disjointness). If A \𝑑 B = C, then B ∗ C.
By direct induction we obtain:
Lemma 3.20 (Completeness of Reverse Subtyping). If A \𝑑 B = C, then B & C ≤ A.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

Making a Type Difference

31:17

Combining three properties above, we prove the completeness of type difference.
Theorem 3.21 (Type Difference Completeness). If A \𝑑 B = C, then A \𝑠 B ≡ C.
Soundness. Soundness means that if there exists a type 𝐶 satisfying A \𝑠 B ≡ C, then we can finda type C ′ that is equivalent to 𝐶 and A \𝑑 B = C ′. We define a new notion called subtractable anduse the decidability lemma of subtractable to prove the soundness.
Definition 3.22 (Subtractable). Subtractable A B ≜ For all 𝐶 ◦, if A ≤ 𝐶 ◦, then B ≤ 𝐶 ◦ ∨ B ∗ 𝐶 ◦ .
An intuition for subtractable is that for every component of type A identified by 𝐶 ◦ , either B
is a subtype of it or B is disjoint with it. Otherwise it is not subtractable, such as Int → Booland Bool → Bool. After subtractable is defined, we can prove the following lemmas directly by
induction on A and B:
Lemma 3.23 (Soundness of Subtractable). If Subtractable A B, then ∃𝐶, A \𝑑 B = C.
Lemma 3.24 (Decidability of Subtractable). Subtractable A B is decidable.
Lemma 3.25 (Completeness of Subtractable). If ∃𝐶, A \𝑠 B ≡ C, then Subtractable A B.
With the completeness Theorem 3.21, all that remains is to show that deterministic type differenceis sound with respect to the type difference specification, and the equivalence between the three
formulations of type differences is established. Furthermore type difference is decidable.
Theorem 3.26 (Type Difference Soundness). A\𝑠 B ≡ C if and only if ∃C ′, A \𝑑 B = C ′ ∧C ≡ C ′ .
Theorem 3.27 (Decidability of Type Difference). Type difference is decidable.
4

A CALCULUS WITH DISJOINT QUANTIFICATION AND OPERATIONS ON MERGESIn this section we extend the previously defined type difference to disjoint polymorphism [Alpuim
et al. 2017] and present it in a full calculus called F𝑖∖ . Disjoint polymorphism enables the calculus to
support encodings of bounded quantification and row polymorphism [Xie et al. 2020]. In particular
Xie et al. has shown that kernel 𝐹 <: [Cardelli and Wegner 1985], which is the most widely used
decidable calculus with bounded quantification, can be encoded in F𝑖+ . F𝑖∖ is proved to be type-safe
via an elaboration into F𝑖+ [Bi et al. 2019; Fan et al. 2022] (a calculus with disjoint polymorphism
but without type difference) in Section 5.
4.1 Syntax and Well-Formedness
The syntax of F𝑖∖ is:Types
Ordinary types
Expressions

𝐴, 𝐵, 𝐶 F Int | ⊤ | ⊥ | A & B | A → B | {l : A} | 𝛼 | ∀𝛼 ∗ A. B
𝐴◦, 𝐵 ◦, 𝐶 ◦ F 𝛼 | Int | ⊤ | ⊥ | A → 𝐵 ◦ | {l : 𝐴◦ } | ∀𝛼 ∗ A. 𝐵 ◦𝑒 F p | 𝑥 | 𝑖 | {} | 𝑒 : 𝐴 | e1 ,, e2 | fix x : A. e | Λ𝛼 . e | 𝜆x : A. e | {l = e}| Λ(𝛼 ∗ A). e | 𝜆x. e | e1 e2 | e A | e.l | e \ A | e1 \ e2

Term contexts

Γ F · | Γ, x : A

Type contexts

Δ F · | Δ, 𝛼 ∗ A

Type and Expression Syntax. Our syntax extends the syntax of the F𝑖+ calculus [Fan et al. 2022] by
the gray parts. A type variable 𝛼 is bound by disjoint quantification ∀𝛼 ∗ A. B, which can only be
instantiated by types that are disjoint to A. We add two new expression forms (e1 \ A and e1 \ e2 ) asa generalization of a record restriction operation, and allow more flexibility on annotating lambda
abstractions and disjoint-quantified abstractions. The expression e \ A removes all components
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31:18

Han Xu, Xuejing Huang, and Bruno C. d. S. OliveiraΔ⊢A≤B(Declarative Subtyping, Additional Rules)
DS-topVar⊢Δ
𝛼 ∗A ∈ Δ

DS-forallΔ ⊢ A2 ≤ A1

Δ⊢A≤⊥

Δ⊢⊤≤𝛼
DS-distAll⊢Δ

Δ, 𝛼 ∗ A2 ⊢ B1 ≤ B2

Δ ⊢ ∀𝛼 ∗ A1 . B1 ≤ ∀𝛼 ∗ A2 . B2
DS-topAll⊢Δ

Δ ⊢ ∀𝛼 ∗ A. (B1 & B2 )Δ ⊢ (∀𝛼 ∗ A. B1 ) & (∀𝛼 ∗ A. B2 ) ≤ ∀𝛼 ∗ A. (B1 & B2 )Δ ⊢ ⊤ ≤ ∀𝛼 ∗ ⊤. ⊤Δ ⊢ A∗B(Disjointness)
D-ax

D-top
Δ⊢B

A ≡Δ ⊤Δ ⊢ A∗B

D-rcd
Δ ⊢ A∗B

D-var
𝛼 ∗A ∈ Δ

Δ ⊢ {l : A} ∗ {l : B}Δ⊢A≤B

Δ ⊢ 𝛼 ∗B
D-arr

D-and
Δ ⊢ A1 ∗ B

Δ ⊢ A2 ∗ B

Δ ⊢ A1 & A2 ∗ B⊢ΔA ∗𝑎𝑥 B
Δ⊢A

Δ⊢B

Δ ⊢ A∗B

D-symmΔ ⊢ B∗A

Δ ⊢ A1Δ ⊢ B1Δ ⊢ A2 ∗ B2

D-forallΔ ⊢ A1Δ ⊢ A2Δ, 𝛼 ∗ A1 & A2 ⊢ B1 ∗ B2

Δ ⊢ A∗B

Δ ⊢ A1 → A2 ∗ B1 → B2

Δ ⊢ ∀𝛼 ∗ A1 . B1 ∗ ∀𝛼 ∗ A2 . B2

Fig. 5. Declarative subtyping and disjointness. The remaining rules of subtyping directly extend Figure 1 with
type contexts.

covered by the type A from expression e, while e1 \ e2 removes components from e1 that conflictwith e1 . It can be interpreted as e1 \ A2 assuming the minimal type of e2 is A2 . These two expressions
enable simple syntactic sugar for a wide range of operations on merges, as shown in Table 1. Finally,
the most notable expression in calculi like F𝑖+ is the merge operator e1 ,, e2 , which enables merging
two arbitrary expressions.
Context and Well-Formedness. We have two contexts. Type contexts Δ track disjointness information of type variables. Term contexts Γ track the type information of term variables. Besides,
three standard well-formedness relations Δ ⊢ A, ⊢ Δ and Δ ⊢ Γ are defined in the Appendix.
Notations and Specification. As subtyping and type difference now depend on the type context,
all the notation needs an update. We still use A = B to denote that type A and B are syntacticallyequivalent. But here we use A ≡Δ B to denote type equivalence (which is Δ ⊢ A ≤ B and Δ ⊢ B ≤ A)
under type context Δ. The specification of type difference is also updated.
Definition 4.1 (Type difference specification). A \𝑠 B ≡Δ C ≜ Δ ⊢ A ≤ C ∧ Δ ⊢ B & C ≤ A ∧ Δ ⊢B ∗ C.
4.2

Subtyping and Disjointness

We now present the subtyping and disjointness relations, which are the same as F𝑖+ [Fan et al. 2022].
Subtyping. The subtyping relation shown at the top of Figure 5 is the extension of Figure 1 withdisjoint polymorphism. Here we only show the new rules. The remaining rules directly extend
Figure 1 with type contexts. The rules DS-distAll and DS-topAll are natural extensions of BCD
subtyping for universal types. The rule DS-topVar adds a new rule for universal quantifiers that aresupertypes of ⊤. The rule DS-forall is the subtyping relation between universal types. It is very
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

Making a Type Difference

31:19

A≡⊥

(Algorithmic Bot-Like)
BL-andlBL-botA≡⊥⊥≡⊥

A&B ≡ ⊥
BL-andrB≡⊥
A&B ≡ ⊥A ≡Δ ⊤
TL-top⊢Δ⊤ ≡Δ ⊤(Algorithmic Top-Like)
TL-arrΔ⊢A

B ≡Δ ⊤A → B ≡Δ ⊤TL-rcdB ≡Δ ⊤{l : B} ≡Δ ⊤TL-allB ≡Δ,𝛼 ∗ A ⊤TL-var⊢Δ
𝛼 ∗A ∈ ΔA≡⊥

TL-andA ≡Δ ⊤B ≡Δ ⊤∀𝛼 ∗ A. B ≡Δ ⊤𝛼 ≡Δ ⊤

A & B ≡Δ ⊤Fig. 6. Algorithmic bottom-like and top-like judgments.

similar to the function subtyping rule S-arr, being covariant on the result type and contravariant
in the argument type.
Disjointness. Disjointness is the same as in F𝑖+ , and it is shown at the bottom of Figure 5. Rule D-top
shows that top-like types, which are types equivalent to top, are disjoint to every type. Rule Dvar shows that a type variable is disjoint to the supertypes of its bound. Rule D-ax is for simple
disjointness axioms for types of different shapes, with a full definition in the Appendix. For instance
Int is disjoint to A → B. Rule D-and shows that an intersection type is disjoint with another typewhen all of its components are disjoint with that type. Rule D-symm shows that all the disjointness
rules are symmetric. The last three rules D-rcd, D-arr, and D-forall show that the disjointnessof types of the same shapes is determined by the substructure of these types.
4.3

Algorithmic Top-Like and Bottom-Like Judgements

Top-like and bottom-like types. Top-like and bottom-like types are types that are equivalent to ⊤and ⊥, respectively. Here we only want to use algorithmic top-like types, while the bottom-like typedefinition serves as an auxiliary relation. We present an algorithmic definition for both relationsin Figure 6. The most important addition in F𝑖+ ’s subtyping is the rule TL-var for type variables,
which allows a type variable to be top-like when its disjointness bound is a bottom-like type. For
example, in ∀𝛼 ∗ ⊥. 𝛼, any type that instantiates 𝛼 later must be disjoint to ⊥. Therefore it must be
disjoint to every type including itself. The correctness of the top-like judgment is given by:
Lemma 4.2 (Correctness of Algorithmic Top-like Types). C ≡Δ ⊤ if and only if Δ ⊢ ⊤ ≤C ∧ Δ ⊢ C ≤ ⊤.
4.4

Zero Type and Deterministic Type Difference with Polymorphism

The zero type function and deterministic type difference are defined in Figure 7. Most extensions
related to polymorphism are natural extensions that simply add the type context. Deterministic
type difference is essentially the same. The zero type function changes slightly. The only changes
are on type variables because we have a new top-like type using rule TL-var. Similarly to Section
3, the zero type function needs to have the soundness of zero type property to keep the rule TDAdisjoint and rule TDA-subtype consistent. So we separate two cases for type variable 𝛼. For 𝛼 Δ⊤ , 𝛼
is returned when the variable 𝛼 is top-like (i.e., the bound of the variable is bottom-like). Otherwise
return the type ⊤ if the variable 𝛼 is not top-like.
Lemma 4.3 (Soundness of zero type). If A ≡Δ ⊤, then A⊤
Δ = A.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31:20

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

⊤⊤
Δ = ⊤
⊥⊤
Δ
⊤
IntΔ

= ⊤
= ⊤

⊤
(A & B)Δ⊤ = A⊤
Δ & BΔ𝛼 Δ⊤ = ⊤ (if 𝛼 ∗ A ∈ Δ and A . ⊥)(A → B)Δ⊤ = A → B⊤Δ

𝛼 Δ⊤ = 𝛼 (if 𝛼 ∗ A ∈ Δ and A ≡ ⊥)⊤{l : B}⊤Δ = {l : BΔ }(∀𝛼 ∗ C. A)Δ⊤ = ∀𝛼 ∗ C. A⊤
Δ,𝛼 ∗ CA \𝑑 B =Δ C

(Deterministic Type Difference)

TDA-subtype
Δ⊢B≤A

TDA-disjoint
Δ ⊢ A∗B

A \𝑑 B =Δ A⊤
Δ

A \𝑑 B =Δ A

TDA-BCDA1  A  A2
A1 \𝑑 B =Δ C1

A ⊢ C1  C  C2
A2 \𝑑 B =Δ C2

A \𝑑 B =Δ C

Fig. 7. Zero type function and deterministic type difference.
Int \𝑎 ∀𝛼 ∗ A. B =Δ Int{l : A} \𝑎 ∀𝛼 ∗ B. C =Δ {l : A}
(A1 → A2 ) \𝑎 ∀𝛼 ∗ B1 . B2 =Δ A1 → A2
∀𝛼 ∗ A. B \𝑎 Int =Δ ∀𝛼 ∗ A. B
∀𝛼 ∗ A. B \𝑎 {l : C} =Δ ∀𝛼 ∗ A. B
∀𝛼 ∗ A1 . A2 \𝑎 (B1 → B2 ) =Δ ∀𝛼 ∗ A1 . A2
𝛼 \𝑎 𝛼 =Δ ⊤(if ¬(𝛼 ≡Δ ⊤))𝛼 \𝑎 A =Δ 𝛼

(if 𝛼 ∗ B ∈ Δ and A \𝑎 B =Δ A⊤
Δ)

A \𝑎 𝛼 =Δ A

(if 𝛼 ∗ B ∈ Δ and A \𝑎 B =Δ A⊤
Δ)∀𝛼 ∗ A1 . A2 \𝑎 ∀𝛼 ∗ B1 . B2 =Δ ∀𝛼 ∗ A1 . (A2 \𝑎 B2 )⊤(if B1 \ A1 =Δ B1 ⊤Δ and A2 \𝑎 B2 =Δ,𝛼 ∗ A1 A2 Δ,𝛼 ∗ A1 )∀𝛼 ∗ A1 . A2 \𝑎 ∀𝛼 ∗ B1 . B2 =Δ ∀𝛼 ∗ A1 . A2

(if A2 \𝑎 B2 =Δ,𝛼 ∗ (A1 & B1 ) A2 )Fig. 8. Selected algorithmic rules for type difference. Full rules can be found in the Appendix.

4.5

Algorithmic Type Difference and Theorems

Algorithmic Type Difference. Figure 8 shows selected rules for type difference, focusing on rules
involving disjoint quantification. The rules assume that the type context and two types are all
well-formed. We can still classify the rules into three categories: subtyping cases, disjoint cases andmixed cases. The correctness of such classification is ensured by Lemmas 3.12 to 3.14 extended
by a type context. These extended lemmas also guarantee that we can still give an algorithm forsubtyping by checking A \𝑎 B =Δ A⊤
Δ , and an algorithm for disjointness by checking A \𝑎 B =Δ A.
Theorems. Most of the properties are preserved. Using the same techniques as in Section 3, we
will reach the same main results below.
Lemma 4.4 (Type Difference Eqivalence). A \𝑑 B =Δ C if and only if A \𝑎 B =Δ C.
Theorem 4.5 (Type Difference Determinism). If A \𝑑 B =Δ C0 and A \𝑑 B =Δ C1 , then C0 = C1 .
Theorem 4.6 (Type Difference Completeness). If A \𝑑 B =Δ C, then A \𝑠 B ≡Δ C.
Theorem 4.7 (Type Difference Soundness). A \𝑠 B ≡Δ C iff ∃C0, A \𝑑 B =Δ C0 ∧ C ≡Δ C0 .
Theorem 4.8 (Decidability of Subtyping). Δ ⊢ A ≤ B is decidable.
Theorem 4.9 (Decidability of Type Difference). Type difference is decidable.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

Making a Type Difference

4.6

31:21

TypingWe show the bidirectional typing rules in Figure 9. The gray parts are for elaborating expressions
to the target language, which we will explain in the next section. We keep most of the typing
rules of F𝑖+ except for six rules Ela-rabs, Ela-annotabs, Ela-diff, Ela-diffe, Ela-rcdinf, andEla-proj. The other typing rules of F𝑖+ are explained in the Section 5. Rule Ela-rabs and rule Elaannotabs are the rules that help us inferring and checking the newly-added lambda and typeabstractions. Rule Ela-rcdinf offers a more convenient infer mode for records, which reduces thenumber of annotations with records. In F𝑖+ there is only a checking rule for records. Rule Ela-diffand rule Ela-diffe are the rules that employ type difference. Rule Ela-diff means removing thetype 𝐴 component of an expression 𝑒, while rule Ela-diffe means removing the conflicting typecomponents of 𝑒 1 that appear in another expression 𝑒 2 . Rule Ela-proj is changed with a record
projection operator l shown in Figure 9 to support multirecord selection so that an arbitrary label𝑙𝑖 can be retrieved from a record {𝑙 1 = 𝑒 1, , ..., , 𝑙𝑛 = 𝑒𝑛 }. The latter is not directly supported by F𝑖+ .
5

THE TARGET LANGUAGE AND ELABORATIONThis section shows the target language F𝑖+ [Fan et al. 2022] and explains the elaboration of F𝑖∖ .
5.1

Typing of F𝑖+

If we remove the six changed rules Ela-rabs, Ela-annotabs, Ela-diff, Ela-diffe, Ela-proj, andEla-rcdinf of F𝑖∖ as well as the elaboration component, then we have the typing rules for F𝑖+ needed
to show the type-safety of the elaboration.
Bidirectional Typing. The typing of F𝑖+ is bidirectional [Pierce and Turner 2000]. Under theinference mode ⇒, the minimal type of the expression is computed. Under the checking mode ⇐,we examine whether the expression is convertible to the given type. F𝑖+ chooses to use a bidirectional
type system because the disjoint merge is incompatible with a general subsumption rule [Huang
et al. 2021; Oliveira et al. 2016]. For example, Int is disjoint to Bool, thus we can merge terms like
1 ,, True. But without a bidirectional type system returning the exact type, we may encounter asituation where 1 ,, True is merged with a boolean (since Int & Bool ≤ Int), causing ambiguity. The
rule Ela-lit states that the type of an integer i is Int. The rule Ela-sub is the standard subsumption
rule. The rule Ela-anno shows how to check whether the expression has a given type. The rule Elamerge allows expressions of disjoint types A and B to be merged safely. The remaining F𝑖+ rules are
standard bidirectional typing for lambda abstractions, applications, type abstractions, fixpoints, etc.
5.2

Elaboration to F𝑖+

The elaboration generates an F𝑖+ expression in the gray parts of Figure 9. Most of the rules generate
an expression similar to the source expression. For instance, rule Ela-lit just keeps the same integer
i from the premise. The rule Ela-anno adds an annotation to the elaborated term e ′ just as theterm e being typed. The rules Ela-rabs, Ela-annotabs, and Ela-rcdinf add a type annotation sothat the new terms can be expressed and typed in F𝑖+ . Only rules Ela-proj, Ela-diff, and Ela-diffechange the structure.
Record Selection. The record projection operator l , shown at the bottom of Figure 9, is a functionthat will return ⊤ if it cannot retrieve any contents of label 𝑙, otherwise it will return a record that
contains all the information. The elaboration of record projection adds an annotation {l : C} in theelaboration so that multi-record selection can be interpreted by the target language. We also havethe following lemmas to show the elaboration is safe and deterministic.
Lemma 5.1 (Determinism of Record Distribution). If A l B and A l C then 𝐵 = 𝐶.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31:22

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

Δ; Γ ⊢ e1 ⇔ A ⇝ e2
Ela-top⊢Δ(Typing)
Ela-lit⊢ΔΔ⊢ΓΔ; Γ ⊢ {} ⇒ ⊤ ⇝ {}Ela-var
⊢Δ
Δ⊢Γ

Δ⊢Γ

Δ; Γ ⊢ i ⇒ Int ⇝ ix:A∈ΓΔ; Γ ⊢ x ⇒ A ⇝ x

Ela-rabs
Δ; Γ, x : A ⊢ e ⇐ B ⇝ e1

Ela-abs

Δ; Γ ⊢ 𝜆x. e ⇐ A → B ⇝ 𝜆x : A. e1

Δ; Γ ⊢ 𝜆x : A. e ⇒ A → B ⇝ (𝜆x : A. e1 ) : A → B

Δ; Γ, x : A ⊢ e ⇒ B ⇝ e1

Ela-rcdinf
Δ; Γ ⊢ e ⇒ A ⇝ e ′Ela-tabsΔ⊢ΓΔ, 𝛼 ∗ A; Γ ⊢ e ⇐ B ⇝ e1

Δ; Γ ⊢ {l = e} ⇒ {l : A} ⇝ {l = e ′ } : {l : A}

Δ; Γ ⊢ Λ𝛼 . e ⇐ ∀𝛼 ∗ A. B ⇝ Λ𝛼 . e1

Ela-annotabs
Δ⊢Γ

Ela-projA l {l : C}Δ, 𝛼 ∗ A; Γ ⊢ e ⇒ B ⇝ e1

Δ; Γ ⊢ e.l ⇒ C ⇝ (e ′ : {l : C}).l

Δ; Γ ⊢ Λ(𝛼 ∗ A). e ⇒ ∀𝛼 ∗ A. B ⇝ (Λ𝛼 . e1 ) : ∀𝛼 ∗ A. B
Ela-tapp
Δ ⊢ A ∗ C1

Δ; Γ ⊢ e ⇒ B ⇝ e ′Ela-diff
Δ; Γ ⊢ e ⇒ A ⇝ e ′B  ∀𝛼 ∗ C1 . C2

Δ; Γ ⊢ e A ⇒ C2 [𝛼 ↦→ A] ⇝ e ′ A
Ela-app
AB→C

Ela-merge
Δ ⊢ A∗B

Δ; Γ ⊢ e1 ⇒ A ⇝ e1′

Ela-subΔ⊢A≤B

Δ; Γ ⊢ e2 ⇐ B ⇝ e2′

Δ; Γ ⊢ e ⇒ A ⇝ e ′Δ; Γ ⊢ e ⇐ B ⇝ e ′Δ; Γ ⊢ e2 ⇒ B ⇝ e2′

Δ; Γ ⊢ e1 ,, e2 ⇒ A & B ⇝ e1′ ,, e2′

Ela-fix
Δ; Γ, x : A ⊢ e ⇐ A ⇝ e ′Δ; Γ ⊢ fix x : A. e ⇒ A ⇝ fix x : A. e ′Ela-diffe
A \𝑑 B =Δ C

Ela-anno
Δ; Γ ⊢ e ⇐ A ⇝ e ′A \𝑑 B =Δ C

Δ; Γ ⊢ e \ B ⇒ C ⇝ e ′ : C

Δ; Γ ⊢ e1 e2 ⇒ C ⇝ e1′ e2′Δ; Γ ⊢ e1 ⇒ A ⇝ e1′

Δ; Γ ⊢ e ⇒ A ⇝ e ′Δ; Γ ⊢ e1 ⇒ A ⇝ e1′

Δ; Γ ⊢ e2 ⇒ B ⇝ e2′

Δ; Γ ⊢ e1 \ e2 ⇒ C ⇝ e1′ : C

Δ; Γ ⊢ (e : A) ⇒ A ⇝ (e ′ : A)A l B(Record Projection Distribution)
l1 ≠ l2{l : A} l {l : A}
A 1 l ⊤⊤ l ⊤
A 2 l ⊤A1 & A2 l ⊤A1 → A2 l ⊤A 1 l ⊤∀𝛼 ∗ A1 . A2 l ⊤A2 l {l : B}

A1 & A2 l {l : B}

A1 l {l : B1 }A1 l {l : B}

{l2 : A} l1 ⊤A2 l ⊤

A1 & A2 l {l : B}

A2 l {l : B2 }A1 & A2 l {l : B1 & B2 }Fig. 9. Bidirectional type system for F𝑖∖ . Note that the syntax for modes is: ⇔ ≜ ⇐ | ⇒.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

Making a Type Difference

31:23

Lemma 5.2 (Safety of Record Distribution). If Δ ⊢ A, ⊢ Δ and A l B, then Δ ⊢ A ≤ B.

Adding Type Difference. Adding type difference is straightforward, since we just have to cast theexpression with the corresponding type computed by type difference. The safety of such casts isguaranteed by the equivalence with the type difference specification. We can get the following
property from the specification. Thus casting to type C is always safe.
Lemma 5.3 (Completeness of Subtyping). If A \𝑑 B =Δ C, then Δ ⊢ A ≤ C.
5.3

Theorems

Since F𝑖+ [Fan et al. 2022] is proven to be deterministic and type sound, we only need to show thatthe elaboration is deterministic and all elaborated terms are typeable in F𝑖+ . We first show that theelaboration is complete with respect to typing, that is:
Theorem 5.4 (Completeness of Elaboration with respect to Typing). ∃e1, Δ; Γ ⊢ e ⇔A ⇝ e1 iff Δ; Γ ⊢ e ⇔ A, where the typing here is the elaboration without the elaborated term.
Then by the determinism of A l B, we can prove the determinism of the elaboration.

Theorem 5.5 (Determinism of Inference). If Δ; Γ ⊢ e ⇒ A ⇝ e1 and Δ; Γ ⊢ e ⇒ B ⇝ e2 ,then 𝑒 1 = 𝑒 2 and 𝐴 = 𝐵.
Theorem 5.6 (Determinism of Checking). If Δ; Γ ⊢ e ⇐ A ⇝ e1 and Δ; Γ ⊢ e ⇐ A ⇝ e2 ,then 𝑒 1 = 𝑒 2 .
As for the typing results, since most of the elaboration rules keep the exact same terms andtypes, we only need non-trivial proofs for the six newly added cases. But the added cases use
annotations to ensure that we get the desired type. So we have the following results, ensuring thatthe elaboration preserves the same type after translation.
Theorem 5.7 (Type Preservation). If Δ; Γ ⊢ e ⇔ A ⇝ e ′, then in F𝑖+ , Δ; Γ ⊢ e ′ ⇔ A.
Summing up, we get the soundness of the calculus, i.e., the calculus is type-safe and deterministic.
6

RELATED WORKIn Section 2 we have already discussed in detail most closely related work, including set difference
in semantic subtyping [Frisch et al. 2008], type-indexed rows [Shields and Meijer 2001] and thework by Cardelli and Mitchell. Here we discuss other related work.
Record Calculi. Wand [1989] proposed a type system that requires constraints to signal whethera field is present or absent in every record type. His calculus uses a biased operator which always
overrides the first record by the second when these two records have conflicts. Harper and Pierce[1991b] enforce a compatibility check on every record concatenation and include the extension andrestriction operators. Their compatibility check # means that two records are safe to concatenate
without conflicts, providing a symmetric, unbiased merge. Compatibility is similar to disjointness
in F𝑖∖ . However, both Wand and Harper and Pierce do not consider subtyping.
Designing a record concatenation operator in a calculus with subtyping is a difficult problem,
as identified by Cardelli and Mitchell [1991]. Records may contain extra labels hidden by the subsumption rule, causing label conflicts to bypass the type system. Pottier [2000], extending the workof Rémy [1995], uses a constraint-based subtyping system to resolve label conflicts. Its constraints
require the presence or absence of certain labels, and supports asymmetric and symmetric concatenation. Cardelli and Mitchell’s work uses a subtyping system and negative quantification to resolve
conflicts, which is described in detail in Section 2. Zwanenburg [1995]’s adds record concatenation
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31:24

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

to a variant of System F<: and uses a compatibility check in the quantification. For example, hisfunctions are of the form 𝜆𝑋 ≤ 𝑇 ; 𝑋 #𝑇 .𝑒. His calculus includes intersection types and can beelaborated to System 𝐹 with pairs and records. Ohori [1992]’s work first uses a notion of record
kind, while Alves and Ramos [2021]’s work extends the record kind with negative information. In
Alves and Ramos’s work, a record kind requires explicit statements of whether a field is present or′ : 𝜏 ′ }} denotes the set ofabsent in the type. For example, the kind {{𝑙 1 : 𝜏1, ..., 𝑙𝑛 : 𝜏𝑛 ∥𝑙 0′ : 𝜏1′, ..., 𝑙𝑚𝑚types contain the fields before ∥ and do not contain the fields after ∥.
The commonality between these works is that they either use a biased operator in evaluation or
use negative quantification like compatibility or label absence in the type system. Both methods
are encodable in our system. The biased operator can be encoded by (e1 \ e2 ) ,, e2 while disjoint
quantification is a negative form of quantification. As for record operators, most works include
label extraction and record concatenation. Some of the works include label restriction, renaming
and overriding. As we have shown in Section 2, all of these operations are encodable in our system.
Disjoint Intersection Types. Disjoint intersection types were proposed by Oliveira et al. [2016] inthe 𝜆𝑖 calculus to address the non-determinism and subject reduction problem in Dunfield [2014]’swork. Dunfield’s calculus is equipped with an unrestricted merge operator for intersection types,
reducing merges in a non-deterministic process. Terms like e1 ,, e2 can be reduced to either e1 or e2 .
𝜆𝑖 imposes a disjointness restriction on the merge operator: only terms with disjoint types can bemerged. Therefore, reduction for the merge operator can be deterministic once the final type of the
program is decided. There are several extensions to 𝜆𝑖 [Alpuim et al. 2017; Bi et al. 2018, 2019] withrelaxed restrictions, BCD subtyping and disjoint polymorphism. Our work is based on the recent
calculus F𝑖+ [Bi et al. 2019; Fan et al. 2022], which is a calculus with disjoint polymorphism.
Compositional Programming and Restriction Operators. In OOP, mixin classes [Ancona et al. 2003;
Bracha and Cook 1990; Duggan and Sourelis 1996; Flatt et al. 1998] and traits [Fisher and Reppy
2004; Schärli et al. 2003] are two composition mechanisms for code reuse and multiple inheritance.
Name conflicts are a common problem. Usually, the mixin model allows overlapping fields and omits
the one with lower priority, like the biased merge operator. In contrast, for two traits to compose,
they must have no conflicts, like our unbiased merge operator. Conflicts have to be resolved before
composition by renaming, restriction or other operators. But even in the mixin model, such explicit
conflict-resolving operators are useful [Bracha 1992]. In Featherweight Jigsaw [Lagorio et al. 2009],
as in F𝑖∖ , both mechanisms are supported. Users can choose between the conflict-free merge andthe conflict-auto-solving merge. We share the same interpretation of overriding with Ancona andZucca [1998, 2002]: overriding = restriction + commutative merge. Both our work and their work
consider operators including renaming, restriction, and overriding. While the merge in their work
has similar semantics to ours, it is limited to mixins and it always has a mixin type. Moreover, wedevelop a general type difference operator that works for types other than records (or record-likethings like objects/modules), and we recover the operators on records/traits from that.
Compositional Programming [Zhang et al. 2021] is a recently proposed modular programming
paradigm based on first-class traits [Bi and Oliveira 2018], and implemented by the CP language.
CP uses disjoint intersection types to naturally solve the Expression Problem [Wadler 1998] andoffers modular pattern matching and dependency injection. In earlier versions of the CP language,
only a weak (and ad-hoc) restriction operator was supported due to the lack of a theory of type
difference. This operator enabled explicitly resolving conflicts on traits:
t1 = trait ⇒ { f = 1; g = "a" };t3 = trait [self: Top] inherits t1 \ {f: Int} & t2 \ {g: String} ⇒ {override f = super.f + (t1 ^ self).f};

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

Making a Type Difference

31:25

Since we can only remove a certain label using an exclusion operator \, this still required userwritten annotations when dealing with merges and inheritance.
Similar approaches are also adopted in previously mentioned OOP designs except that they
provide a more convenient way to override or rename methods to resolve conflicts. But all theseworks only discuss label manipulation, not dealing with function (and other forms of) type difference.
In the CP language, such an ad-hoc restriction is especially problematic because it requires explicit
type annotations, such as {f : Int} above. But with the new operators based on the type difference
that we provide, we can now address the problem in CP with fewer annotations and also convenient
operators such as biased merges, which were previously not available. As we have shown in
Section 2.4, type difference is more generally applicable since it is not restricted to objects orrecords. This enables new applications, such as updating implementations of overloaded functions.
Furthermore it plays well with our encoding of traits, which is based on functions that return
records, rather than primitive objects or records.
Semantic Subtyping. As we have discussed in Section 2.3, semantic subtyping [Castagna andFrisch 2005; Frisch et al. 2008] adopts a set-theoretic view to define the subtraction of two types.
Current systems with semantic subtyping support records and related operations with biased record
concatenation [Benzaken et al. 2013; Castagna 2018]. A type-level merge operator is defined to
calculate the type for concatenated or restricted records. Records have a deterministic runtime
behavior, but their typing rule is quite unique. They are not typed by intersections but by labelindexed function types that may have a union type as its return type. Here we show the definitionof the type-level operator as it also uses the type difference defined in semantic subtyping.
(𝑅1 (𝑙)
if 𝑅1 (𝑙)&𝐴 ≤ ⊥(𝑅1 ,𝐴 𝑅2 ) (𝑙) ≡(𝑅1 (𝑙)\𝐴)|𝑅2 (𝑙) otherwise
In the second case, 𝑅1 (𝑙) subtracts 𝐴 and adds 𝑅2 (𝑙) back. In concatenation, 𝐴 is a special constantthat stands for an undefined field and 𝑅1 is the rightmost record, which has the highest priority. So
when 𝑅1 is undefined on 𝑙, the corresponding field type in 𝑅2 will be returned. We can see herethat union types play a similar role to intersection types in our system as we have very different
interpretations. This operator is specific to records, unlike our type difference, which is generalized
to cover other types.
7

CONCLUSION

In this paper, we present a theory of type difference, and design a F𝑖∖ calculus carrying out such
type difference via an elaboration to the F𝑖+ calculus. We derive a general type difference thatworks for all types from a specification with three simple but essential requirements to a sound,complete, deterministic and algorithmic formulation, verified by the Coq proof assistant. Besides
the theoretical aspects, type difference is expressive enough to encode all the record operators inrecord calculi with subtyping. These operators include concatenation, restriction, overriding andrenaming. Type difference is also useful for languages with traits and compositional programming,
since it can deal with inheritance and merge conflicts, avoiding heavy annotations that would beotherwise necessary. Future work includes studying even more expressive subtyping relations that
include additional features, such as union types [Barbanera et al. 1995].
ACKNOWLEDGMENTS
We are particularly grateful to Yaozhu Sun, who implemented type difference in CP. We thank theanonymous reviewers for their helpful comments. This work has been sponsored by Hong Kong
Research Grant Council projects number 17209519, 17209520 and 17209821.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31:26

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

REFERENCES
João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. 2017. Disjoint Polymorphism. In European Symposium on Programming(ESOP). https://doi.org/10.1145/1391289.1391293
Sandra Alves and Miguel Ramos. 2021. An ML-style Record Calculus with Extensible Records. Electronic Proceedings in
Theoretical Computer Science 351 (dec 2021), 1–17. https://doi.org/10.4204/eptcs.351.1
Davide Ancona, Giovanni Lagorio, and Elena Zucca. 2003. Jam—designing a Java extension with mixins. ACM Transactions
on Programming Languages and Systems (TOPLAS) 25, 5 (2003), 641–712. https://doi.org/10.1145/937563.937567
Davide Ancona and Elena Zucca. 1998. A theory of mixin modules: Basic and derived operators. Mathematical structures incomputer science 8, 4 (1998), 401–446. https://doi.org/10.1017/S0960129598002576
Davide Ancona and Elena Zucca. 2002. A calculus of module systems. Journal of functional programming 12, 2 (2002),
91–132. https://doi.org/10.1017/S0956796801004257
Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de’Liguoro. 1995. Intersection and Union Types: Syntax and
Semantics. Information and Computation 119, 2 (June 1995), 202–230.
Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983. A Filter Lambda Model and the Completenessof Type Assignment. The Journal of Symbolic Logic 48, 4 (1983), 931–940. http://www.jstor.org/stable/2273659
Véronique Benzaken, Giuseppe Castagna, Kim Nguyen, and Jérôme Siméon. 2013. Static and dynamic semantics of NoSQL
languages. ACM SIGPLAN Notices 48, 1 (2013), 101–114. https://doi.org/10.1145/2480359.2429083
Xuan Bi and Bruno C. d. S. Oliveira. 2018. Typed First-Class Traits. In 32nd European Conference on Object-Oriented
Programming (ECOOP 2018). https://doi.org/10.4230/LIPIcs.ECOOP.2018.9
Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2018. The Essence of Nested Composition. In 32nd European Conference
on Object-Oriented Programming, ECOOP 2018, July 16-21, 2018, Amsterdam, The Netherlands (LIPIcs, Vol. 109), Todd D.
Millstein (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 22:1–22:33. https://doi.org/10.4230/LIPIcs.ECOOP.
2018.22
Xuan Bi, Ningning Xie, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. Distributive Disjoint Polymorphism for Compositional Programming. In European Symposium on Programming (ESOP). https://doi.org/10.1007/978-3-030-17184-1_14
Gilad Bracha. 1992. The programming language Jigsaw: mixins, modularity and multiple inheritance. The University of
Utah.
Gilad Bracha and William Cook. 1990. Mixin-based inheritance. ACM Sigplan Notices 25, 10 (1990), 303–311. https://doi.org/10.1145/97945.97982
Luca Cardelli, Simone Martini, John C Mitchell, and Andre Scedrov. 1994. An extension of system F with subtyping.
Information and Computation 109, 1-2 (1994), 4–56.
Luca Cardelli and John Mitchell. 1991. Operations on Records. Mathematical Structures in Computer Science 1 (1991), 3–48.
Luca Cardelli and Peter Wegner. 1985. On Understanding Types, Data Abstraction, and Polymorphism. ACM Comput. Surv.
17, 4 (dec 1985), 471–523. https://doi.org/10.1145/6041.6042
Giuseppe Castagna. 2018. Covariance and Controvariance: a fresh look at an old issue (a primer in advanced type systems
for learning functional programmers). CoRR abs/1809.01427 (2018). arXiv:1809.01427 http://arxiv.org/abs/1809.01427
Giuseppe Castagna and Alain Frisch. 2005. A Gentle Introduction to Semantic Subtyping. In Proceedings of the 7th ACM
SIGPLAN International Conference on Principles and Practice of Declarative Programming (Lisbon, Portugal) (PPDP ’05).
Association for Computing Machinery, New York, NY, USA, 198–208. https://doi.org/10.1145/1069774.1069793
Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, and Pietro Abate. 2015. Polymorphic Functions with Set-Theoretic Types: Part
2: Local Type Inference and Type Reconstruction. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages (Mumbai, India) (POPL ’15). Association for Computing Machinery, New York,NY, USA, 289–302. https://doi.org/10.1145/2676726.2676991
Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, and Luca Padovani. 2014. Polymorphic
Functions with Set-Theoretic Types: Part 1: Syntax, Semantics, and Evaluation. In Proceedings of the 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (San Diego, California, USA) (POPL ’14). Association for
Computing Machinery, New York, NY, USA, 5–17. https://doi.org/10.1145/2535838.2535840
Giuseppe Castagna, Tommaso Petrucciani, and Kim Nguyundefinedn. 2016. Set-Theoretic Types for Polymorphic Variants.
In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Nara, Japan) (ICFP 2016).
Association for Computing Machinery, New York, NY, USA, 378–391. https://doi.org/10.1145/2951913.2951928
Giuseppe Castagna and Zhiwu Xu. 2011. Set-Theoretic Foundation of Parametric Polymorphism and Subtyping. In Proceedingsof the 16th ACM SIGPLAN International Conference on Functional Programming (Tokyo, Japan) (ICFP ’11). Association for
Computing Machinery, New York, NY, USA, 94–106. https://doi.org/10.1145/2034773.2034788
William R. Cook and Jens Palsberg. 1989. A denotational semantics of inheritance and its correctness. In Object-Oriented
Programming: Systems, Languages and Applications (OOPSLA). https://doi.org/10.1145/74878.74922
Mario Coppo and Mariangiola Dezani-Ciancaglini. 1978. A new type assignment for 𝜆-terms. Archiv für mathematische
Logik und Grundlagenforschung 19, 1 (1978), 139–156.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

Making a Type Difference

31:27

Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1981. Functional Characters of Solvable Terms. Math. Log.
Q. 27, 2-6 (1981), 45–58. https://doi.org/10.1002/malq.19810270205
Rowan Davies and Frank Pfenning. 2000. Intersection Types and Computational Effects. In Proceedings of the Fifth ACM
SIGPLAN International Conference on Functional Programming (ICFP ’00). Association for Computing Machinery, New
York, NY, USA, 198–208. https://doi.org/10.1145/351240.351259
Dominic Duggan and Constantinos Sourelis. 1996. Mixin modules. ACM SIGPLAN Notices 31, 6 (1996), 262–273.
Jana Dunfield. 2014. Elaborating intersection and union types. Journal of Functional Programming (JFP) 24, 2-3 (2014),
133–165. https://doi.org/10.1006/inco.1995.1086
Andong Fan, Xuejing Huang, Han Xu, Yaozhu Sun, and Bruno C. d. S. Oliveira. 2022. Direct Foundations for Compositional
Programming. In 36th European Conference on Object-Oriented Programming (ECOOP 2022) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 222), Karim Ali and Jan Vitek (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik,
Dagstuhl, Germany, 18:1–18:28. https://doi.org/10.4230/LIPIcs.ECOOP.2022.18
Kathleen Fisher and John Reppy. 2004. A typed calculus of traits. In Electronic proceedings of FOOL, Vol. 2004.
Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. 1998. Classes and mixins. In Proceedings of the 25th ACM
SIGPLAN-SIGACT symposium on Principles of programming languages. 171–183. https://doi.org/10.1145/268946.268961
Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. 2008. Semantic Subtyping: Dealing Set-Theoretically with
Function, Union, Intersection, and Negation Types. J. ACM 55, 4, Article 19 (Sept. 2008), 64 pages. https://doi.org/10.
1145/1391289.1391293
Robert Harper and Benjamin Pierce. 1991a. A record calculus based on symmetric concatenation. In Proceedings of the 18th
ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 131–142. https://doi.org/10.1145/99583.99603
Robert Harper and Benjamin Pierce. 1991b. A Record Calculus Based on Symmetric Concatenation. In Proceedings of the
18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Orlando, Florida, USA) (POPL ’91).
Association for Computing Machinery, New York, NY, USA, 131–142. https://doi.org/10.1145/99583.99603
Xuejing Huang, Jinxu Zhao, and Bruno C. d. S. Oliveira. 2021. Taming the Merge Operator. 31 (2021). https://doi.org/10.
1017/S0956796821000186 Publisher: Cambridge University Press.
Young Bae Jun, Hee Sik Kim, and Eun Hwan Roh. 2004. Ideal theory of subtraction algebras. Sci. Math. Jpn. Online e-2004(2004), 397–402.
Giovanni Lagorio, Marco Servetto, and Elena Zucca. 2009. Featherweight Jigsaw: A minimal core calculus for modular
composition of classes. In European Conference on Object-Oriented Programming. Springer, 244–268.
Zhaohui Luo. 1999. Coercive Subtyping. J. Log. Comput. 9, 1 (1999), 105–130. https://doi.org/10.1093/logcom/9.1.105
Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias. 2020. Resolution as Intersection
Subtyping via Modus Ponens. Proc. ACM Program. Lang. 4, OOPSLA, Article 206 (nov 2020). https://doi.org/10.1145/
3428274
Atsushi Ohori. 1992. A Compilation Method for ML-Style Polymorphic Record Calculi. In Proceedings of the 19th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Albuquerque, New Mexico, USA) (POPL ’92).
Association for Computing Machinery, New York, NY, USA, 154–165. https://doi.org/10.1145/143165.143200
Atsushi Ohori. 1995. A polymorphic record calculus and its compilation. ACM Transactions on Programming Languages andSystems (TOPLAS) 17, 6 (1995), 844–895. https://doi.org/10.1145/218570.218572
Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. 2016. Disjoint intersection types. In International Conference on
Functional Programming (ICFP). https://doi.org/10.1145/2951913.2951945
Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Trans. Program. Lang. Syst. 22, 1 (jan 2000), 1–44.
https://doi.org/10.1145/345099.345100
François Pottier. 2000. A 3-Part Type Inference Engine. In Programming Languages and Systems, Gert Smolka (Ed.). Springer
Berlin Heidelberg, Berlin, Heidelberg, 320–335.
Garrel Pottinger. 1980. A type assignment for the strongly normalizable 𝜆-terms. To HB Curry: essays on combinatory logic,
lambda calculus and formalism (1980), 561–577.
Didier Rémy. 1990. Type inference for records in a natural extension of ML. Technical Reports (CIS) (1990), 641.
Didier Rémy. 1995. A case study of typechecking with constrained types: Typing record concatenation. (August 1995).
Presented at the workshop on Advances in types for computer science at the Newton Institute, Cambridge, UK.
John C Reynolds. 1988. Preliminary design of the programming language Forsythe. Technical Report. Carnegie Mellon
University.
John C. Reynolds. 1991. The coherence of languages with intersection types. In Lecture Notes in Computer Science (LNCS).
Springer Berlin Heidelberg, 675–700.
John C Reynolds. 1997. Design of the programming language Forsythe. In ALGOL-like languages. 173–233.
Scala Community. 2022. Tour of Scala Self-type. https://docs.scala-lang.org/tour/self-types.html.
Nathanael Schärli, Stéphane Ducasse, Oscar Nierstrasz, and Andrew P Black. 2003. Traits: Composable units of behaviour.
In European Conference on Object-Oriented Programming (ECOOP).

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.

31:28

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

Boris M Schein. 1992. Difference semigroups. Communications in algebra 20, 8 (1992), 2153–2169.
Mark Shields and Erik Meijer. 2001. Type-Indexed Rows. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (London, United Kingdom) (POPL ’01). Association for Computing Machinery, New
York, NY, USA, 261–275. https://doi.org/10.1145/360204.360230
Pablo Tesone, Stéphane Ducasse, Guillermo Polito, Luc Fabresse, and Noury Bouraqadi. 2020. A new modular implementation
for stateful traits. Science of Computer Programming 195 (2020), 102470.
Philip Wadler. 1998. The expression problem. Java-genericity mailing list (1998).
M. Wand. 1989. Type inference for record concatenation and multiple inheritance. In [1989] Proceedings. Fourth Annual
Symposium on Logic in Computer Science. 92–97. https://doi.org/10.1109/LICS.1989.39162
Ningning Xie, Bruno C. d. S. Oliveira, Xuan Bi, and Tom Schrijvers. 2020. Row and Bounded Polymorphism via Disjoint
Polymorphism. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). https://doi.org/10.4230/
LIPIcs.ECOOP.2020.27
Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira. 2022. Making a Type Difference: Subtraction on Intersection Types as
Generalized Record Operations (Artifact). https://doi.org/10.5281/zenodo.7151418
Weixin Zhang, Yaozhu Sun, and Bruno C. d. S. Oliveira. 2021. Compositional Programming. ACM Transactions on
Programming Languages and Systems (TOPLAS) 43, 3 (2021), 1–61. https://doi.org/10.1145/3460228
Jan Zwanenburg. 1995. Record concatenation with intersection types. Technical Report 95-34. Eindhoven University ofTechnology.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 31. Publication date: January 2023.