Contextual Typing
XU XUE, The University of Hong Kong, China
BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, China
Bidirectional typing is a simple, lightweight approach to type inference that propagates known type information
during typing, and can scale up to many different type systems and features. It typically only requires areasonable amount of annotations and eliminates the need for many obvious annotations. Nonetheless thepower of inference is still limited, and complications arise in the presence of more complex features.
In this paper we present a generalization of bidirectional typing called contextual typing. In contextual
typing not only known type information is propagated during typing, but also other known information about
the surrounding context of a term. This information can be of various forms, such as other terms or recordlabels. Due to this richer notion of contextual information, less annotations are needed, while the approachremains lightweight and scalable. For type systems with subtyping, contextual typing subsumption is also
more expressive than subsumption with bidirectional typing, since partially known contextual information
can be exploited. To aid specifying type systems with contextual typing, we introduce Quantitative Type
Assignment Systems (QTASs). A QTAS quantifies the amount of type information that a term needs in orderto type check using counters. Thus, a counter in a QTAS generalizes modes in traditional bidirectional typing,which can only model an all (checking mode) or nothing (inference mode) approach. QTASs enable precise
guidelines for annotatability of contextual type systems formalized as a theorem. We illustrate contextual
typing first on a simply typed lambda calculus, and then on a richer calculus with subtyping, intersection
types, records and overloading. All the metatheory is formalized in the Agda theorem prover.
CCS Concepts: • Theory of computation → Type theory.
Additional Key Words and Phrases: Bidirectional Typing, Type Inference
ACM Reference Format:
Xu Xue and Bruno C. d. S. Oliveira. 2024. Contextual Typing. Proc. ACM Program. Lang. 8, ICFP, Article 266(August 2024), 29 pages. https://doi.org/10.1145/3674655

1

Introduction

Bidirectional typing is a technique for the design and implementation of type systems. It has been
popularized by Pierce and Turner [2000], and surveyed by Dunfield and Krishnaswami [2021].
The key idea is to have two modes for typing: inference and checking, which describe local type
information propagation. The type inferred from a term can be further used to check other terms.
In other words, the type information can be propagated from one term to its neighboring terms.
Bidirectional typing has proved useful for the design of complex type systems with a variety offeatures, including subtyping [Davies and Pfenning 2000; Dunfield and Pfenning 2004; Pierce andTurner 2000], polymorphism [Dunfield and Krishnaswami 2013; Zhao et al. 2019] and dependent
types [Asperti et al. 2012; Coquand 1996; Löh et al. 2010; Norell 2007; Xi and Pfenning 1999].
Bidirectional typing eliminates the need for many obvious annotations, but the power of inference is still limited. Standard bidirectional typing is an all-or-nothing approach: either all type
Authors’ Contact Information: Xu Xue, The University of Hong Kong, Hong Kong, China, xxue@cs.hku.hk; Bruno C. d. S.
Oliveira, The University of Hong Kong, Hong Kong, China, bruno@cs.hku.hk.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2024 Copyright held by the owner/author(s).
ACM 2475-1421/2024/8-ART266
https://doi.org/10.1145/3674655

Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:2

Xu Xue and Bruno C. d. S. Oliveira

information is known and we can type check a term; or no type information is known and we caninfer the type of a term. However, several researchers [Bierman et al. 2014; Norell 2007; Odersky
et al. 2001; Polikarpova et al. 2016; Pottier and Régis-Gianas 2006; Xie and Oliveira 2018] observedthat partially known type information is helpful to improve inference. In some of those works, anotion that naturally arises is some form of contextual type information that aids type inference.
In this paper we present a generalization of bidirectional typing called contextual typing. Contextual typing builds on the idea that partially known type information is helpful for inference,and further extends it. In contextual typing not only known type information is propagated during
typing, but also other (partially) known information about the surrounding context of a term. This
information can be of various forms, such as other terms or record labels. For instance, for terms
representing functions, it could be the terms (arguments) that the function is being applied to.
Conversely, for records, it could be the information about labels that are being projected. Due tothis richer notion of contextual information, fewer annotations are needed, while the approachremains lightweight and scalable. Contextual typing retains the lightweightness of bidirectional
typing, by simply propagating some information from some terms into some other neighboringterms. No advanced mechanisms, such as unification variables, are needed for contextual typing.
For type systems with subtyping, contextual typing subsumption is also more expressive thanbidirectional typing subsumption. Unlike the standard bidirectional subsumption rule, which
requires full type information for the supertype of a term, contextual typing subsumption canbe used when only partial contextual information is known. Contextual subsumption is helpful
to eliminate some complications that arise when applying bidirectional typing to type systems
with subtyping. In particular, in various type systems with subtyping – including features likeintersection types and/or union types [Davies and Pfenning 2000; Huang et al. 2021; Rioux et al.
2023], records [Xue et al. 2022] or polymorphism [Dunfield and Krishnaswami 2013; Zhao et al.
2019] – specialized auxiliary relations are needed in other parts of the typing relation to compensate
for the weak form of bidirectional subsumption. Because contextual typing has a more powerfulform of subsumption, it can avoid many such auxiliary relations. Thus we can have a typing relation
where all uses of subtyping are delegated to the subsumption rule, and dealt with in a single place.
To specify type systems with contextual typing we introduce Quantitative Type Assignment
Systems (QTASs). QTASs serve as an intermediate step in between traditional Type Assignment
Systems (TASs) and algorithmic formulations. Unlike type assignment systems, QTASs precisely
specify where type annotations are needed. Moreover, they quantify (and in some cases qualify) theamount of type information that a term needs in order to type check via counters. Thus, the notionof counters in a QTAS generalizes modes in traditional bidirectional typing from an all (checkingmode) or nothing (inference mode) approach, to a notion that quantifies the amount of needed type
information. With a QTAS it is possible to have precise guidelines for the annotatability of typesystems with contextual typing formalized as a theorem.
We illustrate the key ideas of contextual typing and propagation of partial contextual information
contextual typing first on a simplified setting based on the simply typed lambda calculus. In thiscalculus, contextual information consists of known type information, and known arguments tofunctions. Then we present a richer calculus with subtyping, intersection types, records and asimple form of overloading. This calculus illustrates a more powerful form of subsumption provided
by contextual typing, and shows that we can have other forms of contextual information. In
particular, we use labels of records as contextual information to aid with the type inference ofrecord projections. For both calculi we prove several results, including soundness and completenessbetween a QTAS and its algorithmic formulation, decidability of typing and/or subtyping, andannotatability theorems. All the metatheory is formalized in the Agda theorem prover.
In summary, the contributions of this paper are:Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual Typing

266:3

Γ ⊢ 𝑒 ⇔ 𝐴 (Under environment Γ, 𝑒 can infer (⇒) the type 𝐴 or check (⇐) against the type 𝐴.)Γ ⊢ 𝑖 ⇐ Int

Lit(𝑥 : 𝐴) ∈ ΓΓ⊢𝑥 ⇒𝐴Γ, 𝑥 : 𝐴 ⊢ 𝑒 ⇐ 𝐵Γ ⊢ (𝜆𝑥 . 𝑒) ⇐ 𝐴 → 𝐵

Var

Lam

Γ ⊢𝑒 ⇒𝐴Γ ⊢𝑒 ⇐𝐴

𝐴=𝐵

Γ ⊢𝑒 ⇐𝐵Γ ⊢ 𝑒1 ⇒ 𝐴 → 𝐵

SubΓ ⊢ (𝑒 : 𝐴) ⇒ 𝐴Γ ⊢ 𝑒2 ⇐ 𝐴Γ ⊢ 𝑒1 𝑒2 ⇒ 𝐵

Anno

App

Fig. 1. Bidirectional typing of STLC. Note that ⇔ is a metavariable defined as: ⇔ ::= ⇐ | ⇒.

• Contextual typing: A generalization of bidirectional typing, which retains its lightweightness, and enables programs to type check with fewer annotations.
• Quantitative type assignment systems. A variant of type assignment systems, which specifies the amount of information needed to type check terms, and enables precise annotatability
guidelines to be formalized as theorems.
• A teleportation-based approach for algorithmic typing. To implement a QTAS, weemploy a typing relation that, in addition to a type environment, is also parametrized by asurrounding context. The surrounding context tracks known contextual type information,and is used to aid with the propagation (or teleportation) of information across the AST.
• The metatheory for contextual typing. All the calculi and proofs in this paper are formalized in Agda and they are available at https://github.com/juniorxxue/contextual-typing.
• A contextual intersection type system with subtyping, records and overloading,illustrating how contextual typing scales up to subtyping and some common features.
2

Bidirectional Typing: Some Variants and Limitations

In this section we first introduce a standard formulation of bidirectional typing [Dunfield andKrishnaswami 2021; Pierce and Turner 2000], and an alternative bidirectional approach called letarguments go first [Xie and Oliveira 2018]. We then discuss limitations of both forms of bidirectional
typing, providing us with the motivation for the contextual typing approach.
2.1

Bidirectional Typing

Bidirectional STLC. To illustrate bidirectional typing, we use the variant of the Simply Typed
Lambda Calculus (STLC) by Dunfield and Krishnaswami as an example in Fig. 1. The original
calculus uses unit and unit types, which we replace by integers and integer types. This calculus isdesigned based on a design recipe by Dunfield and Pfenning [2004], called the Pfenning recipe. This
recipe gives a guideline on how to bidirectionalize type assignment systems. Intuitively, we first findthe principal judgment and follow the rules: introduction forms check types, and elimination forms
infer types. The Lit and Var rules are two base rules: 𝑖 can check against the Int type and variable
𝑥 can infer the type 𝐴 by looking up the typing environment Γ. The checking rule for integers
strictly follows the Pfenning recipe. The subsumption rule Sub switches from checking to inferencemode by comparing the type equality between the inferred and the checked types. The annotation
rule Anno infers the type 𝐴 from the annotation and uses it to check the term 𝑒. In the Lam rule, thelambda term 𝜆𝑥 . 𝑒 checks against a function type 𝐴 → 𝐵, and the output type 𝐵 will be used tocheck the body 𝑒 in an extended environment. The application rule App is the most interesting one.
In order to infer the type of the application, we first infer 𝑒 1 ’s type and obtain the function type,then use its input type 𝐴 to check the argument 𝑒 2 and use its output type 𝐵 as the inference resultof the application. For example, we can infer the type of ((𝜆𝑓 . 𝑓 1) : (𝐼 → 𝐼 ) → 𝐼 ) (𝜆𝑥 . 𝑥), where
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:4

Xu Xue and Bruno C. d. S. Oliveira

the annotated lambda expecting a function 𝑓 is applied to a raw lambda (𝐼 stands for Int).
...

...

Γ ⊢ (𝜆𝑓 . 𝑓 1) : (𝐼 → 𝐼 ) → 𝐼 ⇒ (𝐼 → 𝐼 ) → 𝐼AnnoΓ ⊢ 𝜆𝑥 . 𝑥 ⇐ 𝐼 → 𝐼

Lam
App

Γ ⊢ ((𝜆𝑓 . 𝑓 1) : (𝐼 → 𝐼 ) → 𝐼 ) (𝜆𝑥 . 𝑥) ⇒ 𝐼

The derivation infers a function type (𝐼 → 𝐼 ) → 𝐼 . The input type 𝐼 → 𝐼 is used to check theargument 𝜆𝑥 . 𝑥, and the output type 𝐼 is used as the inference result of the application.
Mode-correctness. The possibility of using two modes for typing brings up the question of when
to use one mode or the other in both the premises and the conclusions. The choices in Fig. 1 are notunique, and there are several alternative ways to use modes, and still obtain a set of rules that can bedirectly implemented as an algorithm. However, there are some choices for the usage of the modes
that are non-algorithmic. It is possible to design bidirectional rules where types need to be guessed.
Dunfield and Krishnaswami suggest the notion of mode-correctness as a criterion to ensure thepossibility of a bidirectional rule being implementable. Intuitively, we must avoid guessing a typewhen we design bidirectional typing rules. When we check the term in the premise by some type,
the type must come from other synthesized terms or the checking type in the conclusion. When
we infer the type of the conclusion, the type should come from synthesized results of premises.
Dunfield and Krishnaswami identified four different mode-correct application rules. Among thoserules, App1 is the default choice for most bidirectional type systems.
Γ ⊢ 𝑒1 ⇒ 𝐴 → 𝐵Γ ⊢ 𝑒2 ⇐ 𝐴Γ ⊢ 𝑒2 ⇒ 𝐴Γ ⊢ 𝑒1 ⇐ 𝐴 → 𝐵Γ ⊢ 𝑒1 𝑒2 ⇒ 𝐵
Γ ⊢ 𝑒1 ⇒ 𝐴 → 𝐵Γ ⊢ 𝑒2 ⇒ 𝐴

App1
App3

Γ ⊢ 𝑒1 𝑒2 ⇐ 𝐵
Γ ⊢ 𝑒1 ⇒ 𝐴 → 𝐵Γ ⊢ 𝑒2 ⇐ 𝐴

App2
App4

Γ ⊢ 𝑒1 𝑒2 ⇒ 𝐵
Γ ⊢ 𝑒1 𝑒2 ⇐ 𝐵
Note that App3 and App4 can be subsumed by App1 with the subsumption rule, but not App2, which
does add expressive power to the type system. With App2, we can annotate the application andutilize the inference result of arguments to further check the function. For example, ((𝜆𝑥 . 𝑥) 𝑧) : Intcannot infer a type for a system with only App1, but type checks with App2 included.
...
Γ, 𝑧 : Int ⊢ 𝜆𝑥 . 𝑥 ⇐ Int → Int

Lam(𝑧 : Int) ∈ Γ, 𝑧 : Int
Γ, 𝑧 : Int ⊢ 𝑧 ⇒ Int

Γ, 𝑧 : Int ⊢ (𝜆𝑥 . 𝑥) 𝑧 ⇐ Int
Γ, 𝑧 : Int ⊢ ((𝜆𝑥 . 𝑥) 𝑧) : Int ⇒ Int

Var
App2
Anno

Backtracking. Both App1 and App2 can type check terms that cannot be type checked with theother rule alone. Thus, one may wonder if it is possible to have both rules in the same type system.
This is possible, and it can be implemented. However, simply adding the App2 rule comes at a cost:
we may need to backtrack when type checking an application. Since the two application rules do
not subsume each other we may need to try both rules for some applications in order to make typechecking work. For instance, when type checking expressions such as (((𝜆𝑓 . 𝑓 1) : (𝐼 → 𝐼 ) →𝐼 ) (𝜆𝑥 . 𝑥)) : 𝐼 , we have to check the application with the type Int. In an implementation, we would
typically give less priority to the subsumption rule, in order to try other checking rules first. So,
the natural choice would be to try to use App2 first in this case. In this case App2 fails, then wetry the subsumption rule (Sub), and App1 succeeds. Since applications are pervasive in programs,
backtracking is problematic as it can introduce significant slowdowns in the type checker. Thus,
many implementations would avoid having the two rules and would typically prefer App1.
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual Typing

266:5

Γ pΨ⊢𝑒 ⇒𝐴(Under environment Γ and application stack Ψ, 𝑒 infers the type 𝐴)Γ ⊢ 𝑖 ⇒ Int(𝑥 : 𝐴) ∈ ΓLitΓ⊢𝑥 ⇒𝐴Γ ⊢ 𝑒2 ⇒ 𝐴

Γ, 𝑥 : 𝐴 p Ψ ⊢ 𝑒 ⇒ 𝐵VarΓ p Ψ, 𝐴 ⊢ 𝜆𝑥 . 𝑒 ⇒ 𝐴 → 𝐵Γ p Ψ, 𝐴 ⊢ 𝑒 1 ⇒ 𝐴 → 𝐵Γ p Ψ ⊢ 𝑒1 𝑒2 ⇒ 𝐵

Lam

AppS

Fig. 2. Let arguments go first, and the application mode for the STLC.

2.2

Let Arguments Go First

The two previous application rules are useful. However, there are programs that appear to haveenough contextual information, but do not type check by any of the mode-correct application rulesin bidirectional typing. For instance, to infer the type of (𝜆𝑥 . 𝜆𝑦. 𝑥 +𝑦) 1 2, we can neither pick App1
nor App2. App1 cannot be applied because 𝜆𝑥 . 𝜆𝑦. 𝑥 + 𝑦 is a raw lambda that infers nothing. App2
cannot be applied because the application is not annotated thus we know nothing about the output
type. The approach with bidirectional typing is all-or-nothing and forbids partial type information
to be used (i.e. information about the inputs of functions only) to assist inference. Nonetheless,type information about arguments can be used to infer the type of raw lambdas. This problem has
been observed by Xie and Oliveira [2018], and an alternative formulation of bidirectional typing
has been proposed. Instead of combining checking and inference modes, there is a combination of
application and inference modes. We present the STLC version of this approach in Fig. 2.
The key idea is to introduce an extra environment, called the application stack Ψ, which storescontextual type information about the types of the arguments. The inference mode then becomesa special case of the application mode when the stack is empty. In other words, Γ ⊢ 𝑒 ⇒ 𝐴 is
syntactic sugar that stands for Γ p . ⊢ 𝑒 ⇒ 𝐴. We omit the stack in rule Lit and Var to emphasize
the use of the inference mode in those rules. AppS and Lam are the two rules that interact with theapplication stack. Rule AppS first infers the type 𝐴 from argument 𝑒 2 , and pushes the type 𝐴 into
the application stack of 𝑒 1 . With the help of an extended stack, 𝑒 1 infers the function type 𝐴 → 𝐵,
and the output type is used as the inference result of the application term. In rule Lam, we pop one
type from the stack and use it as the type of bound variable, and then we further infer the body oflambda. With the application mode, (𝜆𝑥 . 𝜆𝑦. 𝑥 + 𝑦) 1 2 is typeable as shown in the derivation:...
Γ, 𝑥 : 𝐼, 𝑦 : 𝐼 p . ⊢ 𝑥 + 𝑦 ⇒ 𝐼

AppSΓ, 𝑥 : 𝐼 p 𝐼 ⊢ 𝜆𝑦. 𝑥 + 𝑦 ⇒ 𝐼 → 𝐼

LamΓ p 𝐼, 𝐼 ⊢ 𝜆𝑥 . 𝜆𝑦. 𝑥 + 𝑦 ⇒ 𝐼 → 𝐼 → 𝐼

Lam

Γ⊢1⇒𝐼

Γ p 𝐼 ⊢ (𝜆𝑥 . 𝜆𝑦. 𝑥 + 𝑦) 1 ⇒ 𝐼 → 𝐼
Γ p . ⊢ (𝜆𝑥 . 𝜆𝑦. 𝑥 + 𝑦) 1 2 ⇒ 𝐼

Lit
AppS

Γ⊢2⇒𝐼

Lit
AppS

Let expressions as sugar. Standard bidirectional typing requires extra annotations on lambdas orapplications to type (𝜆𝑥 . 𝑒 2 ) 𝑒 1 . One virtue of the application mode is that let-expressions can be
simply encoded as syntactic sugar, without adding new constructs or new typing rules:
let 𝑥 = 𝑒 1 in 𝑒 2 ≜ (𝜆𝑥 . 𝑒 2 ) 𝑒 1
Limitations. Unfortunately, the AppS rule excludes cases that standard bidirectional typing canaccept. For example, the term ((𝜆𝑓 . 𝑓 1) : (𝐼 → 𝐼 ) → 𝐼 ) (𝜆𝑥 . 𝑥), cannot be typed with the rules in
Fig 2. More interestingly, even though AppS appears to be related to App2, since both rules require
the inference of the argument, AppS cannot subsume App2 either. For example, AppS cannot typecheck the expression ((𝜆𝑥 . 𝜆𝑦. 𝑦) 1) : 𝐼 → 𝐼 because it does not deal with annotated terms. Thus, it
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:6

Xu Xue and Bruno C. d. S. Oliveiracannot propagate the outer annotation to the subterms of the application. In essence, the powerof the checking mode is missing. As acknowledged by Xie and Oliveira, the application mode isstronger than the inference mode, but weaker than the checking mode.
To combine the power of both approaches, one option discussed (but not formalized) by Xie andOliveira, is to have the inference mode, the application mode and the checking mode in a single
calculus. Then we could have a calculus that could type all the examples shown so far. Basically, thiscalculus would include three modes (checking, inference and application) and also three application
rules: App1, App2 and AppS. We refer to the work of Xie and Oliveira for a more detailed discussion.
We give one example that showcases the power of the three different rules in combination.
let 𝑧 = 1 in (𝜆𝑓 . 𝑓 1 : ((𝐼 → 𝐼 ) → 𝐼 )) ((𝜆𝑥 . 𝜆𝑦. 𝑦) 𝑧)
AppS allows writing let-expressions as sugar to applications and without annotations (when thearguments can be inferred). The rule App1 allows the annotation of functions to be used to check thearguments. Moreover, App2 allows unannotated applications, such as (𝜆𝑥 . 𝜆𝑦. 𝑦) 𝑧, to be checked.
Backtracking. Unfortunately, now there would be an even worse problem with backtracking.
We have 3 different rules for applications, with none of the rules being better than the others. In
the worst case, we have to try the 3 rules for every application. This would be quite inefficient inpractice. While using just one of the rules in an implementation addresses the efficiency problem, it
gives up the expressiveness afforded by the other rules, requiring programs with more annotationsor the addition of new constructs and typing rules. If we use App1 only, then we need to write:((𝜆𝑧. (𝜆𝑓 . 𝑓 1 : (𝐼 → 𝐼 ) → 𝐼 ) (((𝜆𝑥 . 𝜆𝑦. 𝑦) : 𝐼 → 𝐼 → 𝐼 ) 𝑧)) : 𝐼 → 𝐼 ) 1
Here we desugar the let expression into an explicit lambda, so that we can annotate the desugared
lambda. In addition, we would need to introduce an annotation in (𝜆𝑥 . 𝜆𝑦. 𝑦) 𝑧. Alternatively, we
could introduce let expressions directly together with corresponding typing rules, to address theissue with let 𝑧 = 1 in . . ., and also change the term (𝜆𝑥 . 𝜆𝑦. 𝑦) 𝑧 to a let expression. However, as
we shall discuss in Section 2.3, introducing let expressions still has some issues.
2.3

Binding Constructs

As Dunfield and Krishnaswami [2021] observe, binding constructs, such as let expressions or
eliminators for sums introduce some additional complications for bidirectional typing. The Pfenningrecipe to derive bidirectional rules applies to introduction and elimination forms, but let-expressions
are neither. So, the first challenge is to decide how to bidirectionalize let expressions:Γ ⊢ 𝑒1 ⇒ 𝐴
Γ, 𝑥 : 𝐴 ⊢ 𝑒 2 : 𝐵LetΓ ⊢ let 𝑥 = 𝑒 1 in 𝑒 2 : 𝐵
It is unclear to further determine the direction of the second premise and conclusion. The suggested
approach is to have two variants of the rule, to type check more programs.
Γ ⊢ 𝑒1 ⇒ 𝐴
Γ, 𝑥 : 𝐴 ⊢ 𝑒 2 ⇒ 𝐵
Γ ⊢ 𝑒1 ⇒ 𝐴
Γ, 𝑥 : 𝐴 ⊢ 𝑒 2 ⇐ 𝐵
LetInf

LetChkΓ ⊢ let 𝑥 = 𝑒 1 in 𝑒 2 ⇒ 𝐵
Γ ⊢ let 𝑥 = 𝑒 1 in 𝑒 2 ⇐ 𝐵
For the example mentioned above, rewritten into a let-binding form:
let 𝑧 = 1 in (𝜆𝑓 . 𝑓 1 : ((𝐼 → 𝐼 ) → 𝐼 )) (let 𝑥 = 𝑧 in 𝜆𝑦. 𝑦)
the outside let uses LetInf rule to infer its result. The inside let uses LetChk to propagate thetype 𝐼 → 𝐼 to the body. Rule LetChk is similar to App2, but specialized to let expressions.
Unclear annotatability. Dunfield and Pfenning [2004] suggested that annotations are only neededat redexes. However, Dunfield and Krishnaswami [2021] noted that this is not true in the presenceof binding constructs, even with two rules for binding constructs. For instance, consider a typesystem with two let rules and only the App1 rule. Now consider the (unannotated) expression:(let 𝑥 = 1 in 𝜆𝑓 . 𝑓 𝑥) (𝜆𝑥 . 𝑥)
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual Typing

266:7

In this case, we must either put annotations on the body of let, then use LetInf to infer the typeof the let expression, or around the let expression to use the contextual information to check its
body. Thus, for some bidirectional type systems with binding constructs, it may not be easy to giveprogrammers a clear guideline as to where to place annotations.
2.4 Subtyping
In calculi with subtyping, an important idea is that the subsumption rule is used to encapsulate theuses of subtyping in a single place. This is commonly used in type assignment systems (TASs), andalso in (simple) bidirectional type systems. The bidirectional rule for subtyping is analogous to rule
Sub in Fig 1, with type equality replaced with subtyping.
Γ ⊢𝑒 ⇒𝐴
𝐴 <: 𝐵Γ ⊢𝑒 ⇐𝐵

Sub

However, in the presence of more complex subtyping relations, the bidirectional subsumption
rule is not powerful enough to encapsulate many of the desired uses of subtyping. For instance,intersection types [Barendregt et al. 1983; Coppo et al. 1981; Pottinger 1980; Reynolds 1991] areused to assign multiple types to one expression. Type systems with intersection types often use
three subtyping rules to characterize this idea:
𝐴 <: 𝐶𝐵 <: 𝐶𝐴 <: 𝐵𝐴 <: 𝐶
SAndL

SAndR

𝐴 & 𝐵 <: 𝐶SAnd

𝐴 & 𝐵 <: 𝐶

𝐴 <: 𝐵 & 𝐶

If we use rule App1, and the bidirectional subsumption rule, then some programs that we expect
to type check, would no longer type check. For instance, (𝜆𝑓 . 𝑓 1) : ((𝐼 → 𝐼 ) & (𝐹 → 𝐹 )) → 𝐼 (𝐹stands for the Float type) is a higher order function that expects an overloaded function with theintersection type (𝐼 → 𝐼 ) & (𝐹 → 𝐹 ). This function cannot type check using the App1 rule:𝑓 : (𝐼 → 𝐼 ) & (𝐹 → 𝐹 ) ⊢ 𝑓 ⇒ (𝐼 → 𝐼 ) & (𝐹 → 𝐹 )𝑓 : (𝐼 → 𝐼 ) & (𝐹 → 𝐹 ) ⊢ 1 ⇐ ?
App1Fail𝑓 : (𝐼 → 𝐼 ) & (𝐹 → 𝐹 ) ⊢ 𝑓 1 ⇒ ?

In the rule App1, the function 𝑒 1 is expected to have function type 𝐴 → 𝐵, instead of the intersection
type in this case. Thus, rule App1 will reject this program. In contrast, the equivalent TAS would
accept the program above. A possible solution is to modify the application rule as follows:Γ ⊢ 𝑒1 ⇒ 𝐴

𝐴 <: 𝐵 → 𝐶Γ ⊢ 𝑒2 ⇐ 𝐵

Γ ⊢ 𝑒1 𝑒2 ⇒ 𝐶

AppThis rule allows for a more flexible form of application, that solves our problem, since it accounts
for subtyping and for types that are subtypes of functions. However, there are two issues withthis rule. The first one is that the rule gives up the principle of encapsulating uses of subtyping
in the subsumption rule. The second one is that the rule is non-algorithmic (since the type 𝐵 isguessed). The second issue is solvable by creating specialized relations that avoid guessing 𝐵 andthus can be implemented in an algorithm. This is currently the standard solution for this problem incalculi with bidirectional typing. In calculi with intersection types, a selection/matching judgment
is introduced in the application rules [Davies and Pfenning 2000; Huang et al. 2021]:
Γ ⊢ 𝑒1 ⇒ 𝐴

𝐴⊲𝐵 →𝐶Γ ⊢ 𝑒1 𝑒2 ⇒ 𝐶Γ ⊢ 𝑒2 ⇐ 𝐵

AppThe selection judgment 𝐴 ⊲ 𝐵 → 𝐶 simply tries to select one instance from different branches ofintersection types. The selection judgment should, ideally, be sound and complete to 𝐴 <: 𝐵 → 𝐶.
Although this approach addresses the algorithmic problem, it requires modifying the standard
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:8Xu Xue and Bruno C. d. S. Oliveira

application rule and coming up with a new specialized rule and a new auxiliary judgment for
applications. Similar solutions exist for other subtyping relations, such as relations with union
types [Rioux et al. 2023], polymorphic types [Dunfield and Krishnaswami 2013; Zhao et al. 2019],
etc. However, it would be preferable to use the standard application rule and delegate dealing with
subtyping to a stronger subsumption rule, thus avoiding the need for specialized relations.
2.5

Problem Statement and Paper Roadmap

Bidirectional typing provides great value for money: it is a simple, lightweight approach that canscale up to many different type systems and features. In practice, it eliminates the need for many
obvious annotations, while requiring only a reasonable amount of annotations. However, as seenin this section, it does have some limitations. In particular, we identified three concrete problems:(1) Trade-off between expressive power and backtracking. As we have seen in Sections 2.1
and 2.2, there is no single application rule that is always better. Choosing one of the rules
only limits the expressive power (i.e. it results in more required annotations). Choosing all
the rules raises efficiency concerns since backtracking seems to be required.
(2) Unclear annotatability and rule duplication. In the presence of certain features, andin particular binding constructs, there is no simple guideline for how to identify where
annotations are needed. Moreover, often multiple versions of a rule are needed.
(3) Inexpressive subsumption. The bidirectional subsumption rule lacks expressive power.
Many type systems with subtyping require changes in other rules, to accommodate for thelack of expressive power of bidirectional subsumption. In addition, new auxiliary relations,which provide specialized forms of subtyping, are often needed.
We would like to retain the key advantages of bidirectional typing, while improving on the threepoints above. As we shall see, contextual typing provides a generalization of bidirectional typingthat largely realizes this goal. Sections 3 and 4 will show how to address (1) and (2) first in a
simplified setting. Section 5 will show how to deal with (3) and present a more complete typesystem with subtyping.
3

Quantitative Type Assignment Systems

In this section, we introduce Quantitative Type Assignment Systems (QTASs). QTASs are variants oftype assignment systems enriched with a notion of counters, which generalize modes in bidirectional
typing. QTASs serve as an intermediate step in between traditional type assignment systems andalgorithmic formulations. A QTAS guides the formulation of the algorithmic system and aids in its
metatheory. Unlike type assignment systems, QTASs precisely specify where type annotations areneeded. Moreover, they quantify the amount of type information that a term needs in order to typecheck. As we shall see, with QTASs, we can have a type system that includes all the expressive powerof the three application rules discussed in Section 2. In Section 4 we will present a non-backtracking
algorithmic formulation that can be used to implement our most expressive QTAS in this section.
3.1

Quantitative Type Assignment Systems for STLC

We present several variants of QTAS for STLC in this section to illustrate the key ideas and toestablish a connection to standard bidirectional typing and the let arguments go first approaches.
Syntax. The syntax of types and typing environments is the same for all the variants, but
expressions and counters change according to each QTAS. For expressions the key difference iswhether annotated expressions (𝑒 : 𝐴) are supported or not. We define types and environments
below. Metavariables 𝐴, 𝐵, 𝐶, 𝐷 range over types. Types are integer types and function types. A
typing environment is a sequence of variables associated with their types.
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual Typing

266:9

Γ ⊢𝑛 𝑒 : 𝐴(Under Γ, expression 𝑒 needs 𝑛 contextual information to have type 𝐴.)

DLit

DVar

DAnn

DLam

Γ ⊢0 𝑥 : 𝐴Γ ⊢0 (𝑒 : 𝐴) : 𝐴Γ ⊢∞ 𝜆𝑥 . 𝑒 : 𝐴 → 𝐵

𝑥 :𝐴∈Γ

Γ ⊢0 𝑖 : IntΓ ⊢∞ 𝑒 : 𝐴

Γ, 𝑥 : 𝐴 ⊢∞ 𝑒 : 𝐵

DApp2

DApp1

Γ ⊢0 𝑒 1 : 𝐴 → 𝐵

Γ ⊢∞ 𝑒 2 : 𝐴Γ ⊢0 𝑒 1 𝑒 2 : 𝐵Γ ⊢∞ 𝑒 1 : 𝐴 → 𝐵Γ ⊢0 𝑒 2 : 𝐴

DSubΓ ⊢0 𝑒 : 𝐴Γ ⊢∞ 𝑒 1 𝑒 2 : 𝐵

𝐴=𝐵Γ ⊢∞ 𝑒 : 𝐵

Fig. 3. STLC with all-or-nothing counters.

𝐴, 𝐵, 𝐶, 𝐷 ::= Int | 𝐴 → 𝐵

TypesΓ ::= · | Γ, 𝑥 : 𝐴

Typing Environments
3.2

All-or-Nothing Counters

The first QTAS that we are going to show is the one with all-or-nothing counters. We define its
expressions and counters below. This QTAS is equivalent to the standard bidirectional typing rules
presented in Fig. 1 extended with the App2 rule, and with an inference rule for integers.
Expressions
𝑒 ::= 𝑖 | 𝑥 | 𝜆𝑥 . 𝑒 | 𝑒 1 𝑒 2 | 𝑒 : 𝐴
Counters

𝑛 ::= 0 | ∞Expressions consist of integers, variables, lambdas, applications and annotated terms. In this version
of a QTAS, counters are degenerate and can only be nothing (0) or everything (∞). We use countersto represent how much type information is needed, from the surrounding context, when typechecking expressions. The two counters represent two extremes: 0 means that no type informationis needed to type a term; ∞ means that all type information is needed to type a term.
Typing and comparison with modes. We present typing in Fig. 3. The form of the typing judgementis Γ ⊢𝑛 𝑒 : 𝐴, which means that under environment Γ, expression 𝑒 is typeable with 𝐴 assuming𝑛 contextual information about 𝐴. Readers familiar with bidirectional typing may interpret two
instances of counters as modes: counter 0 is the inference mode and counter ∞ is the checking
mode. In other words, for this first formulation of a QTAS, the rules that we present in Fig. 3 arealmost the same as those in Fig. 1. The main difference is notational: we simply use counters insteadof modes, which is of course a rather superficial difference for this version.
There are two other differences to the rules in Fig. 1. Firstly, we include a version of the rule
App2 (rule DApp2) as well, because we wish to capture all mode-correct rules for applications
in standard bidirectional typing. Secondly, the DLit rule, when interpreted bidirectionally, is ininference mode, rather than in checking mode. Using 0 as the counter for the DLit is consistent
with the interpretation of the counter, which measures how much information is needed from thesurrounding context. For integers no information is needed. Finally, although the DSub rule is thesame as in bidirectional typing, it is worthwhile reinterpreting the rule from the point of view of a
QTAS. This rule states that a term that needs no information to be typed can be interpreted as aterm that requires more information to be typed. In other words, additional contextual information
does not affect typeability. The soundness and completeness theorems to the type system in Fig. 1,
extended with an inference rule for integers and with the App2 rule are straightforward.
Theorem 3.1 (Soundness).
• If Γ ⊢0 𝑒 : 𝐴 then Γ ⊢ 𝑒 ⇒ 𝐴. • If Γ ⊢∞ 𝑒 : 𝐴 then Γ ⊢ 𝑒 ⇐ 𝐴.
Theorem 3.2 (Completeness).
• If Γ ⊢ 𝑒 ⇒ 𝐴 then Γ ⊢0 𝑒 : 𝐴. • If Γ ⊢ 𝑒 ⇐ 𝐴 then Γ ⊢∞ 𝑒 : 𝐴.
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:10

Xu Xue and Bruno C. d. S. Oliveira

DLit

DLam

Γ ⊢0 𝑥 : 𝐴Γ ⊢ (𝑆 𝑛) 𝜆𝑥 . 𝑒 : 𝐴 → 𝐵

𝑥 :𝐴∈Γ

Γ ⊢0 𝑖 : Int

DApp

DVar

Γ, 𝑥 : 𝐴 ⊢𝑛 𝑒 : 𝐵Γ ⊢ (𝑆 𝑛) 𝑒 1 : 𝐴 → 𝐵Γ ⊢0 𝑒 2 : 𝐴Γ ⊢𝑛 𝑒 1 𝑒 2 : 𝐵

Fig. 4. STLC with application counters.

3.3

Application Counters

We now present another QTAS with application counters that is equivalent to the type system inFig. 2. Unlike all-or-nothing counters, application counters measure how much contextual type
information we need to type a term. We define the syntax below and present the typing in Fig. 4.
Expressions
𝑒 ::= 𝑖 | 𝑥 | 𝜆𝑥 . 𝑒 | 𝑒 1 𝑒 2𝑛 ::= 0 | 𝑆 𝑛

Counters

We have two instances of counters: nothing (0) and 𝑆 𝑛. We do not deal with annotated terms,
thus 𝑒 : 𝐴 is not included. The two interesting rules are DLam rule and DApp. In DLam, counter 𝑆 𝑛
indicates that in the function type 𝐴 → 𝐵, the input type 𝐴 must be known from the surrounding
context. Then we can use it as the type of bound variable 𝑥. In DApp, we infer the type of 𝑒 2 , andincrement the counter 𝑛 of 𝑒 1 , to express that 𝐴 is known. Thus, we can infer the type 𝐴 → 𝐵 withthe help of propagated information. The output type 𝐵 will be the result type of the application.
Intuitively, the counter denotes the size of the application stack. Thus we can show a correspondence to the type system in Fig. 2 with the following theorems. What we need is to define an
auxiliary judgment that connects the counter to the application stack 𝑛 ∼ Ψ ∼ 𝐴. The 0 counterconnects to an empty stack and any type, and 𝑆 𝑛 connects to Ψ, 𝐴 and 𝐴 → 𝐵 inductively.
𝑛∼Ψ∼𝐵
0∼.∼𝐴

∼Empty𝑆 𝑛 ∼ Ψ, 𝐴 ∼ 𝐴 → 𝐵∼Cons

If the term 𝑒 can be typed with the type 𝐴 with counter 𝑛 and 𝑛 is consistent with Ψ, it can infer 𝐴
with the application stack Ψ, and vice-versa.
Theorem 3.3 (Soundness). If Γ ⊢𝑛 𝑒 : 𝐴 and 𝑛 ∼ Ψ ∼ 𝐴, then Γ p Ψ ⊢ 𝑒 ⇒ 𝐴.
Theorem 3.4 (Completeness). If Γ p Ψ ⊢ 𝑒 ⇒ 𝐴 and 𝑛 ∼ Ψ ∼ 𝐴, then Γ ⊢𝑛 𝑒 : 𝐴.
3.4

All in One

Finally, we show a QTAS that combines all-or-nothing counters and application counters. Comparedwith the previous QTASs, we include both annotated terms and application counters.
Expressions

𝑒 ::= 𝑖 | 𝑥 | 𝜆𝑥 . 𝑒 | 𝑒 1 𝑒 2 | 𝑒 : 𝐴

Counters

𝑛 ::= 0 | ∞ | 𝑆 𝑛

Syntactic Sugar

let 𝑥 = 𝑒 1 in 𝑒 2 ≜ (𝜆𝑥 . 𝑒 2 ) 𝑒 1

We present our typing rules in Fig. 5. DLit and DVar are unsurprising. In rule DAnn the annotatedterm 𝑒 : 𝐴 is typeable with type 𝐴 without any additional contextual type information, if 𝑒 is
typeable with 𝐴 with full contextual information. DLam type checks a lambda only when the
counter can be decreased, which means that the information for the input type 𝐴 must be available
contextually. The 𝑛− meta-operation is defined with two simple cases: ∞− = ∞; and (𝑆 𝑛)− = 𝑛.
The lambda body (𝑒) may itself require some amount of contextual information 𝑛. For instance, thelambda term 𝜆𝑥 . 𝜆𝑦. 𝑥 + 𝑦 is typeable if the counter is at least 2: the lambda body 𝜆𝑦. 𝑥 + 𝑦 requires
type information for 𝑦, whereas the outer lambda requires type information for 𝑥. Rules DApp1
and DApp2 describe two situations: whether the function can infer or the argument can infer. We
use the word infer here to represent the situation where the counter is 0. In DApp1, if the function
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual Typing

266:11

DApp1

DAnn

DLam

Γ ⊢0 (𝑒 : 𝐴) : 𝐴Γ ⊢𝑛 𝜆𝑥 . 𝑒 : 𝐴 → 𝐵

Γ ⊢∞ 𝑒 : 𝐴

Γ, 𝑥 : 𝐴 ⊢𝑛− 𝑒 : 𝐵

DVar

DLit

Γ ⊢0 𝑒 : 𝐴Γ ⊢0 𝑥 : 𝐴Γ ⊢∞ 𝑒 2 : 𝐴Γ ⊢0 𝑒 1 𝑒 2 : 𝐵
DApp2

DSub

𝑥 :𝐴∈Γ

Γ ⊢0 𝑖 : IntΓ ⊢0 𝑒 1 : 𝐴 → 𝐵𝑛≠0Γ ⊢ (𝑆 𝑛) 𝑒 1 : 𝐴 → 𝐵Γ ⊢𝑛 𝑒 : 𝐴Γ ⊢0 𝑒 2 : 𝐴Γ ⊢𝑛 𝑒 1 𝑒 2 : 𝐵

Fig. 5. All-in-one QTAS for STLC.

...
Γ, 𝑧 : 𝐼 ⊢0 𝑧 : 𝐼DLamΓ, 𝑧 : 𝐼 ⊢∞ let 𝑥 = 𝑧 in (𝜆𝑦. 𝑦) : 𝐼 → 𝐼...
Γ ⊢0 1 : 𝐼

Γ, 𝑧 : 𝐼, 𝑥 : 𝐼 ⊢∞ 𝜆𝑦. 𝑦 : 𝐼 → 𝐼

LetΓ, 𝑧 : 𝐼 ⊢0 (𝜆𝑓 . 𝑓 1 : ((𝐼 → 𝐼 ) → 𝐼 )) (let 𝑥 = 𝑧 in (𝜆𝑦. 𝑦)) : 𝐼

DApp1

Γ ⊢0 let 𝑧 = 1 in (𝜆𝑓 . 𝑓 1 : ((𝐼 → 𝐼 ) → 𝐼 )) (let 𝑥 = 𝑧 in (𝜆𝑦. 𝑦)) : 𝐼

Let

Fig. 6. Typing derivation for the motivating example in Section 2.2.

𝑒 1 infers the type 𝐴 → 𝐵, then we have all the information available for the argument, and canuse that to check whether 𝑒 2 has type 𝐴. In rule DApp2, if the argument 𝑒 2 infers the type 𝐴, we
increment the counter for the function, since we have all the type information for the argument.
Thus 𝑒 1 can have the type 𝐴 → 𝐵 with additional contextual information. Note that DApp2 merges
the expressiveness of rules App2 and AppS. Thus, we only need two rules, instead of three. As
before, DSub expresses that additional contextual information does not affect typeability.
We show that our all-in-one QTAS is complete with respect to both traditional bidirectional
typing (including rule App2 and integer inference) and application modes. Note that we allow
successor wrapping around ∞. Thus we use a relation ⋍ that relates modes to counters.
⇐⋍ 𝑛
⋍0

⋍∞

⋍S

⇒⋍ 0
⇐⋍ ∞
⇐⋍ 𝑆 𝑛Theorem 3.5 (Completeness).
• If Γ ⊢ 𝑒 ⇔ 𝐴 and ⇔⋍ 𝑛, then Γ ⊢𝑛 𝑒 : 𝐴. • If Γ p Ψ ⊢ 𝑒 ⇒ 𝐴 and 𝑛 ∼ Ψ ∼ 𝐴, then Γ ⊢𝑛 𝑒 : 𝐴.
Encoding let expressions. Like the approach by Xie and Oliveira [2018], we can encode let
expressions as syntactic sugar. The following derivation shows the derivable typing rule for let
expressions (from the syntactic sugar):Γ, 𝑥 : 𝐴 ⊢𝑛 𝑒 2 : 𝐵Γ ⊢0 𝑒 1 : 𝐴

Γ, 𝑥 : 𝐴 ⊢𝑛 𝑒 2 : 𝐵Γ ⊢𝑛 let 𝑥 = 𝑒 1 in 𝑒 2 : 𝐵

LetΓ ⊢𝑆 𝑛 𝜆𝑥 . 𝑒 2 : 𝐴 → 𝐵

DLamΓ ⊢0 𝑒 1 : 𝐴Γ ⊢𝑛 (𝜆𝑥 . 𝑒 2 ) 𝑒 1 : 𝐵

DApp2

On the left we present the derived rule and on the right we desugar the let expression to show how
the rule can be derived. This rule subsumes the two bidirectional typing rules for let expressions
presented in Section 2.3. The inference rule corresponds to 𝑛 being 0 and the checking rule corresponds to 𝑛 being ∞. Moreover, 𝑛 can also be 𝑆 𝑛 ′ , which has no correspondence in the bidirectionalrules. Figure 6 illustrates the expressiveness of the QTAS with our example in Section 2.2, which
requires the power of the three application rules.
A remark and a closer look at counters. An important remark here is that the STLC allows for a
simple formulation of counters. As we shall see in Section 5, in more complex calculi, we may need
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:12

Xu Xue and Bruno C. d. S. Oliveiraa more fine-grained definition of counters. It is useful to have a closer look at the role of counters
to better understand how counters are used by a QTAS.
Counters in Fig. 5 track the number of times that the DApp2 rule needs to be applied to obtainenough type information from the surrounding context. In turn this implies that counters track thenumber of arguments that must have inferred types (since DApp2 requires that we must be able toinfer types for arguments). For instance consider the term (𝜆𝑥 . 𝑓 ) 1 (𝜆𝑥 . 𝑥) 2, where 𝑓 has type
(𝐼 → 𝐼 ) → 𝐼 → 𝐼 in the typing environment. The typing derivation for this term is:...
Γ ⊢ (𝑆 0) 𝜆𝑥 . 𝑓 : 𝐼 → (𝐼 → 𝐼 ) → 𝐼 → 𝐼

LamΓ ⊢0 1 : 𝐼Γ ⊢0 (𝜆𝑥 . 𝑓 ) 1 : (𝐼 → 𝐼 ) → 𝐼 → 𝐼

DApp2

Γ ⊢∞ 𝜆𝑥 . 𝑥 : 𝐼 → 𝐼Γ ⊢0 (𝜆𝑥 . 𝑓 ) 1 (𝜆𝑥 . 𝑥) : 𝐼 → 𝐼

DApp1

Γ ⊢∞ 2 : 𝐼Γ ⊢0 (𝜆𝑥 . 𝑓 ) 1 (𝜆𝑥 . 𝑥) 2 : 𝐼

DApp1

For typing this term it is necessary that the type of the argument 1 is inferable (which is thecase). In other words we must use DApp2 to type (𝜆𝑥 . 𝑓 ) 1. When typing the abstraction 𝜆𝑥 . 𝑓
the QTAS uses a counter 𝑆 0, to signal that the lambda expression can only be typed in a context
with an inferable argument. The other two arguments (𝜆𝑥 . 𝑥 and 2) will be checked against 𝐼 → 𝐼
and 𝐼 , respectively, by using DApp1. Importantly, the arguments checked with DApp1 do not reallyinfluence the types used in the typing derivation. While this is true for STLC, it is not true ingeneral. In some type systems, especially those with subtyping, the checkable arguments that are
typed with DApp1 may influence the typing derivation in significant ways. In that case, it is also
important to track the number of uses of DApp1 or checkable arguments (in addition to the numberof inferable arguments). We will come back to this point in Section 5.
3.5

Comparison and Correspondence to Type Assignment Systems

Differently from type assignment systems, QTASs use counters to quantify needed contextual
information, and restrict typing derivations. Still, QTASs are (in general) non-algorithmic. For
instance, in rule DLam (from Fig. 5), a counter 𝑆 𝑛 in the conclusion tells us that we have type
information for at least one argument, but does not specify what the type is. We could try tointerpret the typing judgment algorithmically as a function that takes the typing environment
Γ, the expression 𝑒 and the counter 𝑛 as inputs, and returns the type 𝐴 as an output. However, it
should be clear that the counter alone does not provide enough information to determine the type
information available from the context and compute the output type. The role of the counter in a
QTAS is merely to constrain which rules can be used, but types are still being guessed as in a TAS.
For example, if we have an identity function with a non-zero counter, this function can be typed
with multiple types.
Γ, 𝑥 : Int ⊢0 𝑥 : IntΓ ⊢ (𝑆 0) 𝜆𝑥 . 𝑥 : Int → IntDLamΓ, 𝑥 : (Int → Int) ⊢0 𝑥 : Int → Int
Γ ⊢ (𝑆 0) 𝜆𝑥 . 𝑥 : (Int → Int) → (Int → Int)

DLam

Completeness and annotatability. TAS often work on unannotated expressions, guessing all
types. For calculi with undecidable type systems, it is impossible to find algorithms that directly
infer types for all unannotated expressions. Thus, algorithms often need to deal with annotatedexpressions instead. Unlike a TAS, a QTAS requires annotations in a program. Only programs with
sufficient annotations will type-check. Therefore a QTAS can serve as a specification of a typesystem informing where annotations are needed to type check programs.
The completeness of a QTAS with regard to a TAS tells us that a term in a TAS can be typed
in a QTAS after adding some annotations. Dunfield and Krishnaswami [2021] also call this result
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual TypingΓ ⊢ 𝑖 : Int ⇝ 𝑖

266:13ELit(𝑥 : 𝐴) ∈ ΓΓ⊢𝑥 :𝐴⇝𝑥

EVar

Γ, 𝑥 : 𝐴 ⊢ 𝑒 : 𝐵 ⇝ 𝑒 ′Γ ⊢ 𝜆𝑥 . 𝑒 : 𝐴 → 𝐵 ⇝ 𝜆𝑥 . 𝑒 ′Γ ⊢ 𝑒 1 : 𝐴 → 𝐵 ⇝ 𝑒 1′

need 𝑒 1 = 0 ∨ need 𝑒 2 = 0Γ ⊢ 𝑒 1 𝑒 2 : 𝐵 ⇝ 𝑒 1′ 𝑒 2′need 𝑒 1 = 𝑆 𝑛 1 ∧ need 𝑒 2 = 𝑆 𝑛 2

Γ ⊢ 𝑒 1 : 𝐴 → 𝐵 ⇝ 𝑒 1′Γ ⊢ 𝑒 1 𝑒 2 : 𝐵 ⇝ 𝑒 1′ (𝑒 2′ : 𝐴)

Γ ⊢ 𝑒 2 : 𝐴 ⇝ 𝑒 2′

ELam

EApp1

Γ ⊢ 𝑒 2 : 𝐴 ⇝ 𝑒 2′

EApp2

Fig. 7. Elaboration from a TAS to a QTAS, with one possible annotation strategy.

annotatability, which we prefer as it is more descriptive. For instance, we can prove the following
annotatability lemma between a TAS formulation of STLC and the QTAS in Fig. 5:
Theorem 3.6 ((Weak) Annotatability of QTAS). If Γ ⊢ 𝑒 : 𝐴, then ∃ 𝑒 ′, Γ ⊢0 𝑒 ′ : 𝐴 and 𝑒 is thetype erasure of 𝑒 ′ .
The standard annotatability theorem, which we will refer to as weak annotatability, shows that
our QTAS is complete to a TAS by inserting annotations on the unannotated terms. However, it
does not tell us where type annotations are needed. In bidirectional typing, by strictly following
the Pfenning recipe, we can obtain an informal guideline of only putting annotations on redexes.
However this guideline, after adding more constructs and more expressive rules, becomes lessclear [Dunfield and Krishnaswami 2021] (see also Section 2.3).
Strong annotatability of a QTAS. With a QTAS we can prove a stronger annotatability theorem
that also tells us where annotations are needed and formalizes guidelines for how to annotate a
program. To formalize strong annotatability, we first introduce a function need, which specifies
the type information needed by an (unannotated) term to type check in a QTAS.
need (𝜆𝑥 . 𝑒) = 𝑆 (need 𝑒)need 𝑖 = 0

0, if need 𝑒 1 = 0
need 𝑥 = 0
need (𝑒 1 𝑒 2 ) =𝑛, if need 𝑒 1 = 𝑆 𝑛
For a lambda, we need type information for the argument, and the body itself may need some
type information, so we need one more than the body. For an application, if the function 𝑒 1 needs
no type information (i.e. 𝑒 1 is an inferable term), then the whole application does not need type
information to type check. If the function 𝑒 1 needs some amount of type information 𝑆 𝑛, theapplication will need 𝑛, since the only rule that can be used in this case is DApp2, so the argument𝑒 2 must be inferable, thus providing information for the argument of the function.
With need we define a (type-directed) elaboration from a TAS to a QTAS in Fig. 7. In thiselaboration annotations are inserted where needed. The first three rules are straightforward. Only
the two application rules are interesting. EApp1 describes the case where applications do notneed annotations: if 𝑒 1 needs no type information, then we can apply DApp1 to type check thisexpression; if 𝑒 2 needs no type information, then we can apply DApp2. EApp2 describes the casewhere an application needs additional type information: if both 𝑒 1 and 𝑒 2 cannot be inferred (forexample (𝜆𝑥 . 𝑥) (𝜆𝑥 . 𝑥)), we then choose to annotate the argument 𝑒 2 with the type 𝐴. With thiselaboration we can prove the stronger annotatability theorem:
Theorem 3.7 (Strong Annotatability).
(1) If Γ ⊢ 𝑒 : 𝐴 ⇝ 𝑒 ′ , then Γ ⊢ (need 𝑒 ) 𝑒 ′ : 𝐴. (2) If Γ ⊢ 𝑒 : 𝐴 ⇝ 𝑒 ′ , then Γ ⊢0 (𝑒 ′ : 𝐴) : 𝐴.
The first result (1) states that if the term 𝑒 is well-typed in the TAS and elaborated to 𝑒 ′ withannotations inserted, then 𝑒 ′ is well-typed in the QTAS, provided that enough contextual type
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:14

Xu Xue and Bruno C. d. S. Oliveira

information is given. The second result (2) states that, with a top-level annotation we obtainan inferable term. This theorem formalizes a simple annotatability guideline for programmers.
Basically, programmers need to:• provide a top-level type annotation for a term if the term needs type information (for instancethe full term is a lambda) (2);• and, for applications where neither the function or the argument can be inferred, provide anannotation for the argument (1).
Since let expressions let 𝑥 = 𝑒 1 in 𝑒 2 are encodable via applications, from the guideline above we
can deduce that if 𝑒 1 is not inferable then we will need to add an annotation for 𝑒 1 .
Note that the annotation guideline is not unique: we could have different ways to annotate
programs. For instance, instead of annotating the argument, we can annotate the function 𝑒 1 . This
leads to the following elaboration rule:need 𝑒 1 ≡ 𝑆 𝑛 1 ∧ need 𝑒 2 ≡ 𝑆 𝑛 2
Γ ⊢ 𝑒 1 : 𝐴 → 𝐵 ⇝ 𝑒 1′Γ ⊢ 𝑒 2 : 𝐴 ⇝ 𝑒 2′Γ ⊢ 𝑒 1 𝑒 2 : 𝐵 ⇝ (𝑒 1′ : 𝐴 → 𝐵) 𝑒 2′

EApp3

Rules EApp2 and EApp3 provide two different alternative annotatability strategies/guidelines. We
can replace EApp2 by EApp3, or include both rules and the strong annotatability lemma still holds.
To conclude we show how to use our guideline to annotate the example in Section 2.3. In essence,since in the application neither the function nor the argument are inferable, we add an annotation
to the argument, as prescribed by our guideline:(let 𝑥 = 1 in 𝜆𝑓 . 𝑓 𝑥) (𝜆𝑥 . 𝑥 : 𝐼 → 𝐼 )4

Syntax-Directed Algorithmic Type System

In this section, we provide a syntax-directed algorithmic type system that avoids backtracking andimplements the QTAS in Section 3.4. We start with the key idea behind the algorithm, and thenshow the full formalization. Finally, we will discuss its metatheory: decidability, soundness andcompleteness with respect to the QTAS.
4.1

Towards a Non-Backtracking Algorithm

A possible way to naively implement the QTAS discussed in Section 3.4, would be to use theapproach discussed in Section 2.2. Then we would have the three application rules (App1, App2
and AppS) and a type system combining three modes (inference, checking and application). Using
backtracking, we could try all the 3 rules. A key drawback of this approach is performance, since
backtracking could be very costly in practice.
Our goal is to have the same expressive power as the QTAS without using backtracking. Whendesigning the QTAS we already saw that App2 and AppS can be combined into a single rule (DApp2),
which removes some of the overlap between the application rules. However, we still have two
application rules and there are some types being guessed. Thus, in order to find a non-backtracking
algorithmic formulation, we must overcome these two problems first. To do so, it is helpful toanalyse the root cause of backtracking. For this we first identify when we need to use DApp1
and DApp2. Let us consider two special cases in an application 𝑒 1 𝑒 2 : the function 𝑒 1 is a lambda
abstraction 𝜆𝑥 . 𝑒; or the function 𝑒 1 is a variable 𝑥. For these two cases we can clearly identify
which rule is better:Γ ⊢ (𝑆 𝑛) 𝜆𝑥 . 𝑒 : 𝐴 → 𝐵Γ ⊢0 𝑒 2 : 𝐴Γ ⊢0 𝑥 : 𝐴 → 𝐵
Γ ⊢∞ 𝑒 2 : 𝐴
DApp2

DApp1

Γ ⊢𝑛 (𝜆𝑥 . 𝑒) 𝑒 2 : 𝐵Γ ⊢0 𝑥 𝑒 2 : 𝐵
When 𝑒 1 is a lambda abstraction 𝜆𝑥 . 𝑒, DApp1 will never succeed because 𝜆𝑥 . 𝑒 is not typeable
without contextual information. Thus, the only rule that we can use in this case is DApp2 which, if
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual Typing

266:15it successfully infers a type for 𝑒 2 , can then try to infer the type for the abstraction. When 𝑒 1 isa variable 𝑥 it is not too difficult to see that DApp1 is always a better rule to use, since the typeof variables can always be inferred. So using DApp1 instead of DApp2 will lead to strictly more
successful typing derivations. One other case that is similar to variables is when 𝑒 1 is an annotation
expression 𝑒 : 𝐴. In this case, DApp1 is also the best choice. For the cases that we have analysed it
seems that we can pick the best application rule, based on the syntactic structure of 𝑒 1 . This is true,
but 𝑒 1 can, in the general case, have more complex shapes, and those have to be dealt with as well.
Application consumer. An application consumer is either a variable, a lambda or an annotatedterm. The three cases in an application consumer capture the three cases that we analysed so far.
For an application 𝑒 1 𝑒 2 what we are looking for is the application consumer for 𝑒 2 . That is, the termthat will eventually consume the contextual information for the argument. In direct applications,such as (𝜆𝑥 . 𝑥) 𝑒 2 , the application consumer is just 𝑒 1 (𝜆𝑥 . 𝑥 in this case). In the general case theconsumer may lie deep within 𝑒 1 . Consider the application ((𝜆𝑥 . 𝑦) 1) (𝜆𝑧. 𝑧). Here 𝑦 is a variable,with the type (𝐼 → 𝐼 ) → 𝐼 in the typing environment. Note that this term is typeable if we use
DApp1 for the outer application and DApp2 for the inner application. In this case 𝑦 is the consumer
that determines which application rule to use to type check the outer application (for the argument
𝜆𝑧. 𝑧). We should choose DApp1, since the application consumer is a variable (𝑦). Conversely, for the
inner application we should use DApp2 since the application consumer is 𝜆𝑥 . 𝑦. A second exampleis (𝜆𝑥 . 𝜆𝑦. 𝑥 + 𝑦) 1 2, where the consumer for 2 is 𝜆𝑦. 𝑥 + 𝑦 and the consumer for 1 is (𝜆𝑥 . 𝜆𝑦. 𝑥 + 𝑦).
To design an efficient algorithm the notion of application consumer is useful, since the consumer
determines the best application rule to use. Therefore, once we know what is the best rule, we do
not need to try any other rules. A backtracking algorithm does not attempt to choose the best rule
to apply. Instead, it simply blindly tries each rule and, if some rule fails, it tries another one. To
find the best rule to apply, one possibility is to analyse the structure of the application to decide
which rule to apply. In other words we could look into an application 𝑒 1 𝑒 2 and find the consumer
for 𝑒 2 . Then, using the information about the consumer, we could decide which rule use in theapplication. Nonetheless this approach still requires us to do multiple traversals on 𝑒 1 : traversing
𝑒 1 to determine the syntactic form of the application consumer; and traversing 𝑒 1 again to actuallytype check the application. However, it is possible to do better, and traverse 𝑒 1 only one time.
4.2

Key Idea: Teleporting Typing Judgements

Knowing about the syntactic form of the application consumer determines what application rule
is best to use, but it does not determine whether typing will be successful or not. For instance,
we could have the ill-typed application (𝜆𝑥 . 𝑥 + 1) true, for which we could determine thatthe best rule to use is DApp2, but typing would nonetheless fail. The key idea in our algorithm
is to bring the arguments and the corresponding application consumer together, so that once
we find the consumer, we immediately check whether the application succeeds or not. To dothis, in an application 𝑒 1 𝑒 2 , we delay the typing of 𝑒 2 until we encounter the application consumer in the typing derivation. To visualize this idea consider the following (pseudo) derivation:...

Γ, 𝑥 : 𝐼, 𝑦 : 𝐼 ⊢ 2 : 𝐼

Γ, 𝑥 : 𝐼 ⊢ 𝜆𝑦. 𝑥 + 𝑦 : 𝐼 → 𝐼

Lam

Γ, 𝑥 : 𝐼 ⊢ 1 : 𝐼Γ ⊢ 𝜆𝑥 . 𝜆𝑦. 𝑥 + 𝑦 : 𝐼 → 𝐼 → 𝐼Γ ⊢ (𝜆𝑥 . 𝜆𝑦. 𝑥 + 𝑦) 1 : 𝐼 → 𝐼

Lam

Γ⊢1:𝐼

App

Γ⊢2:𝐼

App

Γ ⊢ ((𝜆𝑥 . 𝜆𝑦. 𝑥 + 𝑦) 1) 2 : 𝐼
Normally, when encountering an application 𝑒 1 𝑒 2 , we would attempt to check the typing of 𝑒 2
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:16

Xu Xue and Bruno C. d. S. Oliveira

𝐴, 𝐵, 𝐶, 𝐷 ::= Int | 𝐴 → 𝐵

Types
Expressions

𝑒 ::= 𝑖 | 𝑥 | 𝜆𝑥 . 𝑒 | 𝑒 1 𝑒 2 | 𝑒 : 𝐴

Typing EnvironmentsΓ ::= · | Γ, 𝑥 : 𝐴

Surrounding Contexts

Σ ::= □ | 𝐴 | 𝑒 ↦→ Σ

Generic Consumers

𝑔 ::= 𝑖 | 𝑥 | 𝑒 : 𝐴

Fig. 8. Syntax for the algorithmic type system.

directly in a premise of the application rule for 𝑒 1 𝑒 2 . Instead, what we want is to transport thetyping premise for 𝑒 2 into the rule that deals with the application consumer. We call this process ofmoving the typing premise for 𝑒 2 into the application consumer teleportation. For instance, in thederivation above, we teleport Γ ⊢ 2 : 𝐼 into a premise of the corresponding consumer 𝜆𝑦. 𝑥 + 𝑦.
Similarly, we teleport the typing premise Γ ⊢ 1 : 𝐼 into a premise of 𝜆𝑥 . 𝜆𝑦. 𝑥 + 𝑦.
Teleportation also works for the other 2 types of application consumers: variables and annotatedexpressions. In the algorithm shown next, this idea can be implemented by having an auxiliary
form of context, which captures the surrounding context of an expression.
4.3

Algorithmic Type System

Syntax. The algorithmic type system shares the same syntax of types, expressions and typing
environments as the QTAS in Section 3.4. The differences are two more syntactic categories:
surrounding contexts and generic consumers. The full syntax is shown in Fig. 8. A surrounding
context (or context for short) captures the information that is in context for the current expression.
A surrounding context can be empty (□), which means that the context provides no information.
A context can be a full type 𝐴, which comes from type annotations, or known type information.
More interestingly, a context can also be a sequence of expressions 𝑒, which denote arguments
to applications, followed by more contextual information. Intuitively, expressions in the context
represent deferred type checking tasks of applications, to be carried out when the application
consumer is found in the derivation.
As we have seen in Section 4.1 an important concept is the notion of application consumers.
Application consumers consume contextual information, and are especially interesting because,in particular, they consume the contextual information about application arguments. However,any expression can be a consumer of contextual information, since contextual information canalso be type information coming from type annotations. For instance, in the annotated expression
1 : Int, the surrounding context of 1 is Int, and 1 would consume that contextual type information.
Notice though, that it does not make sense for 1 to consume argument information, since 1 cannot
be applied (thus 1 is not an application consumer). Some kinds of expressions/consumers needto handle contextual information in a special way, but some other expressions handle contextual
information in a generic way, via the subsumption rule. We call such expressions generic consumers.
Generic consumers in our calculus are integers, annotated expressions and variables.
Surrounding context and elimination forms. An important question that a language designer may
ask at this point is: how do we determine the information that needs to be tracked in the surrounding
context in the general case? While in the previous section we have already motivated the needfor tracking arguments of applications, what if we extend the language with new constructs? A
general answer to this question is that we need to look at elimination forms. In the STLC there is
only one elimination form: applications 𝑒 1 𝑒 2 . The arguments of applications provide informationthat is helpful for the application consumers, which include the corresponding introduction form
(lambdas), as well as variables and annotations. The information from the arguments can thenProc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual TypingΓ ⊢Σ⇒𝑒 ⇒𝐴Γ ⊢ □ ⇒ 𝑖 ⇒ Int

266:17(Typing: under environment Γ and context Σ, expression 𝑒 infers type 𝐴.)
𝑥 :𝐴∈Γ

ALitΓ⊢□⇒𝑥 ⇒𝐴Γ ⊢ 𝑒 2 ↦→ Σ ⇒ 𝑒 1 ⇒ 𝐴 → 𝐵

Γ, 𝑥 : 𝐴 ⊢ 𝐵 ⇒ 𝑒 ⇒ 𝐶
Γ ⊢ 𝐴 → 𝐵 ⇒ 𝜆𝑥 . 𝑒 ⇒ 𝐴 → 𝐶

Γ, 𝑥 : 𝐴 ⊢ Σ ⇒ 𝑒 ⇒ 𝐵Γ ⊢ 𝑒 2 ↦→ Σ ⇒ 𝜆𝑥 . 𝑒 ⇒ 𝐴 → 𝐵

ALam1

Γ ⊢□⇒𝑔 ⇒𝐴

Σ≠□

𝐴≈Σ

Γ ⊢ Σ⇒𝑔 ⇒𝐴

ALam2

ASub

(Matching: under environment Γ, type 𝐴 is matched by context Σ.)

Γ⊢𝐴≈Σ
Γ⊢𝐴≈□

AAnn

Γ ⊢□⇒𝑒 :𝐴⇒𝐴Γ ⊢ □ ⇒ 𝑒2 ⇒ 𝐴AAppΓ ⊢ Σ ⇒ 𝑒1 𝑒2 ⇒ 𝐵

Γ ⊢𝐴⇒𝑒 ⇒𝐵

AVar

SubEmpty

Γ⊢𝐴≈𝐴

SubTypeΓ ⊢𝐴 ⇒𝑒 ⇒𝐶Γ⊢𝐵≈ΣΓ ⊢ 𝐴 → 𝐵 ≈ 𝑒 ↦→ Σ

SubTerm

Fig. 9. Algorithmic typing and matching for the STLC.

provide the consumers with enough type information for checking typeability. Thus we need toanalyse the elimination forms in the language and identify the information that is needed for aiding
the consumers to establish typeability. Section 5 shows how this idea extends to record projections.
Typing. We show the full rules for algorithmic typing in Fig. 9. Typing has the form Γ ⊢ Σ ⇒𝑒 ⇒ 𝐴, which is interpreted as: under typing environment Γ and a surrounding context Σ, theexpression 𝑒 infers the type 𝐴. Under this interpretation Γ, Σ and 𝑒 are inputs, and the type 𝐴 is an
output, determined by the three input parameters of the typing relation.
We can group rules ALit, AVar and AAnn together: they all infer the type without needing any
contextual information. Note that these rules cover all the generic consumer expressions. The
empty surrounding context □ expresses that no contextual information is needed. ALit and AVar
are unsurprising. AAnn infers the type 𝐴 from its annotation and the 𝐴 will become surrounding
context information to infer the expression 𝑒.
There is a single rule for applications, unlike in the QTAS. Rule AApp simply adds the argument𝑒 2 to the surrounding context Σ. Using this extended context we then infer 𝑒 1 ’s type, and obtainthe function type 𝐴 → 𝐵. The type 𝐵 will be the result type of the application 𝑒 1 𝑒 2 . Conversely, we
now have two rules for lambda expressions, unlike the QTAS, which has a single rule. Rules ALam1
and ALam2 cover two cases when inferring the type of a lambda expression. The first case (ruleALam1) is that the context is a type 𝐴 → 𝐵, which means that the lambda is fully annotated. We
use the type 𝐴 as the type of bound variable 𝑥 and add 𝐵 to the context to help infer the lambda
body. After we obtain the type 𝐶, we then infer the type 𝐴 → 𝐶. The second case (rule ALam2) iswhen the first entry in the context is an argument expression 𝑒 2 . In this case, we infer the type of𝑒 2 and obtain the type 𝐴. The type 𝐴 is used as the type for the lambda variable 𝑥, and we further
infer the type lambda body with the context Σ. Once we get the type 𝐵, the final inference result
for the lambda expression is 𝐴 → 𝐵. Importantly, note that the two rules do not overlap since thesyntactic form for the context is different. So the rules are syntax-directed.
Subsumption and the matching judgment. The subsumption rule ASub accounts for genericconsumers when their surrounding context is not empty (Σ ≠ □). We first infer their types with theempty context and put the type 𝐴 into a new matching judgment Γ ⊢ 𝐴 ≈ Σ that matches the type
𝐴 with Σ. Subsumption does not deal with applications and lambda expressions, since the rulesthat cover those expressions already deal with the cases when the context is not empty.
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:18

Xu Xue and Bruno C. d. S. Oliveira

The matching judgment checks whether the type inferred in the subsumption premise matches
up with the surrounding context. The rules for this judgment are defined by the structure ofcontexts. SubEmpty states that an empty context matches any type 𝐴. SubType states that a full
type in a context matches type 𝐴 when they are the same (syntactic) type. The most interesting ruleis SubTerm, which matches a function type with an application argument followed by a context: 𝑒
can be typed when the argument 𝑒 has the input type 𝐴, and the output type 𝐵 matches the context
Σ. SubTerm shows that our typing and matching relations are mutually dependent, which adds somecomplexity to the algorithmic metatheory: related properties often need to be mutually proved.
Interestingly, the typing premises for arguments in DApp1, and DApp2 correspond, respectively, tothe typing premise of SubTerm and the first typing premise of ALam2. This observation is key toestablishing the equivalence between the QTAS and the algorithmic system.
Metatheory. Algorithmic typing has the following properties.
Lemma 4.1 (Typing Implies Matching). If Γ ⊢ Σ ⇒ 𝑒 ⇒ 𝐴, then Γ ⊢ 𝐴 ≈ Σ.
This property guarantees that all our typing rules have an invariant that the inferred typematches the context. This gives rise to the following corollary.
Corollary 4.2 (A full type context infers the same type). If Γ ⊢ 𝐴 ⇒ 𝑒 ⇒ 𝐵, then 𝐴 = 𝐵.
ASub has several restrictions to avoid overlapping, but a general form of subsumption that works
for any expression is derivable. This lemma is proved with a generalization, that is proved together
with Lemma 4.1 by induction on typing.
Lemma 4.3 (General Subsumption). If Γ ⊢ □ ⇒ 𝑒 ⇒ 𝐴 and Γ ⊢ 𝐴 ≈ Σ, then Γ ⊢ Σ ⇒ 𝑒 ⇒ 𝐴.
Lemma 4.4 (Decidability of Matching). Γ ⊢ 𝐴 ≈ Σ is decidable.
Lemma 4.5 (Decidability of Typing). Γ ⊢ Σ ⇒ 𝑒 ⇒ 𝐴 is decidable.
The decidability of matching and typing is proved simultaneously. The measure used for typing
is size(Σ) + size(𝑒), and the measure for matching is size(Σ). Note that the size of context Σ isdefined in terms of the size of expressions. The definition of size(Σ) is:size(□) = 0

size(𝐴) = 0 size( 𝑒 ↦→ Σ) = 1 + size(𝑒) + size(Σ)

and the definition of size(𝑒) is:size(𝑖) = 1 size(𝑥) = 1 size(𝜆𝑥 . 𝑒) = 1 + size(𝑒)size(𝑒 1 𝑒 2 ) = 2 + size(𝑒 1 ) + size(𝑒 2 ) size(𝑒 : 𝐴) = 1 + size(𝑒)4.4Soundness and Completeness to the QTAS

Algorithmic typing is equivalent (sound and complete) to the corresponding QTAS in Fig. 5.
Soundness. Informally, the approach to achieve soundness is to extract all arguments (¯𝑒) from the¯ we then assert
context Σ and apply them back to 𝑒. After building an application expression 𝑒 𝑒,that this constructed expression is well-typed in the QTAS. The general lemma that is needed toprove soundness is shown in the appendix. For space reasons, here we just show key results, which
are corollaries of the general soundness lemma.
Corollary 4.6 (Soundness of Typing).
• If Γ ⊢ □ ⇒ 𝑒 ⇒ 𝐴, then Γ ⊢0 𝑒 : 𝐴.

• If Γ ⊢ 𝐴 ⇒ 𝑒 ⇒ 𝐵, then Γ ⊢∞ 𝑒 : 𝐴.

Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual TypingTypes

266:19𝐴, 𝐵, 𝐶, 𝐷 ::= Int | Float | Top | 𝐴 → 𝐵 | 𝐴 & 𝐵 | {𝑎 : 𝐴}

Constants

𝑐 ::= 𝑖 | 𝑢 | + | +𝑖 | +𝑢

Expressions

𝑒 ::= 𝑐 | 𝑥 | 𝜆𝑥 . 𝑒 | 𝑒 1 𝑒 2 | 𝑒 : 𝐴 | {𝑎 = 𝑒} | 𝑒.𝑎

EnvironmentsΓ ::= . | Γ, 𝑥 : 𝐴

Check Counters𝑚 ::= 0 | ∞ | 𝑆𝑐 𝑚 | 𝑆𝑎 𝑚

Counters

𝑛 ::= 𝑚 | 𝑆𝑖 𝑛

Generic Consumers

𝑔 ::= 𝑐 | 𝑥 | 𝑒 : 𝐴 | {𝑎 = 𝑒}Surrounding Contexts

Σ ::= □ | 𝐴 | 𝑒 ↦→ Σ | 𝑎 ↦→ Σ
Fig. 10. Syntax of 𝐶 & .

Completeness. Compared with soundness, completeness is easier to prove. We also need an
auxiliary relation that relates counters and a context Σ. We only show the key results here in theform of corollaries. The generalized completeness theorem can be found in the appendix.
Corollary 4.7 (Completeness of Typing).
• If Γ ⊢0 𝑒 : 𝐴, then Γ ⊢ □ ⇒ 𝑒 ⇒ 𝐴. • If Γ ⊢∞ 𝑒 : 𝐴, then Γ ⊢ 𝐴 ⇒ 𝑒 ⇒ 𝐴.
5

A Calculus with Intersection Types, Overloading and Records

In this section, we present the contextual intersection calculus 𝐶 & . 𝐶 & features subtyping, intersection types, a simple form of overloading, and records. The QTAS and algorithmic typing of 𝐶 &is formalized, and their soundness and completeness are proved. The main purpose of 𝐶 & is toshow how contextual typing can scale up to more complex calculi, and deal with subtyping. We
also illustrate that record labels can be another form of contextual information, helpful to aid with
type inference of record projections. Additionally, we show that, with more variety of contextual
information, counters are enriched to qualify the different kinds of contextual information.
5.1

SyntaxTypes and Expressions. The syntax of 𝐶 & is shown in Fig. 10. Four new types are introduced into
𝐶 & : a Float type; a Top type, which is the supertype of all types; intersection types 𝐴 & 𝐵; andsingle field records {𝑎 : 𝐴}. Multi-field record types are encoded using top, intersection and single
field record types [Reynolds 1997]:{} ≜ Top{𝑎 1 : 𝐴1, . . . , 𝑎𝑖 : 𝐴𝑖 } ≜ {𝑎 1 : 𝐴1 } & . . . & {𝑎𝑖 : 𝐴𝑖 }In expressions, we separate out all constants into a new category: 𝑖 is an integer and 𝑢 is a floating
point number. The overloaded addition + can work on integers and floats. Furthermore, +𝑖 and +𝑢are two specialized partially applied additions that work only on integers and floats respectively.
Two more new constructs are records, which are constructed by a sequence of labels 𝑎 bound to
expressions 𝑒, and record projection 𝑒.𝑎. We define a metafunction ⟦𝑐⟧ that maps constants to
types. Note that we use 𝐼 and 𝐹 as abbreviations for Int and Float, respectively.
⟦𝑖⟧ = 𝐼 ⟦𝑢⟧ = 𝐹 ⟦+⟧ = (𝐼 → 𝐼 → 𝐼 ) & (𝐹 → 𝐹 → 𝐹 ) ⟦+𝑖 ⟧ = 𝐼 → 𝐼 ⟦+𝑢 ⟧ = 𝐹 → 𝐹
Qualifying counters. To account for the richer form of contextual information in the calculus, weuse a richer formulation of counters. Instead of a single successor used in the counters in Section 3,
we have three, more refined, forms of successors: 𝑆𝑖 , 𝑆𝑐 and 𝑆𝑎 . 𝑆𝑖 counts the availability of inferable
argument types (and the uses of CDApp2), and is the closest to the successor used in Section 3.4.
The successor counter (𝑆𝑎 ) counts labels, which are helpful to aid with the inference of types for
projections and provides a distinct use of counters. In addition, we introduce an extra counter 𝑆𝑐
that counts the number of arguments that check against a type (and the uses of CDApp1). Tracking
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:20

Xu Xue and Bruno C. d. S. Oliveira

checkable arguments is important because subtyping exploits information about arguments thatcan be checked: the subtyping derivations will depend on the arguments in the context.
One useful observation here is that there is a mismatch between the syntax of counters andcontexts in the STLC calculus. The QTAS counts the needed contextual information for inferable
arguments; while contexts store all possible arguments, whether they are inferable or not. For our
STLC calculus this mismatch does not matter, so we do not need to track checkable arguments. In
𝐶 & we need to be more precise and track checkable arguments, and there is a closer correspondence
between counters and contexts.
Note that in 𝐶 & a well-formed counter is wrapped around check counters. This exposes aninteresting structure in applications with multiple arguments 𝑓 𝑒 1 𝑒 2 . . . 𝑒𝑛 . The inference result of
inner arguments can assist the inference of function 𝑓 ’s type, and checking outer arguments. In
other words, the general structure of an application is of the form 𝑓 𝑖 𝑐 where 𝑖 denotes a sequence ofinferable arguments, and 𝑐 denotes a sequence of checkable arguments. For example, (𝜆𝑥 . ((𝜆𝑓 . 𝑓 𝑥) :(𝐼 → 𝐼 ) → 𝐼 )) 1 (𝜆𝑥 . 𝑥) type checks, since the first argument 1 is inferable and helps inferring thetype for the corresponding lambda application consumer. Then the second argument (𝜆𝑥 . 𝑥) can bechecked with 𝐼 → 𝐼 . However, if we swap the two arguments, (𝜆𝑓 . ((𝜆𝑥 . 𝑓 𝑥) : (𝐼 → 𝐼 ))) (𝜆𝑥 . 𝑥) 1
does not type-check since 𝜆𝑥 . 𝑥 is not inferable and cannot help inferring the corresponding lambda
application consumer. Note also, that all inferable arguments are checkable. Therefore an applicationsuch as 𝑓 1 (𝜆𝑥 . 𝑥) 2 can be interpreted as being of the form 𝑓 𝑖 𝑐 𝑐. Any 𝑓 𝑖 𝑐 𝑖 expressions are also
𝑓 𝑖 𝑐 𝑐 expressions: we can always check inferable arguments. Once we encounter an argument thatmust be checked, then all subsequent arguments can be checked. We need to apply (C)DApp1, which
provides enough information to check all subsequent arguments. Interestingly, similar structuresappear in applications for approaches based on local type inference [Pierce and Turner 2000].
To conclude, in 𝐶 & counters have a broader role, and they do not only quantify, but they also
qualify available contextual type information. In 𝐶 & counters can be interpreted as a kind of maskthat classifies what each piece of contextual information in the surrounding context is.
Surrounding Contexts. Compared with the changes in counters, there is only one small change
in contexts. We allow labels in contexts: 𝑎 ↦→ Σ is a label followed by a context. In 𝐶 & there is a
new elimination form: record projections 𝑒.𝑎. Thus, as described in Section 4.3, we need to identify
the information from the elimination form that is helpful for the corresponding consumers, which
includes record expressions (the introduction form), as well as variables and annotated expressions.
For projections, labels are the information that is needed to help the consumers establish typeability.
Thus labels are now also tracked in the context. Note also that in 𝐶 & we now achieve a close match
between counters and contexts. For example, 𝑆𝑖 𝑆𝑐 𝑆𝑎 0 matches 𝑒 1 ↦→ 𝑒 2 ↦→ 𝑎 1 ↦→ □, where 𝑒 1
infers and 𝑒 2 checks during typing.
5.2

QTAS: Typing and Subtyping

Typing. The QTAS for 𝐶 & is shown at the top of Fig. 11. The 𝑛− meta-operation is the same as
the first calculus. CDApp1 and CDApp2 account for the two application rules. Rule CDApp1 tracks
one more counter. As before, we check whether 𝑒 2 has the type 𝐴 with full contextual information.
Differently to previous QTASs, function 𝑒 1 has the arrow type 𝐴 → 𝐵 with the incremented counter
𝑆𝑐 𝑚 to denote the availability of one additional checkable argument. This information is helpful forsubsumption. In the CDLam rule it is important to note that the decrement function is only definedfor ∞ and 𝑆𝑖 𝑛, since the type of the argument must be known.
CDRcd deals with the introduction of records and requires some explanation. One may expectthat expressions like {𝑎 = 𝜆𝑥 . 𝑥 }.𝑎 1 are typeable, by propagating the surrounding context (with1), into the lambda. However, consider {𝑎 1 = 1, 𝑎 2 = 𝜆𝑥 . 𝑥 }.𝑎 1 . We expect that this expression has
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual Typing

266:21Γ ⊢𝑛 𝑒 : 𝐴(Under Γ, expression 𝑒 needs 𝑛 contextual information to have type 𝐴.)

CDConst

CDVar

CDAnn

CDLam

Γ ⊢0 𝑥 : 𝐴Γ ⊢0 (𝑒 : 𝐴) : 𝐴Γ ⊢𝑛 𝜆𝑥 . 𝑒 : 𝐴 → 𝐵

𝑥 :𝐴∈Γ

Γ ⊢0 𝑐 : ⟦𝑐⟧Γ ⊢∞ 𝑒 : 𝐴

Γ, 𝑥 : 𝐴 ⊢𝑛− 𝑒 : 𝐵

CDApp2

CDApp1Γ ⊢ (𝑆𝑐 𝑚) 𝑒 1 : 𝐴 → 𝐵

Γ ⊢ (𝑆𝑖 𝑛) 𝑒 1 : 𝐴 → 𝐵

Γ ⊢∞ 𝑒 2 : 𝐴Γ ⊢𝑚 𝑒 1 𝑒 2 : 𝐵Γ ⊢𝑛 𝑒 1 𝑒 2 : 𝐵
CDRcd

CDSub

Γ ⊢0 𝑒 : 𝐴𝑛≠0

Γ ⊢0 𝑒 2 : 𝐴
CDPrj

Γ ⊢0 𝑒𝑖 : 𝐴𝑖

𝐴 <:𝑛 𝐵Γ ⊢𝑛 𝑒 : 𝐵Γ ⊢ (𝑆𝑎 𝑚) 𝑒 : {𝑎 : 𝐴}

Γ ⊢0 {𝑎𝑖 = 𝑒𝑖 } : {𝑎𝑖 : 𝐴𝑖 }Γ ⊢𝑚 𝑒.𝑎 : 𝐴(𝐴 is a subtype of 𝐵 and 𝑛 contextual information is known for 𝐵.)

𝐴 <:𝑛 𝐵
CDSReflCDSInt

CDSFloat

CDSTop𝐴 <:0 𝐴

Int <:∞ Int

Float <:∞ Float

𝐴 <:∞ Top

CDSAndL

CDSRcd𝐴 <:𝑛 𝐶𝐴 <:𝑚⊖ 𝐵{𝑎 : 𝐴} <:𝑚 {𝑎 : 𝐵}

CDSAndR𝑛≠0

𝐵 <:𝑛 𝐶𝐴 & 𝐵 <:𝑛 𝐶

CDSArr𝐶 <:∞ 𝐴𝐵 <:𝑛⊖ 𝐷

𝐴 → 𝐵 <:𝑛 𝐶 → 𝐷
CDSAnd𝑛≠0

𝐴 <:∞ 𝐵

𝐴 & 𝐵 <:𝑛 𝐶

𝐴 <:∞ 𝐶𝐴 <:∞ 𝐵 & 𝐶

Fig. 11. QTAS typing and subtyping for 𝐶 & .

type Int, but we cannot type 𝑎 2 under any surrounding context: it is not possible to propagate
contextual information to 𝑎 2 . A similar situation happens with {𝑎 1 = 1, 𝑎 2 = 𝜆𝑥 . 𝑥 } : {𝑎 1 : Int},
where a record expression may be checked against a type that has fewer fields than the record
expression itself. Both of these bring up the question of what to do for the expressions in the fields
for which there is no contextual information (such as 𝑎 2 ). To avoid this problem we require that
all fields must have inferable types in CDRcd. An alternative approach could be to employ a mixed
strategy where the fields that are present in the type/context are checked, and the fields that are
missing require inference. But this approach is more complex (although it can be algorithmicallymodeled) and seems ad-hoc. Thus we opt for the simpler approach of requiring all record fields tohave inferred types.
For projections (rule CDPrj), we take the same strategy as App1. We increment the counterand delegate the job of label selection to subsumption. Thus, our typing relation does not require
auxiliary relations for dealing with projections and applications. In the subsumption rule CDSub,
we introduce subtyping. Interestingly, subtyping is also parametrized by a counter, enabling it todeal with contextual type information.
To illustrate how typing works, consider an example with overloaded addition. We omit thederivation of subtyping, which will be detailed later.
Γ ⊢0 + : (𝐼 → 𝐼 → 𝐼 ) & (𝐹 → 𝐹 → 𝐹 )CDConst...

Γ ⊢ (𝑆𝑐 𝑆𝑐 0) + : 𝐼 → 𝐼 → 𝐼Γ ⊢ (𝑆𝑐 0) + 1 : 𝐼 → 𝐼Γ ⊢0 + 1 2 : 𝐼

CDSubΓ ⊢∞ 1 : 𝐼

CDApp1Γ ⊢∞ 2 : 𝐼

CDApp1

When applying + to two integers, the counter will be incremented twice by the successor 𝑆𝑐 , whichtells that two arguments are needed. With additional contextual information, the type of + can be
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:22

Xu Xue and Bruno C. d. S. Oliveira

upcast to a function type via the subsumption rule which, in this case, is 𝐼 → 𝐼 → 𝐼 . Projections
are dealt with similarly. For example, assuming 𝑟 : {𝑥 : Int, 𝑦 : Float}, then 𝑟 .𝑥 infers Int.
Subtyping. Unlike conventional subtyping relations, our QTAS subtyping, shown at the bottomof Fig. 11, also carries a counter. The counter 𝑛 expresses how much contextual information is
known for 𝐵, whereas 𝐴 is fully known. CDSRefl describes the situation when the counter is 0,
which means that we have no information for 𝐵. In this case we pick type 𝐴 for the supertype. If
the counter is ∞, then we know everything about type 𝐵, corresponding to traditional subtyping.
CDSInt and CDSFloat are unsurprising and describe reflexivity for the two base types. CDSTop is
also standard. The rule CDSArr is interesting since it can deal with partially known information
about 𝐵. Note that 𝑛 cannot be 0, since it needs to be decreasable:(𝑆𝑖 𝑛)⊖ = 𝑛 ∞⊖ = ∞ (𝑆𝑐 𝑚)⊖ = 𝑚 (𝑆𝑎 𝑚)⊖ = 𝑚
Thus 𝐶 is known. In the first premise, since both 𝐴 and 𝐶 are known, the counter is set to ∞. For thesecond premise, which performs subtyping for the output types, we decrease the counter. CDSRcd
works similarly to CDSArr: the label information must be known for the supertype, although thetype of the field may or may not be known. The rules CDSAndL and CDSAndR are standard forintersection types if we ignore counter information. The counters express that we can have all orjust partial information for 𝐶. Interestingly, for CDSAnd, all the information for the supertype must
be known. Thus, the rule is just the standard rule when an intersection appears in the supertype.
We continue our example, to illustrate how the derivation of subtyping proceeds in subsumption.
CDSIntCDSInt𝐼 <:∞ 𝐼𝐼 <:∞ 𝐼CDSRefl𝐼 <:0 𝐼

(𝐼 → 𝐼 ) <: (𝑆𝑐 0) (𝐼 → 𝐼 )CDSArr(𝐼 → 𝐼 → 𝐼 ) <: (𝑆𝑐 𝑆𝑐 0) (𝐼 → 𝐼 → 𝐼 )(𝐼 → 𝐼 → 𝐼 ) & (𝐹 → 𝐹 → 𝐹 ) <: (𝑆𝑐 𝑆𝑐 0) (𝐼 → 𝐼 → 𝐼 )CDSArrCDSAndL

Metatheory. QTAS subtyping has following properties:
Lemma 5.1 (Reflexivity of Subtyping (Infinity)). 𝐴 <:∞ 𝐴
Lemma 5.2 (Transitivity of Subtyping). If 𝐴 <:𝑛 𝐵 and 𝐵 <:𝑛 𝐶, then 𝐴 <:𝑛 𝐶.
5.3 Algorithmic Typing and Subtyping
Algorithmic typing. We present the rules of algorithmic typing at the top of Fig. 12. Many rules are
the same as the type system in Section 4.3. For records, similarly to the QTAS in Fig. 11, CARcd deals
with the introduction of records. For a record projection 𝑒.𝑎 (rule CAPrj), we push the label 𝑎 into
the context and infer the expression 𝑒 with the single field record type {𝑎 : 𝐴}. CASub is interestingsince subtyping needs to deal with contextual information. Unlike conventional subtyping, which
compares two types, our contextual subtyping relation compares a type with a surrounding context,
which has partial information about the supertype. While comparing the type with the context, we
compute a supertype that matches the information in the context.
Algorithmic contextual subtyping. Algorithmic subtyping is presented at the bottom of Fig. 12. Γ,
𝐴 and Σ are taken as inputs and 𝐵 is an output. We group CASInt, CASTop, CASArr, CASRcd and
CASAnd together, since they cover the same situation where contexts are fully known types. In
those cases the computed supertype is exactly the type in the context. Rule CASArr is standard,
except for the additional computed types. The computed types in the premises are ignored since
the full supertype is already known. CASAnd and CASRcd are also quite standard and work similarly
to CASArr. In CASEmpty the computed supertype is 𝐴. In CASTerm, an arrow type is the subtype of aProc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual Typing

266:23Γ ⊢Σ⇒𝑒 ⇒𝐴Γ ⊢ □ ⇒ 𝑐 ⇒ ⟦𝑐⟧(Under environment Γ and context Σ, expression 𝑒 infers type 𝐴.)
𝑥 :𝐴∈Γ

CAConstΓ⊢□⇒𝑥 ⇒𝐴Γ ⊢ 𝑒 2 ↦→ Σ ⇒ 𝑒 1 ⇒ 𝐴 → 𝐵Γ ⊢ □ ⇒ 𝑒𝑖 ⇒ 𝐴𝑖
Γ ⊢ □ ⇒ {𝑎𝑖 = 𝑒𝑖 } ⇒ {𝑎𝑖 : 𝐴𝑖 }
Γ ⊢𝐴⇒𝑒 ⇒𝐵Γ ⊢□⇒𝑒 :𝐴⇒𝐴Γ ⊢ 𝐴 <: Σ ⇝ 𝐵
Γ ⊢ Int <: Int ⇝ Int

Γ, 𝑥 : 𝐴 ⊢ Σ ⇒ 𝑒 ⇒ 𝐵

Σ≠□

CAPrj

CALam1Γ ⊢ 𝑒 2 ↦→ Σ ⇒ 𝜆𝑥 . 𝑒 ⇒ 𝐴 → 𝐵

Γ ⊢□⇒𝑔 ⇒𝐴Γ ⊢ 𝐴 <: Σ ⇝ 𝐵

CALam2CASubΓ ⊢ Σ⇒𝑔 ⇒𝐵(Under environment Γ, A matches the context Σ and is a subtype of 𝐵.)
CASIntCASFloatΓ ⊢ 𝐵 <: Σ ⇝ 𝐷

Γ ⊢ 𝐴 <: Σ ⇝ 𝐶
Γ ⊢ {𝑎 : 𝐴} <: 𝑎 ↦→ Σ ⇝ {𝑎 : 𝐶}Σ≠□Γ ⊢ 𝐴 & 𝐵 <: Σ ⇝ 𝐶

CASTopΓ ⊢ 𝐴 <: □ ⇝ 𝐴

Γ ⊢ 𝐶 <: 𝐴 ⇝ 𝐴′Γ ⊢ 𝐵 <: 𝐷 ⇝ 𝐷 ′Γ ⊢ 𝐴 <: Top ⇝ TopΓ ⊢ 𝐴 → 𝐵 <: 𝑒 ↦→ Σ ⇝ 𝐴 → 𝐷

Γ ⊢ 𝐵 <: Σ ⇝ 𝐶

Γ ⊢ 𝐴 → 𝐵 ⇒ 𝜆𝑥 . 𝑒 ⇒ 𝐴 → 𝐶Γ ⊢ □ ⇒ 𝑒2 ⇒ 𝐴

CARcd

CAAnn

Γ ⊢ Float <: Float ⇝ FloatΓ ⊢𝐴 ⇒𝑒 ⇒𝐶Γ ⊢ Σ ⇒ 𝑒.𝑎 ⇒ 𝐴
Γ, 𝑥 : 𝐴 ⊢ 𝐵 ⇒ 𝑒 ⇒ 𝐶

CAAppΓ ⊢ Σ ⇒ 𝑒1 𝑒2 ⇒ 𝐵

Γ ⊢ 𝑎 ↦→ Σ ⇒ 𝑒 ⇒ {𝑎 : 𝐴}CAVar

CASAndRΓ ⊢ 𝐴 → 𝐵 <: 𝐶 → 𝐷 ⇝ 𝐶 → 𝐷

CASTerm

CASLabelΓ ⊢ 𝐴 <: 𝐵 ⇝ 𝐵 ′Γ ⊢ {𝑎 : 𝐴} <: {𝑎 : 𝐵} ⇝ {𝑎 : 𝐵}Γ ⊢ 𝐴 <: Σ ⇝ 𝐶Σ≠□Γ ⊢ 𝐴 & 𝐵 <: Σ ⇝ 𝐶

Γ ⊢ 𝐴 <: 𝐵 ⇝ 𝐵 ′CASEmpty

CASArr

CASRcdCASAndLΓ ⊢ 𝐴 <: 𝐶 ⇝ 𝐶 ′Γ ⊢ 𝐴 <: 𝐵 & 𝐶 ⇝ 𝐵 & 𝐶

CASAndFig. 12. Algorithmic typing and subtyping for 𝐶 & .

term 𝑒 followed by a context Σ. We use the type 𝐴 as the context for typing 𝑒, and check subtyping
between 𝐵 and Σ inductively, while computing a supertype 𝐷 for 𝐵. The computed supertype
is then 𝐴 → 𝐷. CASLabel works similarly: a record type is a subtype of a label 𝑎 followed by acontext if their labels are the same. CASAndL and SAndR describe intersection cases. If 𝐴 & 𝐵 is asubtype of the context Σ, then either 𝐴 or 𝐵 are subtypes of Σ resulting in a supertype 𝐶. Notethat backtracking is needed here: we have to try with both CASAndL and CASAndR. This is expected
since this form of backtracking is inherent to subtyping relations with intersection types.
Metatheory. Algorithmic typing and subtyping have the following properties.
Lemma 5.3 (A full type context infers the same type). If Γ ⊢ 𝐵 ⇒ 𝑒 ⇒ 𝐴, then 𝐴 = 𝐵.
Lemma 5.4 (A full type context computes the same type). If Γ ⊢ 𝐴 <: 𝐵 ⇝ 𝐶, then 𝐵 = 𝐶.
Lemma 5.5 (Typing implies Subtyping). If Γ ⊢ Σ ⇒ 𝑒 ⇒ 𝐴, then Γ ⊢ 𝐴 <: Σ ⇝ 𝐴.
Lemma 5.6 (General Subsumption of Algorithmic Typing). If Γ ⊢ □ ⇒ 𝑒 ⇒ 𝐴 and Γ ⊢ 𝐴 <:
Σ ⇝ 𝐴′ , then Γ ⊢ Σ ⇒ 𝑒 ⇒ 𝐴′ .
5.4

Key Properties

The metatheory of 𝐶 & requires significant changes, compared to the STLC calculus, because of
subtyping. Nonetheless soundness and completeness proofs employ similar strategies as the STLC
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:24

Xu Xue and Bruno C. d. S. Oliveira

calculus, with auxiliary relations relating counters to contexts. Furthermore the key corollaries arestill essentially of the same form.
Corollary 5.7 (Soundness of Typing).
• If Γ ⊢ □ ⇒ 𝑒 ⇒ 𝐴, then Γ ⊢0 𝑒 : 𝐴. • If Γ ⊢ 𝐴 ⇒ 𝑒 ⇒ 𝐵, then Γ ⊢∞ 𝑒 : 𝐴.
Corollary 5.8 (Completeness of Typing).
• If Γ ⊢0 𝑒 : 𝐴, then Γ ⊢ □ ⇒ 𝑒 ⇒ 𝐴. • If Γ ⊢∞ 𝑒 : 𝐴, then Γ ⊢ 𝐴 ⇒ 𝑒 ⇒ 𝐴.
Annotatability. One point worth mentioning about annotatability is that, for records, if the TAS
expression 𝑒 in a record field {𝑎 = 𝑒} needs contextual information, then the QTAS expression must
be annotated with its type. This is needed because records require all the fields to have inferred
types. Except for this, the annotatability guidelines remain the same as in the STLC. Note that therules for the TAS can be recovered by: 1) erasing the counter information in the rules in Fig. 11; and2) ommiting the CDAnn rule. The full elaboration rules from the TAS to the QTAS, and the extended
need function can be found in the appendix.
Theorem 5.9 (Strong Annotatability).
(1) If Γ ⊢ 𝑒 : 𝐴 ⇝ 𝑒 ′ , then Γ ⊢ (need 𝑒 ) 𝑒 ′ : 𝐴. (2) If Γ ⊢ 𝑒 : 𝐴 ⇝ 𝑒 ′ , then Γ ⊢0 (𝑒 ′ : 𝐴) : 𝐴.
Type safety. The type-safety of 𝐶 & is proved by first showing that typing is preserved between
the QTAS and the TAS. We use a simple erasure function |𝑒 | that erases all type annotations, so that
we obtain an unannotated expression that is typeable in the TAS. Then we prove that the TAS is
type sound via standard preservation and progress theorems. The small-step operational semantics
𝑒 ↩→ 𝑒 ′ is shown in the appendix.
Theorem 5.10 (Type preservation after erasure to TAS). If Γ ⊢𝑛 𝑒 : 𝐴, then Γ ⊢ |𝑒 | : 𝐴.
Theorem 5.11 (Preservation of TAS). For well-formed 𝑒, if · ⊢ 𝑒 : 𝐴 and 𝑒 ↩→ 𝑒 ′ , then · ⊢ 𝑒 ′ : 𝐴.
Theorem 5.12 (Progress of TAS). For well-formed 𝑒, if · ⊢ 𝑒 : 𝐴 , then ∃ 𝑒 ′, 𝑒 ↩→ 𝑒 ′ or 𝑒 is a value.
Determinism and decidability. Typing and subtyping are non-deterministic, without further
restrictions, due to the presence of the subtyping rules for intersection types, which are overlapping.
To recover determinism in algorithmic typing, we need to impose some additional well-formedness
conditions on environments Γ, surrounding contexts Σ, types 𝐴 and expressions 𝑒, to deal with
non-determinism caused by intersections. Well-formed intersections can either contain: record
types with distinct labels, or function types where the domains are distinct primitive types (Int andFloat). The latter restriction is sufficient to cover the form of overloading that we have in calculus,
but it is rather strict. We leave for future work relaxing the restrictions to allow more forms offunctional intersections and overloading. Under this set of restrictions we can prove determinism:
Lemma 5.13 (Determinism of Typing). For well-formed Γ, Σ and 𝑒, if Γ ⊢ Σ ⇒ 𝑒 ⇒ 𝐴 andΓ ⊢ Σ ⇒ 𝑒 ⇒ 𝐵, then 𝐴 = 𝐵.
Lemma 5.14 (Determinism of Subtyping). For well-formed Γ, Σ and 𝐴, if Γ ⊢ 𝐴 <: Σ ⇝ 𝐵 andΓ ⊢ 𝐴 <: Σ ⇝ 𝐶, then 𝐵 = 𝐶.
Furthermore, using the same restrictions we can prove the decidability of typing and subtyping:
Theorem 5.15 (Decidability of Typing). For well-formed Γ, Σ and 𝑒, Γ ⊢ Σ ⇒ 𝑒 ⇒ 𝐴 is
decidable.
Theorem 5.16 (Decidability of Subtyping). For well-formed Γ, Σ and 𝐴, Γ ⊢ 𝐴 <: Σ ⇝ 𝐵 isdecidable.
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual Typing

266:25The measure used for decidability of 𝐶 & is similar to Section 4.3. With soundness, completenessand decidability of algorithmic formulation, we can obtain the decidability of QTAS as a corollary.
Corollary 5.17 (Decidability of the QTAS). For well-formed Γ and 𝑒, Γ ⊢0 𝑒 : 𝐴 is decidable.
6

Related Work

In Section 2 we have already covered the closest related work: standard bidirectional typing [Dunfield and Krishnaswami 2021], and the let arguments go first approach [Xie and Oliveira 2018]. As
discussed in Section 3, contextual typing can be viewed as a generalization of both approaches.
In this section we focus on discussing other closely related work. Other variants of bidirectional
typing, which are further away from our work, are covered in Dunfield and Krishnaswami’s survey.
Forms of contextual typing. Xie and Oliveira’s application stack Ψ is a form of context. As wehave seen our notion of surrounding context subsumes the application stack. There are several
other works [Bierman et al. 2014; Polikarpova et al. 2016; Pottier and Régis-Gianas 2006] that
employ typing relations similar to our algorithmic typing. Typically the form of the typing relation,
adapted to our notation here, is a variant of Γ ⊢ 𝐴 ⇒ 𝑒 ⇒ 𝐵, where the context is a type 𝐴. Bierman
et al. model the type inference approach adopted by TypeScript. Their expression contextual typing
judgment fills the role of the checking mode. The judgment is used to type-check 𝑛-ary uncurried
applications and it is useful to instantiate type variables coming from the function, and to type-checkthe arguments of the function. Polikarpova et al.’s contextual type is an unrefined type, whichgets refined as more information is learned from doing inference on the subterms. Pottier andRégis-Gianas use a context that is a shape. A shape has the form 𝛼 .𝐴, where 𝛼 denotes a collectionof flexible type variables that are bound within 𝐴. A flexible type variable is similar to a unification
variable and can match with other types. In comparison to our work, we allow more forms ofcontextual type information, since we can also have term arguments or labels. Moreover, thoseworks do not have a direct correspondence to the rule DApp2 in our work.
Norell [2007] formalizes Agda’s typing. Typing has an implicit context tracking a constraint set
that is used to aid type inference. This constraint set can also be viewed as a form of contextual
typing, and is helpful to defer type checking tasks until more information is discovered. However,the constraint set is a global form of context that is updated and threaded through typing derivations.
Bidirectional typing with subtyping. Bidirectional typing has been extensively applied to typesystems with subtyping. Several bidirectional type systems with intersection types [Davies andPfenning 2000; Huang et al. 2021; Xue et al. 2022] require changes to the application rule to allow
functions to infer intersection types. An auxiliary relation is used to upcast the intersection type toa function type. Some of these works [Huang et al. 2021; Xue et al. 2022] also support distributivity
rules for subtyping and model records via intersection types, where a similar problem appears for
projections. In a projection 𝑒.𝑎 the type of 𝑒 can be an intersection of single field records. Then weneed an auxiliary relation that takes the intersection and the label and selects the corresponding
field type. Our contextual typing approach avoids changes to existing rules and specialized auxiliary
relations. Instead, subsumption and contextual subtyping deal with intersection types in a single
place. Rioux et al. [2023] also have a calculus with intersection types, but additionally support
union types and more distributivity rules for subtyping. They need a special application rule witha sophisticated auxiliary relation to deal with types of functions that can be intersection or union
types. This relation requires both the type of the function, as well as the type of the argument. So
the application rule also requires the inference of the argument, and is a variant of the App3 ruledescribed in Section 2.1. Consequently, their rule is, in some cases, weaker than DApp1 and there isProc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:26

Xu Xue and Bruno C. d. S. Oliveirano correspondence to the DApp2 rule either. While our work does not cover all the features studied
by Rioux et al., we believe that it is possible to scale up our techniques to deal with those features.
In bidirectional type systems with polymorphism [Dunfield and Krishnaswami 2013; Zhao et al.
2019], specialized auxiliary relations are also needed for applications. In this case, a function canhave a polymorphic type, which needs to be instantiated to become a function type. Then we canuse the domain of the instantiated function type to check the argument of the function. We believethat our approach can also be used in type systems with polymorphism, and avoid the need forspecialized rules and relations. However, those type systems introduce important complications. In
particular, we need to also employ a form of unification variables to aid with instantiation. Studying
the interaction between contextual typing and polymorphism is an interesting line for future work.
Spines. Application spines [Cervesato and Pfenning 2003] model the arguments of 𝑛-ary applications of the form ℎ 𝑒 1 . . . 𝑒𝑛 . Cervesato and Pfenning propose a syntactic representation of spines,
motivated by gaining efficient access to the head of an application (ℎ). The notions of a surrounding
context and application consumer in our work are closely related to the concept of an application
spine and its head, respectively. However, the structure of a surrounding context is more generalthan a spine, and the head of an application is not the same as the application consumer. For an
application 𝑒 1 𝑒 2 what we are looking for is the application consumer for 𝑒 2 . In some cases, such as
𝑥 1 2, the concept of an application head coincides with the application consumer. However, consider
the application (𝜆𝑥 . 𝑦) 1 (𝜆𝑧. 𝑧) in Section 4.1. Here 𝑦 is a variable, with the type (𝐼 → 𝐼 ) → 𝐼
in the typing context. In this case 𝑦 would be the application consumer that determines whichapplication rule to use to type check the (outer) application. But this example illustrates that theapplication consumer does not always coincide with the application head, which is 𝜆𝑥 . 𝑦 in thiscase. In addition to tracking information about applied arguments, surrounding contexts also track
known type information, which are not tracked in syntactic representations of spines.
The notion of spines has been found to be useful in type inference for languages with implicit
polymorphism [Jenkins and Stump 2018; Leijen 2008; Mercer et al. 2022; Serrano et al. 2020, 2018].
Most of these works [Leijen 2008; Mercer et al. 2022; Serrano et al. 2020, 2018], employ a syntactic
representation of spines (also called argument lists), similar to the representation proposed byCervesato and Pfenning, to assist type inference. Spine-local type inference [Jenkins and Stump
2018] also employs the concept of spines, but without requiring a syntactic representation forspines in the syntax for terms. Instead they use standard lambda calculus syntax, like in our own
work. Their typing relation employs bidirectional typing. Their rule for applications employs some
auxiliary relations that are responsible for finding the head of an application, and collect argumentsof an application spine. In addition, they also track known type information about the output typeof an application, when available. Then their typing relation is able to accept:
pair : ∀𝑋 𝑌 . 𝑋 → 𝑌 → ⟨𝑋 × 𝑌 ⟩ ⊢ pair (𝜆𝑥 . 𝑥) 1 ⇐ ⟨(Int → Int) × Int⟩
Here we want to find the implicit instantiations for 𝑋 and 𝑌 and deal with the first argument 𝜆𝑥 . 𝑥.
Because they find the type of the head (∀𝑋 𝑌 . 𝑋 → 𝑌 → ⟨𝑋 × 𝑌 ⟩) and they track the output typeof the application (⟨(Int → Int) × Int⟩), when they find the argument 𝜆𝑥 . 𝑥 they are able toconclude that 𝑋 = Int → Int, and check the lambda with that type. Unlike our work, spine-local
type inference cannot type-check terms like (𝜆𝑥 𝑦. 𝑥 + 𝑦) 1 2, and it lacks the power afforded by
the AppS rule [Xie and Oliveira 2018]. Although the output types of applications are partly tracked,
spine-local type inference also rejects programs such as ((𝜆𝑥 . 𝑥) 1) : Int, which are accepted using
rule App2. So spine-local type inference does not provide the power afforded by App2 either.
Local type inference. Local type inference [Pierce and Turner 2000] combines bidirectional typing
with local argument synthesis, to deal with implicit polymorphism. Instead of spines, local type
inference uses 𝑛-ary uncurried applications, which also gives direct access to the head of an
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual Typing

266:27application. This representation, combined with local argument synthesis, enables the instantiationof type arguments for applications. Colored local type inference [Odersky et al. 2001] is an extensionof local type inference. Like us, Odersky et al. observe that a drawback of bidirectional typing
is that it cannot exploit partial type information. To address this limitation they propose coloredtypes, in which types are annotated with two propagation directions: inherited; or synthesized. An
inherited type is a known type, and should be propagated downwards the AST. A synthesized type,on the other hand, must be propagated upwards the AST, after some information about the type is
discovered. From a bidirectional typing perspective, checked types are types that are fully inherited,
whereas inferred types are types that are fully synthesized. Colored types enable types where some
portions are inherited and others synthesized. Nonetheless, this adds complexity in the syntax oftypes, since all types need to be annotated with propagation directions. Consequentely, the typing
rules also become more complicated in order to deal with colored types. Contextual typing deals
with partial type information via the surrounding context, and does not require changes to thesyntax of types. Thus the propagation of partial type information is considerably simpler. However,
we currently do not deal with implicit polymorphism, which is left to future work.
7

Conclusion

Contextual typing is a lightweight form of type inference that exploits partially known contextual
information. It enables several improvements over bidirectional typing. Firstly, fewer annotations
are needed, by having a more powerful treatment for applications, and propagating contextual
information. This is achieved without backtracking, keeping the approach efficient. More powerfulapplication rules also help with binding constructs and avoid duplicated rules. Secondly, annotatability becomes clearer, and specifications of typing describing where annotations are needed aremade precise via a QTAS. Finally, for type systems with subtyping, contextual subsumption deals
with partially known contextual information, and avoids changes in other rules and specialized
auxiliary relations. For implementations, instead of two mutually recursive inference and checking
functions, we need mutually recursive typing and subtyping/matching functions.
To design a type system with contextual typing, an informal design recipe is to start with thecorresponding TAS. Then there are two main tasks: 1) determining contextual type informationand the structure of the surrounding context; and 2) designing the QTAS and counters. For (1) wemust analyse the elimination forms in the language and determine the information that needs tobe tracked in the context to aid the consumers. For (2), the design of the QTAS and counters issomewhat interconnected. A simpler case is when there is only a single QTAS typing rule for eachelimination form. In this case, the design of counters is simple: we simply need a different kindof successor for each entry in the surrounding context. The main complication that can show up
when designing a QTAS and counters is that we may want multiple rules for the same elimination
form. This is what happens with applications, where we wish to have 2 different rules for added
flexibility. In the general case, we need a successor counter for each typing rule dealing with theelimination form, although for STLC it is possible to have a simpler design with only one successor.
We only cover a small set of features in this work. More study is needed to show the practicalapplicability of contextual typing to other features. The interaction between contextual typing andpolymorphism is a particularly interesting direction for future work.
Acknowledgments
We are grateful to the anonymous reviewers for their valuable comments, and to Shengyi Jiang for
his insight of substitution lemma and help in complex induction. This work has been sponsored byHong Kong Research Grant Council project number 17209821.
Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

266:28

Xu Xue and Bruno C. d. S. Oliveira

References
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. 2012. A bi-directional refinement algorithm forthe calculus of (co) inductive constructions. Logical Methods in Computer Science 8 (2012).
Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983. A filter lambda model and the completeness oftype assignment. Journal of Symbolic Logic 48, 4 (1983), 931–940.
Gavin Bierman, Martín Abadi, and Mads Torgersen. 2014. Understanding typescript. In European Conference on ObjectOriented Programming.
Iliano Cervesato and Frank Pfenning. 2003. A Linear Spine Calculus. J. Log. Comput. 13, 5 (2003), 639–688.
Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1981. Functional characters of solvable terms. Mathematical
Logic Quarterly 27, 2-6 (1981), 45–58.
Thierry Coquand. 1996. An algorithm for type-checking dependent types. Science of computer programming 26, 1-3 (1996),
167–177.
Rowan Davies and Frank Pfenning. 2000. Intersection types and computational effects. In Proceedings of the fifth ACM
SIGPLAN international conference on Functional programming. 198–208.
Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional typing. ACM Computing Surveys (CSUR) 54, 5 (2021), 1–38.
Jana Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and easy bidirectional typechecking for higher-rankpolymorphism. In ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA September 25 - 27, 2013, Greg Morrisett and Tarmo Uustalu (Eds.). ACM, 429–442. https://doi.org/10.1145/2500365.2500582
Jana Dunfield and Frank Pfenning. 2004. Tridirectional typechecking. In Proceedings of the 31st ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, Neil D. Jones andXavier Leroy (Eds.). ACM, 281–292. https://doi.org/10.1145/964001.964025
Xuejing Huang, Jinxu Zhao, and Bruno C. d. S. Oliveira. 2021. Taming the Merge Operator. Journal of Functional Programming
31 (2021), e28.
Christopher Jenkins and Aaron Stump. 2018. Spine-local type inference. In Proceedings of the 30th Symposium on Implementation and Application of Functional Languages. 37–48.
Daan Leijen. 2008. HMF: simple type inference for first-class polymorphism. In Proceeding of the 13th ACM SIGPLAN
international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, James Hookand Peter Thiemann (Eds.). ACM, 283–294.
Andres Löh, Conor McBride, and Wouter Swierstra. 2010. A tutorial implementation of a dependently typed lambda calculus.
Fundamenta informaticae 102, 2 (2010), 177–207.
Henry Mercer, Cameron Ramsay, and Neel Krishnaswami. 2022. Implicit Polarized F: Local Type Inference for Impredicativity.
arXiv preprint arXiv:2203.01835. https://doi.org/10.48550/arXiv.2203.01835
Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Vol. 32. Chalmers University ofTechnology.
Martin Odersky, Christoph Zenger, and Matthias Zenger. 2001. Colored Local Type Inference. In Proceedings of the 28th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL, 41–53. https://doi.org/10.1145/
360204.360207
Benjamin C Pierce and David N Turner. 2000. Local type inference. ACM Transactions on Programming Languages andSystems (TOPLAS) 22, 1 (2000), 1–44.
Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program synthesis from polymorphic refinement types.
In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16).
Association for Computing Machinery, New York, NY, USA.
François Pottier and Yann Régis-Gianas. 2006. Stratified type inference for generalized algebraic data types. In Conference
Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’06). Association
for Computing Machinery, New York, NY, USA.
Garrel Pottinger. 1980. A type assignment for the strongly normalizable 𝜆-terms. To HB Curry: essays on combinatory logic,
lambda calculus and formalism (1980), 561–577.
John C Reynolds. 1991. The coherence of languages with intersection types. In International Symposium on Theoretical
Aspects of Computer Software. Springer, 675–700.
John C Reynolds. 1997. Design of the programming language Forsythe. In ALGOL-like languages. Springer, 173–233.
Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliveira, and Steve Zdancewic. 2023. A Bowtie for a Beast: Overloading, Eta
Expansion, and Extensible Data Types in 𝐹 ⊲⊳ . Proc. ACM Program. Lang. 7, POPL, Article 18 (jan 2023).
Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis. 2020. A quick look at impredicativity. Proc.
ACM Program. Lang. 4, ICFP, Article 89 (aug 2020).
Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones. 2018. Guarded impredicative polymorphism.
In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018).
Association for Computing Machinery, New York, NY, USA.

Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.

Contextual Typing

266:29Hongwei Xi and Frank Pfenning. 1999. Dependent types in practical programming. In Proceedings of the 26th ACM
SIGPLAN-SIGACT symposium on Principles of programming languages. 214–227.
Ningning Xie and Bruno C d S Oliveira. 2018. Let arguments go first. In Programming Languages and Systems: 27th European
Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software,
ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings 27. Springer, 272–299.
Xu Xue, Bruno C d S Oliveira, and Ningning Xie. 2022. Applicative Intersection Types. In Asian Symposium on Programming
Languages and Systems. Springer, 155–174.
Jinxu Zhao, Bruno C d S Oliveira, and Tom Schrijvers. 2019. A mechanical formalization of higher-ranked polymorphic
type inference. Proceedings of the ACM on Programming Languages 3, ICFP (2019), 1–29.

Received 2024-02-28; accepted 2024-06-18

Proc. ACM Program. Lang., Vol. 8, No. ICFP, Article 266. Publication date: August 2024.