Imperative Compositional Programming
Type Sound Distributive Intersection Subtyping with References via Bidirectional Typing

WENJIA YE, The University of Hong Kong, ChinaYAOZHU SUN, The University of Hong Kong, China
BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, China
Compositional programming is a programming paradigm that emphasizes modularity and is implemented in the
CP programming language. The foundations for compositional programming are based on a purely functionalvariant of System F with intersection types, called 𝐹 i+ , which includes distributivity rules for subtyping.
This paper shows how to extend compositional programming and CP with mutable references, enablinga modular, imperative compositional programming style. A technical obstacle solved in our work is theinteraction between distributive intersection subtyping and mutable references. Davies and Pfenning [2000]
studied this problem in standard formulations of intersection type systems and argued that, when combinedwith references, distributive subtyping rules lead to type unsoundness. To recover type soundness, they
proposed dropping distributivity rules in subtyping. CP cannot adopt this solution, since it fundamentally relies
on distributivity for modularity. Therefore, we revisit the problem and show that, by adopting bidirectional
typing, a more lightweight and type sound restriction is possible: we can simply restrict the typing rule
for references. This solution retains distributivity and an unrestricted intersection introduction rule. We
present a first calculus, based on Davies and Pfenning’s work, which illustrates the generality of our solution.
Then we present an extension of 𝐹 i+ with references, which adopts our restriction and enables imperative
compositional programming. We implement an extension of CP with references and show how to model a
modular live-variable analysis in CP. Both calculi and their proofs are formalized in the Coq proof assistant.
CCS Concepts: • Software and its engineering → Imperative languages; Data types and structures.
Additional Key Words and Phrases: Bidirectional Typing, Mutable References, Intersection Types, Distributive
Subtyping, Type Soundness, Compositional Programming
ACM Reference Format:
Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira. 2024. Imperative Compositional Programming: Type Sound
Distributive Intersection Subtyping with References via Bidirectional Typing. Proc. ACM Program. Lang. 8,
OOPSLA2, Article 342 (October 2024), 30 pages. https://doi.org/10.1145/3689782

1

Introduction

Compositional programming [Zhang et al. 2021] is a programming paradigm that emphasizes
modularity and is implemented in the CP programming language. The well-known expression
problem [Wadler 1998] can be naturally solved with compositional programming. Compositional
programming borrows ideas from both functional and object-oriented programming (OOP). The
OOP idea of family polymorphism [Ernst 2001] is closely related to compositional programming.
Prior research on family polymorphism [Aracic et al. 2006; Ernst et al. 2006; Nystrom et al. 2004,
2006; Zhang and Myers 2017] explored extensions to OOP that enable inheritance of complete
Authors’ Contact Information: Wenjia Ye, The University of Hong Kong, Hong Kong, China, yewenjia@connect.hku.hk;
Yaozhu Sun, The University of Hong Kong, Hong Kong, China, yzsun@cs.hku.hk; Bruno C. d. S. Oliveira, The University ofHong Kong, Hong Kong, China, bruno@cs.hku.hk.
Permission to make digital or hard copies of all or part 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).
© 2024 Copyright held by the owner/author(s).
ACM 2475-1421/2024/10-ART342
https://doi.org/10.1145/3689782

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:2

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira

hierarchies of classes, instead of just a single class. In compositional programming, complete setsof traits [Bi and Oliveira 2018; Ducasse et al. 2006] (which play a similar role to classes) can becomposed. This is similar to the composition of whole hierarchies of classes in family polymorphism.
However, the programming style employed in compositional programming departs from traditional OOP programming, and is based on a form of open pattern matching. This is an influence
from functional programming. Compositional programming fits within a more general and recent
theme of work [Fan and Parreaux 2023; Jin et al. 2023; van der Rest and Poulsen 2022, 2023], whichaims at addressing modularity problems of functional programming. In particular, in functional
programming, both algebraic datatypes and functions, defined by pattern matching, are closed
to extensions. Several researchers have noted this problem and have proposed language designs
with constructs that enable a similar programming style based on pattern matching, but wheredefinitions are open, and nonetheless checked for exhaustiveness of patterns. In compositional
programming, compositional interfaces play a similar role to algebraic datatypes, declaring sets ofconstructors. Unlike algebraic datatypes, compositional interfaces are composable and extensible.
Traits are used to implement sets of reusable patterns, playing a similar role to pattern matching
definitions in functional programming. However, traits are also open and extensible.
The foundations for compositional programming are based on a variant of System F [Girard 1972;
Reynolds 1974] with intersection types [Coppo et al. 1981; Pottinger 1980], called 𝐹 i+ [Fan et al. 2022],
which includes distributive subtyping rules [Barendregt et al. 1983] and a merge operator [Dunfield
2014; Reynolds 1988]. Distributive subtyping rules are needed to support nested composition [Biet al. 2018], which is key to compositional programming, and enables the composition of sets oftraits. For instance, the distributivity rule between intersection and function types is:
S-d(𝐴 → 𝐵 1 )&(𝐴 → 𝐵 2 ) <: 𝐴 → (𝐵 1 &𝐵 2 )So far, compositional programming, as well as work within the same theme [Fan and Parreaux2023; Jin et al. 2023; van der Rest and Poulsen 2022, 2023], has focused on purely functional styles.
The current implementation of CP and the core 𝐹 i+ calculus is purely functional and lacks support
for imperative features. However, the addition of imperative features, such as mutable references,can be helpful. For instance, CP supports objects. Adding mutable references would enable CP
to model stateful objects. In addition, mutable references are useful to model certain programs,
which are hard to model in a purely functional setting. For instance, in program analysis, we often
need algorithms that operate on graphs. More generally, graph algorithms are common in several
domains such as graph databases, grammars, finite state machines or transition systems. While
in a purely functional setting, it is easy and natural to write programs on tree structures, graphstructures are challenging, and not many techniques exist to deal with graph structures (but see[Erwig 2001; Oliveira and Cook 2012b]). The use of references provides a simple way to modelgraph structures. Cycles can be created using mutable references and detected using reference
equality.
Our goal is to extend previous calculi for compositional programming with references, to broaden
the scope of compositional programming to imperative programming. This will enable mutableobjects, as well as programs that operate on graph structures. Unfortunately, there is a major obstacle
to achieving this goal. Davies and Pfenning [2000] have argued that references are incompatible
with distributive intersection subtyping, including the rule S-d. They showed that a calculus withstandard distributive intersection subtyping and references leads to type unsoundness. Thus, since
compositional programming fundamentally relies on distributive intersection subtyping, it seems,
at first, that there is little hope of adding references to compositional programming.
In this paper, we propose a simple, and lighter, alternative restriction that enables references in
the presence of distributive intersection subtyping, while preserving type soundness. Our restriction
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

Imperative Compositional Programming

342:3

exploits bidirectional typing [Dunfield and Krishnaswami 2021], which distinguishes between twomodes of typing: checking and inference. With bidirectional typing, an expression can be checkedagainst many types, but typically it can only infer the most precise type. We exploit this distinction
to restrict the typing rule for references, allowing only a rule in inference mode:
Σ; Γ ⊢ 𝑒 ⇒ 𝐴Σ; Γ ⊢ ref 𝑒 ⇒ Ref 𝐴
We show that, with a bidirectional type system with this rule, we can forbid the problems identified
by Davies and Pfenning. Our restriction enables an unrestricted intersection introduction ruleand distributivity. We present two type sound calculi with distributive intersection subtyping
and references. Both calculi adopt our lighter restriction. The first one is a variant of the calculus
presented in Davies and Pfenning’s work. This calculus is useful to show the key ideas of ourapproach, and to illustrate that the solution can be applied to a wide range of calculi with intersection
types. The second calculus is a variant of 𝐹 i+ with references, and it is the calculus that underlies our
new extension of the CP programming language. Using our new implementation of CP extended
with references, in Section 2, we illustrate how graph structures are encoded by CP using a livevariable analysis example. Overall, the contributions of this paper are as follows:• Imperative Compositional Programming: We show how to integrate references into alanguage with compositional programming, enabling highly modular imperative programs.
• A lightweight restriction, based on bidirectional typing, to enable a calculus featuring
distributive intersection subtyping and references.
• Two type sound calculi that demonstrate the use of the restriction. The first calculus is avariant of Davies and Pfenning’s calculus while the second is a variant of 𝐹 i+ with references.
• Coq formalization, CP implementation and examples. Both calculi and their proofs in
the paper are formalized in the Coq proof assistant. Furthermore, we have an implementationof CP, based on 𝐹 i+ extended with references, that can type check and run examples for thepaper. An extended version of the example is also provided in the artifact [Ye et al. 2024].
2

Compositional Programming with References

In this section, we provide background on the expression problem and compositional programming,and show how compositional programming and the CP language are extended with support forreferences. We illustrate this support via an example that modularly constructs components of animperative programming language and its control-flow graph, enabling a live-variable analysis [Ahoet al. 2007].
2.1

Background: the Expression Problem

The imperative programming language that we are going to model starts with a minimal set of
language constructs. We first illustrate how one could model such language constructs in Java tomotivate and demonstrate the expression problem [Wadler 1998]. The expression problem is awell-known dilemma in programming languages, which shows that some programming languages
are good at achieving certain forms of extensibility but bad at some other forms of extensibility.
The abstract syntax of the initial language is defined in Java as follows:interface Exp { String print(); }class Var extends Exp { String print() { ... } }class Ass extends Exp { String print() { ... } }class Seq extends Exp { String print() { ... } }// variable: x, y, z, ...
// assignment: x = y// sequential composition: p; q

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:4

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira

Exp represents the interface for all language constructs, which only contains a pretty-printing
method at the beginning. Var, Ass, and Seq implement the interface and contain different print

implementations.
First dimension of extensibility: more language constructs. The initial language is so minimal that
we can hardly write any useful programs. In particular, it does not even allow primitive values. To
make the language more expressive, we may want to add more language constructs like booleans
and while-loops. In Java, adding more language constructs is simply done by adding new classes:
class NewConstruct extends Exp { String print() { ... } }The addition of language constructs is modular because we do not need to modify existing code.
This demonstrates that Java has good support for this form of extensibility.
Second dimension of extensibility: more operations. However, it is hard to modularly add more
operations other than pretty-printing in Java. Usually, we have to modify the Java Exp interface to:interface Exp { String print(); T newOperation(); }Of course, we need to do similar modifications to the classes that implement the interface to include
the new operation. Changing existing code like this is not modular. Thus, Java is not good at thissecond form of extensibility. Such a modularity problem is known as the expression problem. As weshall see, compositional programming provides a natural solution to this dilemma of extensibility.
2.2

A Brief Introduction to Compositional Programming

The compositional programming paradigm [Zhang et al. 2021] is implemented by the CP language
and introduces several new notions for modularity. The first notion that needs explanation isthat of a compositional interface. A compositional interface consists of type signatures for a set of
constructors, and plays an analogous role to algebraic datatype definitions in functional languages.
For example, the same abstract syntax previously defined in Java can be rewritten in CP as follows:
type SeqSig<Exp> = {Var: String → Exp;-- variable: x, y, z, ...
Ass: String → Exp → Exp; -- assignment: x = y
Seq: Exp → Exp → Exp;-- sequential composition: p; q};

In this compositional interface, we declared three constructors for three language constructs. The
type parameter Exp, delimited by angle brackets, is called a sort and must be the return type ofevery constructor. A sort abstracts over different kinds of operations that can be applied to theprogram. A simple example is the aforementioned pretty-printing operation. We can instantiate
the sort with type Print as follows:
type Print = { print: String };printSeq = trait implements SeqSig<Print> ⇒ {(Varx).print = x;(Assx e).print = x ++ " = " ++ e.print;(Seq e1 e2).print = e1.print ++ "; " ++ e2.print;};

The instantiated interface is implemented by a compositional trait [Bi and Oliveira 2018; Ducasse
et al. 2006], which is a basic reusable unit in CP. A trait is by default in an anonymous form, such as
trait ... ⇒ { ... }, but we can always assign it to a variable, for example printSeq, to give it aname. The pattern-matching-like syntax (Var x).print = x is called a method pattern and desugars
into a record field with nested traits:
Var = \x → trait ⇒ { print = x };Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

Imperative Compositional Programming

342:5-- Extension 1: Compositional interface and trait for booleans and pretty-printing
type BoolSig<Exp> = {Lit: Bool → Exp; -- literal: true, false
Not: Exp → Exp;-- negation: not x};
printBool = trait implements BoolSig<Print> ⇒ {(Lit b).print = toString b;(Not e).print = "not " ++ e.print;};-- Extension 2: Compositional interface and trait for while-loops and pretty-printing
type LoopSig<Exp> = {WhileDo: Exp → Exp → Exp; -- while (...) do { ... }DoWhile: Exp → Exp → Exp; -- do { ... } while (...)};
printLoop = trait implements LoopSig<Print> ⇒ {(WhileDo cond body).print ="while (" ++ cond.print ++ ") do { " ++ body.print ++ " }";(DoWhile body cond).print ="do { " ++ body.print ++ " } while (" ++ cond.print ++ ")";};
Fig. 1. Adding more language constructs for booleans and while-loops in CP.

Such syntactic sugar allows programming in CP in a style resembling pattern matching in functional
languages like Haskell and ML.
First dimension of extensibility: more language constructs. Although the initial language is too
simple to be useful in isolation, it captures basic imperative constructs in a standalone manner andcan be composed with other features later, enabling a modular style advocated in compositional
programming. What we expect is to add more language constructors in a modular way like in Java.
The extension of language constructs is similarly easy in CP. Instead of new classes, we create acompositional interface and some traits implementing the existing operation for new constructs.
For example, we add two more compositional interfaces and traits for booleans and while-loops
respectively in Figure 1.
Second dimension of extensibility: more operations. We have shown the second dimension of theexpression problem is difficult to solve in mainstream OOP languages like Java. In CP, the solution
to the second dimension is trivial. We will show how CP solves the expression problem next.
2.3

Solving the Expression Problem: Adding CFG Construction

Extending CP with imperative features. The original formulation of CP [Zhang et al. 2021] ispurely functional and lacks support for imperative programming constructs, such as mutablereferences. In this work, we extend CP itself with references and four related operations:(1) ref e creates a reference cell with an initial value e.
(2) !e reads the value stored in the reference cell e (a.k.a. dereference).
(3) e1 := e2 writes the value e2 to the reference cell e1 (a.k.a. assignment).
(4) e1 >> e2 executes the imperative statement e1 and then returns e2 (a.k.a. sequencing).
To illustrate the importance of imperative features in compositional programming, we present an
example of a data-flow analysis. The goal is to compute the set of variables that are live at eachProc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:6

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. OliveiragraphSeq = trait implements SeqSig<Graph> ⇒ {(Varx).graph = let r = ref (newNode ("Var " ++ x) [] [x]) in
mkPair r r;(Assx p).graph = let r = ref (newNode ("Ass " ++ x) [x] []) in
addAdj (snk p) [r] >>mkPair (src p) r;(Seq p1 p2).graph = addAdj (snk p1) [src p2] >>mkPair (src p1) (snk p2);};
newNode (s: String) (def: [String]) (use: [String]) = {name = s;adj = ref ([] : [Ref Node]);def = def;
use = use;
IN = ref ([] : [String]); OUT = ref ([] : [String]);};
addAdj (x: Ref Node) (ys: [Ref Node]) = !x.adj := !(!x.adj) ++ ys;
Fig. 2. Building a CFG for the initial language constructs.

program point. The live-variable analysis is done on a control-flow graph (CFG) constructed fromthe program. Without mutable references, it is inconvenient to construct a CFG and perform someanalysis in CP. The first difficulty is how to represent the directed edges in the CFG. Since a whileloop may introduce a cycle in the graph, the connected nodes should be represented by references
instead of values. When traversing a cyclic graph, we need to detect cycles using reference equality
to avoid infinite loops. In addition, we also need flag variables to indicate whether an analysis hasconverged.
Representation of the CFG. In a CFG, each node represents a program segment, whose edges
are directed and represent possible execution paths. The directed edges are implemented as an
adjacency array stored in a node. The whole graph is represented by a pair of nodes: one for thesource, and the other for the sink. The definitions are as follows:interface Node {name: String;
adj: Ref [Ref Node];
def: [String];
use: [String];-- variables defined and used
IN: Ref [String]; OUT: Ref [String]; -- for live-variable analysis};
type Graph = { graph: PairRefNode }; -- (src, snk)
Node uses the keyword interface instead of type because it is a recursive type – the adj field uses
Node itself. Recursive types are not supported in the work by Zhang et al. [2021]. Our enhanced
implementation of CP supports recursive types, via interface declarations, based on the work by

Zhou et al. [2022]. The adjacency array can be updated during the construction of the CFG, so the
adj field is a reference. In other words, adj is similar to a mutable field in other languages. The
element of the adjacency array is also a reference – otherwise, the same node can have multiple
copies in its predecessors, and cycles in the graph cannot be represented.
CFG construction for the initial language. In CP, adding a new operation is as easy as adding new
language constructs – all that we need is to create more traits. In Figure 2, we create one more trait
for the initial language. We instantiate Exp with type Graph in the trait graphSeq and implement the
CFG construction. Both Var and Def are mainly creating new CFG nodes, while the task of Seq is to
add a directed edge from the sink node of p1’s graph to the source node of p2’s graph.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

Imperative Compositional Programming

342:7

graphBoolLoop = trait implements BoolSig<Print ⇒ Graph> & LoopSig<Graph> ⇒ {[self]@(Lit b).graph = let r = ref (newNode self.print [] []) in mkPair r r;
(Not e).graph = e.graph;(WhileDo cond body).graph = addAdj (snk cond) [src body] >>addAdj (snk body) [src cond] >>mkPair (src cond) (snk cond);(DoWhile body cond).graph = addAdj (snk body) [src cond] >>addAdj (snk cond) [src body] >>mkPair (src body) (snk cond);};
Fig. 3. Building a CFG for booleans and while-loops.
snk

cond
src

src
cond

……

snk
cond

body
src
body

……

body
snk
body

(a) while (cond) do { body }

src

src
body

……

cond
snk
body

src
cond

……

snk
cond

snk

(b) do { body } while (cond)Fig. 4. CFG examples for while-loops.

In newNode, we initialize the adjacency array to be empty. Some extra type annotations are needed
there because, by default, an empty array [] is inferred to have type [Bot]. Then ref [] has type
Ref [Bot] and cannot be coerced into type Ref [String], for instance, because the former is not a
subtype of the latter. The addAdj function adds more nodes to the adjacency array, to add more
directed edges that start from a certain node. Since the function body is merely an assignment
statement, addAdj returns the unit value.
CFG construction for booleans and while-loops. As mentioned in Section 2.2, adding new language
constructs is easy. The implementation for both booleans and while-loops is shown in Figure 3.
Of course, if desired, we could also separate the implementation into two traits. Compositional
programming allows finer- or coarser-grained traits for different scenarios. The boolean part does
not affect control flow, but shows CP’s ability to modularly inject dependencies between different
traits [Zhang et al. 2021]. Instead of directly creating a string for the node identifier, as we did ingraphSeq, we call print. Although print is not defined in graphBoolLoop, we state the dependency
on print by instantiating BoolSig with <Print ⇒ Graph>. Thus we can use self.print in (Litb).graph. At composition time (see Section 2.4), an implementation of Print must be provided tosatisfy the dependency. The CFGs built for while-loops are shown in Figure 4. The two variantsof CFGs are similar except that the sink node for while (cond) do { body } is not in body, but in
cond, since we have to check if the condition holds before quitting the loop.
2.4

Putting Everything Together: Distributive Intersection Types in Action

After we have the five traits that implement pretty-printing and CFG construction for the seven
existing language constructs, we may combine them together. Our goal is graphically illustrated in
Figure 5. The difficulty here is how to nestedly compose multiple operations (in this case, print andgraph) within the same constructor. In CP, such nested trait composition [Bi et al. 2018] is achievedby the merge operator [Dunfield 2014; Reynolds 1997], which is denoted by a comma:
type ProgSig<Exp> = SeqSig<Exp> & BoolSig<Exp> & LoopSig<Exp>;merged: ProgSig<Print&Graph> = new printSeq,printBool,printLoop,graphSeq,graphBoolLoop;

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:8

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira

Without nested composition and distributivity (as indicated by the type annotation), merged would
have type ProgSig<Print> & ProgSig<Graph> and contain duplicate fields for each constructor. After
desugaring method patterns, merged would be:
merged = {Var = \x → trait ⇒ { print = x };Var = \x → trait ⇒ { graph = let r = ... in mkPair r r };-- other constructors are similar};

However, what we actually expect is, as shown in Figure 5, to have only one Var field that serves asa constructor that can be used for both pretty-printing and CFG construction:
merged = {Var = \x → trait ⇒ { print = x; graph = let r = ... in mkPair r r };-- other constructors are similar};
In other words, we desire merged to be coerced into the type ProgSig<Print&Graph>. The subtyping
relation between ProgSig<Print> & ProgSig<Graph> and ProgSig<Print&Graph> is valid becauseintersection types in CP are distributive over function, trait, and record types.
Encoding of traits. It is helpful to understand how traits are encoded in CP, to understand how+ does not include any OOP-related
the distributivity of traits works. As we shall see in Section 4, 𝐹 im
constructs. This is because these language constructs are encoded using functions and records in+ . For example, a trait in CP is desugared to a function, where the argument of the function is the
𝐹 imself-reference of the trait [Bi and Oliveira 2018; Zhang et al. 2021]. This encoding of traits follows
the denotational model of inheritance by Cook and Palsberg [1989]. A simple example illustrating
the encoding is given next:
t1 = trait ⇒ { x = 1 };t1' = \(self: Top) → { x = 1 };-- is desugared to:-- having type: Top → {x: Int}t2 = trait [self: {x: Int}] ⇒ { y = self.x }; -- is desugared to:t2' = \(self: {x: Int}) → { y = self.x };-- having type: {x: Int} → {y: Int}Thus, the nested composition of two traits is essentially merging two functions, powered by the
distributive intersection subtyping over functions. In other words, distributivity over trait types
boils down to distributivity of intersections over function types, and the rule rule S-d. For example,
the merge t1',t2' has type(Top → {x: Int}) & ({x: Int} → {y: Int})

which is, via distributivity, a subtype of
Top & {x: Int} → {x:Int} & {y: Int}-- or equivalently, {x: Int} → {x: Int; y: Int}

Back to CP’s trait encoding, the function type above corresponds to Trait<{x: Int} ⇒ {x: Int;y: Int}>. That is, the trait itself contains two fields x and y while assuming the self-reference has
type {x: Int}. We refer the readers who are interested in the encoding of other constructs likecompositional interfaces to previous work [Zhang et al. 2021].
2.5

Live-Variable Analysis

Let us go back to the topic of data-flow analysis. Since we can already build a CFG from a given
program, it should be easy to do various analyses based on the CFG. Here we pick live-variable
analysis, which computes the set of variables that are live at each program point. As shown in
Figure 6, we continue making use of imperative features in CP to make the analysis possible. The
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

Imperative Compositional Programming

342:9
mergedprintSeq
Var

Ass+ print+ printSeq+ print,

printBool

printLoop

Lit

WhileDo+ print
Not+ print,+ print
DoWhile+ print

graphSeq

,

Var

Ass

+ graph+ graphSeq

graphBoolLoop,+ graphLit

Not+ graph+ graphWhileDo

DoWhile+ graph+ graph

=

Var

Ass

Seq

+ print+ print+ print+ graph+ graph+ graphLit

Not

WhileDo

DoWhile+ print+ print+ print+ print+ graph+ graph+ graph+ graphFig. 5. Nested trait composition in CP.

algorithm is standard and can be found in any textbook on program analysis (see, for instance,
Aho et al. [2007]). The analysis is performed in a backwards manner, starting from the sink node of
the whole CFG and propagating the live variables back to the source node. The IN and OUT states
represent the set of live variables corresponding to the entry and exit of each node, respectively.
The basic idea of the analyze function is to iteratively update the IN/OUT states of each node until
no IN is changed anymore. The transfer functions for IN/OUT in each iteration are:IN[𝑃] = use𝑃 ∪ (OUT[𝑃] \ def𝑃 )Ø
OUT[𝑃] =IN[𝑄]𝑄 ∈adj𝑃

The live variables at the entry of a node 𝑃 are those used in 𝑃 plus the live variables at the exit of 𝑃
that are not defined in 𝑃. The live variables at the exit of 𝑃 are the union of those at the entry of allnodes that are successors of 𝑃. Since IN/OUT need to be updated iteratively, they are modeled as
references in CP, or mutable fields in other languages. Some implementations of set operations onarrays like union and difference are omitted for brevity. Note that the notation adj!!i is used toaccess the 𝑖-th element of the array adj. The visited set is used to avoid repeated visits to the samenode as well as infinite loops if the CFG is cyclic. The set is cleared before a new iteration. The
flag variable changed, in the first line of analyzeLiveVar’s body in Figure 6, is also a reference. It is
initialized to store the boolean value false at the beginning of each iteration and will be updatedwith true if there is any change on the IN states. The analyzeLiveVar function is essentially a loopthat checks if the dereferenced value !changed is true. If so, it will start a new iteration; otherwise,
the loop ends. A sample program is constructed in the last part of Figure 6. The open keyword isused to open a record, which brings all constructors in merged into the current scope. Thus we candirectly use, for example, Seq instead of merged.Seq. Then we call analyzeLiveVar on the program
to compute the live variables, which are stored in IN/OUT fields of each node.
In conclusion, CP extended with mutable references enables imperative compositional programming, as showcased by our modular live-variable analysis example. Some more complicatedalgorithms that usually depend on mutability, such as program analysis, are made possible by theimperative features. What is more, distributive intersection types can interact well with mutablereferences in CP, resulting in a type sound language.
2.6

CP Implementation and Extended Example

All the examples presented in this section can run in our CP implementation. Note that we extended
the original implementation by Zhang et al. [2021]. In particular, we added references and some otherfeatures such as recursive types [Zhou et al. 2022]. In the original design of CP, the implementation
works by elaborating CP into a core calculus, called 𝐹 i+ [Fan et al. 2022], which is based on disjoint
intersection types [Oliveira et al. 2016] and disjoint polymorphism [Alpuim et al. 2017] and distributive
subtyping. Our implementation works similarly, except that we extend 𝐹 i+ with additional features.
+ , which serves as a foundation
In Section 4, we formalize an extension of 𝐹 i+ with references, called 𝐹 im
for our implementation. The elaboration from source language constructs (such as traits andProc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:10

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira

analyze (x: Ref Node) (changed: Ref Bool): () = if isVisited x then () else
visited := !visited ++ [x] >>letrec go (i: Int): [String] =let adj = !(!x.adj) in
if i == #adj then [] else analyze (adj!!i) changed >>union !(!(adj!!i).IN) (go (i+1)) in!x.OUT := go 0 >>let oldIN = !(!x.IN) in!x.IN := union !x.use (difference !(!x.OUT) !x.def) >>if equal oldIN !(!x.IN) then () else changed := true;
analyzeLiveVar (prog: Graph): () =let changed = ref true in
letrec go (_: ()): () =if !changed then changed := false >>clearVisited () >>analyze (src prog) changed >>go ()else () ingo ();
prog = open merged in
Seq (Ass "x" (Lit true))-- x = true;(Seq (Ass "y" (Lit false))-- y = false;(Seq (WhileDo (Var "x") (Ass "x" (Var "y"))) -- while (x) do { x = y };(Ass "z" (Not (Var "x")))));-- z = not x
analyzeLiveVar prog -- main bodyFig. 6. Live-variable analysis based on the CFG.

compositional interfaces) is treated in previous work [Bi and Oliveira 2018; Zhang et al. 2021]. The
addition of references is mostly orthogonal to source language constructs and has little impact on
the elaboration. In other words, source language constructs like assignments or reference creation+ . Thus, they are trivial to add to the elaboration step. One
map directly into similar constructs in 𝐹 im
significant change in our implementation of CP is that CP now supports compilation into JavaScript.
The previous implementation was based on an interpreter. Our extended implementation of CP isavailable in the artifact.
Extended example. An extended version of the example presented in this section is also available
in our artifact. All code that is omitted for space reasons in this section can be found there. In theextended example, we add more language constructs like numeric literals, more operations onbooleans and integers, and if-then-else statements. We also implement a depth-first traversal of the
CFG, which can print the live variables at each program point.
3

A Type Sound Calculus with Distributive Subtyping and References

This section proposes a simple restriction for calculi with distributive subtyping, intersection types
and references based on bidirectional typing. This restriction is lighter than the one proposed by
Davies and Pfenning [2000], since it allows distributive subtyping in the presence of references. In
addition, it does not require a value restriction. Since in CP distributive subtyping is fundamental,
our lighter restriction enables the design of calculi that support compositional programming in thepresence of references, as shown in Section 4. We start by revisiting the type unsoundness problem
identified by Davies and Pfenning, and then present our solution.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

Imperative Compositional Programming

342:11

𝐴 <: 𝐵 1
S-Andl
𝐴1 & 𝐴2 <: 𝐴1
𝐵 <: 𝐴

𝐴 <: 𝐵 2

S-AndrS-And

𝐴1 & 𝐴2 <: 𝐴2

𝐴 <: 𝐵 1 & 𝐵 2

𝐴 <: 𝐵
S-Ref

S-d(𝐴 → 𝐵 1 ) & (𝐴 → 𝐵 2 ) <: 𝐴 → (𝐵 1 & 𝐵 2 )Ref 𝐴 <: Ref 𝐵

Fig. 7. Declarative subtyping of Davies and Pfenning [2000] (excerpt).
let x = ref 1 : Ref Nat & Ref Pos in
let y = (x := 0) in
let z = !x in z : Pos↩→ o = 1; let y = (o := 0) in
let z = !o in z : Pos↩→ o = 0; let z = !o in z : Pos↩→ o = 0; 0 : Pos(a)let x = (𝜆x. ref 1) unit : Ref Nat & Ref Pos in
let y = (x := 0) in
let z = !x in z : Pos↩→ let x = ref 1 : Ref Nat & Ref Pos in
let y = (x := 0) in let z = !x in z : Pos↩→* o = 0; let z = !o in z : Pos↩→* o = 0; 0 : Pos(b)Fig. 8. Counter-examples identified by Davies and Pfenning [2000].

3.1

Problematic Interaction between References and Distributive Subtyping

Davies and Pfenning [2000] proposed a calculus and type assignment system for a language withintersection types and references. As usual for most type assignment systems, expressions areallowed to have multiple types. For instance, 1 can have as type Nat or Pos, among others. In theirsubtyping relation, they use standard rules for intersection and reference types in Figure 7. Notethat subtyping for reference types (rule S-ref) is invariant (𝐴 <: 𝐵 and 𝐵 <: 𝐴). The distributivity
rule S-d states that an intersection of two functions with the same input type is a subtype of afunction that returns the intersection of the output types. Davies and Pfenning [2000] concluded
that general intersection types are unsound with mutable references. Next we will illustrate why
type unsoundness happens using their examples.
Type unsoundness from intersection introduction. We show some typing rules of Davies andPfenning [2000] that are used to illustrate the problem next:
Σ; Γ ⊢ 𝑒 : 𝐴

Pty-subΣ; Γ ⊢ 𝑒 : 𝐵
Σ; Γ ⊢ 𝑒 : 𝐴

Σ; Γ ⊢ 𝑒 : 𝐴

𝐴 <: 𝐵Σ; Γ ⊢ 𝑒 : 𝐵

Σ; Γ ⊢ 𝑒 : 𝐴 & 𝐵

Σ; Γ ⊢ ref 𝑒 : Ref 𝐴

Σ; Γ ⊢ 𝑒 : Ref 𝐴
Pty-ref

Σ; Γ ⊢ 𝑒 1 : Ref 𝐴
Pty-intro

Σ; Γ ⊢ !𝑒 : 𝐴

Pty-def

Σ; Γ ⊢ 𝑒 2 : 𝐴

Σ; Γ ⊢ 𝑒 1 := 𝑒 2 : Unit

Pty-setNote that, in our presentation of the two examples, we first present the original program by Davies
and Pfenning in the first 4 lines, and then present reduction steps to illustrate what happens duringexecution. The first problematic program that Davies and Pfenning illustrate is in Figure 8a. In
this program, 1 has type Pos. Moreover, since Pos is a subtype of Nat, by rule Pty-sub, 1 can havetype Nat as well. Then, by rule Pty-ref, the expression ref 1 can have type Ref Pos and also type
Ref Nat. Finally, because of rule Pty-intro, the expression ref 1 can be typed as the intersection
type Ref Nat & Ref Pos. From the subtyping rule S-Andl for intersection types, we know that
Ref Nat & Ref Pos is a subtype of Ref Nat. Thus, x can be assigned a Nat number 0. Because x has
type Ref Nat & Ref Pos, and it can be upcast to Ref Pos via the subsumption rule, then z can havetype Pos. Therefore, this program is typeable. However, when we run the program, z is going tobe 0. In the first step, a new cell is created with value 1 referenced by the location o. Note that asemicolon (;) is used to separate the cell (o = 1) and the program. Then a value 0 is assigned to thatlocation. After that, we read the content and annotate the value to have type Pos. Obviously, 0 can
not be typed as Pos. So typing is unsound. In essence, the assignment in the program is problematic
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:12

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira

since x also has type Ref Pos, but ref 0 should not have that type, since 0 is not a positive number.
In this program the intersection introduction rule plays an important role because it allows ref 1
to be typed with two different reference types.
Type unsoundness from distributivity. A second problematic program that Davies and Pfenning
illustrate is in Figure 8b. This program is nearly the same as the first one, except for the firstline, where ref 1 is replaced by (𝜆x.ref 1) unit. The expression (𝜆x.ref 1) can be typed with
(Unit → Ref Nat) & (Unit → Ref Pos). From subtyping distributivity (rule S-d), (Unit → Ref
Nat) & (Unit → Ref Pos) <: Unit → (Ref Nat & Ref Pos) holds. Therefore, type Unit → (RefNat & Ref Pos) can be used to type check (𝜆x.ref 1). Then the lambda body ref 1 can be checked
as Ref Nat & Ref Pos. This expression exploits the subtyping distributivity rule, to also create avariable x with the same type as the x in the first program. After one step of reduction, the programin Figure 8b becomes essentially the program in Figure 8a. Then, using the same line of reasoning
for the first program, we are able to conclude that this program also leads to type unsoundness.
It is worthwhile noting, that while we show counter-examples using Nat and Pos, the counterexamples can be adapted to many other settings, as Davies and Pfenning observe. For instance,
suppose that the calculus contains a canonical top value ⊤, which can only be typed with ⊤, then we
can easily produce similar counter-examples by replacing Nat by ⊤, and 0 by ⊤. Another example
would be two record types 𝐴 and 𝐵 where 𝐴 <: 𝐵. In this case, 𝐴 would play the role of Pos and 𝐵
would play the role of Nat. Then we could replace 1 and 0 by two records of type 𝐴 and 𝐵. Thus, it iseasy to adapt the counter-examples to various other settings, and obtain similar counter-examples
to type soundness.
3.2

Davies and Pfenning’s Solution

Davies and Pfenning [2000] suggested that the intersection introduction rule, and the distributivity
rule used in subtyping are the causes of type unsoundness. To address this problem they proposed
two restrictions: 1) a value restriction on intersection introduction; and 2) removing distributivity
from subtyping. Their value restriction is inspired by the restriction employed in ML [Wright1995] to solve the unsoundness problem of parametric polymorphism. Concretely, only values areallowed in intersection introduction:
Σ; Γ ⊢ 𝑣 : 𝐴
Σ; Γ ⊢ 𝑣 : 𝐵
Σ; Γ ⊢ 𝑣 : 𝐴&𝐵
Now, we can consider the first program again. With the restricted intersection introduction rule,
the first program fails to pass the type checker. Even though ref 1 can be typed with ref Nat and
Ref Pos, ref 1 is not a value. In standard calculi with references, the values denoting references
can only be locations. Therefore, the first program is rejected. More generally, type unsoundness
cannot be triggered by this restricted intersection introduction rule.
However, we still need to deal with the second program. For lambdas, (𝜆x.ref 1) is a value,so the value-restricted intersection introduction can still be used in this case, and the programis still well-typed. In other words, the distributivity rule on function types can escape the value
restriction. Therefore, Davies and Pfenning remove distributivity (rule S-d) from subtyping. Without
distributivity, then the program is rejected.
While, with their restrictions, Davies and Pfenning obtain a type sound system, this comes at thecost of expressive power. In particular, we cannot adopt their restriction of removing distributivity
in subtyping in compositional programming. As we have seen in Section 2, distributivity plays afundamental role in CP to model nested composition, and enable a high degree of modularity. Thus
we take a different approach in our work, and propose a lighter restriction, which is able to retain
both distributivity and an unrestricted intersection introduction rule.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

Imperative Compositional Programming

3.3

342:13

Our Solution: Bidirectional Typing to the Rescue

While Davies and Pfenning identified intersection introduction and distributivity for the typeunsoundness problems, we believe that these features are not necessarily a problem. Indeed, we
can design a type system and calculus with references and both features, which is type sound.
One reason for the two counter-examples to exist is because expressions can infer multiple types.
This is expected in a type assignment system (TAS), which is often used to specify type systems.
For instance, in the TAS proposed by Davies and Pfenning, the expression 1 can have multiple
types, including Nat or Pos. However, implementations often cannot use a TAS, since a TAS may
not be syntax-directed and can guess types. Moreover, while a TAS is often specified without
type annotations, for many type systems (for instance those with undecidable type inference) wemust specify some annotations. Thus, implementations have to adopt other approaches, such as
bidirectional typing [Dunfield and Krishnaswami 2021]. For instance, in Davies and Pfenning’s
work, they adopt bidirectional typing for algorithmic typing.
For algorithmic typing and concrete implementations, we would expect that type inference ismore (if not completely) deterministic. We would usually expect that an inferred type is unique, andthat type annotations are needed in some parts of the program. In other words, we do not expect
to run the type checker twice on the same program and get different types; or to be able to type all
programs without type annotations (for many type systems, at least).
Our first observation is that with bidirectional typing, we can naturally require annotations,and avoid inference of multiple types for the same expression if necessary. For instance, for the
expression 1 we can infer the type Pos only. Nevertheless, with bidirectional typing, 1 can still bechecked against many types, including both Pos and Nat. If we want 1 to be of type Nat, then wecan, for instance, require a type annotation 1:Nat, and then 1 has type Nat via the check mode.
Our second, and most important observation, is that with bidirectional typing we can preventthe counter-examples by restricting the rule for typing references. In their algorithmic typing
formulation, Davies and Pfenning [2000] use the following checking rule for references:Σ; Γ ⊢ 𝑒 ⇐ 𝐴Σ; Γ ⊢ ref 𝑒 ⇐ Ref 𝐴
This rule allows ref 1 to be checked against both Ref Pos and Ref Nat, since 1 can be checkedwith both Pos and Nat. As such, their algorithmic typing, if unrestricted, can still type-check the
problematic programs in Figure 8. We propose instead to use the following rule:Σ; Γ ⊢ 𝑒 ⇒ 𝐴Σ; Γ ⊢ ref 𝑒 ⇒ Ref 𝐴
With this rule, both counter-examples (or other similar ones) are not typeable in the bidirectional
type systems proposed in this paper:• In the program in Figure 8a, intersection introduction cannot be used to type ref 1 with Ref
Pos & Ref Nat, since it would require checking ref 1 with Ref Nat. Because of our restrictedreference rule, ref 1 can only infer the type Ref Pos, and it is not possible to check ref 1
against Ref Nat. Using subsumption does not allow ref 1 to have type Ref Nat, since Ref Pos
is not a subtype of Ref Nat, due to the invariant subtyping rule for references (rule Sub-ref).
Thus, the program is not typeable.
• In the program in Figure 8b, because ref 1 infers Ref Pos, then the lambda 𝜆x.ref 1 in thesecond program cannot be checked by (Unit → Ref Nat) & (Unit → Ref Pos) or (Unit→ (Ref Nat & Ref Pos)). Therefore, the second program is not typeable either, even in thepresence of distributivity.
With this simple change on a bidirectional type system, we can have a type sound calculus with
distributive intersection subtyping, references, and an unrestricted intersection introduction rule.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:14

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira

Types
Expressions
Pre-Values
ValuesContexts
Value Stores
Typing Stores
Frames𝐴, 𝐵, 𝐶 F Pos | Nat | Unit | ⊤ | 𝐴 → 𝐵 | 𝐴&𝐵 | Ref 𝐴
𝑒 F 𝑥 | 𝑖 | unit | ⊤ | 𝜆𝑥 : 𝐴.𝑒 | 𝑒 : 𝐴 | 𝑒 1 𝑒 2 | 𝑜 | ref 𝑒 | !𝑒 | 𝑒 1 := 𝑒 2
𝑝 F unit | ⊤ | 𝑜 | 𝑖 | 𝜆𝑥 : 𝐴.𝑒𝑣 F 𝑝 : 𝐴 | 𝜆𝑥 : 𝐴.𝑒
Γ F · | Γ, 𝑥 : 𝐴
𝜇 F · | 𝜇, 𝑜 = 𝑣
Σ F · | Σ, 𝑜 : 𝐴
𝐹 F 𝑣 □ | □ 𝑒 | ref □ | !□ | 𝑣 := □ | □ := 𝑒Fig. 9. Syntax.

A complication is that we can no longer use a TAS and unannotated expressions to prove typesoundness directly. Our solution relies on bidirectional typing and the presence of type annotations.
Thus, we need to prove type soundness directly using a type system based on bidirectional typing.
Furthermore, the operational semantics needs to account for type annotations. Fortunately, there
are several calculi in the literature where type annotations are relevant and influence the resultof reduction [Fan et al. 2022; Garcia et al. 2016; Herman et al. 2010; Huang et al. 2021; Siek andWadler 2009; Wadler and Findler 2009]. These works provide techniques that are helpful to conduct
type soundness proofs in similar settings to the one that we have here. Thus, we can reuse some ofthose ideas, to create a calculus similar to Davies and Pfenning’s and show type soundness. As weshall see in Section 3.5, for this calculus (but not the one in Section 4), type annotations are still
computationally irrelevant and can be erased. Thus no overhead needs to be introduced at runtime.
3.4

Syntax and Type System

The calculus that we present next is similar to the one by Davies and Pfenning, but we directly
employ bidirectional typing. Since our goal is to illustrate how bidirectional typing can help to solve
the problematic interaction between distributive intersection types and references, we present a
simple type system, without a focus on maximizing type inference. We also make one simplificationin lambda abstractions, and allow only abstractions of the form 𝜆𝑥 : 𝐴.𝑒, with a single annotation
for the variable. This form is limiting for calculi with intersection types, since it forbids certain
forms of overloading such as 𝜆𝑥 .𝑥 : (Nat → Nat)&(Unit → Unit). To keep the full expressive
power of an intersection type system it is well-known that standard forms of type annotations
cannot work, and we must employ other forms of annotations [Pierce 1993; Reynolds 1997]. We
avoid the extra complexity of those solutions here. Nevertheless, our form of lambda abstractions
is still sufficient to encode the abstraction needed by the program in Figure 8b, which illustrates
the issues with distributivity.
Syntax. The syntax of our calculus is shown in Figure 9. Meta-variables 𝐴, 𝐵 and 𝐶 range overtypes. A type is either a positive number (Pos), a natural number (Nat), a unit type (Unit), a top
type (⊤) or a compound type. Compound types include arrow types (𝐴 → 𝐵), intersection types(𝐴&𝐵) and reference types (Ref 𝐴).
Meta-variable 𝑒 ranges over expressions. Most expressions are standard. For references, there arelocations (𝑜), reference expressions ref 𝑒, dereferences !𝑒 and reference assignments 𝑒 1 := 𝑒 2 . Values
𝑣 are pre-values with a type (𝑝 : 𝐴) and lambdas. Since there is no constructor for intersection types,
the annotation for values is used for preservation. For instance, to preserve types, 1 : Nat&Pos
should keep the annotations Nat&Pos, otherwise the preservation lemma would not hold. Ourcontexts Γ have bindings of term variables with their types (𝑥 : 𝐴). There are stores for values 𝜇
and types Σ. Value stores are bindings of reference locations with their values (𝑜 = 𝑣 ), while atype store contains bindings of reference locations with the type of values (𝑜 : 𝐴). We use context
evaluation, and the frames are standard.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

Imperative Compositional Programming

342:15𝐴◦, 𝐵 ◦ F Pos | Nat | Unit | ⊤ | Ref 𝐴 | 𝐴 → 𝐵 ◦⇔ F ⇒|⇐

Ordinary Types
Typing Modes(Subtyping)𝐴 <: 𝐵𝐴1 <: 𝐴◦3
S-refl

S-posi𝐴 <: 𝐴

Pos <: Nat
𝐵 <: 𝐴
𝐴 <: 𝐵𝐴 <: 𝐵 1
𝐴 <: 𝐵 2
𝐵1 ◁ 𝐵 ▷ 𝐵2

S-top

S-ref

𝐴 <: ⊤𝐵 ◁𝐴 ▷𝐶

𝐴1 → 𝐴2 <: 𝐵 1 → 𝐵 2◦

S-arr

𝐴2 <: 𝐴◦3
S-and

Ref 𝐴 <: Ref 𝐵

𝐴2 <: 𝐵 2◦

𝐵 1 <: 𝐴1

S-andl
𝐴1 & 𝐴2 <: 𝐴◦3

S-andr
𝐴1 & 𝐴2 <: 𝐴◦3(Type Splitting)𝐴 <: 𝐵𝐶 ◁𝐵▷𝐷
Sp-andSp-arrow
𝐴 →𝐶 ◁𝐴 →𝐵 ▷𝐴 →𝐷

𝐴 ◁ 𝐴&𝐵 ▷ 𝐵
Σ; Γ ⊢ 𝑒 ⇔ 𝐴(Bidirectional Typing)Σ; Γ ⊢ ⊤ ⇒ ⊤ITyp-topΣ; Γ ⊢ unit ⇒ Unit

ITyp-unit

Σ; Γ ⊢ i ⇒ Pos

ITyp-posΣ; Γ ⊢ x ⇒ 𝐴Σ; Γ ⊢ 𝑒 1 ⇒ 𝐴1 → 𝐴2

Σ; Γ ⊢ o ⇒ Ref 𝐴

Σ; Γ ⊢ !𝑒 ⇒ 𝐴

ITyp-subITyp-anno

Σ; Γ ⊢ 𝑒 2 ⇐ 𝐴

Σ; Γ ⊢ 𝑒 1 := 𝑒 2 ⇒ Unit

𝐵1 ◁ 𝐵 ▷ 𝐵2

𝐴 <: 𝐵Σ; Γ ⊢ 𝑒 ⇐ 𝐵Σ; Γ ⊢ 𝑒 : 𝐴 ⇒ 𝐴

Σ; Γ ⊢ 𝑒 ⇒ Ref 𝐴
ITyp-abst

ITyp-abs

Σ; Γ ⊢ 𝑒 ⇐ 𝐴
ITyp-app

ITyp-loc

Σ; Γ, x : 𝐴 ⊢ 𝑒 ⇐ ⊤Σ; Γ ⊢ 𝑒 ⇒ 𝐴Σ; Γ ⊢ 𝜆x : 𝐴1 . 𝑒 ⇐ 𝐴2 → 𝐵

Σ; Γ ⊢ 𝑒 1 ⇒ Ref 𝐴

o:𝐴 ∈ ΣΣ; Γ ⊢ 𝜆x : 𝐴. 𝑒 ⇐ ⊤ITyp-varΣ; Γ ⊢ 𝑒 2 ⇐ 𝐴1

Σ; Γ ⊢ 𝑒 1 𝑒 2 ⇒ 𝐴2

ITyp-lit

𝐴2 <: 𝐴1
Σ; Γ, x : 𝐴1 ⊢ 𝑒 ⇐ 𝐵

x :𝐴 ∈ Γi>0Σ; Γ ⊢ 0 ⇒ Nat

ITyp-ass

Σ; Γ ⊢ 𝑒 ⇒ 𝐴
ITyp-deref
Σ; Γ ⊢ 𝑒 ⇐ 𝐵 1
Σ; Γ ⊢ 𝑒 ⇐ 𝐵Σ; Γ ⊢ ref 𝑒 ⇒ Ref 𝐴

ITyp-refΣ; Γ ⊢ 𝑒 ⇐ 𝐵 2
ITyp-intro

Fig. 10. Type system.

Subtyping. The subtyping rules are shown at the top of Figure 10. The subtyping relation is avariant of the standard BCD-style distributive subtyping relation [Barendregt et al. 1983], and issimilar to the one employed by Davies and Pfenning. However, we choose a presentation for therules based on the work by Huang et al. [2021], which employs splittable types and ordinary types.
Ordinary types [Davies and Pfenning 2000; Huang et al. 2021], represented as 𝐴◦ , are types thatare not intersections or function types returning intersections. The opposite to ordinary types are
splittable types, which are types that are intersections or function types returning intersections.
Splittable types can be decomposed, unlike ordinary types, and they are helpful to eliminate theneed for an explicit transitivity rule. Splittable types, along with ordinary types, are also helpful for
obtaining an algorithmic formulation, as well as developing the metatheory of subtyping.
Ordinary and splittable types remove some overlap between the rules for intersection types.
When an intersection appears on the right (𝐴 <: 𝐵&𝐶), we know that we never lose expressive powerby employing rule S-and so, we can always pick this rule instead of the other two intersection
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:16

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira

𝜇; 𝑒 ↦−→ 𝜇 ′ ; 𝑒 ′(Small-Step Semantics)′

𝜇; 𝑒 ↦−→ 𝜇 ; 𝑒

′

′

o∉𝜇
′

IStep-eval

𝜇; 𝐹 [𝑒] ↦−→ 𝜇 ; 𝐹 [𝑒 ]IStep-ref𝜇; ref 𝑣 ↦−→ 𝜇, o = 𝑣; oo=𝑣 ∈ 𝜇𝑒 ≠𝑝
IStep-deref𝜇; !(o : Ref 𝐴) ↦−→ 𝜇; 𝑣 : 𝐴

𝜇; 𝑒 ↦−→ 𝜇 ′ ; 𝑒 ′𝜇; 𝑒 : 𝐴 ↦−→ 𝜇 ′ ; 𝑒 ′ : 𝐴

IStep-annoo =𝑝 :𝐶 ∈ 𝜇
IStep-ass
𝜇; o : Ref 𝐴 := 𝑣 ↦−→ 𝜇 [o ↦→ |𝑣 | : 𝐶]; unit

IStep-annov
𝜇; 𝑝 : 𝐴 : 𝐵 ↦−→ 𝜇; 𝑝 : 𝐵

IStep-p
𝜇; 𝑝 ↦−→ 𝜇; 𝑝 : ty(𝑝) 𝜇IStep-beta𝜇; (𝜆x : 𝐴1 . 𝑒 : 𝐵 1 → 𝐵 2 ) 𝑣 ↦−→ 𝜇; 𝑒 [x ↦→ |𝑣 | : 𝐴1 ] : 𝐵 2
Fig. 11. Reduction.

rules. Thus, the ordinary condition expresses that in the two other rules (rules S-andl and S-andr)
the type on the right cannot be an intersection. So, the other rules will not apply in cases whereintersections appear on the right. In a setting with distributive subtyping, we need to generalize
the definition of ordinary types a bit more because 𝐴 → 𝐵&𝐶 is equivalent to (𝐴 → 𝐵)&(𝐴 → 𝐶).
So function types such as those should be considered as non-ordinary (or splittable). Ordinary andsplittable types also help in proving inversion lemmas about the subtyping relation, which areneeded for the type soundness proof. Usually, in subtyping relations with less overlapping rules, it
becomes easier to prove inversion lemmas.
Types are split in rule S-and by the type splitting relation 𝐵 ◁ 𝐴 ▷ 𝐶, which is shown in the
middle of Figure 10. An intersection type 𝐴&𝐵 is split into 𝐴 and 𝐵. An arrow type is split by
the output type. The rule S-d rule is admissible from rule S-and [Huang et al. 2021]. Rules S-arr,
S-andl, and S-andr are for ordinary types. The subtyping rule S-ref for references is standard: it
compares two reference types and requires that both types are subtypes of each other. Note that
Ref (𝐴&𝐵) is not equivalent to (Ref 𝐴)&(Ref 𝐵), and that reference types are unsplittable. In otherwords, there is no distributivity rule for references. The subtyping rules are reflexive and transitive.
Type system. The bidirectional type system is shown at the bottom of Figure 10. The typing
judgement is represented as Σ; Γ ⊢ 𝑒 ⇔ 𝐴. There are two typing modes ⇔: infer mode (⇒) andcheck mode (⇐), shown at the top of Figure 10. An expression 𝑒 is inferred or checked by type 𝐴
under the reference typing store Σ and term variable context Γ. Most rules are standard. As wediscussed, for references, expressions must infer a type (rule ITyp-ref). Because of distributivity,
the intersection introduction rule requires type splitting. Lambdas are checked by ⊤ or a function
type 𝐴2 → 𝐵 if 𝐴2 is the subtype of the lambda input type 𝐴1 and the body is checked by 𝐵.
3.5

Dynamic Semantics

Figure 11 shows the reduction rules of our calculus. We have two variants of reduction. Onevariant has type annotations, which are needed to prove type soundness. The other variant has
no annotations and is used to illustrate that annotations are computationally irrelevant in thiscalculus.
Reduction with annotations. Rule IStep-eval reduces the expressions under the frames. Rule IStepp reduces inferrable raw values to be values by annotating their types (ty(𝑝) 𝜇 ). The definition for
inferrable raw values is:ty(⊤) 𝜇 = ⊤ty(unit) 𝜇 = Unitty(𝑜) 𝜇 = Ref ty(𝜇 (𝑜)) 𝜇ty(0) 𝜇 = Nat

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

ty(i) 𝜇 = Pos (i > 0)

Imperative Compositional Programming

342:17Rule IStep-anno is applied for annotations and 𝑒 cannot be a pre-value 𝑝. Annotations are notincluded in the evaluation context because there is a side condition stating that 𝑒 is not a 𝑝. The side
condition is needed to avoid rule IStep-anno and rule IStep-p creating a cycle. Rule IStep-annov
replaces the annotation for a value. Rule IStep-beta substitutes argument values by replacing theannotated type with the input type of lambdas after erasing the outer annotation. The result of beta
reduction is annotated by the output type of the function. Since values include annotated values
and lambdas, |𝑣 | erases the annotation of annotated values but returns lambdas themselves. So,after annotating the input type of functions, the argument is still a value. Similarly, rule IStepass replaces new values with the type of old values in the store before updating. Rule IStep-ref
generates a fresh location and stores the reference values. Rule IStep-deref gets the values in thestore. Importantly, our calculus is proved to be type sound by the usual progress (Theorem 3.1) andpreservation (Theorem 3.2) theorems.
Theorem 3.1 (Progress). If Σ; · ⊢ 𝑒 ⇔ 𝐴 and Σ ⊢ 𝜇 then either 𝑒 is a value or ∃ 𝑒 ′ 𝜇 ′ , 𝜇; 𝑒 ↦−→ 𝜇 ′ ; 𝑒 ′ .
Theorem 3.2 (Type preservation). If Σ; · ⊢ 𝑒 ⇔ 𝐴, Σ ⊢ 𝜇, and 𝜇; 𝑒 ↦−→ 𝜇 ′ ; 𝑒 ′ then ∃ Σ′ ⊇ Σ,

Σ′ ; · ⊢ 𝑒 ′ ⇔ 𝐴 and Σ′ ⊢ 𝜇 ′ .

Type annotations are computationally irrelevant. We show an alternative dynamic semantics,
without annotations in the extended version of the paper. The rules are standard. Importantly,
we show that dynamic semantics with annotations reduces to the same values as the dynamic
semantics without annotations (Theorem 3.3). The erase functions |𝑒 | and |Σ | remove annotations
from expressions and values of typing stores. To be distinguishable, we use the subscript |i| torepresent the dynamic semantics without annotations.
Theorem 3.3 (Type annotations are computationally irrelevant). If 𝜇; 𝑒 ↦−→∗ 𝜇 ′ ; 𝑣 then|𝜇 |; |𝑒 | ↦−→∗|i| |𝜇 ′ |; |𝑣 |.
4+ Calculus: Extending 𝐹 + with References
The 𝐹 imi

+ calculus: a variant and extension of the 𝐹 + calculus [Fan et al.
In this section, we introduce the 𝐹 imi2022] with references. This calculus is the core language employed by our implementation of CP+ calculus employs bidirectional typing and adopts the restriction proposedwith references. The 𝐹 im
+ includes several other features, including the merge operator [Dunfieldin Section 3. In addition, 𝐹 im
2014; Reynolds 1997], and disjoint polymorphism [Alpuim et al. 2017], which are inherited from 𝐹 i+ .
Note that disjoint polymorphism is a form of parametric polymorphism where type variables canhave disjointness constraints.

4.1

Syntax+ is shown in Figure 12. Many of the syntactic forms are the same as the calculus
The syntax of 𝐹 im
in Section 3, but we have a few new constructs.

Types and expressions. Types are extended with a type variable (𝑋 ), single field record types({𝑙 : 𝐴}) and disjoint polymorphic quantification [Alpuim et al. 2017] (∀𝑋 ∗ 𝐴.𝐵). With disjoint
polymorphism, disjointness constraints like ∀𝑋 ∗ 𝐴 express that the type that instantiates 𝑋 must
be disjoint to the type 𝐴. This form of constraint is similar to absence constraints seen in row
polymorphic calculi [Cardelli and Mitchell 1989; Harper and Pierce 1991; Leijen 2005; Shields and
Meijer 2001], except that disjoint polymorphism accounts for subtyping. Ordinary types also include
records with ordinary fields and polymorphic types with ordinary type bodies. The type of numbers
is simplified to be only an integer type Int. Expressions are extended with merge expressions(𝑒 1 , 𝑒 2 ), record projections (𝑒 .𝑙), and expressions for polymorphism. Merges can be used to encode
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:18

Types
Ordinary Types
Expressions
Functionals
Pre-Values
ValuesContexts
Value Stores
Typing Stores
Application Arguments
FramesWenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira

𝐴, 𝐵, 𝐶 F Int | Unit | ⊤ | 𝐴 → 𝐵 | 𝐴&𝐵 | Ref 𝐴 | 𝑋 | {𝑙 : 𝐴} | ∀𝑋 ∗ 𝐴.𝐵
𝐴◦, 𝐵 ◦, 𝐶 ◦ F Int | Unit | ⊤ | 𝑋 | Ref 𝐴 | 𝐴 → 𝐵 ◦ | {𝑙 : 𝐴◦ } | ∀𝑋 ∗ 𝐴.𝐵 ◦𝑒 F 𝑥 | 𝑖 | unit | ⊤ | 𝜆𝑥 .𝑒 | 𝑒 : 𝐴 | 𝑒 1 𝑒 2 | 𝑜 | ref 𝑒 | !𝑒 | 𝑒 1 := 𝑒 2| 𝑒 1 , 𝑒 2 | {𝑙 = 𝑒 } | 𝑒 .𝑙 | Λ𝑋 .𝑒 | 𝑒 𝐴
𝑓 F (𝜆𝑥 .𝑒) : 𝐴 → 𝐵 | 𝑓 : 𝐴 → 𝐵
𝑝 F 𝑜 | Λ𝑋 .𝑒𝑣 F 𝑝 : 𝐴 | 𝑓 | unit | ⊤ | 𝑖 | 𝑣 1 , 𝑣 2 | {𝑙 = 𝑣 }Γ F · | Γ, 𝑥 : 𝐴 | Γ, 𝑋 ∗ 𝐴
𝜇 F · | 𝜇, 𝑜 = 𝑣
Σ F · | Σ, 𝑜 : 𝐴
arg F 𝑣 | 𝐴 | 𝑙
𝐹 F 𝑣 □ | □ 𝑒 | □ : 𝐴 | ref □ | !□ | 𝑣 := □ | □ := 𝑒
| 𝑣 , □ | □ , 𝑒 | □.𝑙 | {𝑙 = □} | □ 𝐴+ calculus.
Fig. 12. The syntax of the 𝐹 im

multiple field records with single field records ({𝑙 = 𝑒 }) [Reynolds 1997]. For polymorphism, we
have type abstractions (Λ𝑋 .𝑒) and type applications (𝑒 𝐴).
Values, application arguments and contexts. Because we prove type preservation using a bidi+ has to account for type annotations, our form of values requires
rectional type system, and 𝐹 imsome non-standard forms to ensure that enough type information is preserved on values, andthroughout the reduction process. For instance, if 𝑣 : 𝐴 reduces to 𝑣 , simply forgetting about the
annotation, this would be ok in terms of the runtime behavior (for the calculus in Section 3.5), butwould not be ok for preservation. An example would be (𝜆𝑥 .𝑥) : Int → Int reducing to 𝜆𝑥 .𝑥. After
doing this reduction, we would not be able to type check the resulting term using the bidirectional
typing rules. Thus, we would not be able to prove type preservation. Therefore, values need tohave sufficient annotations and reductions like the above should not be allowed.
We employ a form of values similar to those adopted in approaches based on type-directed
operational semantics [Fan et al. 2022; Huang et al. 2021]. A functional value (𝑓) is a lambda
expression with one or more arrow types. Pre-values 𝑝 are locations and type abstractions. A
value 𝑣 can be an annotated pre-value (𝑝 : 𝐴), a functional value, a top value ⊤, an integer
value 𝑖, a merge of values or a record value (𝑣 1 , 𝑣 2 ). The value form (𝑝 : 𝐴) is just a simple
way to ensure sufficient annotations, but we could inline and/or simplify the definition of values,at the cost of making some rules more complicated. Furthermore, consider a function with two
annotations (𝜆𝑥 .𝑒) : Int → Int : (Int&Bool) → ⊤. If we want to preserve types, we must retain(Int&Bool) → ⊤. However, for the runtime behavior, we must make sure that the argument is cast
to Int before reduction. Thus we must also retain the inner input type Int. A very similar issue
occurs in gradually typed languages, for essentially similar reasons: we wish to have preservation
but, at the same time, types can have an effect on reduction and must be preserved for that effectto be enforced. In the work of Wadler and Findler [2009], they solve this problem by accumulating
annotations of lambdas. We adopt a similar solution too. The only difference is that we syntactically
capture that functional values can only be a lambda followed by annotations using the syntactic
category 𝑓. Overall, these value categories help to simplify the presentation.
Values, types and projection labels can also be the argument of parallel elimination (discussed
in Section 4.3). Thus, we have a syntactic category for application arguments. Our contexts Γ areextended with bindings of type variables with their disjoint types (𝑋 ∗ 𝐴). Frames are augmented
with merges, records, projections and type applications as well as annotations.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

Imperative Compositional Programming

342:19(Extended Subtyping)𝐴 <: 𝐵𝐵 1 <: 𝐵 2◦

𝐴2 <: 𝐴1
S-var

𝐴 <: 𝐵 ◦S-rcd{l : 𝐴} <: {l : 𝐵 ◦ }(Extended Type Splitting)

S-forall∀X ∗ 𝐴1 . 𝐵 1 <: ∀X ∗ 𝐴2 . 𝐵 2◦

X <: X𝐵 ◁𝐴 ▷𝐶𝐶 ◁𝐵▷𝐷

𝐵 ◁𝐴 ▷𝐶
Sp-forallSp-rcd∀X ∗ 𝐴. 𝐶 ◁ ∀X ∗ 𝐴. 𝐵 ▷ ∀X ∗ 𝐴. 𝐷

{l : 𝐵} ◁ {l : 𝐴} ▷ {l : 𝐶}𝐴 ∗ax 𝐵

(Disjointness Axioms for References)
Dax-refInt

Dax-Intref

Ref 𝐴 ∗ax Int

Dax-Arrref

Int ∗ax Ref 𝐴

𝐴1 → 𝐴2 ∗ax Ref 𝐴

Dax-allref

Dax-refrcd∀X ∗ 𝐴. 𝐵 ∗ax Ref 𝐴

Dax-rcdref

Ref 𝐴 ∗ax {l : 𝐵}{l : 𝐵} ∗ax Ref 𝐴
Dax-refall

Dax-refarr
Ref 𝐴 ∗ax 𝐴1 → 𝐴2

Ref 𝐴 ∗ax ∀X ∗ 𝐴. 𝐵

Γ⊢𝐴 ∗𝐵

Unit ∗ax Ref 𝐴

Dax-refu
Ref 𝐴 ∗ax Unit

Dax-uref𝐴 ∗ax 𝐵
Γ ⊢𝐴∗𝐵𝐴1 ◁ 𝐴 ▷ 𝐴2

⌉𝐴⌈
D-ax
Γ ⊢ 𝐴1 ∗ 𝐵

Γ ⊢ 𝐴 ∗ 𝐵1

D-andLΓ ⊢ {l : 𝐴} ∗ {l : 𝐵}
X ∗𝐴 ∈ Γ

D-andR𝐴 <: 𝐵

D-refΓ ⊢ Ref 𝐴 ∗ Ref 𝐵(Top-Like Types)

D-for

⌉𝐴 ⌈
⌉𝐴⌈

⌉𝐵 ⌈

⌉⊤⌈

⌉𝐵 ⌈
TL-and⌉𝐴 & 𝐵 ⌈D-varlΓ ⊢𝐴∗𝐵Γ ⊢ ∀X ∗ 𝐴1 . 𝐵 1 ∗ ∀X ∗ 𝐴2 . 𝐵 2

TL-topD-rcdeqΓ ⊢ X ∗𝐵

Γ, X ∗ 𝐴1 & 𝐴2 ⊢ 𝐵 1 ∗ 𝐵 2
D-varr

D-topRΓ ⊢𝐴∗𝐵Γ ⊢ 𝐴 ∗ 𝐵2

𝐴 <: 𝐵Γ ⊢𝐵∗XΓ ⊢𝐴∗𝐵Γ ⊢ 𝐴2 ∗ 𝐵

Γ ⊢𝐴∗𝐵X ∗𝐴 ∈ Γ⌉𝐵 ⌈D-topLΓ ⊢𝐴∗𝐵Γ ⊢𝐴∗𝐵𝐵1 ◁ 𝐵 ▷ 𝐵2

(Disjointness)⌉𝐵 ⌈TL-arr

TL-forall⌉𝐴 → 𝐵 ⌈⌉𝐴⌈⌉∀X ∗ 𝐴. 𝐵 ⌈⌉𝐴⌈

TL-rcd⌉{l : 𝐴}⌈

TL-ref⌉Ref 𝐴⌈

Fig. 13. Subtyping and disjointness (excerpt).

4.2

Subtyping and Disjointness

The extended subtyping rules are shown at the top of Figure 13. New rules S-var, S-forall, andS-rcd are for type variables, polymorphic types and record types. Importantly, extended subtyping
is still proved to be reflexive and transitive (Lemma 4.1 and Lemma 4.2).
Lemma 4.1 (Reflexivity of subtyping). 𝐴 <: 𝐴.
Lemma 4.2 (Transitivity of subtyping). If 𝐴 <: 𝐵 and 𝐵 <: 𝐶 then 𝐴 <: 𝐶.
Disjointness is shown in Figure 13. Disjoint intersection types were proposed by Oliveira et al.
[2016] to solve the ambiguity problem of merging expressions such as 1 and 2. In general, in calculi
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:20

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveirawith a merge operator, disjointness of two types ensures that two types cannot have supertypes
in common, except for top-like types. We extend the disjointness of 𝐹 i+ with reference types. The
rule D-ax shows that two different structural types are disjoint, and relies on an auxiliary relation
𝐴 ∗ax 𝐵. This relation captures simple disjointness axioms, such as an integer is disjoint to a function.
The different structural types 𝐴 ∗ax 𝐵 for references are defined in the middle of Figure 13, while
the full rules are shown in the extended version of the paper. The main disjointness relation has
rules that deal with compound types, such as intersection types or records. Note that rules D-topL
and D-topR have a special treatment for top-like types, which are shown at the bottom of Figure 13.
Top-like types are disjoint to any type because they do not overlap with other types. Top-liketypes arise in calculi with merges and disjoint intersection types, and are covered in detail inprevious works [Huang 2023; Oliveira et al. 2016]. They are helpful to achieve determinism (seealso Section 4.4). With the disjointness relation, we know, for example, that Int is not disjoint with
Int&Bool, since Int is not disjoint with Int. Then Ref (Int&Bool) and Ref Int would not be disjoint
either.
4.3

Bidirectional Typing

For typing, similarly to 𝐹 i+ and the simplified system in Section 3, we use bidirectional typing. As
explained by Huang et al. [2021] and Oliveira et al. [2016], a general subsumption rule can stillcause ambiguity problems in the presence of the merge operator. For instance, 1 , True can havetype Bool and 2 can have type Int, but if we merge these two expressions, ambiguity is introduced.
Bidirectional typing avoids the ambiguity problem by using the weaker bidirectional subsumption
rule. For 1 , True, we can infer the type Int&Bool. However, we can check the same term with type
Bool and Int.
Moreover, types in programs should always be well-formed. The well-formedness relation isdefined at the top of Figure 14. Type Int and ⊤ are well-formed. Arrow types, reference types andrecord types are well-formed if all their subcomponents are well-formed. The interesting casehappens with intersection types 𝐴&𝐵: an intersection type is well-formed when types 𝐴 and 𝐵
are well-formed, and these types are disjoint (rule wel-and). If a type variable 𝑋 is bound to a
type in the context then it is well-formed (rule wel-x). Our design is based on the original work
on disjoint intersection types [Oliveira et al. 2016], which has a similar restriction. The work on
𝐹 i+ [Fan et al. 2022], avoids this restriction but, as we shall discuss in Section 5, in the presence ofreferences avoiding this restriction creates important technical difficulties.
+ . Compared to the calculus in Section 3, there
Typing. Figure 14 shows the typing rules of 𝐹 im
are annotations for locations 𝑜 (rule Typ-loc). This design choice is essentially similar to what
happens in the work with gradual typing and references [Toro and Tanter 2020]. In their work,
reference values have a similar annotated form for references. An annotated reference type Ref 𝐵
should always be a supertype of the reference type in the store Ref 𝐴. If there is no annotation,
values in the store would need to be cast every time to preserve types. This alternative design
would be significantly more complicated, since value stores should be considered during casting.
For example, let’s assume we have a value of 1 in the store, located at 𝑜, and this 𝑜 is annotatedwith type Ref (Int&⊤) (i.e., 𝑜 : (Ref Int&⊤)). To preserve the type we would need to cast values inthe store to have type Int&⊤. However, if we keep one type annotation for 𝑜, there is no need tocast the value in the store. Consequently, stores do not need to be updated every time. We delve
into a more detailed discussion about the complexities and difficulties that arise if stores are carried
everywhere at runtime in Section 4.4.

Applicative distribution. In rules Typ-app, Typ-prj, and Typ-tapp, there is an applicative distribution relation 𝐴 ▷ 𝐵, which increases the flexibility of typing, and is shown at the bottom ofProc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

Imperative Compositional Programming

342:21Γ⊢𝐴(Well-Formed Types)
Γ⊢𝐴

Γ⊢⊤

wel-topΓ ⊢ UnitΓ⊢𝐴

wel-unitΓ⊢𝐴Γ ⊢ Ref 𝐴Γ⊢𝐵

wel-ref

Σ; Γ ⊢ ⊤ ⇒ ⊤Γ⊢𝐴Σ; Γ ⊢ 𝑒 ⇒ 𝐴

Γ ⊢ {l : 𝐴}Σ; Γ ⊢ unit ⇒ Unit

x :𝐴 ∈ Γ

Typ-unitΓ⊢𝐴
Typ-varΣ; Γ ⊢ x ⇒ 𝐴

Typ-prj

Typ-appΣ; Γ ⊢ 𝑒 : 𝐴 ⇒ 𝐴

Σ; Γ ⊢ {l = 𝑒} ⇒ {l : 𝐴}Σ; Γ ⊢ 𝑒 ⇒ 𝐴Γ⊢𝐴
Typ-ref

Typ-rcd

Σ; Γ ⊢ 𝑒 ⇒ Ref 𝐴
Typ-ass

Σ; Γ ⊢ 𝑒 1 := 𝑒 2 ⇒ Unit

Typ-anno

Σ; Γ ⊢ 𝑒 ⇒ 𝐴
Typ-locΣ; Γ ⊢ 𝑒 2 ⇐ 𝐴

Σ; Γ ⊢ !𝑒 ⇒ 𝐴

Typ-deref

Σ; Γ, X ∗ 𝐴 ⊢ 𝑒 ⇐ 𝐵Σ; Γ ⊢ ΛX . 𝑒 : ∀X ∗ 𝐴. 𝐵 ⇒ ∀X ∗ 𝐴. 𝐵Γ⊢𝐴
𝐵 ▷ ∀X ∗ 𝐵 1 . 𝐵 2
Γ ⊢ 𝐴 ∗ 𝐵1
Σ; Γ ⊢ 𝑒 ⇒ 𝐵Σ; Γ ⊢ 𝑒 𝐴 ⇒ 𝐵 2 [X ↦→ 𝐴]

Typ-abs

Σ; Γ ⊢ 𝑒 ⇐ 𝐴Σ; Γ ⊢ o : Ref 𝐵 ⇒ Ref 𝐵

Σ; Γ ⊢ ref 𝑒 ⇒ Ref 𝐴

Σ; Γ, x : 𝐴 ⊢ 𝑒 ⇐ 𝐵

Ref 𝐴 <: Ref 𝐵

Σ; Γ ⊢ 𝑒 1 ⇒ Ref 𝐴

Typ-litΣ; Γ ⊢ i ⇒ Int

Σ; Γ ⊢ 𝑒 1 𝑒 2 ⇒ 𝐴2

Typ-mergeΣ; Γ ⊢ 𝑒 1 , 𝑒 2 ⇒ 𝐴 & 𝐵
o:𝐴 ∈ Σ(Bidirectional Typing)Σ; Γ ⊢ 𝑒 1 ⇒ 𝐴
Σ; Γ ⊢ 𝑒 2 ⇐ 𝐴1
𝐴 ▷ 𝐴1 → 𝐴2

Σ; Γ ⊢ 𝑒 1 ⇒ 𝐴
Σ; Γ ⊢ 𝑒 2 ⇒ 𝐵
Γ ⊢𝐴∗𝐵Γ⊢𝐵

wel-rcd

Σ; Γ ⊢ 𝜆x. 𝑒 : 𝐴 → 𝐵 ⇒ 𝐴 → 𝐵

𝐴 ▷ {l : 𝐵}Σ; Γ ⊢ 𝑒.l ⇒ 𝐵

wel-X

Γ⊢X

Γ⊢𝐴
wel-all

Typ-topwel-arrow

X ∗𝐴 ∈ Γ
wel-andΓ, X ∗ 𝐴 ⊢ 𝐵Γ ⊢ ∀X ∗ 𝐴. 𝐵

Γ⊢𝐵

Γ⊢𝐴→𝐵

Γ ⊢𝐴∗𝐵Γ ⊢ 𝐴&𝐵

Γ⊢𝐴Σ; Γ ⊢ 𝑒 ⇔ 𝐴

wel-intΓ ⊢ Int

Σ; Γ ⊢ 𝑒 ⇒ 𝐴
Typ-tapp

𝐴 <: 𝐵

Typ-tabsΓ⊢𝐵
Typ-subΣ; Γ ⊢ 𝑒 ⇐ 𝐵(Applicative Distribution)

𝐴 ▷𝐵
𝐴 ▷ 𝐴1 → 𝐴2

𝐵 ▷ 𝐴1 → 𝐵 2

apd-refl

apd-andarr
𝐴 & 𝐵 ▷ 𝐴1 → 𝐴2 & 𝐵 2

𝐴 ▷ 𝐴
𝐴 ▷ ∀X ∗ 𝐴1 . 𝐴2

𝐵 ▷ ∀X ∗ 𝐵 1 . 𝐵 2

𝐴 ▷ {l : 𝐴1 }𝐵 ▷ {l : 𝐵 1 }apd-andall
𝐴 & 𝐵 ▷ ∀X ∗ (𝐴1 & 𝐵 1 ). (𝐴2 & 𝐵 2 )apd-andrcd

𝐴 & 𝐵 ▷ {l : 𝐴1 & 𝐵 1 }+ .
Fig. 14. Type system of 𝐹 im

Figure 14. This relation reflects the subtyping (and distributivity rules) in function application andrecord projection. Normally, rule Typ-app should only allow 𝐴 to be a function type. However,
due to subtyping, we additionally allow intersections of function types to act as a function. For
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:22

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira

𝐴⪅𝐵(Isomorphic Subtyping)𝐴 ⪅ 𝐵
IS-refl𝐴 ⪅ 𝐵
IS-ref

𝐴1 ⪅ 𝐵 1

𝐴2 ⪅ 𝐵 2

IS-rcd{l : 𝐴} ⪅ {l : 𝐵}

Ref 𝐴 ⪅ Ref 𝐵

𝐴 ⪅ 𝐴

𝐵1 ◁ 𝐵 ▷ 𝐵2
IS-and𝐴1 & 𝐴2 ⪅ 𝐵
Fig. 15. Isomorphic subtyping.

example, suppose that 𝐴 is (Int → Int)&(Bool → Bool). Since 𝐴 is a subtype of both (Int → Int)and (Bool → Bool) it can act as any of these 2 functions, and the application should be allowed
provided that a compatible argument type is provided. Similar handling happens in rule Typ-tappand rule Typ-prj. Note that, in rule apd-andarr the two distributed function types should havethe same input type. Unlike output types, input types cannot be intersected. Otherwise, we would
generate types that are not well-formed. For instance, (Int → Int)&(Int → Bool) can be matchedas (Int&Int) → (Int&Bool), but Int&Int is not well-formed. Other typing rules are similar to 𝐹 i+ .
The typing rules infer unique types (Lemma 4.4). Furthermore, types that can be used to infer orcheck expressions must be well-formed (Lemma 4.3). Lemma 4.5 shows that if an expression can bechecked by one type, then it can also be checked by a supertype.
Lemma 4.3 (Well-formedness of typing). If Σ; Γ ⊢ 𝑒 ⇔ 𝐴 then Γ ⊢ 𝐴.
Lemma 4.4 (Uniqeness of type inference). If Σ; Γ ⊢ 𝑒 ⇒ 𝐴1 and Σ; Γ ⊢ 𝑒 ⇒ 𝐴2 then 𝐴1 = 𝐴2 .
Lemma 4.5 (Subsumption of type checking). If Σ; Γ ⊢ 𝑒 ⇐ 𝐴 and 𝐴 <: 𝐵 then Σ; Γ ⊢ 𝑒 ⇐ 𝐵.
Store typing. In the dynamic semantics, types should be split first and then values are cast under
the split types in parallel. Thus we are not using the syntactic equality of types. Instead, we use a
restricted form of equivalent types called isomorphic subtyping [Fan et al. 2022], which is shownin Figure 15. Lemma 4.7 shows that if two types are in an isomorphic subtyping relation then they
are equivalent.
With the help of typing and isomorphic subtyping, we define the relation between value andtype stores. Definition 4.6 defines well-formed stores (𝜇) with respect to the typing locations Σ:Definition 4.6 (Well-formedness of the store with respect to Σ). Σ ⊢ 𝜇 ≜ if 𝑑𝑜𝑚(𝜇) = 𝑑𝑜𝑚(Σ) then∀𝑜 ∈ 𝜇, Σ; · ⊢ 𝜇 (𝑜) ⇒ 𝐴 and 𝐴 ⪅ Σ (𝑜).
A store is well-formed with the typing location if the store and the typing location contain thesame domains. For each location, which is in the store, the bounded value 𝜇 (𝑜) can be inferredwith a type, which is an isomorphic subtype of the type bound in the typing location (Σ (𝑜)).
Lemma 4.7 (Isomorphic subtyping). If 𝐴 ⪅ 𝐵 then 𝐴 <: 𝐵 and 𝐵 <: 𝐴.
4.4

Dynamic Semantics

We employ a type-directed operational semantics (TDOS) [Huang et al. 2021] for the dynamic
semantics. Following the TDOS approach, our dynamic semantics consists of two parts: casting
and reduction. Moreover, small-step reduction uses an auxiliary parallel elimination relation.
Our subtyping is essentially coercive, and casting implements coercions in the operationalsemantics provided a type as the casting target, which is why we use the term type-directed
operational semantics. As a result, types cannot be erased at runtime because casting relies ontypes. The simplest way to trigger casting is with an explicit type annotation like (1 , True) : Int
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

Imperative Compositional Programming

342:23𝑣 ↦−→𝐴 𝑣 ′(Casting)◦⌉𝐴 ⌈𝑣 ↦−→𝐴◦ TV(𝐴◦ )cast-top

cast-icast-uniti ↦−→Int i¬⌉𝐴 → 𝐵 ◦ ⌈unit ↦−→Unit unit
𝐵 <: 𝐶 ◦f ↦−→𝐴→𝐵 ◦ f : 𝐴 → 𝐵◦ cast-f¬⌉𝐶 ◦ ⌈

𝑝 : 𝐵 ↦−→𝐶 ◦ 𝑝 : 𝐶 ◦𝑣 ↦−→𝐴◦ 𝑣 ′cast-anno𝑣 1 ↦−→𝐴◦ 𝑣 1′

cast-rcd{l = 𝑣 } ↦−→ {l:𝐴◦ } {l = 𝑣 ′ }𝑣 2 ↦−→𝐴◦ 𝑣 2′

𝑣 1 , 𝑣 2 ↦−→𝐴◦ 𝑣 1′
𝑣 ↦−→𝐵 𝑣 1

𝐵 ◁𝐴 ▷𝐶

cast-merger
𝑣 1 , 𝑣 2 ↦−→𝐴◦ 𝑣 2′

cast-mergel𝑣 ↦−→𝐶 𝑣 2
cast-and𝑣 ↦−→𝐴 𝑣 1 , 𝑣 2+ .
Fig. 16. Casting of 𝐹 im

(which will trigger casting and return the value 1). Another example is function application:((𝜆𝑥 .𝑥 + 1) : Int → Int) (1 , True)
The argument will be cast (or coerced) from (1 , True) to 1 before addition (+1). This kind of casting(or coercion) is vital because of a semantic ambiguity issue. This issue arises when the merge
operator interacts with subtyping, and it has been identified by Cardelli and Mitchell [1989]. Let us
see an example in CP:
let f (r: {x : Bool}) = r, {y = 1} in (f {x = true; y = 2}).y

The function f expects the parameter r to have field x, but by width subtyping the argument canactually contain extra fields like {y = 2}. After merging r with {y = 1} in the function body, field y
has two possible values, and the final result can be either 1 or 2. Our solution is to cast the argument
to exactly type {x: Bool}. That is, casting removes field {y = 2}. Therefore, we have to keep thefunction type at runtime to cast the argument. In this way, we avoid the semantic ambiguity, and+ and play an
the final result is always 1. Thus, type annotations are computationally relevant in 𝐹 im
important role since type casting is essential for avoiding ambiguity problems.
Casting. Figure 16 shows the casting relation, which gives an interpretation to subtyping at
runtime. The 𝑣 ↦−→𝐴 𝑣 ′ notation means that we cast value 𝑣 under type 𝐴 and return 𝑣 ′ . Like
subtyping, casting also needs to prioritize some rules over others in certain cases. Thus, castingalso employs the notion of ordinary and splittable types to aid with such prioritization. If the casttype 𝐴 is splittable, then values are cast by the splitting types separately and returning a merge ofthe two casting results (rule cast-and). This rule ensures that we first decompose the intersections,as in the subtyping rule. Then most of the other rules only apply when the type is ordinary (i.e. it
cannot be split further). Note that this rule showcases why annotations are needed for locations inrule Typ-loc. If the value store 𝜇 is carried during casting, the store 𝜇 would be updated in parallel
to be 𝜇1 and 𝜇2 (𝜇; 𝑣 ↦−→𝐵 𝜇1 ; 𝑣 1 and 𝜇; 𝑣 ↦−→𝐶 𝜇2 ; 𝑣 2 ). Thus, it would be hard to decide what theresulting store is, which could lead to a type unsoundness problem. Thus, we annotate locations 𝑜with an annotation to avoid carrying 𝜇 everywhere and to simplify the casting rules.
When the cast type 𝐴 is an ordinary and a top-like type, we generate the top-like values with an
auxiliary TV(𝐴) function, which is shown in the extended version of the paper. A naive rule forcasting under the top type could be:
𝐴 <: ⊤
𝑣 : 𝐴 ↦−→⊤ 𝑣 : ⊤Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:24

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira

𝜇; 𝑣 • arg ↦−→ 𝜇 ′ ; 𝑒(Parallel Elimination)𝑣 ↦−→𝐴 𝑣′

𝜇 ; 𝜆x. 𝑒 : 𝐴 → 𝐵 • 𝑣 ↦−→ 𝜇 ; 𝑒 [x ↦→ 𝑣 ′ ] : 𝐵

pap-betao = 𝑣1 ∈ 𝜇pap-app𝜇 ; f : 𝐴 → 𝐵 • 𝑣 ↦−→ 𝜇 ; f (𝑣 : 𝐴) : 𝐵

𝑣 2 ↦−→ty(𝑣1 ) 𝑣 2′

𝜇 ; o : Ref 𝐴 • 𝑣 2 ↦−→ 𝜇 [o ↦→ 𝑣 2′ ] ; unit

𝜇 ; ΛX . 𝑒 : ∀X ∗ 𝐴. 𝐵 • 𝐶 ↦−→ 𝜇 ; 𝑒 [X ↦→ 𝐶] : 𝐵 [X ↦→ 𝐶]

pap-ass

pap-tapp

𝜇 ; 𝑣 1 • arg ↦−→ 𝜇 ; 𝑒 1
𝜇 ; 𝑣 2 • arg ↦−→ 𝜇 ; 𝑒 2
pap-pjpap-merge
𝜇 ; 𝑣 1 , 𝑣 2 • arg ↦−→ 𝜇 ; 𝑒 1 , 𝑒 2(Small-Step Semantics)

𝜇 ; {l = 𝑣 } • l ↦−→ 𝜇 ; 𝑣
𝜇; 𝑒 ↦−→ 𝜇 ′ ; 𝑒 ′𝜇; 𝑒 ↦−→ 𝜇 ′ ; 𝑒 ′𝑣 :𝐴≠fStep-eval𝜇; 𝐹 [𝑒] ↦−→ 𝜇 ′ ; 𝐹 [𝑒 ′ ]𝑣 ↦−→𝐴 𝑣 ′𝜇; 𝑣 : 𝐴 ↦−→ 𝜇; 𝑣 ′Step-annov

𝜇 ; 𝑣 1 • 𝑣 2 ↦−→ 𝜇 ; 𝑒o∉𝜇Step-refStep-beta

𝜇; ref 𝑣 ↦−→ 𝜇, o = 𝑣; o : Ref ty(𝑣)𝜇; 𝑣 1 𝑣 2 ↦−→ 𝜇; 𝑒o=𝑣 ∈ 𝜇𝜇 ; 𝑣 1 • 𝑣 2 ↦−→ 𝜇 ′ ; 𝑒Step-deref𝜇; !(o : Ref 𝐴) ↦−→ 𝜇; 𝑣 : 𝐴
𝜇 ; 𝑣 • 𝐴 ↦−→ 𝜇 ; 𝑒

𝜇; 𝑣 1 := 𝑣 2 ↦−→ 𝜇 ′ ; 𝑒
𝜇 ; 𝑣 • l ↦−→ 𝜇 ; 𝑒

Step-tapp𝜇; 𝑣 𝐴 ↦−→ 𝜇; 𝑒

Step-ass

Step-pj
𝜇; 𝑣.l ↦−→ 𝜇; 𝑒

+ .
Fig. 17. Small-step semantics of 𝐹 im

but this causes a problem, because for the above merge, we could either have 1 : ⊤ , 2 : ⊤ ↦−→⊤ 1 : ⊤or 1 : ⊤ , 2 : ⊤ ↦−→⊤ 2 : ⊤. So casting would not be deterministic. In a coercive semantics like ours,
the correct way to deal with ⊤ is to view ⊤ as the unit type that has a single value. Then castingunder the top type returns that value and then this recovers determinism. However, there are othertop-like types that cause similar issues and have to be dealt with accordingly, which is why thisnotion appears in the literature of disjoint intersection types [Huang 2023; Oliveira et al. 2016]. If
the cast type 𝐴 is not an ordinary and top-like type, they are covered by case analysis on the value.
An integer 𝑖 cast under type Int results in itself (rule cast-i). Rule cast-f shows that a functional
value, cast under an ordinary function type, simply adds the annotation to the value. Annotatedvalues replace the annotation by the cast type (rule cast-anno). Rule cast-rcd states that records
cast under ordinary record types update the field value by casting under the field type of records.
When merged values are cast under ordinary types, the result of casting comes from either the leftor the right branch (rules cast-mergel and cast-merger).
Parallel elimination. The parallel elimination relation deals with elimination forms requiring an
extra argument during the elimination process. It gives an interpretation to applicative distribution
at runtime. An argument can be a value, a type or a label. There are four expressions that benefit fromparallel elimination: applications, reference assignments, record projections and type applications.
The definition of parallel elimination is shown in Figure 17. The 𝜇; 𝑣 • arg ↦−→ 𝜇 ′ ; 𝑒 notationmeans that value 𝑣 takes an argument with value store 𝜇 and returns expression 𝑒 with store 𝜇 ′ .
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

Imperative Compositional Programming

342:25Rules pap-beta and pap-app are used for expression applications. The annotations of functional
values are erased one by one by rule pap-app. Before doing beta reduction, the argument values 𝑣
are cast under the input type of functions, and the lambda body is annotated with the output typeof function rule pap-beta. Rule pap-ass casts the value argument 𝑣 2 to have the type of value 𝑣 1 inthe store and then updates values in the store. The type of values is obtained from the functionty(𝑣 ):
ty(𝑖) = Intty(⊤) = ⊤ty({𝑙 = 𝑣 }) = {𝑙 : ty(𝑣 )}ty(unit) = Unitty(𝑝 : 𝐴) = 𝐴

ty(𝑓 : 𝐴 → 𝐵) = 𝐴 → 𝐵

ty(𝑣 1 , 𝑣 2 ) = ty(𝑣 1 ) & ty(𝑣 2 )ty((𝜆𝑥 .𝑒) : 𝐴 → 𝐵) = 𝐴 → 𝐵

Type applications are performed in rule pap-tapp. Rule pap-pj projects the field value of a recordby its label. For merged values (𝑣 1 , 𝑣 2 ), both values reduce in parallel (rule pap-merge).
An example showing how parallel elimination works is:·; ((𝜆𝑥 .(𝑥 , False) : Int → Int&Bool : Int&Bool → Bool) , (𝜆𝑥 .𝑥 : Int&Bool → Int)) • (1 , True)↦−→∗ {by rules pap-merge, pap-app, and pap-beta}·; ((1 , False) : Int&Bool : Bool) , ((1 , True) : Int)In this example, we consider an empty value store. Two merged functional values (𝜆𝑥 .(𝑥 , False) :Int → Int&Bool : Int&Bool → Bool) and (𝜆𝑥 .𝑥 : Int&Bool → Int) are reduced in parallel under
the argument (1 , True) to be ((1 , False) : Int&Bool : Bool) and ((1 , True) : Int), respectively.
Reduction. Reduction rules are shown at the bottom of Figure 17. Reduction has the form
𝜇; 𝑒 ↦−→ 𝜇 ′ ; 𝑒 ′ . An expression 𝑒 with the value store 𝜇 reduces to 𝑒 ′ and store 𝜇 ′ . Rule Step-evalevaluates the expressions with different contexts. Casting is triggered by annotations (rule Stepannov). Rules Step-beta, Step-ass, Step-tapp, and Step-pj trigger the parallel application to geta resulting expression. Reference values allocate a fresh location and save the value in the store(rule Step-ref). Rule Step-deref gets the corresponding value in the store by the location address.
+ is deterministic. For well-typed expressions with well-formed
Importantly, the reduction of 𝐹 im
stores, they reduce to the same expressions and same stores:
Theorem 4.8 (Determinism of reduction). If Σ; · ⊢ 𝑒 ⇔ 𝐴, Σ ⊢ 𝜇, 𝜇; 𝑒 ↦−→ 𝜇1 ; 𝑒 1 , and𝜇; 𝑒 ↦−→ 𝜇2 ; 𝑒 2 then 𝑒 1 = 𝑒 2 and 𝜇1 = 𝜇2 .
+ is type sound. Theorem 4.9 says that every well-type expression
Type soundness. Moreover, 𝐹 imwith well-formed stores is either or a value or can be reduced. While Corollary 4.11 shows that the
reduction of well-typed expressions 𝑒 with well-formed stores 𝜇 can be checked by the starting
type 𝐴 and the resulting stores 𝜇 ′ are well-formed with the extended typing store Σ′ . The corollaryof preservation is concluded from Theorem 4.10.

Theorem 4.9 (Progress of reduction). If Σ; · ⊢ 𝑒 ⇔ 𝐴 and Σ ⊢ 𝜇 then either 𝑒 is a value or ∃ 𝑒 ′𝜇 ′ , 𝜇; 𝑒 ↦−→ 𝜇 ′ ; 𝑒 ′ .

Theorem 4.10 (Type preservation with respect to isomorphic subtyping). If Σ; · ⊢ 𝑒 ⇔ 𝐴,
Σ ⊢ 𝜇, and 𝜇; 𝑒 ↦−→ 𝜇 ′ ; 𝑒 ′ then ∃ 𝐵 Σ′ , Σ′ ⊇ Σ, Σ′ ; · ⊢ 𝑒 ′ ⇔ 𝐵, 𝐵 ⪅ 𝐴, and Σ′ ⊢ 𝜇 ′ .
Corollary 4.11 (Type preservation). If Σ; · ⊢ 𝑒 ⇔ 𝐴, Σ ⊢ 𝜇, and 𝜇; 𝑒 ↦−→ 𝜇 ′ ; 𝑒 ′ then ∃ Σ′ ,

Σ′ ⊇ Σ, Σ′ ; · ⊢ 𝑒 ′ ⇐ 𝐴, and Σ′ ⊢ 𝜇 ′ .
5Related WorkIntersection types with references. As discussed in Section 3, Davies and Pfenning identified that anaive use of intersection types is type unsound in the presence of references, and proposed a set of
restrictions. There are some other solutions in the literature. Dezani-Ciancaglini and Della Rocca
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:26

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira[2007] solved the problem by only intersecting non-reference types. With this restriction, subtyping
is allowed to have distributivity and an unrestricted intersection introduction rule. Both counterexamples are rejected, since ref 1 cannot be typed with Ref Nat & Ref Pos. Nevertheless, thisapproach forbids reference types to be intersected even with non-reference types. For instance,(Ref Nat) & Pos is not allowed. Dezani-Ciancaglini et al. [2009], refined the previous proposal toallow intersections between reference and non-reference types. They proposed a kind for types
to track whether the type is a reference type or contains reference types in case of intersection.
Then the type soundness is achieved by restricting intersection elimination rule to intersection
types not containing references. While both works put restrictions on types, our solution does notrely on the sophisticated restriction of no reference intersections. Furthermore, this restriction
seems to prevent some practical programs, such as records/objects with multiple reference fields.
Blaauwbroek [2017] used a pass-by-sharing [Liskov et al. 1979] approach to model computational
effects. In their approach, no reference type exists, and referencing and dereferencing are implicit,
while variables are mutable. For assignments, an invariant typing rule is required.
𝑥 :𝐴 ∈ Γ Γ⊢𝑒 :𝐴
Γ ⊢ 𝑥 := 𝑒 : 𝐴
In this rule, the left expression can only be a variable and the 𝑒 should be of the same type as thevariable. Counter-examples are forbidden because the type of 𝑒 is invariant. Our solution adopts aconventional form of references, and the restriction that we impose is lightweight, while allowing
both distributivity and unrestricted intersection introduction. Furthermore, the restriction does notseem to be restrictive for practical programs.
Merge operator. Reynolds [1988] introduced a calculus with a restricted merge operator andintersection types. Dunfield [2014] proposed a calculus with an unrestricted merge operator, but
the semantics is non-deterministic. To solve the source of non-determinism, Oliveira et al. [2016]
introduced the notion of disjoint intersection types. Two types can be intersected if they are disjoint.
The semantics of calculi with the merge operator is type-directed. Huang et al. [2021] proposed a
new form of semantics called Type-Directed Operational Semantics (TDOS), which we also employ in+ . Over the years several extensions have been proposed for calculi with disjoint intersection types.
𝐹 im
Alpuim et al. [2017] proposed disjoint polymorphism in the calculus 𝐹 i . Bi et al. [2019] improved 𝐹 iwith distributive subtyping and unrestricted intersections. Later, Fan et al. [2022] improved thework of Bi et al. by employing a TDOS to obtain a 𝐹 i+ calculus with simpler proofs. Compared+ is extended with references. So imperative programming is supported. However, 𝐹 +to 𝐹 i+ , 𝐹 imimdoes not support unrestricted intersections and two intersected types should be disjoint. To allow
programs such as 1 : Int&Int, a notion called consistency is required. Consistency states that twovalues are consistent when casting them with the same type returns the same value. To preserve
types, consistency should be preserved at runtime. To achieve this, merge expressions should be
reduced in parallel when distributivity is present. But this introduces difficulties with references,+ ,since two value stores would be evaluated in parallel. Thus we do not employ consistency in 𝐹 im
and resort to restricting all intersections to be disjoint as in Oliveira et al.’s work.
Language designs for modularity. Family polymorphism [Ernst 2001] is a well-known idea in OOP.
A family of related virtual classes is refined simultaneously via inheritance in family polymorphism.
Family polymorphism provides an elegant solution to the expression problem [Ernst 2004]. There
have been several languages and calculi that incorporate the idea of family polymorphism andvirtual classes [Aracic et al. 2006; Clarke et al. 2007; Ernst 1999; Ernst et al. 2006; Jolly et al. 2004;
Madsen and Møller-Pedersen 1989; Nystrom et al. 2004, 2006; Zhang and Myers 2017]. Among theseapproaches, J& [Nystrom et al. 2006] and Familia [Zhang and Myers 2017] share common features
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

Imperative Compositional Programming

342:27

with CP. J& uses intersections to compose related packages or classes. Familia, which is a Javalike language with family polymorphism, also integrates subtype polymorphism and parametricpolymorphism successfully. However, both J& and Familia do not support the merge operator,
which allows for a more dynamic form of composition. All of the aforementioned approaches aim
at modelling a traditional OOP language (usually Java-like) with family polymorphism.
CP is inspired by some of the ideas of family polymorphism. In particular, CP adopts subtyping
and nested composition to enable powerful forms of multiple trait-based inheritance, which canmodel inheritance of whole sets of traits (that are similar to classes). However, CP is both technically very different from traditional calculi with family polymorphism, and it also employs adifferent programming style, based on a form of open pattern matching. As described in Section 1
compositional programming fits within a more general and recent theme of work [Fan and Parreaux2023; Jin et al. 2023; van der Rest and Poulsen 2022, 2023], which aims at addressing modularity
problems of functional programming. All these approaches promote a programming style basedon open forms of pattern matching, although the technical details differ significantly. Previous
work has mostly focused on purely functional settings. Closer to us, van der Rest and Poulsen[2022, 2023] also explore algebraic effects and handlers [Plotkin and Pretnar 2009], which are a
popular approach to introduce effects into purely functional languages. However, they do not fully
consider algorithmic aspects, or provide an implementation. In our work, we aim at supporting amore classical ML-style impure (functional) programming style, which does not track effects. As
we illustrate in our work, this allows us to model mutable objects, as well as programs that create
and traverse cyclic structures, which are difficult in a pure setting.
The motivation and inspiration for new language designs supporting open forms of pattern matching comes partly from previous work on design patterns to support extensibility and modularity.
Such design patterns include, among others: tagless-final embeddings [Carette et al. 2009] and datatypes à la carte [Swierstra 2008] in functional programming; and polymorphic embeddings [Hofer
et al. 2008] and object algebras [Oliveira and Cook 2012a; Rendel et al. 2014] in OOP languages. Whilethese design patterns enable extensible and modular designs, they typically require boilerplate code,
the use of sophisticated type-level features, and an unconventional programming style. By adopting
a dedicated programming language design these issues can be overcome. CP is inspired by the workon object algebras and extensible Church encodings [Oliveira 2009; Oliveira et al. 2006]. However,
CP has significantly improved linguistic support over object algebras. As discussed extensively
by Zhang et al. [2021], nested composition and modular dependencies require sophisticated andcumbersome encodings in languages like Scala. In CP, these concepts are naturally supported.
6

Conclusion

In this paper, we propose two calculi. One solves the type soundness problem identified by Davies
and Pfenning [2000] with lighter restrictions, based on bidirectional typing. The other calculus,+ , is a variant of 𝐹 + with references. We augment the CP language with references based
named 𝐹 imi+on 𝐹 im as the core calculus. With references, CP enables a modular imperative programming style.
We illustrate how graph structures can be encoded by CP with a live-variable analysis example.
A direction for future work is to study whether disjoint union types [Rehman et al. 2022] arecompatible with references, and add support for them in CP. Moreover, it would be interesting to
explore whether effect handlers and algebraic effects can be encoded in CP, perhaps with someextensions.
Acknowledgments
We are grateful to anonymous reviewers and our colleagues at the HKU PL group. This work has
been sponsored by Hong Kong Research Grants Council project number 17209821.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:28

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira

Data-Availability Statement
The artifact that supports the paper is available on Zenodo [Ye et al. 2024].
References
Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2007. Compilers: Principles, Techniques and Tools. Pearson
Education.
João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. 2017. Disjoint Polymorphism. In Programming Languages andSystems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory
and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings (Uppsala, Sweden). Springer-Verlag,
Berlin, Heidelberg, 1–28. https://doi.org/10.1007/978-3-662-54434-1_1
Ivica Aracic, Vaidas Gasiunas, Mira Mezini, and Klaus Ostermann. 2006. An Overview of CaesarJ. In Transactions on
Aspect-Oriented Software Development I, Awais Rashid and Mehmet Aksit (Eds.). Springer Berlin Heidelberg, Berlin,
Heidelberg, 135–173.
Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983. A Filter Lambda Model and the Completenessof Type Assignment. Journal of Symbolic Logic 48 (12 1983). https://doi.org/10.2307/2273659
Xuan Bi and Bruno C. d. S. Oliveira. 2018. Typed First-Class Traits. In ECOOP. 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 ECOOP. 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 Programming Languages and Systems, Luís Caires (Ed.). Springer International Publishing, Cham,
381–409.
Lasse Blaauwbroek. 2017. On the Interaction Between Unrestricted Union and Intersection Types and Computational Effects.
Master’s thesis. Technical University Eindhoven.
Luca Cardelli and John C. Mitchell. 1989. Operations on records. Mathematical Structures in Computer Science 1 (1989), 3 –48. https://api.semanticscholar.org/CorpusID:8648683
Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. 2009. Finally Tagless, Partially Evaluated: Tagless Staged Interpreters
for Simpler Typed Languages. J. Funct. Program. 19, 5 (2009). https://doi.org/10.1017/S0956796809007205
Dave Clarke, Sophia Drossopoulou, James Noble, and Tobias Wrigstad. 2007. Tribe: a simple virtual class calculus. In
Proceedings of the 6th International Conference on Aspect-Oriented Software Development (Vancouver, British Columbia,
Canada) (AOSD ’07). Association for Computing Machinery, New York, NY, USA, 121–134. https://doi.org/10.1145/
1218563.1218578
William Cook and Jens Palsberg. 1989. A Denotational Semantics of Inheritance and Its Correctness. In OOPSLA. https://doi.org/10.1145/74878.74922
Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1981. Functional Characters of Solvable Terms. Zeitschrift
für matematische Logik und Grundlagen der Mathematik 27 (1981), 44–58.
Rowan Davies and Frank Pfenning. 2000. Intersection Types and Computational Effects. In Proceedings of the 5th ACM
SIGPLAN International Conference on Functional Programming. https://doi.org/10.1145/351240.351259
Mariangiola Dezani-Ciancaglini and Simona Ronchi Della Rocca. 2007. Intersection and reference types. Reflections on Type
Theory, Lambda Calculus, and the Mind (2007), 77–86.
Mariangiola Dezani-Ciancaglini, Paola Giannini, and Simona Ronchi Della Rocca. 2009. Intersection, Universally Quantified,and Reference Types. In Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the
EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings (Lecture Notes in Computer Science, Vol. 5771), Erich Grädel
and Reinhard Kahle (Eds.). Springer, 209–224. https://doi.org/10.1007/978-3-642-04027-6_17
Stéphane Ducasse, Oscar Nierstrasz, Nathanael Schärli, Roel Wuyts, and Andrew P. Black. 2006. Traits: A Mechanism for
Fine-Grained Reuse. ACM Trans. Program. Lang. Syst. 28, 2 (2006). https://doi.org/10.1145/1119479.1119483
Jana Dunfield. 2014. Elaborating intersection and union types. Journal of Functional Programming 24, 2–3, 133–165.
Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing. ACM Comput. Surv. 54, 5, Article 98 (may 2021), 38 pages.
https://doi.org/10.1145/3450952
Erik Ernst. 1999. gbeta - a Language with Virtual Attributes, Block Structure, and Propagating, Dynamic Inheritance. Ph. D.
Dissertation. University of Aarhus.
Erik Ernst. 2001. Family Polymorphism. In European Conference on Object-Oriented Programming. https://doi.org/10.1007/3540-45337-7_17
Erik Ernst. 2004. The expression problem, Scandinavian style. On Mechanisms For Specialization 27 (2004).
Erik Ernst, Klaus Ostermann, and William R. Cook. 2006. A virtual class calculus. In Conference Record of the 33rd ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’06). 270–282.

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

Imperative Compositional Programming

342:29Martin Erwig. 2001. Inductive graphs and functional graph algorithms. Journal of Functional Programming (2001). https://doi.org/10.1017/S0956796801004075
Andong Fan, Xuejing Huang, Han Xu, Yaozhu Sun, and Bruno C. d. S. Oliveira. 2022. Direct Foundations for Compositional
Programming. In ECOOP. https://doi.org/10.4230/LIPIcs.ECOOP.2022.18
Andong Fan and Lionel Parreaux. 2023. super-Charging Object-Oriented Programming Through Precise Typing of OpenRecursion. In 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington,
United States (LIPIcs, Vol. 263), Karim Ali and Guido Salvaneschi (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
11:1–11:28.
Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting Gradual Typing. In Proceedings of the 43rd Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St. Petersburg, FL, USA) (POPL ’16). Association
for Computing Machinery, New York, NY, USA, 429–442. https://doi.org/10.1145/2837614.2837670
Jean-Yves Girard. 1972. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Ph. D.
Dissertation. Université Paris VII.
Robert Harper and Benjamin Pierce. 1991. 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
David Herman, Aaron Tomb, and Cormac Flanagan. 2010. Space-efficient gradual typing. Higher-Order and Symbolic
Computation 23, 2 (2010), 167.
Christian Hofer, Klaus Ostermann, Tillmann Rendel, and Adriaan Moors. 2008. Polymorphic Embedding of DSLs. In GPCE.
https://doi.org/10.1145/1449913.1449935
Xuejing Huang. 2023. Taming intersection types and the merge operator. HKU Theses Online (HKUTO) (2023).
Xuejing Huang, Jinxu Zhao, and Bruno C. d. S. Oliveira. 2021. Taming the Merge Operator. J. Funct. Program. 31 (2021), e28.
https://doi.org/10.1017/S0956796821000186
Ende Jin, Nada Amin, and Yizhou Zhang. 2023. Extensible Metatheory Mechanization via Family Polymorphism. Proc. ACM
Program. Lang. 7, PLDI (2023), 1608–1632.
Paul Jolly, Sophia Drossopoulou, Christopher Anderson, and Klaus Ostermann. 2004. Simple Dependent Types: Concord. In
ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP 2004). Oslo, Norway.
Daan Leijen. 2005. Extensible records with scoped labels. In Symposium on Trends in Functional Programming. https://api.semanticscholar.org/CorpusID:856697
Barbara Liskov, Russ R Atkinson, Toby Bloom, J Eliot B Moss, Craig Schaffert, Bob Scheifler, and Alan Snyder. 1979. CLU
reference manual. (1979).
Ole Lehrmann Madsen and Birger Møller-Pedersen. 1989. Virtual classes: a powerful mechanism in object-oriented
programming. In Conference Proceedings on Object-Oriented Programming Systems, Languages and Applications (New
Orleans, Louisiana, USA) (OOPSLA ’89). Association for Computing Machinery, New York, NY, USA, 397–406. https://doi.org/10.1145/74877.74919
Nathaniel Nystrom, Stephen Chong, and Andrew C. Myers. 2004. Scalable extensibility via nested inheritance (OOPSLA ’04).
Association for Computing Machinery, New York, NY, USA, 99–115. https://doi.org/10.1145/1028976.1028986
Nathaniel Nystrom, Xin Qi, and Andrew C. Myers. 2006. J&: nested intersection for scalable software composition. In
Proceedings of the 21st Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, andApplications (Portland, Oregon, USA) (OOPSLA ’06). Association for Computing Machinery, New York, NY, USA, 21–36.
https://doi.org/10.1145/1167473.1167476
Bruno C. d. S. Oliveira. 2009. Modular Visitor Components: A Practical Solution to the Expression Families Problem. In
ECOOP. https://doi.org/10.1007/978-3-642-03013-0_13
Bruno C. d. S. Oliveira and William R. Cook. 2012a. Extensibility for the Masses: Practical Extensibility with Object Algebras.
In ECOOP. https://doi.org/10.1007/978-3-642-31057-7_2
Bruno C. d. S. Oliveira and William R. Cook. 2012b. Functional programming with structured graphs. In ACM SIGPLAN
International Conference on Functional Programming, ICFP’12, Copenhagen, Denmark, September 9-15, 2012, Peter Thiemann
and Robby Bruce Findler (Eds.). ACM, 77–88.
Bruno C. d. S. Oliveira, Ralf Hinze, and Andres Löh. 2006. Extensible and Modular Generics for the Masses. In TFP.
Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. 2016. Disjoint intersection types. In Proceedings of the 21st ACM
SIGPLAN International Conference on Functional Programming (Nara, Japan) (ICFP 2016). Association for Computing
Machinery, New York, NY, USA, 364–377. https://doi.org/10.1145/2951913.2951945
Benjamin C. Pierce. 1993. Intersection Types and Bounded Polymorphism. In Typed Lambda Calculi and Applications,International Conference on Typed Lambda Calculi and Applications, TLCA ’93, Utrecht, The Netherlands, March 16-18, 1993,
Proceedings (Lecture Notes in Computer Science, Vol. 664), Marc Bezem and Jan Friso Groote (Eds.). Springer, 346–360.
Gordon Plotkin and Matija Pretnar. 2009. Handlers of algebraic effects. In European Symposium on Programming. Springer,
80–94.

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.

342:30

Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira

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.
Baber Rehman, Xuejing Huang, Ningning Xie, and Bruno C. d. S. Oliveira. 2022. Union Types with Disjoint Switches. 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,
25:1–25:31. https://doi.org/10.4230/LIPIcs.ECOOP.2022.25
Tillmann Rendel, Jonathan Immanuel Brachthäuser, and Klaus Ostermann. 2014. From object algebras to attribute grammars.
In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications,OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014, Andrew P. Black and Todd D. Millstein (Eds.).
ACM, 377–395.
John C. Reynolds. 1974. Towards a theory of type structure. In Symposium on Programming (LNCS, Vol. 19). Springer,
408–423.
John C. Reynolds. 1988. Preliminary design of the programming language Forsythe. Carnegie-Mellon University. Departmentof Computer Science.
John C. Reynolds. 1997. Design of the programming language Forsythe. In ALGOL-like languages. 173–233.
Mark Shields and Erik Meijer. 2001. Type-indexed rows. In ACM-SIGACT Symposium on Principles of Programming Languages.
https://api.semanticscholar.org/CorpusID:3321216
Jeremy G. Siek and Philip Wadler. 2009. Threesomes, with and without Blame. In Proceedings for the 1st Workshop on Script
to Program Evolution (Genova, Italy) (STOP ’09). Association for Computing Machinery, New York, NY, USA, 34–46.
https://doi.org/10.1145/1570506.1570511
Wouter Swierstra. 2008. Data Types à la Carte (Functional Pearl). J. Funct. Program. 18, 4 (2008). https://doi.org/10.1017/
S0956796808006758
Matías Toro and Éric Tanter. 2020. Abstracting Gradual References. In 34th European Conference on Object-Oriented
Programming (ECOOP 2020) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 166), Robert Hirschfeld andTobias Pape (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 33:1–33:4. https://doi.org/
10.4230/LIPIcs.ECOOP.2020.33
Cas van der Rest and Casper Bach Poulsen. 2022. Towards a Language for Defining Reusable Programming Language
Components (Project Paper). In Trends in Functional Programming - 23rd International Symposium, TFP 2022, Virtual
Event, March 17-18, 2022, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 13401), Wouter Swierstra andNicolas Wu (Eds.). Springer, 18–38. https://doi.org/10.1007/978-3-031-21314-4_2
Cas van der Rest and Casper Bach Poulsen. 2023. Types and Semantics for Extensible Data Types. In Programming Languages
and Systems - 21st Asian Symposium, APLAS 2023, Taipei, Taiwan, November 26-29, 2023, Proceedings (Lecture Notes in
Computer Science, Vol. 14405), Chung-Kil Hur (Ed.). Springer, 46–66.
Philip Wadler. 1998. The Expression Problem. Posted on the Java Genericity mailing list. https://homepages.inf.ed.ac.uk/
wadler/papers/expression/expression.txt
Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can’t Be Blamed. In Proceedings of the 18th European
Symposium on Programming Languages and Systems: Held as Part of the Joint European Conferences on Theory and Practiceof Software, ETAPS 2009 (York, UK) (ESOP ’09). Springer-Verlag, Berlin, Heidelberg, 1–16. https://doi.org/10.1007/978-3642-00590-9_1
Andrew K. Wright. 1995. Simple Imperative Polymorphism. LISP and Symbolic Computation 8, 4 (1995), 343–355. https://doi.org/10.1007/BF01018828
Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira. 2024. Imperative Compositional Programming (Artifact). https://doi.org/10.5281/zenodo.13373228
Weixin Zhang, Yaozhu Sun, and Bruno C. d. S. Oliveira. 2021. Compositional Programming. ACM Trans. Program. Lang.
Syst. 43, 3 (2021). https://doi.org/10.1145/3460228
Yizhou Zhang and Andrew C. Myers. 2017. Familia: unifying interfaces, type classes, and family polymorphism. Proc. ACM
Program. Lang. 1, OOPSLA, Article 70 (oct 2017), 31 pages. https://doi.org/10.1145/3133894
Yaoda Zhou, Bruno C. d. S. Oliveira, and Andong Fan. 2022. A Calculus with Recursive Types, Record Concatenation andSubtyping. In APLAS. https://doi.org/10.1007/978-3-031-21037-2_9

Received 2024-04-04; accepted 2024-08-18

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 342. Publication date: October 2024.