Direct Foundations for Compositional Programming
Andong Fan1 !
Zhejiang University, Hangzhou, China

Xuejing Huang1 !
The University of Hong Kong, China

Han Xu !
Peking University, Beijing, China

Yaozhu Sun !
The University of Hong Kong, China

Bruno C. d. S. Oliveira !
The University of Hong Kong, China
Abstract
The recently proposed CP language adopts Compositional Programming: a new modular programming style that solves challenging problems such as the Expression Problem. CP is implemented on+
top of a polymorphic core language with disjoint intersection types called F+
i . The semantics of Fi
employs an elaboration to a target language and relies on a sophisticated proof technique to provethe coherence of the elaboration. Unfortunately, the proof technique is technically challenging andhard to scale to many common features, including recursion or impredicative polymorphism. Thus,
the original formulation of F+
i does not support the two later features, which creates a gap between
theory and practice, since CP fundamentally relies on them.
This paper presents a new formulation of F+i based on a type-directed operational semantics(TDOS). The TDOS approach was recently proposed to model the semantics of languages withdisjoint intersection types (but without polymorphism). Our work shows that the TDOS approach
can be extended to languages with disjoint polymorphism and model the full F+i calculus. Unlike theelaboration semantics, which gives the semantics to F+
indirectlyviaatargetlanguage, the TDOSiapproach gives a semantics to F+
directly.
With
a
TDOS,
there
is
no
need
for
a coherence proof.
iInstead, we can simply prove that the semantics is deterministic. The proof of determinism only uses
simple reasoning techniques, such as straightforward induction, and is able to handle problematicfeatures such as recursion and impredicative polymorphism. This removes the gap between theory
and practice and validates the original proofs of correctness for CP. We formalized the TDOS variantof the F+i calculus and all its proofs in the Coq proof assistant.
2012 ACM Subject Classification Theory of computation → Type theory
Keywords and phrases Intersection types, disjoint polymorphism, operational semantics
Digital Object Identifier 10.4230/LIPIcs.ECOOP.2022.18
Related Version Extended Version: https://arxiv.org/abs/2205.06150
Supplementary Material Supplements can be found as follows:
Software (ECOOP 2022 approved artifact): https://doi.org/10.4230/DARTS.8.2.4
Software (Coq formalization): https://github.com/andongfan/CP-Foundations
Software (Online demo of CP implementation): https://plground.org
Funding This research was funded by the University of Hong Kong and Hong Kong Research Grants
Council projects number 17209519, 17209520 and 17209821.
Acknowledgements We thank the anonymous reviewers for their helpful comments.

1

The first two authors contributed equally to this work.

© Andong Fan, Xuejing Huang, Han Xu, Yaozhu Sun, and Bruno C. d. S. Oliveira;licensed under Creative Commons License CC-BY 4.0
36th European Conference on Object-Oriented Programming (ECOOP 2022).
Editors: Karim Ali and Jan Vitek; Article No. 18; pp. 18:1–18:28
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

18:2

Direct Foundations for Compositional Programming

1

Introduction

Compositional Programming [46] is a recently proposed modular programming paradigm.
It offers a natural solution to the Expression Problem [42] and novel approaches to modular pattern matching and dependency injection. The CP language adopts Compositional
Programming. In CP, several new programming language constructs enable Compositional
Programming. Of particular interest for this paper, CP has a notion of typed first-classtraits [5], which are extended in CP to also enable a form of family polymorphism [16].
The semantics of CP and its notion of traits is defined via an elaboration to the corecalculus F+i [7]: a polymorphic core language with a merge operator [34] and disjoint
intersection types [30]. The elaboration of traits is inspired by Cook’s denotational semantics
of inheritance [12]. In the denotational semantics of inheritance, the key idea is thatmechanisms such as classes or traits, which support self-references (a.k.a. the this keyword
in conventional OOP languages), can be modeled via open recursion. In other words, theencoding of classes or traits is parametrized by a self-reference. This allows late binding of selfreferences at the point of instantiation and enables the modification and composition of traits
before instantiation. Instantiation happens when new is used, just as in conventional OOP
languages. When new is used, it essentially closes the recursion by binding the self-reference,
which then becomes a recursive reference to the instantiated object. In the denotationalsemantics of inheritance, new is just a fixpoint operator.
The semantics of the original formulation of F+i [7] itself is also given by an elaboration
into Fco , a System F-like language with products. Unlike F+
i , Fco has no subtyping orintersection types, and it has a conventional operational semantics. The main reason for F+ito use elaboration is that F+
i has a type-dependent semantics: types may affect the runtime
behavior of a program. The elaboration semantics for F+
i seems like a natural choice, since
this is commonly seen in various other type-dependent languages and calculi. For instance,
the semantics of type-dependent languages with type classes [43], Scala-style implicits [29]or gradual typing [40] all usually adopt an elaboration approach. In contrast, in the past,
more conventional direct formulations using an operational semantics have been avoided for
languages with a type-dependent semantics. The appeals of the elaboration semantics are
simple type-safety proofs, and the fact that they directly offer an implementation techniqueover conventional languages without a type-dependent semantics.
There are also important drawbacks when using an elaboration semantics. One of themis simply that more infrastructure is needed for a target language (such as Fco ) and its
associated semantics and metatheory. Moreover, the elaboration semantics is indirect, andto understand the semantics of a program, we must first translate it to the target language(which may be significantly different from the source) and then reason in terms of thetarget. More importantly, besides type-safety, another property that is often desirable for an
elaboration semantics is coherence [35]. Many elaboration semantics are non-deterministic:
the same source program can elaborate into different target programs. If those different
programs have a different semantics, then this is problematic, as it would imply that thesource language would have a non-deterministic or ambiguous semantics. Coherence ensuresthat even if the same program elaborates to different target expressions, the different target
expressions are semantically equivalent, eventually evaluating to the same result.
For some languages, including F+
i , proving coherence is highly non-trivial and hard toscale to common programming language features. For the original F+i , the proof of coherence
comes at the cost of simple features such as recursion and impredicative polymorphism. The
proof of coherence for F+
i is based on a logical relation called canonicity [6]. Together with a

A. Fan, X. Huang, H. Xu, Y. Sun, and B. C. d. S. Oliveira

18:3

notion of contextual equivalence, the two techniques are used to prove coherence. The useof logical relations is a source of complexity in the proof and the reason why recursion andimpredicative polymorphism have not been supported. For recursion, in principle, the use ofa more sophisticated step-indexed logical relation [3] may enable a proof of coherence, at thecost of some additional complexity. However, due to the extra complexity, this was left for
future work. For impredicative polymorphism, Bi et al. [7] identified important technicalchallenges, and it is not known if the proof can be extended with such a feature.
The absence of recursion and impredicative polymorphism creates a gap between theory
and practice, since CP fundamentally relies on them. Moreover, the proofs of correctnessof CP rely on the assumption that F+
i with recursion and impredicative polymorphism
would preserve all the properties of F+i . Impredicative polymorphism is needed in CP toallow the types of traits with polymorphic methods to be used as type parameters for otherpolymorphic functions. Recursion is needed in CP because the denotational semantics uses
fixpoint operators to instantiate traits. In addition, the fixpoint operators must be lazy;otherwise, self-references can easily trigger non-termination. Therefore, a call-by-name (CBN)semantics is more natural and also assumed in the CP encoding of traits. However, thesemantics of the Fco calculus is call-by-value (CBV) and, by inheritance, the elaboration
semantics of F+i has a CBV semantics as well.
This paper presents a new formulation of F+i based on a type-directed operational semantics(TDOS) [20]. The TDOS approach has recently been proposed to model the semantics oflanguages with disjoint intersection types (but without polymorphism). Although F+
i is nota new calculus, we revise its formulation significantly in this paper. Our new formulation of+F+
i is different from the original one in three aspects. Firstly, the semantics of the original Fi+
is given by elaborating to Fco , while our semantics for Fi is a direct operational semantics.
Secondly, our new formulation of F+i supports recursion and impredicative polymorphism.
Finally, we employ a call-by-name evaluation strategy.
Our work shows that the TDOS approach can be extended to languages with disjoint
polymorphism and model the complete F+i calculus with recursion and impredicative polymorphism. Moreover, there is no need for a coherence proof. Instead, we can simply provethat the semantics is deterministic. The proof of determinism uses only simple reasoning
techniques, such as straightforward induction, and is able to handle problematic features
such as recursion and impredicative polymorphism. Thus, this removes the gap between
theory and practice and validates the original proofs of correctness for the CP language.
Figure 1 contrasts the differences in terms of proofs and implementation of CP using Zhang
et al.’s original work and our own work. We formalized the TDOS variant of the F+i calculus,
together with its type-soundness and determinism proof in the Coq proof assistant. Moreover,
we have a new implementation of CP based on our new reformulation of F+i .
In summary, the contributions of this work are:
CBN F+
i with recursion and impredicative polymorphism. This paper presents a
CBN variant of F+i extended with recursion and impredicative polymorphism.
Determinism and type-soundness for F+
i using a TDOS. We prove the typesoundness and determinism of F+
usingadirectTDOS. These proofs validate the proofsiof correctness previously presented for CP by Zhang et al. [46].
Technical innovations. Our formulation of F+i has various technical innovations over
the original one, including a new formulation of subtyping using splittable types [22] andmore flexible term applications.
Implementation and Mechanical formalization. We formalized the TDOS variantof the F+i calculus, together with its type-soundness and determinism proof in the Coq

ECOOP 2022

18:4

Direct Foundations for Compositional Programming

Fco

+

Fi
CP proof ﬂow by
Zhang et al.

type-safety

type-soundness

coherenceelaboration

indirect semantics

determinism
direct semantics

call-by-valueCPhaving neither recursion nor
impredicative polymorphism

type-safety
coherenceelaboration

assuming call-by-name,+Fi

recursion, and impredicative
polymorphism

type-soundness
determinism
direct semantics

CP proof ﬂow in
our work

call-by-namehaving recursion andimpredicative polymorphism

Figure 1 Contrasting the flow of results for CP using the original formulation, and our work.

proof assistant. We also have a new implementation of CP built on top of a TDOS
formulation of F+i available at https://plground.org. The full Coq formalizationand the extended version of this paper are available at:https://github.com/andongfan/CP-Foundations

2

Motivations and Technical Innovations

In this section, we introduce Compositional Programming by example and show how CP
traits elaborate to F+
i expressions. After that, we will discuss the practical issues that
motivate us to reformulate F+
i , as well as technical challenges and innovations.

2.1

Compositional Programming by Example

To demonstrate the capabilities of Compositional Programming, we show how to solve a
variant of the Expression Problem [42] in the CP language. Our solution is adapted fromthe original one by Zhang et al. [46]. In this variant, in addition to the usual challenge ofextensibility in multiple directions, we also consider the problem of context evolution [25, 37],
so the interpreter may require different contextual information for different features of theinterpreter. The CP language allows a modular solution to both challenges, which also
illustrates some key features in Compositional Programming, including first-class traits [5],nested composition [6], and disjoint polymorphism [2].
Examples are based on a simple expression language, and the goal is to perform various
operations over it, such as evaluation and free variable bookkeeping. The expression language
consists of numbers, addition, variables, and let-bindings. Besides CP code, we also provide
analogous Haskell code in the initial examples so that readers can connect them with existing
concepts in functional languages.
Compositional interfaces. First, we define the compositional interface for numeric literals
and addition. The compositional interface at the top of Figure 2a is similar to Haskell’s
algebraic data type at the top of Figure 2b. Exp is a special kind of type parameter in CP
called a sort, which serves as the return type of both constructors Lit and Add. Sorts will
be instantiated with concrete representations later. Internally, sorts are handled differently
from normal type parameters [46]. In accordance with the compositional interface, we canthen define how to evaluate the expression language.

A. Fan, X. Huang, H. Xu, Y. Sun, and B. C. d. S. Oliveira

type NumSig<Exp> = {Lit : Int → Exp;
Add : Exp → Exp → Exp;};

data Exp where
Lit :: Int → Exp
Add :: Exp → Exp → Exp

type Eval Ctx = { eval : Ctx → Int };evalNum Ctx = trait implements
NumSig<Eval Ctx> ⇒ {(Litn).eval _= n;(Add e1 e2).eval ctx =e1.eval ctx + e2.eval ctx;};

type Eval ctx = ctx → Int(a) CP code.

(b) Haskell counterpart.

18:5

eval :: Exp → Eval ctx
eval (Litn) _= neval (Add e1 e2) ctx =eval e1 ctx + eval e2 ctx

Figure 2 Initial expression language: numbers and addition.
type VarSig<Exp> = {Let : String → Exp → Exp → Exp;
Var : String → Exp;};
type Env = { env : String → Int };evalVar (Ctx*Env) = trait implements VarSig<Eval (Env&Ctx)> ⇒ {(Let s e1 e2).eval ctx = e2.eval{ ctx with env = insert s (e1.eval ctx) ctx.env };(Vars).eval ctx = lookup s ctx.env;};
Figure 3 Adding more expressions: variables and let-bindings.

Polymorphic contexts. As shown in the middle of Figure 2a, the type Eval declares amethod eval that takes a context and returns an integer. Ctx is a type parameter that canbe instantiated later, enabling particular traits to assume particular contextual information
for the needs of various features. The technique is called polymorphic contexts [46] inCompositional Programming.
Compositional traits. The trait evalNum in Figure 2a is parametrized by a type parameter
Ctx. Note that, in CP, type parameters always start with a capital letter, while regularparameters are lowercase. The trait evalNum implements the compositional interface NumSig
by instantiating it with the sort Eval Ctx. Traits are the basic reusable unit in CP, which
are usually type-checked against compositional interfaces. In this trait, we use a lightweight
syntax called method patterns to define how to evaluate different expressions. Such a definition
is analogous to pattern matching in Figure 2b. Since Lit and Add do not need to be consciousof any information in the context, the type parameter Ctx is unconstrained. The only thingthat we can do to the polymorphic context is either to ignore it (like in Lit) or to pass it torecursive calls (like in Add).
More expressions. Adding more constructs to the expression language is awkward in Haskell
because algebraic data types are closed. However, language components can be modularly
declared in CP. Two new constructors, Let and Var, are declared in the second compositional
interface VarSig, as shown in Figure 3. Then the two traits implement VarSig using method

ECOOP 2022

18:6

Direct Foundations for Compositional Programming

type FV = { fv : [String] };fv = trait implements ExpSig<FV> ⇒ {(Litn).fv = [];(Adde1 e2).fv = union e1.fv e2.fv;(Let s e1 e2).fv = union e1.fv (delete s e2.fv);(Vars).fv = [s];};evalWithFV (Ctx*Env) = trait implements ExpSig<FV ⇒ Eval (Env&Ctx)> ⇒ {(Litn).eval _= n;(Add
e1 e2).eval ctx = e1.eval ctx + e2.eval ctx;
(Let s e1 e2).eval ctx = if elem s e2.fv
then e2.eval { ctx with env = insert s (e1.eval ctx) ctx.env }else e2.eval ctx;
(Vars).eval ctx = lookup s ctx.env;};
Figure 4 Adding more operation: free variable bookkeeping and another version of evaluation.

patterns for the new constructors. Since the two new expressions need to inspect or update
some information in the context, we expose the appropriate Env part to evalVar, while theremaining context is kept polymorphic. This is achieved with the disjointness constraint [2]Ctx*Env in evalVar. A disjointness constraint denotes that the type parameter Ctx is
disjoint to the type Env. In other words, types that instantiate Ctx cannot overlap with thetype Env. Also note that the notation { ctx with env = ... } denotes a polymorphic
record update [9]. In the code for let-expressions, we need to update the environment in therecursive calls to extend it with a new entry for the let-variable.
Intersection types. Independently defined interfaces can be composed using intersection
types. For example, ExpSig below is an intersection of NumSig and VarSig, containing all of
the four constructors:
type ExpSig<Exp> = NumSig<Exp> & VarSig<Exp>;-= { Lit : ...; Add : ...; Let : ...; Var : ... };More operations. Not only can expressions be modularly extended, but we can easily add
more operations. In Figure 4, a new trait fv modularly implements a new operation thatrecords free variables in an expression. Here, union and delete are two library functions
for arrays. The modular definition of fv is quite natural in functional programming, but it
is hard in traditional object-oriented programming. We have to modify the existing classdefinitions and supplement them with a method. This is typical of the well-known Expression
Problem. In summary, we have shown that Compositional Programming can solve bothdimensions of this problem: adding expressions and operations.
Dependency injection. Besides the Expression Problem, Figure 4 also shows anothersignificant feature of CP: dependency injection. In evalWithFV, a new implementation ofevaluation is defined with a dependency on free variables. The method pattern for Let will
check if s appears as a free variable in e2. If so, it evaluates e1 first as usual; otherwise, we
do not need to do any computation or update the environment since s is not used at all.
Note that the compositional interface ExpSig is instantiated with two types separated by a
fat arrow (⇒) (⇒ was originally denoted by % in Zhang et al.’s implementation of CP). FV
on the left-hand side is the dependency of evalWithFV. In other words, the definition of

A. Fan, X. Huang, H. Xu, Y. Sun, and B. C. d. S. Oliveira

18:7

evalWithFV depends on another trait that implements ExpSig<FV>. The static type checkerof CP will check this fact later at the point of trait instantiation. With such dependency
injection, we can call e2.fv even if evalWithFV does not have an implementation of fv. In
other words, evalWithFV depends only on the interface of fv (the type FV), but not any
concrete implementation.
Self-type annotations. Before we show how to perform the new version of the evaluation
over the whole expression language, we want to create a repository of expressions for later
use. We expect that these expressions are unaware of any concrete operation, so we use apolymorphic Exp type to denote some abstract type of expressions. The code that creates
the repository of expressions is1 :repo Exp = trait [self : ExpSig<Exp>] ⇒ {num = Add (Lit 4) (Lit 8);var = Let "x" (Lit 4) (Let "y" (Lit 8) (Add (Var "x") (Var "y")));};

To make constructors available from the compositional interface, we add a self-type annotation
to the trait repo. The self type annotation [self : ExpSig<Exp>] imposes a requirementthat the repo should finally be merged with some trait implementing ExpSig<Exp>. Thisrequirement is also statically enforced by the static type checker of CP. This is the second
mechanism in Compositional Programming to modularly inject dependencies.
Nested trait composition. With the language components ready, we can compose themusing the merge operator [14], which in the CP language is denoted as a single comma (,).
First, we show how to compose the old version of the evaluation:
exp = new repo @(Eval Env) , evalNum @Env , evalVar @Top;exp.var.eval { env = empty } --> 12

Since the context has evolved after we add variables, we pass different type arguments tothe two traits to make the final context consistent. The final context type is Env, so wepass Env to evalNum and Top to evalVar. Type arguments are prefixed by @ in CP. A moreinteresting example is to merge the new version of evaluation with free variable bookkeeping:exp’ = new repo @(Eval Env & FV) , evalWithFV @Top , fv;
exp’.var.eval { env = empty } --> 12

After the trait composition, both operations (eval and fv) are available for expressions
that are built with the four constructors (Lit, Add, Let, and Var). Note that here fv
satisfies the dependency of evalWithFV. If no implementation of the type FV is present in thecomposition, there would be a type error, since the requirement for evalWithFV would not
be satisfied. The composition of the three traits is nested because the two methods nested in
the four constructors are composed, as visualized in Figure 5. With nested trait composition,
the Expression Problem is elegantly solved in Compositional Programming. Moreover, weallow context evolution using a relatively simple way with polymorphic contexts.
Impredicative polymorphism. Another feature of CP is that it allows the creation of objects
with polymorphic methods, similar to most OOP languages with generics where classes
can contain polymorphic methods (like Java). However, for this to work properly, CP

1
In Zhang et al.’s original work [46], the new operator must be added before every constructor. However,
our new implementation will implicitly insert new (see Section 2.2 for details).

ECOOP 2022

18:8

Direct Foundations for Compositional Programming

dependency

evalWithFV

+ var

exp'
+ var

+ num

repo
+ num

fv

,

Lit

Add

+ eval+ evalLetVar+ eval+ eval

Lit

,

+ fv

Let

+ fv

Add

+ fv

Var

=

+ fv

Lit

Add

Let

Var

+ eval+ eval+ eval+ eval

+ fv

+ fv

+ fv

+ fv

Figure 5 Visualization of nested composition.

must support impredicative polymorphism (the ability to instantiate type parameters withpolymorphic types) as System F does. For example, consider:
type Poly = { id : forall A. A → A };idTrait = trait implements Poly ⇒ { id = ΛA. \(x:A) → x };(new idTrait).id @Poly-- impredicative

While accepted by our variant of CP and F+
i , such polymorphic instantiations are forbidden+in the original formulation of Fi .

2.2

Elaborating CP to F+i

Under the surface of CP, the foundation for Compositional Programming is the F+i calculus.
We present the key features in F+
and
take
a
closerlookattheconnection
betweenCP andiF+expressions.
Here
we
focus
on
the
elaborationoftraits,
which
are
the
most
importanti
aspect of this paper. We refer curious readers to the work by Zhang et al. [46] for the fullformulation of the type-directed elaboration of CP.
+
Key features of the F+i calculus. Fi is basically a variant of System F [17, 33] extended withintersection types and a merge operator. In the F+i calculus, we denote the merge operator
with a double comma (, ,) (instead of the single comma notation in CP), following the original
notation proposed by Dunfield [14]. The merge operator allows us to introduce terms ofintersection types. For example, 1 , , true is a term of type Int & Bool. Moreover, record
concatenation, which is used to encode multi-field traits, is encoded as merges of records
in F+
i . Thus, multi-field records are represented as merges of multiple single-field records.
However, to ensure determinism of operational semantics, not all terms can be merged witheach other. We impose a disjointness check when typing merges: a merge can only typecheck when the types of the terms being merged are disjoint, ensuring that every part in amerge can be distinguished by its type. For traits, for example, the disjointness restriction
ensures that traits cannot have two fields/methods with the same name m and overlappingtypes, which could otherwise lead to ambiguity when doing method lookup. Here, we show
an example of ambiguity if there is no disjointness check. With intersection types, both
A & B ≤ A and A & B ≤ B are valid. Therefore, a merge 1 , , 2 of type Int & Int can be typed
with Int, but at runtime, two different values of type Int are found. Thus, an expression suchas (1 , , 2) + 1 could evaluate to either 2 or 3. Since we wish for a deterministic semantics, we
use disjointness to prevent such forms of ambiguity. On the other hand, (1 , , true) + 1 typechecks because Int and Bool are disjoint, and it evaluates to 2 unambiguously. A disjointness
constraint can also be added to a type variable in a System F-style polymorphic type, suchas ∀X ∗ Int. X & Int. Moreover, to support unrestricted intersection types like Int & Int, theA. Fan, X. Huang, H. Xu, Y. Sun, and B. C. d. S. Oliveira

18:9

disjointness check is relaxed to consistency for certain terms, so that merges with duplications
like 1 , , 1 are allowed.
Elaborating traits into F+
i . The elaboration of traits is inspired by Cook’s denotationalsemantics of inheritance [12]. To use a concrete example, we revisit the trait repo defined in
Section 2.1. Both the creation and instantiation of traits are included in the definition of
repo:
repo Exp = trait [self : ExpSig<Exp>] ⇒ {num = Add (Lit 4) (Lit 8);var = ...
};The CP code above is elaborated to corresponding F+
i code of the form:
repo = ΛExp. λ(self : ExpSig<Exp>).
let $Lit = self.Lit in let $Add = self.Add in
let $Let = self.Let in let $Var = self.Var in{ num = fix self:Exp. $Add (fix self:Exp. $Lit 4 self)(fix self:Exp. $Lit 8 self) self } ,,{ var = ... };The type parameter Exp in the repo trait is expressed by a System-F-style type lambda(ΛX. e). Note that CP employs a form of syntactic sugar for constructors to allow concise
use of constructors and avoid explicit uses of new. The source code Add (Lit 4) (Lit 8)
is first expanded into new $Add (new $Lit 4) (new $Lit 8), which insert new operators.
Next we describe the elaboration process of creating and instantiating traits:
Creation of traits: A trait is elaborated to a generator function whose parameter isa self-reference (like self above) and whose body is a record of methods;
Instantiation of traits: The new construct is used to instantiate a trait. Uses of new
are elaborated to a fixpoint which applies the elaborated trait function to a self-reference.
In the definition of the field num there are three elaborations of new. For instance, theCP code new $Lit 4 corresponds to the F+
i code fix self:Exp. $Lit 4 self.
It is clear now that our trait encoding is heavily dependent on recursion, due to theself-references employed by the encoding. However, the original F+i [7] does not support
recursion, which reveals a gap between theory and practice.

2.3

The Gap Between Theory and Practice

Our primary motivation to reformulate F+i is to bridge the gap between theory and practice.
The original formulation of F+
lacks
recursion,
impredicative polymorphism and uses theitraditional call-by-value (CBV) evaluation strategy. However, the recent work of CP assumes adifferent variant of F+i that is equipped with fixpoints and the call-by-name (CBN) evaluation.
It is worthwhile to probe into the causes of such differences.
Non-triviality of coherence. Recursion is essential for general-purpose computation inprogramming. More importantly, our encoding of traits requires recursion. For example,
new e is elaborated to fix self. e self. However, adding recursion to the original version+of F+
i turns out to be highly non-trivial. The original Fi is defined using an elaboration
semantics. A fundamental property of F+
i is coherence [35], which states that the semantics
is unambiguous. Coherence is non-trivial due to the presence of the merge operator [14]. To
prove coherence, a logical relation, called canonicity [7], is used to reason about contextual
equivalence in the original work of F+
i . For example, with contextual equivalence, we can

ECOOP 2022

18:10

Direct Foundations for Compositional Programmingshow that the two possible elaborations for the same F+i source expression into Fco arecontextually equivalent:
1 : Int & Int : Int

fst (1, 1)

1 : Int & Int : Int

snd (1, 1)

Two typing derivations lead to two elaborations in this example, which pick different sides ofthe merge. However, both elaborated expressions will be reduced to 1 eventually.
Unfortunately, the proof technique for coherence based on logical relations does not
immediately scale to recursive programs and programs with impredicative polymorphism.
A possible solution, known from the research of logical relations, is to move to a moresophisticated step-indexed form of logical relations [1]. However, this requires a major
reformulation of the proofs and metatheory of the original F+i , and it is not clear whether
additional challenges would be present in such an extension. Thus, the lack of the two
features in the theory of the original F+i remains a serious limitation since only terminating
programs and predicative polymorphism are considered. In other words, we cannot encode
traits as presented in Section 2.2 in the original F+
i . To get around this issue and enable theencoding of traits, Zhang et al. [46] simply assumed an extension of F+
i with recursion andtheir proof of coherence for CP was done under the assumption that the original F+i withrecursion was coherent or deterministic.
Our work rectifies this gap in the theory of Compositional Programming and the CP
language. We reformulate F+i using a direct type-directed operational semantics [22] thatallows recursion and prove that the semantics is deterministic. Thus, our reformulation ofF+
i can serve as a target language to encode traits and validate the proofs of the elaboration+of CP in terms of F+
i with recursion. In addition, our approach gives a semantics to Fi
directly, instead of relying on an indirect elaboration semantics to a System F-like language.
Evaluation strategies. Most mainstream programming languages use CBV, but CBN is amore natural evaluation strategy for object encodings such as Cook’s denotational semantics
of inheritance. As stated by Bruce et al. in their work on object encodings [8]:“Although we shall perform conversion steps in whatever order is convenient for thesake of examples, we could just as well impose a call-by-name reduction strategy. (Mostof the examples would diverge under a call-by-value strategy. This can be repaired at
the cost of some extra lambda abstractions and applications to delay evaluation at
appropriate points.)”
In our elaboration of traits, we adopt a similar approach to object encodings. For example,
consider the following CP expression:
type A = { l1 : Int; l2 : Int };new (trait [self : A] ⇒ { l1 = 1; l2 = self.l1 })which is elaborated to the following (slightly simplified) F+i expression:
fix self : A. {l1 = 1} , , {l2 = self .l1 }The trait expression is elaborated to a function, and the new expression turns the function
into a fixpoint. Unfortunately, this expression terminates under CBN but diverges under
CBV. If evaluated under CBV, the variable self will be evaluated repeatedly, despite theA. Fan, X. Huang, H. Xu, Y. Sun, and B. C. d. S. Oliveira

18:11

fact that only self .l1 is used:
fix self : A. {l1 = 1} , , {l2 = self .l1 },→{l1 = 1} , , {l2 = (fix self : A. {l1 = 1} , , {l2 = self .l1 }).l1 },→{l1 = 1} , , {l2 = ({l1 = 1} , , {l2 = (fix self : A. {l1 = 1} , , {l2 = self .l1 }).l1 }).l1 }

,→

···

We may tackle the problem of non-termination by wrapping self-references in thunks, but
CBN provides a simpler and more natural way. In our CBN formulation of F+
i , {l = e} isalready a value (instead of {l = v}), so we do not need to further evaluate e:
fix self : A. {l1 = 1} , , {l2 = self .l1 },→{l1 = 1} , , {l2 = (fix self : A. {l1 = 1} , , {l2 = self .l1 }).l1 }The l2 field is further evaluated only when a record projection is performed:(fix self : A. {l1 = 1} , , {l2 = self .l1 }).l2,→ ({l1 = 1} , , {l2 = (fix self : A. {l1 = 1} , , {l2 = self .l1 }).l1 }).l2,→ (fix self : A. {l1 = 1} , , {l2 = self .l1 }).l1,→ ({l1 = 1} , , {l2 = (fix self : A. {l1 = 1} , , {l2 = self .l1 }).l1 }).l1,→

1This example illustrates how our new CBN formulation of F+i avoids non-termination of trait
instantiation.

2.4

Technical Challenges and Innovations

The main novelty of our reformulation of F+
i is the use of a type-directed operationalsemantics [20] instead of an elaboration semantics. With a TDOS, adding recursion andimpredicative polymorphism to our proof of determinism is trivial. Our work is an extensionof the λ+i calculus [22] which adapts the TDOS approach. We also follow the subtyping
algorithm design in λ+i . While λ+i supports BCD-style distributive subtyping [4], the additionof disjoint polymorphism does bring some technical challenges. Moreover, there are somesmaller changes to F+
i that enable us to type-check more programs and improve the design+of the original Fi . We will give an overview of the technical challenges and innovations next.
The role of casting. A merge like 1 , , true has multiple meanings under different types (e.g.
Int or Bool). Eventually, we have to extract some components via the elimination of merges,
which is a key issue when designing a direct operational semantics for a calculus with themerge operator. A non-deterministic semantics could allow e1 , , e2 ,→ e1 and e1 , , e2 ,→ e2
without any constraints, at the cost of losing both type preservation and determinism [14].
To obtain a non-ambiguous and type-safe semantics, we follow the TDOS approach [20]:which uses (up)casts to ensure that values have the right form during reduction. In a TDOS,
there is a casting relation, which is used in the reduction rule for annotated values:v ,→A v 0
v : A ,→ v 0

Step-annov

Casting enables us to drop certain parts from a term (e.g., 1 , , true ,→Int 1). Very often,
it is necessary for us to do so to satisfy the disjointness constraint. Consider a function

ECOOP 2022

18:12

Direct Foundations for Compositional Programming

λx : Int. x , , false. For its body to be well-typed, x cannot contain a boolean. Hence, when
the function is applied to 1 , , true, we cannot directly substitute the argument in. Instead, itis wrapped by (and later cast to) Int to resolve the potential conflict.
((λx : Int. x , , false) : Int & Bool → Int & Bool) (1 , , true),→((1 , , true) : Int , , false) : Int & Bool,→ (1 , , false) : Int & Bool,→ 1 , , false
TDOS and function annotations. In casting, values in a merge are selected based ontype information. In the absence of runtime type-checking, we need to know the typeof input value syntactically to match it with the target type. Thus, functions must be
accompanied by type annotations. The previous work λ+i [22] defines the syntax of functions
like λx. e : A → C . While the original argument type A is always kept during reduction,
λ+i ’s casting relation may generate a value that has a proper subtype of the requested type:λx. e : A → C ,→B1 →B2 λx. e : A → B2 . We make casting more precise with a more liberal+
syntax in F+
i . We allow bare abstractions λx : A. e while λi does not. Our casting relation
requires lambdas to be annotated (λx : A. e) : B, but the full annotation B does not have to
be a function type. For example, (λx : Int. x , , true) : (Int → Int) & (Int → Bool) still acts as afunction, and is equivalent to (λx : Int. x , , true) : Int → Int & Bool.
Algorithmic subtyping with disjoint polymorphism. F+
i extends BCD-style distributive
subtyping [4] to disjoint polymorphism. ∀X ∗ Int. X & Int represents the intersection ofsome type X and Int assuming X is disjoint to Int. Like arrows or records, such universal
types distribute over intersections. Hence, (∀X ∗ Int. X ) & (∀X ∗ Int. Int) is a subtype of∀X ∗ Int. X & Int. A well-known challenge in supporting distributivity in the BCD-style
subtyping is to obtain an algorithmic formulation of subtyping. There have been many efforts
to eliminate the explicit transitivity rule to obtain an algorithmic formulation [26, 31, 39].
Compared with the original F+i [7], we employ a different subtyping algorithm design, using
splittable types [21]. This approach employs a type-splitting operation (B C A B C ) thatconverts a given type A to an equivalent intersection type B & C , for example, A → B1 & B2
is split to A → B1 and A → B2 . The subtyping algorithm uses type splitting whenever anintersection type is expected in the conventional algorithm for subtyping without distributivity,
and therefore handles distributivity smoothly and modularly. For space reasons, the novel
algorithmic subtyping approach is discussed in the extended version of the paper.
Enhanced subtyping and disjointness with more top-like types. Unlike previous systems
with disjoint polymorphism [2, 7], we add a context in subtyping judgments to track the
disjointness assumption X ∗ A whenever we open a universal type ∀X ∗ A. B, similar to thesubtyping with F-bounded quantification. The extra information enhances our subtyping:
we know a type must be a supertype of Top, if it is disjoint with Bot. This also fixes thefollowing broken property in the original F+i , as we now have more types that are top-like.
I Definition 2.1 (Disjointness specification). If A is disjoint with B, any common supertypes
they have must be equivalent to Top.
Keeping this property is necessary for us to obtain a deterministic operational semantics.
Meanwhile, we prove our subtyping and disjointness relations are decidable in Coq. Notethat in the original F+i , the decidability of the two relations was proved manually, although
the rest of the proof was mechanized.

A. Fan, X. Huang, H. Xu, Y. Sun, and B. C. d. S. Oliveira

18:13

The F+i Calculus and Its Operational Semantics

3This section introduces the F+i calculus, including its static and dynamic semantics.

3.1

SyntaxThe syntax of F+
i is as follows:
Types

A, B, C ::= X | Int | Top | Bot | A & B | A → B | ∀X ∗ A. B | {l : A}

Checkable terms

p ::= λx : A. e | ΛX . e | {l = e}Expressions

e ::= p | x | i | > | e : A | e1 , , e2 | fix x : A. e | e1 e2 | e A | e.l

Valuesv ::= p | p : A | i | > | v1 , , v2

Term contexts

Γ ::= · | Γ, x : A

Type contexts∆ ::= · | ∆, X ∗ A

Types. Types include the Top type and the uninhabited type Bot. Intersection types are
created with A & B. Disjoint polymorphism, a key feature of F+i , is based on universal types
with a disjointness quantifier ∀X ∗ A. B, expressing that the type variable X is bound inside
B and disjoint to type A. {l : A} denotes single-field record types, where l is the record label.
Multi-field record types are desugared to intersections of single-field ones [36]:{l1 : A1 ; . . . ; ln : An } , {l1 : A1 } & · · · & {ln : An }Expressions. As we will explain later with the typing rules, some expressions do not havean inferred type (or principal type), including lambda abstractions, type abstractions, andsingle-field records. We use metavariable p to represent these expressions, which with optionalannotations, are values. Also, note that expressions inside record values do not have to
be a value since our calculus employs call-by-name. The merge operator , , composes two
expressions to make a term of an intersection type. The top value > can be viewed as amerge of zero elements. Fixpoint expressions fix x : A. e construct recursive programs. The
type annotation A denotes the type of x as well as the whole expression. Like record types,
multi-field records are desugared to merges of single-field ones:{l1 = e1 ; . . . ; ln = en } , {l1 = e1 } , , . . . , , {ln = en }Contexts. We have two contexts: Γ tracks the types of term variables; ∆ tracks the
disjointness information of type variables, which follows the original design of F+
i . We use∆ ` A, ` ∆, and ∆ ` Γ judgments for the type well-formedness and the context wellformedness (defined in the extended version of the paper). For multiple type well-formedness
judgments, we combine them into one, i.e., ∆ ` A, B means ∆ ` A and ∆ ` B.

3.2

Subtyping

Figure 6 shows our subtyping relation, which extends BCD-style subtyping [4] with disjoint
polymorphism, records, and the bottom type. Compared with the original F+
i , we add acontext to track type variables and their disjointness information. The context not only
ensures the well-formedness of types, but is also important to our new rule DS-topVar.
An equivalence relation (Definition 3.1) is defined on types that are subtype of each other.
These equivalent types can be converted back and forth without loss of information.

ECOOP 2022

18:14

Direct Foundations for Compositional Programming∆ ` A <: B

(Declarative Subtyping)DS-trans∆ ` A <: B

DS-refl`∆∆`A∆ ` A <: A∆ ` B <: C

∆ ` A <: CDS-and∆ ` A <: B

∆ ` A <: C

∆ ` A <: B & C
DS-arrow∆ ` A2 <: A1

DS-top`∆∆`A

DS-bot`∆∆`A∆ ` A <: Top∆ ` Bot <: A

DS-andl`∆∆ ` A, B

DS-andr`∆∆ ` A, B∆ ` A & B <: A

∆ ` A & B <: B

DS-distArrow`∆∆ ` B1 <: B2∆ ` A1 → B1 <: A2 → B2

∆ ` A, B, C

∆ ` (A → B) & (A → C ) <: A → B & C

DS-topArrow`∆

DS-rcd∆ ` A <: B

DS-distRcd`∆∆ ` Top <: Top → Top∆ ` {l : A} <: {l : B}

∆ ` {l : A} & {l : B} <: {l : A & B}

DS-topRcd`∆

DS-all∆ ` A2 <: A1∆ ` Top <: {l : Top}DS-distAll`∆∆`A∆, X ∗ A2 ` B1 <: B2∆ ` ∀X ∗ A1 . B1 <: ∀X ∗ A2 . B2∆, X ∗ A ` B1 , B2

∆ ` (∀X ∗ A. B1 ) & (∀X ∗ A. B2 ) <: ∀X ∗ A. (B1 & B2 )∆ ` A, B

DS-topAll`∆∆ ` Top <: ∀X ∗ Top. Top

DS-topVar
X ∗A∈∆∆ ` A <: Bot∆ ` Top <: X

Figure 6 Declarative subtyping rules.

I Definition 3.1 (Type equivalence). ∆ ` A ∼ B , ∆ ` A <: B and ∆ ` B <: A.
For functions (rule DS-arrow) and disjoint quantifications (rule DS-all), subtyping
is covariant in positive positions and contravariant in negative positions. The intuition isthat type abstractions of the more specific type (subtype) should have a looser disjointness
constraint for the parameter type. ∀X ∗ Top. A denotes that there is no constraint on X , since
Top is disjoint to all types. On the contrary, Bot is the strictest constraint. It is useful in types
like ∀X ∗ {l : Bot}. A which expresses that X does not contain any informative field of labell [44]. For intersection types, rules DS-andl, DS-andr, and DS-and axiomatize that A & B
is the greatest lower bound of A and B. As a typical characteristic of BCD-style subtyping,type constructors distribute over intersections, including arrows (rule DS-distArrow),records (rule DS-distRcd) and disjoint quantifications (rule DS-distAll).
Another feature of BCD subtyping, which is often overlooked, is the generalization of
top-like types, i.e. supertypes of Top.
I Definition 3.2 (Specification of top-like types). ∆ `eAd , ∆ ` A ∼ Top.
Initially, top-like types include Top and intersections like Top & Top. But the BCD
subtyping adds Top → Top to it via rule DS-topArrow, as well as A → Top for any type
A due to the contravariance of function parameters. Rule DS-topArrow can be viewed
as a special case of rule DS-distArrow where intersections are replaced by Top (one canconsider it as an intersection of zero components). Like the original F+
i , we extend this idea
to universal types and record types (rules DS-topAll and DS-topRcd).

A. Fan, X. Huang, H. Xu, Y. Sun, and B. C. d. S. Oliveira

18:15

The most important change is the rule DS-topVar. This rule means that a type variable
is top-like if it is disjoint with the bottom type. Every type B is a common supertype of B
itself and Bot. If B is disjoint with Bot, then it must be top-like. We proved that subtyping
is decidable via an equivalent algorithmic formulation.
The discussion about algorithmic subtyping is in the extended version of the paper.
I Lemma 3.3 (Decidability of subtyping). ∆ ` A <: B is decidable.
Disjointness. The notion of disjointness (Definition 2.1), defined via subtyping, is used in
the original F+i , as well as calculi with disjoint intersection types [30]. We proved that ouralgorithmic definition of disjointness (written as ∆ ` A ∗ B, in the extended version of thepaper) is sound to a specification in terms of top-like types.
I Lemma 3.4 (Disjointness soundness). If ∆ ` A ∗ B then for all type C that ∆ ` A <: Cand ∆ ` B <: C we have ∆ `eC d.
Informally, two disjoint types do not have common supertypes, except for top-like types.
This definition is motivated by the desire to prevent ambiguous upcasts on merges. That is,
we wish to avoid casts that can extract different values of the same type from a merge. Thus
in F+
i and other calculi with disjoint intersection types, we only allow merges of expressions
whose only common supertypes are types that are (equivalent to) the top type. For instance,
consider the merge (1 , , true) , , (2 , , ‘c’). The first component of the merge (1 , , true) has
type Int & Bool, while the second component (2 , , ‘c’) has type Int & Char. This merge isproblematic because Int is a supertype of the type of the merge (Int & Bool) & (Int & Char),allowing us to extract two different integers by casting the two terms to Int. Fortunately, ourdisjointness restriction rejects such merges since the supertype Int is not top-like.

3.3

Bidirectional Typing

The type system of F+
i is bidirectional [15], where the subsumption rule is triggered by type
annotations. Calculi with a merge operator are incompatible with a general subsumption rulebecause it cancels disjointness checking. For example, with a general subsumption rule, we
can directly use 1 , , true as a term of type Int since Int & Bool <: Int. Then, merging 1 , , true
with the term false would type-check since disjointness simply checks whether the static typesof merging terms are disjoint, and Int is disjoint with Bool. But now, the merge contains twobooleans, which would lead to ambiguity if later we wish to extract a boolean value from themerge. The key issue is that a general subsumption rule loses static type information that isnecessary to reject ambiguous merges. A bidirectional type system solves this problem byhaving a more restricted form of subsumption that only works in the checking mode where
the type is provided. A more detailed description of the problem for calculi with the merge
operator can be found in Huang et al.’s work [22]. We should also remark that this issue
of incompatibility with a general subsumption rule is not unique to calculi with a merge
operator. It shows up, for instance, in calculi with gradual typing [41] and calculi with record
concatenation and subtyping [9].
Typing. As presented in Figure 7, there are two modes of typing: synthesis (⇒) and checking(⇐). We use ⇔ as a metavariable for typing modes. ∆; Γ ` e ⇔ A indicates that under typecontext ∆ and term context Γ, the expression e has type A in mode ⇔. A bidirectional typesystem directly provides a type-checking algorithm. ∆, Γ, e are all inputs in both modes.
Type synthesis generates a unique type as the output (also called the inferred type), while
type checking takes a type as an input and examines the term.

ECOOP 2022

18:16

Direct Foundations for Compositional Programming

Typing modes⇔ ::= ⇐ | ⇒Pre-values

u ::= i | > | e : A | u1 , , u2∆; Γ ` e ⇔ A(Bidirectional Typing)

Typ-top`∆∆`Γ

Typ-lit`∆∆`Γ∆; Γ ` > ⇒ Top∆; Γ ` i ⇒ Int

Typ-var
`∆
∆`Γ

x:A∈Γ

∆; Γ ` x ⇒ A

Typ-abs∆ ` B1 <: A∆; Γ, x : A ` e ⇐ B2

Typ-tabs∆; Γ ` λx : A. e ⇐ B1 → B2∆; Γ ` ΛX . e ⇐ ∀X ∗ A. B∆`Γ∆, X ∗ A; Γ ` e ⇐ B

Typ-rcd∆; Γ ` e ⇐ A∆; Γ ` {l = e} ⇐ {l : A}∆; Γ ` e1 ⇒ A
ABB →C∆; Γ ` e2 ⇐ B∆; Γ ` e ⇒ B
B B ∀X ∗ C1 . C2
∆ ` A ∗ C1

Typ-proj∆; Γ ` e ⇒ A
A B {l : C }∆; Γ ` e1 e2 ⇒ C∆; Γ ` e A ⇒ C2 [X 7→ A]∆; Γ ` e.l ⇒ C

Typ-tapp

Typ-app

Typ-merge∆`A∗B∆; Γ ` e1 ⇒ A∆; Γ ` e2 ⇒ B

Typ-mergev`∆∆`Γ
u1 ≈ u2·; · ` u1 ⇒ A·; · ` u2 ⇒ B

Typ-inter∆; Γ ` e ⇐ A∆; Γ ` e ⇐ B∆; Γ ` e1 , , e2 ⇒ A & B∆; Γ ` u1 , , u2 ⇒ A & B∆; Γ ` e ⇐ A & B

Typ-fix∆; Γ, x : A ` e ⇐ A

Typ-anno∆; Γ ` e ⇐ A∆; Γ ` fix x : A. e ⇒ A∆; Γ ` (e : A) ⇒ A

Typ-sub∆; Γ ` e ⇒ A∆ ` A <: B∆; Γ ` e ⇐ B

Figure 7 Bidirectional typing rules for F+i .

I Lemma 3.5 (Uniqueness of type synthesis). If ∆; Γ ` e ⇒ A1 and ∆; Γ ` e ⇒ A2 thenA1 = A2 .
Conversion of typing modes happens in rule Typ-sub. With it, a term with inferred type
A can be checked against any B that is a supertype of A. Compared to the original F+i ,fixpoints are new. They model recursion with a self-reference (x in fix x : A. e). Other thanthis, rule Typ-fix is almost the same as rule Typ-anno. It checks the expression e by the
annotated type A, with assumption that x has type A in e.
Checking abstractions, type abstractions, and records. To check a function λx : A. e against
B1 → B2 by rule Typ-abs, we track the type of the term variable as the precise parameter
type A, and check if e can be checked against B2 . B1 must be a subtype of A to guarantee
the safety of the function application. The type-checking of type abstractions ΛX . e works bytracking the disjointness relation of the type variable with the context and checking e against
the quantified type B. Typing of records works similarly. Additionally, there is a rule Typinter, which checks an expression against an intersection type by seperately checking theexpression against the composing two types. With this design, we allow λx : Int. x , , true tobe checked against (Int → Int) & (Int → Bool).
Application, record projection, and conversion of applicable types. It is not surprisingA. Fan, X. Huang, H. Xu, Y. Sun, and B. C. d. S. Oliveira

ABB

18:17

(Applicative Distribution)
AD-andArrow
A1 B B1 → C1

A2 B B2 → C2

A1 & A2 B B1 & B2 → C1 & C2
AD-andAll
A1 B ∀X ∗ B1 . C1A2 B ∀X ∗ B2 . C2

A1 & A2 B ∀X ∗ B1 & B2 . (C1 & C2 )AD-andRcd
A1 B {l : B1 }A2 B {l : B2 }A1 & A2 B {l : B1 & B2 }AD-refl
ABA

Figure 8 Applicative distribution rules.

that a merge can act as a function. But in the original F+i , this requires annotations since
the expression being applied in an application must have an inferred arrow type. Our
design, following the λ+i calculus [22], allows a term of an intersection type to directly apply,
as long as the intersection type can be converted into an applicable form. For example,(Int → Int) & (Int → Bool) is converted into (Int & Int) → (Int & Bool), which is a supertypeof the former. When inferring the type of the application e1 e2 , rule Typ-app first converts
the inferred type of e1 into an arrow form B → C and then checks the argument e2 against
B. If the check succeeds, the whole expression has inferred type C .
In F+
i , we have three applicable forms: arrow types, record types, universal types. Like
rule Typ-app, the typing of type application and record projection also allows the applied
term to have an intersection type, and relies on applicative distribution to convert the type.
Applicative distribution A B B (defined in Figure 8) takes type A and generates a
supertype B that has an applicable form. The first three rules bring all parts of the
input intersection type together. For example, assuming that we apply several mergedfunctions whose types are A1 → B1 , A2 → B2 , ..., An → Bn , the combined function typeis (A1 & ... & An ) → (B1 & ... & Bn ). It is equivalent to the input type only when A1 , A2 ,..., and An are all equivalent. Essentially, applicative distribution (A B B) is a subset ofsubtyping (A <: B). The supertype is selected to ensure that when a merge is applied toan argument, every component in the merge is satisfied. Although each one of the three
first rules overlaps with the reflexivity rule, for any given type, at most one result has anapplicable form.
Since merges are treated as a whole applicable term, programmers can extend functions
via a compositional approach without modifying the original implementation. It also enables
the modular extension of type abstractions and especially records, which play a core role in
the trait encoding used in Compositional Programming.
Davies and Pfenning also employ a similar design in their bidirectional type system
for refinement intersections [13]. Their type conversion procedure respects subtyping as
well. Instead of combining function types, it makes use of A & B <: A and A & B <: B to
enumerate components in intersections and uncover arrows.
Typing merges with disjointness and consistency. Well-typed merges always have inferred
types. There are two type synthesis rules for merges, both combining the inferred types of
the two parts into an intersection. Typ-merge requires the two subterms to have disjoint
inferred types, like 1 , , true. Typ-mergev relaxes the disjointness constraint to consistency
checking (written as u1 ≈ u2 ) to accept overlapping terms like 1 , , 1. Such duplicationis meaningless to users but may appear during evaluation. In fact, rule Typ-mergev isdesigned for metatheory properties, and not to allow more user-written programs [22]. We

ECOOP 2022

18:18

Direct Foundations for Compositional ProgrammingArguments

arg ::= e | A | {l}Evaluation contexts

E ::= [ ] e | [ ] A | [ ] .l | [ ] , , v | v , , [ ] | [ ] : Av • arg ,→ u(Parallel Application)

PApp-absB B C1 → C2

PApp-tabse2A

A B ∀X ∗ B1 . B2u

(λx : A. e1 ) : B • e2 ,→ (e1 [x 7→ u]) : C2
PApp-proj
A B {l : B}

(ΛX . e) : A • C ,→ (e[X 7→ C ]) : (B2 [X 7→ C ])PApp-merge
v1 • arg ,→ u1{l = e} : A • {l} ,→ e : B

v2 • arg ,→ u2

v1 , , v2 • arg ,→ u1 , , u2

e1 ,→ e2

(Small-Step Semantics)

Step-pappv • e ,→ u

Step-pprojv • {l} ,→ u

Step-ptappv • A ,→ uv e ,→ uv.l ,→ uv A ,→ uv ,→A v 0

Step-merge
e1 ,→ e10
e2 ,→ e20

Step-cntx
e ,→ e 0

e1 , , e2 ,→ e10 , , e20

E[e] ,→ E[e 0 ]Step-annov
pre-value v

v : A ,→ v 0

Step-fix
fix x : A. e ,→ e[x 7→ fix x : A. e] : A

Figure 9 Small-step semantics rules.

will state the formal specification of consistency in Section 4.1 and show how it is involvedin the proofs of determinism and type soundness. Informally, consistent merges cause noambiguity in the runtime. For practical reasons, we only consider pre-values (defined at the
top of Figure 7) in consistency checking, for which the inferred type can be told directly.
The algorithms for disjointness and consistency are presented in the extended version of thepaper. In general, disjointness and consistency avoid introducing ambiguity of merges, andenable a deterministic semantics for F+
i .

3.4

Small-Step Operational Semantics

We specify the call-by-name reduction of F+i using a small-step operational semantics inFigure 9. Step-papp, Step-pproj, and Step-ptapp are reduction rules for application andrecord projection. They trigger parallel application (defined in the middle of Figure 9) of
merged values to the argument. Rule Step-fix substitutes the fixpoint term variable withthe fixpoint expression itself. Note that the result is annotated with A. With the explicit
type annotation, the result of reduction preserves the type of the original fixpoint expression.
Through rule Step-annov, values are cast to their annotated type. Such values must also
be pre-values. This is to filter out checkable terms p including bare abstractions or records
without annotations, as p : A is a form of value itself and thus should not step.
A merge of multiple terms may reduce in parallel, as shown in rule Step-merge. Only
when one side cannot step, the other side steps alone, as suggested by the evaluation context
E , , v and v , , E. Rule Step-cntx is the reduction rule of expressions within an evaluation
context. Since the rule can be applied repeatedly, we only need evaluation contexts of depth
one (shown at the top of Figure 9). Our operational semantics substitutes arguments wrapped

A. Fan, X. Huang, H. Xu, Y. Sun, and B. C. d. S. Oliveira

18:19

by type annotations into function bodies, while it forbids the reduction of records sincerecords are values.
Parallel application. Parallel application is at the heart of what we call nested compositionin CP. It provides the runtime behavior that is necessary to implement nested composition,and it reflects the subtyping distributivity rules at the term level. A merge of functions istreated as one function. The beta reduction of all functions in a merge happens in parallel
to keep the consistency of merged terms. For type abstractions or records, things are similar.
The parallel application handles these applicable merges uniformly via rule PApp-merge.
To align record projection with the other two kinds of application, we define arguments which
abstract expressions, types, and record labels (at the top of Figure 9). In rule PApp-abs,
the argument expression is wrapped by the function argument type before we substituteit into the function body. Parallel application of type abstractions substitutes the typeargument into the body and annotates the body with the substituted disjoint quantified type.
Rule PApp-proj projects record fields. Note these three rules have types to annotate theresult, since in Typ-abs, Typ-tabs, and Typ-rcd we only type the expression e inside inchecking mode. With an explicit type annotation, the application preserves types.
Splittable types. Before explaining wrapping or casting, we first introduce splittable types [22],which are a key component of our algorithmic formulations of various relations. Ordinary
types are the basic units, values of ordinary types can be constructed without the merge
operator. As defined at the top of Figure 10, ordinary types do not have intersection types inpositive positions. By contrast, splittable types are isomorphic to appropriate intersections.
Recall that in BCD-style distributive rules, arrows distribute over intersection, making
Int → Int & Bool equivalent to the intersection (Int → Int) & (Int → Bool). Therefore we saythat the former type splits into the latter two arrow types. In Figure 10, we extend the typesplitting algorithm of λ+i to universal types in correspondence to the distributive subtyping
rules (rule DS-distArrow, rule DS-distRcd, and rule DS-distAll). It gives a decision
procedure to check whether a type is splittable or ordinary.
I Lemma 3.6 (Type splitting loses no information). B C A B C only if · ` A ∼ B & C .
Expression wrapping. Rules for expression wrapping (e A u) are listed in the middle of
Figure 10. Basically, it splits the type A when possible, annotates a duplication of e by eachordinary part of A, and then composes all of them. The only exception is that it never uses
top-like types to annotate terms, to avoid ill-typed results like {l = 1} : Int → Top, but rather
generates a normal value whose inferred type is that top-like type, like (λx : Int. >) : Int → Top(via the top-like value generating function [[A◦ ]], defined in the extended version of the paper).
Casting. Casting (shown in Figure 10) is the core of the TDOS, and is triggered by the
Step-annov rule. Recalling that only values that are also pre-values will be cast, we canalways tell the inferred type of the input value and cast it by any supertype of that inferred
type. The definition of casting uses the notion of splittable types. In rule Cast-and, thevalue is cast under two parts of a splittable type separately, and the results are put together
by the merge operator. The following example shows that a merge retains its form whencast under equivalent types.
((λx : Int. x) : Int → Int) , , ((λx : Int. true) : Int → Bool),→(Int→Int) & (Int→Bool)((λx : Int. x) : Int → Int) , , ((λx : Int. true) : Int → Bool),→Int→Int & Bool((λx : Int. x) : Int → Int) , , ((λx : Int. true) : Int → Bool)In the latter case, the requested type is a function type, but the result has an intersection
type. This change of type causes a major challenge for type preservation.

ECOOP 2022

18:20

Direct Foundations for Compositional Programming

Ordinary types

A◦ , B ◦ , C ◦ ::= X | Int | Top | Bot | A → B ◦ | ∀X ∗ A. B ◦ | {l : A◦ }BCABC

(Splittable Types)
Sp-arrow
C1 C B B C2

Sp-rcdC1 C B B C2

A → C1 C A → B B A → C2

{l : C1 } C {l : B} B {l : C2 }Sp-allSp-andC1 C B B C2
∀X ∗ A. C1 C ∀X ∗ A. B B ∀X ∗ A. C2e

A C A&B B BuA(Expression Wrapping)
EW-anno· ` ¬eB ◦ d

EW-top· `eA◦ deA◦◦[[A ]]

e

B◦

e :B

EW-andB1 C A B B2

e

◦

e

A

B1

u1

e

B2

u2

u1 , , u2

v1 ,→A v2(Casting)

Cast-int

Cast-top· `eA◦ d

Cast-mergel
v1 ,→A◦ v 0

Cast-merger
v2 ,→A◦ v 0

i ,→Int iv ,→A◦ [[A◦ ]]v1 , , v2 ,→A◦ v 0

v1 , , v2 ,→A◦ v 0

Cast-anno· ` ¬eB ◦ d· ` A <: B ◦e : A ,→B ◦ e : B ◦Cast-andB1 C A B B2

v ,→B1 v1v ,→B2 v2v ,→A v1 , , v2

Figure 10 Type splitting, expression wrapping and value casting rules.

For ordinary types, rule Cast-int casts an integer to itself under type Int. Under any
ordinary top-like type, the cast result is the output of the top-like value generator. The
casting of values with annotations works by changing the type annotation to the casting (nottop-like) supertype. Rule Cast-mergel and rule Cast-merger make a selection between
two merged values. The two rules overlap, but for a well-typed value, the casting result is
unique.
Example. We show an example to illustrate the behavior of our semantics:
Let f := λx : Int & Top. x , , false in((f : (Int & Top → Int) & (Int & Top → Bool)) : Int & Bool → Int & Bool) (1 , , true),→∗{by rules Step-annov, Cast-and, and Cast-anno}(f : Int & Bool → Int) , , (f : Int & Bool → Bool) (1 , , true),→∗{by rules Step-papp, EW-and, EW-anno, and EW-top}(((1 , , true) : Int , , >) , , false) : Int , , (((1 , , true) : Int , , >) , , false) : Bool,→∗{by rules Step-merge, Step-annov, Cast-int, Cast-mergel, and Cast-merger}
1 , , false

This example shows that a function with a splittable type will be cast to a merge of two
copies of itself with different type annotations, i.e., two split results. The application of a

A. Fan, X. Huang, H. Xu, Y. Sun, and B. C. d. S. Oliveira

18:21

merge of functions works by distributing the argument to both functions. Finally, casting
selects one side of the merge under the annotated type. From this example, we can see thatwithout the precise parameter annotation of a lambda function (here Int & Top), there is no
way to filter the argument 1 , , true, causing a conflict.

4

Type Soundness and Determinism

In this section, we show that the operational semantics of F+
i is type-sound and deterministic.
+
In Fi , determinism also plays a key role in the proof of type soundness. Proving progress isstraightforward and is discussed in the extended version of the paper.

4.1

Determinism

A common problem with determinism for calculi with a merge operator is the ambiguityof selection between merged values. In our system, ambiguity is removed by employing
disjointness and consistency constraints on merges via typing.
I Definition 4.1 (Consistency specification). v1 ≈spec v2 , For all type A that v1 ,→A v10
and v2 ,→A v20 then v10 = v20 .
Two values in a merge have no conflicts as long as casting both values under any typeleads to the same result. This specification allows v1 and v2 to contain identical expressions(may differ in annotations), and terms with disjoint types as such terms can only be castunder top-like types, and the cast result is only decided by that top-like type.
I Lemma 4.2 (Top-like casting is term irrelevant). If · `eAd and v1 ,→A v10 and v2 ,→A v20
then v10 = v20 .
This is because casting only happens when the given type is a supertype of the cast value’stype, and disjoint types only share top-like types as common supertypes (Lemma 3.4).
I Lemma 4.3 (Upcast only). If ·; · ` v ⇒ B and v ,→A v 0 then · ` B <: A.
With consistency, casting all well-typed values leads to a unique result. The remaining reduction rules, including expression wrapping and parallel application, are trivially deterministic.
I Lemma 4.4 (Determinism of casting). If ·; · ` v ⇒ B and v ,→A v1 and v ,→A v2 , thenv1 = v2 .
I Theorem 4.5 (Determinism of reduction). If ·; · ` e ⇒ A and e ,→ e1 and e ,→ e2 thene1 = e2 .

4.2

Preservation

Retaining preservation is challenging. When typing merges, we need to satisfy the extra side
conditions in rules Typ-merge and Typ-mergev: disjointness and consistency. While theformer only depends on types, the latter needs special care.
Consistency. As discussed in Section 3.4, casting may duplicate terms. For example,
1 ,→Int & Int 1 , , 1 by rule Cast-and. Rule Typ-mergev is a relaxation of rule Typ-merge
to type such merges. We have to ensure any two merged casting results are consistent:
I Lemma 4.6 (Value consistency after casting). If ·; · ` v ⇒ C and v ,→A v1 and v ,→B v2
then v1 ≈ v2 .

ECOOP 2022

18:22

Direct Foundations for Compositional Programming

A.B(Isomorphic Subtyping)
IS-reflA.A

IS-andB1 C B B B2

A1 . B1

A2 . B2

A1 & A2 . B

Figure 11 Isomorphic subtyping.

Then we need to make sure that consistency is preserved during reduction.
I Lemma 4.7 (Reduction keeps consistency). If ·; · ` u1 ⇒ A and ·; · ` u2 ⇒ B and u1 ≈ u2
then
if u1 is a value and u2 ,→ u20 then u1 ≈ u20 ;if u2 is a value and u1 ,→ u10 then u10 ≈ u2 ;if u1 ,→ u10 and u2 ,→ u20 then u10 ≈ u20 .
Besides, when parallel application substitutes arguments into merges of applicable terms
or projects the wished field, consistency is preserved as well. This requirement enforces us todefine consistency not only on values but also on pre-values since the application transforms
a value merge into a pre-value merge.
I Lemma 4.8 (Parallel application keeps consistency). If ·; · ` v1 ⇒ A and ·; · ` v2 ⇒ B andv1 ≈ v2 and v1 • arg ,→ u1 and v2 • arg ,→ u2 then u1 ≈ u2 whenarg is a well-typed expression;or arg is a label;or arg is a type C ; we know A B ∀X ∗ A1 . A2 and B B ∀X ∗ B1 . B2 ; and · ` C ∗ A1 & B1 .
Our algorithmic formulation of consistency (u1 ≈ u2 , presented in the extended version of
the paper) keeps the above properties and is sound to the specification (Definition 4.1). The
basic idea is to tear all merges apart and compare every component from u1 and u2 . They
are either the same expression with different annotations or have disjoint types.
I Lemma 4.9 (Consistency soundness). If v1 ≈ v2 then v1 ≈spec v2 .
Isomorphic subtyping. In F+
i , types are not always precisely preserved by all reduction steps.
Specifically, when we cast a value v ,→A v 0 (in rule Step-annov) or wrap a term e A u(in rule PApp-abs), the context expects v 0 or u to have type A, but this is not always true.
In our casting rules shown at the bottom of Figure 10, most values will be reduced to resultswith the exact type that we want, except for rule Cast-and. The inferred type of the result
is always an intersection, which may differ from the original splittable type. To describe
the change of types during reduction accurately, we define isomorphic subtyping (Figure 11).
If A . B, we say A is an isomorphic subtype of B. The following lemma shows that while
the two types in an isomorphic subtyping relation may be syntactically different, they areequivalent under an empty type context (i.e. · ` A <: B and · ` B <: A).
I Theorem 4.10 (Isomorphic subtypes are equivalent). If A . B then · ` A ∼ B.
With isomorphic subtyping, we define the preservation property of casting, expression
wrapping, and parallel application as follows.
I Lemma 4.11 (Casting preserves typing). If ·; · ` v ⇒ A and v ,→B v 0 then there exists a
type C such that ·; · ` v 0 ⇒ C and C . B.

A. Fan, X. Huang, H. Xu, Y. Sun, and B. C. d. S. Oliveira

18:23

I Lemma 4.12 (Expression wrapping preserves typing). If ·; · ` e ⇐ B and · ` B <: A ande A u then there exists a type C such that ·; · ` u ⇒ C and C . A.
I Lemma 4.13 (Parallel application preserves typing). If ·; · ` v • arg ⇒ A and v • arg ,→ uthen there exists a type B such that ·; · ` u ⇒ B and B . A.
Of course, we can prove that the result of casting always has a subtype (or an equivalenttype) of the requested type instead of an isomorphic subtype. But it would be insufficientfor type preservation of reduction. In summary, if casting or wrapping generates a term oftype B when the requested type is A, we need B to satisfy:
B is a subtype of A because we want a preservation theorem that respects subtyping.
For any type C , A ∗ C implies B ∗ C . This is for the disjointness and consistency checking.
If A converts into an applicable type C , then B converts into an applicable type too.
Finally, with the lemmas above and isomorphic subtyping, we have the type preservation∗
property of F+
i . That is, after one or multiple steps of reduction (,→ ), the inferred type ofthe reduced expression is an isomorphic subtype. Therefore, for checked expressions, theinitial type-checking always succeeds.
I Theorem 4.14 (Type preservation with isomorphic subtyping). If ·; · ` e ⇔ A and e ,→∗ e 0then there exists a type B such that ·; · ` e 0 ⇔ B and B . A.
I Corollary 4.15 (Type preservation). If ·; · ` e ⇔ A and e ,→∗ e 0 then ·; · ` e 0 ⇐ A.

5

Related WorkIn the following discussion, sometimes we attach the publication year to its calculus name for+easy distinction. For instance, F+i ’19 means the original formulation of Fi by Bi et al. [7].
The merge operator, disjoint intersection types and TDOS. The merge operator for calculi
with intersection types was proposed by Reynolds [34]. His original formulation came withsignificant restrictions to ensure that the semantics is not ambiguous. Castagna [11] showedthat a merge operator restricted to functions could model overloading. Dunfield [14] proposeda calculus, which we refer to as λ,, , with an unrestricted merge operator. While powerful,
λ,, lacked both determinism and subject reduction, though type safety was proved via a
type-directed elaboration semantics.
To address the ambiguity problems in Dunfield’s calculus, Oliveira et al. [30] proposed
λi ’16, which only allows intersections of disjoint types. With that restriction and the useof an elaboration semantics, it was then possible to prove the coherence of λi ’16, showingthat the semantics was not ambiguous. Bi et al. [6] relaxed the disjointness restriction,requiring it only on merges, in a new calculus called λ+i ’18 (or NeColus). This enabled
the use of unrestricted intersections in λ+i ’18. In addition, they added a more powerfulsubtyping relation based on the well-known BCD subtyping [4] relation. The new subtyping
relation, in turn, enabled nested composition, which is a fundamental feature of Compositional
Programming. Unfortunately, both unrestricted intersections and BCD subtyping greatly
complicated the coherence proof of λ+i ’18. To address those issues, Bi et al. turned to an
approach based on logical relations and a notion of contextual equivalence.
To address the increasing complexities arising from the elaboration semantics and thecoherence proofs, Huang et al. [20, 22] proposed a new approach to model the type-directedsemantics of calculi with a merge operator. The type-directed elaboration in λi ’16 andλ+i ’18 is replaced by a direct type-directed operational semantics (TDOS). In the new TDOSECOOP 2022

18:24

Direct Foundations for Compositional Programming

Disjointness
Unrestricted Intersections
Determinism / Coherence
Recursion
Direct Semantics
Subject Reduction
Distributive Subtyping
Disjoint Polymorphism
Evaluation Strategy

λ,,λi ’16

Fi

λ+i ’18

F+
i ’19

λi

λ+i

F+
i

No

Coh.

Coh.

Coh.

Coh.

Det.

Det.

Det.

-

-

-

-

CBV

CBV

CBV

CBV

CBV

CBV

CBN

CBV

Figure 12 Summary of intersection calculi with the merge operator.
( = yes, = no, - = not applicable )formulations of λi and λ+i , coercive subtyping is removed since subtyping no longer needs togenerate explicit coercion for the elaboration to a target calculus. Instead, runtime implicit(up)casting is used. This is implemented by the casting relation, which was originally called
typed reduction. Our work adopts TDOS and adds disjoint polymorphism. Disjoint polymorphism is used in Compositional Programming to enable techniques such as polymorphic
contexts. We also change the evaluation strategy from call-by-value (CBV) to call-by-name(CBN), motivated by the elaboration of trait instantiation in Compositional Programming.
Otherwise, with a CBV semantics, many uses of trait instantiation would diverge.
Calculi with disjoint polymorphism. Disjoint polymorphism was originally introduced ina calculus called Fi by Alpuim et al. [2]. A disjointness constraint is added to universal
quantification in order to allow merging components whose type contains type variables.
Later, Bi et al. [7] augment it with distributive subtyping in the F+
i ’19 calculus. In addition,
the bottom type is added, and unrestricted intersection types are also allowed to fully encode+
row and bounded polymorphism [44]. Compared to F+
i ’19, our new formulation of Fi adopts a
direct semantics, based on a TDOS approach, where simpler proofs of determinism supersede
the original proofs of coherence. As a result, recursion and impredicative polymorphism
can be easily added. Both features are important to fully support the trait encoding in
Compositional Programming. A detailed comparison of calculi with a merge operator, whichsummarizes our discussion on related work, can be found in Figure 12.
F+i versus F<: . There are quite a few typed object encodings in the literature [8], most ofwhich are based on F<: [10]. As it is not our goal in this paper to encode full OOP in F+i ,we will not compare our trait encoding with other object encodings. However, it is stillinteresting to compare F+
i with F<: . Some disadvantages of F<: have been studied in theliterature. It has been shown that, with bounded quantification, the subtyping of F<: isundecidable [32], and some useful operations like polymorphic record updates [9] are not+directly supported. F+
i does not have these drawbacks. Fi has decidable subtyping. For F<:
the most common decidable fragment is the so-called kernel F<: variant [10]. Xie et al. [44]have shown that kernel F<: is encodable in F+
i . Therefore the bounded quantification thatis present in kernel F<: can be expressed in F+
i as well. In addition, polymorphic record
updates can be easily encoded without extra language constructs. For example, concerning a
polymorphic record that contains an x field among others (rcd : { x: Int } & R), therecord update { rcd with x = 1 } can be encoded in F+
i as { x = 1 } ,, (rcd : R).
In other words, we can rewrite whichever fields we want and then merge the remaining
polymorphic part back.
F+
i versus row-polymorphic calculi. Row polymorphism provides an alternative way to modelA. Fan, X. Huang, H. Xu, Y. Sun, and B. C. d. S. Oliveira

18:25

extensible record types in System F-like calculi. There are many variants of row-polymorphic
calculi in the literature [9, 19, 24, 38]. Among them, the most relevant one with respect toour work is λ|| by Harper and Pierce [19]. Disjoint quantification has a striking similarity
to constrained quantification in λ|| . Their compatibility constraint plays a similar role todisjointness in our system. Furthermore, their merge operator (||) can concatenate either two
records like our merge operator ( , , ) or two record types like our intersection type operator( & ). However, their compatibility constraint and merge operator are only applicable torecord types, while we generalize them to arbitrary types. λ|| has no subtyping and does notallow for distributivity and nested composition either. Disjoint polymorphism also subsumes
the form of row polymorphism present in λ|| as demonstrated by Xie et al. [44]. We refer to
Xie et al.’s work for an extended discussion of the relationship between F+
i and various otherrow polymorphic calculi.
Semantics for type-dependent languages. The elaboration semantics approach is commonlyused to model the semantics of type-dependent languages and calculi. The appeals of theelaboration semantics are simple type-safety proofs, and the fact that they directly offer animplementation technique over conventional languages without a type-dependent semantics.
For instance, the semantics of type-dependent languages with type classes [18, 43], Scala-style
implicits [27, 29] or gradual typing [40] all use an elaboration semantics. In contrast, in thepast, more conventional direct formulations using an operational semantics have been avoided
for languages with a type-dependent semantics. A problem is that the type-dependent
semantics introduces complexity in the formulation of an operational semantics since enoughtype information should be present at runtime and type information needs to be properly
propagated. Early work on the semantics of type classes [23, 28], for instance, attempted
to employ an operational semantics. However, those approaches had significant practical
restrictions in comparison to conventional type classes. The TDOS approach has shownhow to overcome important issues when modeling the direct semantics of type-dependent
languages. An important advantage of the TDOS approach is that it removes the need for
non-trivial coherence proofs. The TDOS approach has also been recently shown to work formodeling the semantics of gradually typed languages directly [45].

6Conclusion

In this paper, we presented a new formulation of the F+i calculus and showed how it serves
as a direct foundation for Compositional Programming. In contrast to the original F+
i , weadopt a direct semantics based on the TDOS approach and embrace call-by-name evaluation.
As a result, the metatheory of F+
i is significantly simplified, especially due to the factthat a coherence proof based on logical relations and contextual equivalence is not needed.
In addition, our formulation of F+i enables recursion and impredicative polymorphism,validating the original trait encoding by Zhang et al. [46]. We proved the type-soundness anddeterminism of F+i using the Coq proof assistant. Our research explores further possibilitiesof the TDOS approach and shows some novel notions that could inspire the design of othercalculi with similar features.
Although F+
i is already expressive enough to work as a core calculus of the CP language,
some useful constructs like type operators are missing. We leave the extension of type-level
operations for future work. Another interesting design choice that we want to explore is tolazily evaluate both sides of merges, just like what we have done for record fields, which canhelp avoid some redundant computation on the unused side of a merge.

ECOOP 2022

18:26

Direct Foundations for Compositional Programming

References
1
2
3
4
5
6
7

8

9
10
11
12
13
14
15
16
17
18
19
20

21

22

Amal Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In
European Symposium on Programming (ESOP), 2006.
João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. Disjoint polymorphism. In European
Symposium on Programming (ESOP), 2017.
Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational
proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657–683, sep 2001.
Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda modeland the completeness of type assignment. The journal of symbolic logic, 48(04):931–940, 1983.
Xuan Bi and Bruno C. d. S. Oliveira. Typed First-Class Traits. In European Conference on
Object-Oriented Programming (ECOOP), 2018.
Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The Essence of Nested Composition.
In European Conference on Object-Oriented Programming (ECOOP), 2018.
Xuan Bi, Ningning Xie, Bruno C. d. S. Oliveira, and Tom Schrijvers. Distributive disjoint
polymorphism for compositional programming. In European Symposium on Programming(ESOP), 2019.
Kim B Bruce, Luca Cardelli, and Benjamin C Pierce. Comparing object encodings. In
International Symposium on Theoretical Aspects of Computer Software, pages 415–438. Springer,
1997.
Luca Cardelli and John C Mitchell. Operations on records. In International Conference onMathematical Foundations of Programming Semantics, 1989.
Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism.
ACM Computing Surveys, 17(4):471–523, 1985.
Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded functions
with subtyping. In Conference on LISP and Functional Programming, 1992.
William R. Cook. A Denotational Semantics of Inheritance. PhD thesis, Brown University,
1989.
Rowan Davies and Frank Pfenning. Intersection types and computational effects. In International Conference on Functional Programming (ICFP), 2000.
Jana Dunfield. Elaborating intersection and union types. Journal of Functional Programming(JFP), 24(2-3):133–165, 2014.
Jana Dunfield and Neel Krishnaswami. Bidirectional typing. ACM Comput. Surv., 54(5), May
2021. doi:10.1145/3450952.
Erik Ernst. Family polymorphism. In European Conference on Object-Oriented Programming(ECOOP), 2001.
Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l’arithmétiqued’ordre supérieur. PhD thesis, Université Paris 7, 1972.
Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip L. Wadler. Typeclasses in haskell. ACM Trans. Program. Lang. Syst., 18(2):109–138, mar 1996.
Robert Harper and Benjamin Pierce. A record calculus based on symmetric concatenation. In
Principles of Programming Languages (POPL), 1991.
Xuejing Huang and Bruno C. d. S. Oliveira. A type-directed operational semantics fora calculus with a merge operator. In Robert Hirschfeld and Tobias Pape, editors, 34th
European Conference on Object-Oriented Programming (ECOOP 2020), volume 166 of Leibniz
International Proceedings in Informatics (LIPIcs), pages 26:1–26:32, Dagstuhl, Germany, 2020.
Schloss Dagstuhl–Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/
opus/volltexte/2020/13183, doi:10.4230/LIPIcs.ECOOP.2020.26.
Xuejing Huang and Bruno C d S Oliveira. Distributing intersection and union types withsplits and duality (functional pearl). Proceedings of the ACM on Programming Languages,
5(ICFP):1–24, 2021.
Xuejing Huang, Jinxu Zhao, and Bruno C. d. S. Oliveira. Taming the merge operator. Journalof Functional Programming, 31:e28, 2021. doi:10.1017/S0956796821000186.

A. Fan, X. Huang, H. Xu, Y. Sun, and B. C. d. S. Oliveira

23
24
25

26
27

28

29

30
31
32
33
34
35
36
37

38

39
40
41

42

18:27

Stefan Kaes. Parametric overloading in polymorphic programming languages. In H. Ganzinger,
editor, ESOP ’88, Berlin, Heidelberg, 1988. Springer Berlin Heidelberg.
Daan Leijen. Extensible records with scoped labels. Trends in Functional Programming,
5:297–312, 2005.
Sheng Liang, Paul Hudak, and Mark Jones. Monad transformers and modular interpreters. In
Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on principles of programming
languages, pages 333–343, 1995.
Fabian Muehlboeck and Ross Tate. Empowering union and intersection types with integrated
subtyping. In OOPSLA, 2018.
Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, andSandro Stucki. Simplicitly: Foundations and applications of implicit function types. Proc.
ACM Program. Lang., 2(POPL), dec 2017.
Martin Odersky, Philip Wadler, and Martin Wehr. A second look at overloading. In Proceedingsof the Seventh International Conference on Functional Programming Languages and Computer
Architecture, FPCA ’95, page 135–146, New York, NY, USA, 1995. Association for Computing
Machinery.
Bruno C. d. S. Oliveira, Adriaan Moors, and Martin Odersky. Type classes as objects andimplicits. In William R. Cook, Siobhán Clarke, and Martin C. Rinard, editors, Proceedingsof the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems,
Languages, and Applications, OOPSLA 2010, October 17-21, 2010, Reno/Tahoe, Nevada,USA, pages 341–360. ACM, 2010. doi:10.1145/1869459.1869489.
Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. Disjoint intersection types. In
International Conference on Functional Programming (ICFP), 2016.
Benjamin C Pierce. A decision procedure for the subtype relation on intersection types withbounded variables. Technical report, Carnegie Mellon University, 1989.
Benjamin C Pierce. Bounded quantification is undecidable. Information and Computation,
112(1):131–165, 1994.
John C Reynolds. Towards a theory of type structure. In Programming Symposium, pages
408–425. Springer, 1974.
John C Reynolds. Preliminary design of the programming language forsythe. Technical report,
Carnegie Mellon University, 1988.
John C. Reynolds. The coherence of languages with intersection types. In Lecture Notes in
Computer Science (LNCS), pages 675–700. Springer Berlin Heidelberg, 1991.
John C Reynolds. Design of the programming language forsythe. In ALGOL-like languages,
pages 173–233. Birkhauser Boston Inc., 1997.
Tom Schrijvers and Bruno C. d. S. Oliveira. Monads, zippers and views: virtualizing themonad stack. In Proceedings of the 16th ACM SIGPLAN international conference on functional
programming, pages 32–44, 2011.
Mark Shields and Erik Meijer. Type-indexed rows. In Proceedings of the 28th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’01, page 261–275,
New York, NY, USA, 2001. Association for Computing Machinery. doi:10.1145/360204.
360230.
Jeremy G. Siek. Transitivity of subtyping for intersection types. CoRR, abs / 1906.09709,
2019. URL: http://arxiv.org/abs/1906.09709, arXiv:1906.09709.
Jeremy G Siek and Walid Taha. Gradual typing for functional languages. In Scheme andFunctional Programming Workshop, 2006.
Jeremy G. Siek and Walid Taha. Gradual typing for objects. In Erik Ernst, editor, ECOOP
2007 - Object-Oriented Programming, 21st European Conference, Berlin, Germany, July 30 August 3, 2007, Proceedings, volume 4609 of Lecture Notes in Computer Science, pages 2–27.
Springer, 2007.
Philip Wadler. The expression problem. Java-genericity mailing list, 1998.

ECOOP 2022

18:28

Direct Foundations for Compositional Programming

43

44

45

46

Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad-hoc. In
Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming
Languages, Austin, Texas, USA, January 11-13, 1989, pages 60–76. ACM Press, 1989. doi:
10.1145/75277.75283.
Ningning Xie, Bruno C d S Oliveira, Xuan Bi, and Tom Schrijvers. Row and boundedpolymorphism via disjoint polymorphism. In 34th European Conference on Object-Oriented
Programming (ECOOP 2020). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020.
Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang. Type-directed operational semantics
for gradual typing. In Anders Møller and Manu Sridharan, editors, 35th European Conference
on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual
Conference), volume 194 of LIPIcs, pages 12:1–12:30. Schloss Dagstuhl - Leibniz-Zentrum fürInformatik, 2021.
Weixin Zhang, Yaozhu Sun, and Bruno C. d. S. Oliveira. Compositional programming. ACM
Transactions on Programming Languages and Systems (TOPLAS), 43(3):1–61, 2021.