Merging Gradual Typing
WENJIA YE, The University of Hong Kong, China
BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, ChinaMATÍAS TORO, PLEIAD Lab, Computer Science Department (DCC), University of Chile, Chile
Programming language mechanisms with a type-directed semantics are nowadays common and widelyused. Such mechanisms include gradual typing, type classes, implicits and intersection types with a merge
operator. While sharing common challenges in their design and having complementary strengths, type-directedmechanisms have been mostly independently studied.
This paper studies a new calculus, called λM⋆ , which combines two type-directed mechanisms: gradualtyping and a merge operator based on intersection types. Gradual typing enables a smooth transition between
dynamically and statically typed code, and is available in languages such as TypeScript or Flow. The merge
operator generalizes record concatenation to allow merges of values of any two types. Recent work has
shown that the merge operator enables modelling expressive OOP features like first-class traits/classes anddynamic inheritance with static type-checking. These features are not found in mainstream statically typed
OOP languages, but they can be found in dynamically or gradually typed languages such as JavaScript or
TypeScript. In λM⋆ , by exploiting the complementary strengths of gradual typing and the merge operator,
we obtain a foundation for modelling gradually typed languages with both first-class classes and dynamic
inheritance. We study a static variant of λM⋆ (called λM); prove the type-soundness of λM⋆ ; show that λM⋆
can encode gradual rows and all well-typed terms in the GT FL≲ calculus; and show that λM⋆ satisfies gradualtyping criteria. The dynamic gradual guarantee (DGG) is challenging due to the possibility of ambiguity
errors. We establish a variant of the DGG using a semantic notion of precision based on a step-indexed logicalrelation.
CCS Concepts: • Software and its engineering → Functional languages; Data types and structures.
Additional Key Words and Phrases: Bidirectional Typing, Gradual Typing, Type-Directed Semantics, Merge
Operator
ACM Reference Format:
Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro. 2024. Merging Gradual Typing. Proc. ACM Program. Lang.
8, OOPSLA2, Article 294 (October 2024), 29 pages. https://doi.org/10.1145/3689734

1

Introduction

Programming language mechanisms with a type-directed semantics are nowadays widely used.
Such mechanisms include gradual typing [Siek and Taha 2006; Tobin-Hochstadt and Felleisen 2006],
type classes [Wadler and Blott 1989], implicits [Oliveira et al. 2010] and intersection types with amerge operator [Dunfield 2014; Reynolds 1997]. In all those mechanisms the semantics of a program
may depend on the types assigned to the program. In other words, changing some type in the
program (without changing anything else) may change the semantics of the program. Programming
Authors’ Contact Information: Wenjia Ye, The University of Hong Kong, Hong Kong, China, yewenjia@connect.hku.hk;
Bruno C. d. S. Oliveira, The University of Hong Kong, Hong Kong, China, bruno@cs.hku.hk; Matías Toro, PLEIAD Lab,
Computer Science Department (DCC), University of Chile, Santiago, Chile, mtoro@dcc.uchile.cl.
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-ART294
https://doi.org/10.1145/3689734

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

294:2

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Torolanguages such as Haskell (via type classes), Scala (via implicits), gradually typed languages oreven Java (via static overloading) all include language mechanisms with a type-directed semantics.
While sharing common challenges in their design and having complementary strengths, typedirected mechanisms have been mostly independently studied. In this paper we focus on integrating
two type-directed mechanisms: gradual typing and the merge operator in calculi with intersection
types. Gradual typing enables a gradual transition between dynamically and statically typed code,and is nowadays available in languages such as TypeScript and Flow (which are supersets of
JavaScript). The merge operator generalizes record concatenation to allow merges of values of any
two types. Recent work [Bi and Oliveira 2018; Zhang et al. 2021] showed that the merge operator
can model expressive OOP features like first-class traits/classes [Takikawa et al. 2012] and dynamic
inheritance [Ernst 2000] with static type-checking. Such features are not found in mainstream
statically typed OOP languages, but they are found in dynamic languages such as JavaScript.
Due to its practical importance, there has been much research in past years on gradual typing.
Nonetheless, much of the focus of research on gradual typing has been on gradualizing common
statically-typed calculi that do not have a type-directed semantics. Within this line of work, Siek andTaha [2007] initiated a line of work exploring minimal gradually typed calculi for modelling objects,
based on an object calculus by Abadi and Cardelli [1996]. Siek and Taha’s calculus is relatively
limited in that it only supports objects with a fixed number of fields/methods. More recently, gradualvariants of record calculi, such as the GT FL≲ calculus, have been proposed [Bañados Schwerter
et al. 2021; Garcia et al. 2016]. Similarly to Siek’s work, the GT FL≲ calculus only supports fixed-sizerecords. The restrictions in those calculi mean that there is still a large gap to the features thatare available in JavaScript. In particular the lack of extensible objects/records prevents modelling(dynamic) multiple inheritance and more expressive OOP mechanisms that are available in languages
such as JavaScript. A notable reference in this space is Takikawa et al. [2012] work, which hasaddressed the integration of gradual typing and first-class classes. However, this integration is at
the module level, allowing dynamically typed and statically typed modules to interoperate.
Calculi with extensible records provide a natural foundation for languages with inheritance,
which can be modelled by record concatenation [Cook and Palsberg 1989; Wand 1989]. Unfortunately, as identified by Cardelli and Mitchell [1991], there are important challenges to develop a
typed language with both record concatenation and subtyping. Calculi with the merge operator anddisjoint intersection types [Oliveira et al. 2016] overcome such challenges with a type-directedsemantics. Recently, Huang et al. [2021] proposed a type-directed operational semantics (TDOS)
approach for such calculi. The TDOS approach allows giving a direct operational semantics to
calculi with the merge operator. Furthermore the TDOS approach is not tied to calculi with themerge operator, and can be used to model the semantics of other type-directed mechanisms as well.
In particular, it has been adapted by Ye et al. [2021] to gradual typing. However, so far there is no
calculus including both the merge operator and gradual typing.
This paper studies a new calculus, called λM⋆ , combining gradual typing and a merge operator
based on intersection types. With λM⋆ , we obtain a foundation for modelling gradually typed
languages with expressive OOP features, such as first-class classes and dynamic inheritance ina purely functional setting with records. There is still a gap between our work, and mainstream
languages like JavaScript and TypeScript, since we do not consider imperative features, such as
references and object identity. Nevertheless, we address fundamental questions that arise from theinteraction between dynamic inheritance and method overriding. Without care, such interaction
can easily lead to type unsoundness, as shown in Section 2.3 using TypeScript. Furthermore, with
gradual typing, this interaction is further complicated by the possibility of runtime ambiguity
errors. We make the following contributions in this paper:

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

Merging Gradual Typing

294:3• We show how to combine two type-directed mechanisms (gradual typing and themerge operator) into a single language. This sheds new insights such as how to integrate
multiple type-directed mechanisms, and how to design casting relations for the dynamic
semantics.
• The λM and the λM⋆ calculi. We present the λM⋆ calculus as a concrete language design
integrating gradual typing and the merge operator using a TDOS. The static counterpart is avariant of a calculus with a merge operator called λM. We prove several results for λM and
λM⋆ , including type soundness, determinism and the gradual guarantee for λM⋆ .
• A new solution to the problem of modular type invariants for gradual rows identified
by Bañados Schwerter et al. [2021]. λM⋆ provides a solution (inherited from previous calculi
with a merge operator [Huang et al. 2021]) to preserve such modular type invariants. Moreover
we relate the problem to a problem that was identified 30 years earlier by Cardelli and Mitchell[1991] for record calculi with subtyping.
• An encoding of gradual rows and the GT FL≲ calculus in λM⋆ . Compared to the GT FL≲
calculus, λM⋆ does not need a special type for gradual rows, and supports extensible records.
• Prototype, Coq proofs and a proof of the dynamic gradual guarantee. All the calculi
and proofs in this paper are mechanically formalized in Coq, with the exception of dynamic
gradual guarantee, which employs a step-indexed logical relation and is manually proved. We
also offer an interactive prototype implementation of λM⋆ (including some simple extensions).
Both the formalization, proofs and implementation are available in the artifact [Ye et al. 2024].
2

Overview

We start with an overview of the merge operator and gradual typing, motivate the combination of
the two features, and give an overview of our work and the λM and λM⋆ calculi.
2.1

Background: Gradual Typing

Gradual typing [Siek and Taha 2006; Tobin-Hochstadt and Felleisen 2006] enables programs torange from dynamic typing to static typing. To defer static type checks to runtime, gradual typing
employs the unknown type ⋆ and consistency relations. The unknown type ⋆ is consistent withany type. Dynamic type errors are triggered by casts. The implicit casts in gradual typing have atype-directed semantics: the semantics of programs depends on the types used in the casts. For
example, in the simple expression 1 : ⋆ : Bool casting 1 to type Bool will result in blame (i.e. a
runtime type error). However, if we have 1 : ⋆ : Int instead, we obtain the integer 1 after running the
program. Thus, the types used by casts can give rise to different evaluation results. Note that in theprevious examples (and the examples that follow), we adopt a notation similar to type annotations
to denote casts. For instance, in the expression 1 : ⋆ : Bool there are two casts: a first cast from Int(the type of 1) to ⋆; and a second cast from ⋆ to Bool. We choose the use of this notation throughout
the paper to be consistent with the notation in the λM and λM⋆ calculi.
Typed-Directed Operational Semantics (TDOS). Traditionally the semantics of gradual languages
is given by an elaboration to an intermediate (cast) calculus [Siek and Taha 2006]. Ye et al. [2021]
proposed an alternative approach to give the semantics of gradually typed calculi that avoids anelaboration. The approach is based on typed-directed operational semantics (TDOS): a variant ofsmall-step semantics first proposed by Huang and Oliveira [2020]. A TDOS uses type annotations
to determine the result of reduction at run-time. TDOS contains two main components. One is a
traditional reduction relation with a few adjustments. The other one is a typed reduction relation
v ,→A v ′ , which we call casting in our work. The casting relation takes a value and a type as the
input and produces a value matching the shape of input type. Ye et al. [2021] applied the TDOS to
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

294:4

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro

gradual typing successfully to two different gradually typed calculi. For gradual typing, the casting
relation generalizes the result of casting (v ,→A r) to a result r, which contains not only values
but also run-time errors (err∗ ). Compared to the elaboration approach, a benefit of the TDOS isthat the dynamic semantics is defined directly for the gradually typed source language.
2.2

Background: The Merge Operator

Some calculi with intersection types employ a special operator, called the merge operator [Dunfield
2014; Reynolds 1997], that allows building values that can have multiple types. For example, in thefollowing program, x has both an integer and a boolean value and has the type Int & Bool:let x = 1 , , True in (x + 1, not x)
x is built using the merge operator ( , , ). When x is used, it can act as either an integer or a boolean.
In calculi with a merge operator multi-field records are merges of single field records. As Dunfieldnoticed, the merge operator can encode various other programming language features, including
extensible records, dynamic typing and operator overloading. Recent research has further shown
programming language designs, such as SEDEL [Bi and Oliveira 2018] or CP [Zhang et al. 2021],
based on variants of the merge operator. These designs enable applications such as first-classclasses/traits [Bi and Oliveira 2018] and Compositional Programming [Zhang et al. 2021].
Type-directed Semantics of Merges and the Interaction with Subtyping. The semantics of the merge
operator is type-directed: components are extracted from merges based on types. For instance, in theexpression x + 1 above, the type Int is required by +. Therefore 1 should be extracted from x. Whileconvenient, the type-directed extraction of values can lead to ambiguity. Consider (1 , , 2) : Int.
This program is ambiguous because the result can be either 1 or 2. Moreover, the interaction
between subtyping and the merge operator is subtle [Dunfield 2014; Huang et al. 2021]. A closely
related problem was identified by Cardelli and Mitchell [1991], for calculi with subtyping and record
concatenation (a special case of the general merge operator). We illustrate the issue with an example
based on Cardelli and Mitchell’s work:
let x : {l2 : Bool} = {l1 = "Boom!"} , , {l2 = True} in ({l1 = 2} , , x).l1 + 3
Variable x has type {l2 : Bool}. The value for x includes a field l1 , which is hidden due to subtyping.
The merge {l1 = 2}, , x, appears to be safe statically (since statically x does not contain l1 ). However,what should happen when we do the field lookup? If the original field l1 is preserved in x then,when we lookup l1 , there will be two l1 fields. Naive biased lookups are problematic. For instance,in the program above, if a right-biased lookup is used, then the program would extract the string"Boom!" and try to add that to an integer, which would crash the program. In other words a naive
biased lookup for merges in the presence of subtyping is not type-sound. Even if the two valuesof the field l1 have the same type, extracting the value of the hidden field may lead to surprising
behaviour to programmers, since the type of x appears to promise that no field l1 is present. For
these reasons Cardelli and Mitchell argued that biased lookups should not be used.
Disjoint Intersection Types. To address the ambiguity problems, as well as the problems arisingfrom the interactions between merges and subtyping, Oliveira et al. [2016] proposed to havea restriction where only merges of disjoint types are accepted. Disjointness rejects ambiguous
programs such as True , , False or 1 , , 2, since the types of the two values being merged are notdisjoint. Similarly to gradual typing (as discussed in Section 2.1), the semantics for languages withthe merge operator can also be given using a TDOS approach [Huang and Oliveira 2020; Huang
et al. 2021]. Huang et al. proposed λi : a calculus with a merge operator and disjoint intersection
types. λi solves the ambiguity of issues of the merge operator with disjointness and a TDOS. We
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

Merging Gradual Typing

294:5

illustrate how λi ’s TDOS solves the problem next:(λx. ((x , , 1) + 1) : Bool → Int) (True , , 2) ,→∗ ((True , , 1) + 1) : Int ,→∗ 2
If we just substitute True , , 2 with a normal beta reduction, a non-disjoint expression would be
generated after substitution (True , , 2 , , 1). Instead, True is extracted by casting True , , 2 under
the function input type Bool. Thus the value that gets substituted in the body of the lambda is True
instead of True , , 2. This enables the program to reduce without encountering ambiguities in themerges. Coming back to the example with records:
let x : {l2 : Bool} = {l1 = "Boom!"} , , {l2 = True} in ({l1 = 2} , , x).l1 +3
What λi (extended with records) does is to drop the field l1 in x when the value is upcast to havethe type {l2 : Bool}. Therefore, ({l1 = 2} , , x).l1 would become ({l1 = 2} , , {l2 = True}).l1 and thefinal result of the program would be 5. In other words, the solution of λi to the problem of theinteraction between merges and subtyping is to ensure that values in a merge that are hidden by
subtyping are dropped from the value when (up)casting.
2.3

Motivation: Combining Merges and Gradual Typing

While TDOS has been applied to both gradual typing and calculi with the merge operator separately,
there is no calculus that supports both gradual typing and the merge operator. However there arecompelling reasons to develop calculi supporting both features, which we discuss next.
Modelling Expressive Dynamic OOP features. Most mainstream implementations of gradually
typed languages target languages such as JavaScript. While in gradual typing research has focusedon gradualizing a variety of common type systems, there is much less effort on type systems thatmodel highly dynamic OOP features. Yet, since languages like JavaScript are actually the mostcommon practical focus on mainstream gradually typed language implementations (like TypeScript
or Flow), this leaves open the question of how to design and implement type systems that support
such features. Since one of the use-modes of gradual typing is full static typing, it is desirable tosupport (static) type systems that enable type-checking for (some of) the advanced OOP features ofdynamic languages such as JavaScript.
For example, JavaScript supports first-class classes [Takikawa et al. 2012], and dynamic inheritance [Ernst 2000]. First-class classes are first-class values (just like lambdas in functional programming), and can be passed as arguments or returned as results. Dynamic inheritance means that theinherited classes are not statically known (they can be parametrized, for instance). With first-classclasses and dynamic inheritance, the programmer can abstract over patterns in the hierarchy ofclasses and model mixins [Bracha and Cook 1990]. In JavaScript a mixin is as a function that takes
a superclass as input and returns a subclass that extends the superclass. For example:
const circleMixin = shape ⇒ {return class extends shape { area(radius) { return PI * radius * radius; } }};In this JavaScript code, circleMixin extends shape with a method to calculate the area of a circle.
The super class shape is a function parameter, which means that circleMixin can be extended byany shape class at runtime. In a conventional statically-typed class-based language such as Java,such parametrization by a superclass is not possible, due to restrictions of the type system.
A Type Unsound Approach to First-Class Classes in TypeScript. TypeScript supports conventional
static inheritance idioms and its type system prevents type-unsafe overrides (similarly to Java or
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

294:6

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toroclass A {m() : number {return 5};n() : number {return this.m() - 4;} }interface C {n() : number}
type GConstructor<T = {}> = new (...args: any[]) ⇒ T;
function mkB<TBase extends GConstructor<C>>(Base: TBase) {return class B extends Base {m() : string {return "hello";} // If m exists in Base it will be overriden};}
const cl = mkB(A);// Problem: Superclass already contains an mconst o = new cl;console.log(o.n());
Fig. 1. Type unsoundness of first-class classes in TypeScript.

C#). In addition, TypeScript also supports first-class classes and dynamic inheritance1 . However,as we shall illustrate next, the fact that with dynamic inheritance we do not have the exact type
information for superclasses is problematic and leads to type unsoundness (without relying on
dynamic types). For instance consider the TypeScript program in Figure 1. In this program, wecreate a class A with m and n methods, which return integers. Importantly, n is defined in terms of m.
Then mkB is parametrized by a class Base, which is used as the superclass of B. We can specify theinterface of the superclass as being C, which only contains a method n. Note that B defines anothermethod m, which returns a string. TypeScript checks that there are no conflicts between m and themethods in the superclass interface C. We then create an object o using A as the superclass for B (viamkB). Unfortunately, the m that is present in B overrides the m from A. Then when we run n we end up
subtracting an integer from a string, which results in a runtime type error (TypeScript/JavaScript
actually tries to convert the string to a number and we get NaN instead).
In short, the TypeScript approach to deal with first-class classes is type unsound. The reason
for unsoundness is mkB(A). A is a subtype of C with an extra m() : number field, but when typechecking B we do not know about the extra members (m() : number) of the subtype. Thus thetype system of TypeScript fails to detect the problematic override. This problem is a manifestationof the problem identified by Cardelli and Mitchell [1991] discussed in the Section 2.2. Note also thatin languages with static inheritance and top-level classes only (such as Java or C#) there is no suchflexibility and the issue above does not arise. The problem is more pervasive with the dynamic
type, where we may be able to inherit from a supertype with an unknown interface, but then wecannot statically prevent overrides since there is no information at all about the supertype.
First-class Traits and Dynamic Inheritance with Merges. Calculi and languages with the merge
operator can model mechanisms such as first-class classes. For instance, in the CP language [Zhang
et al. 2021], we can rewrite the circle mixin as:
type Shape = { name : String }circle (super: Trait<Shape>) =trait inherits super ⇒ { area radius = PI * radius * radius; };1 https://www.typescriptlang.org/docs/handbook/mixins.html

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

Merging Gradual Typing

294:7

The CP language supports a form of first-class traits [Bi and Oliveira 2018] (which are analogous
to classes), and supports dynamic inheritance like JavaScript. However, unlike JavaScript, CP isstatically typed. In the program above, the trait being inherited is parametrized. For simplicity,in the code above we assume that the interface of the trait being inherited is Shape, but CP also
supports dynamic inheritance even when the interface of the superclass is not fully know using
disjoint polymorphism [Alpuim et al. 2017]. Section 2.4 gives a brief overview of how the encodingof first-class classes in CP in terms of merges works. We also show how the semantics of casting
and merges together with disjointness solve the problem in Figure 1, and enable type-sound andexpressive designs of languages with first-class classes. We refer the reader interested in moreadvanced features of CP and the full details of how CP elaborates first-class traits and dynamic
inheritance to a calculus with a merge operator to the work by Bi and Oliveira [2018] and Zhang
et al. [2021].
In this work we propose to combine the merge operator with gradual typing. Thus we envisiona language like CP, supporting gradual typing. In such language, we could have a variation of the
program above that combines first-class traits, dynamic inheritance and gradual typing:circle (super: Trait<⋆>) = trait inherits super ⇒ {area (radius : ⋆) : number = PI * radius * radius;};

In the program above, we mix static and dynamic typing. There are two noteworthy points. Firstly,
we make the type of radius dynamic (or unknown), and implicitly cast radius from ⋆ to a number.
Secondly, and more interestingly, the inherited trait has an unknown interface. We cannot rule out
conflicts statically, like in CP, because there is no static type information about the interface ofthe supertype. Therefore, how can we deal with possible method conflicts? For instance, what if
the super class/trait has an area method, taking one argument, already? Adopting an overriding
semantics would be prone to issues similar to those identified by Cardelli and Mitchell. So, instead,
we propose to detect ambiguity at runtime: if the superclass contains a conflicting method, then aruntime error may be raised to indicate ambiguity. By allowing programs like the above, we canhave a language, which supports very dynamic OOP features similar to those in JavaScript, whileat the same time supporting gradual typing.
Unified Foundation for Type-Directed Mechanisms. A second reason to have a unified framework
for type-directed mechanisms is that it is beneficial to avoid duplication of efforts in addressing common problems. For example, performant sound gradual typing is currently a hot topic [Greenman
2023; Greenman et al. 2019; Kuhlenschmidt et al. 2019; Muehlboeck and Tate 2017, 2021; Takikawa
et al. 2016], since there is a high cost imposed by casting. Because calculi with the merge operator
have casting, this is an issue for such calculi as well. Thus, leveraging on the developments forgradually typed languages is helpful to address similar problems in calculi with merges. In thecurrent work we do not address the important issue of performance. However, we hope to leverageon the existing work on gradual typing in the future to improve the performance in calculi with themerge operator. Section 7 briefly sketches some possible directions for performance improvements.
Furthermore, designs for the semantics of calculi with the merge operator can also lead to new
developments that are useful for gradual typing. For instance, the TDOS approach to gradual typing
originated from developments in the semantics of languages with the merge operator.
2.4

Key Ideas and Challenges

In this paper we propose two new calculi. The λM calculus is a statically typed calculus, which isa variant of the λi calculus with the merge operator and disjoint intersection types. We createdProc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

294:8

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro

λM because, to integrate gradual typing with the merge operator more easily, we need to modify
some details of the semantics. In particular λM has a different form of values and a lazy semantics
for higher-order values [Wadler and Findler 2009] that is not present in λi . A side-benefit of thechanges in λM is that it leads to a standard type preservation theorem, whereas in λi the reduction
increases the precision of types and preservation has to be relaxed. The λM⋆ calculus is a gradualversion of the λM calculus, and adds the unknown type ⋆ to λM. The addition of ⋆ to the calculus
is nontrivial and leads to several changes in the semantics and the metatheory. We describe someof the key ideas next. The details are presented in Sections 3, 4 and 5.
Gradual Disjointness. In λi disjointness of types implies that Int is disjoint with Bool, but Int is
not disjoint with Int or Int & Bool. Disjointness has a simple specification: two types are disjoint if
they have no common supertypes, except for top-like types. Top-like types include ⊤ itself andtypes isomorphic to ⊤, such as ⊤&⊤. When using a simple subtyping relation with intersection
types, this definition of disjointness means that two function types are never disjoint: we canalways find common supertypes that are not top-like for any two functions [Oliveira et al. 2016].
Oliveira et al. shows some alternatives to allow functions to be disjoint. However, for simplicity
here, we adopt the simpler formulation by Oliveira et al. where functions cannot be disjoint.
When adding ⋆ to a calculus with disjointness, an interesting question is: How should ⋆ behavewith respect to disjointness? To define gradual disjointness, we use the existential lifting of thestatic relation from the Abstracting Gradual Typing (AGT) approach [Garcia et al. 2016]. With anexistential lifting we know that ⋆ is disjoint with A, if there exists some disjoint pair of static types
more precise than ⋆ and A. As ⊤ is more precise than ⋆, and ⊤ is disjoint with any other type, thenthis means that ⋆ is disjoint to any other type.
Ambiguity Errors and Type Errors. As expected, if we consider imprecise types, we need tocheck at runtime if disjointness is violated. For instance, (1 : ⋆ , , 2 : ⋆) : Int reduces to an error(Int is a possible supertype of ⋆). Otherwise the reduction would be non-deterministic: we could
choose any of the two integers. Now consider the reduction of (True : ⋆ , , 1 : ⋆) : Int. First,
as both components of the merge operator are suitable for casting, we cast both components to
Int: True : ⋆ ,→Int err and 1 : ⋆ ,→Int 1. Then as the left component reduces to an error, we
keep the right component and reduce the whole expression to 1. This approach is motivated by
the fact that Bool & Int is a subtype of Int. Therefore, by the type safety property of the static
type discipline, a program such as (True , , 1) : Int does not fail, using similar reasoning. Now
consider the expression ((1 : ⋆ , , 2 : ⋆) : ⋆ , , 3) : Int. We would like this expression to reduce toan error. However, the approach that we have adopted so far does not work. Let’s see why. First,(1 : ⋆ , , 2 : ⋆) : ⋆ ,→Int err due to ambiguity, and then 3 : ⋆ ,→Int 3. Then, as the left component
reduces to an error, we keep the right component and reduce the whole expression to 3. However,
we would like an error instead.
To avoid this problem, we differentiate two kinds of errors: ambiguity errors erra and type errors
errt . The expression (1 : ⋆, 2 : ⋆) : Int reduces to an ambiguity error erra , and 1 : ⋆ : Bool reduces toa type error errt . Going back to the last example ((1 : ⋆ , , 2 : ⋆) : ⋆ , , 3) : Int, as the left component
reduces to an ambiguity error, we propagate this error to the whole expression and reduce to erra .
Encoding the GT FL≲ Calculus and Modular Type-based Invariants. Garcia et al. [2016] developed agradually-typed lambda calculus with records and subtyping (GT FL≲ ) using the AGT methodology.
They use gradual rows ({li : Si , ⋆}) to represent records with incomplete type information. Extra
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

Merging Gradual Typing

294:9

fields, which are not reflected in the type, can be typed with ⋆. Two examples are given next.
({l1 = 1, l2 = True, l3 = . . . , . . .} : {l1 : Int, l2 : Bool}).l2 ,→∗ True({l1 = 1, l2 = True, l3 = . . . , . . .} : {l1 : Int, ⋆}).l2 ,→∗ True : ⋆In the first program, we have a record with multiple fields, but where only two fields are staticallyknown. The other fields are hidden via subtyping. The projection label l2 is contained in the record
type and value. Thus the program is well-typed. If we try to project l3 instead, the program is
ill-typed and it is statically rejected. The second program illustrates gradual rows. Although the
projected field is missing in the type, the value of l2 field can still be projected. Since the l2 field
is contained in the extra unknown part ⋆. Gradual rows allow extra fields to be projected andchecking whether fields are present is performed at runtime.
Gradual rows can be encoded easily in λM⋆ via merges, intersection types and the unknown
type in λM⋆ . The above programs are encoded in λM⋆ as follows.
(({l1 = 1} , , {l2 = True} , , {l3 = . . .} , , . . .) : {l1 : Int} & {l2 : Bool}).l2 ,→∗ True∗(({l1 = 1} , , {l2 = True} , , {l3 = . . .} , , . . .) : {l1 : Int} & ⋆).l2 ,→ True : ⋆

(1)
(2)

Compared to GT FL≲ , λM⋆ has extensible records (via the merge operator), whereas GT FL≲ only
supports fixed size records. Thus, GT FL≲ cannot immediately encode multiple inheritance directly(which can be supported via record concatenation) and, it cannot encode first-class classes anddynamic inheritance either. An important difference between GT FL≲ and our work is that GT FL≲
does not allow records with the same label to be present, even if these are in the dynamic parts of
the rows: GT FL≲ statically rejects records with repeated labels. This approach is possible to adopt
in GT FL≲ because, with fixed-sized records, all labels are statically known. However, this approachis problematic with extensible records and concatenation. Let us look at the following program:let f (x : ⋆)(y : ⋆) = x , , y in f {l1 = 1} {l1 = 2}
Here two dynamically typed expressions (x and y) are merged. If two records {l1 = 1} and {l1 =2} are passed as arguments to f, there will be ambiguity. There are two possible designs. We
could conservatively reject concatenation/merges with dynamic components. But this would beundesirable as it would prevent programs such as the gradual circle trait with an unknown superclasspresented earlier. The other option is to allow concatenating two records with unknown fields atruntime and check ambiguity errors at runtime, which is the approach that we take.
The dynamic semantics of λM⋆ does not preserve the semantics of GT FL≲ . Thus we do notprove an operational correspondence result. The first reason for this is that λM⋆ employs a lazy
semantics, whereas GT FL≲ uses an eager semantics for higher-order casts. The second reason isthat the original semantics of GT FL≲ [Garcia et al. 2016] fails to preserve some expected modular
type invariants. Although this definition has never been formally stated, it is associated with thestatic guarantees that types can provide regarding programs, such as parametricity granted bypolymorphism. Subtyping also provides modular type invariants. Consider A <: B and program:let x : B = new A() in e. By looking at the type of x, we know that e cannot use x as an A.
In the context of gradual typing, Bañados Schwerter et al. [2021] pointed out that the semantics
of GT FL≲ fails to preserve expected modular type invariants. Let us consider program let x : {l1 :Int} = {l1 = 5, l2 = True} in x. According to subtype-based reasoning of static typing, the l2 fieldshould not be accessed in the body of the let. However, for a gradually typed variant of the program:let x : {l1 : Int} = {l1 = 5, l2 = True} : ⋆ in (x : ⋆).l2 . the original formulation of GT FL≲ should
signal a run-time type error, but it does not. Instead it accesses the l2 field of the record. In essence,
the record preserves the hidden fields and allows them to be accessed later. When casting to ⋆ andback to the original record type, the l2 field is exposed.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

294:10

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro

As discussed in Section 2.2, calculi with the merge operator and disjoint intersection types
provide a solution for similar problems by enforcing the expected invariants using casting. Thissolution extends to a setting with gradual typing. The earlier example can be encoded in λM⋆ :(({l1 = 5} , , {l2 = True}) : ⋆ : {l1 : Int} : ⋆ : {l1 : Int} & {l2 : Bool}).l2,→ ({l1 = 5} : ⋆ : {l1 : Int} & {l2 : Bool}).l2 ,→ errt
When ({l1 = 5} , , {l2 = True}) : ⋆ is cast under {l1 : Int}, the field l1 is selected and l2 field is
dropped. Then, trying to cast the resulting record under {l1 : Int} & {l2 : Bool}, a type error is raisedsince the record no longer contains l2 .
The Dynamic Gradual Guarantee in λM⋆ . Siek et al. [2015b] proposed a set of criteria for gradualtyping that encompasses several properties. An important property is referred to as the dynamic
gradual guarantee (DGG), which relates to the notion of (im)precision. We say that one type is more
precise than another (A ⊑ B) if it provides more static information. For instance, Int & Bool ⊑Int & ⋆ ⊑ ⋆ & ⋆ ⊑ ⋆. Similarly, we say that one program is more precise than another if it has more
precise types. The DGG ensures that reduction is monotone with respect to imprecision.
The DGG requires special attention as it is in conflict with determinism. If we define the DGG as:
decreasing precision does not alter the behavior of the program (and does not introduce new errorsof any kind), then the DGG is not satisfied. To illustrate this, we provide a minimal example that
demonstrates this incompatibility. Consider the following program:((1 , , True) : Int , , (2 , , False) : Bool) : Bool,→ (1 , , (2 , , False) : Bool) : Bool ,→ (1 , , False) : Bool ,→ False
If we consider a less precise version of this program, ((1 , , True) : ⋆ , , (2 , , False) : ⋆) : Bool,a significant problem arises. We cannot determine which of the two merges should provide therequired boolean. Arbitrarily selecting the left merge would yield True, breaking the DGG. Arbitrarily choosing the right merge does not address this problem either. For instance, a slightly
different program ((1 , , True) : Int , , (2 , , False) : Bool) : Int reduces to 1, but a less precise
program ((1 , , True) : ⋆ , , (2 , , False) : ⋆) : Int would reduce to 2, also violating the DGG. Hence,in λM⋆ , this expression reduces to an ambiguity error erra . However, if the program is modified
to ((1 , , False) : ⋆ , , (2 , , False) : ⋆) : Bool, λM⋆ reduces to False since any path would yield thesame result. In our work we prove a variant of the DGG: decreasing precision does not alter the
behavior of the program modulo ambiguity errors (i.e. new type errors are not introduced).
Encoding First-Class Classes and Dynamic Inheritance. With λM⋆ we can encode a form of firstclass classes/traits and dynamic multiple inheritance with gradual typing. The encoding follows
an existing encoding of first-class traits employed in the SEDEL and CP programming languages.
The addition of gradual typing is essentially orthogonal to the existing encoding. The basic idea ofthe encoding is well-known and itself inspired by work on object encodings using records [Bruce
et al. 1999; Cardelli 1988; Cook and Palsberg 1989; Wand 1989]. In the well-known record encoding
records are used to model objects, record concatenation models (multiple) inheritance, classes (ortraits) can be modeled as functions parametrized by self-references that return records (objects), andfixpoints model class instantiation. In the translation of those ideas to λM⋆ , records are modeled
as merges of single field records, and record concatenation is just a special case of merges. For
example, a simplified version of the encoding, for the circle trait, in λM⋆ is:let circle = λsuper. (super,, {area = (λradius. pi * radius * radius) : ⋆ → int}) in
let obj = circle {} inobj.area 2
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

Merging Gradual Typing

Types
Ordinary Types
Expressions
Functionals
ValuesTerm contexts
FramesSyntactic sugar

294:11

A, B, C F Int | ⊤ | ⊥ | A → B | {l : A} | A & B
A F Int | A → B | {l : A}e F x | i | Top | λx. e | {l = e} | e.l | e : A | e1 e2 | e1 , , e2 | fix x. ef F λx. e | f : A → B
v F Top | i | f : A → B | v1 , , v2 | {l = v}
Γ F · | Γ, x : A
F F (λx. e) □ | □ e | □ : A | v , , □ | □ , , e | {l = □} | □.l{l1 : A1 ; . . . ; ln : An } ≜ {l1 : A1 } & · · · & {ln : An }{l1 = e1 ; . . . ; ln = en } ≜ {l1 = e1 } , , . . . , , {ln = en }Fig. 2. The syntax of the λM calculus.

In this example we omit the treatment of self references for simplicity of presentation. The idea isthat circle models the corresponding trait. To model the inheritance of a super trait, we simply use
the merge operator to merge super with the new methods. Furthermore, note that it is easy to model
multiple inheritance. For instance, we could modify the program above to take two super traits
super1 and super2 as arguments instead of super. Then we could simply use the merge operator tocompose all the super traits (super1,,super2) and then merge that with the additional methods.
Note also, that in this case super has an unknown type. We create an object by calling circle witha superclass, which for this example is empty. Then we call the area method in the object, to obtain
the area as a result. If we change the second line to:let obj = circle ({area = (λp. 1) : ⋆ → int}) inwith a super trait containing a conflicting area method, then an ambiguity error is raised at runtime
for the program. Since the addition of the unknown type is essentially orthogonal to the encoding,we can simply reuse previous encodings in λM⋆ to model a source language with first-class traits
or classes. Thus we omit a formal treatment of the encoding in this paper. For the formal treatmentof the encoding, and its full details, including the treatment of self-references, we refer the reader
to previous work on encoding first-class traits [Bi and Oliveira 2018; Zhang et al. 2021].
3

The λM Calculus: Syntax, Typing and Semantics

This section introduces the λM calculus: a variant of the λi calculus [Huang et al. 2021; Oliveira et al.
2016]. The main change is the adoption of lazy dynamic semantics for annotations on higher-ordervalues. The λM calculus is the static counterpart of the gradually typed calculus in Section 4.
3.1

SyntaxThe syntax of the λM calculus is shown in Figure 2. Meta-variables A, B, and C range over types.
There are base types (Int), the greatest type (⊤), the least type (⊥) and compound types. Compoundtypes are function types (A → B) or intersection types (A & B). A single field record type {l : A}
has a field l with type A. Multi-field record types are encoded by intersections of single field record
types [Reynolds 1997]. Ordinary types (A ) are types that are not intersection types, the top typeor the bottom type. They are the types of atomic values appearing in a merge.
Meta-variable e ranges over expressions. Most expressions are typical: variables (x); integers (i);a canonical top value (Top); annotated expressions (e : A); applications (e1 e2 ); lambda expressions(λx. e) and fixpoints (fix x. e). The merge of expressions e1 and e2 is denoted by (e1 , , e2 ). A record{l = e} stands for a single field record with label l and expression e. Selection of record fields isdone by the projection expression e.l. A merge of single field records encodes multi-field records.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

294:12

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro

⇔ F ⇒|⇐

Typing modesΓ ⊢e ⇔ A(Bidirectional Typing)⊢BΓ ⊢e ⇒ AΓ ⊢ e1 ⇒ A → BΓ ⊢ e2 ⇐ A

A <: BTyp-subΓ ⊢e ⇐ BΓ ⊢ e1 e2 ⇒ B

Γ, x : A ⊢ e1 ⇐ B
Γ ⊢ e2 ⇒ A
Typ-appΓ ⊢ (λx. e1 ) e2 ⇐ BΓ ⊢e ⇐ AΓ ⊢ Top ⇒ ⊤Typ-topΓ ⊢e:A ⇒ A⊢AΓ ⊢ i ⇒ Int

Typ-litΓ ⊢ {l = e} ⇒ {l : A}⊢A

Typ-abs

Typ-varΓ ⊢ e 1 , , e2 ⇒ A & B

Typ-rcd

Γ, x : A ⊢ e ⇐ AΓ ⊢ fix x. e ⇐ AA∗BΓ ⊢ e1 ⇒ A
Γ ⊢ e2 ⇒ B

x:A ∈ ΓΓ ⊢x ⇒ AΓ ⊢e ⇒ A
Typ-anno

Γ, x : A ⊢ e ⇐ BΓ ⊢ λx. e ⇐ A → B

Typ-rtTyp-fixA•l▷BΓ ⊢e ⇒ A
Typ-merge

Γ ⊢ e.l ⇒ B

Typ-proj

Fig. 3. The type system of the λM calculus.

Meta-variable f ranges over functionals, which are lambdas with zero or more function type
annotations. Meta-variable v ranges over values. Values include: integers i; the top value Top;
annotated functionals f : A → B; a merge of values v1 , , v2 and records {l = v}. This is different
from the λi calculus, where functional values only have a single annotation. This change is madeto delay the combination of function type annotations, to help gradualizing the calculus. Typing
context Γ tracks bound variables x with their type A. Meta-variable F ranges over frames [Sieket al. 2015a]. The frame is mostly standard but it includes annotated expressions, and merges.
Additionally, the frame for application (λx. e) □ restricts the function to be an unannotated lambda,
as applications of annotated lambdas are eliminated by annotating both the argument and theentire application.
3.2

Bidirectional Typing

Like λi , we use bidirectional type checking, to avoid a general subsumption rule. As shown by
previous work, a general subsumption rule is known to cause ambiguity in the presence of a merge
operator [Huang et al. 2021; Oliveira et al. 2016]. The typing judgment is represented as Γ ⊢ e ⇔ A.
The typing mode ⇔ is a metavariable, whose definition is shown at the top of Figure 3, and iseither inference (⇒) or checking (⇐). As in λi , besides disallowing non-disjoint merges, we donot support unrestricted intersections, which means that expressions like 1 : Int & Int, where theintersection in the type annotation is not disjoint, are not allowed.
Typing Relation. The typing relation of the λM calculus is shown in Figure 3. Most of the rules
follow the bidirectional type system of the λi calculus. In these rules, to avoid the ambiguity
introduced by the merge operator, the disjointness restriction on rule Typ-merge is used to rejectexamples such as 1 , , 2. The disjointness restriction applies to any types. We define an auxiliary
judgement ⊢ A, adopted from Oliveira et al. [2016], which defines well-formed types. The full
relation is mostly straightforward and shown in the extended version of the paper. The only notable
rule imposes a disjointness restriction on all intersection types. There is also a standard (omitted)
relation that checks if contexts are well-formed (i.e. all bound variables have well-formed types).
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

Merging Gradual Typing

294:13(Subtyping)A <: BA1 <: A2

B1 <: A1{l : A1 } <: {l : A2 }

S-rcd

S-z
Int <: Int

A1 <: A2A1 <: A3

A <: ⊤

A1 <: A3
S-andl
A1 & A2 <: A3

⊥⊔⊥

S-arr

S-andrS-bot

A1 & A2 <: A3A⊔B
co-intA1 → A2 <: B1 → B2

A2 <: A3S-and
A1 <: A2 & A3

Int ⊔ Int

S-top

A2 <: B2

co-bot⊥ <: A(Common Ordinary Super Types (COST))
co-ob
co-bo
⊥⊔A
A ⊔⊥
A1 ⊔ B(A1 → B1 ) ⊔ (A2 → B2 )co-arrA2 ⊔ B(A1 & A2 ) ⊔ B{l : A} ⊔ {l : B}

co-rcdA ⊔ B1co-andrA ⊔ (B1 & B2 )(A1 & A2 ) ⊔ B

co-andlA ⊔ B2co-randl

A ⊔ (B1 & B2 )co-randr

Fig. 4. Subtyping and the COST.

Furthermore, we add two more typing rules for records and projections. The typing rule for single
field records is standard (rule Typ-rcd). The type of a projection e.l is obtained by inferring thetype A of the expression being projected, and extracting the field type from A (rule Typ-proj) using
an auxiliary relation A • l ▷ B, which is shown in the extended version of the paper. Finally, there
is a typing rule Typ-rt that is only needed for proofs, and is used to type-check terms that only
arise in intermediate steps of reduction. Since lambdas do not have annotations in beta reduction,
the type information is obtained from the arguments.
3.3

Subtyping and Disjointness

Subtyping. The subtyping rules, which are mostly standard, are shown at the top of Figure 4.
Our rules follow the formalization by Davies and Pfenning [2000] but with an additional rule S-rcd
to incorporate record types. The extended subtyping relation is reflexive and transitive.
Disjointness. Our specification of disjointness follows one of the definitions in the original λi :Definition 3.1 (Disjointness Specification). A ∗spec B ≡ ∀C, A <: C ∧ B <: C =⇒ ⊤ <: CThis definition implies that the values that inhabit the two types cannot have overlapping types,
with the exception of top values. Such top values do not cause ambiguity because there is only
one canonical value of type top [Alpuim et al. 2017]. Furthermore, we define a simpler algorithmic
formulation based on a relation that checks whether two types have common ordinary super types(COST). To define the algorithmic formulation of disjointness, the Common Ordinary Super Types
Relation (COSTR) A ⊔ B is presented in the bottom of Figure 4. In essence values with ordinary
types are the atomic components (i.e. they cannot themselves be merges) of merges. If two types
have a COST then they overlap. For example Int & Bool and Int have the COST Int. When two
types have a COST in common they cannot be disjoint, since we can obtain a different value withthe same overlapping type from each value of the two types. Firstly, note that the top type is acommon supertype of every other type, but it is not a COST (since the top type is not ordinary).
Most rules are intuitive. One rule that deserves explanation rule co-arr: two functions have at
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

294:14

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toroleast one COST: ⊥ → ⊤. Thus, functions cannot be disjoint. For intersections, when A1 & A2 andone of the types A1 or B1 share ordinary supertypes with the other type B, we can easily conclude
that A1 & A2 has a COST with B (rules co-andl, co-andr, co-randl, and co-randr). With thehelp of the COSTR relation, an equivalent algorithmic formulation definition of disjointness is:Definition 3.2 (Algorithmic Disjointness). A ∗ B ≡ ¬(A ⊔ B)
3.4

Dynamic Semantics

The dynamic semantics of λM employs a type-directed operational semantics (TDOS) [Huang andOliveira 2020]. In TDOS, besides the usual reduction relation, there is a special casting relation forvalues that is used to convert values to the specified type. Casting is used by the TDOS reduction
relation, and it essentially gives an interpretation of type coercions at runtime.
Casting. The casting rules are shown at the top of Figure 5. Most of the rules directly follow λi .
Rule cast-top and rule cast-lit reduce the values according to the cast type. The main difference,compared to λi , is in rule cast-abs, which now employs a lazy semantics: functions accumulate
the casting function type (C → D) to the functional value. We return a record value after casting
the field value under the field type (rule cast-rcd). Rule cast-mergel and rule cast-merger
select a value from a merge of values (v1 , , v2 ) using an ordinary type A. Rule cast-and splits theintersection type used for the cast, and casts the value and each type separately.
Properties of Casting. Most of the properties of casting of λi hold here as well, and most proofs
are proved by induction on the casting derivation.
Some important properties of the casting relation are shown next.
Lemma 3.3 (Casting Determinism). If · ⊢ v ⇐ B, v ,→A v1 and v ,→A v2 then v1 = v2 .
Lemma 3.4 (Casting Preservation). If · ⊢ v ⇐ B, ⊢ A and v ,→A v ′ then · ⊢ v ′ ⇒ A.
Lemma 3.5 (Casting Progress). If · ⊢ v ⇐ A then ∃v ′ , v ,→A v ′ .
Lemma 3.3 says that the result of casting is unique. Note that the determinism lemma is nontrivial and only holds for well-typed values. Its proof requires reasoning about the properties ofwell-typed values. The casting relation preserves the type of the cast (Lemma 3.4), and there always
exists a result when the value is cast under A (Lemma 3.5).
Reduction. The reduction rules are shown at the bottom of Figure 5. Rule Step-eval is a standard
rule for evaluation contexts. Dealing with applications and beta reduction is interesting and different
from λi . Firstly, rule step-beta is standard beta reduction. Secondly, the top-level function annotation is eliminated by annotating the input types for arguments and output types for applications(rule step-app). In rule step-annov, annotated values v : A are evaluated by casting them under
the annotated types. However, (v : A) can be a (functional) value. In such case, since the expressionis already a value, it should not be reduced. Thus, we require the condition NotVal (v : A) which isdefined as not a functional value: NotVal e ≡ e ≠ (f : A → B). Fixpoints substitute themselves inthe body (rule step-fix). Rule Step-proj is for projections of record values. To project the fieldvalue, we cast the value v by the record type {l : A}. The field type A is obtained by projecting the
dynamic type of v by projection label l. The dynamic type for values ty(v) is:ty(i) = Intty(Top) = ⊤ty((f : A → B)) = A → Bty({l = p}) = {l : ty(p)}ty((v1 , , v2 )) = (ty(v1 )) & (ty(v2 ))An important property of a well-typed value is that its dynamic type is the inferred type of a value.
Lemma 3.6 (Dynamic Types). For any value v, if · ⊢ v ⇒ A then ty(v) = A.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

Merging Gradual Typing

294:15v ,→A v ′(Casting)
A → B <: C → D
cast-top

cast-lit
i ,→Int iv ,→⊤ Topv ,→A v ′′{l = v} ,→{l:A} {l = v }cast-rcd

v2 ,→A v2′
cast-merger
v1 , , v2 ,→A v2′

f : A → B ,→C→D f : A → B : C → D

cast-abs

v1 ,→A v1′
cast-mergel
v1 , , v2 ,→A v1′
v ,→A v1

v ,→B v2

cast-andv ,→A & B v1 , , v2

e ,→ e ′(Small-step Semantics)
e ,→ e ′F[e] ,→ F[e ′ ]Step-eval(λx. e) v ,→ e[x 7→ v]
v ,→A v ′Step-beta

Step-app(fix x. e) : A ,→ e[x 7→ (fix x. e) : A] : Aty(v) • l ▷ A

NotVal (v : A)v : A ,→ v ′(f : A1 → A2 ) e ,→ (f (e : A1 )) : A2

Step-annov

Step-fixv ,→{l:A} {l = v ′ }v.l ,→ v ′Step-proj

Fig. 5. Casting and small-step semantics for λM.

Finally, the λM calculus is deterministic and type sound:
Theorem 3.7 (Determinism). If · ⊢ e ⇔ A, e ,→ e1 and e ,→ e2 then e1 = e2 .
Theorem 3.8 (Type Preservation). If · ⊢ e ⇔ A and e ,→ e ′ then · ⊢ e ′ ⇔ A.
Theorem 3.9 (Progress). If · ⊢ e ⇒ A then e is a value or ∃e ′ , e ,→ e ′ .
4The λM⋆ Calculus : Syntax, Typing and Semantics

This section introduces the λM⋆ calculus, the gradual counterpart of λM. We prove determinism
and type soundness. Section 5 presents the gradual typing criteria satisfied by λM⋆ .
4.1

SyntaxThe syntax of λM⋆ calculus is shown in Figure 6. Types extend the types of λM calculus with the
unknown type (⋆). Because λM⋆ is gradually typed, runtime type errors are possible. Runtime typeerrors are denoted as errt for type errors, and erra for ambiguity errors. We use err∗ when the typeof the error is not important or inferred from the context. Results (r) can be any expressions or anerror err∗ . Meta-variable s ranges over ordinary values. Ordinary values include: integers i; the top
value Top; functional values and records with a value field {l = v}. Meta-variable g ranges overground values. Ground values are values with ground types (⊤, Int or dynamic compound types
such as ⋆ & ⋆). Meta-variable v stands for well-formed values. Values are either ordinary values s, amerge of values v1 , , v2 or ground values annotated with unknown type (g : ⋆). Compared to the
λM calculus, we extend values with dynamic ground values (g : ⋆).
To encode dynamically typed lambdas (i.e. lambdas without static type information) we needto insert ⋆ annotations. This approach is similar to the approach used in GTLC [Siek and Taha
2006], where an unannotated lambda λx. e is syntactic sugar for λ(x : ⋆). e. While we could apply aProc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

294:16

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro

Types
Expressions
Results
Functionals
Ordinary values
Ground values
ValuesTerm contexts
FramesA, B, C F Int | ⊤ | ⊥ | A → B | A & B | {l : A} | ⋆e F x | i | Top | λx. e | {l = e} | e.l | e : A | e1 e2 | e1 , , e2 | fix x. e
r F e | err∗f F λx. e | f : A → B
s F Top | i | f : A → B | {l = v}
g F Top | i | λx. e : ⋆ → ⋆ | f : ⋆ → ⋆ | {l = g : ⋆} | g : ⋆ , , g : ⋆v F s | v 1 , , v2 | g : ⋆Γ F · | Γ, x : A
F F (λx. e) □ | □ e | v , , □ | □ , , e | {l = □} | □.l | □ : A
Fig. 6. Syntax of the λM⋆ calculus.

similar transformation for λM⋆ terms, simply adding a ⋆ annotation in non-annotated lambdas, we
can do better in λM⋆ because of bidirectional type checking. We only need to insert annotations on
unannotated lambdas that are in inference positions. For example, given the dynamically typed expression (λf.λx. f x)(λy.y) we can obtain a well-typed λM⋆ program by automatically annotating
only one lambda abstraction: ((λf.λx. f x) : ⋆)(λy.y). Bidirectional type checking can propagate
type information to lambdas in checking positions. So, while those lambdas are unannotated, they
are still statically typed. This idea extends to dynamically typed fixpoints, which can be annotatedin a similar way. We show the details of this sugaring process in the extended version of the paper.
4.2

Consistent Subtyping and Disjointness

Consistent Subtyping. To integrate the type consistency and subtyping relations in gradual typing,
we follow the consistent subtyping approach in Xie et al. [2019]’s work, which was inspired byan earlier approach by Siek and Taha [2007]. The type consistency rules are at the top of Figure 7.
They are standard and proved to be reflexive and symmetric but not transitive. The subtyping rules
extend the subtyping rules of λM with a rule for dynamic types (rule S-dyn), where a dynamic
type is only a subtype of itself. Following Xie et al.’s approach, we add a premise in rule S-Top,
which restricts type A to be static. The subtyping rules are also reflexive and transitive.
The definition of consistent subtyping is supported by subtyping and consistency. Our consistentsubtyping relation is extended with intersection types and (single field) record types, and is shownin Figure 7. Consistent subtyping is proved to be equivalent to the declarative formulation of
consistent subtyping proposed by Xie et al. [2019]:
Lemma 4.1 (Consistent Subtyping). A ≲ B ≜ ∃A ′ B ′ . A <: A ′ and A ′ ∼ B ′ and B ′ <: B.
This specification defines consistent subtyping in terms of type consistency and subtyping, andis a useful guideline for the design of consistent subtyping relations. Note that, compared to thesubtyping relation, all the rules are essentially the same, with the exception of rules CS-dynl,
CS-dynr, and CS-top which have a different treatment from subtyping.
Disjointness and COSTR. To establish the specification of gradual disjointness (A ∗spec B), we
draw inspiration from AGT and lift the disjointness definition from λM, as follows:
Definition 4.2 (Disjointness Specification). A ∗spec B ≡ ∃ Static A ′ B ′ . A ′ ⊑ A ∧ B ′ ⊑ B ∧(∀ C, A ′ <: C ∧ B ′ <: C =⇒ ⊤ <: C)
We use an adapted version of the existential lifting of predicates, which relies on the precision
relation ⊑ between types, defined in Figure 7. Every type is more precise than itself and the unknown
type ⋆. The remaining rules are defined inductively. The original AGT existential lifting of predicates
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

Merging Gradual Typing

294:17A∼B(Type Consistency)

Int ∼ Int

⋆∼A

sim-i

⊤∼⊤

sim-dynlA∼⋆

sim-top⊥∼⊥A∼C

sim-dynrA∼C

sim-bot

B∼D

A&B ∼ C&D

B∼D

A→B∼C→D

sim-arr

A1 ∼ A2

sim-merge{l : A1 } ∼ {l : A2 }sim-rcd(Additional or Changed Subtyping Rules)

A <: B
Static A
S-Top

A <: ⊤

S-dyn⋆ <: ⋆(Consistent Subtyping)

A≲B
CS-z

CS-dynlCS-dynr⋆≲A

Int ≲ Int
B1 ≲ A1A2 ≲ B2

A1 → A2 ≲ B1 → B2
A1 ≲ A2⊥≲AA≲⋆
A1 ≲ A3

CS-arrCS-botA2 ≲ A3

CS-andl

A1 & A2 ≲ A3
A1 ≲ A3

CS-andA1 ≲ A2 & A3

A≲⊤

CS-topCS-andr

A1 & A2 ≲ A3
A1 ≲ A2{l : A1 } ≲ {l : A2 }CS-rcdA⊑B(Type Precision)
A1 ⊑ A2
A⊑A

tp-reflA1 ⊑ A2

A⊑⋆

tp-dyn(A1 → B1 ) ⊑ (A2 → B2 )tp-absA1 ⊑ A2

B1 ⊑ B2

A1 & B1 ⊑ A2 & B2

B1 ⊑ B2

tp-and{l : A1 } ⊑ {l : A2 }tp-rcdFig. 7. Consistency, Subtyping, Consistent Subtyping and Type Precision.

e
is as follows: P(A,B) = ∃ Static A ′ ∈ γ(A), Static B ′ ∈ γ(B).P(A ′ , B ′ ), where γ represents a
concretization function that maps gradual types to set of static types. As the precision relation in
AGT is also defined in terms of concretization (A ⊑ B ≡ γ(A) ⊆ γ(B)), the existential lifting ofepredicates can be equivalently expressed as P(A,B) = ∃ Static A ′ ⊑ A, Static B ′ ⊑ B.P(A ′ , B ′ ).
We provide a simplified definition of Def. 4.2 in the extended version of the paper, which does
not use existentials (proving its equivalence). Finally, the algorithmic definition of disjointness is
syntactically identical to the one in λM (as ⋆ is not related to any other gradual type in COSTR):A ∗ B ≡ ¬(A ⊔ B). This definition has been proven to be equivalent to both formal specifications.
4.3

Bidirectional Typing

As in the λM calculus, bidirectional typing is used. The typing rules are almost the same as thoseused by the λM calculus in Figure 3. New rules, or rules that are changed are shown next.
Typ-csTyp-app

Typ-abs⊢B
A≲B
Γ ⊢e ⇒ AΓ ⊢e ⇐ B

A ▷ A1 → A2
Γ ⊢ e1 ⇒ A
Γ ⊢ e2 ⇐ A 1
Γ ⊢ e1 e2 ⇒ A 2⊢ A1
A ▷ A1 → A2
Γ, x : A1 ⊢ e ⇐ A2
Γ ⊢ λx. e ⇐ A

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

294:18

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro

In gradual typing, the unknown type is used to allow some programs with runtime type errors.
We allow these kind of programs by changing the subsumption rule (rule Typ-sub) in Figure 3 torule Typ-cs, which now uses consistent subtyping instead of subtyping. For example, 1 : ⋆ : Booland True : ⋆ : Int are allowed by the new rule Typ-cs. Application and lambdas (rules Typ-app
and Typ-abs) use the match partial operator to deduce a function type from a gradual type. This
operator is defined as ⋆ ▷ ⋆ → ⋆, and A1 → A2 ▷ A1 → A2 . For projections, we allow programs
such as (({l1 = 1} , , True) : ⋆).l2 and ((1 , , True) : ⋆).l. The presence of a dynamic type relaxes
the type checker to allow projections from expressions with type ⋆. In the case that the label being
projected does not exist a runtime error is raised. The definitions of projection typing (A • l ▷ B)
and well-formed types for λM⋆ are shown in the extended version.
4.4

Casting

The casting rules are shown in the Figure 8. Because of runtime errors, the casting judgement
v ,→A r returns a result (r), which contains values v, type errors errt and ambiguous errors erra .
Casting ordinary values. Rule cast-top, rule cast-lit and rule cast-rcd are the same as λM calculus. To adapt to a gradual calculus, the subtyping premise of rule cast-Abs is updated to accountfor consistent subtyping.
Casting merges and intersection types. Rule cast-and mimics its static counterpart: it casts thevalue to both A and B. However, it also handles ambiguity errors and type errors. To achieve this,
this rule utilizes the r1 ∧ r2 = r3 meta-function defined at the bottom right side of Figure 8. The
cast reduces to an error if either of the results is an error, giving priority to type errors to maintain
determinism with respect to rule cast-err. Otherwise, it merges both results. Rule cast-merge
handles the case where a merge is cast to an ordinary type. Compared to λM, as both components
of a merge can have imprecise type annotations, the ordinary type can be a consistent supertypeof both types (e.g. (1 : ⋆, True) cast to Bool). Thus, we need to check dynamically if there is noambiguity (e.g. (1 : ⋆, 2) cast to Int). This rule first casts both components of the merge and then
combines the results using the meta-function r1 ∨ r2 = r3 defined at the bottom left side of Figure 8.
The cast reduces to a value if either both components reduce to the same value or one component
reduces to a value and the other to a type error. For example, if we cast (1 : ⋆, True) to Int, the left
and right components reduce to 1 and errt respectively, so we reduce to 1. Similarly, (1 : ⋆ , , 1) cast
to Int reduces to 1 as both branches reduce to the same value. However, in cases like (1 : ⋆ , , 2) , , 3
cast to Int, the left component would result in an ambiguity error and the right component would
yield 3. Instead of wrongly keeping the right component, we yield an ambiguity error. In otherwords, contrary to rule cast-and, we prioritize ambiguity errors over type errors.
Casting to and from unknown. Rules cast-sd and cast-mergd cast values to ⋆. In rule cast-sd,
ordinary values are cast to the top-level constructor of their type with the ground(A) function:
ground(⊤) = ⊤ ground(Int) = Int ground(A → B) = ⋆ → ⋆ ground({l : A}) = {l : ⋆}The result of this cast is a ground value, annotated with the ⋆ type to preserve types. We cast toa ground type, instead of just annotating the value with ⋆ directly, to allow dropping the ⋆ typewhen the ground value is used. For example, λx. x : Int → Int cast to ⋆ returns λx. x : Int →Int : ⋆ → ⋆ : ⋆ then, if the value is cast to Bool → Bool, the ⋆ type can be dropped safely toobtain λx. x : Int → Int : ⋆ → ⋆ : Bool → Bool. On the contrary, rule cast-mergd does not castthe merge value (v1 , , v2 ) to the type-level constructor ⋆ & ⋆. Otherwise it would create a cyclewith rule cast-and. Consider program (1 , , True) cast to ⋆. If we cast (1 , , True) to ⋆ & ⋆, thenby rule cast-and, we would yield casting from (1 , , True) to ⋆ again, forming a cycle. Therefore,
we cast v1 and v2 to ⋆ separately. For example, if (1 , , λx. x : Int → Int) is cast to ⋆, the dynamic
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

Merging Gradual Typing

294:19(Casting)

v ,→A rv ,→A vcast-top

cast-lit

A→B≲C→Df : A → B ,→C→D f : A → B : C → D
v ,→A r1

v ,→B r2

v ,→A & B r1 ∧ r2
v1 ,→⋆ v1′

v2 ,→A r2

v1 ,→A r1

cast-Absv1 , , v2 ,→A r1 ∨ r2
s ,→ground(ty(s)) g

cast-Andv2 ,→⋆ v2′
g : ⋆ ,→⋆ g : ⋆cast-sd

cast-botv ,→⊥ errt==verra where v1 ≠ v2r ∨ errt = rr ∨ erra = erra

cast-dynag : ⋆ ,→A r
v ,→A err∗

cast-errv∨v
v1 ∨ v 2
errt ∨ r = r
erra ∨ r = erra

cast-merge

g ,→A rcast-dd

Av ,→A errt

cast-rcds ,→⋆ g : ⋆cast-mergd
v1 , , v2 ,→⋆ (v1′ , , v2′ ) : ⋆ty(v){l = v} ,→{l:A} {l = v ′ }i ,→Int iv ,→⊤ Top′{l = v} ,→{l:A} err∗v 1 ∧ v2
erra ∧ errar ∧ errt = errtv ∧ erra = erra==

cast-rcdp

v 1 , , v2
erra
errt ∧ r = errt
erra ∧ v = erraFig. 8. Casting for the λM⋆ calculus.

annotated value (1 : ⋆ , , (λx. x : Int → Int : ⋆ → ⋆ : ⋆)) : ⋆ is returned. Rule cast-dd returns itself
since the value being cast already has type ⋆. Finally, rule cast-dyna casts dynamic ground values
to an ordinary type A. When (1 : ⋆ , , True) : ⋆ is cast to Int, it results in 1.
Casting to error. Rule cast-err raises a type error if the dynamic type of value v is not a consistentsubtype of the cast type. Rule cast-bot raises a type error when a value is cast to ⊥, to cover thecase when a value v of unknown type is cast to ⊥. Finally, rule Cast-rcdp propagates errors whena cast on the underlying value of a record fails.
4.5

Reduction

The reduction rules are shown in Figure 9. Rule Step-eval, rule Step-annov, rule Step-beta,
rule Step-app and rule Step-proj are the same as λM. However note that NotVal e is extended
to: NotVal e ≡ e ≠ (f : A → B) ∧ e ≠ g : ⋆. In gradually typed lambda calculi, errors may beraised at run-time. Therefore, rule Step-blame is designed to deal with that case. Rule Step-annop
can deal with the case where casting fails. Rule Step-projp shows that we need to consider thecase of projecting a value with unknown types, and the projection fails. There are three rules
related to beta reduction: rule Step-beta, rule Step-app and rule Step-dyn. Compared to λM,
rule Step-dyn is new. Because the unknown type ⋆ can be matched with ⋆ → ⋆ in applications((g : ⋆) e), (g : ⋆) should be annotated with ⋆ → ⋆ (rule Step-dyn). Then the lambda abstraction
can be extracted via casting (rule Step-annov) or filter the ill-typed values, which are hidden by
the type ⋆ (rule Step-annop). For example, both (1 : ⋆) 2 and ((1 , , λx. x : ⋆ → ⋆) : ⋆) 2 are well
typed. For the expression (1 : ⋆) 2, a type error is detected when rule Step-dyn annotates (1 : ⋆)with ⋆ → ⋆ and the cast fails via rule Step-annov. However the lambda value (λx. x : ⋆ → ⋆) isextracted for the second expression with a ⋆ → ⋆ annotation after using rule Step-annov.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

294:20

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro

(Small-step Semantics)

e ,→ re ,→ e′F[e] ,→ F[e ′ ]e ,→ err∗

Step-eval

Step-blame(λx. e) v ,→ e[x 7→ v]

F[e] ,→ err∗v ,→{l:A} {l = v ′ }ty(v) • l ▷ A(g : ⋆) e ,→ ((g : ⋆) : ⋆ → ⋆) ety(v) • l ▷ A

Step-dynv ,→{l:A} err∗

v.l ,→ v ′Step-projp

v ,→A v ′(f : A1 → A2 ) e ,→ (f (e : A1 )) : A2
v ,→A err∗

Step-app

Step-annop

Step-annov(λx. e) : ⋆ ,→ (λx. e) : ⋆ → ⋆ : ⋆(fix x. e) : A ,→ e[x 7→ (fix x. e) : A] : A

v : A ,→ err∗

Step-proj

NotVal (v : A)v : A ,→ v ′v.l ,→ err∗

Step-beta

Step-abs

Step-fix

Fig. 9. Semantics of λM⋆ .

Properties of Reduction. The λM⋆ calculus is deterministic and type sound. Theorem 4.3 saysthat the dynamic semantics is deterministic. Furthermore, the λM⋆ calculus preserves types(Theorem 4.4), and it has progress (Theorem 4.5).
Theorem 4.3 (Determinism). If · ⊢ e ⇔ A, e ,→ r1 and e ,→ r2 then r1 = r2 .
Theorem 4.4 (Type Preservation). If · ⊢ e ⇔ A and e ,→ e ′ then · ⊢ e ′ ⇔ A.
Theorem 4.5 (Progress). If · ⊢ e ⇒ A then e is a value or ∃r, e ,→ r.
Example. Finally, an example to demonstrate how reduction in λM⋆ works is:(((1 : ⋆) , , (λx. (x : Int) : ⋆ → ⋆ : ⋆)) : ⋆) (1 , , Top),→∗ {by rule Step-dyn, rule Step-eval, rule Step-app and rule Step-annov }((λx. (x : Int) : ⋆ → ⋆) (1 , , Top) : ⋆) : ⋆,→∗ {by rule Step-eval, rule Step-app, rule Step-beta and rule Step-annov }(1 : ⋆ , , Top : ⋆) : ⋆ : Int : ⋆ : ⋆,→∗ {by rule Step-eval and rule Step-annov }1:⋆
In this example, the lambda (λx. (x : Int) : ⋆ → ⋆) is extracted by casting ((1 : ⋆) , , (λx. (x : Int) :⋆ → ⋆ : ⋆)) to ⋆ → ⋆. The argument (1 , , Top) is cast with the function input type ⋆ to obtain(1 : ⋆ , , Top : ⋆) : ⋆. Then the argument is substituted into the function body and cast to Int. Finallythe expected result 1 : ⋆ is returned.
5

Gradual Typing Criteria and Encoding GTFL

In this section, we show that λM⋆ satisfies gradual typing criteria, and can encode the static
semantics of GT FL≲ [Garcia et al. 2016], which is a gradual calculus with records and subtyping. As
we have mentioned in Section 2.4, we need to employ a variant of the dynamic gradual guarantee.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

Merging Gradual Typing

294:21e1 ⊑ e2(Precision relation for expressions)e1 ⊑ e2e1 ⊑ e2e ⊑ e

ep-reflλx. e1 ⊑ λx. e2

e1 ⊑ e1′e2 ⊑ e2′

e1 e2 ⊑ e1′ e2′e1 ⊑ e1′

ep-abse2 ⊑ e2′e1 , , e2 ⊑ e1′ , , e2′

fix x. e1 ⊑ fix x. e2A⊑B

ep-appe1 ⊑ e2

e1 : A ⊑ e2 : B
e1 ⊑ e2

ep-merge{l = e1 } ⊑ {l = e2 }

ep-fixep-annoe1 ⊑ e2

ep-rcde1 .l ⊑ e2 .l

ep-proj

Fig. 10. Expression precision.

5.1

Conservative Extension, Static Gradual Guarantee and GTFL Encoding

Conservative Extension of the Static Discipline. We proved that if an expression is well-typed in
λM then it is well-typed in λM⋆ , which is shown in Theorem 5.1. Theorem 5.2 shows that for
any well-typed expressions, the dynamic semantics of λM can be encoded in λM⋆ . Note that afully-annotated expression means that all subexpressions are static, which are expressions in λM.
To be distinguishable, we use subscript m to represent typing or reduction from λM.
Theorem 5.1 (Eqivalence for fully-annotated terms (static)). Suppose that e is fully
annotated, Γ is well-formed and Γ , A are static. Γ ⊢ e ⇔m A if and only if Γ ⊢ e ⇔ A.
Theorem 5.2 (Eqivalence for fully-annotated terms (dynamic)). Suppose that e is fully
annotated, Γ is well-formed and Γ , A are static. If Γ ⊢ e ⇔m A then e ,→∗m v ⇐⇒ e ,→∗ v.
Static Gradual Guarantee. λM⋆ comes with a static gradual guarantee [Siek et al. 2015b], definedin terms of precision relations for types and expressions. We have already shown the precision fortypes. The precision relation for expressions is shown in Figure 10. e1 ⊑ e2 means that e1 is more
precise than e2 . Most of the rules are inductive and derived from the precision relation of types.
Theorem 5.3 shows that the static criteria of the gradual guarantee holds for the λM⋆ calculus: if e
is more precise than e ′ , e has type A then e ′ has type B, and type A is more precise than B.
Theorem 5.3 (Static Gradual Guarantee of the λM⋆ Calculus). If e ⊑ e ′ and · ⊢ e ⇔ Athen ∃B, · ⊢ e ′ ⇔ B and A ⊑ B.
Encoding the Static Semantics of the GT FL≲ Calculus. We proved that λM⋆ can encode the typesystem of the GT FL≲ calculus [Bañados Schwerter et al. 2021; Garcia et al. 2016]. In other words
every well-typed expression in the GT FL≲ calculus can be translated into a well-typed expression
in the λM⋆ calculus. The dynamic (lazy) semantics of λM⋆ does not preserve the (eager) semantics
of GT FL≲ . Thus we do not prove an operational correspondence result. An important difference inthe semantics is that the original semantics of GT FL≲ [Garcia et al. 2016] fails to preserve some
expected modular type invariants. However, as we discussed in Section 2, the λM⋆ calculus iscapable of smoothly dealing with the problem of modular type-based invariants.
The syntax and type system of GT FL≲ are shown in the Figure 11. Its expressions are standard
and the interesting part are the (gradual) types. Not only we have an unknown type ⋆, but also
we have gradual rows ({l : S, ⋆}), which represent rows with statically unknown extra fields. In
addition, the syntactic sugar {l : S, ∗} is used to represent either a normal multi-field record type({l : S}) or gradual row types ({l : S, ⋆}). The judgment Γ̄ ⊢ t : S { e has an elaboration step fromGT FL≲ expressions t to λM⋆ expressions e in the gray portion of the judgement. This elaboration
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

294:22

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro

SyntaxS F Int | S1 → S2 | {l : S} | {l : S, ⋆} | ⋆t F x | i | λx : S. t | {l = t} | t.l | t : S | t1 t2
Γ̄ F · | Γ̄ , x : S

GTypesExpressions
Term contextsΓ̄ ⊢ t : S { e(Typing)Γ̄ , x : S1 ⊢ t : S2 { ex : S ∈ Γ̄Γ̄ ⊢ x : S { xAty-varAty-absΓ̄ ⊢ λx : S1 . t : S1 → S2 { λx. e : | S1 | → | S2 |Γ̄ ⊢ t2 : S3 { e2S3 ≲ S1
Aty-iΓ̄ ⊢ t1 : S1 → S2 { e1Aty-appΓ̄ ⊢ t1 t2 : S2 { e1 e2Γ̄ ⊢ i : Int { iS ≲ S1Γ̄ ⊢ t : S { eAty-prjg l) { e.lΓ̄ ⊢ t.l : proj(S,Γ̄ ⊢ t : S { eAty-assertΓ̄ ⊢ (t : S1 ) : S1 { e : | S1 |Γ̄ ⊢ ti : Si { eiAty-recΓ̄ ⊢ {li = ti } : {li : Si } { {l1 = e1 } , , . . . , , {ln = en }g : S, li : Si , ∗}, l)proj({lg i : Si , ⋆}, l)proj({l==g l)proj(⋆,gproj(S, l)S⋆ if l ∉ {l̄i }⋆undef. otherwise==(Consistent Subtyping)S1 ≲ S2
ACS-z
Int ≲ Int

ACS-dynl

ACS-dynr

Si1 ≲ Si2
{li : Si1 , lj : Sj , ⋆} ≲ {li : Si2 , lk : Sk , ∗}S3 ≲ S1S2 ≲ S4S≲⋆

S1 → S2 ≲ S3 → S4

ACS-rcdr{li : Si1 , lj : Sj } ≲ {li : Si2 , ∗}⋆≲S

Si1 ≲ Si2

ACS-arr

ACS-rcdl

Fig. 11. Type System of GT FL≲ .

step is used to prove that λM⋆ can encode well-typed programs of GT FL≲ . Theorem 5.6 showsthat if a term t in GT FL≲ calculus is well-formed with type S and context Γ̄ and t elaborates to
λM⋆ expression e then e infers the type | S | and context | Γ̄ |. The definition of translation for types
and contexts are shown as follows.
Definition 5.4 (Type Translation). | S | translates the types of GT FL≲ to the types of λM⋆ .
| Int | = Int| ⋆ |=⋆| (S1 → S2 ) | = | S1 | → | S2 || {li : Si } | = {l1 : | S1 |} & . . . & {ln : | Sn |}| {li : Si , ⋆} | = {l1 : | S1 |} & . . . & {ln : | Sn |} & ⋆Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

Merging Gradual Typing

294:23⇒W⇐
k JA ⊑ BK = {(w1 , w2 ) | (w1 : A, w2 : B) ∈ Ek JA ⊑ BK}}⇒
Vk J⊤ ⊑ ⊤K = {(Top, Top)}}V⇒
k JInt ⊑ IntK = {(i, i)}}
V⇒
JA
→
A
⊑ B1 → B2 K = {(v1 , v2 ) | ∀j ⩽ k, ty(v1 ) = A1 → A2 , ty(v2 ) = B1 → B212k⇒(e1 , e2 ) ∈ E⇐
j JA1 ⊑ B1 K. (v1 e1 , v2 e2 ) ∈ Ej JA2 ⊑ B2 K}}⇒⇒
Vk J{l : A} ⊑ {l : B}K = {({l = v1 }, {l = v2 }) | (v1 , v2 ) ∈ Vk−1 JA ⊑ BK}}⇒V⇒
k JA1 &A2 ⊑ B1 &B2 K = {((v11 ,,v12 ), (v21 ,,v22 )) | (v11 , v21 ) ∈ Vk−1 JA1 ⊑ B1 K
∧ (v12 , v22 ) ∈ V⇒
JA
⊑
B
K}
}
2
2
k−1
⇒
V⇒
k JA ⊑ ⋆K = {(s1 , g : ⋆) | ∃s2 ∈ g : ⋆ ∧ (s1 , s2 ) ∈ Vk Jty(s1 ) ⊑ ty(s2 )K}}⇒∪ {(v1 ,,v2 , (g : ⋆)) | (v1 , (g : ⋆)) ∈ Vk−1 Jty(v1 ) ⊑ ⋆K
∧ (v2 , (g : ⋆)) ∈ V⇒
k−1 Jty(v2 ) ⊑ ⋆K}}
∪ {(g1 : ⋆, g2 : ⋆) | (g1 , g2 : ⋆) ∈ V⇒
k Jty(g1 ) ⊑ ⋆K}}
R⇔
JA
⊑
BK
=
{
(r
,
r
)
|
(r
=
err
)
∨
(r
=
err
∗
a )}}
1
2
1
2
k
∪ {(w1 , w2 ) | (w1 , w2 ) ∈ W⇔
JA
⊑
BK}}
k
E⇔
k JA ⊑ BK = {(e1 , e2 ) | ∀j < k, (e1 7−→j r1 ⇒ e2 7−→∗ r2∧ (r1 , r2 ) ∈ R⇔
k−j JA ⊑ BK)}}
GJΓ1 ⊑ Γ2 K = {(σ1 , σ2 ) | ∀k ⩾ 0, x ∈ dom(Γ1 ) ∩ dom(Γ2 ).
(σ1 (x), σ2 (x)) ∈ V⇒
k JΓ1 (x) ⊑ Γ2 (x)K}}
Γ1 ⊑ Γ2 ⊢ e1 ⊑ e2 ⇔ A ⊑ B ⇐⇒ ∀k ⩾ 0, (σ1 , σ2 ) ∈ GJΓ1 ⊑ Γ2 K. (σ1 (e1 ), σ2 (e2 )) ∈ E⇔
k JA ⊑ BK

s∈v

s∈s

s∈g
s∈g:⋆

Top ∈ ss ∈ v1s ∈ v1 ,,v2s ∈ v2s ∈ v1 ,,v2

Fig. 12. Logical relation.

Definition 5.5 (Context Translation). | Γ̄ | translates the typing context of GT FL≲ to the typing
context of λM⋆ .
| · |=·| Γ̄ , x : S | = | Γ̄ |, x : | S |Theorem 5.6 (Well-typed Encoding of GT FL≲ ). If Γ̄ ⊢ t : S { e then | Γ̄ | ⊢ e ⇒ | S |.
5.2

Dynamic Gradual Guarantee

Section 2 illustrates that the standard formulation of the DGG and determinism (Theorem 4.3) are
incompatible. In this section we present a relaxed notion of the DGG that states that reduction ismonotone with respect to imprecision, but modulo ambiguity errors. Instead of syntactic precision(defined in Figure 10), we use a semantic notion of precision [New et al. 2020]. To motivate thischoice, consider (syntactically) related expressions (1 , , True) : Int ⊑ (1 , , True) : ⋆. As the firstexpression reduces to 1, according to the DGG, the second expression should reduce to a related
value. But it reduces to (1 , , True) : ⋆ which is not related by the syntactic relation.
To address this, we define a semantic notion of precision using a step-indexed logical relation,
shown in Figure 12. The interpretations of values and expressions are mutually defined using
four category of sets: for irreducible values at check mode W⇐
k JA ⊑ BK, for values at infer mode
⇔
V⇒
JA
⊑
BK,
for
results
at
any
mode
R
JA
⊑
BK,
and
for
expressions or computations at anykkmode E⇔
JA
⊑
BK.
Each
categoryisindexed
by
the
step
index
k, the mode ⇔, and a pair of types.
kProc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

294:24

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro

An irreducible value w represents an irreducible expression that can be typed by the check mode,and can be a value v or a raw lambda λx.e. A pair of irreducible values are related at A ⊑ B andcheck mode, if the respective ascriptions to A and B yield related computations at infer mode.
Two values are related at the same base types, if the values are the same. Two values are related
at two function types, if their application to related expressions yield related computations. Notethat we use expressions as arguments (instead of values) in order to simplify the proofs. Two merge
values are related at two intersection types, if the first (resp. second) components of the merges are
related at the first (resp. second) components of the types.
The most complicated case is when the least precise type of the relation is ⋆. For this, we consider
three sub-cases. First, ordinary value s1 and dynamic value g : ⋆ are related if there exists a related
ordinary value s2 that can be projected from g : ⋆, denoted as s2 ∈ g : ⋆. The s2 ∈ g : ⋆ relation isdefined at the bottom of the Figure, and checks whether s2 is a subcomponent of g : ⋆. For example,
1 ∈ (1 , , True) holds, and Top ∈ v holds for any v. Going back to the first example in this section,
1 is now more precise than (1,,True) : ⋆ at Int ⊑ ⋆, because (1, 1) is related at Int ⊑ Int. Second, amerge and a dynamic value are related if each component of the merge is related to the dynamic
value. For example, 1 : Int&⊤ is more precise than 1 : ⋆. Program 1 : Int&⊤ reduces to 1,,Top while
1 : ⋆ is a value. They are related because 1 is related to 1 : ⋆, and Top with 1 : ⋆ (because Top ∈ 1 : ⋆).
Third, two dynamic values are related if the underlying first ground value is related to the second
dynamic value at the underlying ground type and ⋆. Although some cases do not reduce the index
k, the relation is well-founded because each recursive occurrence will eventually lower the index.
Two results are related to some mode if either (1) the first result is an error, (2) the second result
is an ambiguity error, or (3) the results are related irreducible values at the same mode. Note thatthe relation for irreducible values at infer mode W⇒
k JA ⊑ BK is defined as the relation for values
at the same mode V⇒
JA
⊑
BK.
A
pair
of
expressions(e1 , e2 ) are related at k steps and some modek
⇔ if, when e1 reduces to a result in j steps, e2 must reduce to a related result at k − j steps within
the same mode. A pair of type environments are related if every variable maps to a related value atinfer mode.
Finally, we use notation Γ1 ⊑ Γ2 ⊢ e1 ⊑ e2 ⇔ A ⊑ B to denote that expression e1 is semanticallymore precise than e2 under related type environments Γ1 ⊑ Γ2 at related types A ⊑ B and somemode ⇔, if the expressions, closed under related value environments, are related expressions forany number of steps k. For simplicity, if contexts are empty we use notation ⊢ e1 ⊑ e2 ⇔ A ⊑ B.
Armed with the logical relation and semantic precision, we can establish the fundamental
property that states that well-typed expressions related by the syntactic precision relation are
related by the semantic precision relation.
Theorem 5.7 (Fundamental Property).
(1) if Γ1 ⊢ e1 ⇒ A, Γ2 ⊢ e2 ⇒ B and e1 ⊑ e2 then Γ1 ⊑ Γ2 ⊢ e1 ⊑ e2 ⇒ A ⊑ B.
(2) if Γ1 ⊢ e1 ⇐ A, Γ2 ⊢ e2 ⇐ B and e1 ⊑ e2 then Γ1 ⊑ Γ2 ⊢ e1 ⊑ e2 ⇐ A ⊑ B.
The key lemma to prove this theorem is the ascription lemma, which states that the ascriptionsof related values to related types, yield related expressions.
′′′′Lemma 5.8 (Ascription Lemma). if (v1 , v2 ) ∈ V⇒
k JA ⊑ B K ∧ A ≲ A ∧ B ≲ B ∧ A ⊑ B⇒
then (v1 : A, v2 : B) ∈ Ek JA ⊑ BK.

Finally, based on the fundamental property, we can establish the DGG modulo ambiguity errors.
We use e ⇑ to denote that e diverges.
Theorem 5.9 (Dynamic Gradual Guarantee). Suppose that ⊢ e1 ⇔ A, ⊢ e2 ⇔ B and e1 ⊑ e2 .
(1) e1 7−→∗ v1 then ((e2 7−→∗ v2 and ⊢ v1 ⊑ v2 ⇔ A ⊑ B) or e2 7−→∗ erra ).
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

Merging Gradual Typing

294:25(2) e1 ⇑ then e2 ⇑ or e2 7−→∗ erra .
(3) e2 7−→∗ v2 then ((e1 7−→∗ v1 and ⊢ v1 ⊑ v2 ⇔ A ⊑ B) or e1 7−→∗ err∗ ).
(4) e2 ⇑ then e1 ⇑ or e1 7−→∗ err∗ .
Cases (1) and (2) are similar to the original DGG [Siek et al. 2015b] except for the fact thatthe less precise expression can reduce to an ambiguity error. Case (2) may be counter-intuitive,in particular when e2 reduces to erra , so we provide a simple example that illustrates this case.
Let Ω = ((λx.x x) (λx.x x)). Expression ((((1,,True) : Bool),,2) : Int),,Ω diverges, but lessprecise expression ((((1,,True) : ⋆),,2) : Int),,Ω raises an ambiguity error. Cases (3) and (4) also
include instances where the most precise expression can reduce to an ambiguity error. To illustratecase (3), consider value ((1 : ⋆),,2) : ⋆. The more precise expression ((1 : ⋆),,2) : Int reduces toan ambiguity error. For case (4), (((1 : ⋆),,2) : ⋆),,Ω diverges but the more precise expression(((1 : ⋆),,2) : Int),,Ω reduces to an ambiguity error.
6

Related Work

In Section 2 we already discussed the most closely related work. Thus here we will only briefly
summarize key points and discuss other closely related work.
Gradual Objects. Siek and Taha [2007] designed a calculus (Ob?<: ), which extended Ob<: [Abadi
and Cardelli 1996] with the unknown type ⋆. Although the unknown type ⋆ is powerful and generalfor gradual typing, there is a significant loss of information with record types and subtyping. To
solve this, Garcia et al. [2016] proposed a new kind of gradual type called gradual row. A gradual row
type ({li : Si , ⋆}) has extra (statically) unknown fields in the record type. With gradual rows, Garcia
et al. [2016] defined a calculus with records and subtyping named GT FL≲ by using the Abstracting
Gradual Typing (AGT) methodology. GT FL≲ represents gradual typing derivations as intrinsically
typed terms to give dynamic semantics directly instead of elaborating to an intermediate language.
As Bañados Schwerter et al. [2021] point out GT FL≲ fails to enforce modular invariants, which
are expected from the static type discipline. They address the problems by refining the underlying
theory of AGT dynamic checking, and have also designed their calculus to be space efficient. Since
we employ a conventional lazy semantics, λM⋆ is not space efficient. Sekiyama and Igarashi [2019]
generalize gradual row types to variant types and row polymorphism [Wand 1994]. Compared to
GT FL≲ , their records are extensible. However, they drop subtyping, in favour of row polymorphism.
As we have shown, λM⋆ can encode the static semantics of GT FL≲ and gradual rows using single
field record types, intersection types and the unknown type ⋆. Furthermore, with λM⋆ , records areextensible, by employing the merge operator as record concatenation, and subtyping is supported.
Thus, not only λM⋆ can encode multiple inheritance, but it can encode dynamic inheritance andfirst-class traits/classes as well. Because AGT gradual rows have fixed size, there is no concatenation
and ambiguity is statically rejected (records with repeated labels are not allowed). Thus, it is notpossible to encode dynamic inheritance and first-class classes. Finally, casting in λM⋆ preserves
the modular invariants expected from the static type discipline naturally.
Based on their earlier work in Nom [Muehlboeck and Tate 2017], Muehlboeck and Tate [2021]
present MonNom: a gradual language supporting seamless transition between untyped structuraland typed nominal paradigms. They propose a novel approach to transitioning from untyped
structural objects to nominal objects. Precision between types is restricted as any type is more
precise than itself or the unknown type, disallowing precision between different partially untyped
types. Precision between expressions is complex, as it enables the correlation of untyped structural
code with nominal code. The authors provide proof for both gradual guarantees and type safety.
Unlike λM⋆ , MonNom does not support dynamic inheritance and first-class traits/classes. Instead
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

294:26

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro

MonNom’s focus is on improving the performance of more conventional (gradual) OOP languages.
In the future we hope to learn from Nom and MonNon to improve the performance of λM⋆ .
First-Class Classes and Traits. Many dynamically-typed languages support first-class classes/traits,
including Racket [Flatt et al. 2006] or JavaScript. To type first-class classes, Takikawa et al. [2012]extended Racket with a gradual type system, called TFCC, for first-class classes. TFCC consists of
two parts: an untyped portion and a typed portion of the language. The interactions between thetwo portions are mediated by contracts. Row polymorphism [Wand 1994] is used to type mixins.
Compared to λM⋆ , TFCC mixes typed and untyped modules instead of allowing fine-grained
gradual typing at the level of expressions. TFCC can have fully typed modules, dynamically typed
modules and these modules can interoperate with each other. However TFCC cannot have a modulethat mixes static and dynamically typed expressions. In contrast the form of gradual typing in
λM⋆ is more fine-grained and it works at the level of expressions. Moreover, λM⋆ is a lower leveland simpler language, since it is basically a lambda calculus extended with merges and single label
records. So, high-level constructs like classes/traits are encodable in terms of simpler, more atomic
constructs. In contrast, TFCC is significantly more complex, as it has a built-in notion of classes,
and requires both a form of row polymorphism and subtyping for modelling first-class classes.
Some statically typed calculi support first-class classes, but do not support gradual typing. Tagged
objects are used to type first-class classes by Lee et al. [2015]. SEDEL was proposed by Bi andOliveira [2018] to type first-class traits. The type system of SEDEL is based on disjoint intersection
types [Oliveira et al. 2016] and disjoint polymorphism [Alpuim et al. 2017]. In SEDEL traits areelaborated into a target calculus with the merge operator and disjoint intersection types. The later
CP language [Zhang et al. 2021] also adopts a similar approach to typed-first class traits.
Gradual Typing with Intersection Types. Castagna and Lanvin [2017] developed a gradual typing
system with union and intersection types using set-theoretic types. They show how to lift definitions,such as subtyping, from non-gradual types to gradually typed ones. There are two main parts: agradually-typed language with its type system, and a cast calculus. The dynamic semantics is givenin the cast calculus. In later work, Castagna et al. [2019] improved the work of Castagna and Lanvin[2017] with a blame calculus style dynamic semantics and blame labels. An important difference tothis line of work is that λM⋆ includes a merge operator, which brings significant complications,such as the issue of ambiguity or type safety in the presence of subtyping in merges.
7

Conclusion and Future Work

This paper presented a calculus, called λM⋆ , that unifies two type-directed mechanisms: gradualtyping and the merge operator. We prove that λM⋆ is type sound, deterministic and satisfies thegradual guarantee. λM⋆ is expressive, and it can encode gradual rows and the GT FL≲ calculus
using intersection types and the merge operator. In addition λM⋆ has extensible records via themerge operator and it can encode first-class classes/traits and dynamic inheritance following an
existing encoding by Bi and Oliveira [2018]. This brings λM⋆ closer to dynamically typed languages,
such as JavaScript, which are common targets for practical implementations of gradual typing.
There are still several important gaps between λM⋆ and languages such as TypeScript. In
particular λM⋆ in purely functional, and omits imperative features like references [Toro andÉric Tanter 2020], as well as other common features such as polymorphism [Ahmed et al. 2011].
References will require some further study. Although there is already some work integratingreferences and polymorphism in a TDOS with gradual typing [Ye and Oliveira 2023], merges havenot been considered. An issue that is important to study is related to the notion of object identity,
which most OOP languages rely on. In our work, due to our coercive semantics, we essentiallycreate proxy objects around existing objects. However proxy objects may have a different object
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

Merging Gradual Typing

294:27

identity. We expect to be able to address this issue by building on existing research on transparent
proxies [Keil et al. 2015], which aims at addressing such concerns with proxy objects.
On the more theoretical side, it will be interesting to study a general framework for type-directedmechanisms and look at integrating other type-directed mechanisms such as type classes [Wadler
and Blott 1989] or implicits [Oliveira et al. 2010].
An important question that we have not touched in this paper is performance. There are at least
three points that deserve further study in the future. Firstly, we are interested in exploring a variantof λM⋆ with either threesomes [Siek and Wadler 2009], or an eager semantics for higher-order casts.
Both of these can help avoid the accumulation of type annotations, which are known to cause timeand space inefficiencies [Herman et al. 2010]. Secondly, in its current form, all applications in the
TDOS are flexible. Since applications in the TDOS model the semantics of a source gradual language,
they allow mismatched (but consistent) types between arguments and functions, thus requiring
casting. To address this performance drawback, a possible solution is to introduce strict forms ofapplications, alongside flexible applications, where the type of the argument must exactly match the
expected input type of the function. In this way casting can be avoided for strict applications. This
would be somewhat analogous to optimization techniques used in OOP languages, where somedynamically dispatched method calls can be optimized to statically dispatched method calls. Adding
strict applications could be complemented with further optimizations that removes unnecessary
annotations such as in (λx. x : Int → Int) (1 : Int). Finally, runtime ambiguity detection is costly. It
is possible to avoid runtime ambiguity detection by forbidding merges with unknown types. But
this would be quite restrictive. A better solution would be to detect static merges (merges without
components with unknown types) and employ an optimized version of casting without ambiguity
detection. This should be possible because, for static merges, all ambiguity can be statically detected.
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.
Data-Availability Statement
The artifact that supports the paper is available on Zenodo [Ye et al. 2024].
References
Martín Abadi and Luca Cardelli. 1996. A Theory of Objects. In Monographs in Computer Science.
Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011. Blame for All. In Proceedings of the 38th Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Austin, Texas, USA) (POPL ’11). Association
for Computing Machinery, New York, NY, USA, 201–214. https://doi.org/10.1145/1926385.1926409
João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. 2017. Disjoint Polymorphism. In ESOP.
Felipe Bañados Schwerter, Alison M. Clark, Khurram A. Jafery, and Ronald Garcia. 2021. Abstracting Gradual Typing
Moving Forward: Precise and Space-Efficient. Proc. ACM Program. Lang. 5, POPL, Article 61 (jan 2021), 28 pages.
https://doi.org/10.1145/3434342
Xuan Bi and Bruno C. d. S. Oliveira. 2018. Typed First-Class Traits. In ECOOP.
Gilad Bracha and William Cook. 1990. Mixin-Based Inheritance. In Proceedings of the European Conference on Object-Oriented
Programming on Object-Oriented Programming Systems, Languages, and Applications (Ottawa, Canada) (OOPSLA/ECOOP’90). Association for Computing Machinery, 303–311.
Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce. 1999. Comparing Object Encodings. Inf. Comput. 155, 1-2 (1999),
108–133.
Luca Cardelli. 1988. A Semantics of Multiple Inheritance. Inf. Comput. 76, 2/3 (1988), 138–164.
Luca Cardelli and John C. Mitchell. 1991. Operations on records. Mathematical Structures in Computer Science 1, 1 (1991),
3–48.
Giuseppe Castagna and Victor Lanvin. 2017. Gradual typing with union and intersection types. Proceedings of the ACM on
Programming Languages 1, ICFP (2017), 1–28.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 294. Publication date: October 2024.

294:28

Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro

Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek. 2019. Gradual typing: a new perspective.
Proceedings of the ACM on Programming Languages 3 (2019), 1 – 32.
William R. Cook and Jens Palsberg. 1989. A denotational semantics of inheritance and its correctness. In Object-Oriented
Programming: Systems, Languages and Applications (OOPSLA).
Rowan Davies and Frank Pfenning. 2000. Intersection types and computational effects. In Proceedings of the Fifth ACM
SIGPLAN International Conference on Functional Programming (ICFP ’00), Montreal, Canada, September 18-21, 2000, Martin
Odersky and Philip Wadler (Eds.). ACM, 198–208. https://doi.org/10.1145/351240.351259
Jana Dunfield. 2014. Elaborating intersection and union types. Journal of Functional Programming (JFP) 24, 2-3 (2014),
133–165.
Erik Ernst. 2000. gbeta-a language with virtual attributes, Block Structure, and Propagating, Dynamic Inheritance. DAIMI
Report Series 29, 549 (2000).
Matthew Flatt, Robert Bruce Findler, and Matthias Felleisen. 2006. Scheme with Classes, Mixins, and Traits. In APLAS.
Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting Gradual Typing. SIGPLAN Not. 51, 1 (jan 2016), 429–442.
https://doi.org/10.1145/2914770.2837670
Ben Greenman. 2023. GTP Benchmarks for Gradual Typing Performance. In REP. ACM, 102–114. https://doi.org/10.1145/
3589806.3600034
Ben Greenman, Asumu Takikawa, Max S. New, Daniel Feltey, Robert Bruce Findler, Jan Vitek, and Matthias Felleisen.
2019. How to evaluate the performance of gradual type systems. Journal of Functional Programming 29 (2019), 45.
https://doi.org/10.1017/S0956796818000217
David Herman, Aaron Tomb, and Cormac Flanagan. 2010. Space-efficient gradual typing. Higher-Order and Symbolic
Computation 23, 2 (2010), 167.
Xuejing Huang and Bruno C. d. S. Oliveira. 2020. A Type-Directed Operational Semantics For a Calculus with a Merge
Operator. In 34th European Conference on Object-Oriented Programming (ECOOP 2020) (Leibniz International Proceedings inInformatics (LIPIcs), Vol. 166), Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl–Leibniz-Zentrum für Informatik,
Dagstuhl, Germany, 26:1–26:32. https://doi.org/10.4230/LIPIcs.ECOOP.2020.26
Xuejing Huang, Jinxu Zhao, and Bruno C. d. S. Oliveira. 2021. Taming the Merge Operator. Journal of Functional Programming
31 (2021), e28.
Matthias Keil, Sankha Narayan Guria, Andreas Schlegel, Manuel Geffken, and Peter Thiemann. 2015. Transparent Object
Proxies in JavaScript. In 29th European Conference on Object-Oriented Programming, ECOOP 2015, July 5-10, 2015, Prague,
Czech Republic (LIPIcs, Vol. 37), John Tang Boyland (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 149–173.
Andre Kuhlenschmidt, Deyaaeldeen Almahallawi, and Jeremy G. Siek. 2019. Toward Efficient Gradual Typing for Structural Types via Coercions. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and
Implementation (Phoenix, AZ, USA) (PLDI 2019). Association for Computing Machinery, New York, NY, USA, 517–532.
https://doi.org/10.1145/3314221.3314627
Joseph Lee, Jonathan Aldrich, Troy Shaw, and Alex Potanin. 2015. A Theory of Tagged Objects. In ECOOP.
Fabian Muehlboeck and Ross Tate. 2017. Sound Gradual Typing is Nominally Alive and Well. Proc. ACM Program. Lang. 1,
OOPSLA, Article 56 (oct 2017), 30 pages. https://doi.org/10.1145/3133880
Fabian Muehlboeck and Ross Tate. 2021. Transitioning from structural to nominal code with efficient gradual typing. Proc.
ACM Program. Lang. 5, OOPSLA (2021), 1–29. https://doi.org/10.1145/3485504
Max S. New, Dustin Jamner, and Amal Ahmed. 2020. Graduality and parametricity: together again for the first time. Proc.
ACM Program. Lang. 4, POPL (2020), 46:1–46:32. https://doi.org/10.1145/3371114
Bruno C.d.S. Oliveira, Adriaan Moors, and Martin Odersky. 2010. Type Classes as Objects and Implicits. In Proceedings of
the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA ’10).
341–360.
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
John C Reynolds. 1997. Design of the programming language Forsythe. In ALGOL-like languages. 173–233.
Taro Sekiyama and Atsushi Igarashi. 2019. Gradual Typing for Extensibility by Rows. ArXiv abs/1910.08480 (2019).
Jeremy Siek, Peter Thiemann, and Philip Wadler. 2015a. Blame and Coercion: Together Again for the First Time. In Proceedingsof the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (Portland, OR, USA) (PLDI’15). Association for Computing Machinery, New York, NY, USA, 425–435. https://doi.org/10.1145/2737924.2737968
Jeremy G. Siek and Walid Taha. 2006. Gradual typing for functional languages. In Scheme and Functional Programming
Workshop, Vol. 6. 81–92.
Jeremy G. Siek and Walid Taha. 2007. Gradual Typing for Objects. In ECOOP.
Jeremy G Siek, Michael M Vitousek, Matteo Cimini, and John Tang Boyland. 2015b. Refined criteria for gradual typing. In
1st Summit on Advances in Programming Languages (SNAPL 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

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

Merging Gradual Typing

294:29Jeremy 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
Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. 2016. Is Sound Gradual
Typing Dead? (POPL ’16). Association for Computing Machinery, New York, NY, USA, 456–468. https://doi.org/10.1145/
2837614.2837630
Asumu Takikawa, T. Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. 2012. Gradual
Typing for First-Class Classes. SIGPLAN Not. 47, 10 (oct 2012), 793–810. https://doi.org/10.1145/2398857.2384674
Sam Tobin-Hochstadt and Matthias Felleisen. 2006. Interlanguage migration: from scripts to programs. https://doi.org/10.
1145/1176617.1176755
Matías Toro and Éric Tanter. 2020. Abstracting gradual references. Science of Computer Programming 197 (2020), 102496.
https://doi.org/10.1016/j.scico.2020.102496
P. Wadler and S. Blott. 1989. How to Make Ad-hoc Polymorphism Less Ad Hoc. In Proceedings of the 16th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL ’89).
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
Mitchell Wand. 1989. Type Inference for Record Concatenation and Multiple Inheritance. In Symposium on Logic in Computer
Science (LICS).
Mitchell Wand. 1994. Type inference for objects with instance variables and inheritance.
Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. Consistent Subtyping for All. ACM Trans. Program.
Lang. Syst. 42, 1, Article 2 (nov 2019), 79 pages. https://doi.org/10.1145/3310339
Wenjia Ye and Bruno C. d. S. Oliveira. 2023. Pragmatic Gradual Polymorphism with References. In Programming Languages
and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferenceson Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings (Lecture Notes in Computer
Science, Vol. 13990), Thomas Wies (Ed.). Springer, 140–167.
Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang. 2021. Type-Directed Operational Semantics for Gradual Typing.
In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Schloss Dagstuhl-Leibniz-Zentrum fürInformatik.
Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro. 2024. Merging Gradual Typing (Artifact). https://doi.org/10.5281/zenodo.
13378311
Weixin Zhang, Yaozhu Sun, and Bruno C. d. S. Oliveira. 2021. Compositional Programming. ACM Trans. Program. Lang.
Syst. 43, 3, Article 9 (sep 2021), 61 pages. https://doi.org/10.1145/3460228

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

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