JFP, pages, . © Cambridge University Press

1

Type-Directed Operational Semantics for
Gradual Typing
WENJIA YE

BRUNO C. D. S. OLIVEIRAThe University of Hong Kong(e-mail: {wjye , bruno}@cs.hku.hk)

Abstract
The semantics of gradually typed languages is typically given indirectly via an elaboration into a castcalculus. This contrasts with more conventional formulations of programming language semantics,
where the semantics of a language is given directly using, for instance, an operational semantics.
This paper presents a new approach to give the semantics of gradually typed languages directly.
We use a recently proposed variant of small-step operational semantics called type-directed operational semantics (TDOS). In a TDOS, type annotations become operationally relevant and can affectthe result of a program. In the context of a gradually typed language, type annotations are used totrigger type-based conversions on values. We illustrate how to employ a TDOS on gradually typed
languages using two calculi. The first calculus, called λ Bg , is inspired by the semantics of the blame
calculus, but it has implicit type conversions, enabling it to be used as a gradually typed language.
The second calculus, called λ e, explores an eager semantics for gradually typed languages using a
TDOS. For both calculi, type safety is proved. For the λ Bg calculus, we also present a variant withblame labels, and illustrate how the TDOS can also deal with such an important feature of gradually
typed languages. We also show that the semantics of λ Bg with blame labels is sound and complete with respect to the semantics of the blame calculus, and that both calculi come with a gradualguarantee. All the results have been formalized in the Coq theorem prover.

1 Introduction
Gradual typing aims to provide a smooth integration between the static and dynamic typing disciplines. In gradual typing, a program with no type annotations usually behaves
as a dynamically typed program1 , whereas a fully annotated program behaves as a statically typed program. The interesting aspect of gradual typing is that programs canbe partially typed in a spectrum ranging from fully dynamically typed into fully statically typed. Several mainstream languages, including TypeScript (Bierman et al., 2014),
Flow (Chaudhuri et al., 2017) or Dart (Bracha, 2015) enable forms of gradual typing tovarious degrees. Much research on gradual typing has focused on the pursuit of soundgradual typing (Siek & Taha, 2006, 2007; Wadler & Findler, 2009), where certain typesafety properties, and other properties about the transition between dynamic and static
typing, are preserved.
The semantics of gradually typed languages is typically given indirectly via an elaboration into a cast calculus. For instance, the blame calculus (Wadler & Findler, 2009; Siek
1

In some gradually typed calculi with type inference, programs without annotations can still be statically
typed (Garcia & Cimini, 2015).

2

Type-Directed Operational Semantics for Gradual Typing

et al., 2015a), the threesome calculus (Siek & Wadler, 2009) or other cast calculi (Findler& Felleisen, 2002; Gray et al., 2005; Henglein, 1994; Tobin-Hochstadt & Felleisen, 2006;
Siek et al., 2015a, 2009) are often used to give the semantics of gradually typed languages.
Since a gradual type system can accept programs with unknown types, run-time checks arenecessary to ensure type safety. Thus, the job of the (type-directed) elaboration is to insert
casts that bridge the gap between known and unknown types. Then the semantics of a castcalculus can be given in a conventional manner.
While elaboration is the most common approach to give the semantics for gradually
typed languages, it is also possible to have a direct semantics. In fact, a direct semantics
is more conventionally used to provide the meaning to more traditional forms of calculi
or programming languages. A direct semantics avoids the extra indirection of a target language and can simplify the understanding of the language. Garcia et al. (2016), as part oftheir Abstracting Gradual Typing (AGT) approach, advocated and proposed an approachfor giving a direct semantics to gradually typed languages. They showed that the cast insertion step provided by elaboration, which was until then seen as essential to gradual typing,
could be omitted. Instead, in their approach, they develop the dynamic semantics as proof
reductions over source language typing derivations.
We present a different approach to give the semantics of gradually typed languages
directly. We use a recently proposed variant of small-step operational semantics (Wright& Felleisen, 1994) called type-directed operational semantics (TDOS) (Huang & Oliveira,2020). For the most part, developing a TDOS is similar to developing a standard small stepsemantics as advocated by Wright and Felleisen. However, in a TDOS type annotations
become operationally relevant and can affect the result of a program. While there have been
past formulations of small-step semantics where type annotations are also relevant (Bettini
et al., 2018; Goguen, 1994; Feng & Luo, 2011), the distinctive feature of TDOS is the useof a big-step casting relation for casting values under a given type. While typically values
are the final result of a program, in TDOS casting can further transform them based on their
run-time type. Thus, casting provides an operational interpretation to type conversions in
the language, similarly to coercions in coercion-based calculi (Henglein, 1994).
We illustrate how to employ TDOS on gradually typed languages using two calculi. The
first calculus, called λ Bg , is inspired by the semantics of a variant of the blame calculus(λ B) (Wadler & Findler, 2009) by Siek et al. (2015a). However, unlike the blame calculus,
λ Bg allows implicit type conversions, enabling it to be used as a gradually typed language.
Gradually typed languages can be built on top of λ B using an elaboration from a source
language into λ B. In contrast, λ Bg can already act as a gradual language, without the needfor an elaboration process.
The second calculus, called λ e, explores a variant of the eager semantics for gradually typed languages (Herman et al., 2007, 2010), inspired by the semantics adopted in
AGT (Garcia et al., 2016). In the λ B calculus, a lambda expression annotated with a chainof types is taken as a value. This means that it accumulates the type annotations, and checks
if there are errors only when the function is applied to a value. This has some drawbacks.
Perhaps most notably, and widely discussed in the literature (Herman et al., 2010; Siek
et al., 2009; Siek & Wadler, 2009; Siek & Taha, 2007; Garcia, 2013), is that the accumulation of annotations affects space efficiency. A nice aspect of the eager semantics is that it
avoids the accumulation of type annotations, being more space-efficient. Furthermore, asJournal of Functional Programming3

we shall see, the eager semantics also enables simple proofs for the gradual guarantee (Sieket al., 2015b).
For both calculi, type safety and the gradual guarantee are proved. For λ Bg , we alsopresent a variant with blame labels (Wadler & Findler, 2009). Blame labels are an important feature of gradually typed languages, which enable tracking run-time type errors andpinpointing the origin of the errors. Our variant of λ Bg shows how the TDOS deals withsuch an important feature of gradually typed languages. This is noteworthy since blamelabels can be a significant challenge for some gradual typing approaches. For instance, theAGT approach has yet to provide an account for blame labels. As far as we know, our work
provides the first gradually typed calculus without elaboration to an intermediate language
but with blame tracking. In addition, we show that blame safety can also be proved directlyfor λ Bg . Finally, we show that λ Bg with blame labels is sound and complete with respect
to the blame calculus.
A non-goal of the current paper is to investigate efficient implementations of a TDOS.
The three TDOS developed in this paper are directly implementable, but inefficient. We
believe that the primary strength of a TDOS is its ability to provide a direct and simple
semantics for gradual languages, and focus on that in this article. However, it is currently
unclear whether a TDOS can also be used to guide efficient implementations of gradually
typed languages. While we believe that it is possible to adapt TDOS to account for performance, this would require introducing additional complexity, which would be in conflictwith our goals here. We provide some discussion about potential directions to investigate
performant TDOS-based implementations, as well as discussing other potential criticismsof the TDOS approach in Section 6.
In summary, the contributions of this work are:
• TDOS for gradual typing: We show that a TDOS can be employed in gradually
typed languages. This enables simple, and concise specifications of the semantics
of gradually typed languages, without resorting to an intermediate cast calculus. A
nice aspect of TDOS is that it remains close to the simple and familiar small-stepsemantics approach by Wright and Felleisen.
• The λ Bg calculus provides a first concrete illustration of TDOS for gradual typing.
It follows closely the semantics of the blame calculus, but it allows implicit typeconversions. We show type-safety, determinism, as well as the gradual guarantee.
• The eager λ e calculus. λ e explores a TDOS design with an eager semantics forgradual typing. λ e is type-safe and it comes with a gradual guarantee (Siek et al.,2015b), which is quite simple to prove.
• TDOS with blame labels. We illustrate that the TDOS approach can deal with blamelabels. We provide a variant of λ Bg , called λ Bgl , which supports blame labels andblame tracking. λ Bgl is type-safe and deterministic, preserves the gradual guarantee
and is also blame safe. Two noteworthy results are the soundness and completenessto the blame calculus, and our blame safety proof, which is done directly on λ Bgl(instead of indirectly via the blame calculus).
• Coq formalization: All calculi and all associated lemmas and theorems, have beenformalized in the Coq theorem prover. The Coq formalization can be found in the
supplementary materials of this article:

4Type-Directed Operational Semantics for Gradual Typing
https://github.com/YeWenjia/TypedDirectedGradualTypingWithBlame

This article is an extended, and significantly rewritten, version of a conference paper (Yeet al., 2021). There are three main novelties with respect to the conference version. Firstly,
we now cover blame labels and blame tracking and introduce the new λ Bgl calculus, which
is a variant of λ Bg with blame labels. The conference work did not account for blamelabels at all. Furthermore, this article adds several important results for λ Bgl , such as thesoundness and completeness to the blame calculus, a novel blame safety theorem and thegradual guarantee for λ Bgl . Secondly, the conference version did not prove the gradualguarantee for λ Bg , whereas we now show the gradual guarantee for λ Bgl . The gradualguarantee is a non-trivial result for λ Bgl , due primarily to the lazy semantics of higherorder casts. Thirdly, the λ e calculus is also new, and it provides the first TDOS design
for a calculus with an eager semantics. In the conference version, we explored a forgetfulsemantics (Greenberg, 2015), but we opted to study an eager semantics instead for thejournal version since the eager semantics is more widely accepted.

2 Overview
This section provides background on gradual typing and the blame calculus, and then illustrates the key ideas of our work, the λ Bg calculus (with and without blame labels) and the
λ e calculus.
2.1 Background: Gradual Typing and the λ B Calculus
Traditionally, programming languages can be divided into statically typed languages anddynamically typed languages. In a statically typed language, a type system checks thetypes of terms before execution or compilation. The language may support type inference,but usually some type annotations are required for type checking. Type annotations bearsome extra work for a programmer. However, the benefit of static typing is that type-unsafe
programs are rejected before they are executed. On the other hand, in dynamically typed
languages terms do not have static types (and no type annotations are needed). This waives
the burden of a strict type discipline, making programs more flexible, but at the cost of
static type safety.
Gradual typing (Siek & Taha, 2006) is like a bridge connecting the two styles. Gradualtyping extends the type system of static languages by allowing terms to have an unknown
type ⋆. A term with the unknown type ⋆ is not rejected in any context by the type checker.
When all terms in a program have unknown types the type checker does not reject program,similarly to a dynamically typed language. In a gradually typed language, programs can becompletely statically typed, or completely dynamically typed, or anything in between.
To cooperate with the very flexible ⋆ type, the common practice in gradual type systems
is to define a binary relation called type consistency. Consistency offers a more relaxednotion of type compatibility compared to conventional statically typed languages whereequality is used instead. The key feature of consistency is that the unknown type ⋆ isconsistent with any other type. Thus, dynamic snippets of code can be embedded into thewhole program without breaking type soundness. Of course, the notion of type soundness
is relaxed to tolerate some kinds of run-time type errors. Besides type soundness, there are5

Journal of Functional Programmingsome other criteria for gradual typing systems. One well-recognized standard is the gradualguarantee proposed by Siek et al. (2015b).
Elaboration Semantics of Gradual Typing and the λ B Calculus. The semantics of gradually typed languages is usually given by an elaboration into a cast calculus. This approachhas been widely used since the original work on gradual typing by both Siek & Taha (2006)
and Tobin-Hochstadt & Felleisen (2006).
One of the most widely used cast calculi for the elaboration of gradually typed languages
is the blame calculus (Wadler & Findler, 2009; Siek et al., 2015a). Figure 1 shows thedefinition of the blame calculus. Here we base ourselves in a variant of the blame calculus
by Siek et al. (2015a). The blame calculus is the simply-typed lambda calculus extendedlwith the unknown type (⋆) and the cast expression (t ∶ A ⇒ B). Meta-variables G and H
range over ground types, which include Int and ⋆ → ⋆. The definition of values in thelblame calculus contains some interesting forms. In particular, casts (V ∶ A → B ⇒ A′ → B′ )land V ∶ G ⇒ ⋆ are included. Run-time type errors are denoted as blame l. The syntactic sort
l represents blame labels. A blame label l¯ is the complement of label l and the complement
is involutive, which means that ¯l̄ is the same as l. Notably, when casting with a label l,the expression being cast is to blame, while when casting with l,¯ the context of the cast is
to blame. Besides the standard typing rules of the simply typed lambda calculus (STLC),
there is an additional typing rule for casts: if term t has type A and A is consistent with B, acast on t from A to B has type B with blame label l. The consistency relation for types statesthat every type is consistent with itself, ⋆ is consistent with all types, and function types
are consistent only when input types and output types are consistent with each other. In
rule BT YP - C, ⌉c⌈ is the dynamic type of the constant c. For example, ⌉+⌈ is Int → Int → Int.
In the premise of rule BSTEP - DYNA, there is a predicate ug which says that type A should
be consistent with a ground type G, but it should not be G itself and type ⋆. The definitionof ug is:ug(A, G)::=A≠⋆ ∧ A≠G ∧ A∼G

In rule BSTEP - C, if 〚+〛(i) then +i is returned, while for 〚(+i1 )〛(i2 ), the result (i1 + i2 ) isreturned.
The bottom of Figure 1 shows a selection of the reduction rules of the blame calculus.
The dynamic semantics of the λ B calculus is standard for most rules. For first-order values, reduction is straightforward: a cast either succeeds or it fails and raises blame. For
example2 :
l1

l2

l1

l2

1 ∶ Int ⇒ ⋆ ∶ ⋆ ⇒ Int z→∗ 1
1 ∶ Int ⇒ ⋆ ∶ ⋆ ⇒ Bool z→∗ (blame l2 )For higher-order values such as functions, the semantics is more complex, since the castresult cannot be immediately obtained. For example, if we cast from ⋆ → ⋆ to Int → Int,
2

Note that throughout the paper we will assume that we have primitive types, such as Bool, for illustrating our
examples more simply. While the calculi that we formalize do not contain such primitive types, they are easy
to add and can be replaced by other types, such as Int → Int, for similar effect in the examples.

6Type-Directed Operational Semantics for Gradual Typing

SyntaxBlame Labels l
Types
Ground types
Constants

A, B ∶∶= Int ∣ ⋆ ∣ A → B
G, H ∶∶= Int ∣ ⋆ → ⋆c ∶∶= i ∣ + ∣ +il

Terms
Resultst ∶∶= c ∣ x ∣ t ∶ A ⇒ B ∣ t1 t2 ∣ λ x ∶ A.tr ∶∶= t ∣ blame lll

V, W ∶∶= c ∣ V ∶ A → B ⇒ A′ → B′ ∣ λ x ∶ A.t ∣ V ∶ G ⇒ ⋆Γ ∶∶= ⋅ ∣ Γ, x ∶ A

ValuesContextl

FrameF ∶∶= ◻ t ∣ V ◻ ∣ ◻ ∶ A ⇒ B

Γ⊩t ∶A(Typing Rules for the λ B Calculus)

B TYP - C

B TYP - ABS

B TYP - VARΓ ⊩ c ∶⌉c⌈

B TYP - APP

x∶A ∈ ΓΓ, x ∶ A ⊩ t ∶ BΓ ⊩ t1 ∶ A → BΓ⊩x∶AΓ ⊩ λ x ∶ A. t ∶ A → BΓ ⊩ t2 ∶ A

Γ ⊩ t1 t2 ∶ B

B TYP - CASTΓ⊩t ∶AA∼BlΓ⊩t ∶A⇒B∶B
A∼B(Consistency of types)
S- ARRS- I

A ∼CInt ∼ IntA → B ∼C → D

S- DYNL

B∼D

S- DYNR⋆∼A
A∼⋆(Reduction for the λ B Calculus)

t z→ r
BSTEP - BLAME

BSTEP - EVAL

BSTEP - BETA

t z→ t ′t z→ blame lF[t] z→ F[t ′ ]F[t] z→ blame l(λ x ∶ A. t) V z→ t[x ↦ V ]BSTEP - VANYBSTEP - DD

l1

l2

l

(V ∶ G ⇒ ⋆) ∶ ⋆ ⇒ G z→ V
BSTEP - DYNA

V ∶ ⋆ ⇒ ⋆ z→ V
BSTEP - ANYD

ug(A, G)lug(A, G)ll

V ∶ ⋆ ⇒ A z→ V ∶ ⋆ ⇒ G ∶ G ⇒ A

l

l

l

V ∶ A ⇒ ⋆ z→ (V ∶ A ⇒ G) ∶ G ⇒ ⋆BSTEP - ABETA

BSTEP - C

l¯

l

l

c v z→ 〚c〛(v)(V1 ∶ A1 → B1 ⇒ A2 → B2 ) V2 z→ (V1 (V2 ∶ A2 ⇒ A1 )) ∶ B1 ⇒ B2
BSTEP - VANYP

G≠H
l1

l2

(V ∶ G ⇒ ⋆) ∶ ⋆ ⇒ H z→ blame l2

BSTEP - LITli ∶ Int ⇒ Int z→ i

Fig. 1. The λ B Calculus (selected rules).

Journal of Functional Programming

7

we cannot judge the cast result immediately. So the checking process is deferred until thefunction is applied to an argument. Rule BSTEP - ABETA shows that process: a function withthe cast is a value which does not reduce until it has been applied to a value.
2.2 Motivation for a Direct Semantics for Gradual Typing
In this paper, we propose not to use an elaboration semantics into a cast calculus, but touse a direct semantics for gradual typing instead. We are not the first to propose suchan approach. For instance, the AGT framework for gradual typing (Garcia et al., 2016)
also employs a direct semantics. In that work, the authors state that “developing dynamic
semantics for gradually typed languages has typically involved the design of an independent cast calculus that is peripherally related to the source language”. We partly agreewith such arguments. In addition, as argued by Huang & Oliveira (2020), there are someother reasons why a direct semantics is beneficial over an elaboration semantics.
A direct semantics enables a simple and direct way for programmers and tools to reason
about the behavior of programs. For instance, we can reason directly about source programs by employing the operational semantics rules. With a TDOS, we can easily (andjustifiably) employ similar steps to reason about the source language (say GTLC or λ Bg ).
With a semantics defined via elaboration, however, that is not so easy because of the indirect semantics. In essence, with an elaboration semantics, one must first translate a source
expression to a target calculus, then reason about the semantics in the target calculus, andfinally translate the final result in the target calculus back to the source language. This process is not only more laborious, but it requires knowledge about the target language andits semantics. We refer readers to Huang and Oliveira’s work, which has an extensive discussion about this point. Additionally, some tools, especially some debuggers or tools fordemonstrating how programs are computed, require a direct semantics, since those tools
need to show transformations that happen after some evaluation of the source program.
Another potential benefit of a direct semantics is simpler and shorter metatheory/implementation. For instance, with a direct semantics we can often save quite a few
definitions/proofs, including a second type system, various definitions on well-formednessof terms, substitution operations and lemmas, pretty printers, etc. Though these are notarguably difficult, they do add up. Perhaps more importantly, some proofs can be simpler
with a direct semantics. For example, proving the gradual guarantee can often be simpler,since some lemmas that are required with an elaboration semantics (for instance, Lemma
6 in the original work on the refined criteria for gradual typing (Siek et al., 2015b)) are notneeded with a direct operational semantics. Moreover, only the precision relation for thesource language is necessary. We shall see some of those benefits in this paper.
Finally, another source of complication in an elaboration semantics, especially in languages with more advanced type systems, is coherence (Reynolds, 1991). Coherence is a
desirable property for an elaboration semantics, where we show that all possible elaborations for a source program have the same semantics in the target language. For simpler
languages, coherence is typically not an issue because the elaboration process is deterministic. That is there is always a unique target expression that is generated for the same
source program. The elaboration of the GTLC into the blame calculus, for example, isdeterministic. Thus, coherence is trivial in that case. However, for more advanced type

8Type-Directed Operational Semantics for Gradual Typing

system features, including implicit polymorphism (Xie et al., 2019; Bottu et al., 2019) orsome systems with subtyping (Huang & Oliveira, 2020), coherence becomes non-trivial
because the elaboration becomes non-deterministic. That is, for the same source program
we may be able to generate multiple distinct target expressions. Then a coherence proof
has to show that despite generating different expressions, those expressions have the same
meaning. Typically this is done by employing some form of contextual equivalence, andusually requires the use of logical relations (Reynolds, 1993). In those cases, the coherence
proof may become quite non-trivial and involved.
One of the original motivations of the TDOS (Huang & Oliveira, 2020) was to avoid
the need for coherence proofs. In Huang and Oliveira’s work, the source calculus that they
considered had subtyping with intersection types, and during elaboration coercions in thetarget language were generated by the subtyping relation. Unfortunately, these coercions
in a system with intersection types are not unique, requiring an involved proof of coherence using contextual equivalence and logical relations. A TDOS avoids coherence proofs.
Instead, we can simply prove that the semantics is deterministic, which can usually be doneusing standard proof techniques and simple inductions. Similar coherence issues arise withother type systems, such as for instance type systems with type classes. The proof that theelaboration of a language with type classes to a target language without type classes iscoherent is highly non-trivial, as shown by the work of Bottu et al. (2019). Finally, there isalso work in gradual typing where coherence issues also arise. For instance, Xie et al.
(2019) has shown that a source language with gradual typing and higher-ranked typeinference can be elaborated into the polymorphic blame calculus (Ahmed et al., 2011).
However, coherence was not proved due to its difficulty and was left as an open problem.
While in this paper the calculi involved are simple enough that no complications arise
from coherence, those complications will arise in more complex settings. Thus, avoiding
the complications of coherence is another argument to employ a TDOS.
2.3 λ Bg : A Gradually Typed Lambda Calculus
In this subsection, we introduce some of the key ideas in λ Bg , which is a gradually typed
lambda calculus that is given a semantics via a TDOS. In Section 3, we provide the fulldetails of λ Bg .
Cast Calculi vs Gradually Typed Calculi. Since λ B requires explicit casts whenever aterm’s type is converted, it cannot be considered as a gradually typed calculus. For comparison, the application rule for typing in the Gradually Typed Lambda Calculus (GTLC) (Sieket al., 2015b; Siek & Taha, 2006, 2007):Γ ⊩ e1 ∶ TΓ ⊩ e2 ∶ T3

T ▷ T1 → T2

Γ ⊩ e1 e2 ∶ T2

T3 ∼ T1

GTLC-A PP

does not force the input term to have the same type to what the function expects. It justchecks the consistency of the two terms’ types and can do implicit type conversions (casts)
automatically. Note that the function T ▷ T1 → T2 allows T to be either a function type or⋆. When T is a function type, then T itself is returned. Otherwise, if T is ⋆, then ⋆ → ⋆ isreturned. In a cast calculus, similar flexibility only exists when the term is wrapped with

9

Journal of Functional Programminga cast, since the application rule strictly requires the argument type to be the same as the
input type of the function type.
Bidirectional Type-Checking for λ Bg . In this paper, a key argument is that we do notneed two calculi to formulate the semantics of a gradually typed language. Instead, we canhave a single calculus that supports explicit type conversions (like casts in cast calculi) as
well as implicit type conversions (like the GTLC). To introduce implicit type conversions,
we turn to the bidirectional type checking (Pierce & Turner, 2000). Unlike in the GTLCor λ B, a bidirectional typing judgement may be in one of the two modes: inference orchecking. In the former, a type is synthesized from the term. In the latter, both the type andthe term are given as input, and the typing derivation examines whether the term can beused under that type safely. Notably, via the checking mode, the type consistency betweena type annotation and a given type is checked. Furthermore, uses of the checking mode in
typing essentially denote points where runtime casts need to happen to enforce type-safety.
In a typical bidirectional type system with subtyping, the subsumption rule is only
employed in the checking mode, allowing a term to be checked by a supertype of its
inferred type. That is to say, the checking mode is more relaxed than the inference mode,
which typically infers a unique type. With bidirectional type-checking the application rulein such a system is not as strict as in the λ B calculus, as the input term is typed with achecking mode. For example, the rules for applications and subsumption in λ Bg are:
T YP - APP

A ▷ A1 → A2
Γ ⊢ e1 ⇒ A
Γ ⊢ e2 ⇐ A1
Γ ⊢ e1 e2 ⇒ A2

T YP - SIM

Γ⊢e⇒A

A∼B

Γ⊢e⇐B

Implicit Type Conversion in Function Applications. λ Bg supports annotated lambdas of
the form λ x.e ∶ A → B with both input and output types for the function. A raw lambda λ x.e
is sugar for a lambda with a function type ⋆ → ⋆. Note also that, throughout this article,
whenever we have an expression of the form λ x.e ∶ A → B, this should be interpreted as(λ x.e) ∶ A → B. In other words, type annotations bind more weakly than lambdas (and otherforms of expressions). By using bidirectional type checking, we can type-check programs
such as:(λ x.x) 1

Accepted!

(λ x.not x) 1

Accepted!

(λ x.not x ∶ ⋆ → Bool) 1

Accepted!

(λ x.x + 1 ∶ Int → Int) 1

Accepted!

In addition bidirectional type checking can also reject ill-typed programs, such as:(λ x.not x ∶ Bool → Bool) 1

Rejected!

In the first two examples, λ x.x and λ x.not x are equivalent to λ x.x ∶ ⋆ → ⋆ and λ x.not x ∶⋆ → ⋆. Thus, in the first example, the argument 1 is type checked with type ⋆. For the 3rd
and 4th examples, 1 can be type checked by the function input types ⋆ and Int. However,1 cannot be checked by type Bool in the last example, and that program is rejected.

10Type-Directed Operational Semantics for Gradual Typing

Explicit Type Conversion. Besides implicit conversions, programmers are able to trigger
type conversions in an explicit fashion by wrapping the term with a type annotation e ∶ A,
where A denotes the target type. For instance, the two simple examples in λ B in Section 2.1
can be encoded in λ Bg as:
1 ∶ ⋆ ∶ Int z→∗ 1
1 ∶ ⋆ ∶ Bool z→∗ blamewith similar results to the same programs in the λ B calculus. Notice that, unlike λ B, there
is no cast expression in λ Bg . Casts are triggered by type annotations. For instance, in thefirst expression above (1 ∶ ⋆ ∶ Int), the first type annotation (⋆) triggers a cast from Int to ⋆.
The source type Int is the type of 1, whereas the target type ⋆ is specified by the annotation.
Then the second annotation Int will trigger a second cast, but now from ⋆ to Int.
2.4 Designing a TDOS for λ Bg
The most interesting aspect of λ Bg is its dynamic semantics. We discuss the key ideas next.
Background: Type-Directed Operational Semantics. A type-directed operationalsemantics is helpful for language features whose semantics is type dependent. TDOS was
originally proposed for languages that have intersection types and a merge operator (Huang
et al., 2021). To enable expressive forms of the merge operator, the dynamic semantics has
to account for types, just like the semantics of gradually typed languages. In many traditional operational semantics, type annotations are often ignored. In a TDOS that is not thecase. Instead, type annotations are used at runtime to determine the result of the reduction. A TDOS has two parts. One part is similar to the traditional reduction rules, modulo
some changes on type-related rules, like beta reduction for application, and annotation
elimination for values. The second component of a TDOS is the casting relation v ⇓A r.
Casting for λ Bg . Due to consistency, some form of run-time checking is needed in gradual typing. The casting relation v ⇓A r is used when run-time checks are needed. Casting
compares the dynamic type of the input value with the target type. When the type of the
input value (v) is not consistent with the target type (A), blame is raised. Otherwise, casting
adapts the value to suit the target type. Eventually, terms become more and more precise.
Two easy examples to show how casting works are shown next:
1 ⇓Int 1
1 ∶ ⋆ ⇓Bool blame
If we have an integer value 1 and we want to transform it with type Int, we simply return
the original value. In contrast, attempting to transform the value 1 ∶ ⋆ under type Bool will
result in blame.
Casting takes place in some reduction rules, such as the beta reduction rule and theannotation elimination rule for values. Here we illustrate the beta-reduction rule, and defer

Journal of Functional Programming11

the explanation of other reduction rules to Section 3:
S TEP -B ETA

v2 ⇓A v′2
(λ x. e ∶ A → B) v2 z→ e[x ↦ v′2 ] ∶ BCasting is used in beta-reduction to ensure that the argument value v2 matches the expected
input type of the function (A). Consider another example to illustrate the behavior of
casting in beta reduction:(λ x. x ∶ Bool → ⋆) (1 ∶ ⋆)If we perform substitution directly, as conventionally done in beta-reduction, we would
not check if there are run-time errors, for which blame should be raised. Since the typing
rule for the argument of the application is in checking mode, we need to check if the typeof the argument is consistent with the target type. Therefore the argument must be further
reduced with casting under the expected input type of the function. When we check thatthe type Int (the type for the value 1) is not consistent with Bool, blame is raised. However,
if we take the example:(λ x.x + 1 ∶ Int → Int) (1 ∶ ⋆)then the value 1 (which arises from casting) is substituted in the function body and theresult is 2.
2.5 λ e: Gradual Typing with an Eager Semantics
To further illustrate the application of a TDOS to gradually typed languages, we also propose a second calculus, called λ e. The λ e calculus has different design choices in terms of
the runtime semantics. In particular its semantics for casts is a variant of the eager semantics (Herman et al., 2010) inspired by the approach employeed in AGT (Garcia et al.,2016). Here we overview key ideas in λ e, while the full details of λ e will be given in
Section 5.
Lazy versus Eager. Both the blame calculus and λ Bg employ a lazy semantics for higherorder values, where functions with an arbitrary number of annotations are values. In otherwords, the checking process for higher-order values is deferred until the function is applied
to an argument. Garcia et al. (2016) proposed the AGT based methodology, which has been
widely applied (Toro et al., 2019; Labrada et al., 2022; Ye et al., 2023). In AGT, a variantof the eager semantics is applied for higher-order values. In the following example, weshow how higher-order values are reduced in AGT (using our notation):
λ x. 1 ∶ Int → Int ∶ ⋆ → ⋆ ∶ Bool → Bool z→∗ blame
Unlike the lazy semantics, where a lambda with multiple annotations would be a value,in λ e the above expression is not a value and it reduces to blame. blame is raised directly
because, during the reduction process, we attempt to eliminate the intermediate annotation⋆ → ⋆, by checking whether Int → Int and Bool → Bool are consistent. Since these two
types are not consistent blame would be raised in this case.

12Type-Directed Operational Semantics for Gradual Typing

Meets: Making Sure that no Cast is Forgotten. A complication in the eager semantics
is that we should guarantee that possible casts that arise from intermediate annotations are
not forgotten. To formalize this behavior, lambda values in λ e are of the form Lλ x. e ∶ A1 →A2 ∶ B1 → B2 ∶ CM and include three annotations:• The first annotation (A1 → A2 ) is used to type check the lambda body and to cast theargument using the input type before beta-reduction.
• The second annotation B1 → B2 is key to the eager semantics: it stores a type, which
we call the meet type, that is the greatest lower bound (with respect to precision)of all the intermediate annotations that have been eliminated during reduction of
the lambda value. In other words, it is the most imprecise type among the types
equivalent to or more precise than the eliminated types. The meet type triggers casts,
subsuming the casts needed for the eliminated intermediate annotations.
• Finally, the outer annotation C is needed for type preservation.
Lets see how meet types are used in the following example:(λ x. x ∶ Bool → ⋆ ∶ ⋆ → Bool ∶ ⋆ → ⋆ ∶ ⋆ → Int) 1
z→ (Lλ x. x ∶ Bool → ⋆ ∶ Bool → ⋆ ∶ Bool → ⋆M ∶ ⋆ → Bool ∶ ⋆ → ⋆ ∶ ⋆ → Int) 1
z→ (Lλ x. x ∶ Bool → ⋆ ∶ Bool → Bool ∶ ⋆ → BoolM ∶ ⋆ → ⋆ ∶ ⋆ → Int) 1
z→ (Lλ x. x ∶ Bool → ⋆ ∶ Bool → Bool ∶ ⋆ → ⋆M ∶ ⋆ → Int) 1
z→ blame
We first reduce λ x. x ∶ Bool → ⋆ to a tagged value Lλ x. x ∶ Bool → ⋆ ∶ Bool → ⋆ ∶ Bool →⋆M, which ensures that the intermediate type is more precise than the outer type. The details
are explained in Section 5. Then, in the 3rd line, we are safe to remove the outer type andupdate the intermediate type with the meet result between Bool → ⋆ and ⋆ → Bool, which is
the more precise type Bool → Bool. Finally, in the 4th line, the meet between Bool → Booland ⋆ → Int is undefined and error is raised. Note that, without storing the more precise type
Bool → Bool in the middle, then the type information of the intermediate type annotation⋆ → Bool would be ignored.
The eager semantics does have some drawbacks compared to the lazy semantics. For
instance, New et al. (2019) show that the η principle for the higher-order values is violated. Nevertheless, there are also some nice aspects in an eager semantics. With an eager
semantics it is possible to avoid the accumulation of annotations for higher-order values.
Another nice aspect of the eager semantics in the AGT approach is that the dynamic gradualguarantee can be formalized in a simple way and proved easily. This is because the number of reduction steps when evaluating a program is not affected by precision (except whenruntime errors occur in the less precise version of the program). In a lazy semantics, annotations are sometimes accumulated or added during reduction. So the reduction of more
precise and less dynamic programs can take different number of steps in some cases. Here,a more precise program means that the program is more statically typed. For instance, for
λ x. x ∶ Int → Int ∶ ⋆ and λ x. x ∶ ⋆ → ⋆ ∶ ⋆, the more precise program λ x. x ∶ Int → Int ∶ ⋆ shouldtake a step to λ x. x ∶ Int → Int ∶ ⋆ → ⋆ ∶ ⋆. In contrast, the less precise one λ x. x ∶ ⋆ → ⋆ ∶ ⋆Journal of Functional Programming

13(which is a value) takes zero steps. Since in the eager semantics annotations are not accumulated, the dynamic semantics for more and less precise programs behaves in the sameway, satisfying the dynamic gradual guarantee more directly and naturally.
Functions. One interesting aspect in the type system of λ e is how we deal with lambdas.
If the programmer wants to have a function statically type checked, they can write down
the full annotations or the annotations can be propagated by bidirectional type checking.
For instance, in the term:(λ f . f 2 ∶ (Int → Int) → Int) (λ x. x + 1)
The argument to the function (λ x. x + 1), which is itself a lambda, has no type annotations. Here bidirectional type-checking propagates the annotations, removing the need for
explicit annotations in the lambda. This is in contrast to typical gradual languages, such as
the GTLC, where a raw lambda λ x. e is syntactic sugar for λ (x ∶ ⋆). e. The key differenceis that in GTLC the raw lambda (λ x. x + 1) in a similar program to the above would lose
type information and be of type ⋆ → Int. A consequence of this loss of type precision is thatthe elaboration of GTLC into a cast calculus would need to insert a few casts here. Firstly,
one cast from ⋆ to Int would be needed to convert the type of the argument. Secondly a castfrom Int to ⋆ would be needed to cast x back to an integer. These casts could potentially be
avoided if there was no loss of type information. In λ e, the lambda is of type Int → Int andno static information is lost.
To achieve this, our rule for lambda expressions, which is quite standard for bidirectional
typing, is:Γ, x ∶ A1 ⊢ e ⇐ A2

A ▷ A1 → A2

Γ ⊢ λ x. e ⇐ A

TYP- ABS

The premise A ▷ A1 → A2 in rule TYP- ABS ensures that type A can be the unknown type⋆ or a function type. The unknown type is interpreted as the unknown function ⋆ → ⋆. The
typing rule TYP- ABS is employed to type-check both lambdas above: the first one because
the explicit type annotation triggers the checking mode; and the second one because theapplication rule employs the checking mode to check that arguments conform to the righttype.
2.6 Blame Tracking
An important feature of gradual typing is blame tracking, which enables pinpointing thesource of blame in a program. This is helpful for programmers as they can determine thesource of the problem. λ Bg can support blame tracking, showing that the TDOS approach
can smoothly deal with such an important feature of gradual typing. Next, we discuss the
key ideas of adding blame tracking to λ Bg . The full details are discussed in Section 4.
Blame Tracking. For gradually typed lambda calculi, due to the notion of consistency,
runtime type errors may arise from type inconsistency. A natural question is what is thecause of the error, and which part of the program is to blame. In the λ B calculus, blamelabels, which are the blue parts in Figure 1, are used to track the source of errors. Blame¯ Positive blamelabels include the positive blame label (l) and the negative blame label (l).

14Type-Directed Operational Semantics for Gradual Typing

labels (l) arise when the terms contained in the cast are to blame. Negative blame labels¯ arise when the context which contains the cast is to blame. An example to show the(l)mechanism of blame tracking with different labels in λ B is:l0l1((λ x ∶ Int. x) ∶ Int → Int ⇒ ⋆ → Int) (True ∶ Bool ⇒ ⋆)
l¯1

l0

l1

z→ ((λ x ∶ Int. x) ((True ∶ Bool ⇒ ⋆) ∶ ⋆ ⇒ Int)) ∶ Int ⇒ Intz→∗ (blame l¯1 )l0

In this example, when the argument (True ∶ Bool ⇒ ⋆) is cast from ⋆ to Int, blame withlabel l¯1 is raised: the source type Bool is different from the target type Int causing blame
to be raised.
Blame Tracking for λ Bg . The λ Bgl calculus is a variant of λ Bg with blame tracking.
In λ Bgl blame labels are introduced in annotation expressions (e ∶l A), lambdas (λ x. e ∶l
A → B), application expressions ((e1 e2 )l ) and projections (πil e). Annotation expressionsl(e ∶l A) trigger casts, and are similar to cast expressions (t ∶ B ⇒ A) in λ B. While the label
in lambdas is to track the implicit cast in lambda bodies. Notably, there is a blame label for
applications since the typing rule for applications is:Γ ⊢ e1 ⇒ A

A ▷ A1 → A2

Γ ⊢ e2 ⇐ A1l

Γ ⊢ (e1 e2 ) ⇒ A2

T YP - APP

In this rule, the typing for the argument e2 is in checking mode. This means that e2 may
have a different type, which can be consistent with A1 . However, the cast induced by theapplication, may be the source of blame. For instance, consider the following program:((λ x. x ∶l1 Int → Int) (True ∶l3 ⋆))l2
For this example, the argument (True ∶l3 ⋆) is cast under type Int, and the type of True is notconsistent with type Int. Blame is raised with the blame label (l2 ). Furthermore, if A is type⋆, there is an implicit cast to ⋆ → ⋆ and label l is used as well. The label l in projections
πil e has the similar behavior. The λ Bgl calculus is proved to be sound and complete withrespect to the blame calculus with blame labels. Furthermore, we formalized and proved
the gradual guarantee theorem for λ Bgl .
Blame Theorem. “Well-typed programs can’t be blamed” is the slogan of Wadler &Findler (2009)’s paper. To express this slogan formally, Wadler and Findler proposed theblame theorem, which expresses the idea that we should blame the right part of a program.
More specifically, a cast from a more precise type to a less precise type cannot give rise topositive blame, and negative blame cannot be triggered while casting from a less precise
type to a more precise type. We have proved the blame theorem for λ Bgl , showing that thiskey result can be proved using a TDOS approach to gradual typing.
3 The λ Bg Calculus: Syntax, Typing and Semantics
In this section, we introduce the gradually typed λ Bg calculus. The semantics of the
λ Bg calculus follows closely the semantics of the λ B cast calculus. It employs a typedirected operational semantics (Huang & Oliveira, 2020) to have a direct operational

15

Journal of Functional Programming
SyntaxA, B ∶∶= Int ∣ ⋆ ∣ A → B ∣ A × B
c ∶∶= i ∣ + ∣ +ie ∶∶= c ∣ x ∣ λ x. e ∶ A → B ∣ e1 e2 ∣ e ∶ A ∣ (e1 , e2 ) ∣ πi er ∶∶= e ∣ blamev ∶∶= c ∣ v ∶ A → B ∣ v ∶ ⋆ ∣ λ x. e ∶ A → B ∣ (v1 , v2 )Γ ∶∶= ⋅ ∣ Γ, x ∶ A
F ∶∶= ◻ e ∣ v ◻ ∣ ◻ ∶ A ∣ (◻, e) ∣ (v, ◻) ∣ πi ◻

TypesConstants
Expressions
Results
ValuesContext
Frame(Well-formed values for λ Bg calculus)

value eVALUE - FANNOVALUE - C

VALUE - ABS

value cvalue λ x. e ∶ A → B⌉v⌈= C → D

value v ∶ A → B
VALUE - PRO

VALUE - DYN

Ground ⌉v⌈

value vvalue v1

value vvalue v2

value (v1 , v2 )value v ∶ ⋆Ground A(Ground types)
G ROUND - INT

G ROUND - ARR

G ROUND - PRO

Ground Int

Ground ⋆ → ⋆Ground ⋆ ×⋆

Fig. 2. Syntax and well-formed values for the λ Bg calculus.
semantics. λ Bg uses bidirectional type-checking (Pierce & Turner, 2000). We keep thepresentation light here to better illustrate the key ideas of our approach. Thus, we mainly
focus on presenting the semantics and proving basic results such as determinism and typesoundness. In Section 4, we present an extension of λ Bg with blame labels, and develop
many more results, such as the gradual guarantee, the blame theorem and the soundness
and completeness to the blame calculus.
3.1 Syntax
The syntax of the λ Bg calculus is shown in Figure 2.
Types and Ground types. Meta-variables A and B range over types. There is a basic type:the integer type Int. The calculus also has function types A → B, the unknown type ⋆, andproduct types A × B. Compared to λ B calculus, ground types not only include Int and⋆ → ⋆, but also ⋆ × ⋆. We sometimes use the abbreviation G to denote ground types.
Constants, Expressions and Results. Meta-variable c ranges over constants. Each constant is assigned a unique type. The constants include integers (i) of type Int and additions(+, +i ). The type of + is Int → Int → Int. The type of +i is Int → Int, taking an integer and16Type-Directed Operational Semantics for Gradual Typing

returning another integer. Meta-variable e ranges over expressions. There are some standard constructs, which include: constants (c); variables (x); annotated expressions (e ∶ A);
annotated lambdas (λ x. e ∶ A → B); application expressions (e1 e2 ); products (e1 , e2 ) andprojections (πi e). Similarly to GTLC, lambdas without type annotations are just sugar for
lambdas with the annotation ⋆ → ⋆. Results (r) include all expressions and blame, which isused to denote cast-errors at run-time.
Values and Contexts. Typing contexts are standard. Γ is used to track bound variables
x with their type A. The meta-variable v ranges over well-formed values. Values contain
constants, annotated values and lambda abstractions (λ x. e ∶ A → B). Similarly to λ B, notall syntactic values are well-formed values. The value predicate, at the bottom of Figure 2,
defines well-formed values, which are a subset of syntactic values. Lambda expressions
are values (rule VALUE - ABS). A syntactic value v with a function type annotation is awell-formed value if the dynamic type of the value is also a function type (rule VALUE FANNO ). Note that, for well-typed values, it is guaranteed that the type of v is consistent
with the annotation A → B. So, the value predicate only needs to check if the type of thevalue has an arrow form. The expression v ∶ ⋆ is a value only when the type of v is a groundtype (rule VALUE - DYN). Products are values if there is a pair of values. Constants are also
values. Note that the meta-function ⌉v⌈, defined next, denotes the dynamic type of a value.
Definition 3.1 (Dynamic type). ⌉v⌈ denotes the dynamic type of the value v.
⌉i⌈ = Int⌉λ x. e ∶ A → B⌈ = A → B⌉+⌈ = Int → Int → Int⌉+i ⌈ = Int → Int⌉v ∶ A⌈ = A⌉(v1 , v2 )⌈ =⌉v1 ⌈×⌉v2 ⌈Frame. The meta-variable F ranges over frames (Siek et al., 2015a), which is a form ofevaluation contexts (Felleisen & Hieb, 1992). The frame is mostly standard, though it isperhaps noteworthy that it includes annotated expressions.
3.2 Typing
We use bidirectional typing for our typing rules. The typing judgment is represented asΓ ⊢ e ⇔ A, which means that the expression e could be inferred (⇒) or checked (⇐) by thetype A under the typing context Γ. The typing mode (⇔), whose definition is shown at the
top of Figure 3, is used to represent the two modes of the bidirectional typing judgment.
Typing Relation. The typing relation of the λ Bg calculus is shown in Figure 3. Many rules
in inference mode follow the λ B type system. The typing for constants (rule T YP - C) uses
the dynamic type definition to infer the type. Rule T YP - VAR for variables is standard. For
lambda expressions, the λ Bg calculus is different from the λ B calculus: in the λ Bg calculus
the function type of a lambda expression is annotated and the function body is checkedwith the function output type. Lambdas are annotated with full types because at runtime
we want to get the type of lambdas without performing type-checking.

17

Journal of Functional Programming
Typing mode⇔ ∶∶= ⇒∣⇐

(Typing of λ Bg )Γ⊢e⇔AT YP - ABS

T YP - VAR
T YP - Cx∶A ∈ ΓΓ, x ∶ A ⊢ e ⇐ BΓ ⊢ c ⇒⌉c⌈Γ⊢x⇒A

Γ ⊢ λ x. e ∶ A → B ⇒ A → B

T YP - APP

A ▷ A1 → A2
Γ ⊢ e1 ⇒ A
Γ ⊢ e2 ⇐ A1

T YP - ANNOΓ⊢e⇐AΓ ⊢ e1 e2 ⇒ A2Γ⊢e⇒AΓ⊢e∶A⇒A

T YP - PROΓ ⊢ e1 ⇒ A1

T YP - SIM

A∼B

Γ⊢e⇐B

T YP -P IΓ ⊢ e2 ⇒ A2Γ⊢e⇒AΓ ⊢ (e1 , e2 ) ⇒ A1 × A2

A ▸ A1 × A2

i ∈ {1, 2}

Γ ⊢ πi e ⇒ Ai

⋆
A→B
⋆
A×B

⊳
⊳
▸
▸

⋆→⋆
A→B
⋆×⋆
A×B

Fig. 3. Type system of the λ Bg calculus.

For applications e1 e2 , the rule is almost standard for bidirectional type-checking: thetype of e1 is inferred, and the type of e2 is checked against the domain type of e1 . However,there is some additional flexibility in the typing of applications. The expression e1 can havetype ⋆. In that case, ⋆ is interpreted as a dynamic function type ⋆ → ⋆, by employing amatching function (shown at the bottom of Figure 3). The rule for annotations (rule T YP ANNO ) is standard, inferring the annotated type, while checking the expression against
the annotated type. Consistency checks happen in the subsumption rule (rule T YP - SIM).
However, it is important to notice that, since the subsumption rule is in checking mode, allconsistency checks can only happen when typing is invoked in the checking mode. This is
the case, for instance, for the rule T YP -A PP, which checks whether the argument is of type
A1 . In addition, to type check the product related expressions, we have rule T YP - PRO andrule T YP -P I. A pair (e1 , e2 ) is well-typed with type A × B, if e1 is well-typed with type
A and e2 is well-typed with type B. When performing projections, we should make surethat the projections happen on pairs. Therefore, we use the matching relation A ▸ B withproduct types A1 × A2 . The unknown type ⋆ matches the dynamic product type ⋆ × ⋆.
Consistency. Consistency plays an important role in a gradually typed lambda calculus,
acting as a relaxed equality relation. The consistency relation extends λ B’s consistency,

18Type-Directed Operational Semantics for Gradual Typing

which is already shown in Figure 1, with product types:
A1 ∼ B1A2 ∼ B2

A1 × A2 ∼ B1 × B2
In consistency, reflexivity and symmetry hold. However, it is well-known that consistency is not a transitive relation. If consistency were transitive then every type would beconsistent with any other type (Siek & Taha, 2006).
Some important properties of the typing relation are that it computes dynamic types forthe inference mode, and the type inference has unique types.
Lemma 3.1 (Dynamic Types for Values). If ⋅ ⊢ v ⇒ A then ⌉v⌈= A.
Lemma 3.2 (Inference is Checkable). If Γ ⊢ e ⇒ A then Γ ⊢ e ⇐ A.
Lemma 3.3 (Uniqueness of Inference). If Γ ⊢ e ⇒ A1 and Γ ⊢ e ⇒ A2 then A1 = A2 .
3.3 Dynamic Semantics
The dynamic semantics of λ Bg employs a type-directed operational semantics(TDOS) (Huang & Oliveira, 2020). In a TDOS, besides the usual reduction relation, there
is a special casting relation for values that is used to further reduce values based on the typeof the value. Casting is used by the TDOS reduction relation. In a gradually typed calculus
with a TDOS, the casting relation plays a role analogous to various cast-related reduction
rules in a cast calculus (Wadler & Findler, 2009; Siek et al., 2015a; Siek & Wadler, 2009;
Herman et al., 2007). We first introduce casting and then move on to the definition of
reduction.
Casting. We reduce a value under a certain type using the casting relation. The form of thecasting relation is v ⇓A r, which means that a value v reduces under type A to a result r.
Unlike reduction, casting is defined using a big-step style. Note that the result r producedby casting can only be a value or blame. Blame is raised during casting if we try to reducethe value under a type that is not consistent with the type of the value. For instance, trying
to reduce the value 1 ∶ ⋆ under the type Bool will raise blame. Thus, it should be clearthat casting mimics the behavior of casts in cast calculi such as the λ B calculus. In the
λ B calculus, t ∶ B ⇒ A casts t from source type B into target type A. Using casting in λ Bg ,the type A is the target type (which arises from a type annotation), whereas the dynamic
type of v is the source type.
Figure 4 shows the rules of casting. Rule C AST- ABS and rule C AST- V just add a type
annotation to the value. In rule C AST- ABS, the dynamic type of the value (⌉v⌈) is a function
type, thus v annotated with A → B is a value. Note that several casting rules employ the
dynamic type function to compute the type of a value at runtime. However, the type of avalue is never computed from scratch, since we use existing type annotations to return thetype of a value. In rule C AST- V, v ∶ ⋆ is also a value when the dynamic type of v is a groundtype. Rule C AST- LIT is for integer values: an integer i being reduced under the integer type
results in the same integer i. A value v ∶ ⋆ cast under ⋆ returns the original value as well(rule C AST- DD). In rule C AST- ANYD, the premise is that the dynamic type of v should bea ug type which is defined in λ B. It means that the type of v should be any function type

19

Journal of Functional Programmingv ⇓A r(Casting)

C AST- ABS

C AST- V⌉v⌈= C → D

C→D∼A→Bv ⇓A→B v ∶ A → B
C AST- ANYD

Ground ⌉v⌈

C AST- LIT

C AST- DDv ⇓⋆ v ∶ ⋆i ⇓Int iv ∶ ⋆ ⇓⋆ v ∶ ⋆C AST- BLAMEv ⇓G v′

ug(⌉v⌈, G)′v ⇓⋆ v ∶ ⋆C AST- VANYv ∶ ⋆ ⇓⌉v⌈ v

C AST- PRO

v1 ⇓A1 v′1⌉v⌈≁ Av ∶ ⋆ ⇓A blame

C AST- DYNA

ug(A, G)v ⇓A rv ∶ ⋆ ⇓A r

C AST- Lv2 ⇓A2 v′2(v1 , v2 ) ⇓A1 ×A2 (v′1 , v′2 )v1 ⇓A1 blamev2 ⇓A2 r(v1 , v2 ) ⇓A1 ×A2 blame

C AST- R

v1 ⇓A1 v′1v2 ⇓A2 blame(v1 , v2 ) ⇓A1 ×A2 blame
Fig. 4. Casting for the λ Bg calculus.
A → B except for ⋆ → ⋆ or any product type A × B except for ⋆ × ⋆. In the end, v is castunder ground type G and returns the value v′ annotated with ⋆.
In rule C AST- VANY, v ∶ ⋆ is cast under the dynamic type of v, returning v and dropping
the annotation ⋆. In rule C AST- BLAME, if the dynamic type of v is not consistent to thetype A that we are casting, then blame is raised. Finally, in rule C AST- DYNA, a value v ∶ ⋆being cast under type A (where A is a ug type) returns the result of v cast under type A. For
products, pairs of values are cast under the corresponding types. Rule C AST- PRO models
the case when both casts succeeds, while rule C AST- L and rule C AST- R model the cases
where at least one of the casts fails.
Properties of Casting. Some properties of casting for the λ Bg calculus are shown next:
Lemma 3.4 (Casting preserves well-formedness of values). If value v and v ⇓A v′ thenvalue v′ .
Lemma 3.5 (Preservation of Casting). If ⋅ ⊢ v ⇐ A and v ⇓A v′ then ⋅ ⊢ v′ ⇒ A.
Lemma 3.6 (Progress of Casting). If ⋅ ⊢ v ⇐ A then ∃r, v ⇓A r.
Lemma 3.7 (Determinism of Casting). If ⋅ ⊢ v ⇐ B, v ⇓A r1 and v ⇓A r2 then r1 = r2 .
Lemma 3.8 (Casting Respects Consistency). If ⋅ ⊢ v ⇒ B and v ⇓A r then B ∼ A.
According to Lemma 3.4, if the result of a value cast under a type A is a value, then it
should be well-formed. Lemma 3.5 shows that the target type A is preserved after casting:if a value v is cast using A, the result type of v′ is of type A. Note that this lemma (andsome others) have a premise that ensures that the value under casting must be well-typed
under some type B. That is, the lemma only holds for well-typed values (which are theonly ones that we care about). Lemma 3.6 shows that if a value v is well-typed with type A,

20Type-Directed Operational Semantics for Gradual Typing

e z→ r(Small-step Semantics)

S TEP - EVALS TEP - BLAMEe z→ e′S TEP - ANNOV

e z→ blame′

F[e] z→ blame

F[e] z→ F[e ]¬value (v ∶ A)v ∶ A z→ r

S TEP -B ETAS TEP - BETAP⌉v1 ⌈= A → B

v ⇓A rv2 ⇓A v′2

v2 ⇓A blame(λ x. e ∶ A → B) v2 z→ e[x ↦ v′2 ] ∶ B

v1 v2 z→ blame
S TEP -A BETA

value (v1 ∶ A → B)

S TEP - DYN

v2 ⇓A v′2

value (v1 ∶ ⋆)(v1 ∶ A → B) v2 z→ (v1 v′2 ) ∶ B
S TEP - PJD(v1 ∶ ⋆) v2 z→ (v1 ∶ ⋆ ∶ ⋆ → ⋆) v2
S TEP -Ci ∈ {1, 2}
πi (v ∶ ⋆) z→ πi (v ∶ ⋆ ∶ ⋆ × ⋆)⌉c⌈= A → B

S TEP - PJv ⇓A v′c v z→ 〚c〛(v )′i ∈ {1, 2}
πi (v1 , v2 ) z→ vi

Fig. 5. Semantics of λ Bg .
then casting the value will either return a well-formed value or blame. The casting relation
is deterministic for well-typed values (Lemma 3.7): if a well-typed value v is cast by typeA, the result will be unique. Finally, if v is cast by A, the dynamic type of v should beconsistent with type A (Lemma 3.8). Most of these lemmas are proved by induction on thecasting relation.
Reduction. The reduction rules are shown in Figure 5. Rule S TEP - EVAL and rule S TEP BLAME are standard rules to reduce subterms under evaluation contexts. A key difference
between the reduction rules for λ Bg and the blame calculus lies on the treatment of applications. λ Bg supports flexible applications with implicit type conversions, while the blame
calculus does not have such flexibility. To account for the extra flexibility, the semantics ofapplications needs to be more complex in λ Bg .
Rule S TEP - BETA is the beta reduction rule. Importantly, note that casting under type A
is needed for v2 : that is we cast value v2 to v′2 so that v′2 has the required input type A.
Moreover, the result of the reduction is the substitution e[x ↦ v′2 ] annotated with type B.
In rule S TEP - ABETA, the type of the argument v2 should also be consistent with the input
type (A) of the annotated function value. Furthermore, v1 ∶ A → B is a well-formed value.
From typing, we know that ⋆ matches with a dynamic function type ⋆ → ⋆. Therefore,
rule STEP - DYN annotates functional values of the form v1 ∶ ⋆ with type ⋆ → ⋆. Note that,when the value (v1 ) does not match the required type structure, blame should be raised. For
example, program (1 ∶ ⋆) 2 raises blame during reduction by first applying rule S TEP - DYN
and then rule S TEP - ANNOV. Rule S TEP - PJD follows a similar behavior and it is annotatedto product type ⋆ × ⋆. Rule S TEP -A NNOV is used when a value v is annotated with a type
A. In that case, the value should have a type consistent with type A. So a cast is performed
for the value with target type A and a result (which could be blame) is produced by casting.
Rule S TEP -C shows a rule that deals with primitive operations for + and +i (we introduced those in Section 2), similarly to those in λ B. The argument value v is cast by theJournal of Functional Programming

21

input type of the primitive operations such as Int for +. Rule S TEP - PJ projects the values
from products.
Determinism. The operational semantics of λ Bg is deterministic: expressions reduce to aunique result. Theorem 3.1 is proved using Lemma 3.7.
Theorem 3.1 (Determinism of λ Bg calculus). If ⋅ ⊢ e ⇔ A, e z→ r1 and e z→ r2 thenr1 = r2 .
Type Soundness. The λ Bg calculus is type sound. Theorem 3.2 says that if an expression
is well-typed with type A, the type will be preserved after the reduction. Progress is given
by Theorem 3.3. A well-typed expression e is either a value, or it reduces to a result.
Theorem 3.2 (Type Preservation of λ Bg Calculus). If ⋅ ⊢ e ⇔ A and e z→ e′ then ⋅ ⊢ e′ ⇔A.
Theorem 3.3 (Progress of λ Bg Calculus). If ⋅ ⊢ e ⇔ A then e is a value or ∃r, e z→ r.

4 The λ Bgl Calculus
In Section 3, we introduced the λ Bg calculus. In this section, we show that the TDOS
approach can also support blame labels. We introduce the λ Bgl calculus, which is the λ Bg
calculus with blame labels and show that it is sound and complete with respect to λ B withblame labels. Furthermore, we prove the gradual guarantee and a blame safety theorem forthe λ Bgl calculus.
4.1 Static Semantics
Syntax. The syntax of the λ Bgl calculus is shown in Figure 6. Most of the syntax isgthe same as λ B . One small difference is that for annotations, lambdas, projections, andapplication expressions, there are labels.
Typing. The typing rules of λ Bgl are shown at the bottom of Figure 6. The rules follow
those of λ Bg . Compared to the λ Bg calculus, rules T YP -A BS, T YP -A PP, T YP -A NNO, andT YP - PI now deal with blame labels. In particular, for applications (e1 e2 )l , the type of
the argument (e2 ) must be consistent with the input type of the function type, which is A.
For this reason applications require a label for tracking the implicit cast for the applicationargument. Furthermore, since the type of e1 can be ⋆, there can be an implicit cast to type⋆ → ⋆. The label in applications is used to track these possible casts. Similarly, the label
for projections πil e is used to track the possible cast from ⋆ to ⋆ × ⋆.
4.2 Dynamic Semantics
Casting. The form of the casting relation changes to v ⇓lA r. The new form means that avalue v annotated with type A reduces under type A with blame label l. Blame is raisedwith a label during casting if we try to reduce a value with unknown type under a type thatis not consistent with the type of the value. The label indicates the location in the program
to blame. For instance, trying to cast the value 1 ∶l1 ⋆ under the type Bool with label l2
indicates that this cast raises blame and we get the result blame l2 . The same example would

22Type-Directed Operational Semantics for Gradual Typing

SyntaxBlame Labels l
TypesConstants
Expressions
ResultValuesContext
Frame

A, B ∶∶= Int ∣ ⋆ ∣ A → B ∣ A × B
c ∶∶= i ∣ + ∣ +ie ∶∶= c ∣ x ∣ (e1 , e2 ) ∣ πil e ∣ λ x. e ∶l A → B ∣ (e1 e2 )l ∣ e ∶l A
r ∶∶= e ∣ blame lv ∶∶= c ∣ (v1 , v2 ) ∣ λ x. e ∶l A → B ∣ v ∶l A → B ∣ v ∶l ⋆Γ ∶∶= ⋅ ∣ Γ, x ∶ A
F ∶∶= (◻, e) ∣ (v, ◻) ∣ πil ◻ ∣ (◻ e)l ∣ (v ◻)l ∣ ◻ ∶l A

(Well-formed values for λ Bgl calculus)

value eVALUEL - FANNOVALUEL - ABS

VALUEL - C⌉v⌈= C → D
lvalue cvalue λ x. e ∶ A → B

VALUEL - DYN

value vlvalue v ∶ A → B
VALUEL - PRO

Ground ⌉v⌈

value vvalue v1lvalue v2

value (v1 , v2 )value v ∶ ⋆Ground A(Ground types)
G ROUND - INT

G ROUND - ARR

G ROUND - PRO

Ground Int

Ground ⋆ → ⋆Ground ⋆ ×⋆Γ⊢e⇔A

(Typing)
T YP -A PP

A ▷ A1 → A2
Γ ⊢ e1 ⇒ A
Γ ⊢ e2 ⇐ A1

T YP - VAR
T YP - Cx∶A ∈ ΓΓ ⊢ c ⇒⌉c⌈

Γ⊢x⇒A

Γ⊢e⇐B

T YP - PRO

Γ, x ∶ A ⊢ e ⇐ B

A∼BlΓ ⊢ λ x. e ∶ A → B ⇒ A → BΓ ⊢ e1 ⇒ A1

A ▸ A1 × A2

Γ ⊢ e2 ⇒ A2

Γ ⊢ (e1 , e2 ) ⇒ A1 × A2

T YP - PI

Γ⊢e⇒A

Γ⊢e⇐A
Γ ⊢ e ∶l A ⇒ A

Γ ⊢ (e1 e2 ) ⇒ A2

T YP -A BS

T YP - SIM

Γ⊢e⇒A

l

T YP -A NNO

i ∈ {1, 2}

Γ ⊢ πil e ⇒ Ai
Fig. 6. Static semantics for the λ Bgl calculus.

23

Journal of Functional Programming(Casting for λ Bgl calculus)v ⇓lA r
CAST- ABS

CAST- V⌉v⌈= C → D

C→D∼A→Bv ⇓lA→B v ∶l A → B

CAST- LIT

CAST- DDv ⇓l⋆ v ∶l ⋆i ⇓lInt iv ∶l1 ⋆ ⇓l⋆2 v ∶l1 ⋆CAST- DYNA

CAST- ANYDug(⌉v⌈, G)

Ground ⌉v⌈v ⇓lG v′ug(A, G)⌉v⌈≁ Av ∶l1 ⋆ ⇓lA2 (blame l2 )CAST- PROv1 ⇓lA1 v′1

CAST- VANY2v ∶l1 ⋆ ⇓l⌉v⌈v

v ∶l1 ⋆ ⇓lA2 rv ⇓l⋆ v′ ∶l ⋆CAST- BLAMEv ⇓lA2 r

CAST- Lv2 ⇓lA2 v′2v1 ⇓lA1 (blame l)(v1 , v2 ) ⇓lA1 ×A2 (v′1 , v′2 )v2 ⇓lA2 r(v1 , v2 ) ⇓lA1 ×A2 (blame l)

CAST- Rv2 ⇓lA2 (blame l)

v1 ⇓lA1 v′1(v1 , v2 ) ⇓lA1 ×A2 (blame l)
Fig. 7. Casting for the λ Bgl Calculus.

l1

l2

be represented in the λ B calculus as (1 ∶ Int ⇒ ⋆) ∶ ⋆ ⇒ Bool, which also raises blame withlabel l2 .
Figure 7 shows the rules of casting. Except for rule CAST- BLAME, the other rules in casting are similar to the λ Bg calculus. For rule CAST- BLAME, we use the blame label tracked
by casting to return the blame result. The casting of λ Bgl shares all the same properties in
λ Bg .
Reduction. The reduction rules of λ Bgl are shown in Figure 8. They extend the rules in
Figure 5 with blame labels l. The rule S STEP - BETA deals with applications where thefunctions are annotated: ((λ x. e ∶l A → B) v)l1 . Note that this reduction rule requires casting
the arguments before beta-reduction. To type such applications we use:Γ ⊢ λ x. e ∶l A → B ⇒ A → B
l

Γ⊢v⇐A
l1

Γ ⊢ ((λ x. e ∶ A → B) v) ⇒ B
Due to the checking mode for the argument of an application, there is an implicit cast,which is tracked by the label l1 . For instance, consider (((λ x. x) ∶l0 Bool → Bool) (1 ∶l1⋆))l . In this example, 1 ∶l1 ⋆ needs to be cast to type Bool with the application label l andraise blame l. The label of applications (e1 e2 )l is helpful for two reasons. Firstly, it is used
to track blame for casts of the argument. Secondly, it is also used to track blame whencasting e1 from ⋆ to the dynamic function type ⋆ → ⋆ (rule S STEP - DYN). In rule S STEP ABETA , l is used to track blame in the cast from v1 to A → B. While removing the annotation¯ if a cast is raised, then the context
A → B, the label of application (v1 v′2 ) is flipped to l:which contains the cast is to blame.
Let us look at two small examples to illustrate reduction behavior and blame tracking.
The first example is the term (((λ x. x ∶l1 ⋆ → ⋆) ∶l2 Bool → Bool) (1 ∶l4 ⋆))l3 , which reduces

24Type-Directed Operational Semantics for Gradual Typing

e z→ r(Small-step Semantics)

S STEP - EVALS STEP - ANNOVS STEP - BLAMEe z→ e′e z→ blame lF[e] z→ F[e′ ]F[e] z→ blame lv ⇓lA r¬(value v ∶l A)v ∶l A z→ r

S STEP -B ETAS STEP - BETAPv ⇓lA1 v′v2 ⇓lA (blame l)⌉v1 ⌈= A → B(v1 v2 )l z→ blame l((λ x. e ∶l A → B) v)l1 z→ e[x ↦ v′ ] ∶l B

S STEP -A BETA

value (v1 ∶l A → B)l((v1 ∶ A → B) v2 )l1

v2 ⇓lA1 v′2¯z→ ((v1 v′2 )l ) ∶l B

S STEP - PIi ∈ {1, 2}
πil (v1 , v2 ) z→ vi
S STEP -C

S STEP - DYN

value (v1 ∶l1 ⋆)⌉v⌈= A → B((v1 ∶l1 ⋆) v2 )l2 z→ ((v1 ∶l1 ⋆ ∶l2 ⋆ → ⋆) v2 )l2v ⇓lA v′(c v)l z→ 〚c〛(v′ )S STEP - PDi ∈ {1, 2}
πil1 (v ∶l0 ⋆) z→ πil1 (v ∶l0 ⋆ ∶l1 ⋆ × ⋆)Fig. 8. Semantics of λ Bgl .
to (blame l3 ).
(((λ x. x ∶l1 ⋆ → ⋆) ∶l2 Bool → Bool) (1 ∶l4 ⋆))l3z→ {by rule S STEP - BETAP}
blame l3
The second example is a term (((λ x. x ∶l1 ⋆ → ⋆) ∶l2 Int → ⋆) (1 ∶l4 ⋆))l3 , which reduces to1 ∶l2 ⋆. We show the detailed reduction steps below:(((λ x. x ∶l1 ⋆ → ⋆) ∶l2 Int → ⋆) (1 ∶l4 ⋆))l3z→ {by rule CAST- VANY and rule S STEP - ABETA }¯(((λ x. x ∶l1 ⋆ → ⋆) 1)l2 ) ∶l2 ⋆z→ {by rule S STEP - EVAL , rule S STEP - BETA}¯((1 ∶l2 ⋆) ∶l1 ⋆) ∶l2 ⋆z→ {by rule S STEP - EVAL , rule S STEP - ANNOV and rule CAST- DD}¯(1 ∶l2 ⋆) ∶l2 ⋆z→ {rule S STEP - ANNOV and rule CAST- DD}¯

1 ∶l2 ⋆
Correspondence with λ Bg . We proved that after removing the blame labels in λ Bgl ,the static and dynamic semantics are the same as in λ Bg (Theorem 4.1). Function ∣ ⋅ ∣removes the blame labels. To distinguish between the typing and reduction relations of25

Journal of Functional Programminge ∶∶= ... ∣ e1 e2Expressions

e z→ r(New Small-Step Semantics)
STEP - APP⌉v1 ⌈= A → B

v2 ⇓lA v′2

STEP - BETA(v1 v2 )l z→ v1 v′2(λ x. e ∶l A → B) v z→ e[x ↦ v] ∶l B

STEP - ABETASTEP - C⌉v1 ⌈= C → Dl¯

c v z→ 〚c〛(v)(v1 ∶l A → B) v2 z→ (v1 (v2 ∶ C)) ∶l B

Fig. 9. New reduction steps.
g

λ Bg and λ Bgl , we use their name as a superscript in the relation. For example, z→λ Bl is
the reduction of λ Bgl .
gg

Theorem 4.1 (Relation between λ Bg and λ Bgl ). Γ ⊢λ Bl e ⇔ A and e z→λ Bl r iff Γ ⊢λ B
g∣e ∣ ⇔ A and ∣e ∣ z→λ B ∣r ∣.

g

4.3 A More Refined Reduction Relation for Proofs
The reduction relation in the previous section is fine for an implementation. However,for some of our proofs, including the completeness to the blame calculus and the gradualguarantee, it is more convenient to have a more refined reduction relation that introducessome additional reduction steps. Here we present the more refined reduction relation. We
proved that this new relation is equivalent to the reduction relation in Section 6.3.
In the new reduction relation (shown in Figure 9), the original rule S STEP - BETA,
rule S STEP - ABETA and rule S STEP -C are divided into two separate steps. While otherrules are the same. Figure 10 illustrates the relationship between the original rules and the
new rules. Take rule STEP - BETA as an example. There are two steps: 1) cast the argument;
and 2) do the substitution. To record that the argument has been cast, we use strict applications e1 e2 . In strict applications, the type of the argument matches the input type offunction e1 . The typing rule for strict applications is:Γ ⊢ e1 ⇒ A → BΓ ⊢ e2 ⇒ AΓ ⊢ e1 e2 ⇒ B

T YP - APPVOther rules follow the same principle as rule STEP - BETA. The first step is to cast theargument, and then do the corresponding operations such as substitution and unwrapping type annotations. The bottom-left triangle in Figure 10 regards that (v1 ∶l A → B) v′2¯
reduces to ((v1 v′2 )l ) ∶l B. Strictly speaking, this does not hold because (v1 ∶l A → B) v′2¯
reduces to (v1 (v′2 ∶l C)) ∶l B for some C such that ⌉v1 ⌈= C → D by rule STEP - ABETA.
¯
However, the result can be regarded as ((v1 v′2 )l ) ∶l B because by rule STEP - APP, appli′ l¯cations (v1 v2 ) convert to strict applications v1 v′′
2 , which can also be written as strict

26

Type-Directed Operational Semantics for Gradual Typing((λ x. e ∶l A → B) v)l1

e[x ↦ v′ ] ∶l B

v
l1

⇓A

′

v

(λ x. e ∶l A → B) v′¯((v1 ∶l A → B) v2 )l1〚c〛(v′ )((v1 v′2 )l ) ∶l B (c v)l

v

v2

l

⇓A

l1

⇓A

′

v

′

v2

(v1 ∶l A → B) v′2

c v′

Fig. 10. Decomposition of reduction steps.
¯

applications v1 (v′2 ∶l C) and the casting is then triggered by annotations. We illustrate the
new reduction on an earlier example shown in Section 6.3.
(((λ x. x ∶l1 ⋆ → ⋆) ∶l2 Int → ⋆) (1 ∶l4 ⋆))l3z→ ((λ x. x ∶l1 ⋆ → ⋆) ∶l2 Int → ⋆) 1¯z→ ((λ x. x ∶l1 ⋆ → ⋆) (1 ∶l2 ⋆)) ∶l2 ⋆¯z→ ((1 ∶l2 ⋆) ∶l1 ⋆) ∶l2 ⋆¯z→ (1 ∶l2 ⋆) ∶l2 ⋆¯z→ 1 ∶l2 ⋆4.4 Soundness and Completeness to λ B
We use an elaboration step in the typing relation to prove the soundness result between
the semantics of λ Bgl and λ B. The elaboration from λ Bgl to λ B is shown at the top oflFigure 11. The elaborating typing relation Γ ⊢ e ⇔ A ↝ t shows how to translate expression
e in λ Bgl to the term t in λ B. The translation does not include products and projections,lsince they are not part of λ B. The typing mode ⇔ includes the infer mode ⇒ and thelchecking mode with labels ⇐. However, in λ Bgl , every rule in checking mode induces
a cast and we need the label for the elaboration into λ B. Therefore, the blame labels of
λ Bgl are transferred to λ B via the checking mode. In particular, in rule TYP - SIM, when we
produce a λ B cast expression we need to use the label that was tracked by the checking
mode. There are three rules where the blame labels are propagated using the checking modein the premises (rule TYP - ABS, rule TYP - APP and rule TYP - ANNO). Note that the λ Bgl
calculus can also act as a source language. An application of expression e1 can, not only

27

Journal of Functional ProgramminglTyping model⇔ ∶∶= ⇒∣⇐l(Elaboration from λ Bgl to λ B)

Γ⊢e⇔A↝t
TYP - APP
TYP - CA ▷ A1 → A2

TYP - VARΓ ⊢ c ⇒⌉c⌈↝ clΓ ⊢ e1 ⇒ A ↝ t1

x∶A ∈ ΓΓ ⊢ e2 ⇐ A1 ↝ t2

Γ ⊢ (e1 e2 )l ⇒ A2 ↝ ⟨t1 , l, A⟩ t2

Γ⊢x⇒A↝x

TYP - ANNO

TYP - SIMlΓ⊢e⇒A↝tΓ⊢e⇐A↝tA∼Bll

Γ⊢e∶ A⇒A↝tlΓ⊢e⇐B↝t ∶A⇒B

TYP - ABS

TYP - APPVlΓ, x ∶ A ⊢ e ⇐ B ↝ tΓ ⊢ e1 ⇒ A → B ↝ t1l

Γ ⊢ λ x. e ∶ A → B ⇒ A → B ↝ λ x ∶ A. tΓ ⊢ e2 ⇒ A ↝ t2

Γ ⊢ e1 e2 ⇒ B ↝ t1 t2
l⟨t, l, ⋆⟩⟨t, l, A → B⟩==t ∶⋆⇒⋆→⋆
t⟪t, l, ⋆⟫⟪t, l, A × B⟫==t ∶⋆⇒⋆×⋆
t

⋆
A→B

▷
▷

⋆→⋆
A→B

⋆
A×B

▸
▸

⋆×⋆
A×B

l

(Elaboration from λ B to λ Bgl )Γ⊩t ∶A↝e
BTYP - C

BTYP - VARΓ ⊩ c ∶⌉c⌈↝ c

BTYP - ABSx∶A ∈ ΓΓ, x ∶ A ⊩ t ∶ B ↝ e ∶l B

Γ⊩x∶A↝xΓ ⊩ λ x ∶ A. t ∶ A → B ↝ (λ x. e) ∶l A → B
BTYP - CASTBTYP -A PP

Γ ⊩ t1 ∶ A → B ↝ e 1

Γ ⊩ t2 ∶ A ↝ e2

Γ ⊩ t1 t2 ∶ B ↝ e1 e2Γ⊩t ∶A↝eA∼BlΓ ⊩ t ∶ A ⇒ B ∶ B ↝ e ∶l B

Fig. 11. Elaboration between λ Bgl and λ B.

infer a function type, but also infer the unknown type ⋆. Thus, the function ⟨t, l, A⟩ adds acast from ⋆ to ⋆ → ⋆ to the λ B term. At the bottom of Figure 11, we show the elaborationfrom λ B to λ Bgl . The elaboration typing relation Γ ⊩ t ∶ A ↝ e shows the expression t in
λ B to the expression e in λ Bgl . The elaboration is straightforward. One thing that needs tobe mentioned is that for rule BTYP - ABS the lambda body (t) is elaborated to an annotatedexpression, since the body is in checking mode, which triggers an implicit cast. To bealigned between these two calculi, the λ B calculus adds an identity cast for the lambda
body.

28

Type-Directed Operational Semantics for Gradual Typing

Theorem 4.2 states that both elaborations are type preserving. Theorem 4.3 shows thesoundness and completeness property between the dynamic semantics of λ Bgl and λ B.
We use ⇑ to represent that a term diverges. The soundness and completeness result are
proved using the auxiliary lemmas 4.1, 4.2 , 4.3 and 4.4. In Lemma 4.3, t z→ j t ′ meansthat t takes j steps to evaluate to t ′ . Lets take an example that shows how can t ′ reducel1

l2

to error. In λ B, we can have a program (i ∶ Int ⇒ ⋆) ∶ ⋆ ⇒ Int → Int which corresponds toi ∶l1 ⋆ ∶l2 Int → Int in our λ Bgl . In λ Bgl , error is raised directly but λ B first reduces to ((i ∶
l1

l2

l2

Int ⇒ ⋆) ∶ ⋆ ⇒ ⋆ → ⋆) ∶ ⋆ → ⋆ ⇒ Int → Int and then raises the error.
Theorem 4.2 (Type Preservation of Elaboration).
l• If Γ ⊢ e ⇔ A ↝ t then Γ ⊩ t ∶ A.
• If Γ ⊩ t ∶ A ↝ e then Γ ⊢ e ⇒ A.
Lemma 4.1 (Soundness of λ Bgl Casting with respect to λ B for Values). If ⋅ ⊢ v ∶l A ⇒ A ↝ tand v ⇓lA v′ then ∃t ′ , t z→∗ t ′ and ⋅ ⊢ v′ ⇒ A ↝ t ′ .
Lemma 4.2 (Soundness of λ Bgl Casting with respect to λ B for Blame). If ⋅ ⊢ v ∶l A ⇒ A ↝ tand v ⇓lA (blame l) then t z→∗ blame l.
Lemma 4.3 (Completeness of λ Bgl Casting with respect to λ B for Values). If ⋅ ⊩ t ∶ B ↝lv and t ∶ B ⇒ A z→ t ′ then (∃ j t ′′ v′ , 0 ≤ j ≤ 1, t ′ z→ j t ′′ , v ⇓lA v′ and ⋅ ⊩ t ′′ ∶ A ↝ v′ ) or(t ′ z→ blame l and v ⇓lA (blame l)).
Lemma 4.4 (Completeness of λ Bgl Casting with respect to λ B for Blame). If ⋅ ⊩ t ∶ B ↝ v
land t ∶ B ⇒ A z→ blame l then v ⇓lA (blame l).
Theorem 4.3 (Soundness and Completeness between λ Bgl and λ B).
1) if ⋅ ⊢ e ⇒ A ↝ t and e z→∗ v then ∃v′ , t z→∗ v′ and ⋅ ⊢ v ⇒ A ↝ v′ .
2) if ⋅ ⊢ e ⇒ A ↝ t and e z→∗ blame l then t z→∗ blame l.
3) if ⋅ ⊢ e ⇒ A ↝ t and e ⇑ then t ⇑.
4) if ⋅ ⊩ t ∶ A ↝ e and t z→∗ v then ∃v′ , e z→∗ v′ and ⋅ ⊩ v ∶ A ↝ v′ .
5) if ⋅ ⊩ t ∶ A ↝ e and t z→∗ blame l then e z→∗ blame l.
6) if ⋅ ⊩ t ∶ A ↝ e and t ⇑ then e ⇑.
4.5 Gradual Guarantee
Siek et al. (2015b) suggested that a calculus for gradual typing should also enjoy thegradual guarantee, which ensures that programs can smoothly move from being more/less dynamically typed into more/less statically typed. We show how to prove the gradualguarantee for λ Bgl next.
Precision. The top of Figure 12 shows the precision relation on types. A ⊑ B means that
A is more precise than B. Every type is more precise than type ⋆. A function type A1 →B1 is more precise than A2 → B2 if type A1 is more precise then A2 and type B1 is more
precise than B2 . A product type A1 × B1 is more precise than A2 × B2 if type A1 is more

29

Journal of Functional Programming
A ⊑ B(Precision relation for types)
TPRE - ABS

TPRE - I

TPRE - DYN

Int ⊑ IntA⊑⋆

TPRE - PRO

A1 ⊑ A2

B1 ⊑ B2A1 ⊑ A2(A1 → B1 ) ⊑ (A2 → B2 )

Γ1 ; Γ2 ⊢ e1 ⊑ e2

B1 ⊑ B2

A1 × B1 ⊑ A2 × B2

(Precision relation for expressions)
EPRE - ABS

A1 → B1 ⊑ A2 → B2
Γ1 , x ∶ A1 ; Γ2 , x ∶ A2 ⊢ e1 ⊑ e2

EPRE - C

EPRE - X

Γ1 ; Γ2 ⊢ c ⊑ c

Γ1 ; Γ2 ⊢ x ⊑ x

Γ1 ; Γ2 ⊢ λ x. e1 ∶l A1 → B1 ⊑ λ x. e1 ∶l A2 → B2

EPRE - APP

EPRE - APPVΓ1 ; Γ2 ⊢ e1 ⊑ e′1

Γ1 ; Γ2 ⊢ e2 ⊑ e′2

Γ1 ; Γ2 ⊢ e1 ⊑ e′1

Γ1 ; Γ2 ⊢ (e1 e2 )l ⊑ (e′1 e′2 )lΓ1 ; Γ2 ⊢ e2 ⊑ e′2

Γ1 ; Γ2 ⊢ e1 e2 ⊑ e′1 e′2
EPRE - ANNO L

EPRE - PRO

Γ1 ; Γ2 ⊢ e1 ⊑ e′1

Γ1 ; Γ2 ⊢ e2 ⊑ e′2
Γ1 ; Γ2 ⊢ (e1 , e2 ) ⊑ (e′1 , e′2 )Γ1 ⊢ e1 ⇒ A1
Γ1 ; Γ2 ⊢ e1 ⊑ e2

Γ2 ⊢ e2 ⇒ A2
A ⊑ A2A1 ⊑ A2

Γ1 ; Γ2 ⊢ e1 ∶l A ⊑ e2

EPRE - ANNO R

Γ1 ⊢ e1 ⇒ A1
Γ1 ; Γ2 ⊢ e1 ⊑ e2

Γ2 ⊢ e2 ⇒ A2
A1 ⊑ A2A1 ⊑ AlΓ1 ; Γ2 ⊢ e1 ⊑ e2 ∶ A

EPRE - ANNOA⊑B

Γ1 ; Γ2 ⊢ e1 ⊑ e2

Γ1 ; Γ2 ⊢ e1 ∶l A ⊑ e2 ∶l B

EPRE - PI

Γ1 ; Γ2 ⊢ e1 ⊑ e2
Γ1 ; Γ2 ⊢ πil e1 ⊑ πil e2
Fig. 12. Precision relations.
precise then A2 and type B1 is more precise than B2 . The bottom of Figure 12 shows theprecision relation for expressions. Γ1 ; Γ2 ⊢ e1 ⊑ e2 means that e1 is more precise than e2
under typing contexts Γ1 and Γ2 . The precision relation of expressions is derived fromthe precision relation of types. Every expression is related to itself. There are contexts Γ1
for e1 and Γ2 for e2 . The typing contexts are needed because some rules only work forwell-typed expressions, and the typing judgement requires typing contexts. We use thefollowing abbreviation e1 ⊑ e2 ≡ ⋅; ⋅ ⊢ e1 ⊑ e2 , when the contexts of the expressions are
empty.
For annotation expressions, precision is defined as follows: e1 ∶ A is more precise thane2 ∶ B if e1 is more precise than e2 and A is more precise than B. Similarly, for projections precision holds if the precision between e1 and e2 holds. Two lambdas are related
when their bodies and annotated types are related. In applications ((e1 e2 )l and e1 e2 ) andproductions ((e1 , e2 )), precision holds if the precision between e1 and e′1 holds and theprecision between e2 and e′2 holds.

30Type-Directed Operational Semantics for Gradual Typing

An important complication arises from the presence of values with an unknown typesuch as 1 ∶ ⋆. The term 1 ∶ Int is more precise than 1 ∶ ⋆, but while 1 ∶ ⋆ is a value, theterm 1 ∶ Int reduces to 1. Similarly, the term (λ x. x) ∶ Int → Int ∶ ⋆ is more precise than
(λ x. x) ∶ ⋆ → ⋆ ∶ ⋆, while (λ x. x) ∶ ⋆ → ⋆ ∶ ⋆ is a value and (λ x. x) ∶ Int → Int ∶ ⋆ reduces to(λ x. x) ∶ Int → Int ∶ ⋆ → ⋆ ∶ ⋆. Such examples create the need for the precision relation todeal with unaligned expressions. These unaligned cases are covered by rule EPRE - ANNOL
and rule EPRE - ANNOR. Rule EPRE - ANNOL deals with more precise programs with extra
annotations, while rule EPRE - ANNOR is for less precise programs with extra annotations.
To ensure that the extra type annotations preserve the type precision relation, the typing
judgement is used.
Static Criteria. The dynamic counterpart of expressions (ě) (basically expressions without
type annotations) can be encoded in λ Bgl by the translation function (⌈ě⌉), which annotates
dynamic expressions with type ⋆ (Theorem 4.4). The translation function is:⌈x⌉ = x⌈c⌉ = c ∶l ⋆⌈λ x.ě⌉ = λ x.⌈ě⌉ ∶l1 ⋆ → ⋆ ∶l2 ⋆⌈eˇ1 eˇ2 ⌉ = (⌈eˇ1 ⌉ ⌈eˇ2 ⌉)l⌈(eˇ1 , eˇ2 )⌉ = (⌈eˇ1 ⌉, ⌈eˇ2 ⌉) ∶l ⋆⌈πi ě⌉ = πil ⌈ě⌉
Furthermore, if all expressions are static, the type system of λ Bgl is equivalent to a fully
static type system (Theorem 4.5). The predicate static on e and A means that the expression and type are fully static. The static type system is represented as ⊢S which is alsobidirectional but only type checks the static expressions. Theorem 4.6 shows that the static
gradual guarantee holds for the λ Bgl calculus. It says that if e is more precise than e′ and e
has type A then e′ has type B and type A is more precise than B.
Theorem 4.4 (Dynamic Embedding). If ě is closed then ⋅ ⊢ ⌈ ě ⌉ ⇒ ⋆.
Theorem 4.5 (Equivalence for Static Type System). For all static e and A, ⋅ ⊢S e ⇔ A iff⋅ ⊢ e ⇔ A.
Theorem 4.6 (Static Gradual Guarantee of λ Bgl Calculus). If e ⊑ e′ and ⋅ ⊢ e ⇔ A then ∃B,⋅ ⊢ e′ ⇔ B and A ⊑ B.
Dynamic Gradual Guarantee. We formalized and proved the dynamic gradual guarantee for the λ Bgl calculus. Theorems 4.7 and Theorem 4.8 show that less precise
programs will not change the dynamic semantics of programs. Lemma 4.5 is an important auxiliary lemma for Theorem 4.7 and Theorem 4.8. Notably, the dynamic gradualguarantee (Theorem 4.9) is a corollary of Theorem 4.7 and Theorem 4.8.
Lemma 4.5 (Dynamic Gradual Guarantee for Casting). If v1 ⊑ v2 , ⋅ ⊢ v1 ⇐ A1 , ⋅ ⊢ v2 ⇐ B1
, A ⊑ B and v1 ⇓lA1 v′1 then ∃v′2 , v2 ⇓lB2 v′2 and v′1 ⊑ v′2 .
Theorem 4.7 (Dynamic Gradual Guarantee ⊑ ). If e1 ⊑ e2 , ⋅ ⊢ e1 ⇔ A, ⋅ ⊢ e2 ⇔ B ande1 z→ e′1 then ∃e′2 , e2 z→∗ e′2 and e′1 ⊑ e′2 .

Journal of Functional Programming

31

Theorem 4.8 (Dynamic Gradual Guarantee ⊒ ). Suppose e1 ⊑ e2 , ⋅ ⊢ e1 ⇔ A and ⋅ ⊢ e2 ⇔B.
• If e2 z→ e′2 then (∃e1 , e1 z→∗ e′1 and e′1 ⊑ e′2 ) or (∃l, e1 z→∗ blame l).
• If e2 z→ blame l2 then ∃l1 , e1 z→∗ blame l1 .
Theorem 4.9 (Dynamic Gradual Guarantee). Suppose e1 ⊑ e2 , ⋅ ⊢ e1 ⇔ A and ⋅ ⊢ e2 ⇔ B.
• If e1 z→∗ v1 then ∃v2 , e2 z→∗ v2 and v1 ⊑ v2 .
• If e1 ⇑ then e2 ⇑.
• If e2 z→∗ v2 then e1 z→∗ v1 and v1 ⊑ v2 , or e1 z→∗ blame l.
• If e2 ⇑ then e1 ⇑ or e1 z→∗ blame l.
4.6 Blame Theorem
The blame theorem (Wadler & Findler, 2009) shows that a cast from a more precise type toa less precise type cannot raise positive blame, but negative blame is possible. In addition,a cast from a less precise type to a more precise type cannot raise negative blame, but
positive blame is possible. The blame theorem has been proved for the λ B calculus. Fromthe soundness theorem, which we have shown above, terms in λ Bgl raise blame with labell, and the corresponding terms in λ B raise blame with the same label. Thus, the blame
theorem also holds in λ Bgl . However, this proof of the blame theorem relies on the existenceof λ B. While this proof technique works, we cannot easily use it if we extend λ Bgl withnew features, because that would require similar extensions to λ B. For instance, we opted
to add products and projections in λ Bgl , which are not available in λ B. Thus, we cannot
obtain the blame theorem for λ Bgl with products via the soundness theorem. Furthermore,
having to rely on another calculus makes the proof rather indirect and involved. Therefore,
here we show that we can also prove the blame theorem directly on λ Bgl .
The top of Figure 13 shows the subtyping, positive subtyping, and negative subtyping
relations, which are the same as those for λ B. Note that our type precision is also the sameas the naive subtyping relation in λ B. Therefore, Lemma 4.6 and Lemma 4.7 show that
subtyping and type precision factor negative and positive subtyping as in λ B.
At the bottom of Figure 13 we have the safe terms for λ Bgl . The relation Γ ⊢ e safe for ldenotes that e is safe for label l under typing context Γ. For safe terms, after the reduction ofe, label l can never be raised. Labels are raised only when casting is performed. Therefore,
safe terms require us to consider all the casts (explicit or implicit) in the expressions. In
the safe term definition, we are making implicit casts explicit. There are no casts in x andc so they are safe for label l (rule SF - VAR and rule SF - C). Lambda abstractions induce acast from the type of the lambda body to the annotated function output type. Consequently,(λ x. e ∶l1 A1 → A2 ) is safe for label l2 if e ∶l1 A2 is safe for label l2 (rule SF - ABS). Obviously,
if one label does not appear in the expression, the expression is safe for that label. So e ∶l1 A
is safe for l2 if l2 is not equal to (l1 , l¯1 ) and e is safe for l2 (rule SF - EQ). Even when the
checking label is the same as the casting label, if the type of the source type is a positive
subtype of the target type then the cast is also safe for the checking label (rule SF - NEQA).
In the expression 1 ∶l1 ⋆, the cast from Int to ⋆, will not raise blame with label l1 . In
general, e ∶l B is safe for l if e is safe for l and A (the type of e) is a positive subtype of B.

32

Type-Directed Operational Semantics for Gradual Typing

A <∶ B(Subtyping)
SUB - ARR

SUB - INTSUB - DYN

Int <∶ Int⋆ <∶ ⋆SUB - ADYNSUB - PROB1 <∶ B2

A <∶ GA1 <∶ A2

A1 → B1 <∶ A2 → B2

A <∶ ⋆

A1 × B1 <∶ A2 × B2

A2 <∶ A1

A <∶+ BB1 <∶ B2

(Positive Subtyping)
SUBA - ARR

SUBA - INT

SUBA - DYN

Int <∶+ Int

A <∶+ ⋆

SUBA - PRO

A2 <∶− A1

B1 <∶+ B2

A1 <∶+ A2

A1 → B1 <∶+ A2 → B2

B1 <∶+ B2

A1 × B1 <∶+ A2 × B2

A <∶− B

(Negative Subtyping)
SUBB - ARR

SUBB - INT

SUBB - DYN

Int <∶− Int⋆ <∶− ASUBB - ADYN

A2 <∶+ A1

B1 <∶− B2

A <∶− G

A1 → B1 <∶− A2 → B2

A <∶− BSUBB - PRO

A1 <∶− A2

B1 <∶− B2

A1 × B1 <∶− A2 × B2
Γ ⊢ e safe for l(Safe Terms)
SF - ABSΓ, x ∶ A1 ⊢ (e ∶l1 A2 ) safe for l2

SF - VAR

SF - CΓ ⊢ x safe for lΓ ⊢ c safe for lΓ ⊢ λ x. e1 ∶l1 A1 → A2 safe for l2

SF - APPΓ ⊢ e1 ⇒ A
A ▷ A1 → A2Γ ⊢ ⟨e1 , l1 , A⟩ safe for l2Γ ⊢ (e2 ∶l1 A1 ) safe for l2

SF - EQ

l1 ≠ l2l1

l¯1 ≠ l2Γ ⊢ e safe for l2l1Γ ⊢ (e1 e2 ) safe for l2Γ ⊢ e ∶ A safe for l2
SF - NEQA

SF - APPVΓ ⊢ e1 safe for lΓ⊢e⇒AΓ ⊢ e2 safe for lΓ ⊢ e safe for llΓ ⊢ e1 e2 safe for lΓ ⊢ e ∶ B safe for l

SF - NEQBΓ⊢e⇒AA <∶+ BSF - PROA <∶− BΓ ⊢ e safe for lΓ ⊢ e1 safe for ll¯Γ ⊢ e ∶ B safe for lΓ ⊢ e2 safe for lΓ ⊢ (e1 , e2 ) safe for l

SF - PIA ▸ A1 × A2Γ⊢e⇒AΓ ⊢ ⟪e, l1 , A⟫ safe for l2Γ ⊢ πil1 e safe for l2
Fig. 13. Safe expressions of λ Bgl .

Journal of Functional Programming
Types
Expressions
Results
Raw values
Value
Contexts
Frames33

A, B, C ∶∶= Int ∣ A → B ∣ ⋆ ∣ A1 × A2
e ∶∶= x ∣ c ∣ e1 e2 ∣ e ∶ A ∣ (e1 , e2 ) ∣ πi e ∣ λ x. e ∣ Lp ∶ AMr ∶∶= e ∣ blamep ∶∶= c ∣ (λ x. e ∶ A1 → B1 ) ∶ A2 → B2 ∣ (p1 , p2 )v ∶∶= Lp ∶ AM
Γ ∶∶= ⋅ ∣ Γ, x ∶ A
F ∶∶= ◻ e ∣ (v, ◻) ∣ (◻, e) ∣ πi ◻ ∣ ◻ ∶ A ∣ (λ x. e) ◻ ∣ Lc ∶ AM ◻
Fig. 14. Syntax of the λ e calculus.

Annotation e ∶l B is safe for l¯ if e is safe for l and A (the type of e) is a negative subtype ofB (rule SF - NEQB). For example, (λ x. x ∶l1 ⋆ → Int ∶l2 Int → Int) should be safe for l¯2 since
when the argument is applied, which triggers a cast from Int to ⋆ with l¯2 , blame cannot beraised. For (e1 e2 )l1 , if e1 has type ⋆, there are two implicit casts: one is for e1 , which casts
from ⋆ to ⋆ → ⋆, and the other is for e2 cast from the type of e2 to the input type of functionof e1 . Therefore, if e1 has type ⋆, (e1 e2 )l1 is safe for label l2 if e1 ∶l1 ⋆ → ⋆ is safe for l2 ande2 ∶l1 ⋆ is safe for l2 . While e1 has type A → B, (e1 e2 )l1 is safe for label l2 if e1 is safe forl2 and e2 ∶l1 A is safe for l2 (rule SF - APP). Similarly, for rule SF - PI, if e1 has type ⋆, thereis implicit cast from ⋆ to ⋆ × ⋆. Thus if e has type ⋆, πi e l1 is safe for label l2 if e ∶l1 ⋆ × ⋆is safe for l2 . The cast is added via the function ⟪e, l, A⟫ at the bottom of figure 11. If e
has type A × B, πil1 e is safe for label l2 if e is safe for l2 . Strict applications (e1 e2 ) andproductions (e1 , e2 ) are safe for l, if the sub-term e1 and e2 are safe for l (rule SF - APPV).
Lemma 4.8 shows the preservation of safe expressions: if e is safe for l and e reduces
to e′ then e′ is safe for l. Lemma 4.9 says that if e is safe for l then l will not be raised.
By Lemma 4.8, 4.9, 4.6 and 4.7, we can derive Corollary 4.9.1, showing that if blame israised, the less precise program is to blame.
Lemma 4.6 (Factoring Subtyping). A <∶ B if and only if A <∶+ B and A <∶− B.
Lemma 4.7 (Factoring Precision). A ⊑ B if and only if A <∶+ B and B <∶− A.
Lemma 4.8 (Preservation of Safe Expressions). If ⋅ ⊢ e ⇔ A, ⋅ ⊢ e safe for l and e z→ e′then ⋅ ⊢ e′ safe for l.
Lemma 4.9 (Progress of Safe Expressions). If ⋅ ⊢ e ⇔ A and ⋅ ⊢ e safe for l then e z→/
blame l.
Corollary 4.9.1 (Well-typed programs cannot be blamed). Let e be a well typed term witha subterm e′ ∶l B where e′ is well typed with type A, containing the only occurrences of l ine, and l¯ does not appear in e.
∗• If A <∶+ B then e z→
/ blame l.
∗• If A <∶− B then e z→
/ blame l.¯∗∗• If A <∶ B then e z→
/ blame l and e z→
/ blame l.¯∗• If A ⊑ B then e z→
/ blame l.
∗• If B ⊑ A then e z→
/ blame l.¯

34Type-Directed Operational Semantics for Gradual Typing
5 The λ e Calculus

In this section, we will introduce a gradually typed calculus with a variant of the eager
semantics (Herman et al., 2007), inspired by AGT (Garcia et al., 2016). The main idea inthis variant of the eager semantics is that if a function value flows through multiple casts,
the effect of those casts is preserved in the updated function value. In particular, all types
involved in the multiple casts must be checked for consistency.
5.1 Syntax
The syntax of the λ e calculus is shown in Figure 14.
Types, Expressions and Results. A type in λ e is either an integer type Int, a function
type A → B , an unknown type ⋆ or a product type A × B. For expressions and results, λ e isextended with tagged values Lp ∶ AM with respect to λ Bg .
Values. Metavariable p ranges over raw values. Constants c, annotated lambdas (λ x. e ∶A1 → B1 ) ∶ A2 → B2 and products (p1 , p2 ) are included in the raw values. Values are tagged
raw values. The metavariable v denotes values, which are annotated values (Lp ∶ AM). Thus
Li ∶ AM and Lλ x. e ∶ A1 → B1 ∶ A2 → B2 ∶ CM are examples of values. Notably, in contrast with
λ Bg , λ e’s notion of (well-formed) values is purely syntactic: no additional constraints(besides syntax) are needed. Moreover, it should be noted that in λ e values have a bounded
number of annotations (up-to three for lambda values), unlike the λ Bg calculus. We should
remark that we choose to use tagged values for simplicity. It should be possible to use amore refined notion of values where some values would require no type tag, as in λ Bg .
Although this would probably require some different rules to distinguish between thosedifferent forms of values.
Contexts and Frames. Typing environments are just the same as in the λ Bg calculus. In
frames, compared to the λ Bg calculus, the first expression in an application is not a value,
but a raw lambda.
5.2 Type System
As the λ Bg calculus, bidirectional typing is used. Before showing the typing rules, we
present the dynamic type function.
Dynamic Types for the λ e Calculus. As in the λ Bg calculus, dynamic types play animportant role in the calculus. ⌉p⌈ denotes the dynamic type of p, and ⌉v⌈ denotes the
dynamic type of v. We need both dynamic types for raw values and values, and we candefine dynamic types easily.

35

Journal of Functional Programming
Γ⊢e⇔A(Typing Rules)

TYP- LITΓ ⊢ c ⇒⌉c⌈

TYP- VAR

TYP- ABSx∶A ∈ ΓA ▷ A1 → A2

Γ⊢x⇒AΓ, x ∶ A1 ⊢ e ⇐ A2

Γ ⊢ λ x. e ⇐ A

TYP- APPA ▷ A1 → A2
Γ ⊢ e1 ⇒ A
Γ ⊢ e2 ⇐ A1

TYP- ANNO

TYP- SIMΓ⊢e⇐AΓ ⊢ e1 e2 ⇒ A2Γ⊢e⇒AΓ⊢e∶A⇒AΓ⊢e⇐B

TYP- PRODUCTTYP- ABSVΓ, x ∶ A ⊢ e ⇐ BΓ ⊢ e1 ⇒ A

Γ ⊢ e2 ⇒ AΓ ⊢ e2 ⇒ B

Γ ⊢ (e1 , e2 ) ⇒ A × BΓ ⊢ (λ x. e) e2 ⇐ B
TYP- PRODUCTI

Γ⊢e⇒A

A∼B

TYP- VALUE

i ∈ {1, 2}

A ▸ A1 × A2⋅⊢ p⇐AΓ ⊢ πi e ⇒ Ai⌉p⌈⊑ AΓ ⊢ Lp ∶ AM ⇒ A

A ⊑ B(Precision relation for types)
TPRE - ABS

TPRE - I

TPRE - DYN

Int ⊑ IntA⊑⋆

TPRE - PRO

A1 ⊑ A2

B1 ⊑ B2(A1 → B1 ) ⊑ (A2 → B2 )A1 ⊑ A2

B1 ⊑ B2

A1 × B1 ⊑ A2 × B2

Fig. 15. Typing rules for λ e.
Definition 5.1 (Dynamic type). ⌉p⌈ returns the dynamic type of the raw values p. ⌉v⌈
returns the dynamic type of the annotated value v.
⌉i⌈ = Int⌉+⌈ = Int → Int → Int⌉+i ⌈ = Int → Int⌉((λ x. e ∶ A1 → B1 ) ∶ A2 → B2 )⌈ = A2 → B2⌉(p1 , p2 )⌈ =⌉p1 ⌈×⌉p2 ⌈⌉Lp ∶ AM⌈ = A
Typing Rules for the λ e Calculus. In λ e, raw lambdas are checked by function types or
the unknown type ⋆. Raw lambdas are allowed in applications by using rule TYP- ABSV.
This rule is important to allow beta-reductions to type-check, and is essentially a runtime
checking rule. That is, rule TYP- ABSV is used to enable certain intermediate expressions
that arise from reduction to type-check. Otherwise, using rule TYP- APP, in an application,
the function input type is the type of the argument. In rule TYP- VALUE, a well-typed
value ensures that the inner raw value p can be checked by the annotated type A. Also the
dynamic type of the raw value should be more precise than annotated type A. The bottomof Figure 15 shows the precision relation on types. A ⊑ B means that A is more precise than36

Type-Directed Operational Semantics for Gradual Typingp ⇓A r(Casting for λ e)
CAST- ABS
CAST- CA1 → A2 ∼ C

c ⇓A c(λ x. e ∶ A1 → A2 ) ∶ B ⇓C (λ x. e ∶ A1 → A2 ) ∶ C

CAST- ABSP

CAST- PRO

p1 ⇓A1 p′1

A1 → A2 ≁ C

p2 ⇓A2 p′2(p1 , p2 ) ⇓A1 ×A2 (p′1 , p′2 )(λ x. e ∶ A1 → A2 ) ∶ B ⇓C blame
CAST- PROL

CAST- PROR

p1 ⇓A1 blame

p1 ⇓A1 p′1

p2 ⇓A2 r(p1 , p2 ) ⇓A1 ×A2 blame

p2 ⇓A2 blame(p1 , p2 ) ⇓A1 ×A2 blame(Type Meet)A ⊓ B =C
MEET- ARR
MEET- INT

MEET- DYNL

MEET- DYNR

A1 ⊓ A2 = A3

Int ⊓ Int = Int

⋆⊓A=A

A⊓⋆=A

A1 → B1 ⊓ A2 → B2 = A3 → B3

B1 ⊓ B2 = B3

MEET- PROA1 ⊓ A2 = A3

B1 ⊓ B2 = B3

A1 × B1 ⊓ A2 × B2 = A3 × B3

Fig. 16. Casting for the λ e Calculus.

B. Type precision is the same as in λ Bgl . Other typing rules are exactly the same as thoseused by the λ Bg calculus in Figure 3. Lemmas about dynamic types and a typing lemma
about the inference mode include:
Lemma 5.1 (Dynamic Types of Raw Values). If ⋅ ⊢ p ⇒ A then ⌉p⌈= A.
Lemma 5.2 (Dynamic Types of Values). If ⋅ ⊢ v ⇒ A then ⌉v⌈= A.
Lemma 5.3 (Inference Uniqueness). If Γ ⊢ e ⇒ A1 and Γ ⊢ e ⇒ A2 then A1 = A2 .
5.3 Dynamic Semantics
As in the λ Bg calculus, casting is used in the semantics to get a direct operationalsemantics.
Casting. The casting rules are shown in Figure 16. Compared to λ Bg , the rules are simpler.
The casting relation casts raw values instead of values. Rule CAST- C returns the constantc. Rule CAST- ABS shows that if the type of annotated lambdas A1 → A2 is consistent
with type C, then type B is replaced by C. Otherwise, if type A1 → A2 is not consistent
with type C, casting raises blame using rule CAST- ABSP. In rule CAST- PRO, when aproduct (p1 , p2 ) is cast under product type A1 × A2 , we cast both components under A1

Journal of Functional Programming

37

and A2 , respectively and return a product of the resulting raw values. Rule CAST- PROL
and rule CAST- PROR cover the case when the casts of p1 and p2 raise blame.
Casting Properties. Casting for the λ e calculus has some interesting properties, similar
to those shown in Section 3. In these Lemmas, the meet of two types (⊓) is defined at thebottom of Figure 16. The meet of two types is the greatest lower bound between the types
in terms of precision. That is, it is the most imprecise type among the types equivalent toor more precise than the given types.
Lemma 5.4 (Preservation of Casting). If ⋅ ⊢ p ⇐ A, ⌉p⌈⊓B = A and p ⇓A p′ then ⋅ ⊢ Lp′ ∶BM ⇒ B.
Lemma 5.5 (Progress of Casting). If ⋅ ⊢ p ⇐ A′ and ⌉p⌈⊓A = A′ then ∃r, p ⇓A′ r.
Lemma 5.6 (Determinism of Casting). If ⋅ ⊢ p ⇐ B, p ⇓A r1 and p ⇓A r2 then r1 = r2 .
Reduction. Figure 17 shows the reduction rules of the λ e calculus. Rule STEP- BETA is
the usual beta reduction rule. For rule STEP- APP, the argument e2 is annotated with the
input types, and the annotations with the output types are added in the final expression.
As the type system shows, the unknown type ⋆ can be matched as a function type ⋆ → ⋆or a product ⋆ × ⋆. Because the ⋆ type is consistent with any types, there can be run-time
type-errors. For instance (1 ∶ ⋆) 1 and πi (1 ∶ ⋆) raise errors at runtime. Rule STEP- DYN
and rule STEP- PROIP raise blame if the raw values cannot match with function types andproduct types, respectively. Rule STEP- PRO extracts type annotations from a pair of values
and rule STEP- PROI projects the corresponding value. Rule STEP- ABS and rule STEPI add an extra annotation with the dynamic type to produce a value. For values Lp ∶ AM
annotated with a type B, we perform consistency checking between the dynamic type of
p and B. When consistency checking fails, blame is raised using rule STEP- ANNOP. If
consistency checking succeeds, the raw value p is cast by the meet result of A′ and B. If
the casting succeeds, the result of casting annotated with type B is returned (rule STEPANNOV ), otherwise blame is raised using rule STEP- ANNOVP . Note that these two rules
and casting are the essence of our variant of the eager semantics: consistency checking
happens directly, instead of waiting for the argument to be applied for high-order values.
For additions (+ and +i ), if the argument is an integer then it can be used to do the operation(rule STEP- C) otherwise an error is raised (rule STEP- CF and rule STEP- CFA).
Example. Let us use an example to explain the behavior of casting with the eager semantics. Suppose that we take a chain of annotations λ x. x ∶ ⋆ → Int ∶ Int → ⋆ ∶ ⋆ ∶ Bool → Bool.

38

Type-Directed Operational Semantics for Gradual Typing

e z→ r(Small-step semantics for the λ e calculus)

STEP- EVAL

STEP- BLAME
STEP- BETAe z→ e′e z→ blame

F[e] z→ F[e′ ]F[e] z→ blame(λ x. e) v z→ e[x ↦ v]

STEP- APPC ▷ C1 → C2
(L((λ x. e ∶ A1 → A2 ) ∶ B1 → B2 ) ∶ CM) e2 z→ ((λ x. e) (e2 ∶ C1 ∶ B1 ∶ A1 )) ∶ A2 ∶ B2 ∶ C2
STEP- DYN

STEP- PROIP⌉p⌈≁ ⋆ → ⋆i ∈ {1, 2}⌉p⌈≁ ⋆ × ⋆Lp ∶ AM v2 z→ blame

πi Lp ∶ AM z→ blame
STEP- PROI

STEP- PROA ▷ A1 × A2

(Lp1 ∶ AM, Lp2 ∶ BM) z→ L(p1 , p2 ) ∶ A × BMi ∈ {1, 2}

πi L(p1 , p2 ) ∶ AM z→ Lpi ∶ Ai M

STEP- ABS
STEP- IA ▷ A1 → A2
(λ x. e) ∶ A z→ L(λ x. e ∶ A1 → A2 ) ∶ A1 → A2 ∶ AM
STEP- ANNOPc z→ Lc ∶⌉c⌈M

STEP- ANNOV

STEP- ANNOVP⌉p⌈⊓B = A′⌉p⌈≁ B
Lp ∶ AM ∶ B z→ blamep ⇓A′ p′⌉p⌈⊓B = A′′p ⇓A′ blame

Lp ∶ AM ∶ B z→ blame

Lp ∶ AM ∶ B z→ Lp ∶ BM

STEP- CFSTEP- CA ▷ A1 → A2⌉c⌈= B1 → B2⌉p⌈∼ B1

Lc ∶ AM Lp ∶ BM z→ (〚c〛(p)) ∶ A2⌉c⌈= B1 → B2⌉p⌈≁ B1

Lc ∶ AM Lp ∶ BM z→ blame

STEP- CFA

Lc ∶ AM (λ x. e) z→ blame
Fig. 17. Semantics of the λ e Calculus.
The reduction (and casting) steps to reduce such an expression are shown next:
λ x. x ∶ ⋆ → Int ∶ Int → ⋆ ∶ ⋆ ∶ Bool → Boolz→ {by rule STEP- ABS}Lλ x. x ∶ ⋆ → Int ∶ ⋆ → Int ∶ ⋆ → IntM ∶ Int → ⋆ ∶ ⋆ ∶ Bool → Boolz→ {by rule STEP- ANNOV and casting under Int → Int}Lλ x. x ∶ ⋆ → Int ∶ Int → Int ∶ Int → ⋆M ∶ ⋆ ∶ Bool → Boolz→ {by rule STEP- ANNOV and casting under Int → Int}Lλ x. x ∶ ⋆ → Int ∶ Int → Int ∶ ⋆M ∶ Bool → Boolz→ {by rule STEP- ANNOP}

blame

Journal of Functional Programming

39

Firstly, λ x. x ∶ ⋆ → Int reduces to a value Lλ x. x ∶ ⋆ → Int ∶ ⋆ → Int ∶ ⋆ → IntM. Type ⋆ → Int is
consistent with type Int → ⋆ and the meet of these two types is Int → Int. So the intermediate type ⋆ → Int is replaced by Int → Int and the outer type is replaced by ⋆ → Int. Similarly,
Int → Int is consistent with type ⋆ and the meet of these two types is still Int → Int. So
only the outer type is replaced by type ⋆. Finally, type Int → Int is not consistent with
Bool → Bool so blame is raised.
One important property is that the reduction relation is deterministic:
Theorem 5.1 (Determinism of the λ e Calculus). If ⋅ ⊢ e ⇔ A, e z→ r1 and e z→ r2 thenr1 = r2 .
Type Soundess. Another important property is that the λ e calculus is type sound.
Theorems 5.2 and 5.3 for type preservation and progress, respectively, have the same form
as in λ Bg .
Theorem 5.2 (Type Preservation of the λ e Calculus). If ⋅ ⊢ e ⇔ A and e z→ e′ then ⋅ ⊢e′ ⇔ A.
Theorem 5.3 (Progress of the λ e Calculus). If ⋅ ⊢ e ⇒ A then e is a value or ∃r, e z→ r.
5.4 Gradual Guarantee
Precision. Figure 18 shows the precision relation of expressions for λ e. Compared to
Figure 12, lambdas are not annotated with types and rules for pairs and projections arenew. For pairs (e1 , e2 ) and projections (πi e), precision just employs simple structural
rules. For annotated expressions, e1 ∶ A is more precise than e2 ∶ B if e1 is more precise thane2 and A is more precise than B. For two values (rule EPRE - VAL), precision holds if the
precision of raw values and types hold. To make sure the less precise values (Lp2 ∶ BM)
are well-typed, the type of raw values should be more precise than annotated types. Notethat there is an implicit assumption that the more precise values are well-typed, which
ensures that the pre-value is more precise than the type annotation. Thus no such explicit
assumption is needed in rule EPRE - VAL for p1 .
One noteworthy point is that the precision relation for expressions in λ e is significantly
simpler than the precision for λ Bg . There are a few reasons that contribute to the simpler
precision relation:
1. The form of values is similar for both dynamic and static values. Values in λ ehave a more consistent form for dynamic and statically typed values. For example,in λ Bg , static integers are represented as i, but dynamic integers are represented
as i ∶ ⋆. In λ e both static and dynamic integers require an annotation (Li ∶ IntM andLi ∶ ⋆M).
2. The eager semantics avoids accumulation of annotations. In the eager semantics,
we can avoid accumulating annotations for higher-order values. This means thathigher-order values always have exactly 3 annotations. Therefore, in combination
with the previous point, we can define precision of expressions, while avoidingalignment rules such as those in λ Bg .

40Type-Directed Operational Semantics for Gradual Typing

e1 ⊑ e2(Precision relation for expressions)
EPRE- ABS

EPRE- Cc ⊑ c

EPRE- Xx ⊑ x

e1 ⊑ e′1e1 ⊑ e′1e2 ⊑ e′2

λ x. e1 ⊑ λ x. e2(e1 , e2 ) ⊑ (e′1 , e′2 )e1 ⊑ e2e2 ⊑ e′2(e1 e2 ) ⊑ (e′1 e′2 )EPRE- PROI

EPRE- PROEPRE- ANNO

EPRE-A PP

e1 ⊑ e2A⊑B

e1 ⊑ e2e1 ∶ A ⊑ e2 ∶ B

EPRE- VALi ∈ {1, 2}A⊑B

πi e1 ⊑ πi e2p1 ⊑ p2⌉p2 ⌈⊑ B

Lp1 ∶ AM ⊑ Lp2 ∶ BM

Fig. 18. Precision relations.

3. No need for typing premises and typing contexts. In addition, there are no typing
premises. Therefore typing contexts can also be avoided. The need for inference
typing premises in the precision relation of λ Bgl follows the blame calculus, which
employs similar premises in its precision relation. However, in order to support
inference typing premises, lambda expressions need to be annotated. Otherwise raw
lambdas cannot be inferred in the general case, and the precision relation would
not be able to deal with raw lambdas. In λ e, there is no such issue because theprecision relation does not include any typing premises. Therefore, raw lambdas
can be easily supported in λ e. We conjecture that it is also possible to support raw
lambdas in λ Bgl , but this would require changing the current setup and proof for the
dynamic gradual guarantee, which is based on that of the blame calculus. We leavethis exploration for future work.
4. No need for introducing strict applications. As discussed in Section 4, the proofof the dynamic gradual guarantee for λ Bgl requires a second set of reduction rules
and the introduction of strict applications. This introduces a significant burden interms of definitions and proofs compared to λ e. The need for strict applications forthe dynamic gradual guarantee of λ Bgl is discussed in more detail in Section 6.3.
Static Criteria. The λ e calculus can also encode the dynamic counterpart of expressions(ě) by the translation function (⌈ě⌉b ) (Theorem 5.4). However, unlike in λ Bgl , where weneed to insert ⋆ → ⋆ every time for raw lambdas, in λ e, we can do a simple optimization
by exploiting bidirectional type-checking. In essence, when raw lambdas are in checking
positions, the types can be inferred from the contextual type information. The translation
function (⌈ě⌉b ) is shown as follows and the boolean flag b indicates an unknown type
annotation should be inserted or not:⌈x⌉b = x⌈c⌉true = c ∶ ⋆⌈c⌉false = c⌈λ x.ě⌉true = λ x.⌈ě⌉false ∶ ⋆⌈λ x.ě⌉false = λ x.⌈ě⌉false⌈eˇ1 eˇ2 ⌉b = ⌈eˇ1 ⌉true ⌈eˇ2 ⌉false

Journal of Functional Programming

41

For example, the dynamic expression (λ x. λ y. x y) (λ x. x) 1 can be translated to((λ x. λ y. x y) ∶ ⋆) (λ x. x) 1. Only one unknown type ⋆ is inserted, despite the presenceof 3 lambda expressions without annotations in the original expression. We should also
remark that, more generally, we can use a similar idea to improve on the syntactic sugarfor dynamic lambdas. Instead of blindly adding ⋆ → ⋆ annotations to lambdas without type
annotations, we only need to add ⋆ → ⋆ to lambdas in inference positions.
Theorem 5.5 shows that the static gradual guarantee holds for the λ e calculus. It saysthat if e of type A is more precise than e′ , then e′ has some type B, and type A is more
precise than B.
Theorem 5.4 (Dynamic Embedding). If ě is closed then ⋅ ⊢ ⌈ ě ⌉true ⇒ ⋆.
Theorem 5.5 (Static Gradual Guarantee of the λ e Calculus). If e ⊑ e′ and ⋅ ⊢ e ⇔ A then∃B, ⋅ ⊢ e′ ⇔ B and A ⊑ B.
Dynamic Gradual Guarantee. The λ e calculus has a dynamic gradual guarantee.
Theorem 5.6 shows that if e1 is more precise than e2 , e1 and e2 are well-typed, and if
e1 reduces to e′1 , then e2 reduces to e′2 . Note that e′1 is guaranteed to be more precise thane′2 . Theorem 5.6 is similar to the one formalized in the AGT approach (Garcia et al., 2016).
Theorem 5.7 is derived easily from Theorem 5.6. The auxiliary Lemma 5.7, which shows
the property of dynamic gradual guarantee for casting, is helpful to prove Theorem 5.7.
Lemma 5.7 (Dynamic Gradual Guarantee for Casting). If p1 ⊑ p2 , ⋅ ⊢ p1 ⇐ A0 , ⋅ ⊢ p2 ⇐B0 , A2 ⊑ B2 , ⌉p1 ⌈⊓A2 = A1 , ⌉p2 ⌈⊓B2 = B1 and p1 ⇓A1 p′1 then ∃p′2 , p2 ⇓B1 p′2 and Lp′1 ∶A2 M ⊑ Lp′2 ∶ B2 M.
Theorem 5.6 (Dynamic Gradual Guarantee (single-step)). If e1 ⊑ e2 , ⋅ ⊢ e1 ⇔ A, ⋅ ⊢ e2 ⇔B and e1 z→ e′1 then ∃e′2 , e2 z→ e′2 and e′1 ⊑ e′2 .
Theorem 5.7 (Dynamic Gradual Guarantee). Suppose e1 ⊑ e2 , ⋅ ⊢ e1 ⇔ A and ⋅ ⊢ e2 ⇔ B.
• If e1 z→∗ v1 then ∃v2 , e2 z→∗ v2 and v1 ⊑ v2 .
• If e1 ⇑ then e2 ⇑.
• If e2 z→∗ v2 then e1 z→∗ v1 and v1 ⊑ v2 , or e1 z→∗ blame.
• If e2 ⇑ then e1 ⇑ or e1 z→∗ blame.

6 Discussion
In this section, we wish to discuss our results and further compare the TDOS based
approach with traditional cast calculi. In particular, we wish to go through some possible
criticisms of the TDOS approach and to analyse the results obtained in this work.
To conduct this discussion, we believe that it is useful, at points, to draw an analogy withwork on the semantics of object-oriented languages. During the 80s and the 90s, there wereat least two schools of thought working on the semantics of OOP languages. One school ofthought was on using lambda calculi, such as F<∶ (Cardelli et al., 1994; Curien & Ghelli,
1992; Pierce, 1994), to give the semantics of OOP languages via an elaboration (Bruce
et al., 1999; Abadi et al., 1996). Another school of thought was to give the semantics
of OOP languages directly (Abadi & Cardelli, 1996; Igarashi et al., 2001). The work on

42Type-Directed Operational Semantics for Gradual Typing

Featherweight Java (FJ) (Igarashi et al., 2001) is a highlight of the direct approach. Bothlines of work have been highly influential and led to much innovation. We believe that
the TDOS can bring some new ideas into the landscape of gradual typing, complementing
already established ideas studied with the elaboration approach.
6.1 Comparing TDOS based Calculi with Traditional Cast Calculi
The semantics of applications. Perhaps the most notable difference between the TDOS
and traditional cast calculi, such as the blame calculus, is on the semantics of applications. In the blame calculus, applications are standard and strict. Here strict means thatapplications accept only arguments that exactly match the type of the input of the function. Explicit casts, together with strict applications, are then used in the blame calculus toencode flexible applications, where the arguments can have different (but consistent) types
and casts bridge the gap between the types.
In a TDOS, we must support flexible applications, because calculi with a TDOS modela gradual typing semantics directly. Since gradual source languages support flexible applications, the semantics of applications in a TDOS needs to be necessarily more complex
than that in a cast calculus. This difference can be seen in our work. For instance, in thesemantics of λ B in Figure 1, there are three rules dedicated to the semantics of applications(rules BSTEP - BETA, BSTEP - ABETA, and BSTEP - C). In contrast, for λ Bg (Figure 5), there
are five rules for applications (rules S TEP - BETAP, S TEP - BETA, S TEP - ABETA, S TEP - DYN,
and S TEP - C). In a TDOS, applications may raise blame due to inconsistent arguments.
Thus rule S TEP - BETAP is needed in λ Bg . In the blame calculus, applications themselves
cannot raise blame, since they are strict. So rule S TEP - BETAP or similar rules are unnecessary. Furthermore, in λ Bg , a function with type ⋆ can be directly applied to an argument,
since ⋆ ∼ ⋆ → ⋆. Thus, we also need rule S TEP - DYN in λ Bg . In the blame calculus, function applications require a function to always have a function type. So rule S TEP - DYN orsimilar is also not needed in λ B. In summary, in a TDOS, because applications are more
flexible, they can assume less about the functions and the arguments. As a result, to ensurethat applications are safe, casting must be used to check that the functions and arguments
have adequate value forms at runtime.
There are some important consequences of having flexible applications that are worth
noting and are discussed next.
Non-orthogonality of the semantics. A first point is that, from a language design pointof view, one may question the non-orthogonality of the semantics of applications in a
TDOS. In the blame calculus, applications are strict and no casting is involved. All castingthat happens is delegated into a separate cast construct. In a TDOS, applications are notorthogonal to casting, since applications also perform some casting. The non-orthogonality
is a direct consequence of the goal to have a direct gradual typing semantics. So, while a
TDOS can eliminate the need of a source language, and an elaboration to a cast calculus, aprice to pay is some additional complexity on the semantics for applications.
To build on our analogy with the semantics of OOP languages, this is similar to thesemantics of method calls versus the semantics of applications in lambda calculi such asF<∶ . Method calls in OOP languages have a relatively complex semantics due to dynamic

Journal of Functional Programming

43

dispatching, where the implementation of the method to be executed may only be determined at runtime. Thus, method calls are analogous to flexible applications and require
encodings that involve several constructs, including applications, in conventional lambda
calculi. In general, the non-orthogonality of the semantics is one of the trade-offs that weneed to make if we want to directly model a semantics similar to the source language.
Often, in source languages, constructs are made more flexible to provide programming
convenience.
Non-standard beta-reduction. A more technical point is that beta-reduction in λ Bg is
non-standard. It is well-established how to efficiently implement standard beta-reduction.
But it is unclear whether the form of beta reduction in λ Bg can be efficiently implemented.
However, we have shown that, for all calculi presented in this paper, it is possible to recoverconventional beta-reduction. For λ e, we already employ a standard beta-reduction rule. For
λ Bg and λ Bgl , we have seen that it is possible to have an alternative design for the reduction rules (Figure 9). In this alternative design, we introduce a form of strict applicationsin addition to flexible applications. Then, flexible applications will reduce into strict applications, and the beta-reduction of strict applications is standard. The cost of the alternative
design is one extra form of application.
Flexible applications are costly. Another important concern is that flexible applications
entail extra runtime costs. Casting must be used in applications to validate the types ofarguments and functions being applied. In the elaboration approach, it is possible to detect
strict applications, and avoid casts for those applications when doing cast insertion (Siek& Taha, 2006). So, while with the elaboration approach, many applications will be strict
and avoid casts, in the TDOS considered in this paper, all applications will require casts.
One downside of switching to a TDOS is that it becomes less clear where the dividing
line is between static checking and dynamic checking. Therefore, an important question iswhether it is possible to optimize TDOS to obtain similar benefits to those of cast insertion.
We will discuss this question in more detail next.
6.2 Optimizing a TDOS
We are advocating the TDOS primarily as a more direct way to provide the semantics ofgradually typed languages. In doing so, we forfeit some optimization benefits that are wellestablished for the elaboration approach. A question that then arises is whether or not we
can recover the same benefits, in terms of optimizations, that we obtain in an elaboration
approach. While it is not the goal of this paper to investigate how to optimize the TDOS,
here we briefly discuss some possible directions and wish to argue that it is possible tohave more efficient TDOS-based implementations.
Simplicity of the semantics versus guiding efficient implementations. A first point that
we wish to stress is that the main goal of the TDOS is to express the semantics and metatheory of a gradual language as directly and simply as possible. However, this goal can be inconflict with using the semantics to guide efficient implementations. We believe that thisconflict is not specific to the TDOS, but arises in many other formulations of operationalsemantics. For instance, going back to our OOP analogy, we believe that the semantics
of FJ was designed with the primary goal of simplicity in mind. The work on FJ does

44

Type-Directed Operational Semantics for Gradual Typing

not provide a direct answer for questions such as how to optimize dynamically dispatchedmethod calls. Although, of course, this is an important concern in the implementation of
OOP languages. At the same time, we believe that there is nothing preventing variants
of FJ that enable answering such questions directly. For instance, it should be possible tohave variants of FJ with multiple kinds of method calls (including dynamic and static),
and some pre-processing analysis that detects dynamic calls that can be transformed into
static calls. Of course, such an extension to FJ would require more constructs and rules,
and thus would have some extra complexity compared to the original calculus. Similarly
to FJ, our formulations of the TDOS in this paper express the semantics of all applications
with flexible applications, even if many applications can be made strict to achieve better
performance.
A point worth mentioning here is that in the elaboration approach for gradual languages,
the elaboration itself is, of course, compulsory to give the semantics of the source language.
Since the elaboration is compulsory anyway, it makes sense to exploit it and couple some
optimizations with this step. In essence, this enables us to exploit static knowledge about
the program to generate optimized code in cast calculi. A TDOS does not require an elaboration step. However, we could have an optional step type-checking a TDOS program andattempting to use static type information to generate more efficient code. In such a step, we
could do similar optimizations to those performed in the traditional elaboration of graduallanguages. For these optimizations to be possible it may be necessary to extend the TDOS
with more constructs. We briefly sketch a couple of possible optimizations next.
Optimizing Strict Applications. With the alternative set of reduction rules for λ Bgl in
Figure 9, we can avoid casting for arguments if we know that an application is strict. Thus,
assuming an optimization pass on a program, before compilation, we could try to optimize
some applications. For example, suppose that we would have the application:(λ x. x + 1 ∶ Int → ⋆) 5
With the current set of reduction rules, using flexible applications, we would need to cast
the integer argument to an integer. However, we statically know that such a cast is unnecessary. With a pre-optimization pass, we could detect this, and then transform the flexible
application above into a strict application:(λ x. x + 1 ∶ Int → ⋆) 5
Then the cast of the argument would be avoided at runtime.
Clearly the alternative syntax and set of rules in Figure 9 does not go far enough into
what we could do. For instance, in the example above, although we can avoid the cast of
the argument, we still need to cast the result of beta-reduction with the return type of thefunction. A possible idea here would be to make lambda expressions strict, by ensuring thatthe return type of the function matches exactly with the type of the body of the function.
With such a form of strict lambdas, the expression above could not type check, since x + 1(the expression in the body) should have type Int, but the return type of the function is⋆. Strict lambdas do not lose expressiveness compared to the current, more flexible, formof lambdas. This is because we can always insert a cast in the body to encode a flexible

Journal of Functional Programming

45

lambda. For instance, we could have (λ x. (x + 1 ∶ ⋆) ∶ Int → ⋆), and now the body would
have type ⋆.
We have not fully investigated the optimizations discussed above. For optimizing strict
applications, we believe that we could employ techniques similar to existing cast insertion
techniques (Siek & Taha, 2006). For the possibility of replacing flexible lambdas by strictlambdas, we have not formalized the idea yet and we may need to pay some attention to
the gradual guarantee.
Design Choices in the TDOS. Formulations of the TDOS are relatively new and underexplored. Thus, there could be different design choices with potential advantages over thecurrent design choices. One design choice that we have made is to have lambda values withboth input and output annotations. This is in contrast to the blame calculus, where lambda
abstractions only include the input type annotation: that is they are of the form λ x ∶ A. e.
One alternative TDOS design that was explored by Fan et al. (2022) for calculi with themerge operator, models lambda expressions as λ x ∶ A. e. However, function values need tobe wrapped under an annotation. That is they need to be of the form λ x ∶ A. e ∶ C (where C is
the type of the whole function). In a TDOS, output types are needed because casts require
the source type of the cast. In the blame calculus source types are written explicitly. For
example, consider the TDOS application:(λ x. x ∶ ⋆ → ⋆) 5
which casts the argument to a dynamic value. In the blame calculus, one possible cast that
we could insert to enable the program above would be:(λ x ∶ ⋆. x ∶ ⋆ → ⋆ ⇒ Int → ⋆) 5
Here we cast the function from the source type ⋆ → ⋆ to the target type Int → ⋆. In theblame calculus, both the source and target types of a cast have to be explicitly written.
In a TDOS, we require functions to have output types to ensure that the source type of acast can be easily computed, and sometimes, the target type can be left implicit. One could
wonder if we could compute an imprecise type for λ x ∶ A. e and use that form of lambdas.
That is, we could always return ⋆ for the output of function ⌉λ x ∶ A. e⌈= A → ⋆. However,
the missing output type information would bring problems in a TDOS. Suppose that wehave the following program:(λ x ∶ ⋆. 1) ∶ ⋆ ∶ Bool → Bool
The dynamic type of the lambda expression λ x ∶ ⋆. 1 would be ⋆ → ⋆, which is a groundtype. Thus, the program would reduce to an ill-typed program:(λ x ∶ ⋆. 1) ∶ Bool → BoolWith our current formulation, the lambda expression takes the form λ x. 1 ∶ ⋆ → Int. Thenthe dynamic type would be the more precise type ⋆ → Int, which is not a ground type. Thus
the problem with (λ x ∶ ⋆. 1) ∶ ⋆ ∶ Bool → Bool would not happen.

46

Type-Directed Operational Semantics for Gradual Typing
6.3 Metatheory and the Gradual Guarantee

One of our arguments for the TDOS is that it can enable a more direct approach tothe semantics of gradual languages, as well as potentially simpler metatheory. For most
proofs in the paper, we believe that the proofs are quite simple. This includes proofs ofpreservation, progress, determinism and the blame theorem. One proof that deserves morediscussion is the (dynamic) gradual guarantee, which we talk about next.
Gradual Guarantee Proofs. Using an elaboration approach to provide the semantics ofa source gradual language usually requires two separate precision relations for the source
language and the cast calculus. Furthermore, because of the elaboration, properties such as
elaboration type preservation are necessary. In contrast, the λ e calculus leads to a simple
proof of the gradual guarantee. Only one set of precision rules is required and no elaboration theorems are needed. For λ e, we believe that the gradual guarantee is simpler thanwith an elaboration approach.
For λ Bgl , however, we faced some issues for the dynamic gradual guarantee. Due to thegeneralization of the application typing rule, there are some complications in the gradualguarantee for λ Bgl . In particular, λ Bgl needs to introduce an alternative set of reduction
rules with strict applications (e1 e2 ). So the precision for the dynamic gradual guarantee
should account for strict applications, whereas no strict applications are needed for thestatic gradual guarantee.
It is worthwhile discussing why strict applications are needed. From the precision
relation, we know that the following two programs are in a precision relation:(((λ x. x ∶l1 Int → Int) ∶l2 ⋆ → ⋆) 1)l3 ⊑ ((λ x. x ∶l1 ⋆ → ⋆) 1)l3
To prove the dynamic gradual guarantee, we need to satisfy Theorem 4.7, which shows that
if the more precise expression reduces to a new expression, then the less precise expression, after multiple steps of reduction, must preserve the precision relation. If expression(((λ x. x ∶l1 Int → Int) ∶l2 ⋆ → ⋆) 1)l3 takes a reduction step:¯(((λ x. x ∶l1 Int → Int) ∶l2 ⋆ → ⋆) 1)l3 z→ (((λ x. x ∶l1 Int → Int) (1 ∶l3 ⋆))l2 ) ∶l2 ⋆¯Then (λ x. x ∶l1 ⋆ → ⋆) 1 should be in precision with (((λ x. x ∶l1 Int → Int) (1 ∶l3 ⋆))l2 ) ∶l2⋆ after multiple reduction steps. However, if ((λ x. x ∶l1 ⋆ → ⋆) 1)l3 takes a step then betareduction is performed, and the result cannot preserve precision. So, the only option is not
to reduce. However, the argument 1 is not less precise than (1 ∶l3 ⋆). The problem is that theargument type is not the same as the function input type. This is due to the generalizationof the typing of applications, where there is an implicit cast for the arguments.
To address the issue above, we introduce strict applications to perform the implicit castearlier. Then, for a strict application, the type of the argument is the same as the function
input type. For (λ x. x ∶l1 ⋆ → ⋆) 1, there is a cast from 1 to function input type ⋆. After wecast 1 to ⋆, the result is (1 ∶l1 ⋆), which is less precise than (1 ∶l2 ⋆) as expected. Therefore,
we use strict applications to label the applications which have performed the implicit cast
for arguments, and have the same type as function inputs. Another potential solution would
be to use a semantic proof method based on logical relations for proving the dynamic
gradual guarantee (New et al., 2019). With this approach, we believe that the intermediate reduction system with strict applications would not be needed. The key observation

Journal of Functional Programming

47

is that the final reduction result should be in a precision relation (even if intermediate
results may not be in a precision relation). However, a semantic approach introduces its
own complexity, so we have not explored this possibility.
In short, for the proof of the dynamic gradual guarantee in λ Bgl , while we can avoid
some proofs and definitions required by elaboration, we faced other complications. Thus
we cannot claim that the proof of the dynamic gradual guarantee for λ Bgl is simpler thanthe proof for the blame calculus.

7 Related Work
This section discusses related work. We focus on gradual typing criteria, cast calculi,
gradually typed calculi, the AGT approach and typed operational semantics.
Gradual Typing and Criteria. There is a growing number of research work focusing
on combining static and dynamic typing (Rastogi et al., 2012; Strickland et al., 2012;
Matthews & Findler, 2009; Abadi et al., 1991; Meijer & Drayton, 2004; Boyland, 2014;
Wolff et al., 2011; Swamy et al., 2014; Hansen, 2007; Thatte, 1989). Many mainstream
programming languages have some form of integration between static and dynamic typing.
These include TypeScript (Bierman et al., 2014), Dart (Bracha, 2015), Hack (Verlaguet,2013), Cecil (Chambers, 1992), Bigloo (Serrano & Weis, 1995), Visual Basic.NET (Meijer& Drayton, 2004), ProfessorJ (Gray et al., 2005), Lisp (Moon, 1989), Dylan (Shalit, 1996)
and Typed Racket (Tobin-Hochstadt & Felleisen, 2008).
A gradually typed lambda calculus (GTLC) should support both fully statically typed
and fully dynamically typed programs, as well as partially statically typed or dynamically
typed ones. Siek & Taha (2006) introduced gradual typing with the notion of the unknown
type ⋆ and type consistency. Because run-time checking is needed by a gradually typed
language, function type annotations are accumulated at run-time in most of the gradually
typed languages. Therefore, the number of accumulated type annotations can be unbound.
Herman et al. (2007) implemented gradual typing based on coercions and combined adjacent coercions. Thus, space consumption has been limited and the type system was proved
to be type-safe. Addressing the space consumption issues of gradual typing has been an
ongoing research effort, with many works on the area (Siek et al., 2009; Siek & Wadler,
2009; Garcia, 2013; Herman et al., 2010).
Much work in the research literature of gradual typing focuses on the pursuit of soundgradual typing. A language with sound gradual typing should come with a guaranteeof type soundness. This often requires some dynamic checks that arise from static type
information. Furthermore, gradually typed languages should provide a smooth integration
between dynamic and static typing. For instance, one of the criteria for gradual typing isthat a program that has static types should behave equivalently to a standard statically typed
program (Siek & Taha, 2006). Siek et al. (2015b) proposed the gradual guarantee to clarify
the kinds of guarantees expected in gradually typed languages. The principle of the gradualguarantee is that static and dynamic behavior changes by changing type annotations. For
the static (gradual) guarantee, the type of a more precise term should be more precise than
the type of a less precise term. For the dynamic (gradual) guarantee, any program that runs
without errors should continue to do so with less precise types.

48

Type-Directed Operational Semantics for Gradual Typing

Cast Calculi. The semantics of a gradually typed calculus is normally given indirectly
via a translation (or elaboration) into a cast calculus. The process of the translation to
cast calculi involves inserting casts whenever type consistency holds between different
types. Cast calculi are independent from the GTLC, having their own type systems andoperational semantics. In λ Bg and λ e, by using TDOS, the semantics of a GTLC is given
directly without translating to any other calculus.
There are several varieties of cast calculi. Findler & Felleisen (2002) introduced
assertion-based contracts for higher-order functions. Based on the coercions and checks
for higher-order values, which are implemented by an ad-hoc mixture of wrappers, reflection, and dynamic predicates, Gray et al. (2005) provided the following observation. First,
the wrapper and reflection operations fit the profile of mirrors. Second, the checks correspond to contracts. Finally, the timing and shape of mirror operations coincide with thetiming and shape of contract operations. Consequently, they presented a new model ofinteroperability that builds on the ideas of mirrors and contracts. Henglein’s dynamically
typed λ -calculus (Henglein, 1994) is an extension of the statically typed λ -calculus witha dynamic type and explicit dynamic type coercions. To port portions of programs from
scripting languages to sound typed languages, Tobin-Hochstadt & Felleisen (2006) presented a framework for expressing this interlanguage migration. They proved that, for a
program which consists of modules in the untyped lambda calculus, rewriting one of themin a simply typed lambda calculus can produce an equivalent program and be type safe.
Wadler & Findler (2009) introduced the blame calculus. The blame comes from Findler
and Felleisen’s contracts and tracks the locations where cast errors happen using blamelabels. Siek et al. (2009) explored the design space of higher-order casts. For first-order
casts (casts on base types), the semantics is straightforward. But there are issues for higherorder casts (functions): a higher-order cast is not checked immediately. For higher-order
casts, checking is deferred until the function is applied to an argument. After application,
the cast is checked against the argument and return value. A cast is used as a wrapper andsplit when the wrapped function is applied to an argument. Wrappers for higher-order casts
can lead to unbounded space consumption (Herman et al., 2010).
There are some different designs for the dynamic semantics for cast calculi in the literature. Wadler & Findler (2009) use a lazy error detection strategy, which coerces thearguments of a function to the target type, and checking is only done when the argument isapplied. Siek & Taha (2006) use a different strategy where checking higher-order casts is
performed immediately when the source type is the unknown type (⋆). Otherwise, the later
strategy is the same as lazy error detection.
Siek & Wadler (2009) introduced threesomes, where a cast consists of three types insteadof two types (twosomes) of the blame calculus. The threesome calculus is proved to beequivalent to a coercion-based calculus (Herman et al., 2007) without blame labels butwith space efficiency. The three types in a threesome contain the source, intermediate andtarget types. The intermediate type is computed by the greatest lower bound of all theintermediate types. In λ e the three annotations in lambda values play a similar role to thethree annotations in threesomes. Castagna & Lanvin (2017) proposed a calculus that discards annotations for higher-order functions, following an eager semantics. The dynamic
semantics for higher-order values above can be summarized as two categories. One is theJournal of Functional Programming

49

lazy semantics, and the other is the eager semantics which attempts to merge intermediate
annotations for higher-order casts. In our work, we study calculi with both variants.
Finally, various cast calculi have been extended with various of features of practicalinterest. For instance, Ahmed et al. (2011) extended the blame calculus to incorporate
polymorphism, based on the dynamic sealing proposed by Matthews & Ahmed (2008) andNeis et al. (2009).
Cast calculi require explicit casts and cannot be used directly as a gradually typed language. They can be used as the target of source gradual languages via an elaboration that
inserts casts where needed. In contrast, the calculi presented in this work support both
explicit and implicit casts. Explicit casts are supported via type annotations, which can
act as casts at runtime. Implicit casts arise from the use of bidirectional type-checking,where the checking mode denotes points in the program where casts are needed. Because
implicit casts are supported in all our calculi (λ Bg , λ Bgl and λ e), these calculi can all be
used directly as gradually typed languages and no elaboration step is necessary.
In the conference version of this work, we introduced the λ Br calculus (Ye et al., 2021),
which uses a forgetful semantics (Greenberg, 2015) called the blame recovery semantics.
The blame recovery semantics ignores intermediate type annotations in a chain of type
annotations for higher-order functions. The idea is to only raise blame if the initial source
type of the value and final target types are not consistent. Otherwise, even if intermediate
annotations trigger type conversions, which would not be consistent, the final result canstill be a value provided that the initial source and final target types are themselves consistent. This alternative approach has a bounded number of annotations, which avoids theaccumulation of type annotations (up-to 2 for higher-order values). In the present work,
we opted to present an eager semantics, inspired by the AGT approach, instead. However,
the eager semantics in λ e and traditional AGT (Garcia et al., 2016), is only applied to values. In other work (Herman et al., 2010; Siek & Wadler, 2009; Bañados Schwerter et al.,2021), the eager semantics is applied to all expressions and leads to a space-efficiency
GTLC. Furthermore, both AGT and our eager semantics is more eager than the original
approach by Herman et al. (2010), since, if two types are inconsistent, an error is raised
directly. However in space efficient calculi, error is recorded and raised when arguments
are applied. We leave a space-efficient formulation of the eager semantics using TDOS as
future work.
Abstracting Gradual Typing (AGT). Garcia et al. (2016) introduce the abstracting gradual typing (AGT) approach, following an idea by Bañados Schwerter et al. (2014). An
externally justified cast calculus is not required in AGT. Instead, runtime checks are
deduced by the evidence for the consistency judgement. For the static semantics, AGT
uses techniques from abstract interpretation to lift terms of the static system to gradualterms. A concretization function is used to lift gradual types to static type sets. After that,a gradual type system can be derived according to the static type system. The gradual typesystem retains the type safety of the static type system, and enjoys the criteria of Siek et al.
(2015b). The dynamic semantics is given by reasoning about the type derivations obtained
from the type safety proof of the static language counterpart. Gradual typing derivations
are represented as intrinsically typed terms (Church, 1940), which correspond to typing
derivations directly.

50

Type-Directed Operational Semantics for Gradual Typing

One aspect that the TDOS has in common with the AGT approach is that by using
the TDOS for the dynamic semantics and a bidirectional type system, we can design a
gradually typed language with a direct semantics. Nevertheless, the two approaches havedifferent and perhaps complementary goals. The goals of TDOS are more modest thanthose of AGT, which aims at deriving various definitions for gradually typed languages
in a systematic manner. In contrast, TDOS and our work have no such goals. Our main
aim is to adapt the standard and well-known techniques from small-step semantics, into
the design of gradually typed languages. We expect that the familiarity and simplicity of
the TDOS approach would be a strength, whereas the AGT approach requires some more
infrastructure, but the payoff is that many definitions can then be derived. For future work,
it would be interesting to see whether it is possible to combine ideas from both approaches.
It would be interesting to reuse much of the AGT infrastructure, but with an alternativemodel for the dynamic semantics based on a TDOS instead. One current limitation of the
AGT approach is that it does not offer an account of blame tracking and blame labels. As
we have seen in Section 4, the TDOS can model languages with blame tracking and blamelabels and be used to prove important theorems such as blame safety.
Typed Operational Semantics. In this paper, we use the type-directed operational semantics (TDOS) approach (Huang & Oliveira, 2020). TDOS was originally used to describe thesemantics of languages with intersection types and a merge operator. Like gradual typing,such features require a type-dependent semantics. In a TDOS, type annotations become
operationally relevant and can affect the result of a program. Casting is used to provide
an operational interpretation to type conversions in the language, similarly to coercions incoercion-based calculi (Henglein, 1994). Our work shows that a TDOS enables a directsemantics for gradual typing. We explored two possible semantics for gradual typing: one
following a semantics similar to the blame calculus, and another with an eager semantics.
There are other variants of operational semantics that make use of type annotations.
Types are used in Goguen’s typed operational semantics (Goguen, 1994), similarly to
TDOS. Typed operational semantics has been applied to various calculi, including simply typed lambda calculi (Goguen, 1995) and calculi with dependent types (Feng & Luo,2011) and higher-order subtyping (Compagnoni & Goguen, 2003). An extensive overview
of related work on type-dependent semantics is given by Huang & Oliveira (2020).

8 Conclusion
In this work, we proposed an alternative approach to give a direct semantics to gradually typed languages without an intermediate cast calculus. Our approach is based on a
TDOS (Huang & Oliveira, 2020). TDOS is a variant of small-step semantics where type
annotations are operationally relevant and a special big-step casting relation gives an interpretation to such type annotations at runtime. We believe that TDOS can be a valuable
technique for language designers of gradually typed languages, giving them a simple anddirect way to express the semantics of their languages.
We presented two gradually typed lambda calculi: λ Bg and λ e. The λ Bg semantics
follows the semantics of λ B. The λ e calculus explores the use of an eager semantics forgradually typed languages using a TDOS. In addition, the λ Bgl calculus shows that blame

Journal of Functional Programming

51labels can be modeled using a TDOS, and results such as the blame theorem and the gradualguarantee can also be proved.
There is much to be done for future work. Although we argued that some benefits of
the TDOS include easier and more direct proofs, we have not empirically validated thoseclaims. To do so we would need to formalize the GTLC and a target cast calculus (suchas the blame calculus or a cast calculus with an eager semantics) in Coq together with all
the relevant proofs (such as the blame theorem the gradual guarantee and others). Then we
could empirically compare the proofs, for instance in terms of size or number of lemmas
that are required and/or other metrics. In our work, we have only informally mentionedthat some lemmas and definitions would not be needed in a TDOS, but perhaps it could
be the case that a TDOS would also require some extra lemmas or extra complexity in the
proofs that is not necessary in the conventional approach using an elaboration semantics.
One issue that we have identified in the proofs with the TDOS is the dynamic gradualguarantee proof for λ Bgl , which we discussed in Section 6. An empirical evaluation would
help assessing such benefits (or not) more precisely, and it is one direction for future work.
Obviously, to prove that TDOS is a worthy alternative to existing cast calculi or otherapproaches for the semantics of gradually typed languages, many more features should
be developed with the TDOS. Cast calculi have been shown to support a wide range offeatures such as polymorphism (Ahmed et al., 2011), subtyping (Siek & Taha, 2007) andvarious other features (Siek & Vachharajani, 2008; Takikawa et al., 2012). We hope to
explore these in the future.
Acknowledgements: We are grateful to anonymous reviewers and our colleagues at theHKU PL group. This work has been sponsored by Hong Kong Research Grants Council
projects number 17209520 and 17209821.
Conflicts of Interest: None.

References
Abadi, M., & Cardelli, L. (1996). A theory of objects. Springer-Verlag.
Abadi, Martı́n, Cardelli, Luca, Pierce, Benjamin, & Plotkin, Gordon. (1991). Dynamic typing in astatically typed language. ACM Transactions on Programming Languages and Systems (TOPLAS),
13(2), 237–268.
Abadi, Martı́n, Cardelli, Luca, & Viswanathan, Ramesh. (1996). An interpretation of objects andobject types. Pages 396–409 of: Proceedings of the 23rd acm sigplan-sigact symposium on
principles of programming languages.
Ahmed, Amal, Findler, Robert Bruce, Siek, Jeremy G, & Wadler, Philip. (2011). Blame for all. Pages
201–214 of: Proceedings of the 38th annual ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages.
Bañados Schwerter, Felipe, Clark, Alison M., Jafery, Khurram A., & Garcia, Ronald. (2021).
Abstracting gradual typing moving forward: precise and space-efficient. Proc. acm program. lang.,
5(POPL).
Bañados Schwerter, Felipe, Garcia, Ronald, & Tanter, Éric. (2014). A theory of gradual effect systems. Pages 283–295 of: Proceedings of the 19th ACM SIGPLAN International Conference on
Functional programming.
Bettini, Lorenzo, Bono, Viviana, Dezani-Ciancaglini, Mariangiola, Giannini, Paola, & Venneri, Betti.
(2018). Java & Lambda: a Featherweight Story. Logical Methods in Computer Science, 14(3).

52Type-Directed Operational Semantics for Gradual Typing

Bierman, Gavin, Abadi, Martı́n, & Torgersen, Mads. (2014). Understanding TypeScript. Pages
257–281 of: European Conference on Object-Oriented Programming. Springer.
Bottu, Gert-Jan, Xie, Ningning, Marntirosian, Koar, & Schrijvers, Tom. (2019). Coherence of TypeClass Resolution. Proc. acm program. lang., 3(ICFP).
Boyland, John Tang. (2014). The problem of structural type tests in a gradual-typed language.
Foundations of Object-Oriented Langauges.
Bracha, Gilad. (2015). The Dart Programming Language.
Bruce, Kim B., Cardelli, Luca, & Pierce, Benjamin C. (1999). Comparing object encodings. vol.
155.
Cardelli, Luca, Martini, Simone, Mitchell, John C., & Scedrov, Andre. (1994). An extension ofsystem f with subtyping. Information and computation, 109(1-2), 4–56.
Castagna, Giuseppe, & Lanvin, Victor. (2017). Gradual typing with union and intersection types.
Proceedings of the ACM on Programming Languages, 1(ICFP), 1–28.
Chambers, Craig. (1992). Object-Oriented Multi-Methods in Cecil. European conference on objectoriented programming.
Chaudhuri, Avik, Vekris, Panagiotis, Goldman, Sam, Roch, Marshall, & Levi, Gabriel. (2017). Fastand Precise Type Checking for JavaScript. Proc. acm program. lang., 1(OOPSLA).
Church, Alonzo. (1940). A formulation of the simple theory of types. The Journal of Symbolic Logic,
5(2), 56–68.
Compagnoni, Adriana, & Goguen, Healfdene. (2003). Typed operational semantics for higher-ordersubtyping. Information and Computation, 184(2), 242–297.
Curien, Pierre-Louis, & Ghelli, Giorgio. (1992). Coherence of subsumption, minimum typing andtype-checking in f≤ . Mathematical structures in computer science, 2(1), 55–91.
Fan, Andong, Huang, Xuejing, Xu, Han, Sun, Yaozhu, & Oliveira, Bruno C. d. S. (2022). Direct
Foundations for Compositional Programming. Pages 18:1–18:28 of: Ali, Karim, & Vitek,
Jan (eds), 36th european conference on object-oriented programming (ecoop 2022). Leibniz
International Proceedings in Informatics (LIPIcs), vol. 222. Dagstuhl, Germany: Schloss Dagstuhl– Leibniz-Zentrum für Informatik.
Felleisen, Matthias, & Hieb, Robert. (1992). The Revised Report on the Syntactic Theories ofSequential Control and State. Theor. comput. sci., 103(2), 235–271.
Feng, Yangyue, & Luo, Zhaohui. (2011). Typed Operational Semantics for Dependent Record Types.
Electronic Proceedings in Theoretical Computer Science, 53(Mar), 30–46.
Findler, Robert Bruce, & Felleisen, Matthias. (2002). Contracts for higher-order functions. Pages
48–59 of: Proceedings of the seventh ACM SIGPLAN International Conference on Functional
programming.
Garcia, Ronald. (2013). Calculating threesomes, with blame. Pages 417–428 of: Proceedings of the
18th ACM SIGPLAN International Conference on Functional programming.
Garcia, Ronald, & Cimini, Matteo. (2015). Principal Type Schemes for Gradual Programs. Pages
303–315 of: Rajamani, Sriram K., & Walker, David (eds), Proceedings of the 42nd annual ACM
SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2015, mumbai,
india, january 15-17.
Garcia, Ronald, Clark, Alison M., & Tanter, Éric. (2016). Abstracting Gradual Typing. Pages
429–442 of: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages. POPL ’16. New York, NY, USA: Association for Computing
Machinery.
Goguen, Healfdene. (1994). A typed operational semantics for type theory. Ph.D. thesis, Universityof Edinburgh.
Goguen, Healfdene. (1995). Typed operational semantics. Pages 186–200 of: International
Conference on Typed Lambda Calculi and Applications. Springer.
Gray, Kathryn E., Findler, Robert Bruce, & Flatt, Matthew. (2005). Fine-Grained Interoperability
through Mirrors and Contracts. Page 231–245 of: Proceedings of the 20th Annual ACM SIGPLAN
Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA’05. New York, NY, USA: Association for Computing Machinery.

Journal of Functional Programming

53

Greenberg, Michael. (2015). Space-efficient manifest contracts. Pages 181–194 of: Proceedings ofthe 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
Hansen, Lars T. (2007). Evolutionary programming and gradual typing in ECMAScript 4. Tech.
rept.
Henglein, Fritz. (1994). Dynamic typing: Syntax and proof theory. Science of Computer
Programming, 22(3), 197–230.
Herman, David, Tomb, Aaron, & Flanagan, Cormac. (2007). Space-efficient gradual typing. In
Trends in Functional Programming (TFP).
Herman, David, Tomb, Aaron, & Flanagan, Cormac. (2010). Space-efficient gradual typing. HigherOrder and Symbolic Computation, 23(2), 167.
Huang, Xuejing, & Oliveira, Bruno C. d. S. (2020). A Type-Directed Operational Semantics
For a Calculus with a Merge Operator. Pages 26:1–26:32 of: Hirschfeld, Robert, & Pape,
Tobias (eds), 34th European Conference on Object-Oriented Programming (ECOOP 2020).
Leibniz International Proceedings in Informatics (LIPIcs), vol. 166. Dagstuhl, Germany: Schloss
Dagstuhl–Leibniz-Zentrum für Informatik.
Huang, Xuejing, Zhao, Jinxu, & Oliveira, Bruno C. d. S. (2021). Taming the Merge Operator. Journalof Functional Programming, 31, e28.
Igarashi, Atsushi, Pierce, Benjamin C., & Wadler, Philip. (2001). Featherweight java: a minimal corecalculus for java and gj. Acm transactions on programming languages and systems (toplas), 23(3),396–450.
Labrada, Elizabeth, Toro, Matı́as, Tanter, Éric, & Devriese, Dominique. (2022). Plausible sealing for
gradual parametricity. Proc. acm program. lang., 6(OOPSLA1).
Matthews, Jacob, & Ahmed, Amal. (2008). Parametric polymorphism through run-time sealingor, theorems for low, low prices! Pages 16–31 of: Drossopoulou, Sophia (ed), Programming
languages and systems.
Matthews, Jacob, & Findler, Robert Bruce. (2009). Operational Semantics for Multi-Language
Programs. ACM Trans. Program. Lang. Syst., 31(3).
Meijer, Erik, & Drayton, Peter. (2004). Static typing where possible, dynamic typing when needed:
The end of the cold war between programming languages. Citeseer.
Moon, David A. (1989). The Common LISP Object-Oriented Programming Language Standard.
New York, NY, USA: Association for Computing Machinery. Page 49–78.
Neis, Georg, Dreyer, Derek, & Rossberg, Andreas. (2009). Non-Parametric Parametricity. Page
135–148 of: Proceedings of the 14th ACM SIGPLAN International Conference on Functional
Programming. ICFP ’09. New York, NY, USA: Association for Computing Machinery.
New, Max S., Licata, Daniel R., & Ahmed, Amal. (2019). Gradual Type Theory. Proc. ACM
Program. Lang., 3(POPL).
Pierce, Benjamin C. (1994). Bounded quantification is undecidable. Information and computation,
112(1), 131–165.
Pierce, Benjamin C, & Turner, David N. (2000). Local type inference. ACM Transactions on
Programming Languages and Systems (TOPLAS), 22(1), 1–44.
Rastogi, Aseem, Chaudhuri, Avik, & Hosmer, Basil. (2012). The Ins and Outs of Gradual Type
Inference. Page 481–494 of: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages. POPL ’12. New York, NY, USA: Association for
Computing Machinery.
Reynolds, John C. (1991). The coherence of languages with intersection types. Pages 675–700 of:
Lecture notes in computer science (lncs). Springer Berlin Heidelberg.
Reynolds, John C. (1993). An introduction to logical relations and parametric polymorphism(abstract). Page 155–156 of: Proceedings of the 20th acm sigplan-sigact symposium on principles of programming languages. POPL ’93. New York, NY, USA: Association for Computing
Machinery.
Serrano, Manuel, & Weis, Pierre. (1995). Bigloo: a portable and optimizing compiler for strict
functional languages. Pages 366–381 of: International Static Analysis Symposium. Springer.

54

Type-Directed Operational Semantics for Gradual Typing

Shalit, Andrew. (1996). The Dylan reference manual: the definitive guide to the new object-oriented
dynamic language. Addison Wesley Longman Publishing Co., Inc.
Siek, Jeremy, & Taha, Walid. (2007). Gradual typing for objects. Pages 2–27 of: European
Conference on Object-Oriented Programming. Springer.
Siek, Jeremy, Garcia, Ronald, & Taha, Walid. (2009). Exploring the design space of higher-order
casts. Pages 17–31 of: European Symposium on Programming. Springer.
Siek, Jeremy, Thiemann, Peter, & Wadler, Philip. (2015a). Blame and Coercion: Together Again
for the First Time. Page 425–435 of: Proceedings of the 36th ACM SIGPLAN Conference
on Programming Language Design and Implementation. PLDI ’15. New York, NY, USA:
Association for Computing Machinery.
Siek, Jeremy G., & Taha, Walid. (2006). Gradual typing for functional languages. Pages 81–92 of:Scheme and Functional Programming Workshop, vol. 6.
Siek, Jeremy G, & Vachharajani, Manish. (2008). Gradual typing with unification-based inference.
Pages 1–12 of: Proceedings of the 2008 Symposium on Dynamic languages.
Siek, Jeremy G., & Wadler, Philip. (2009). Threesomes, with and without blame. Page 34–46 of:Proceedings for the 1st Workshop on Script to Program Evolution. STOP ’09. New York, NY,
USA: Association for Computing Machinery.
Siek, Jeremy G, Vitousek, Michael M, Cimini, Matteo, & Boyland, John Tang. (2015b). Refined
criteria for gradual typing. 1st Summit on Advances in Programming Languages (SNAPL 2015).
Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
Strickland, T. Stephen, Tobin-Hochstadt, Sam, Findler, Robert Bruce, & Flatt, Matthew. (2012).
Chaperones and Impersonators: Run-Time Support for Reasonable Interposition. Page 943–962
of: Proceedings of the ACM International Conference on Object Oriented Programming Systems
Languages and Applications. OOPSLA ’12. New York, NY, USA: Association for Computing
Machinery.
Swamy, Nikhil, Fournet, Cedric, Rastogi, Aseem, Bhargavan, Karthikeyan, Chen, Juan, Strub,
Pierre-Yves, & Bierman, Gavin. (2014). Gradual Typing Embedded Securely in JavaScript.
Page 425–437 of: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages. POPL ’14. New York, NY, USA: Association for Computing
Machinery.
Takikawa, Asumu, Strickland, T Stephen, Dimoulas, Christos, Tobin-Hochstadt, Sam, & Felleisen,
Matthias. (2012). Gradual typing for first-class classes. Pages 793–810 of: Proceedings of
the ACM International Conference on Object Oriented Programming Systems Languages andApplications.
Thatte, Satish. (1989). Quasi-static typing. Pages 367–381 of: Proceedings of the 17th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
Tobin-Hochstadt, Sam, & Felleisen, Matthias. (2006). Interlanguage migration: from scripts to programs. Pages 964–974 of: Companion to the 21st ACM SIGPLAN Symposium on Object-oriented
Programming Systems, Languages, and Applications.
Tobin-Hochstadt, Sam, & Felleisen, Matthias. (2008). The Design and Implementation of Typed
Scheme. Page 395–406 of: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages. POPL ’08. New York, NY, USA: Association for
Computing Machinery.
Toro, Matı́as, Labrada, Elizabeth, & Tanter, Éric. (2019). Gradual parametricity, revisited.
Proceedings of the acm on programming languages, 3(POPL), 17:1–17:30.
Verlaguet, Julien. (2013). Facebook: Analyzing PHP statically. Commercial Users of Functional
Programming (CUFP), 13.
Wadler, Philip, & Findler, Robert Bruce. (2009). Well-typed programs can’t be blamed. Pages 1–16
of: European Symposium on Programming. Springer.
Wolff, Roger, Garcia, Ronald, Tanter, Éric, & Aldrich, Jonathan. (2011). Gradual typestate. Pages
459–483 of: European Conference on Object-Oriented Programming. Springer.
Wright, Andrew K, & Felleisen, Matthias. (1994). A syntactic approach to type soundness.
Information and Computation, 115(1), 38–94.

Journal of Functional Programming

55

Xie, Ningning, Bi, Xuan, Oliveira, Bruno C. D. S., & Schrijvers, Tom. (2019). Consistent Subtyping
for All. Acm trans. program. lang. syst., 42(1).
Ye, Wenjia, Oliveira, Bruno C. d. S., & Huang, Xuejing. (2021). Type-Directed Operational
Semantics for Gradual Typing. 35th European Conference on Object-Oriented Programming(ECOOP 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik.
Ye, Wenjia, Toro, Matı́as, & Olmedo, Federico. (2023). A gradual probabilistic lambda calculus.
Proc. acm program. lang., 7(OOPSLA1).