<figure><img src="image_1.png" /></figure>

HAL
open science

# On Type-Cases, Union Elimination, and Occurrence Typing

Giuseppe Castagna, Mickael Laurent, Kim Nguyen, Matthew Lutze

► To cite this version:

Giuseppe Castagna, Mickael Laurent, Kim Nguyen, Matthew Lutze. On Type-Cases, Union Elimination, and Occurrence Typing. Proceedings of the ACM on Programming Languages, 2022, 49th ACM SIGPLAN Symposium on Principles of Programming Languages, 6 (POPL), pp.75. 10.1145/3498674. hal-03426711v2

HAL Id: hal-03426711

https://hal.science/hal-03426711v2

Submitted on 20 Jan 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# On Type-Cases, Union Elimination, and Occurrence Typing

GIUSEPPE CASTAGNA, CNRS, Université de Paris, France

MICKAËL LAURENT, Université de Paris, France

KIM NGUYỄN, Université Paris-Saclay, France

MATTHEW LUTZE, Université de Paris, France

We extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses occurrence typing. To apply this system in practice, we define a canonical form for the expressions of our extension, called MSC-form. We show that an expression of the extension is typable if and only if its MSC-form is, and reduce the problem of typing the latter to the one of reconstructing annotations for that term. We provide a sound algorithm that performs this reconstruction and a proof-of-concept implementation.

**CCS Concepts:** • **Theory of computation** → *Type structures*; *Program analysis*; • **Software and its engineering** → *Functional languages*.

**Additional Key Words and Phrases:** subtyping, union types, intersection types, type-case, dynamic languages, type systems.

**ACM Reference Format:**

Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, and Matthew Lutze. 2022. On Type-Cases, Union Elimination, and Occurrence Typing. *Proc. ACM Program. Lang.* 6, POPL, Article 13 (January 2022), 75 pages. https://doi.org/10.1145/3498674

# 1 INTRODUCTION

TypeScript [Microsoft] and Flow [Facebook] are extensions of JavaScript that allow the programmer to specify in the code type annotations used to statically type-check the program. For instance, the following function definition is valid in both languages

```javascript
function foo(x : number | string) {
    return (typeof(x) === "number")? x+1 : x.trim();
}
```

Apart from the type annotation (in red) of the function parameter, the above is standard JavaScript code defining a function that checks whether its argument is an integer; if it is so, then it returns the argument's successor ($x+1$), otherwise it calls the method `trim()` of the argument. The annotation specifies that the parameter is either a number or a string (the vertical bar denotes a union type). If this annotation is respected and the function is applied to either an integer or a string, then the application cannot fail because of a type error (`trim()` is a standard string method) and both TypeScript and Flow rightly accept this function and deduce that it will return either a number or a string, that is, a result of type `number|string`. This is possible because both type-checkers

Authors' addresses: Giuseppe Castagna, Mickaël Laurent, Matthew Lutze, Institut de Recherche en Informatique Fondamentale (IRIF), Université de Paris, CNRS, 8 place Aurélie Nemours, 75013 Paris, France; Kim Nguyễn, Laboratoire Méthodes Formelles (LMF), Université Paris-Saclay, CNRS, ENS Paris-Saclay, 91190, Gif-sur-Yvette, France.
implement a specific type discipline called *occurrence typing* or *flow typing*:<fnref n="1" /> as a matter of fact, standard type disciplines would reject this function. The reason for that is that standard type disciplines would try to type every part of the body of the function under the assumption that x has type *number* | *string* and they would fail, since the successor is not defined for strings and the method *trim()* is not defined for numbers. This is so because standard disciplines do not take into account the type test performed on x. Occurrence typing is the typing technique that uses the information provided by the type test to specialize—precisely, to *refine*—the type of the occurrences of x in the branches of the conditional: since the program tested that x is of type *number*, then we can safely assume that x is of type *number* in the “then” branch, and that it is *not* of type *number* (and thus deduce from the type annotation that it must be of type *string*) in the “else” branch.

Occurrence typing was first defined and formally studied by Tobin-Hochstadt and Felleisen [2008] to statically type-check untyped Scheme programs, and later extended by Tobin-Hochstadt and Felleisen [2010] yielding the development of Typed Racket. To that end the authors define a system to deduce propositions, that express relations between variables and types, and these are attached to functional types (*à la* effect system) to describe facts about the result of applying the corresponding functions. In this work we argue that to capture occurrence typing—and, as we detail later on, much, much more—it is not necessary to resort to effect-like systems, perform flow analysis, or invent new expressive types. It just suffices to add to the language at issue a type-case expression and combine (a tailored definition of) its typing rules with the classic union elimination rule as it was first introduced by MacQueen et al. [1986]. More precisely, let *t* be a type and (*e*∈*t*) ? *e*₁: *e*₂ be the type-case expression that first evaluates *e* to a value *v* and continues as *e*₁ if *v* is of type *t*, and as *e*₂ otherwise. Then we claim that all the situations in which occurrence typing is used are covered by these three typing rules.

$$ \frac{\Gamma \vdash e' : t_1 \lor t_2 \qquad \Gamma, x:t_1 \vdash e : t \qquad \Gamma, x:t_2 \vdash e : t}{\Gamma \vdash e \{e' / x\} : t} \qquad \frac{\Gamma \vdash e : t \qquad \Gamma \vdash e_1 : t_1 \qquad \Gamma \vdash (e \in t) ? e_1 : e_2 : t_1}{\Gamma \vdash (e \in t) ? e_1 : e_2 : t_2} $$

The first is the classic union elimination rule by MacQueen et al. [1986] where $e\{e'/x\}$ is the expression obtained from *e* by substituting *e'* for *x* and $t_1 \lor t_2$ is a *union type* (for union and intersection we respectively use | and & in code snippets and ∨ and ∧ in formal types). If we interpret a type set-theoretically as the set of all values that have that type, then $t_1 \lor t_2$ is the type that contains all values of type $t_1$ and all values of type $t_2$. In a sound system an expression *e* is given a type *t* only if it can only produce a result in *t*; this implies that an expression of type $t_1 \lor t_2$ can produce a result either of type $t_1$ or of type $t_2$. The union elimination rule states that given some expression (here, $e\{e'/x\}$) with a subexpression *e'* of type $t_1 \lor t_2$, if we can give to this expression the type *t* both under the hypothesis that *e'* produces a result of type $t_1$ and under the hypothesis the *e'* produces a result in $t_2$, then we can safely give this expression type *t*.

The two other rules are new and provide a natural and nifty way to type type-case expressions. The first rule states that if *e* can only produce a result in *t*, then the type of (*e*∈*t*) ? *e*₁: *e*₂ is the type of *e*₁. The second rule states that if *e* can only produce a result in ¬*t*, then the type of (*e*∈*t*) ? *e*₁: *e*₂ is the type of *e*₂: since the *negation type* ¬*t* is interpreted set-theoretically as the set of all values that are *not* of type *t*, this means that, in that case, *e* can only produce a result *not* of type *t*.

The reader may wonder how we type a type-case expression (*e*∈*t*) ? *e*₁: *e*₂ when the tested expression *e* is neither of type *t* nor of type ¬*t*. As a matter of fact, a type-case is interesting only if we cannot statically determine whether it will succeed or fail. For instance, the type-case in (1) tests whether *x* is of type *number*, but since *x* is of type *number* | *string*, then it is neither of type *number* nor of type ¬*number*. Here, the combination of set-theoretic types and the union rule plays its

<footnote n="1">¹TypeScript calls it “type guard recognition” while Flow uses the terminology “type refinements”.</footnote>
magic. Union and negation types, give intersection types for free: just define $t_1 \land t_2$ as $\neg(\neg t_1 \lor \neg t_2)$. Thus, even though the tested expression $e$ has some type $s$ that is neither contained in (i.e., subtype of) $t$ nor in $\neg t$, we can use intersection and negation to split $s$ into the union of two types that have this property, since $s \approx (s \land t) \lor (s \land \neg t)$. We can thus apply the union rule and check the type-case under the hypothesis that the tested expression has type $(s \land t)$ and under the hypothesis that it has type $(s \land \neg t)$. For instance, for (1) we check the type-case under the hypothesis that $x$ has type number (i.e., $(number \lor string) \land number$) and deduce the type number, and under the hypothesis that $x$ has type string (i.e., $(number \lor string) \land \neg number$) and deduce the type string, which by subsumption gives for the whole expression the expected type $number \lor string$.

We see that our treatment of occurrence typing heavily depends on the properties of set-theoretic types: unions, intersections, and negations of types. This does not come as a surprise since from its inception occurrence typing was intimately tied to type systems with set-theoretic types. Union was the first type connective to appear, since it was already used in [Tobin-Hochstadt and Felleisen 2008] to characterize the different control flows of a type test, as our *foo* example shows: one flow for integer arguments and another for strings. Intersection types appear (in limited forms) combined with occurrence typing both in *TypeScript* and in *Flow* and serve to give, among other things, more precise types to functions such as *foo*. For instance, since $x+1$ evaluates to an integer and $x.trim()$ to a string, then our function *foo* has type $(number|string) \rightarrow (number|string)$. But it is clear that a more precise type would be one that states that *foo* returns a number when it is applied to a number and returns a string when it is applied to a string, so that the type deduced for, say, *foo(42)* would be *number* rather than the less precise *number|string*. This is exactly what the intersection type

$$ (number \rightarrow number) \& (string \rightarrow string) \qquad (2) $$

states (intuitively, an expression has an intersection of types, noted &, if and only if it has all the types of the intersection) and corresponds in *Flow* to declaring *foo* as follows:

$$ \begin{array}{l} var foo : (number => number) \& (string => string) = x => { \\ \quad return (typeof(x) === "number")? x+1 : x.trim(); \\ } \end{array} \qquad (3) $$

For what concerns negation types, they are pervasive in the occurrence typing approach, even though they are used only at meta-theoretic level, in particular to determine the type environment when the type-case fails. We already saw negation types at work when we informally typed the “else” branch in *foo*, for which we assumed that $x$ did not have type *number*—i.e., it had the (negation) type $\neg number$—and deduced from it that $x$ then had type *string*—i.e., $(number|string) \& \neg number$ which is equivalent to the set-theoretic difference $(number|string) \setminus number$ and, thus, to *string*.

Since set-theoretic types play such a pivotal role in our treatment the system we study in this work is a conservative extension of the standard type assignment system for union and intersection types, which was defined by Barbanera et al. [1995, Definition 3.5]. To cope with occurrence typing we extend, in a nutshell, the system of [Barbanera et al. 1995] with three simple ingredients:

(1) we add to its expressions the type-case expression $(e \in t) ? e : e$;

(2) we add to its types the negation connective and the empty type;

(3) we add to its deduction rules the typing rules for type-cases we showed before.

The resulting system, presented in Section 2, is a type-assignment system for an untyped $\lambda$-calculus with constants, pairs, and type-cases.

We said earlier that the combination of the union rule and set-theoretic types gives us much more than what current formalizations of occurrence typing can capture. The approaches cited above essentially focus on refining the type of variables that occur in an expression whose type is being tested. They do it when the variable occurs at top-level in the test (i.e., the variable is the
expression being tested) or under some specific positions such as in nested pairs or at the end of a path of selectors. The union elimination rule of MacQueen et al. [1986] does not have such limitations: it can refine the type of any expression e' occurring in any position of the current expression e, by splitting the type of e' into a union of types that are tested separately for e. The separation of these tests combines with our new rules for type-cases to yield a system in which different branches of the same type-case are typed under different typing hypotheses, which is the essence of occurrence typing. In this work we aim at exploiting this power of the union rule and refine the type of any expression that occurs in a tested expression (or elsewhere). Of particular interest will be the expressions occurring in applications since the refinement of their types is pivotal in deducing and exploiting intersection types for functions. For example, let $x_1$ be a variable of type $(\text{Int} \to \text{Int}) \wedge (\text{String} \to \text{String})$ (e.g., $x_1$ binds the function `foo` defined in (3)) and $x_2$ be of type $\text{Int} \lor \text{String}$. If `@` denotes string concatenation, then we can use the three typing rules above to deduce that the following expression has type $\text{Int} \lor \text{String}$.

$$ (x_1 x_2 \in \text{Int})?(x_2 + 1):((x_1 x_2) @ x_2) \qquad (4) $$

This is done by splitting the type of $x_2$: if $x_2$ is of type `Int`, then $x_1 x_2$ is also of type `Int`, thus the first branch is selected and the addition in it is well typed with type `Int`; if $x_2$ is of type `String`, then $x_1 x_2$ is also of type `String`, thus the second branch is selected and the concatenation in it is well typed with type `String`. This is an example of typing that is out of reach for all the previously cited approaches. This is possible because our approach does not perform occurrence typing using only the information given by type-cases: it also uses all type information provided by applications, even more when functions are overloaded (i.e., typed by an intersection of arrows, as $x_1$ in (4)).

One of the most important consequences of such a thorough analysis is that we can use its results to infer intersection types for functions, even in the absence of precise annotations such as the one given in the definition of `foo` in (3): we split the type of the function parameter (initially supposed to be the top type `Any`) and deduce a distinct arrow for each split of the input type, discarding from the domain the split types for which the inference fails. To put it simply, we can infer the type (2) for the unannotated pure JavaScript code of `foo` (i.e., no type annotation at all), while in `TypeScript` and `Flow` (and any other formalism we are aware of) this requires an explicit and full type annotation as the one given in (3). This creates a virtuous circle since, as the program in (4) shows, determining intersection types for functions is crucial to refine the type of expressions in applications, which allows to deduce more precise types for functions and so forth. Thanks to this virtuous circle our system can type a whole class of functions that other systems fail to type (even when given explicit full type annotations) and must then hard-code to retain sufficient expressiveness. And for well-typed programs our approach needs, in general, fewer annotations. For instance, we can type all the 14 paradigmatic examples of Tobin-Hochstadt and Felleisen [2010] without any annotation, whereas they need to specify annotations for 5 of them (see Section 6).

Having three typing rules that allow us to type all the examples of occurrence typing (and even more) is still a far cry from a practical system that can decide whether a program of our source language (the untyped $\lambda$-calculus with constants, pairs, and type-cases) is well-typed or not. The culprit is, of course, the powerful union rule: to use this rule to type some expression e one has to guess a subexpression e' of e to single out, the occurrences of e' to be tested, and how to split the type of this e' in a union of types to be tested separately. This is no simple feat: according to Mariangiola Dezani, arguably the best expert in union and intersection type systems, determining an inversion (a.k.a., generation) lemma for this union rule is the most important open problem in this field of research [Dezani-Ciancaglini 2020]. And an inversion lemma is an important aid to define a type-inference algorithm, since it tells us when and how to apply the rule.
<figure><img src="image_3.png" /><figcaption>Fig. 1. Pure MSC-form</figcaption></figure>

<caption>Fig. 2. Annotated MSC-form</caption>

In order to tackle this last problem of deciding whether an expression is well typed or not, we transform it into an equivalent problem in which the range of possible choices is much more restricted. To that end we introduce a canonical form for the expressions of our source language that we call *maximal-sharing canonical form (MSC-form)*. A MSC-form is essentially a list of bindings from variables to *atoms*. An atom is either an expression of our source language in which all subexpressions are variables, or it is a *λ*-abstraction whose body is a MSC-form. We call these forms *maximal-sharing* forms because they must satisfy the property that there cannot be two distinct bindings for the same atom. This is a crucial property because it ensures that every expression of the source language (*i*) is equivalent to a unique (modulo some trivial syntactic conversions) MSC-form and (*ii*) is well-typed if and only if its MSC-form is. For instance, consider the expression in (4) where $x_1$ and $x_2$ rather than being variables are generic atoms of type $t_1 = (\text{Int} \to \text{Int}) \wedge (\text{String} \to \text{String})$ and $t_2 = \text{Int} \vee \text{String}$, that is $(a_1 a_2 \in \text{Int}) ? (a_2 + 1) : ((a_1 a_2) @ a_2)$. Its MSC-form will look like the term in Figure 1. Notice that this term satisfies the maximal sharing property because the two occurrences of the application $a_1 a_2$ in the source language expression are bound by the same variable $x_3$. The other crucial property that we prove is that an MSC-form is well-typed if and only if it is possible to explicitly annotate all the bindings of variables so that the MSC-form type-checks. These annotations essentially define how the type of the variables must be split and the annotated MSC-form type-checks if the rest of the expression type-checks for each of the splits specified in its annotations. Figure 2 gives the annotations for the previous MSC-form. The important annotations are those of the variables $x_2$ and $x_3$. The first states that to type the expression, the type $\text{Int} \vee \text{String}$ of $a_2$ must be split and the expression must be checked separately for $x_2 : \text{Int}$ and $x_2 : \text{String}$. The annotation of $x_3$ states that when $x_2$ has type $\text{Int}$ then $x_3$ must be assumed to be of type $\text{Int}$ and when $x_2$ has type $\text{String}$ so must have $x_3$ (see Section 4 for details).

Since we can effectively transform a source language expression into its MSC-form, then we have a method to check the well-typedness of an expression of the source language: transform it into its MSC-form and infer all the annotations of its variables, if possible. Inferring the annotations of a MSC-form boils down to deciding how to split the types of its atoms. This is done by an algorithm we present in Section 5 which starts from a MSC-form in which all variables are annotated with the top type Any and performs several passes to refine these annotations. Each pass has three possible outcomes: either (*i*) the MSC-form type-checks with its current annotations and the algorithm stops with a success, or (*ii*) the MSC-form does not type-check, the pass proposes a new version of the same MSC-form but with refined annotations, and a new pass is started, or (*iii*) the MSC-form does not check and it is not possible to further refine the annotations so that the form may become typable, then the algorithm stops with a failure. The algorithm refines the annotations differently for variables that are bound by lambdas and by binds. For the variables in binds the algorithms produces a set of disjoint types so that their union is the type of the atom in the bind; for lambdas the algorithm splits the type of the parameter into a set of disjoint types and rejects the types in this set for which the function does not type-check, thus determining the domain of the function. The very last point that remains to explain is how to determine the split of a type: as a matter of fact, in general there are infinitely many different ways to split a type. The split of the types is driven by the types tested in type-cases and the operations applied to their components. For instance, the
split of the type of $a_2$ for the variable $x_2$ in Figures 1 and 2 is determined by the test $x_3 \in \text{Int}$: the algorithm will propose to split the type $t_3$ of $x_3$ into $t_3 \wedge \text{Int}$ and $t_3 \wedge \neg\text{Int}$. Since $t_3$ is $\text{Int} \vee \text{String}$, the split proposed for $x_3$ is actually Int or String. This split triggers in the subsequent pass the split for the type of $x_2$ since $x_3$ is defined as $x_1x_2$ and $x_3$ can be of type Int only if $x_2$ is of type Int and it can be of type String only if $x_2$ is of type String. We just got the expected annotation.

*Contributions.* This work provides four main technical contributions. (i) We show how to extend the system of Barbanera et al. [1995] with negation types and type-cases and prove its soundness (§2); (ii) we define MSC-forms and prove that the problem of typing a term of the previous system is equivalent to the one of typing its MSC-form (§3); (iii) we prove that the latter problem is equivalent to adding type annotations in a MSC-form so that it becomes a well-typed term and that checking well-typedness of an annotated MSC-form is decidable (§4); (iv) we define a sound reconstruction algorithm for the annotations of a MSC-form (§5) and provide an implementation (§6).

More generally, this work provides a novel formal lens for viewing the conceptual core of occurrence typing, whose essence it reveals. It reframes occurrence typing in the more standard and general setting of classic union and intersection type systems and, in doing so, it removes several current limitations of existing approaches. The removal of these limitations makes it possible for our system not only to type several examples that are out of reach of existing approaches but also to deduce precise intersection types for completely unannotated functions, something that, in our ken, no other system is currently capable of. By the definition of MSC-forms, it circumscribes the use of union elimination to a very specific setting, thus advancing in the quest for the characterization of inversion of union rules. More importantly, it shows that well-typing in such systems is equivalent to the problem of reconstructing annotations for MSC-forms, thus providing a formal yard-stick to compare different approaches. We exploited this new setting to define a sound reconstruction algorithm that we rendered in a proof-of-concept implementation. This implementation demonstrates the potential practical implications of our work, even though the gap with mature implementations such as those of Flow, Typed Racket, or TypeScript is still huge. Last but not least, we obtained a system that is arguably more robust to extensions such as the addition of side-effects and of polymorphic types, as we are eager to verify in the near future.

For space reasons several definitions and rules, the extensions with records and let-constructs, and all the proofs are moved to the appendix, available on line as supplemental material.

# 2 SOURCE LANGUAGE AND DECLARATIVE TYPE SYSTEM

## 2.1 Types

Types are exactly those of the semantic subtyping framework by Frisch et al. [2002, 2008].

**DEFINITION 2.1 (TYPES).** The set of types **Types** is formed by the terms **t** coinductively produced by the grammar:

$$ \mathbf{Types} \ t ::= b \mid t \to t \mid t \times t \mid t \vee t \mid \neg t \mid \emptyset $$

and that satisfy the following conditions

- (regularity) every term has a finite number of different sub-terms;

- (contractivity) every infinite branch of a term contains an infinite number of occurrences of the arrow or product type constructors.

We introduce the abbreviations $t_1 \wedge t_2 \stackrel{\text{def}}{=} \neg(\neg t_1 \vee \neg t_2)$, $t_1 \wedge t_2 \stackrel{\text{def}}{=} t_1 \wedge (\neg t_2)$, and $\mathbf{1} \stackrel{\text{def}}{=} \emptyset$. $b$ ranges over basic types (e.g., Int, Bool), $\emptyset$ and $\mathbf{1}$ respectively denote the empty (that types no value) and top (that types all values) types. Coinduction accounts for recursive types and the condition on infinite branches bars out ill-formed types such as $t = t \vee t$ (which does not carry any information about the set denoted by the type) or $t = \neg t$ (which cannot represent any set). Regularity is needed
for the decidability of the subtyping relation. We refer to $b$, $\times$, and $\rightarrow$ as *type constructors*, and to $\lor$, $\neg$, $\land$, and $\lhd$ as *type connectives*. As customary, connectives have priority over constructors and negation has the highest priority—e.g., $\neg s \lor t \rightarrow u \land v$ denotes $((\neg s) \lor t) \rightarrow (u \land v)$.

The subtyping relation for these types, noted $\leq$, is the one defined by Frisch et al. [2008] to which the reader may refer for the formal definition (we recall it in Appendix A.1 for the reader's convenience). A detailed description of the algorithm to decide this relation can be found in [Castagna 2020]. For this presentation it suffices to consider that types are interpreted as sets of *values* (i.e., either constants, $\lambda$-abstractions, or pairs of values: see Section 2.2 right below) that have that type, and that subtyping is set containment (i.e., a type $s$ is a subtype of a type $t$ if and only if $t$ contains all the values of type $s$). In particular, $s \rightarrow t$ contains all $\lambda$-abstractions that when applied to a value of type $s$, if their computation terminates, then they return a result of type $t$ (e.g., $\emptyset \rightarrow 1$ is the set of all functions and $1 \rightarrow \emptyset$ is the set of functions that diverge on every argument). Type connectives (i.e., union, intersection, negation) are interpreted as the corresponding set-theoretic operators (e.g., $s \lor t$ is the union of the values of the two types). We use $\approx$ to denote the symmetric closure of $\leq$: thus $s \approx t$ (read, $s$ is equivalent to $t$) means that $s$ and $t$ denote the same set of values and, as such, they are semantically the same type.

## 2.2 Terms

The expressions of our *source language*, that is the language the programmer uses, are defined as:

$$
\begin{align}
\textbf{Test Types} \qquad & \tau ::= b \mid \emptyset \rightarrow 1 \mid \tau \times \tau \mid \tau \lor \tau \mid \neg \tau \mid \emptyset \notag \\
\textbf{Expressions} \qquad & e ::= c \mid x \mid \lambda x.e \mid ee \mid (e, e) \mid \pi_i e \mid (e \in \tau) \ ? \ e : e \tag{5} \\
\textbf{Values} \qquad & v ::= c \mid \lambda x.e \mid (v, v) \notag
\end{align}
$$

Expressions are an untyped $\lambda$-calculus with constants $c$, pairs $(e, e)$, pair projections $\pi_i e$, and type-cases. A typecase $(e_0 \in \tau) \ ? \ e_1 : e_2$ is a dynamic type test that first evaluates $e_0$ and, then, if $e_0$ reduces to a value $v$ evaluates $e_1$ if $v$ has type $\tau$ or $e_2$ otherwise. Type-cases cannot test arbitrary types but just types of the form $\tau$ where the only arrow type that can occur in them is $\emptyset \rightarrow 1$, the type of all functions. This means that type-cases can distinguish functions from other values but they cannot distinguish, say, functions that have type $\mathrm{Int} \rightarrow \mathrm{Int}$ from those that do not. In previous work on semantic subtyping, there is no such restriction, but this is possible only because $\lambda$-abstractions are explicitly annotated with their types. If in the presence of non-annotated $\lambda$-abstractions we allowed tests on function types, then in a practical implementation the semantics would depend on the implementation of the type checking or type inference algorithms. Thanks to this restriction, instead, the semantics does not depend on the type system: it can be implemented without keeping track of compile-time types at runtime. Moreover, the interest of the typecase construct in this work is mostly to encode a pattern matching construct. Standard pattern matching cannot check function types, so the restriction is not a problem for this. Typecases of this form also have the same expressiveness as the type-testing primitives of dynamic languages like JavaScript and Racket.

Since every test type $\tau$ is also a type, then in what follows we may sometimes use the metavariable $t$ to denote test types when this is clear from the context.

## 2.3 Reduction Semantics

The reduction semantics is the one of call-by-value pure $\lambda$-calculus with products and with a type-case expression. The reduction is given by the following notions of reductions

$$
\begin{align*}
(\lambda x.e)v &\rightsquigarrow e\{v/x\} & (v \in \tau) \ ? \ e_1 : e_2 &\rightsquigarrow e_1 && \text{if } v \in \tau \\
\pi_1(v_1, v_2) &\rightsquigarrow v_1 & & & \\
\pi_2(v_1, v_2) &\rightsquigarrow v_2 & (v \in \tau) \ ? \ e_1 : e_2 &\rightsquigarrow e_2 && \text{if } v \in \neg \tau
\end{align*}
$$

together with the context rules that implement a leftmost outermost reduction strategy.
The definition uses the standard substitution operation $e\{e'/x\}$ that denotes the capture avoiding substitution of $e'$ for $x$ in $e$, and the relation $v \in \tau$ that determines whether a value is of a given type or not and holds true if and only if $typeof(v) \le \tau$, where $typeof(\lambda x.e) = \emptyset \to \mathbf{1}$, $typeof(c) = b_c$, $typeof((v_1, v_2)) = typeof(v_1) \times typeof(v_2)$, and $b_c$ is the unique basic type of the constant $c$ (e.g., $b_{42} = \text{Int}$). Note that $typeof()$ maps every $\lambda$-abstraction to $\emptyset \to \mathbf{1}$, so it does not depend on static types. This approximation is allowed by the restriction on arrow types in typecases.

The language we just defined is the same as the functional core of CDuce defined by Frisch et al. [2002, 2008] but two important differences. The first difference is that $\lambda$-abstractions in [Frisch et al. 2002, 2008] are explicitly annotated with their types while here no annotation is needed. The absence of annotations not only relieves the programmer of an important burden but also, in the case of curried functions, makes it possible to type some expressions that could not be typed with the annotations used in CDuce (see Section 4). The price to pay for this choice is twofold: the burden of finding the annotations for $\lambda$-abstractions is passed on the type system and, as explained before, we no longer allow type-cases to test for arbitrary types. The second difference is that the type-case expressions in [Frisch et al. 2002, 2008] introduce a binding since they are of the form $(x:=e_o \in \tau) \ ? \ e_1 : e_2$, that is, the expression binds the result of the tested expression $e_o$ to the variable $x$ so that it is possible to specialize the type of $x$ differently for typing $e_1$ and $e_2$ and thus implement a limited form of occurrence typing (if $e_o : t$, then we assume $x : t \land \tau$ when typing $e_1$ and $x : t \land \neg \tau$ when typing $e_2$). Here we do not ask the programmer to write such a binding: in our system such a binding is deduced by the type system (and this deduction is not limited to type-case expressions). The deduction of this binding is the core of our approach and constitutes the key idea of our generalization of occurrence typing.

## 2.4 Type System

While the terms, types, and operational semantics of the language are essentially the same as the language by Frisch et al. [2002, 2008], the type inference system is completely different, in particular in what concerns the typing of the type-cases. *Per se* the typing system we detail below is far from being new: it is composed exactly by the rules of the classic system of union and intersection types defined by Barbanera et al. [1995] to which we add standard introduction and elimination rules for products ($[\times I]$, $[\times E_1]$, $[\times E_2]$) and the three rules for the type-cases ($[\emptyset]$, $[\epsilon_1]$, $[\epsilon_2]$). The typing rules are given in Figure 3 and use the following definition of type environments.

**DEFINITION 2.2 (TYPE ENVIRONMENT).** *Type environments, ranged over by $\Gamma$ are finite sets of mappings from pairwise distinct variables to types. We denote by $dom(\Gamma)$ the set of variables mapped by $\Gamma$. We write $\Gamma, x : t$ for the type environment $\Gamma \cup \{x \mapsto t\}$, when $\Gamma$ is a type environment such that $x \notin dom(\Gamma)$. We write $\emptyset$ for the type environment formed by an empty set of mappings.*

If we remove from Figure 3 the three rules for type-cases ($[\emptyset]$, $[\epsilon_1]$, $[\epsilon_2]$) the resulting system is the same as the one in Definition 3.5 of Barbanera et al. [1995, Definition 3.5] (extended with standard rules for products and constants). The rules for abstractions and applications are those of the simply typed $\lambda$-calculus while those for pairs and projections extend it to products. Union and intersection types are handled by the rule $[\land]$ that introduces intersections, the rule $[\lor]$ that eliminates unions, and the subsumption rule $[\le]$ that introduces unions and eliminate intersections.

Notice that, by the definition of type-environments, it is not possible to type two nested $\lambda$-abstractions abstracting the same variable and that in the rule $[\lor]$ we have that $x \notin dom(\Gamma)$. It is instead possible to have two distinct (not nested) $\lambda$-abstractions with the same abstracted variable, even though from a type-perspective point of view this is not relevant since, as it is
<figure><img src="image_4.png" /><figcaption>Fig. 3. Declarative type system</figcaption></figure>

standard in such systems, the deduction is defined modulo $\alpha$-conversion. In other terms, we suppose the existence of the implicit rule given below on the right (where $\equiv_\alpha$ denotes $\alpha$-conversion).
Working modulo $\alpha$-conversion is crucial in systems with union types since rule $[\vee]$ breaks the $\alpha$-invariance property (see Hindley and Seldin [2008, Discussion 12.5]). For instance, the following judgement $y : \mathbf{1} \to \mathbf{Bool} \vdash (y(\lambda x.x), y(\lambda x.x)) : (\mathbf{True} \times \mathbf{True}) \lor (\mathbf{False} \times \mathbf{False})$ can be derived in the system above by using $[\vee]$ together with the rules for application and pairs (where $\mathbf{Bool} = \mathbf{True} \lor \mathbf{False}$, with True being the singleton type containing the value true,<fnref n="2" /> and likewise for False). However, to derive the same type for the $\alpha$-equivalent term $(y(\lambda x.x), y(\lambda z.z))$ the rule $[\equiv_\alpha]$ must be used. In what follows, we will use a variant of the system above where the rules $[\vee]$ and $[\wedge]$ are replaced by the following rules that produce more compact derivations and are closer to the syntax-directed system given in the next section:

$$ [\wedge+] \frac{(\forall i \in I) \quad \Gamma \vdash e : t_i}{\Gamma \vdash e : \bigwedge_{i \in I} t_i} \quad I \neq \emptyset \qquad [\vee+] \frac{\Gamma \vdash e' : \bigvee_{i \in I} t_i \quad (\forall i \in I) \quad \Gamma, x : t_i \vdash e : t}{\Gamma \vdash e\{e'/x\} : t} \quad I \neq \emptyset $$

Although the rules in our system are textually the same as those in [Barbanera et al. 1995, Definition 3.5] there is an important difference, namely, that our types are an extension of those of Barbanera et al. [1995] since they include recursive types, negation types, and the empty type. As a consequence our subsumption rule uses a type-theory that is more general than the one of Barbanera et al. [1995], the theory of semantic subtyping $\mathfrak{C}$ rather than the type theory $\mathfrak{T}$ of Barbanera et al. [1995] of which semantic subtyping is a conservative extension (cf. Dezani-Ciancaglini et al. [2003]). The subsumption rule handles directly the addition of recursive types; negation and empty types are explicitly handled by the rules to type type-case expressions that we comment next.

The combination of the union rule $[\vee]$ with the three new rules $[\emptyset]$, $[\epsilon_1]$, $[\epsilon_2]$ is the key novelty of our type-system and, we claim, it captures the essence of occurrence typing. For one thing, thanks to this combination it is possible to type all the examples of [Tobin-Hochstadt and Felleisen 2010], all examples of [Castagna et al. 2022a], and several more examples that are captured by neither of these systems. Of course, to paraphrase a famous quotation [see Wikipedia 2021], with great power comes great algorithmic complexity, and thus to determine when an expression is well typed is more challenging with $[\vee]$ than in the cited systems. To see how this combination works

<footnote n="2">²Henceforth, for every constant of the language we suppose the existence of a singleton type containing that constant.</footnote>
it may be useful to see how type-case expressions are typed in the system by Frisch et al. [2002, 2008]. These, we remind, require an explicit binding to perform occurrence typing, and are typed by the following rule:

$$ \frac{\Gamma \vdash e' : s \quad (s \land \tau \approx \emptyset \text{ or } \Gamma, x : s \land \tau \vdash e_1 : t) \quad (s \land \neg \tau \approx \emptyset \text{ or } \Gamma, x : s \land \neg \tau \vdash e_2 : t)}{\Gamma \vdash (x := e' \in \tau) ? e_1 : e_2 : t} $$

In a nutshell, we know that $e'$ can yield only a result in $s$ and that this result will be bound to $x$; so we type $e_1$ only if $e'$ can yield a result in $\tau$ (i.e., $s \land \tau \neq \emptyset$) and in that case we can assume that the obtained value (bound to $x$) is of type $s \land \tau$; likewise for $e_2$. We can type exactly the same type-case by using $[\lor]$ combined with $[\emptyset]$, $[\in_1]$, and/or $[\in_2]$ and for that we do not need an explicit binding, since this is taken care of by $[\lor]$; our rules can directly type the expression in which we removed the binding, that is $e = (e' \in \tau) ? (e_1\{e'/x\}) : (e_2\{e'/x\})$, simply by noticing that this expression is equivalent to $((x \in \tau) ? e_1 : e_2)\{e'/x\}$, that $s \approx (s \land \tau) \lor (s \land \neg \tau)$, and then applying $[\lor]$. For instance, when both $s \land \tau$ and $s \land \neg \tau$ are different from $\emptyset$ we have:

$$ \frac{\Gamma \vdash \begin{array}{c} [\text{Ax}] \\ [\le] \\ [\in_1] \Gamma \vdash e' : s \end{array} \quad \frac{\Gamma, x:s \land \tau \vdash x : s \land \tau}{\Gamma, x:s \land \tau \vdash x : \tau} \quad \frac{\Gamma, x:s \land \tau \vdash e_1 : t}{\Gamma, x : s \land \tau \vdash (x \in \tau) ? e_1 : e_2 : t} \quad [\Gamma \vdash (x \in \tau) ? e_1 : e_2)\{e'/x\} : t}{\Gamma \vdash (x \in \tau) ? e_1 : e_2 : t} $$

and if either $s \land \tau$ or $s \land \neg \tau$ is empty, then we replace the corresponding $[\in_i]$ rule by $[\emptyset]$. In summary, the combination of $[\lor]$ with the three type-cases rule $[\emptyset]$, $[\in_1]$, and $[\in_2]$ encodes and simplifies the system by Frisch et al. [2002, 2008] moving the burden of the binding from the programmer to the type-system. But it also generalizes the approaches for occurrence typing defined by Tobin-Hochstadt and Felleisen [2010] and Castagna et al. [2022a] since the binding in $[\lor]$ is unconstrained, that is, it is not limited to the occurrences of an expression $e'$ that appear in some particular positions (e.g., in the tests of type-cases [Castagna et al. 2022a] or at the root of path expressions [Tobin-Hochstadt and Felleisen 2010]).

## 2.5 Type Soundness

It is well-known that subject-reduction (i.e., type preservation) does not hold in systems that, like ours, include the rule $[\lor]$. For instance, consider the expression ($f_3, f_3$) where $f:1 \to \text{Bool}$. Using the rule $[\lor]$, it can be typed by $(\text{True} \times \text{True}) \lor (\text{False} \times \text{False})$. However, after a step of reduction, we might get for instance the expression $(\text{true}, f_3)$, which cannot be typed by $(\text{True} \times \text{True}) \lor (\text{False} \times \text{False})$ anymore (the smallest type we can deduce for it is $(\text{True} \times \text{Bool})$). Nevertheless, our type system is sound in the sense of Wright and Felleisen [1994]:

**THEOREM 2.3 (TYPE SOUNDNESS).** If $\emptyset \vdash e : t$, then either $e$ diverges or $e \sim^* v$ with $\emptyset \vdash v : t$.

For instance, with the earlier example, even if $(\text{true}, f_3)$ cannot be typed by $(\text{True} \times \text{True}) \lor (\text{False} \times \text{False})$, it will finally reduce to $(\text{true}, \text{true})$ which is of type $(\text{True} \times \text{True}) \lor (\text{False} \times \text{False})$.

In order to prove this theorem, we introduce an alternative semantics which performs parallel reductions and that satisfies both subject reduction and progress (a typable expression is either a value or can be reduced). These two properties yield soundness for the parallel semantics. Finally, we prove that the parallel semantics is equivalent to the semantics introduced in Section 2.3, in the sense that for any expression $e$, if $e$ diverges with one semantics then it also diverges with the other, and if $e$ reduces to a value $v$ with one semantics then it also reduces to the value $v$ with the other. From this we deduce the soundness of our system. All the details are given in the appendix.
## 3 INTERMEDIATE SYSTEM: SYNTAX-DIRECTED RULES AND CANONICAL FORMS

We have seen that the previous system is sound, that is, that every well-typed term can only diverge or yield a result of the same type. Now the problem is to decide whether a given term is well typed or not. For that the rules of Figure 3 are not very useful since they allow too many different possibilities to type a given term. As customary, there are essentially two problems:

(1) the rules are not syntax directed: given a term, to type it we can try to apply some elimination/introduction rule, but also to apply the intersection rule $[\wedge]$, or the subsumption rule $[\le]$, or the union rule $[\vee]$.

(2) some rules are non-analytic.<fnref n="3" /> if we use the $[\rightarrow I]$ rule to type some $\lambda$-abstraction we do not know how to determine the type $t_1$ in the premise; if we use the $[\vee]$ rule we know neither how to determine $e'$ nor how to determine the types $t_1$ and $t_2$ that split the type of $e'$.

Notice that $[\vee]$ cumulates both problems. We tackle each problem in the order.

In the rest of this section we deal with rules that are not syntax directed. These are the intersection rule $[\wedge]$, the subsumption rule $[\le]$, and the union rule $[\vee]$ insofar as the expression in their conclusion can have any form. We adopt different solutions for the rules $[\wedge]$ and $[\le]$ and for the rule $[\vee]$. For $[\wedge]$ and $[\le]$ we simply eliminate them and embed the use of intersections and subtyping in the remaining rules. This essentially amounts to resorting to canonical derivations: we prove that it is possible to derive a type for a term if and only if there exists a derivation for that typing judgment in which intersection $[\wedge]$ and subsumption $[\le]$ rules are used only at determined specific places.<fnref n="4" /> For the union rule $[\vee]$ we add to the language a *binding* expression whose typing rule will replace the current $[\vee]$ rule. Since the binding expressions will explicitly determine both the subterm $e'$ and the variable $x$ to be used in a $[\vee]$ instance, then the introduction of bindings also addresses part the non-analyticity of the union rule.

In Section 4 we tackle the non-analyticity problem, or what it remains of it, namely, how to determine the type(s) to assign to a function parameter in a $[\rightarrow I]$ instance and the split types $t_1, t_2$ in a $[\vee]$ instance. We solve this problem by adding explicit type annotations for the variables bound in bind-expressions and $\lambda$-abstractions: these annotations will provide the information that is missing when applying the $[\rightarrow I]$ and $[\vee]$ rules. The rest of this section proceeds as follows:

(1) In Section 3.1 we introduce an intermediate language obtained by adding bind-expressions to the source language of Section 2.2.

(2) In Section 3.2 we define a syntax-directed type system for this intermediate language (with a small caveat for the union rule). We prove that this system is sound and complete with respect to the source language type system, in the sense that every well-typed term of the intermediate language encodes a valid derivation in the source language (soundness) and that every term of the source language is well typed only if there exists a term of the intermediate language that encodes one of its type derivations (completeness).

(3) In Section 3.3 we show that soundness and completeness hold also for a strict sub-language of the intermediate language. We call the terms of this sub-language the *MSC-forms* (maximal sharing canonical forms). The advantage of this sub-language is that there is a one-to-one correspondence between MSC-forms and the expressions of the source language and such a correspondence is effective since it is easy to transform every source language expression into “its” MSC-form.

<footnote n="3">³We consider *non-analytic* (or *synthetic*) a rule in which the input (i.e., $\Gamma$ and $e$) of the judgement at the conclusion is not sufficient to determine the inputs of the judgments at the premises (cf. [Martin-Löf 1994; Types 2019]).</footnote>

<footnote n="4">⁴Intuitively, a deduction is canonical if (i) subsumption is only used on the premises of application, type-case, union, and projection rules and (ii) intersection is only used for expressions that are $\lambda$-abstractions, that is, all the premises of an intersection rule are the consequence of a $[\rightarrow I]$. See the deduction system in Appendix A.3 and Lemmas D.5 and D.6.</footnote>
In this way, we reduced the problem of typing a source language expression to the one of typing "its" MSC-form, for which a syntax-directed type system exists. In Section 4 we show this to be equivalent to searching for a way to annotate this MSC-form to make it typable. The search for these annotations is performed by the algorithm described in Section 5.

## 3.1 Expressions with Bindings

Formally, we consider the following grammar of intermediate expressions (or expressions with bindings) ranged over by the meta-variable *e* so as to distinguish them from expressions of the source language (declarative expressions) for which we continue to use the non-bold symbol *e*.

$$ \textbf{Intermediate exprs} \quad e ::= c \mid x \mid \lambda x.e \mid ee \mid (e, e) \mid \pi_i e \mid (e \in \tau) \ ? e : e \mid \text{bind } x = e \text{ in } e \quad (6) $$

Intermediate expressions extend the syntax of declarative expressions by adding a new construction `bind x = e' in e`. Given an expression `bind x = e' in e` we call *e'* the *argument* of the expression and *e* the *body* of the expression. Such an expression is used to bind a variable to a definition. A bind-expression is different from a let-expression `let x = e' in e` (cf. Appendix C.1) as it is not associated with a call-by-value semantics: `bind x = e' in e` is just a way to indicate that a specific instance of the `[V]` rule must be used to type the expression, but it does not force the evaluation of the argument of the bind expression (call-by-need would be appropriate: cf. Appendix A.6).

## 3.2 Intermediate Typing Rules

We want to define a syntax-directed type-system for the expressions above. The addition of a binding expression makes `[V]` syntax-directed, but we still have to eliminate the intersection `[A]` and subsumption `[\le]` rules. In order to define the typing of applications and projections in the absence of subsumption we need some operators on types. Consider the rule `[\to E]` for applications of source language expressions (Figure 3). It essentially does three things: (i) it checks that the expression in the function position has a functional type; (ii) it checks that the argument is in the domain of the function, and (iii) it returns the type of the application. In systems without set-theoretic types these operations are straightforward: (i) corresponds to checking that that expression in the function position has an arrow type, (ii) corresponds to checking that the argument is in the domain of the arrow deduced for the function, and (iii) corresponds to returning the codomain of that arrow. With set-theoretic types things get more complicated, since in general the type of a function is not always a single arrow, but it can be a union of intersections of arrow types and their negations. Checking that the expression in the function position has a functional type is easy since it corresponds to checking that it has a type subtype of `0` to `1`. Determining its domain and the type of the application is more complicated and needs the operators `dom()` and `\circ` defined as `dom(t) def= max{u | t \le u \to 1}` and `t \circ s def= min{u | t \le s \to u}`. In short, `dom(t)` is the largest domain of any single arrow that subsumes `t` while `t \circ s` is the smallest codomain of an arrow type that subsumes `t` and has domain `s`. We need similar operators for projections since the type `t` of *e* in $\pi_i e$ may not be a single product type but, say, a union of products: all we know is that *t* must be a subtype of `1` to `1`. So let *t* be a type such that $t \le 1 \times 1$, we define $\pi_1(t) def= \min\{u | t \le u \times 1\}$ and $\pi_2(t) def= \min\{u | t \le 1 \times u\}$. All these type operators can be effectively computed (cf. Appendix A.4). We have now all the notions we need to define the syntax-directed type system for the intermediate language whose rules are given in Figure 4. The rules for constants, variables, and pairs are omitted since they are the same as in the deduction system for the declarative expressions. Contrary to the previous system, there no longer are explicit rules for intersection and subtyping: we want to have canonical derivations for which the deductions performed by these rules are distributed over the rest of the system. In particular, the only rule that introduces intersections is now the rule `[\to I-INT]` for $\lambda$-abstractions. The type subsumption rule `[\le]` is no longer needed since the
<figure><img src="image_5.png" /><figcaption>Fig. 4. Intermediate typing rules</figcaption></figure>

checks for the subtyping relation are performed in the elimination rules and in the two $[\epsilon_i]$ rules. The $[\to E-INT]$ rule works as we explained above: (i) it checks that the type $t_1$ of the expression in the function position is functional (i.e., $t_1 \le 0 \to 1$); (ii) it checks that the type $t_2$ of the argument is contained the domain of the function (i.e, $t_2 \le \text{dom}(t_1)$), and (iii) it returns the type $t_1 \circ t_2$ of the application. The product elimination rules check whether the argument of the projection is a product (i.e., $t_1 \le 1 \times 1$) and apply the corresponding type operator on this type.

The three rules for type-case expressions are essentially as before, bar two minor modifications. First, in the $[\epsilon_i-INT]$ rules the checked expression must be explicitly subsumed to either $t$ or $\neg t$ since there no longer is a $[\le]$ rule in our system to do that. Second, since we want our type-system to be syntax-directed, then we add the side condition $t_0 \ne 0$ in the $[\epsilon_i]$ rules so as to avoid any overlap with the $[0]$ rule and thus giving priority to the latter.

Finally, the $[\vee]$ rule (actually, $[\vee+])$ is encoded by a binding expression. We split the $[\vee+)$ in two rules. One, $[\vee_1-INT]$, is for the case when the variable $x$ in $e_2$ is not reachable (either because it is not free in $e_2$ or because it is in a type-case branch that cannot be selected such as in $(42 \in \text{Int}) ? 3 : x$). The other, $[\vee_2-INT]$, is the normal case for $[\vee+)$ where the bind-expression determines the variable $x$ and the expression $e_1$ to be substituted for it, but does not specify how to split the type of $e_1$ into a union of types. Notice that in $[\vee_1-INT]$ we added the side condition $x \notin \text{dom}(\Gamma)$: this condition is not necessary in $[\vee_2-INT]$ since (as in $[\vee]$ and $[\vee+])$ the environment $\Gamma$ is extended and, by Definition 2.2, the extension $\Gamma, x : t_j$ is defined only if $x \notin \text{dom}(\Gamma)$.

The system is syntax-directed: the form of the expression determines the rules to apply and the rules for a same form do not overlap (for bindings, $[\vee_1-INT]$ must be used only if $e_1$ is not typable: we will be more precise in Section 4).

*Soundness and completeness.* A well-typed expression of the intermediate language is typed by derivations in which every instance of the $[\vee]$ rule corresponds to a bind-expression. Any such derivation is also a canonical derivation for a particular expression of the source language. This expression can be obtained from the intermediate language expression by unfolding its bindings. Formally, this is obtained by the *unwinding* operation, noted $[.]$ and defined for the binding expressions as $[\text{bind } x = e_1 \text{ in } e_2] \stackrel{\text{def}}{=} [e_2]\{[e_1]/x\}$, as the identity for constants and variables, and homomorphically for all the other expressions (cf. Appendix A.5).

We can now prove that the problem of typing a declarative expression is equivalent to the problem of finding a typable intermediate expression whose unwinding is that declarative expression. In other terms, a declarative expression is typable if and only if we can enrich it with bindings so that it becomes a typable intermediate expression. This is formally stated by the theorems of soundness and completeness of the intermediate system:

**THEOREM 3.1 (SOUNDNESS).** If $\Gamma \vdash_I e : t$ then $\Gamma \vdash [e] : t$

**THEOREM 3.2 (COMPLETENESS).** If $\Gamma \vdash e : t$ then $\exists e', t' \text{ such that } [e'] \equiv_{\alpha} e, t' \le t$, and $\Gamma \vdash_I e' : t'$
## 3.3 Maximal Sharing Canonical Forms

The definition of the intermediate expressions is a step forward in solving the problem of typing a declarative expression, but it also brings a new problem, since we now have to decide where to add the bindings in a declarative expression so as to make it typable in the intermediate system. We get rid of this problem by defining the maximal sharing canonical forms (MSC-form for short). The idea is pretty simple, and consists in adding a new binding for every distinct (modulo α-conversion) sub-expressions of a declarative expression. Formally, this transformation yields a MSC-form:

**DEFINITION 3.3 (MSC FORMS).** An intermediate expression *e* is a maximal sharing canonical form if it is produced by the following grammar:

$$ \begin{array}{lclcl} \textbf{Atomic expressions} & \mathbf{a} & ::= & c \mid \lambda x.\mathbf{k} \mid (x, x) \mid xx \mid (x \in \tau) \mid ?x:x \mid \pi_l x & \\ \textbf{MSC-forms} & \mathbf{k} & ::= & x \mid \text{bind } x = \mathbf{a} \text{ in } \mathbf{k} & (7) \end{array} $$

and is α-equivalent to an expression *κ* that satisfies the following properties:

(1) if bind $x_1 = a_1$ in $κ_1$ and bind $x_2 = a_2$ in $κ_2$ are distinct sub-expressions of $κ$, then $[a_1] \neq_a [a_2]$;

(2) if $\lambda x.κ_1$ is a sub-expression of $κ$ and bind $y = a$ in $κ_2$ a sub-expression of $κ_1$, then $fv(a) \notin fv(\lambda x.κ_1)$;

(3) if bind $x = a$ in $κ'$ is a sub-expression of $κ$, then $x \in fv(κ')$.

MSC-forms, ranged over by $κ$, are variables possibly preceded by a list of bindings of variables to atoms. Atoms are either λ-abstractions whose body is a MSC-form or any other expression in which all proper sub-expressions are variables. Therefore, bindings can appear in a MSC-form either at top-level or at the beginning of the body of a function. MSC-forms are defined modulo α-conversion.<fnref n="5" /> Since MSC-forms are also intermediate expressions, then the typing rules and the definition of unwinding for intermediate terms of Section 3.2 apply to MSC-forms, too.

The syntactic form of MSC-forms guarantees that if a source language expression *e* is the unwinding of an MSC-form *κ*, then every distinct sub-expression of *e* is bound by a variable in *κ*, while the first property of Definition 3.3 guarantees that distinct variables bind distinct (i.e., non α-convertible) sub-expressions (i.e., this first property enforces the maximal sharing of common sub-expressions). The second property requires that bind-expressions must extrude λ-abstractions whenever possible. The third property guarantees that in a MSC-form there is no useless binding.

The first two properties of Definition 3.3 are important since they ensure that an expression of the source language is typable *if and only if* it is the unwinding of a typable MSC-form. For the first property, this is because reducing the bindings in an intermediate expression—while preserving unwinding—increases the typeability of a term: if we can type an intermediate term in which two distinct variables bind the same sub-expression, then the same term in which this sub-expression is bound by a single variable can also be typed by assigning to the unique variable the intersection of the types of the distinct variables, but the converse does not hold. For the second property this is because outer bindings may produce better types. For instance, consider the expression bind $x = a$ in $\lambda y.x$, where *a* is an expression that can be either an integer or a Boolean. This expression can be typed with ($1 \to \text{Int}$) $\lor$ ($1 \to \text{Bool}$). However, for the expression $\lambda y$. (bind $x = a$ in $x$) which has the same unwinding as the previous one, the most precise type one can deduce is $1 \to (\text{Int} \lor \text{Bool})$, which is strictly larger than ($1 \to \text{Int}$) $\lor$ ($1 \to \text{Bool}$).

The last property of Definition 3.3 is important because it ensures that given a source language expression *e* there exists a unique (modulo α-conversion and the order of bindings) MSC-form whose unwinding is *e* (cf. Proposition 3.5): we denote this MSC-form by MSC(*e*).

Given a source language expression *e* it is easy to produce its unique MSC-form MSC(*e*). For space constraints we give the formal definition of the transformation and all details in the Appendixes A.7

<footnote n="5">⁵For instance, both $\lambda x.bind z = xy$ in $zy$ and $\lambda x.bind z = xy$ in $z$ are two distinct atoms that can occur in the same MSC-form, even though the atom $xy$ appears in both: an α-renaming of $x$ makes the first MSC-property hold.</footnote>
and A.8, but in practice what the transformation needs to do is to visit *e* bottom up and generate a distinct binding for each distinct sub-expression, taking special care for free-variables, when extruding abstractions, and for α-convertible expressions (see Section 6 for more details).

We just got rid of the problem of determining where to put the bindings in a source language expression *e*: generate MSC(*e*) and try to type it in the syntax-directed system of Section 3.2.

Formally, we define the following congruence on MSC-forms:

**DEFINITION 3.4 (CANONICAL EQUIVALENCE).** We denote by $\equiv_\kappa$ the smallest congruence on MSC-forms that is closed by $\alpha$-conversion and such that

$$ \text{bind } x_1 = a_1 \text{ in bind } x_2 = a_2 \text{ in } \kappa \quad \equiv_{\kappa} \quad \text{bind } x_2 = a_2 \text{ in bind } x_1 = a_1 \text{ in } \kappa \quad x_1 \notin \text{fv}(a_2), x_2 \notin \text{fv}(a_1) $$

Then we prove that all the MSC forms of a source language expression are equivalent:

**PROPOSITION 3.5.** If $\kappa_1$ and $\kappa_2$ are two MSC-forms and $[\kappa_1] \equiv_\alpha [\kappa_2]$, then $\kappa_1 \equiv_\kappa \kappa_2$.

(Proof hint). Given two MSC-forms with the same unwinding, conditions (1) and (3) of Definition 3.3 ensure that there is a one-to-one correspondence between their bindings, and condition (2) that each binding is located in the outermost possible $\lambda$. So the two MSC-forms differ by the relative order between independent bindings that are in the same $\lambda$-abstraction or at top-level and, thus, are equivalent. □

It is easy to observe that the canonical equivalence preserves typeability (this is a direct consequence that type environments are mappings in which order does not matter). Thus, the corollary of this proposition is that an expression *e* is typable if and only if its unique (modulo $\equiv_\kappa$) MSC-form is typable, too. Formally, let MSC(*e*) be any element of the set $\{\kappa \mid e \equiv_\alpha [\kappa]\}$, then

**COROLLARY 3.6 (SOUNDNESS AND COMPLETENESS).** For every closed term *e* of the source language

$$ \vdash e : t \quad \Rightarrow \quad \vdash_I \text{MSC}(e) : t' \le t \quad \text{(completeness)} $$

$$ \vdash e : t \quad \Leftarrow \quad \vdash_I \text{MSC}(e) : t \quad \text{(soundness)} $$

Corollary 3.6 states that given a source language expression *e* it is typable if and only if MSC(*e*) is: we reduced the problem of typing *e* to the one of typing MSC(*e*), a form that we can effectively produce from *e* and for which we have a syntax-directed type system.

# 4 ALGORITHMIC SYSTEM: ADDING TYPE ANNOTATIONS

The intermediate type system of Figure 4 is not algorithmic since it still contains non-analytic rules: we neither know which decomposition in $t_i$'s to use when applying the $[\vee_2\text{-INT}]$ rule, nor which $t_j$'s to choose when applying the $[\rightarrow\text{I-INT}]$ rule. To solve this problem, we enrich our intermediate language with annotations that determine the types to use when typing a bind expression or a $\lambda$-abstraction. It is then straightforward to define an algorithmic system (i.e., a syntax-directed system composed only of analytic rules) for these enriched expressions and prove it to be sound and complete with respect to the system of the intermediate language.

*Annotations.* In a nutshell, we consider expressions of the form $\lambda x:A.e$ and bind $x:A = e$ in $e$, where *A* ranges over annotations of the form $\{\Gamma \vdash t, \dots, \Gamma \vdash t\}$. Our annotations are, thus, finite relations between type environments and types. An annotation of the form $x : \{\Gamma_i \vdash t_i\}_{i \in I}$ indicates that under the hypothesis $\Gamma_i$ the variable *x* is assumed to be of type $t_i$.

We write $\{t_1, \dots, t_n\}$ for $\{\emptyset \vdash t_1, \dots, \emptyset \vdash t_n\}$ and just $t$ for $\{\emptyset \vdash t\}$. So for instance we write $\lambda x:t.e$ for $\lambda x:\{\emptyset \vdash t_1, \dots, \emptyset \vdash t_n\} = e_1$ in $e_2$ stands for bind $x:\{\emptyset \vdash t_1, \dots, \emptyset \vdash t_n\} = e_1$ in $e_2$.

In this system terms encode derivations. Terms with simple annotations such as $\lambda x:t.e$ represent derivations as they can be found in the simply-typed $\lambda$-calculus: in other terms, to type the function the system must look for a type *s* such that $\lambda x:t.e$ is of type $t \rightarrow s$.

When annotations are sets of types, such as in $\lambda x:\{t_1, \dots, t_n\}.e$, then the term represents a derivation for an intersection type, such as the derivations that can be found in semantic subtyping
calculi: in other terms, to type the function the system looks for a set of types {$s_1, ..., s_n$} such that $\lambda x:\{t_1, ..., t_n\}.e$ has type $\bigwedge_{i=1}^n t_i \rightarrow s_i$.

Finally, the reason why we need the more complex annotations of the form {$\Gamma_1 \triangleright t_1, ..., \Gamma_1 \triangleright t_1$} can be shown by an example. Consider $\lambda x.((\lambda y.(x, y))x)$: in the declarative system we can deduce for it the type $(\mathbf{Int} \rightarrow \mathbf{Int} \times \mathbf{Int}) \wedge (\mathbf{Bool} \rightarrow \mathbf{Bool} \times \mathbf{Bool})$. We must find the annotations $A_1$ and $A_2$ such that $\lambda x:A_1.((\lambda y:A_2.(x, y))x)$ has type $(\mathbf{Int} \rightarrow \mathbf{Int} \times \mathbf{Int}) \wedge (\mathbf{Bool} \rightarrow \mathbf{Bool} \times \mathbf{Bool})$. Clearly $A_1 = \{\mathbf{Int}, \mathbf{Bool}\}$. However, the typing of the parameter $y$ depends on the typing of $x$: when $x:\mathbf{Int}$ then $y$ must have type $\mathbf{Int}$ (the type of $y$ must be larger than the one of $x$—the argument it will be bound to—, but also smaller than $\mathbf{Int}$ so as to deduce that $\lambda y.(x, y)$ returns a pair in $\mathbf{Int} \times \mathbf{Int}$). Likewise when $x:\mathbf{Bool}$, then $y$ must be of type $\mathbf{Bool}$, too. Therefore, we use as $A_2$ the annotation {$x:\mathbf{Int} \triangleright \mathbf{Int}, x:\mathbf{Bool} \triangleright \mathbf{Bool}$}, which precisely states that when $x:\mathbf{Int}$, then we must suppose that $y$ (the variable annotated by $A_2$) is of type $\mathbf{Int}$, and likewise for $\mathbf{Bool}$. Using the typing rules we describe in the next section we are then able to deduce that $\lambda x:\{\mathbf{Int}, \mathbf{Bool}\}. (\lambda y:\{x:\mathbf{Int} \triangleright \mathbf{Int}, x:\mathbf{Bool} \triangleright \mathbf{Bool}\}. (x, y))x$ has type $(\mathbf{Int} \rightarrow \mathbf{Int} \times \mathbf{Int}) \wedge (\mathbf{Bool} \rightarrow \mathbf{Bool} \times \mathbf{Bool})$. Because of this last form of annotations, these annotations are strictly more expressive than those of the functional core of CDuce presented in [Frisch et al. 2008]: even if CDuce is a calculus with explicit full annotations, it is not possible to decorate $\lambda x.((\lambda y.(x, y))x)$ with a (CDuce) annotation so that the resulting term has type $(\mathbf{Int} \rightarrow \mathbf{Int} \times \mathbf{Int}) \wedge (\mathbf{Bool} \rightarrow \mathbf{Bool} \times \mathbf{Bool})$: CDuce annotations are exactly as expressive as our {$\emptyset \triangleright t_1, ..., \emptyset \triangleright t_n$} annotations.

In the preceding paragraphs we explained how our annotations work by using as examples expressions of the intermediate language. However, recall that our ultimate goal is to type the expressions of the *source language* we introduced in Section 2.2 and, as we saw in the previous section, for that one does not need to consider the whole intermediate language: the MSC-forms suffice. This is why in the rest of this section we add annotations *only to MSC-forms*: the definitions and results of this section can be easily extended to all expressions of the intermediate language.

## 4.1 Algorithmic Expressions and Typing Rules

Formally, we consider the following grammar of *explicitly annotated MSC-forms* (or *algorithmic expressions*)—i.e., MSC-forms as per Definition 3.3 enriched with annotations—ranged over by the meta-variable $\kappa$ (to distinguish them from the unannotated MSC-forms ranged over by $\kappa$).

$$ 
\begin{array}{l@{\qquad}l}
\textbf{Annotations} & A ::= \{\Gamma \triangleright t_1, \dots, \Gamma \triangleright t_n\} \\
\textbf{Algorithmic Atoms} & a ::= c \mid \lambda x:A.\kappa \mid (x, x) \mid xx \mid (x \in \tau) \mid x:x \mid \pi_i x \quad (8) \\
\textbf{Algorithmic Expressions} & \kappa ::= x \mid \text{bind } x:A = a \text{ in } \kappa
\end{array}
$$

These enrich the syntax of MSC-forms by inserting an annotation wherever a variable is introduced by a binder (either a “$\lambda$” or a “bind”). We use $\varphi$ to range over either atoms $a$ or expressions $\kappa$.

For the algorithmic typing rules we need to define the following pre-order on type environments:

**DEFINITION 4.1 (ENVIRONMENT SUBSUMPTION).** *Given two type environments $\Gamma$ and $\Gamma'$, we say that $\Gamma'$ subsumes $\Gamma$, written, $\Gamma \leq \Gamma'$ if and only if $\forall x \in \text{dom}(\Gamma')$ we have $\Gamma(x) \leq \Gamma'(x)$.*

The algorithmic type system is then given by the rules for abstractions and binding in Figure 5 plus all the other rules of the intermediate type system (specialized for MSC-forms, i.e., where every subexpression is a variable: cf. Figure 4 and Appendix A.9). The introduction of intersections is driven by the annotation {$\Gamma_i \triangleright t_i$}$_{i \in I}$ of the $\lambda$-abstraction: for every $t_j$ whose hypotheses $\Gamma_j$ subsume the current environment $\Gamma$, the system checks whether the function has type $t_j \rightarrow s_j$, that is, under the hypothesis that $x: t_j$ it tries to infer a type $s_j$ for the body $\kappa$ of the function; the condition $J \neq \emptyset$ ensures that at least one $\Gamma_i$ subsumes $\Gamma$. Bind expressions are still handled by the two rules $[\vee_1 \text{-}\mathbf{Int}]$ and $[\vee_2 \text{-}\mathbf{Int}]$. The first one, $[\vee_1 \text{-}\mathbf{Int}]$, is for the case when the variable $x$ is not reachable in $\kappa$. It is used when the current environment $\Gamma$ is not subsumed by any of the environments in
$$ [\rightarrow \text{I-ALG}] \frac{(\forall j \in J) \quad \Gamma, x : t_j \vdash_{\mathcal{A}} \kappa : s_j}{\Gamma \vdash_{\mathcal{A}} \lambda x : \{\Gamma_i \vdash t_i\}_{i \in I} \wedge \bigwedge_{j \in J} t_j \rightarrow s_j} \quad J = \{i \in I | \Gamma \leq \Gamma_i\} \neq \emptyset $$

$$ [\text{V}_1\text{-ALG}] \frac{\Gamma \vdash_{\mathcal{A}} \kappa : s}{\Gamma \vdash_{\mathcal{A}} \text{bind} x : \{\Gamma_i \vdash t_i\}_{i \in I} = a \text{ in } \kappa : s} \quad \begin{array}{l} x \notin \text{dom}(\Gamma) \\ \{i \in I | \Gamma \leq \Gamma_i\} = \emptyset \end{array} $$

$$ [\text{V}_2\text{-ALG}] \frac{\Gamma \vdash_{\mathcal{A}} a : \bigvee_{j \in J} t_j \quad (\forall j \in J) \quad \Gamma, x : t_j \vdash_{\mathcal{A}} \kappa : s_j}{\Gamma \vdash_{\mathcal{A}} \text{bind} x : \{\Gamma_i \vdash t_i\}_{i \in I} = a \text{ in } \kappa : \bigvee_{j \in J} s_j} \quad J = \{i \in I | \Gamma \leq \Gamma_i\} \neq \emptyset $$

<caption>Fig. 5. Algorithmic typing rules</caption>

the annotation of $x$. The other, $[\text{V}_2\text{-ALG}]$, is the normal case for $[\text{V}+]$ where the bind-expression determines both the variable $x$ and the atom $a$ to be substituted for it, and where its annotation determines how to split the type of $a$ into a union of types.

The first important property satisfied by the algorithmic type system is that it is syntax directed and composed only by analytic rules (a simple visual check of the rules in Appendix A.9 suffices to verify it). As such it describes a deterministic algorithm to infer the type of an algorithmic expression. Furthermore, it is also decidable (this can be proved by a simple induction on the structure of the term, by observing that the subtyping relation is decidable, and that the operators used in the rules can be effectively computed: cf. Frisch et al. [2008, Section 6] and Appendix A.4).

The main interest of the algorithmic system is that a well-typed algorithmic term univocally encodes a type derivation for a MSC-form and, in virtue of Corollary 3.6, it also encodes a particular canonical derivation for a source language expression. The source language expression at issue is the one obtained by erasing the annotations from our algorithmic term and then applying the unwinding operation defined in Section 3.2. The annotation erasing operation, noted $\langle\cdot,\cdot\rangle$, is defined as $\langle\text{bind} x:A=a \text{ in } \kappa\rangle \stackrel{\text{def}}{=} \text{bind} x=\langle a\rangle \text{ in } \langle\kappa\rangle$, $\langle\lambda x:A.\kappa\rangle \stackrel{\text{def}}{=} \lambda x.\langle\kappa\rangle$, and as the identity otherwise. We can now prove that the problem of typing an MSC-form is equivalent to the problem of decorating it with some annotations that make it typable with the algorithmic type system. This is formally stated by the theorems of soundness and completeness of the system for algorithmic expressions (ranged over $\kappa$) with respect to the unannotated MSC-forms (ranged over $\kappa$):

**THEOREM 4.2 (SOUNDNESS).** If $\Gamma \vdash_{\mathcal{A}} \kappa : t$ then $\Gamma \vdash_{\text{I}} \langle\kappa\rangle : t$

**THEOREM 4.3 (COMPLETENESS).** If $\Gamma \vdash_{\text{I}} \kappa : t$, then $\exists \kappa \text{ such that } \langle\kappa\rangle = \kappa \text{ and } \Gamma \vdash_{\mathcal{A}} \kappa : t' \leq t$

Soundness states that if an algorithmic expression is well-typed, then removing its annotations gives a well-typed MSC-form. Completeness states that every well-typed MSC-form can be decorated with annotations so that it becomes a well-typed algorithmic expression.

By combining these theorems with the previous results on the intermediate language, we obtain the soundness and completeness of the algorithmic system with respect to the source language.

**COROLLARY 4.4 (ALGORITHMIC SOUNDNESS AND COMPLETENESS).**

$$ \vdash_{\mathcal{A}} \kappa : t \Rightarrow \vdash [\langle\kappa\rangle] : t \qquad (\text{soundness}) $$

$$ \vdash e : t \Rightarrow \exists \kappa . \vdash_{\mathcal{A}} \kappa : t' \leq t \text{ and } [\langle\kappa\rangle] \equiv_{\alpha} e \qquad (\text{completeness}) $$

Notice that in the statement of completeness $[\langle\kappa\rangle] \equiv_{\alpha} e$ is equivalent to writing $\langle\kappa\rangle = \text{MSC}(e)$. Combining this with the soundness result yields that for every closed declarative expression $e$, if $\vdash_{\mathcal{A}} \kappa : t$ and $\langle\kappa\rangle = \text{MSC}(e)$, then $\vdash e : t$. All this gives us a procedure to check whether an expression $e$ of the source language is well typed or not: produce $\text{MSC}(e)$ and look for a way to annotate it so that it becomes a well-typed algorithmic expression $\kappa$. If we find such annotations, then the soundness property tells us that $e$ is well typed. If such annotations do not exist, then the completeness property tells us that $e$ is not well-typed.

In the next section we describe a sound algorithm to search for such annotations.
# 5 ALGORITHM FOR RECONSTRUCTING ANNOTATIONS

We define an algorithm to reconstruct annotations for an MSC-form to make it become a well-typed algorithmic expression. It starts by annotating all the bindings of the MSC-form by 1 (the weakest possible annotation) and performs several passes to refine these annotations until it either obtains a well-typed algorithmic expression or it fails.

At each pass the algorithm takes as input a type environment $\Gamma$, an algorithmic expression $\kappa$, and a type $t$ and checks whether $\kappa$ can be given the type $t$ under the hypothesis $\Gamma$. The check yields one of three possible results: either (i) success with an expression $\kappa'$ obtained from $\kappa$ by refining some annotations—meaning that it is possible to deduce from $\Gamma$ the type $t$ for $\kappa'$—, or (ii) a failure—meaning that the algorithm cannot propose any better refinement of the annotations to type the expression—, or (iii) a refined expression $\kappa'$ and a set of type environments that refine $\Gamma$—meaning that it is not yet possible to deduce $t$ for $\kappa'$ under $\Gamma$ and that the algorithm must try further passes using the new type environments returned by this pass.

Formally, passes are defined by a deduction system whose judgments are of the form $\Gamma \vdash_R \varphi : t \Rightarrow (\varphi', \Gamma)$, where $\Gamma$ denotes a possibly empty set of type environments, $t$ is a type, and $\varphi, \varphi'$ are either algorithmic atoms or algorithmic expressions as defined in (8). $\Gamma, \varphi$, and $t$ form the input of the pass while $\varphi'$ and $\Gamma$ are the output and they refine $\varphi$ and $\Gamma$, respectively. The reason why the output is a pair is because we want to refine the type of all the variables in the input expression $\varphi$: the types of the variables that are free in $\varphi$ are refined by providing new environments that refine the input environment $\Gamma$, yielding $\Gamma$; the types of the variables that are bound in $\varphi$ are refined by refining their annotations in $\varphi$, yielding $\varphi'$.

Given a judgment $\Gamma \vdash_R \varphi : t \Rightarrow (\varphi', \Gamma)$, an empty $\Gamma$ means failure while if $\Gamma$ is the singleton $\{\Gamma\}$, this means success. For instance, the rules for constants in the deduction system are:

$$ \begin{array}{l} \text{[CONST]} \qquad \frac{b_c \le t}{\Gamma \vdash_R c : t \Rightarrow (c, \{\Gamma\})} \qquad \text{[CONSTUNTYPABLE]} \qquad \frac{b_c \not\le t}{\Gamma \vdash_R c : t \Rightarrow (c, \{\})} \end{array} $$

The system succeeds in checking that a constant $c$ has a supertype of $b_c$ and fails otherwise. Notice that the atom in the result is the same as in the input, since in a constant there is no annotation to refine (this is true for all the rules for atoms excluding $\lambda$-abstractions).

If a pass neither fails nor succeeds, then it proposes a refinement of the types of the variables in the expression, refinement that is to submit to a further pass. This corresponds to a judgment $\Gamma \vdash_R \varphi : t \Rightarrow (\varphi', \{\Gamma_1, \dots, \Gamma_n\})$: for the variables that are bound in $\varphi$ it proposes a refinement by refining the annotations in $\varphi$ yielding the new expression $\varphi'$; for the variables that are free in $\varphi$, it proposes a refinement of the environment $\Gamma$ by proposing the refinements $\Gamma_1 \dots \Gamma_n$. The type of a variable is refined in two ways: either it can be restricted to match the usage of the variable or it can be split when it is the union of simpler types (to determine a unique split of unions, the rules use the disjunctive normal forms of [Frisch et al. 2008]: cf. Appendix B.1). For instance, if we try to type the atom $\pi_1 x$ and the current annotation/environment for $x$ is a type $t$ that does not contain only pairs, then the algorithm proposes to refine the type of $x$ into $t \wedge (1 \times 1)$; if the type $t$ is a union of products such as $(s_1 \times s_2) \vee (t_1 \times t_2)$, then the algorithm suggests to split the type of $x$ into two separate types $(s_1 \times s_2)$ and $(t_1 \times t_2)$. Both these refinements are done by the rules for projections:

$$ \begin{array}{l} \text{[PROJ1]} \qquad \frac{\Gamma(x) \wedge (t \times 1) \simeq \bigvee_{i \in I} t_i \times s_i}{\Gamma \vdash_R \pi_1 x : t \Rightarrow (\pi_1 x, \{\Gamma[x : \triangleq t_i \times s_i]\}_{i \in I})} \qquad \text{[PROJ2]} \qquad \frac{\Gamma(x) \wedge (1 \times t) \simeq \bigvee_{i \in I} t_i \times s_i}{\Gamma \vdash_R \pi_2 x : t \Rightarrow (\pi_2 x, \{\Gamma[x : \triangleq t_i \times s_i]\}_{i \in I})} \end{array} $$

where $\Gamma[x : \triangleq t]$ is the environment obtained by refining the binding of $x$ in $\Gamma$ by intersecting it with $t$, that is, $\Gamma[x : \triangleq t] \stackrel{\text{def}}{=} (\Gamma \setminus \{x \mapsto \Gamma(x)\}) \cup \{x \mapsto \Gamma(x) \wedge t\}$ for $x \in \text{dom}(\Gamma)$. The rules force the projections to have the checked type $t$ by intersecting the type of $x$ with $(t \times 1)$ or $(1 \times t)$, and split
the resulting type into the different summands by proposing different refinements of the current environment $\Gamma$. Again, the returned atom is the same as in the input, since there are no annotations to refine in it. The inference for occurrence typing is performed by the rule for type-cases:

$$ [\text{\textbf{CASE}}] \frac{\Gamma \vdash_{\mathcal{R}} (x \in s) ? x_1 : x_2 : t \Rightarrow ((x \in s) ? x_1 : x_2, \{\Gamma[x : \triangleq s][x_1 : \triangleq t], \Gamma[x : \triangleq \neg s][x_2 : \triangleq t]\})}{\Gamma \vdash_{\mathcal{R}} x_1 x_2 : t} $$

In order to analyze the test that $x$ has type $s$, the rule [CASE] splits the current type of $x$ by intersecting it with $s$ and $\neg s$, a split that it proposes in the two refinements $\Gamma[x : \triangleq s]$ and $\Gamma[x : \triangleq \neg s]$ given in the result of the conclusion. The first refinement corresponds to the selection of the “then” branch, that is of $x_1$. Since the rule requires the whole expression to be of type $t$, then the first type environment also refines the type of $x_1$ with $t$. Likewise for the second environment and $x_2$. An important though pretty hidden detail is that the notation for the refinement of type environments handles the cases in which two or more variables coincide: for instance if $x = x_1$, then the rule [CASE] will refine $\Gamma(x)$ in the first refinement by intersecting it both with $s$ and with $t$. In all the rules presented in this section we suppose that the intersections occurring in them are not empty: the cases for empty types are handled by other rules, omitted here (see Appendix B.3).

The reason why we may split the type of a variable $x$ when its type is a union or when we test it dynamically can be understood by considering the typing rule $[\vee_2\text{-ALG}]$ in Figure 5: we are trying to reconstruct the annotation for $x$ in the conclusion of $[\vee_2\text{-ALG}]$ and thus determine the environments compatible with the current one that should be used in this annotation. However, $[\vee_2\text{-ALG}]$ is not the only rule that splits the derivation in sub-derivations with different environments: also $[\rightarrow\text{I-ALG}]$ does it, with the difference that it does not split a union or a tested case, but it splits an intersection of arrows. We encounter this split of intersections in the rules for applications, in particular in [APPR]. These rules are defined as follows (we present a simplified version):

$$ [\text{APPR}] \frac{\Gamma(x_1) \simeq \bigwedge_{i \in I} (s_i \rightarrow t_i)}{\Gamma \vdash_{\mathcal{R}} x_1 x_2 : t \Rightarrow (x_1 x_2, \{\Gamma[x_1 : \triangleq ((s_i \wedge \Gamma(x_2)) \rightarrow t)][x_2 : \triangleq s_i]\}_{i \in I})} $$ $$ [\text{APPL}] \frac{\Gamma(x_1) \wedge (\emptyset \rightarrow \mathbf{1}) \simeq \bigvee_{i \in I} s_i}{\Gamma \vdash_{\mathcal{R}} x_1 x_2 : t \Rightarrow (x_1 x_2, \{\Gamma[x_1 : \triangleq s_i]\}_{i \in I})} $$

The type of a functional expression is in general a union of intersections of arrows (cf. Frisch et al. [2008]). When it is a union then, as for any other algorithmic atom, the system splits this union into distinct type environments, here in the rule [APPL]. Then each summand (which is an intersection of arrows) is separately checked by the rule [APPR] which deserves a detailed explanation. The hypothesis about $x_1$ is that it is bound to a function whose type is an intersection of arrows. For each arrow $s_i \rightarrow t_i$ in this intersection, the rule proposes a refined environment $\Gamma_i$ in which both the type of $x_1$ and the type of $x_2$ are refined: the first by intersecting it with $(s_i \wedge \Gamma(x_2)) \rightarrow t$, to ensure that the application uses the right domain and will yield a result not only in $t_i$ (since $\Gamma(x_1) \le s_i \rightarrow t_i$), but also in $t$ (and, thus, in $t_i \wedge t$); the second by intersecting it with $s_i$ since the argument must be in the domain of $x_1$. The intuition is that these different $\Gamma_i$ correspond to the different typing checks performed by the rule $[\rightarrow\text{I-ALG}]$ to type the body of the function bound to $x_1$. It is important to stress that, as in previous cases, an environment $\Gamma_i$ is added to the result only if $\Gamma(x_2) \wedge s_i$ is not empty since we want to discard from the type of $x_1$ the arrows whose domain is not compatible with the current typing of the argument. Likewise, if the intersection in [APPL] is empty, then this produces an empty set of refinements, meaning failure since we are applying to some argument an expression that is not a function.

All the rules we have seen so far are actually axioms (we only considered atoms in which the only subexpressions are variables) in which the returned expression is the same as in the input (there are no annotations to refine). The bulk of the inference work is done in the rules for binding expressions
$$
\begin{align*}
& [\text{BINDARGSKIP}] \quad \frac{(\Gamma \vdash A) = \{\}}{\Gamma \vdash_R \text{bind} x:A = a \text{ in } \kappa : t \Rightarrow (\kappa', \Gamma)} \\
& [\text{BINDARGUNTYP}] \quad \frac{\Gamma \vdash_R a : \bigvee (\Gamma \vdash A) \Rightarrow (a', \{\})}{\Gamma \vdash_R \text{bind} x:A = a \text{ in } \kappa : t \Rightarrow (\kappa', \Gamma)} \\
& [\text{BINDARGREFENV}] \quad \frac{\Gamma \vdash_R a : \bigvee (\Gamma \vdash A) \Rightarrow (a', \Gamma)}{\Gamma \vdash_R \text{bind} x:A = a \text{ in } \kappa : t \Rightarrow (\kappa', \Gamma \cup \{\Gamma\})} (\Gamma \not\supseteq \{\Gamma\}) \\
& [\text{BINDARGREFANNS}] \quad \frac{\Gamma \vdash_R a : \bigvee (\Gamma \vdash A) \Rightarrow (a', \{\Gamma\}) \quad \Gamma \vdash_R \text{bind} x:A = a' \text{ in } \kappa : t \Rightarrow (\kappa', \Gamma)}{\Gamma \vdash_R \text{bind} x:A = a \text{ in } \kappa : t \Rightarrow (\kappa', \Gamma)} (a' \neq a) \\
& [\text{BIND}] \quad \frac{\Gamma \vdash_R a : \bigvee (\Gamma \vdash A) \Rightarrow (a, \{\Gamma\}) \quad \Gamma \vdash_R a : s \quad \{s_i\}_{i \in I} = \text{partition}(\{s \wedge u \mid u \in (\Gamma \vdash A)\}) \quad (\forall i \in I) \quad \Gamma, (x : s_i) \vdash_R \kappa : t \Rightarrow (\kappa_i, \Gamma_i) \quad \Gamma'_i = \text{propagate}_{x,a,s_i}(\Gamma_i) \quad (A_i, \Gamma''_i) = \text{extract}_x(\Gamma'_i)}{\Gamma \vdash_R \text{bind} x:A = a \text{ in } \kappa : t \Rightarrow (\text{bind} x: \cup_{i \in I} A_i = a' \text{ in merge}(\{\kappa_i\}_{i \in I}), \cup_{i \in I} \Gamma''_i)}
\end{align*}
$$

<caption>Fig. 6. Reconstruction rules for bind-expressions</caption>

(and in those for $\lambda$-abstractions that are conceptually similar to those for bindings). The complete set of rules for bind-expressions are presented in Figure 6 in their priority order: a rule can be applied only if the previous rules cannot (we just did two slight simplifications in the first and third rule: cf. Appendix B.3). These rules use some auxiliary definitions. We note by $(\Gamma \vdash A)$ the set of the types of the annotation $A$ that are compatible with $\Gamma$, that is, $(\Gamma \vdash A) \stackrel{\text{def}}{=} \{t \mid \Gamma' \vdash t \in A \text{ and } \Gamma \le \Gamma'\}$, and by $\bigvee(\Gamma \vdash A)$ the union of these types, that is, $\bigvee_{t \in (\Gamma \vdash A)} t$.

To check that the bind-expression bind x:A = a in k has type t under the hypotheses Γ, the system first focuses on the argument a of the bind-expression using the first four rules in Figure 6. If no type in A is compatible with the current environment Γ (i.e., (Γ>Λ) is empty), then the bind is skipped and the system tries to type the body k of the expression without using x: no type assumption for x is added to Γ and the annotation is emptied (rule [BINDARGSKIP]). If instead (Γ>Λ) is not empty, then the argument a must have a type smaller than the union of all types in (Γ>Λ). Thus the system tries to check under the current hypothesis Γ whether a can be given the type $\bigvee(\Gamma>Λ)$. The result of this check is a pair (a', Π) according to which we can distinguish four different outcomes, corresponding to the last four rules. (1) the check failed, that is, it returned an empty Π (rule [BINDARGUNTYP]): then this binding must be skipped and we proceed as for rule [BINDARGSKIP]. (2) the check did not succeed but it proposed a set of refinements for Γ (and, possibly, for a), that is, Π ≠ {Γ} ([BINDARGREFENV]): then before attacking the body k of the bind expression, the system proposes these refinements for the whole bind-expression updated with the refined argument a'; furthermore, since the first premise of the rules does not guarantee a to be well-typed, then the current environment Γ is also returned for the cases in which this should fail. (3) the test succeeded (i.e., Π = {Γ}) and proposed a refinement a' of a different from it (i.e., a ≠ a', rule [BINDARGREFANNS]): since we do not know whether a' is the best possible refinement for the argument, yet, then before attacking the body k the system retries to check the expression using the new refinement a' for argument. Finally, (4) the check for the argument succeeded (i.e., Π = {Γ}) and it proposed its best refinement for the argument (i.e., a = a'): then the system can attack the body k of the bind-expression, which is done in the rule [BIND].

The [BIND] rule is, by far, the most complex rule of our system and needs several auxiliary definitions. First, [BIND] uses the algorithmic system to deduce the best type s for the argument a, since this can be a strict subtype of $\bigvee(\Gamma>Λ)$. Then it uses this type s to refine the types in the
annotation A that are compatible with the current $\Gamma$, yielding the set $\{s \wedge u \mid u \in (\Gamma \triangleright A)\}$. The function partition is applied to this set: this splits the types in the set so that they are pairwise disjoint (actually, two types with a non-empty intersection are split in three types: their intersection and their two differences).<fnref n="6" /> This yields a set of types $\{s_i\}_{i \in I}$ which are the summands into which we want to split the type of the argument for the union rule: indeed we have $\Gamma \vdash_R a : s = \bigvee_{i \in I} s_i$. Therefore the next step it to check that for each $i \in I$ the body $\kappa$ of the bind-expression has type $t$ under the hypothesis that $x$ has type $s_i$. This gives a set of result pairs $\{(\kappa', \Gamma_i)\}_{i \in I}$. We must extract from this set the appropriate information to elaborate the result for the whole bind-expression.

Using the various $\kappa_i$'s is easy: all these are copies of $\kappa$ with refined annotations, and we merge all of them simply by unioning the corresponding annotations: this is what the merge function occurring in the conclusion of the rule does. Using the various $\Gamma_i$'s requires more work, since the type environments in $\Gamma_i$ contain hypotheses about the variable $x$ defined in the examined bind-expression. In particular, if the type for $x$ has been refined, then we have to reflect this refinement to the free variable of $a$, since $a$ is bound to $x$. Consider a $\Gamma'$ in $\Gamma_i$ for some $i$. If the type of $x$ has been refined in $\Gamma'$, that is, if $\Gamma'(x) \neq s_i$, then we have to refine in $\Gamma'$ also the free variables of $a$. For instance imagine that $a$ is $(x_1, x_2)$, $s_i = 1 \times 1$, and $\Gamma'(x) = (\text{Int} \times \text{Int}) \lor (\text{Bool} \times \text{String})$. Since $\Gamma'(x)$ is strictly smaller than $s_i$, then we have to refine the types of the variables in $a$ by proposing two refinements for $\Gamma'$, namely, $\Gamma'[x_1 := \text{Int}][x_2 := \text{Int}]$ and $\Gamma'[x_1 := \text{Bool}][x_2 := \text{String}]$. This is what propagate$_{x,a,s_i}$ does: it propagates to the types of the free variables of $a$ any refinement of $s_i$ specified in the typing of $x$. This yields a new set $\Gamma'_i$ whose environments refine those in $\Gamma_i$. Once we obtained this new $\Gamma'_i$ we can now extract the hypotheses about $x$ to create a new annotation $A_i$ for the binding and pass the rest of the environment as a refinement for the whole bind expression. This is done by the function extract$_x$ defined as follows: extract$_x(\Gamma) \stackrel{\text{def}}{=} ((\Gamma \setminus x) \triangleright \Gamma(x) \mid \Gamma \in \Gamma), \{\Gamma \setminus x \mid \Gamma \in \Gamma\})$ where $\Gamma \setminus x \stackrel{\text{def}}{=} \Gamma \setminus \{x \mapsto \Gamma(x)\}$ for $x \in \text{dom}(\Gamma)$. Finally, the result of the rule is formed by a pair obtained by unioning all the annotations $A_i$ and all the refinements $\Gamma''_i$ obtained for each $i \in I$.

We conclude the presentation of our system by explaining a simplified version of the main rule for checking $\lambda$-abstractions which is applied when the type $t$ to check is an intersection of arrows:

$$ [\text{ABS}] \frac{\{s_i\}_{i \in I} = \text{partition}((\Gamma \triangleright A) \cup \{s_j \mid j \in J\}) \quad (\forall i \in I) \quad \Gamma, (x : s_i) \vdash_R \kappa : t \circ s_i \Rightarrow (\kappa_i, \Gamma_i) \quad (A_i, \Gamma'_i) = \text{extract}_x(\Gamma_i)}{\Gamma \vdash_R \lambda x: A. \kappa : t \Rightarrow (\lambda x: \bigcup_{i \in I} A_i. \text{merge}(\{\kappa_i\}_{i \in I}), \bigcup_{i \in I} \Gamma'_i)} t \approx \bigwedge_{j \in J}(s_j \to t_j) $$

According to $[\to I-ALG]$, we must find how to split the domain of the function into some domain types, that we assign to the parameter of the function to check its body. This will yield the intersection type of the function. To determine this set of domains, we take those of the type $t$ we are checking (i.e., $\{s_j \mid j \in J\}$, since $t \approx \bigwedge_{j \in J}(s_j \to t_j)$) and we add them to those we already know, which are specified in the annotation A of the parameter (i.e., $(\Gamma \triangleright A)$). Then, as for [BIND], we partition this set yielding the set of domains $\{s_i\}_{i \in I}$. As customary for each $i$ we check under the hypothesis $x : s_i$ that the body has the expected type, that is, the type of the function $t$ applied to the type of the parameter $s_i$, namely, $t \circ s_i$. This yields a set of result pairs $\{(\kappa_i, \Gamma_i)\}_{i \in I}$ that we use in the same way as we did in [BIND] to form the final result. The only difference is that we do not need any further refinements for the $\Gamma_i$'s, since, contrary to [BIND], there is no argument whose variables need to be refined.

All the remaining rules (pairs, variables, and the rules for the special cases of unions and empty types) are mostly straightforward and can be found in Appendix B with a detailed explanation and the formal definition of all the auxiliary functions used therein. All that remains to do is to define

<footnote n="6">⁶Formally, partition($\{t_i\}_{i \in I}$) is the smallest (in term of cardinality) non-empty set of types $\{s_j\}_{j \in J}$ such that $(i) \lor_{j \in J} s_j \approx \lor_{i \in I} t_i$, $(ii) \forall j \in J. \forall j' \in J. j \neq j' \Rightarrow s_j \land s_{j'} \approx \emptyset$, and $(iii) \forall j \in J. \forall i \in I. s_j \leq t_i \text{ or } s_j \land t_i \approx \emptyset$</footnote>
a : ((Int→(Int ∨ Bool)) ∨ (Int × (Int ∨ Bool)))
n : Int

<caption>Fig. 7. Types of the atoms *a* and *n*.</caption>

1 : (a ∈ (Int×Int)) ? π₁a == π₂a
2 : (a ∈ (1×1)) ? π₂a
3 : ((a n) ∈ Int) ? (a n) < 42
4 : (a n)

<caption>Fig. 8. Expression $e_o$ of the source language.</caption>

0 bind x₀ : A₀ = a in
1 bind x₁ : A₁ = n in
2 bind x₂ : A₂ = π₁x₀ in
3 bind x₃ : A₃ = π₂x₀ in
4 bind x₄ : A₄ = x₂ == x₃ in
5 bind x₅ : A₅ = x₀ x₁ in
6 bind x₆ : A₆ = x₅ < 42 in
7 bind x₇ : A₇ = (x₅ ∈ Int) ? x₆ : x₅ in
8 bind x₈ : A₈ = (x₀ ∈ 1×1) ? x₃ : x₇ in
9 bind x₉ : A₉ = (x₀ ∈ Int×Int) ? x₄ : x₈ in x₉

<caption>Fig. 9. MSC-form of the expression $e_o$.</caption>

the result of the inference algorithm as the fixpoint of the transformation defined by that system.
Formally, let $κ$ be a closed MSC-form, we define the annotation reconstruction algorithm $\mathcal{R}$ as:

$$ \mathcal{R}(\kappa) = \begin{cases} \kappa & \text{if } \emptyset \vdash_{\mathcal{R}} \kappa : \emptyset \Rightarrow (\kappa, \{\emptyset\}) \\ \mathcal{R}(\kappa') & \text{if } \emptyset \vdash_{\mathcal{R}} \kappa : \emptyset \Rightarrow (\kappa', \{\emptyset\}) \text{ and } \kappa \neq \kappa' \\ \text{Fail} & \text{if } \emptyset \vdash_{\mathcal{R}} \kappa : \emptyset \Rightarrow (\kappa', \{\}\}) \end{cases} $$

The reconstruction algorithm is sound:

**THEOREM 5.1 (SOUNDNESS).** If $κ$ is a closed MSC-form and $\mathcal{R}(κ) = κ'$, then $\emptyset \vdash_{\mathcal{R}} κ' : t$ for some $t$.

Notice that if the algorithm does not fail, then $\lceil \langle \mathcal{R}(κ) \rangle \rceil = \lceil \langle κ \rangle \rceil$. This, together with Corollary 4.4, yields a sound procedure to type an expression $e$ of the source language. Let $κ$ be the algorithmic expression obtained by adding the annotation $\{\emptyset \vdash 1\}$ everywhere in MSC($e$). If $\mathcal{R}(κ)$ does not fail, then $\emptyset \vdash_{\mathcal{R}} \mathcal{R}(κ) : t$. Since $\lceil \langle \mathcal{R}(κ) \rangle \rceil = \lceil \langle κ \rangle \rceil = \lceil \text{MSC}(e) \rceil \equiv_α e$, then by the soundness part of Corollary 4.4 we can conclude $\emptyset \vdash e : t$. Notice also that the algorithm works for initial annotations different from 1, too. In particular, soundness holds also for intermediate terms whose $λ$-abstractions are explicitly annotated as in $λx:A.e$: if it succeeds, the algorithm will refine the term so that its domain is a subtype of $\lor(Γ \triangleright A)$. This means that we have for free a typing algorithm for the source language (5) of Section 2.2 extended with explicitly annotated functions of the form $λx:A.e$. This is why in our prototype, presented in next section, function parameters may be optionally annotated.<fnref n="7" /> Finally, we conjecture that the algorithm terminates, that is, that $\mathcal{R}(κ)$ is defined for every closed MSC-form $κ$, but this result is difficult to prove because the rule [APR] creates new arrow types.

*Example.* We illustrate on a complete example the behaviour of our inference algorithm. We type the source language expression $e_o$ given in Figure 8 in which $n$ and $a$ are atomic expressions (whose definitions we omit) whose types are given in Figure 7. The MSC-form of $e_o$ is given in Figure 9. Notice that the various occurrences of $π₁a$ and $a n$ are shared, using $x₂$ and $x₅$ respectively. We describe the iterations of Algorithm $\mathcal{R}$ which deduces for $e_o$ the type Bool. In what follows, we call $t_a$ the original type of $a$ given in Figure 8. We start with $A₀ = t_a$, $A₁ = \text{Int}$, and $Aᵢ = 1$ for $i = 2..9$.

*First iteration.*

→ bind $x₀...$, $Γ = \emptyset$, $A₀ = \{t_a\}$: Rule [BIND] on the only type in the annotation $A₀$ (we assume nothing is learned while typing $a$);

→ bind $x₁...$, $Γ = \{x₀ : t_a\}$, $A₁ = \{\text{Int}\}$: Rule [BIND] on the only type in the annotation $A₁$;

→ bind $x₂...$, $Γ = \{x₀ : t_a, x₁ : \text{Int}\}$, $A₂ = \{1\}$: Rule [BINDARGREFENV] triggers recursively rule [PROJ1] to type $π₁ x₀$. It returns the singleton set of environments:

$$ \Gamma = \{ \{x₀ : (\text{Int} \times (\text{Int} \lor \text{Bool})), x₁ : \text{Int}\} \}. $$

<footnote n="7">⁷In the implementation we forbid the annotations written by the user to be refined, so that the domain of $λx:A.e$ will be exactly $\lor(Γ \triangleright A)$. In this way the system deduces for $λx.(x + 1)$ the type $\text{Int} \to \text{Int}$ but rejects $λx:1.(x + 1)$ as ill-typed.</footnote>
bind $x_2...$: Rule [BINDARGREFENV] returns the following set containing two environments
$\Gamma_0 = \{ \{x_0: (\mathbf{Int} \times (\mathbf{Int} \lor \mathbf{Bool})), x_1: \mathbf{Int}\}, \{x_0: t_a, x_1: \mathbf{Int}\} \}$.
Notice that the rest of the program is ignored and $\Gamma_0$ is propagated upward.

bind $x_1...$: Rule [BIND] returns. Here since nothing new is learned about the type of $x_1$ (functions propagate and extract behave as identities), $\Gamma_0$ is propagated upward.

bind $x_0...$: Rule [BIND] returns. Here functions propagate and extract create the new annotation for $x_0$ that is $A'_0 = \{t_a, (\mathbf{Int} \times (\mathbf{Int} \lor \mathbf{Bool}))\}$

At this point a new annotation has been inferred (i.e., $A'_0$), so Algorithm $\mathcal{R}$ restarts.

Second iteration.

bind $x_0...$, $\Gamma = \emptyset$, $A_0 = \{(\mathbf{Int} \times (\mathbf{Int} \lor \mathbf{Bool})), t_a\}$: Rule [BIND] on the two types in $A_0$. Here partition splits the annotation into $\mathbf{Int} \times (\mathbf{Int} \lor \mathbf{Bool})$ and $t_a \setminus (\mathbf{Int} \times (\mathbf{Int} \lor \mathbf{Bool})) \cong \mathbf{Int} \to (\mathbf{Int} \lor \mathbf{Bool})$. The rule tries both types for $x_0$ in turn. We focus first on $\mathbf{Int} \times (\mathbf{Int} \lor \mathbf{Bool})$.

bind $x_1...$, $\Gamma = \{x_0: \mathbf{Int} \times (\mathbf{Int} \lor \mathbf{Bool})\}$, $A_1 = \{\mathbf{Int}\}$: Rule [BIND] on the only type of the annotation $A_1$; (the following cases from bind $x_2$ to bind $x_4$ are similar and omitted);

bind $x_5$, $\Gamma = \{x_4: \mathbf{Bool}, ...\}$: Rule [BINDARGUNTYPE] since $x_0$ does not have a function type;

bind $x_6$ and bind $x_7$, $\Gamma = \{x_4: \mathbf{Bool}, ...\}$: Rule [BINDARGUNTYPE] since $x_5 \notin \text{dom}(\Gamma)$

bind $x_8...$, $\Gamma = \{x_4: \mathbf{Bool}, ...\}$: Rule [BIND] recursively calls [CASE]. Here since, the type of $x_0$ is completely contained in $\mathbf{1} \times \mathbf{1}$, the case rule only returns the original $\Gamma$ (cf. the definition of $[\_ \triangleq \_]$): no new information is learned; the rest of the MSC-form is examined.

bind $x_0...$, $\Gamma = \{x_8: (\mathbf{Int} \lor \mathbf{Bool}), ...\}$: Rule [BINDARGREFENV] recursively calls [CASE] rule. Here, however, the type of $x_0$ is not a subtype of the tested type, this rule therefore returns a singleton with a refined environment $\Gamma = \{\Gamma: \{x_0: \triangleq \mathbf{Int} \times \mathbf{Int}\}$

bind $x_0...$: Rule [BINDARGREFENV] returns the original environment and a refined one for $x_0$. The typing does not continue further and returns upward.

bind $x_0...$ like in the previous iteration the annotation for $x_0$ comes back to its binder, yielding a new annotation: $A_0'' = \{t_a, (\mathbf{Int} \times (\mathbf{Int} \lor \mathbf{Bool})), \mathbf{Int} \times \mathbf{Int}\}$

At the third iteration, partition() used in [BIND] on the "bind $x_0$" expression splits $A_0''$ into three types: $\mathbf{Int} \times \mathbf{Int}$, $\mathbf{Int} \times \mathbf{Bool}$, and $\mathbf{Int} \to (\mathbf{Int} \lor \mathbf{Bool})$. For both product types, the typing succeeds till the end (each time skipping the lines 5-7 where $x_0$ is used as a function). As for the functional annotation, it is almost straightforward. One caveat is in the typing of $x_6$: since $\mathbf{Int} \to \mathbf{Int} \to \mathbf{Bool}$, the application $x_5 < 42$ introduces a new refinement for $x_5$ which, at this point, has type $\mathbf{Int} \lor \mathbf{Bool}$ (the return type of $x_0$). The algorithm propagates both types to $A_5$ and the rest of the program is typed twice, under both hypotheses. Notice that both succeed since, in the case where $x_5$ has type $\mathbf{Bool}$, $x_6$ only occurs in an unreachable branch of a type case. The final MSC-form has annotations $A_0=\{\mathbf{Int} \times \mathbf{Int}, \mathbf{Int} \times \mathbf{Bool}, \mathbf{Int} \to (\mathbf{Int} \lor \mathbf{Bool})\}$, $A_1=A_2=\mathbf{Int}$, $A_3=\{x_0:\mathbf{Int} \times \mathbf{Int} \to \mathbf{Int}, x_0:\mathbf{Int} \times \mathbf{Bool} \lor \mathbf{Bool}\}$, $A_5=\{x_0:\mathbf{Int} \to (\mathbf{Int} \lor \mathbf{Bool}) \to \mathbf{Int}, x_0:\mathbf{Int} \to (\mathbf{Int} \lor \mathbf{Bool}) \lor \mathbf{Bool}\}$, $\mathbf{Bool}$ guarded by the active environments for the others. For this term $\vdash_{A_1}$ infers the type $\mathbf{Bool}$.

# 6 IMPLEMENTATION

We have implemented Algorithm $\mathcal{R}$ in OCaml, using CDuce [CDuce] as a library to provide set-theoretic types and semantic subtyping. The prototype amounts to 3500 lines of OCaml code and features several extensions such as let bindings and records (both formalised in Appendix C) and annotations of function parameters (see Footnote 7). The transformation of terms in their MSC-form is similar to the locally nameless approach ([Charguéraud 2012]). Expressions from the source language are transformed so that bound variables are represented using De Brujin indices, while free variables are represented with symbolic names. While performing this transformation, hash-consing is used to identify structurally equal subterms. We give in Table 1 the code of
<table><caption>Table 1. Types inferred by the implementation (times are in ms)</caption><thead><tr><th>Code</th><th>Inferred type</th><th>MSC</th><th>Inf.</th></tr></thead><tbody><tr><td>1 let is_int = fun x -><br> if x is Int then true else false<br> let is_bool = fun x -><br> if x is Bool then true else false</td><td>(Int → True) ∧ (¬Int → False)<br>(Bool → True) ∧ (¬Bool → False)</td><td>0.02</td><td>0.22</td></tr><tr><td>2 type Falsy = False | "" | 0<br> type Truthy = ~Falsy<br> let not_ = fun x -><br> if x is Truthy then false else true<br> let to Bool = fun x -> not_ (not_ x)<br> let and_ = fun x -> fun y -><br> if x is Truthy then to Bool y else false<br> let or_ = fun x -> fun y -><br> not_ (and_ (not_ x) (not_ y))</td><td>(Truthy → False) ∧ (Falsy → True)<br>(Truthy → True) ∧ (Falsy → False)<br>(Falsy→1→False) ∧ (Truthy→Truthy→True) ∧<br>(Truthy→Falsy→False)<br>(Truthy→1→True) ∧ (Falsy→Truthy→True) ∧<br>(Falsy → Falsy → False)</td><td>0.03<br>0.02<br>0.03<br>0.03</td><td>0.58<br>0.93<br>2.24<br>3.34</td></tr><tr><td>3 strlen : String → Int<br> let example14 =<br> fun input -> fun extra -><br> if and_ (is_int input)<br> (is_int (fst extra)) is True<br> then input + (fst extra)<br> else if is_int (fst extra) is True<br> then (strlen input) + (fst extra)<br> else 0</td><td>((Int ∨ String) → (¬Int×1) → 0) ∧<br>((Int ∨ String) → (Int×1) → Int) ∧<br>(¬(Int ∨ String) → (¬Int×1) → 0)</td><td>0.05</td><td>3.61</td></tr><tr><td>4 let example6_wrong =<br> fun (x : Int|String) -> fun (y : Any) -><br> if and_ (is_int x) (is_string y) is True then<br> add x (strlen y) else strlen x<br> let example6_ok =<br> fun x -> fun y -><br> if and_ (is_int x) (is_string y) is True then<br> add x (strlen y) else strlen x</td><td>Ill typed<br>(String → 1 → Int) ∧<br>(Int → String → Int)</td><td>0.07</td><td>1.52</td></tr><tr><td>5 let detailed_ex =<br> fun (a : (Int -> (Int|Bool)))<br> | (Int, (Int|Bool))) -><br> fun (n : Int) -><br> if a is (Int, Int) then (fst a)=(snd a)<br> else if a is (Any, Any) then snd a<br> else if (a n) is Int then (a n) < 42<br> else a n</td><td>(Int → (Int ∨ Bool)) ∨ (Int×(Int ∨ Bool)) →<br> Int → Bool</td><td>0.08</td><td>1.77</td></tr></tbody></table>

several functions, using a syntax similar to OCaml, where uppercase identifiers (e.g., True, String) denote types and lowercase identifiers denote variables or constants. For each function we report its inferred type, the time taken to put its body in MSC form, and the time taken to infer its type or typecheck it (for annotated functions). All runtimes are given in milliseconds, averaged over ten runs. The experiments were done on an Intel Core i7-8565U 1.8GHz CPU (with 16GB of RAM). The code was compiled natively using OCaml 4.12.0. All these examples (and more) can be tested online with the interactive prototype hosted at https://typecaseunion.github.io [Castagna et al. 2022b].

Code 1 and 2 show that exact overloaded types can be inferred even in the absence of annotations. In Code 1 we encode type predicates as they can be found in Typed Racket. The inferred overloaded types exactly specify the semantics of these functions using the singleton types of the values true and false, while in Typed Racket this requires these predicates to be primitives of the language and are typed with specific rules. Code 2 implements Boolean operators by considering values as in JavaScript where eight specific “falsy” values (false, "", 0, -0, 0n, undefined, null, and NaN) are considered to be equivalent to false, and all the others—called “truthy” values—to be equivalent to true. We first define the type Falsy as the union of the singleton types of false, "", and 0 (the other values are absent in our prototype) and the type Truthy as the negation of F.
example in which the decision is based on the type-cases: the exact inferred intersection type is obtained by splitting the type of `x` because `x` is tested in a type-case. The function `to Bool` is an example in which the decision is based on an overloaded application: the type is inferred by splitting the type of `x` since `x` is the argument of the function `not_`. In `to Bool` by a double application of `not_` we map truthy values into `true` and falsy ones into `false`, as the type inferred for `to Bool` exactly specifies. The function `and_` mixes the two kinds of decision since it tests the type of the first argument and applies an overloaded function to the second argument. We could have defined `and_` as two nested tests checking whether both arguments are truthy and returning false otherwise: the system would have inferred the same type which, once more, exactly specifies the semantics of the function. If we wanted to implement for the "and" operator the same semantics as the one defined for the logical AND (`&&`) of JavaScript, then we should instead have used the following definition `fun x -> fun y -> if x is Falsy then x else y` whose inferred type `(Falsy→1→Falsy)∧(Truthy→1→1)` does not specify the function's exact semantics because our system lacks polymorphism (with polymorphic types we would expect the inferred type to be `∀α.(α∧Falsy→1→α∧Falsy)∧(Truthy→α→α)`—where `α` is a type variable—which states that if the first argument is of type (subtype of) `Falsy`, then the result will be of the same type as the type of first argument—independently from the second one—, while if the first argument is of type `Truthy`, then the result will be of the same type as the type of second argument). Finally, the last example in Code 2 defines `or_` by combining the two previous functions according to De Morgan's laws: again the inferred type is exact. The degree of precision achieved by the type inference for the examples in Code 2 is out of reach of all existing approaches to occurrence typing.

Our implementation can type all the 14 paradigmatic examples listed by Tobin-Hochstadt and Felleisen [2010] (THF) whose results we improve in several ways: first, we infer types that are more precise than those inferred in THF; second, our system types all examples without needing any annotation, whereas THF must specify some annotations in 5 of the 14 examples; third, our analysis works also when in these example we employ user-defined connectives and type predicates, whereas in THF these must be hard-coded to be used inside a test. For space reasons, we did not detail all these examples here (but they can be tested in our online prototype by selecting the appropriate menu entry) and chose instead to show only two of them in Code 3 and 4.

Code 3 is EXAMPLE 14 of THF, which is last and most complete of the 14 examples of THF and summarizes the features of all the others. This definition shows all the improvements brought by our system and listed above: first, we infer a more precise type which discriminates the cases in which the function returns a generic integer or `0` (i.e., `0` is returned whenever the second argument is of type `(-Int × 1)`, independently from the first argument's type); second, our inference does not need any annotation, while in THF both parameters of the function must be explicitly annotated; third, the tested expression is a Boolean expression obtained by applying custom user-defined connectives (`and_`) and type predicates (`is_int`) whose use would make the analysis of THF fail.

Code 4 is EXAMPLE 6 of THF which shows error detection: if `x` is assumed of type `IntVString` (as in `example6_wrong`), then the function is ill-typed, and rightly so since if both arguments are not strings, then `strlen x` is selected and its execution fails. However, if as in `example6_ok`, we let our system determine the types of the parameters, then it rightly determines that the first argument must be either a string or an integer (any other type would select `strlen x` and then fail), but also that when the first is an integer, then the second must be a string, or the function would fail. Such a deduction is out of reach of the approach defined by THF.

Code 5 is the detailed example of the previous section and shows that the type of function parameters can easily be constrained if one wishes. Interestingly, if we remove the `Int` annotation from the second parameter `n`, the system computes a more precise type `((Int→(Bool∨Int)) →`
$Int \to Bool) \wedge ((Int \times (Bool \lor Int)) \to 1 \to Bool)$ which clearly states that the second argument of the function needs to be an integer only when the first one is a function.

# 7 RELATED WORK

As previously said, the present paper extends the system of [Barbanera et al. 1995] with three rules for type-cases and with the use of a particular subtyping relation. We then define, in several steps, a type inference algorithm for this calculus. The resulting calculus and type-inference appears to be particularly well suited for typing programs written in dynamic languages such as JavaScript.

While taking a radically different approach, we achieve a goal similar to occurrence typing, introduced in [Tobin-Hochstadt and Felleisen 2008] and further advanced in [Tobin-Hochstadt and Felleisen 2010], in the context of the Typed Racket language. In this and subsequent work, types are annotated by two logical propositions that record the type of the input depending on the (Boolean) value of the output. For instance, the type of the number? function states that when the output is true, then the argument has type Number, and when the output is false, the argument does not. These propositions are propagated and used in particular in type-cases to refine the type of variables and, more generally, expressions in the “then” and “else” branches of a conditional. Furthermore, this analysis focuses on a particular set of pure operations, so that the approach works also in the presence of side-effects. Contrary to these works, we try not to depend on an external logic but, rather, to express as much as possible these conditions with set-theoretic types. For instance, we track the dependency between input and output types of functions using intersection types (cf. Code 1 in Table 1), while type-case expressions are typed using intersection and negation types to refine the typing environments of the branches. Our approach is more global since, not only our analysis strives to infer type information by analyzing all types of results (and not just true or false), but also tries to perform this analysis for all possible expressions (and not just for a restricted set of expressions). This allows our system to type all the examples given in [Tobin-Hochstadt and Felleisen 2010] (and contrary to the cited work, without needing any annotations) and many more but, as we explain at the end of this section, at the expense of an immediate compatibility with the presence of side-effects.

In a previous work [Castagna et al. 2022a] we already used characteristics of semantic subtyping to improve occurrence typing but the approach we used there was completely different from the one presented here. Instead of relying on bindings to track the different occurrences of a same expression, we enriched type environments so that they mapped occurrences of expressions (expressed in terms of paths) to types. This yielded a type-theoretic approach with non standard features (the type environments) that, contrary to the present one, could not capture the flow of information between variables and thus failed to type Code 3 of Table 1. Furthermore, the connection with the union elimination rule was completely missing.

Set-theoretic types have also been used by [Kent 2019, Chapter 5] to extend the logical techniques developed for Typed Racket to track under which hypotheses an expression returns false or not. Kent uses set-theoretic types to express type predicates (a predicate that holds only for a type *t* has type *p*: (*t*→True) ∧ (¬*t*→False)) as well as to express in a more compact (and, sometimes, more precise) way the types of several built-in Typed Racket functions. It also uses the properties of set-theoretic types to deduce the logical types (i.e., the propositions that hold when an expressions produces *false* or *not*) of arguments of function applications. The main difference of Kent's approach with respect to ours is that, since it builds on the logical propositions approach, then it focuses the use of set-theoretic types and of the analysis of arguments of applications of a selected set of pure expressions (while we use all expressions) to determine when an expression yields a result of type *False* or *NotFalse* (while we use all types of results). The consequence is that not only Kent's approach covers fewer cases than ours and cannot infer intersection types, but also the very
fact of focusing on truthy vs. false results may make Kent's analysis fail even for pure Boolean tests where it would be naively expected to work. The approach has however the advantage of building on Typed Racked which provides a mature and high-performing implementation. The reader will find in [Castagna et al. 2022a, see section on related work] an extensive and detailed comparison between current approaches of occurrence typing and those based on set-theoretic types.

Our approach is based on program transformation: we transform expressions into MSC-forms. A similar approach is used by Rondon et al. [2008] who transform expressions into *A-normal forms* (ANF) [Sabry and Felleisen 1992] and track precise type information for every sub-expression by keeping this information for the variables. While this solution is close to ours it does not achieve the same degree of precision for the simple reason that, contrary to MSC-forms, ANFs were not designed to target occurrence typing. MSC-forms' rationale is to give a unique name to every α-equivalent sub-expression of the initial term, ANFs instead ensure that arguments of applications are immediate values. While the result looks similar, there are key differences: since the sharing of α-equivalent subterms is used only for typing, it does not need to preserve the semantics of the original term. For example, sub-expressions in the branches of a conditional are hoisted outside the conditional (crucial for occurrence-typing), which must not be done for ANFs. Conversely, all proper subterms of an application must be variables in MSC-forms but not in ANFs.

The typing algorithm we present in Section 5 works as a bi-directional typing algorithm: the definition of a variable gives a forward constraint on its type while the use of a variable (e.g., in a type-case or as part of an application) gives a backward constraint that is added to its definition. From the extensive survey by Dunfield and Krishnaswami [2019a] on bi-directional typing, we see that this technique is well-suited for the type-checking or type-inference of complex features such as, for instance, in [Pierce and Turner 2000] (local type inference in the presence of subtyping), [Pottier and Régis-Gianas 2006] (bi-directional type propagation for typing generalized algebraic data-types), or [Dunfield and Krishnaswami 2019b] (bi-directional type checking for higher rank polymorphism). The two latter works, in particular, seem to indicate that our approach remains viable when extending the present work with parametric polymorphism.

A feature we completely omitted in our study is gradual typing. Works such as [Chaudhuri et al. 2017] (for Flow) or [Rastogi et al. 2015] (for TypeScript), account for the presence of unsafe, already written code, by using a form of gradual typing. Castagna et al. [2022a] outline how gradual typing can be integrated in a system with semantic subtyping and occurrence typing using work by [Castagna et al. 2017; 2019]: we think that those ideas can be adapted to the work presented here.

We end this presentation of related work with a discussion on side effects, a crucial feature for dynamic languages. Although in our system we did not take into account side-effects—and actually our system works because all the expressions of our language are pure—it is interesting to see how the different approaches of occurrence typing position themselves with respect to the problem of handling side effects, since this helps to better place our work in the taxonomy of the current literature. As Sam Tobin-Hochstadt insightfully noticed, one can distinguish the approaches that use types to reason about the dynamic behavior of programs according to the set of expressions that are taken into account by the analysis. In the case of occurrence typing, this set is often determined by the way impure expressions are handled. On the one end of the spectrum lies our approach (both this work and the one in Castagna et al. [2022a]): our analysis takes into account *all* expressions but, in its current formulation, it works only for pure languages. On the other end of the spectrum we find the approach of Typed Racket whose analysis reasons about a limited and predetermined set of *pure* operations: all data structure accessors. Somewhere in-between lies the approach of the Flow language—whose core features were formalized by Chaudhuri et al. [2017]—which implements a complex effect systems to determine pure expressions. While the system presented here does not work for impure languages, we argue that its foundational nature
predisposes it to be adapted to handle impure expressions as well, by adopting existing solutions or proposing new ones. For instance, it is not hard to modify our system so that it takes into account only a set of predetermined pure expressions, as done by Typed Racket: it suffices to instruct the transformation in MSC-form to use distinct bind variables for distinct occurrences of expressions that are not in this set. However, such a solution would be marginally interesting since by excluding from the analysis all applications, we would lose most of the advantages of our approach with respect to the one with logical propositions. Thus a more interesting solution would be to use some external static analysis tools—e.g., to graft the effect system of Chaudhuri et al. [2017] on ours—to detect impure expressions. The idea would be to mark different occurrences of a same impure expression using different marks and, again, instruct the transformation in MSC-form to use distinct bind variables for expressions with distinct marks. For instance, consider the test ($f x \in \text{Int}$)? ... : ...: if $f x$ were flagged as impure then an occurrence of $f x$ in the “then” branch would not be supposed to be of type Int since the MSC-form of this expressions would use two distinct variables to bind $f x$ occurring in the test and the one in the branch. Although this would certainly improve our analysis, is would still significantly limit the sharing. Which is why we believe that, ultimately, our system should not resort to external static analysis tools to detect impure expressions but, rather, it has to integrate this analysis with the typing one, so as to mark only those impure expressions whose side-effects may affect the semantics of some type-cases. For instance, consider a JavaScript object `obj` that we modify as follows: `obj["key"] = 3`. If the field `"key"` is already present in `obj` with type `Int` and we do not test it more than about this type, then it is not necessary to mark different occurrences of `obj` with different marks, since the result of the type-case will not be changed by the assignment; the same holds true if the field is absent but type-cases do not discriminate on its presence. Otherwise, some occurrences of `obj` must use different marks: the analysis will determine which ones. We leave this study for future work.

## 8 CONCLUSION

Although the technical development of our work may appear complex, the unfolding of the logical sequence of its steps can be easily summarized. In Section 1 we argued that the essence of occurrence typing can be captured by adding three typing rules, $[\vee]$, $[\epsilon_1]$, and $[\epsilon_2]$: the union elimination rule can split the type of any expressions into a union of two types that can be tested separately and the rules for type-cases distribute these tests differently on the two branches of a type-case. The addition of these three rules yields the system of Section 2 which captures the spirit of occurrence typing, covers the examples proposed by existing approaches, but is not algorithmic. To obtain an algorithmic system, four technical problems are to be solved: (i) how to choose on which expressions the rule $[\vee]$ must be applied; (ii) given an expression chosen for applying $[\vee]$, how to choose which sub-expression of this expression and which occurrences of this sub-expression should the system use to apply $[\vee]$; (iii) how to determine the union of types into which the system should split the type of a sub-expression chosen for $[\vee]$; (iv) how to determine the arrows that form the intersection type of a $\lambda$-abstraction that is not annotated. Section 3 solves the first two problems—which made the system *non syntax-directed*—by the definition of MSC-forms: the fact that MSC-forms bind atoms whose all proper sub-expressions are variables means that the system chooses to apply $[\vee]$ on *all* sub-expressions, while the maximal sharing property of MSC-forms means that the system chooses *all* occurrences of each sub-expression since it replaces all of them by the same variable. Section 4 solves the last two problems—which made the system *non analytic*—by the definition of annotations: annotations state how to split the type of the bound variables into a union of types (when the variable is bound by a $\lambda$ this corresponds to splitting the type of the $\lambda$-abstraction into an intersection, when the variable is bound by a *bind* this corresponds to splitting the type of the argument of the *bind*-expression into a union). By this sequence of steps
we reduced the problem of typing expressions with occurrence typing to the problem of choosing annotations for MSC-forms and shown that this choice corresponds to determining how to split types into unions for bind-expressions and into intersection for $\lambda$-abstractions. Section 5 suggests that the choice of how to split these types can be based on a program analysis that focuses on the types tested in type-cases or involved in applications of overloaded functions. Section 6 implements these choices demonstrating the practical implications of our work.

In summary, the logical sequence described above highlights the connection between union elimination and occurrence typing techniques via the addition of negation types and their use in the typing of type-case expressions. It also provides an effective way to reduce this typing problem to the inference of some specific annotations.

From a theoretical viewpoint, our work is a step forward in the quest of an inversion lemma for the union elimination rule. Although we are still far from an inversion lemma, the results of Sections 3 and 4 show that for a well-typed term *e* of the source language (or of Barbanera et al. [1995]) there exists a canonical way to use the union rule to derive its type, which corresponds to the derivation encoded by MSC(*e*). Thus the problem now is no longer when to use the rule, but how to determine the split of the type of the argument of the union rule into the union of two types, which coincides with inferring the annotations for the corresponding binding-expression.

From a practical viewpoint, our work reframes the problem of occurrence typing into a classical setting that has been actively studied for thirty years and for which a wealth of results and techniques already exists. We want to transpose some of them to our specific setting, in particular the extension to polymorphism and the generation and resolution of systems of constraints, to infer the polymorphic types we hinted at in Section 6. For this we count reusing the theory of polymorphic types with semantic subtyping [Castagna and Xu 2011] together with the typing techniques and algorithms developed for CDuce, both for its explicitly typed version [Castagna et al. 2015, 2014] and the implicitly typed one [Castagna et al. 2016; Petrucciani 2019]. Eminently of practical interest is also the fact that we effectively reduced type inference to a very specific problem, namely, the reconstruction of some specific annotations. The algorithm we described in Section 5 is just one possible solution to this problem, but our formal setting opens the way to the definition of other different techniques. In particular, we are studying the feasibility of switching from the current system that at each pass generates type refinements for the variables of the term, to one that generates, instead, sets of type constraints (such as those defined by Petrucciani [2019, Chapter 4]) whose resolution would yield these (and hopefully better) refinements. This seems an obvious choice if we want to handle polymorphism and it would also improve the precision of our algorithm which currently works poorly when higher-order function parameters are not explicitly annotated. This shortcoming is expected—and shared among the approaches that lack polymorphism—since our algorithm initializes higher-order parameters with the type $0 \to 1$ while, if type variables were available, the algorithm could instead initialize them with $\alpha \to \beta$ where $\alpha$ and $\beta$ are fresh. This would allow the system to better track and refine the types of these parameters.

## ACKNOWLEDGMENTS

This research was partially supported by Labex DigiCosme (project ANR-11-LABEX-0045- DIGI-COSME) operated by ANR as part of the program «Investissement d'Avenir» Idex Paris-Saclay (ANR-11-IDEX-0003-02), by the « Chaire Langages Dynamiques pour les Données » of the Paris-Saclay foundation, and by a Google PhD fellowship. The authors would like to thank Delia Kesner for her help with the rewriting systems.
REFERENCES

Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de'Liguoro. 1995. Intersection and Union Types. *Inf. Comput.* 119, 2 (June 1995), 202–230. https://doi.org/10.1006/inco.1995.1086

Giuseppe Castagna. 2020. Covariance and Controvariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers). *Logical Methods in Computer Science* 16, 1 (2020), 15:1–15:58. https://doi.org/10.23638/LMCS-16(1:15)2020

Giuseppe Castagna and Victor Lanvin. 2017. Gradual Typing with Union and Intersection Types. *Proc. ACM Program. Lang.* 1, ICFP, Article 41 (Aug. 2017), 28 pages. https://doi.org/10.1145/3110285

Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek. 2019. Gradual Typing: a New Perspective. *Proc. ACM Program. Lang.* 3, POPL '19 46th ACM Symposium on Principles of Programming Languages, Article 16 (Jan. 2019), 32 pages. https://doi.org/10.1145/3290329

G. Castagna, M. Laurent, V. Lanvin, and K. Nguyễn. 2022a. Revisiting Occurrence Typing. *Science of Computer Programming* (2022). To appear. Preprint available at https://arxiv.org/abs/1907.05590.

Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, and Matthew Lutze. 2022b. *Prototype for Article: On Type-Cases, Union Elimination, and Occurrence Typing*. https://doi.org/10.1145/3462306 Online interactive version available at https://typecaseunion.github.io.

Giuseppe Castagna, Kim Nguyễn, Zhiwu Xu, and Pietro Abate. 2015. Polymorphic functions with set-theoretic types. Part 2: local type inference and type reconstruction. In *Proceedings of the 42nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '15)*. 289–302. https://doi.org/10.1145/2676726.2676991

Giuseppe Castagna, Kim Nguyễn, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, and Luca Padovani. 2014. Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation. In *Proceedings of the 41st Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '14)*. 5–17. https://doi.org/10.1145/2676726.2676991

Giuseppe Castagna, Tommaso Petrucciani, and Kim Nguyễn. 2016. Set-Theoretic Types for Polymorphic Variants. In *ICFP '16, 21st ACM SIGPLAN International Conference on Functional Programming* 378–391. https://doi.org/10.1145/2951913.2951928

Giuseppe Castagna and Zhiwu Xu. 2011. Set-theoretic Foundation of Parametric Polymorphism and Subtyping. In *ICFP '11: 16th ACM-SIGPLAN International Conference on Functional Programming* 94–106. https://doi.org/10.1145/2034773.2034788

CDuce. *The CDuce Compiler*. CDuce https://www.cduce.org

Arthur Charguéraud. 2012. The Locally Nameless Representation. *J. Autom. Reason.* 49, 3 (Oct 2012), 363–408. https://doi.org/10.1007/s10817-011-9225-2

Avik Chaudhuri, Panagiotis Vekris, Sam Goldman, Marshall Roch, and Gabriel Levi. 2017. Fast and Precise Type Checking for JavaScript. *Proc. ACM Program. Lang.* 1, OOPSLA, Article 48 (Oct. 2017), 30 pages. https://doi.org/10.1145/3133872

Mariangiola Dezani-Ciancaglini. 2020. Personal communication.

Mariangiola Dezani-Ciancaglini, Alain Frisch, Elio Giovannetti, and Yoko Motohama. 2003. The Relevance of Semantic Subtyping. *Electronic Notes in Theoretical Computer Science* 70, 1 (2003), 88 – 105. https://doi.org/10.1016/S1571-0661(04)80492-4 ITRS '02, Intersection Types and Related Systems (FLoC Satellite Event).

Jana Dunfield and Neel Krishnaswami. 2019a. Bidirectional Typing. CoRR abs/1908.05839 (2019). arXiv:1908.05839

Jana Dunfield and Neelakantan R. Krishnaswami. 2019b. Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types. *Proc. ACM Program. Lang.* 3, POPL, Article 9 (Jan. 2019), 28 pages. https://doi.org/10.1145/3290322

Facebook. *Flow*. Facebook https://flow.org/

Alain Frisch. 2004. *Théorie, conception et réalisation d'un langage de programmation adapté à XML*. Ph. D. Dissertation. Université Paris Diderot. http://www.cduce.org/papers/frisch_phd.pdf

Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. 2002. Semantic Subtyping. In *LICS '02, 17th Annual IEEE Symposium on Logic in Computer Science*. IEEE Computer Society Press, 137–146. https://doi.org/10.1109/LICS.2002.1029823

Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. 2008. Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types. *Journal of the ACM* 55, 4 (Sept. 2008), 19:1–19:64. http://doi.acm.org/10.1145/1391289.1391293

J. Roger Hindley and Jonathan P. Seldin. 2008. *Lambda-Calculus and Combinators An Introduction*. Cambridge University Press.

Andrew M. Kent. 2019. *Advanced Logical Type Systems for Untyped Languages*. Ph. D. Dissertation. Indiana University. https://pnwamk.github.io/docs/dissertation.pdf

David MacQueen, Gordon Plotkin, and Ravi Sethi. 1986. An ideal model for recursive polymorphic types. *Information and Control* 71, 1 (1986), 95–130. https://doi.org/10.1016/S0019-9958(86)80019-5

Per Martin-Löf. 1994. *Analytic and Synthetic Judgements in Type Theory*. Springer Netherlands, Dordrecht, 87–99. https://doi.org/10.1007/978-94-011-0834-8_5
Microsoft. *TypeScript*. Microsoft https://www.typescriptlang.org/

Tommaso Petrucciani. 2019. *Polymorphic Set-Theoretic Types for Functional Languages*. Ph. D. Dissertation. Joint Ph.D. Thesis, Università di Genova and Université Paris Diderot. https://tel.archives-ouvertes.fr/tel-02119930

Benjamin C. Pierce and David N. Turner. 2000. *Local Type Inference*. *ACM Trans. Program. Lang. Syst.* 22, 1 (Jan. 2000), 1–44. https://doi.org/10.1145/345099.345100

François Pottier and Yann Régis-Gianas. 2006. Stratified type inference for generalized algebraic data types. In *Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006*, Charleston, South Carolina, USA, January 11-13, 2006, J. Gregory Morrisett and Simon L. Peyton Jones (Eds.). ACM, 232–244. https://doi.org/10.1145/1111037.1111058

Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, and Panagiotis Vekris. 2015. Safe and Efficient Gradual Typing for TypeScript. In *Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages* (Mumbai, India) (POPL '15). Association for Computing Machinery, New York, NY, USA, 167–180. https://doi.org/10.1145/2676726.2676971

Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008. Liquid types. In *Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008*, Rajiv Gupta and Saman P. Amarasinghe (Eds.). ACM, 159–169. https://doi.org/10.1145/1375581.1375602

Amr Sabry and Matthias Felleisen. 1992. Reasoning about Programs in Continuation-Passing Style. In *Proceedings of the 1992 ACM Conference on LISP and Functional Programming (LFP '92)*. Association for Computing Machinery, 288–298. https://doi.org/10.1145/141471.141563

Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The Design and Implementation of Typed Scheme. In *Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages* (San Francisco, California, USA) (POPL '08). ACM, New York, NY, USA, 395–406. https://doi.org/10.1145/1328438.1328486

Sam Tobin-Hochstadt and Matthias Felleisen. 2010. Logical types for untyped languages. In *Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming* (Baltimore, Maryland, USA) (ICFP '10). ACM, New York, NY, USA, 117–128. https://doi.org/10.1145/1863543.1863561

Types 2019. What exactly should we call syntax-directed inference rules? Discussion on the Types mailing list. http://lists.seas.upenn.edu/pipermail/types-list/2019/002138.html.

Wikipedia. 2021. Peter Parker principle. https://en.wikipedia.org/wiki/With_great_power_comes_great_responsibility [Online; accessed 22-October-2021].

Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. *Information and Computation* 115, 1 (1994), 38–94. https://doi.org/10.1006/inco.1994.1093
# A SUPPLEMENTAL DEFINITIONS

## A.1 Subtyping Relation

Subtyping is defined by giving a set-theoretic interpretation of the types of Definition 2.1 into a suitable domain $\mathcal{D}$:

**DEFINITION A.1 (INTERPRETATION DOMAIN [FRISCH ET AL. 2008]).** The interpretation domain $\mathcal{D}$ is the set of finite terms $d$ produced inductively by the following grammar

$$d ::= c \mid (d, d) \mid \{(d, \partial), \dots, (d, \partial)\}$$
$$\partial ::= d \mid \Omega$$

where $c$ ranges over the set $C$ of constants and where $\Omega$ is such that $\Omega \notin \mathcal{D}$.

The elements of $\mathcal{D}$ correspond, intuitively, to (denotations of) the results of the evaluation of expressions. In particular, in a higher-order language, the results of computations can be functions which, in this model, are represented by sets of finite relations of the form $\{(d_1, \partial_1), \dots, (d_n, \partial_n)\}$, where $\Omega$ (which is not in $\mathcal{D}$) can appear in second components to signify that the function fails (i.e., evaluation is stuck) on the corresponding input. This is implemented by using in the second projection the meta-variable $\partial$ which ranges over $\mathcal{D}_{\Omega} = \mathcal{D} \cup \{\Omega\}$ (we reserve $d$ to range over $\mathcal{D}$, thus excluding $\Omega$). This constant $\Omega$ is used to ensure that $1 \to 1$ is not a supertype of all function types: if we used $d$ instead of $\partial$, then every well-typed function could be subsumed to $1 \to 1$ and, therefore, every application could be given the type $1$, independently from its argument as long as this argument is typable (see Section 4.2 of [Frisch et al. 2008] for details). The restriction to finite relations corresponds to the intuition that the denotational semantics of a function is given by the set of its finite approximations, where finiteness is a restriction necessary (for cardinality reasons) to give the semantics to higher-order functions.

We define the interpretation $[[t]]$ of a type $t$ so that it satisfies the following equalities, where $\mathcal{P}_{\text{fin}}$ denotes the restriction of the powerset to finite subsets and $\mathbb{B}$ denotes the function that assigns to each basic type the set of constants of that type, so that for every constant $c$ we have $c \in \mathbb{B}(b_c)$ (we use $b_c$ to denote the basic type of the constant $c$):

$$[[\emptyset]] = \emptyset \qquad [[t_1 \lor t_2]] = [[t_1]] \cup [[t_2]] \qquad [[\neg t]] = \mathcal{D} \setminus [[t]]$$
$$[[b]] = \mathbb{B}(b) \qquad [[t_1 \times t_2]] = [[t_1]] \times [[t_2]]$$
$$[[t_1 \to t_2]] = \{R \in \mathcal{P}_{\text{fin}}(\mathcal{D} \times \mathcal{D}_{\Omega}) \mid \forall(d, \partial) \in R. d \in [[t_1]] \implies \partial \in [[t_2]]\}$$

We cannot take the equations above directly as an inductive definition of $[[\cdot]]$ because types are not defined inductively but coinductively. Notice however that the contractivity condition of Definition 2.1 ensures that the binary relation $\triangleright \subseteq \text{Types} \times \text{Types}$ defined by $t_1 \lor t_2 \triangleright t_i, t_1 \land t_2 \triangleright t_i, \neg t \triangleright t$ is Noetherian. This gives an induction principle<fnref n="8" /> on Types that we use combined with structural induction on $\mathcal{D}$ to give the following definition, which validates these equalities.

**DEFINITION A.2 (SET-THEORETIC INTERPRETATION OF TYPES [FRISCH ET AL. 2008]).** We define a binary predicate $(d : t)$ ("the element $d$ belongs to the type $t$"), where $d \in \mathcal{D}$ and $t \in \text{Types}$, by

<footnote n="8">⁸In a nutshell, we can do proofs and give definitions by induction on the structure of unions and negations—and, thus, intersections—but arrows, products, and basic types are the base cases for the induction.</footnote>
induction on the pair $(d, t)$ ordered lexicographically. The predicate is defined as follows:

$$ (c : b) = c \in \mathbb{B}(b) $$

$$ ((d_1, d_2) : t_1 \times t_2) = (d_1 : t_1) \text{ and } (d_2 : t_2) $$

$$ ((d_1, \partial_1), \dots, (d_n, \partial_n)) : t_1 \to t_2) = \forall i \in [1..n]. \text{ if } (d_i : t_1) \text{ then } (\partial_i : t_2) $$

$$ (d : t_1 \lor t_2) = (d : t_1) \text{ or } (d : t_2) $$

$$ (d : \neg t) = \text{not } (d : t) $$

$$ (\partial : t) = \text{false} \qquad \text{otherwise} $$

We define the set-theoretic interpretation $\llbracket \cdot \rrbracket : \textbf{Types} \to \mathcal{P}(\mathcal{D})$ as $\llbracket t \rrbracket = \{d \in \mathcal{D} \mid (d : t)\}$.

Finally, we define the subtyping preorder and its associated equivalence relation as follows.

**DEFINITION A.3 (SUBTYPING RELATION [FRISCH ET AL. 2008]).** We define the subtyping relation $\leq$ and the subtyping equivalence relation $\approx$ as $t_1 \leq t_2 \iff \llbracket t_1 \rrbracket \subseteq \llbracket t_2 \rrbracket$ and $t_1 \approx t_2 \iff (t_1 \leq t_2)$ and $(t_2 \leq t_1)$.

## A.2 Capture Avoiding Substitution

$$ c\{e'/x\} = c \qquad (9) $$

$$ x\{e'/x\} = e' \qquad (10) $$

$$ y\{e'/x\} = y \qquad x \neq y \qquad (11) $$

$$ (\lambda x.e)\{e'/x\} = \lambda x.e \qquad (12) $$

$$ (\lambda y.e)\{e'/x\} = \lambda y.(e\{e'/x\}) \qquad x \neq y, y \notin \text{fv}(e') \qquad (13) $$

$$ (\lambda y.e)\{e'/x\} = \lambda z.(e\{z/y\}\{e'/x\}) \qquad x \neq y, y \in \text{fv}(e'), z \text{ fresh} \qquad (14) $$

$$ (e_1 e_2)\{e'/x\} = (e_1\{e'/x\})(e_2\{e'/x\}) \qquad (15) $$

$$ (e_1, e_2)\{e'/x\} = (e_1\{e'/x\}, e_2\{e'/x\}) \qquad (16) $$

$$ (\pi_i e)\{e'/x\} = \pi_i(e\{e'/x\}) \qquad (17) $$

$$ ((e_1 \in \tau) ? e_2 : e_3)\{e'/x\} = (e_1\{e'/x\} \in \tau) ? e_2\{e'/x\} : e_3\{e'/x\} \qquad (18) $$

## A.3 Canonical Declarative Deductions

$$ [\text{CONST}] \quad \frac{}{\Gamma \vdash_c c : b_c} $$

$$ [\text{Ax}] \quad \frac{}{\Gamma \vdash_c x : \Gamma(x)} x \in \text{dom}(\Gamma) $$

$$ [\to I^{(\Lambda)}] \quad \frac{\forall i \in I \quad \Gamma, x : s_i \vdash_c e : t_i}{\Gamma \vdash_c \lambda x.e : \bigwedge_{i \in I} s_i \to t_i} $$

$$ [\to E^{(\leq)}] \quad \frac{\Gamma \vdash_c e_1 : t \leq t_1 \to t_2 \quad \Gamma \vdash_c e_2 : t_1}{\Gamma \vdash_c e_1 e_2 : t_2} $$

$$ [\times I] \quad \frac{\Gamma \vdash_c e_1 : t_1 \quad \Gamma \vdash_c e_2 : t_2}{\Gamma \vdash_c (e_1, e_2) : t_1 \times t_2} $$

$$ [\times E_1^{(\leq)}] \quad \frac{\Gamma \vdash_c e : t \leq t_1 \times t_2}{\Gamma \vdash_c \pi_1 e : t_1} $$

$$ [\times E_2^{(\leq)}] \quad \frac{\Gamma \vdash_c e : t \leq t_1 \times t_2}{\Gamma \vdash_c \pi_2 e : t_2} $$

$$ [\vee^{+(\leq)}] \quad \frac{\Gamma \vdash_c e' : \bigvee_{i \in I} t_i \quad (\forall i \in I) \quad \Gamma, x : t_i \vdash_c e : s_i \leq t}{\Gamma \vdash_c e\{e'/x\} : t} \quad I \neq \emptyset $$

$$ [\emptyset] \quad \frac{\Gamma \vdash_c e : \emptyset}{\Gamma \vdash_c (e \in t) ? e_1 : e_2 : \emptyset} $$

$$ [\varepsilon_1^{(\leq)}] \quad \frac{\Gamma \vdash_c e : t_o \leq t \quad \Gamma \vdash_c e_1 : t_1}{\Gamma \vdash_c (e \in t) ? e_1 : e_2 : t_1} $$

$$ [\varepsilon_2^{(\leq)}] \quad \frac{\Gamma \vdash_c e : t_o \leq \neg t \quad \Gamma \vdash_c e_2 : t_2}{\Gamma \vdash_c (e \in t) ? e_1 : e_2 : t_2} $$
## A.4 Operators on Types

The various systems presented in this work use the following type-operators:

$$ \mathrm{dom}(t) = \max\{u \mid t \le u \to 1\} $$

$$ t \circ s = \min\{u \mid t \le s \to u\} $$

$$ t \bullet s = \min\{u \mid t \circ (\mathrm{dom}(t) \setminus u) \le \neg s\} $$

$$ t \triangleright s = \max\{u \mid t \circ u \le s\} $$

$$ \pi_1(t) = \min\{u \mid t \le u \times 1\} $$

$$ \pi_2(t) = \min\{u \mid t \le 1 \times u\} $$

In words, $t \circ s$ is the best (i.e., smallest wrt $\le$) type we can deduce for the application of a function of type $t$ to an argument of type $s$; $t \bullet s$ is the largest type in $\mathrm{dom}(t)$ such that the application of a function of type $t$ to an argument of that type will not surely give a result in $\neg s$, that is, it is the largest set of valid arguments that when applied to a function of type $t$ may return a result in $s$; $t \triangleright s$ is the largest set of valid arguments that when applied to a function of type $t$ only return results in $s$. Projection and domain are standard. All these operators can be effectively computed as shown below (see Castagna et al. [2022a]; Frisch et al. [2008] for details and proofs).

For $t \approx \bigvee_{i \in I} (\bigwedge_{p \in P_i} (s_p \to t_p) \wedge \bigwedge_{n \in N_i} \neg(s'_n \to t'_n))$, the first four operators are computed by:

$$ \mathrm{dom}(t) = \bigwedge_{i \in I} \bigvee_{p \in P_i} s_p $$

$$ t \circ s = \bigvee_{i \in I} \left( \bigvee_{\{Q \subseteq P_i \mid s \notin \bigvee_{q \in Q} s_q\}} \left( \bigwedge_{p \in P_i \setminus Q} t_p \right) \right) \quad (\text{for } s \le \mathrm{dom}(t)) $$

$$ t \bullet s = \mathrm{dom}(t) \wedge \bigvee_{i \in I} \left( \bigwedge_{\{P \subseteq P_i \mid s \le \bigvee_{p \in P} \neg t_p\}} \left( \bigvee_{p \in P} \neg s_p \right) \right) $$

$$ t \triangleright s = \bigwedge_{i \in I} \left( \bigvee_{\{P \subseteq P_i \mid \bigwedge_{p \in P} t_p \le s\}} \left( \bigwedge_{p \in P} s_p \right) \right) $$

For $t \approx \bigvee_{i \in I} (\bigwedge_{p \in P_i} (s_p, t_p) \wedge \bigwedge_{n \in N_i} \neg(s'_n, t'_n))$ the last two operators are computed by:

$$ \pi_1(t) = \bigvee_{i \in I} \bigvee_{N' \subseteq N_i} \left( \bigwedge_{p \in P_i} s_p \wedge \bigwedge_{n \in N'} \neg s'_n \right) $$

$$ \pi_2(t) = \bigvee_{i \in I} \bigvee_{N' \subseteq N_i} \left( \bigwedge_{p \in P_i} t_p \wedge \bigwedge_{n \in N'} \neg t'_n \right) $$
Furthermore the algorithm for reconstructing annotations uses the operator $t \circ_1 s$ defined as

$$ t \circ_1 s = \begin{cases} t \circ s & \text{if } s \le \text{dom}(t) \\ \mathbf{1} & \text{otherwise} \end{cases} $$

that can be easily computed from $\text{dom}(s)$ and $t \circ s$.

## A.5 Unwinding

$$
\begin{align*}
[c] &= c \\
[x] &= x \\
[\lambda x.e] &= \lambda x.[e] \\
[e_1 e_2] &= [e_1][e_2] \\
[(e_1, e_2)] &= ([e_1], [e_2]) \\
[\pi_i e] &= \pi_i [e] \qquad i = 1, 2 \\
[(e \in \tau) ? e_1 : e_2] &= ([e] \in \tau) ? [e_1] : [e_2] \\
[\text{bind } x = e_1 \text{ in } e_2] &= [e_2]{[e_1]/x}
\end{align*}
$$

## A.6 Reduction Semantics of the Intermediate Language

For the goals of this work it is not necessary to define a reduction semantics for the intermediate language defined in Section 3.1. This system was introduced to encode typing derivations, so what really matters is that any typable intermediate term has a type that can be deduced also for its unwinding. Nevertheless, it is interesting to define the reduction semantics of the annotated terms so that their reduction encodes the reduction of their unwindings.

The idea of this definition is that the bind-expressions must be evaluated only when their result is needed. In other words, binding-expressions follow a call-by-need reduction strategy. This can be formalized by using some specific contexts as follows.

A context $C$ is an expression with a hole (written $[]$) in it. We write $C[e]$ for the expression obtained by replacing the hole in $C$ with $e$. We write $C[e']$ for $C[e]$ when the free variables of $e$ are not bound by $C$: for example, $\text{bind } x = e_1 \text{ in } x$ is of the form $C[x] - \text{with } C \equiv (\text{bind } x = e_1 \text{ in } \text{[]}) - \text{but not of the form } C[x']$; conversely, $\text{bind } x = e_1 \text{ in } y$ is both of the form $C[y]$ and $C[y']$.

Evaluation contexts $E$ are the subset of contexts generated by the following grammar:

$$ E ::= [] | vE | Ee | (v, E) | (E, e) | \pi_i E | (E \in \tau) ? e : e | \text{bind } x = e \text{ in } E $$

We then add to the notions of reduction the following one:

$$ \text{bind } x = e \text{ in } E[x] \rightsquigarrow (E[x])\{e/x\} \qquad (19) $$

This implements the reduction defined for the declarative system (i.e., $[e] \rightsquigarrow [e']$ implies $e \rightsquigarrow^+ e'$). If we want to implement the parallel reduction of Appendix D.1.1, then we have to add also the following production to the definition of evaluation context:

$$ E ::= \text{bind } x = E \text{ in } E[x] $$

and replace the previous notion of reduction by the following one:

$$ \text{bind } x = v \text{ in } E[x] \rightsquigarrow (E[x])\{v/x\} \qquad (20) $$
## A.7 Canonical Forms for the Intermediate Language

The definition of the intermediate expressions is a step forward in solving the problem of typing a declarative expression, but it also brings a new problem, since we now have to decide where to put the bindings in a declarative expression so as to make it a typable intermediate expression. We can get rid of this problem simply by adding bindings wherever it is possible, so that every sub-expression of the original declarative expression will be bound to a variable. This corresponds to considering intermediate expressions that have a very specific form that we call *canonical forms* and that constitute a sub-language of the intermediate expressions.

An intermediate expression *e* is a *canonical form* if it is produced by the following grammar.

$$ \begin{array}{lcl} \textbf{Atomic expressions} & \mathbf{a} & ::= x \mid c \mid \lambda x. \mathbf{k} \mid (x, x) \mid xx \mid (x \in \tau) \ ? x : x \mid \pi_i x \\ \textbf{Canonical Forms} & \mathbf{k} & ::= x \mid \text{bind } x = \mathbf{a} \text{ in } \mathbf{k} \end{array} \qquad (21) $$

Canonical forms, ranged over by $\mathbf{k}$, are variables possibly preceded by a list of bindings of variables to atoms. Atoms are either $\lambda$-abstractions whose body is a canonical form or any other expression in which all proper sub-expressions are variables. Therefore, bindings can appear in a canonical form either at top-level or at the beginning of the body of a function. Notice that variables are atoms and, therefore, it is possible to have aliasing (e.g., bind $x = y$ in $\mathbf{k}$): we will get rid of aliasing in the next section, but having it here yields a simpler definition of the transformation $[.]$ later in this section.

Since canonical forms are also intermediate expressions, then the typing rules and the definition of unwinding for intermediate terms of Section 3.2 apply to canonical forms, too. Canonical forms are enough to “represent” well typed intermediate expressions since we have the following (non trivial) property:

**PROPOSITION A.4.** For every intermediate expression *e*, if $\Gamma \vdash_T e : t$, then there exists a canonical form $\mathbf{k}$ such that $\Gamma \vdash_T \mathbf{k} : t$ and $[e] = [\mathbf{k}]$.

Since a well-typed intermediate expression represents a class of derivations for the source language expression obtained by its unwinding, then the property above tells us that canonical forms suffice to provide such a representation.

We can prove the property above by defining a transformation from an intermediate expression to a canonical form that satisfies the property.

Let $\Delta$ denote a possibly empty list of mappings from variables to atoms. We note these lists extensionally by separating elements by a semicolon, that is, $x_1 \mapsto a_1; \dots; x_n \mapsto a_n$ and use $\varepsilon$ to denote the empty list. Next we define an operation term$(\Delta, x)$ which takes a list of mappings $\Delta$ and a variable $x$ and constructs the canonical form whose binding are those listed in $\Delta$ and whose body is $x$, that is:

$$ \begin{array}{lcl} \text{term}(\varepsilon, x) & \stackrel{\text{def}}{=} & x \\ \text{term}((y \mapsto a; \Delta), x) & \stackrel{\text{def}}{=} & \text{bind } y = a \text{ in term}(\Delta, x) \end{array} $$

We can now define the function $[e]$ that transforms an expression *e* into a pair $(\Delta, x)$ formed by a list of mappings $\Delta$ and a variable $x$ that will be bound to the atom representing *e*. The definition
is as follows, where $x_0$ is a fresh variable.

$$ [[c]] = ((x_0 \mapsto c), x_0) $$

$$ [[x]] = (\epsilon, x) $$

$$ [[\lambda x.e]] = ((x_0 \mapsto \lambda x.\text{term}[[e]]), x_0) $$

$$ [[\pi_i e]] = ((\Delta; x_0 \mapsto \pi_i x), x_0) \qquad \text{where } (\Delta, x) = [[e]] $$

$$ [[e_1 e_2]] = ((\Delta_1; \Delta_2; x_0 \mapsto x_1 x_2), x_0) \qquad \text{where } (\Delta_1, x_1) = [[e_1]], (\Delta_2, x_2) = [[e_2]] $$

$$ [[(e_1, e_2)]] = ((\Delta_1; \Delta_2; x_0 \mapsto (x_1, x_2)), x_0) \qquad \text{where } (\Delta_1, x_1) = [[e_1]], (\Delta_2, x_2) = [[e_2]] $$

$$ [[(e \in \tau) ? e_1 : e_2]] = ((\Delta; \Delta_1; \Delta_2; x_0 \mapsto (x \in \tau) ? x_1 : x_2), x_0) $$

$$ \text{where } (\Delta, x) = [[e]], (\Delta_1, x_1) = [[e_1]], (\Delta_2, x_2) = [[e_2]] $$

$$ [[\text{bind } x = e_1 \text{ in } e_2]] = ((\Delta_1; x \mapsto x_1; \Delta_2), x_2) \qquad \text{where } (\Delta_1, x_1) = [[e_1]], (\Delta_2, x_2) = [[e_2]] $$

Notice that if we remove the rule for bindings (i.e., the very last rule), the remaining rules define a transformation of the terms of the source language into a canonical form.

It is easy to see that $[\text{term}([e])] = [e]$ (or that $[\text{term}([e])] = e$ if $e$ is a term of the source language). Moreover, besides unwindings, this transformation preserves also types: if $\Gamma \vdash_T e : t$, then $\Gamma \vdash_T \text{term}([e]_\epsilon) : t$. These two results prove Proposition A.4.

We can thus use the result of Proposition A.4 to refine the Completeness Theorem 3.2 as follows:

**THEOREM A.5 (COMPLETENESS OF CANONICAL FORMS).** If $\Gamma \vdash e : t$ then $\exists \kappa, t' \text{ such that } [\kappa] = e$, $t' \le t$, and $\Gamma \vdash_T \kappa : t'$

This combined with the soundness Theorem 3.1 for intermediate expressions (recall that canonical forms are intermediate expressions) tells us that an expression of the source language is well-typed if and only if it is the unwinding of a well-typed canonical form.

## A.8 Maximal Sharing Canonical Forms

The transformation in Section A.7 returns just one of the possible canonical forms that satisfy Proposition A.4, but there are many of them. In order to infer types for the source language, we are interested in the canonical forms that satisfy four particular properties.

**DEFINITION A.6 (MSC FORMS).** A maximal sharing canonical form (abbreviated as MSC-form) is (any canonical form $\alpha$-equivalent to) a canonical form $\kappa$ such that:

(1) if bind $x_1 = a_1$ in $\kappa_1$ and bind $x_2 = a_2$ in $\kappa_2$ are distinct sub-expressions of $\kappa$, then $[a_1] \neq_\alpha [a_2]$

(2) if bind $x = a$ in $\kappa'$ is a sub-expression of $\kappa$, then $a$ is not a variable.

(3) if $\lambda x.\kappa_1$ is a sub-expression of $\kappa$ and bind $y = a$ in $\kappa_2$ a sub-expression of $\kappa_1$, then $fv(a) \notin fv(\lambda x.\kappa_1)$

(4) if bind $x = a$ in $\kappa'$ is a sub-expression of $\kappa$, then $x \in fv(\kappa')$.

MSC-forms are defined modulo $\alpha$-conversion.<fnref n="9" /> The first property states that distinct variables denote different (i.e., not $\alpha$-convertible) expressions of the source language. The second property forbids aliasing. The third property requires that bindings must extrude $\lambda$ abstractions whenever possible. The fourth condition states that there is no useless bind (the bound variable must occur in the body of the bind).

<footnote n="9">⁹For instance, both $\lambda x.bind z=xy$ in $zy$ and $\lambda x.bind z=xy$ in $z$ are two distinct atoms that can occur in the same MSC-form, even though the atom $xy$ appears in both: an $\alpha$-renaming of $x$ makes the first MSC-property hold.</footnote>
The first two properties ensure the maximal sharing of common sub-expressions in the source language, where *common sub-expressions* designate sets composed by different occurrences of sub-expressions that are equal (in our case, α-convertible). In other terms if we start from a source language term and we put it into a MSC-form, then all common sub-expressions occurring in it will be bound by the same variable. For instance, if we start from the term ($f3$, $f3$), then its MSC-form will be (α-equivalent to) bind $x = 3$ in bind $y = fx$ in bind $z = (y, y)$ in $z$: both occurrences of $f3$ are bound to $y$.<fnref n="10" />

The first three properties of Definition A.6 are important since they ensure that an expression of the source language is typable *if and only if* it is the unwinding of a typable MSC-form. For the first two properties, this is because reducing the bindings in an intermediate expression—while preserving unwinding—increases the typeability of a term: if we can type an intermediate term in which two distinct variables bind the same sub-expression, then the same term in which this sub-expression is bound by a single variable can also be typed by assigning to the unique variable the intersection of the types of the distinct variables, but the converse does not hold. For the third property this is because outer bindings may produce better types. For instance, consider the expression bind $x = a$ in $λy$. $x$, where $a$ is an expression that can be either an integer or a Boolean. This expression can be typed with ($1 \to \text{Int}$) $\lor$ ($1 \to \text{Bool}$). However for the expression $λy$. (bind $x = a$ in $x$) which has the same unwinding as the previous one, the most precise type one can deduce is $1 \to (\text{Int} \lor \text{Bool})$, which is strictly larger than ($1 \to \text{Int}$) $\lor$ ($1 \to \text{Bool}$).

The last property of Definition A.6 is important because it ensures that given a source language expression $e$ there exists a unique (modulo α-conversion and the order of bindings) MSC-form whose unwinding is $e$ (cf. Proposition A.8): we denote this MSC-form by MSC($e$).

An important property of MSC-forms is that given an expression $e$ of the source language, all its MSC-forms (i.e., all MSC-form whose unwinding is $e$) are the same modulo the order in which their bindings appear. Formally, we define the following congruence on canonical forms:

**DEFINITION A.7 (CANONICAL EQUIVALENCE).** We denote by $\equiv_κ$ the smallest congruence on canonical forms that is closed by α-conversion and such that

$$ \text{bind } x_1 = a_1 \text{ in bind } x_2 = a_2 \text{ in } \kappa \equiv_κ \text{bind } x_2 = a_2 \text{ in bind } x_1 = a_1 \text{ in } \kappa \quad x_1 \notin \text{fv}(a_2), x_2 \notin \text{fv}(a_1) \quad (22) $$

Then we prove that all the MSC forms of a source language expression are equivalent:

**PROPOSITION A.8.** If $κ_1$ and $κ_2$ are two MSC-forms and $[κ_1] \equiv_α [κ_2]$, then $κ_1 \equiv_κ κ_2$.

It is easy to observe that the canonical equivalence preserves typeability (this is a direct consequence that type environments are mappings in which order does not matter).

It is easy to transform a canonical form into a MSC-form that has the same type and the same unwinding. This can be done by applying the rewriting rules below, that are confluent and normalizing.

<footnote n="10">¹⁰Notice that this would not be true if aliasing were allowed: for instance ($f3$, $f3$) could be transformed into bind $x = 3$ in bind $w = x$ in bind $y_1 = fx$ in bind $y_2 = fw$ in bind $z = (y_1, y_2)$ in $z$</footnote>
$$ \begin{array}{lclcl} \text{bind } x_1 = \mathbf{a}_1 \text{ in} & \longrightarrow & \text{bind } x_1 = \mathbf{a}_1 \text{ in } \mathbf{\kappa}\{x_1/x_2\} & & \mathbf{a}_1 \equiv_{\alpha} \mathbf{a}_2 \qquad (23) \\ \text{bind } x_2 = \mathbf{a}_2 \text{ in } \mathbf{\kappa} & \longrightarrow & \mathbf{\kappa} & & x \notin \text{fv}(\mathbf{\kappa}) \qquad (24) \end{array} $$

$$ \text{bind } x = \mathbf{a} \text{ in } \mathbf{\kappa} \quad \longrightarrow \quad \mathbf{\kappa} \qquad x \notin \text{fv}(\mathbf{\kappa}) \qquad (24) $$

$$ \lambda x.(\text{bind } y = x \text{ in } \mathbf{\kappa}) \longrightarrow \lambda x.\mathbf{\kappa}\{x/y\} \qquad (25) $$

$$ \begin{array}{lclcl} \text{bind } x = \mathbf{a} \text{ in} & \longrightarrow & \text{bind } x = \mathbf{a} \text{ in } \mathbf{\kappa}\{x/y\} & & (26) \\ \text{bind } y = x \text{ in } \mathbf{\kappa} & & & & \end{array} $$

$$ \begin{array}{lclcl} \text{bind } x = \lambda y.( & \longrightarrow & \text{bind } z = \mathbf{a} \text{ in} & & y \notin \text{fv}(\mathbf{a}), z \notin \text{fv}(\mathbf{\kappa}) \qquad (27) \\ \text{bind } z = \mathbf{a} \text{ in } \mathbf{\kappa}_o) & & & & \\ \text{in } \mathbf{\kappa} & & & & \end{array} $$

$$ \mathbf{\kappa}_1 \longrightarrow \mathbf{\kappa}_2 \qquad \exists \mathbf{\kappa}'_1. \mathbf{\kappa}_1 \equiv_{\mathbf{\kappa}} \mathbf{\kappa}'_1 \longrightarrow \mathbf{\kappa}_2 \qquad (28) $$

Rule (23) implements the maximal sharing: if two variables bind atoms with the same unwinding (modulo $\alpha$-conversion), then the variables are unified. Rule (24) removes useless bindings while (25) and (26) removes aliases. Rule (27) extrudes bindings from abstractions of variables that do not occur in the argument of the binding. Rule (28) applies the previous rule modulo the canonical equivalence: in practice it applies the swap of binding defined in (22) as many times as it is needed to apply one of the other rules. As customary, these rules can be applied under any context.

Since the transformation above transforms every well-typed canonical form into an MSC-form that has the same type (or a more precise one) and the same unwinding, the completeness theorem of canonical forms already holds for MSC-form. The theorem can thus be stated as follows:

**THEOREM A.9 (COMPLETENESS OF MSC-FORMS).** If $\vdash e : t$ then $\exists \mathbf{\kappa}, t'$ such that $\mathbf{\kappa}$ is a maximal sharing canonical form, $[\mathbf{\kappa}] \equiv_{\alpha} e, t' \le t$, and $\vdash_I \mathbf{\kappa} : t'$

Notice that now we used $\alpha$-conversion instead of equality, since $e$ may contain $\alpha$-equivalent but not equal subterms that the MSC-form $\mathbf{\kappa}$ would of course unify.

*Putting it All Together.* The corollary of these propositions is that an expression $e$ is typable if and only if its unique (modulo $\equiv_{\kappa}$) MSC-form is typable, too. More formally, given an expressions $e$ of the source language, let us denote by MSC($e$) any element of the set $\{\mathbf{\kappa} \mid e \equiv_{\alpha} [\mathbf{\kappa}] \text{ and } \mathbf{\kappa}$ is a MSC-form\}$ that is, the unique (modulo $\equiv_{\kappa}$) MSC-form of $e$. Then we have

**COROLLARY A.10 (SOUNDNESS AND COMPLETENESS).** For every closed term $e$ of the source language

$$ \vdash e : t \quad \Rightarrow \quad \vdash_I \text{MSC}(e) : t' \le t \qquad (\text{completeness}) $$

$$ \vdash e : t \quad \Leftarrow \quad \vdash_I \text{MSC}(e) : t \qquad (\text{soundness}) $$

Finally, it is straightforward to generate a particular MSC-form for a closed source language expression $e$: simply apply the rewriting rules in (23)–(28) to term $[e]$. Corollary A.10 states that this MSC-form is typable if and only if $e$ is: we reduced the problem of typing $e$ to the one of typing a MSC-form of $e$, form that we can effectively produce from $e$ and for which we have a syntax-directed type system.
A.9 Algorithmic Typing Rules

$$ [\text{CONST-ALG}] \quad \frac{\Gamma \vdash_{\mathcal{A}} c : \mathbf{b}_c}{\Gamma} \qquad [\text{AX-ALG}] \quad \frac{\Gamma \vdash_{\mathcal{A}} x : \Gamma(x)}{\Gamma} \qquad x \in \text{dom}(\Gamma) $$

$$ [\to\text{I-ALG}] \quad \frac{(\forall j \in J) \quad \Gamma, x : t_j \vdash_{\mathcal{A}} \kappa : s_j}{\Gamma \vdash_{\mathcal{A}} \lambda x : \{\Gamma_i \vdash t_i\}_{i \in I} \kappa : \bigwedge_{j \in J} t_j \to s_j} \quad J = \{i \in I \mid \Gamma \leq \Gamma_i\} \neq \emptyset $$

$$ [\to\text{E-ALG}] \quad \frac{\Gamma \vdash_{\mathcal{A}} x_1 : t_1 \quad \Gamma \vdash_{\mathcal{A}} x_2 : t_2}{\Gamma \vdash_{\mathcal{A}} x_1 x_2 : t_1 \circ t_2} \quad \begin{array}{l} t_1 \leq \emptyset \to \mathbb{1} \\ t_2 \leq \text{dom}(t_1) \end{array} $$

$$ [\times\text{I-ALG}] \quad \frac{\Gamma \vdash_{\mathcal{A}} x_1 : t_1 \quad \Gamma \vdash_{\mathcal{A}} x_2 : t_2}{\Gamma \vdash_{\mathcal{A}} (x_1, x_2) : t_1 \times t_2} $$

$$ [\times\text{E}_1\text{-ALG}] \quad \frac{\Gamma \vdash_{\mathcal{A}} x : t \leq (1 \times 1)}{\Gamma \vdash_{\mathcal{A}} \pi_1 x : \pi_1(t)} \qquad [\times\text{E}_2\text{-ALG}] \quad \frac{\Gamma \vdash_{\mathcal{A}} x : t \leq (1 \times 1)}{\Gamma \vdash_{\mathcal{A}} \pi_2 x : \pi_2(t)} \qquad [\mathbf{0}\text{-ALG}] \quad \frac{\Gamma \vdash_{\mathcal{A}} x : \emptyset}{\Gamma \vdash_{\mathcal{A}} (x \in t) ? x_1 : x_2 : \emptyset} $$

$$ [\in_1\text{-ALG}] \quad \frac{\Gamma \vdash x : t_0 \leq t \quad \Gamma \vdash x_1 : t_1}{\Gamma \vdash (x \in t) ? x_1 : x_2 : t_1} \quad t_0 \neq \emptyset \qquad [\in_2\text{-ALG}] \quad \frac{\Gamma \vdash_{\mathcal{A}} x : t_0 \leq \neg t \quad \Gamma \vdash x_2 : t_2}{\Gamma \vdash_{\mathcal{A}} (x \in t) ? x_1 : x_2 : t_2} \quad t_0 \neq \emptyset $$

$$ [\vee_1\text{-ALG}] \quad \frac{\Gamma \vdash_{\mathcal{A}} \kappa : s}{\Gamma \vdash_{\mathcal{A}} \text{bind } x : \{\Gamma_i \vdash t_i\}_{i \in I} = a \text{ in } \kappa : s} \quad \begin{array}{l} x \notin \text{dom}(\Gamma) \\ \{i \in I \mid \Gamma \leq \Gamma_i\} = \emptyset \end{array} $$

$$ [\vee_2\text{-ALG}] \quad \frac{\Gamma \vdash_{\mathcal{A}} a : \bigvee_{j \in J} t_j \quad (\forall j \in J) \quad \Gamma, x : t_j \vdash_{\mathcal{A}} \kappa : s_j}{\Gamma \vdash_{\mathcal{A}} \text{bind } x : \{\Gamma_i \vdash t_i\}_{i \in I} = a \text{ in } \kappa : \bigvee_{j \in J} s_j} \quad J = \{i \in I \mid \Gamma \leq \Gamma_i\} \neq \emptyset $$
# B ALGORITHM FOR RECONSTRUCTING ANNOTATIONS

In this section we give the complete definition of the algorithm for the reconstruction of annotations together with all the auxiliary operations it uses. We start in Section B.1 with the definitions that concern the refinement of the type environments. In Section B.2 we define the operations that manipulate type environments, annotations and their types, in particular to (1) partition a set of types into a set of disjoint types, to (2) manipulate expressions, in particular to restrict and empty their annotations and to merge several expressions that differ only by their annotations and (3) to extract and propagate the information provided by sets of refinements. Section B.3 present the inference rules that define a single pass of our algorithm.

## B.1 Type Environment Refinements

During the annotation reconstruction process, we start from a generic context and generic annotations (initially 1) and specialize them when necessary as we progress into the expression. In order to refine an environment, we use the following operator.

**DEFINITION B.1 (REFINEMENT OF ENVIRONMENTS).** Let $\Gamma$ a type environment, $x$ a variable and $t$ a type. We define the refinement $\Gamma[x \triangleq t]$ as follows:

$$ \Gamma[x \triangleq t] \stackrel{\text{def}}{=} \begin{cases} (\Gamma \setminus \{x \mapsto \Gamma(x)\}) \cup \{x \mapsto \Gamma(x) \wedge t\} & \text{if } x \in \text{dom}(\Gamma) \text{ and } (\Gamma(x) \simeq \emptyset \text{ or } \Gamma(x) \wedge t \neq \emptyset) \\ \text{undefined} & \text{otherwise} \end{cases} $$

Note that this operator is undefined when $x \notin \text{dom}(\Gamma)$: we do not want to consider refinements on variables that are not in the context. It is also undefined when $\Gamma(x) \neq \emptyset$ and $\Gamma(x) \wedge t \simeq \emptyset$: we do not want to consider refinements that require a variable to have an empty type, except if this variable already had an empty type before the refinement.

**Necessary Refinements.** In a term in canonical form, type-cases test the type of variables bound to atoms. So, morally we are examining expressions of the form $(a \in t) ? a_1 : a_2$. To precisely type such an expression we need to determine the conditions under which each branch is selected or not. The "conditions" at issue are given as possible refinements of the current type environment. More precisely, given a type environment $\Gamma$ and an atom $a$ that is typable under the type environment $\Gamma$, we want to refine the types of the free variables of $a$ in $\Gamma$ so that any result of $a$ under this refined context will possibly be of type $t$.

Rather than a single refinement we will look a finite set of refinements which will be described by a finite set $\{\Gamma_i\}_{i \in I}$ of type environments. Each of these environments $\Gamma_i$ will be subsumed (in the sense of Definition 4.1) by the initial environment $\Gamma$.

In particular, we are interested in refinements that are *necessary* (but may not be sufficient) to ensure that $a$ will produce results of type $t$. This will allow the system to give a precise typing to the branches of typecase expressions by integrating the information that if the branch was selected, then the type-test failed/succeeded.

More precisely, we define a quaternary relations that takes an atom $a$, a type $t$ (into which $a$ must reduce), the current type-environment $\Gamma$ (under which $a$ is typable) and a finite set $\{\Gamma_i\}_{i \in I}$ of type environments subsumed by $\Gamma$. We denote this relation by the following judgment (we use the modal symbol $\sqsubseteq$ to stress that the atom $a$ does not diverge and reduces to a value in $t$):

$$ [\Gamma \vdash \Box(a \rightsquigarrow t)] \supset \{\Gamma_i\}_{i \in I} $$

meaning that if $a$ must reduce to values of type $t$ (connective $\sqsubseteq$), then it is *necessary* (connective $\supset$) that *at least one* of the refinements $\Gamma_i$ of $\Gamma$ holds.

In particular $[\Gamma \vdash \Box(a \rightsquigarrow t)] \supset \{\}$ means that it is impossible under the hypothesis $\Gamma$ that $a$ produces a value of type $t$; $[\Gamma \vdash \Box(a \rightsquigarrow t)] \supset \{\Gamma\}$ means that $\Gamma$ already provides all conditions that
are necessary for *a* to produce a value of type *t*. For example, we have: $[\Gamma \vdash \Box(42 \rightsquigarrow \mathbf{Bool})] \supset \{\}, [\Gamma \vdash \Box(42 \rightsquigarrow \mathbf{Int})] \supset \{\Gamma\}$, and $[x:1 \vdash \Box((x, x) \rightsquigarrow (\mathbf{Int} \times \mathbf{Int}) \vee (\mathbf{Bool} \times \mathbf{Bool}))] \supset \{(x:\mathbf{Int}), (x:\mathbf{Bool})\}$. The latter states that for $(x, x)$ to reduce to a value of type $(\mathbf{Int} \times \mathbf{Int}) \vee (\mathbf{Bool} \times \mathbf{Bool})$ it is necessary that either $x$ is of type $\mathbf{Int}$ or $x$ is of type $\mathbf{Bool}$.

The quaternary relation is defined by induction on atoms as follows:

$$ [\Gamma \vdash \Box(c \rightsquigarrow t)] \supset \{\} \qquad \mathbf{b}_c \wedge t \simeq \emptyset \quad (29) $$

$$ [\Gamma \vdash \Box(c \rightsquigarrow t)] \supset \{\Gamma\} \qquad \mathbf{b}_c \wedge t \neq \emptyset \quad (30) $$

$$ [\Gamma \vdash \Box(x_1 x_2 \rightsquigarrow t)] \supset \{\Gamma[x_1 \stackrel{\triangle}{=} t_i][x_2 \stackrel{\triangle}{=} t_i \bullet t] \mid i \in I\} \quad \Gamma(x_1) \stackrel{\text{DNF}}{\simeq} \bigvee_{i \in I} t_i \quad (31) $$

$$ [\Gamma \vdash \Box(\lambda x.\kappa \rightsquigarrow t)] \supset \{\} \qquad (\emptyset \to \mathbf{1}) \wedge t \simeq \emptyset \quad (32) $$

$$ [\Gamma \vdash \Box(\lambda x.\kappa \rightsquigarrow t)] \supset \{\Gamma\} \qquad (\emptyset \to \mathbf{1}) \wedge t \neq \emptyset \quad (33) $$

$$ [\Gamma \vdash \Box(\pi_1 x \rightsquigarrow t)] \supset \{\Gamma[x \stackrel{\triangle}{=} t \times \mathbf{1}]\} \quad (34) $$

$$ [\Gamma \vdash \Box(\pi_2 x \rightsquigarrow t)] \supset \{\Gamma[x \stackrel{\triangle}{=} \mathbf{1} \times t]\} \quad (35) $$

$$ [\Gamma \vdash \Box((x_1, x_2) \rightsquigarrow \bigvee_{i \in I} (t_i \times s_i))] \supset \{\Gamma[x_1 \stackrel{\triangle}{=} t_i][x_2 \stackrel{\triangle}{=} s_i] \mid i \in I\} \quad (36) $$

$$ [\Gamma \vdash \Box((x \in \tau) ? x_1 : x_2 \rightsquigarrow t)] \supset \{\Gamma[x_1 \stackrel{\triangle}{=} t][x \stackrel{\triangle}{=} \tau], \Gamma[x_2 \stackrel{\triangle}{=} t][x \stackrel{\triangle}{=} \neg \tau]\} \quad (37) $$

with the convention that the sets on the right-hand side of the relations contain only the type-environments for which the operations are defined. So for instance in (34) if $(t \times \mathbf{1}) \wedge \Gamma(x) \simeq \emptyset$, then $\Gamma[x \stackrel{\triangle}{=} t \times \mathbf{1}]$ is undefined and therefore $[\Gamma \vdash \Box(\pi_1 x \rightsquigarrow t)] \supset \{\}$ holds.

Let us explain the rules for each atom. If the atom is a constant *c* then (29) states that it is impossible that the constant produces a result of type *t* if $\mathbf{b}_c \wedge t \simeq \emptyset$; if instead $\mathbf{b}_c \wedge t \neq \emptyset$, then (30) states that $\Gamma$ does not need to be refined (actually, it cannot be refined since the atom *c* has no free variables to refine) to ensure that *c* may produce such a result.

The case (31) for the application of a function $x_1$ of type $\bigvee_{i \in I} t_i$ to an argument $x_2$ is the most interesting one and needs detailed explanation. In short, rule (31) states that if the application must produce a result of type *t*, then there must exist *i* ∈ *I* such that the function is of type $t_i$, $t_i$ is a functional type (i.e., a subtype of $\emptyset \to \mathbf{1}$), and the argument has type $t_i \bullet t$ which, by definition, ensures the property. Let us explain each single bit. First of all, the rule states $\Gamma(x_1) \stackrel{\text{DNF}}{\simeq} \bigvee_{i \in I} t_i$. This means that we take the type $\Gamma(x_1)$ of $x_1$ and we transform it in its disjunctive normal form as defined by Frisch et al. [2008, Section 6.1]. This is a union of intersections of literals of the same form. A literal is an atomic type or its negation. An atomic type (and, thus, literals) has three possible forms: it is either a basic type or an arrow type or a product type. For instance, if *t* is a function type, that is, $t \le \emptyset \to \mathbf{1}$, then it is equivalent to a union of intersections of arrows and their negations: $t \stackrel{\text{DNF}}{\simeq} \bigvee_{i \in I}(\wedge_{p \in P_i}(s_p \to t_p) \wedge \wedge_{n \in N_i} \neg(s'_n \to t'_n))$ for some $P_i$'s and $N_i$'s, a property we used in Appendix A.4. Also in Appendix A.4 there is the definition of $t_i \bullet t$ which is the largest type we can give to an argument of a function of type $t_i$ so that the application may yield a result of type *t*, which is exactly what we need here. Also notice that $t_i \bullet t$ is defined only for $t_i \le \emptyset \to \mathbf{1}$, which means that a refinement will be produced only for those $t_i$ of the disjunctive normal form of $\Gamma(x_1)$ that are functional types. Finally, disjunctive normal forms are not unique but the best results for our algorithm are obtained when the disjunctive normal forms for products are formed by disjoint sets of minimum cardinality (e.g., $(\mathbf{Int}, \mathbf{Int} \vee \mathbf{Bool}) \vee (\mathbf{Int}, \mathbf{Int} \vee \mathbf{String})$) will be decomposed as $(\mathbf{Int}, \mathbf{Int} \vee \mathbf{Bool} \vee \mathbf{String})$ rather than as $(\mathbf{Int}, \mathbf{Int}) \vee (\mathbf{Int}, \mathbf{Bool}) \vee (\mathbf{Int}, \mathbf{String})$) while soundness of our algorithm requires that the disjunctive normal form for arrows has minimum cardinality (obviously they cannot be disjoint unions, since $\mathbf{1} \to \emptyset$ is in the intersection of any pair of arrows). In practice in our implementation we will use the result of the normalize function provided by the CDuce API for types.
The cases for λ-abstraction are just rough approximations since we do not try to refine the type of the variables that are free in the body of a function to determine the type of that function.<fnref n="11" /> As a consequence, the treatment of λ-abstractions is similar to the one for constants. In particular, (33) states that if *t* contains some functions, then we do not need to do anything to ensures that the λ-abstraction may be of type *t*.

The other cases are straightforward. For a projection to yield a result of a certain type the projected expression must be of the corresponding product types (34-35); for a pair to yield a value in a union of products, it must yield a value in at least one of the summands of the union; finally, a type-case will yield a result in *t* if and only if the branch that is selected does it.

## B.2 Auxiliary Definitions

The rules in the next section use several auxiliary functions, some of which where already introduced and more or less formally described in Section 5. We recall all of them with their definitions.

**partition**($\{t_i\}_{i \in I}$) is the smallest (in terms of cardinality) non empty set of types $\{s_j\}_{j \in J}$ such that (i) $\bigvee_{j \in J} s_j \simeq \bigvee_{i \in I} t_i$, (ii) $\forall j \in J. \forall j' \in J. j \neq j' \Rightarrow s_j \wedge s_{j'} \simeq \emptyset$, and (iii) $\forall j \in J. \forall i \in I. s_j \leq t_i$ or $s_j \wedge t_i \simeq \emptyset$. Notice that since partition must return a non-empty set, then for $\bigvee_{i \in I} t_i \simeq \emptyset$ we have partition($\{t_i\}_{i \in I}$) = $\{\emptyset\}$.

**empty**($\varphi$) (where $\varphi$, we recall, denotes either an algorithmic atom $a$ or an algorithmic expression $\kappa$) replaces all the annotations in $\varphi$ by the empty annotation $\emptyset$.

**merge**$_\varphi$($\{\varphi_i\}_{i \in I}$) is defined when all $\varphi_i$ are the same except for their annotations (i.e., they all have the same erasure $\langle\varphi_i\rangle$) and produces a new annotated expression that concatenates all these annotations. If $I = \emptyset$, then it returns empty($\varphi$).

**propagate**$_{x,a,t}$($\Gamma$) propagates to the types of the free variables of $a$ any refinement of $t$ specified in the typings of $x$ in the environments in $\Gamma$. Essentially it applies $[\Gamma \vdash \square(a \multimap \Gamma(x))] \supset \Gamma'$ for each $\Gamma \in \Gamma$ for which a refinement must be propagated. It is defined as:

$$ \text{propagate}_{x,a,t}(\{\Gamma_i\}_{i \in I}) \stackrel{\text{def}}{=} \bigcup_{i \in I} \Gamma_i \quad \text{with } \forall i \in I. \quad \left\{ \begin{array}{ll} \Gamma_i = \{\Gamma_i\} & \text{if } t \le \Gamma_i(x) \\ [\Gamma_i \vdash \square(a \multimap \Gamma_i(x))] \supset \Gamma_i & \text{otherwise} \end{array} \right. $$

**extract**$_x$($\Gamma$) extracts from $\Gamma$ all the hypotheses about $x$ to create a new annotation that it returns with the set of type environments from which these hypotheses were removed, that is, $\text{extract}_x(\Gamma) \stackrel{\text{def}}{=} \{(\Gamma \multimap x) \vdash \Gamma(x) \mid \Gamma \in \Gamma\}, \{\Gamma \multimap x \mid \Gamma \in \Gamma\}$) where $\Gamma \multimap x \stackrel{\text{def}}{=} \Gamma \multimap \{x \mapsto \Gamma(x)\}$.

($\Gamma \vdash A$) denotes the set of the types of the annotation $A$ that are compatible with (i.e., whose hypotheses subsume) $\Gamma$, that is, $(\Gamma \vdash A) \stackrel{\text{def}}{=} \{t \mid \Gamma' \vdash t \in A \text{ and } \Gamma \le \Gamma'\}$. We use $\bigvee(\Gamma \vdash A)$ to denote the union of these types.

**restrict**$_\Gamma$($A$) refines all the type environments in the annotation $A$ with the hypotheses in $\Gamma$, that is $\text{restrict}_\Gamma(A) \stackrel{\text{def}}{=} \{(\Gamma \wedge \Gamma') \vdash t \mid \Gamma' \vdash t \in A\}$ where $\Gamma \wedge \Gamma'$ denotes the pointwise intersection of two type environments with possibly distinct domains, which is formally defined as:

$$ (\Gamma \wedge \Gamma')(x) \stackrel{\text{def}}{=} \left\{ \begin{array}{ll} \Gamma(x) & \text{if } x \in \text{dom}(\Gamma) \setminus \text{dom}(\Gamma') \\ \Gamma'(x) & \text{if } x \in \text{dom}(\Gamma') \setminus \text{dom}(\Gamma) \\ \Gamma(x) \wedge \Gamma'(x) & \text{if } x \in \text{dom}(\Gamma) \cap \text{dom}(\Gamma') \\ \text{undefined} & \text{otherwise} \end{array} \right. $$

$\text{restrict}_\Gamma(\varphi)$ replaces every annotation $A$ in $\varphi$ by $\text{restrict}_\Gamma(A)$.

We have now all the notions to formally define the inference rules of our algorithm.

<footnote n="11">¹¹As a matter of fact, it is possible to handle this case more precisely, but for the sake of simplicity we do not do it here.</footnote>
## B.3 Annotations Reconstruction Rules

The rules below use the convention that the sets on the right-hand side of the conclusion contain only the type-environments for which the operations are defined. In particular, only the environment refinements $\Gamma[x := t]$ for which $x \in \text{dom}(\Gamma)$ and $(\Gamma(x) \approx \emptyset$ or $\Gamma(x) \wedge t \neq \emptyset)$ are considered. This in particular means that the set notation $\{\Gamma[x := t_i]\}_{i \in I}$ used in the rules must be considered as a shorthand for $\{\Gamma_i | i \in I, \Gamma_i = \Gamma[x := t_i], \Gamma_i(x) \neq \emptyset\}$. We list all the rules below and comment them next.

$$ [\text{CONST}] \quad \frac{b_c \le t}{\Gamma \vdash_R c : t \Rightarrow (c, \{\Gamma\})} $$

$$ [\text{CONSTUNTYPABLE}] \quad \frac{b_c \not\le t}{\Gamma \vdash_R c : t \Rightarrow (c, \{\})} $$

$$ [\text{PROJEMPTY}] \quad \frac{\Gamma(x) \approx \emptyset}{\Gamma \vdash_R \pi_i x : t \Rightarrow (\pi_i x, \{\Gamma\})} $$

$$ [\text{PROJ1}] \quad \frac{\Gamma(x) \wedge (t \times 1)^{\text{DNF}} \bigvee_{i \in I} t_i \times s_i}{\Gamma \vdash_R \pi_1 x : t \Rightarrow (\pi_1 x, \{\Gamma[x := \hat{t}_i \times s_i]\}_{i \in I})} \qquad [\text{PROJ2}] \quad \frac{\Gamma(x) \wedge (1 \times t)^{\text{DNF}} \bigvee_{i \in I} t_i \times s_i}{\Gamma \vdash_R \pi_2 x : t \Rightarrow (\pi_2 x, \{\Gamma[x := \hat{t}_i \times s_i]\}_{i \in I})} $$

$$ [\text{PAIREEmpty}] \quad \frac{\Gamma(x_1) \times \Gamma(x_2) \approx \emptyset}{\Gamma \vdash_R (x_1, x_2) : t \Rightarrow ((x_1, x_2), \{\Gamma\})} $$

$$ [\text{PAIR}] \quad \frac{t \wedge (1 \times 1)^{\text{DNF}} \bigvee_{i \in I} t_i \times s_i}{\Gamma \vdash_R (x_1, x_2) : t \Rightarrow ((x_1, x_2), \{\Gamma[x_1 := \hat{t}_i][x_2 := \hat{s_i}]\}_{i \in I})} $$

$$ [\text{CASEEmpty}] \quad \frac{\Gamma(x) \approx \emptyset}{\Gamma \vdash_R (x \in t) ? x_1 : x_2 : t \Rightarrow ((x \in t) ? x_1 : x_2, \{\Gamma\})} $$

$$ [\text{CASE}] \quad \frac{\Gamma \vdash_R (x \in s) ? x_1 : x_2 : t \Rightarrow ((x \in s) ? x_1 : x_2, \{\Gamma[x := \hat{s}] [x_1 := \hat{t}], \Gamma[x := \neg s] [x_2 := \hat{t}]\})}{\Gamma \vdash_R (x \in s) ? x_1 : x_2 : t \Rightarrow ((x \in s) ? x_1 : x_2, \{\Gamma[x := \hat{s}] [x_1 := \hat{t}], \Gamma[x := \neg s] [x_2 := \hat{t}]\})} $$

$$ [\text{APPREEmpty}] \quad \frac{\Gamma(x_2) \approx \emptyset \quad \Gamma(x_1) \le \emptyset \to 1}{\Gamma \vdash_R x_1 x_2 : t \Rightarrow (x_1 x_2, \{\Gamma\})} $$

$$ [\text{APPLEEmpty}] \quad \frac{\Gamma(x_1) \approx \emptyset \quad x_2 \in \text{dom}(\Gamma)}{\Gamma \vdash_R x_1 x_2 : t \Rightarrow (x_1 x_2, \{\Gamma\})} $$

$$ [\text{APPR}] \quad \frac{\Gamma(x_1)^{\text{DNF}} \wedge \bigwedge_{i \in I} (s_i \to t_i) \wedge \bigwedge_{j \in J} (\neg(s'_j \to t'_j))}{\Gamma \vdash_R x_1 x_2 : t \Rightarrow (x_1 x_2, \{\Gamma[x_1 := (s_i \wedge \Gamma(x_2)) \to t][x_2 := \hat{s_i}]\}_{i \in I})} $$

$$ [\text{APPL}] \quad \frac{\Gamma(x_1) \wedge (\emptyset \to 1)^{\text{DNF}} \bigvee_{i \in I} s_i \quad x_2 \in \text{dom}(\Gamma)}{\Gamma \vdash_R x_1 x_2 : t \Rightarrow (x_1 x_2, \{\Gamma[x_1 := \hat{s_i}]\}_{i \in I})} $$

$$ [\text{ABS}] \quad \frac{t^{\text{DNF}} \wedge \bigwedge_{j \in J} (s_j \to t_j) \quad (\Gamma \triangleright A) \neq \emptyset \quad \bigvee_{j \in J} s_j \leq \bigvee (\Gamma \triangleright A)}{\{s_i\}_{i \in I} = \text{partition}((\Gamma \triangleright A) \cup \{s_j \mid j \in J\}) \quad \forall i \in I. \Gamma, (x : s_i) \vdash_R K : t \circ_1 s_i \Rightarrow (\kappa_i, \Gamma'_i) \\ \forall i \in I. (A_i, \Gamma'_i) = \text{extract}_x(\Gamma'_i) \quad A' = \bigcup_{i \in I} A_i \quad \bigvee_{j \in J} s_j \leq \bigvee \{s' \mid (\Gamma' \triangleright s') \in A'\} \\ \Gamma \vdash_R \lambda x : A. \kappa : t \Rightarrow (\lambda x : A'. \text{merge}_\kappa(\{\kappa_i\}_{i \in I}), \bigcup_{i \in I} \Gamma'_i) $$

$$ [\text{ABSUNTYPABLE}] \quad \frac{\Gamma \vdash_R \lambda x : A. \kappa : t \Rightarrow (\lambda x:\{\}.\text{empty}(\kappa), \{\})}{\Gamma \vdash_R \lambda x : A. \kappa : t \Rightarrow (\lambda x:\{\}.\text{empty}(\kappa), \{\})} $$
$$ [\text{UNDEFINEDVAR}] \quad \overline{\Gamma \vdash_R a : t \Rightarrow (a, \{\})} $$

$$ [\text{BINDARGSKIP}] \quad \frac{\Gamma \vdash A = \{\} \qquad \Gamma \vdash_R \kappa : t \Rightarrow (\kappa', \Gamma)}{\Gamma \vdash_R \text{bind } x:A = a \text{ in } \kappa : t \Rightarrow (\text{bind } x:\{\} = \text{empty}(a) \text{ in } \kappa', \Gamma)} $$

$$ [\text{BINDARGUNTYP}] \quad \frac{\Gamma \vdash_R a : \bigvee (\Gamma \vdash A) \Rightarrow (a', \{\}) \qquad \Gamma \vdash_R \kappa : t \Rightarrow (\kappa', \Gamma)}{\Gamma \vdash_R \text{bind } x:A = a \text{ in } \kappa : t \Rightarrow (\text{bind } x:\{\} = a' \text{ in } \kappa', \Gamma)} $$

$$ [\text{BINDARGREFEnv}] \quad \frac{\Gamma \vdash_R a : \bigvee (\Gamma \vdash A) \Rightarrow (a', \Gamma) \qquad \kappa' = \text{restrict}_\Gamma(\kappa) \qquad A' = \text{restrict}_\Gamma(A)}{\Gamma \vdash_R \text{bind } x:A = a \text{ in } \kappa : t \Rightarrow (\text{bind } x:A' = a' \text{ in } \kappa', \Gamma \cup \{\Gamma\})} \quad \Gamma \neq \{\Gamma\} $$

$$ [\text{BINDARGREFAnns}] \quad \frac{\Gamma \vdash_R a : \bigvee (\Gamma \vdash A) \Rightarrow (a', \{\Gamma\}) \qquad \Gamma \vdash_R \text{bind } x:A = a' \text{ in } \kappa : t \Rightarrow (\kappa', \Gamma)}{\Gamma \vdash_R \text{bind } x:A = a \text{ in } \kappa : t \Rightarrow (\kappa', \Gamma)} \quad a' \neq a $$

$$ [\text{BIND}] \quad \frac{\Gamma \vdash_R a : s \quad \{s_i\}_{i \in I} = \text{partition}(\{s \wedge u \mid u \in (\Gamma \vdash A)\}) \quad (\forall i \in I)}{\Gamma, (x : s_i) \vdash_R \kappa : t \Rightarrow (\kappa_i, \Gamma_i) \qquad \Gamma_i' = \text{propagate}_{x,a,s_i}(\Gamma_i) \qquad (A_i, \Gamma_i'') = \text{extract}_x(\Gamma_i')} \quad \Gamma \vdash_R \text{bind } x:A = a \text{ in } \kappa : t \Rightarrow (\text{bind } x: \bigcup_{i \in I} A_i = a' \text{ in merge}_\kappa(\{\kappa_i\}_{i \in I}), \bigcup_{i \in I} \Gamma_i'') $$

$$ [\text{VAR}] \quad \overline{\Gamma \vdash_R x : t \Rightarrow (x, \{\Gamma[x := \Delta t]\})} $$

The rules above are listed in priority order, meaning that a rule applies only if no other previous rule does.

In Section 5 we said that we omitted the rules for empty types. A first example of such rules is the rule [PROJEMPTY] that states that when $x$ is of type $\emptyset$ (i.e., the variable is bound to an expression that diverges), then the atom $\pi_i x$ is well-typed (since by subsumption it has type $t \times 1$ and $1 \times t$, that can be used for each specific $\pi_i$).

The rules [PROJ$_i$] are as in Section 5 with the only difference that instead of $\approx$ they use the relation $\overset{\text{DNE}}{\cong}$ we defined in Appendix B.1. The reason is that we want a deterministic algorithm and therefore these rules simply apply to the types on the left-hand side the normalization algorithm by Frisch et al. [2008] yielding the type on the right-hand side.

The rule [PAIREMPTY] follows the same logic as [PROJEMPTY], where $\Gamma(x_1) \times \Gamma(x_2) \approx \emptyset$ is just a notational trick to state that either $\Gamma(x_1) \approx \emptyset$ or $\Gamma(x_2) \approx \emptyset$.

The rule [PAIR] states that for a pair to have a type $t$, it must inhabit the product part of $t$, that is $t \wedge (1 \times 1)$. The rule then performs the decomposition of this part in its disjunctive normal form.

The [CASEEMPTY] states that if in type-case expression the tested expression diverges, then the expression is well typed. The rule [CASE] was explained in Section 5.

The rules [APPLEEMPTY] and [APPREEMPTY] reflect the use of our left to right evaluation strategy: if $x_1$ diverges then the application is well typed provided $x_2$ is defined; if $x_2$ diverges then the application is well typed provided $x_1$ has a functional type and thus, implicitly, it already converged to a $\lambda$-abstraction.
The rule [APPR] is as the one presented and explained in Section 5 apart from two details. First, as for the other rules, instead of checking the equivalence $\cong$, we use $\simeq$ which transforms the type of the function into its disjunctive normal form. Second, even though this has no consequence on the conclusion of the rule, we stress that this transformation can make some negated arrow types appear. We omitted this detail in the main presentation because to see that this is possible one needs to examine the details of the definition of partition, that in the rule [ABS] is used to partition the domain of the function. If we have a function whose parameter is annotated with some functional type, say, $\text{Int} \to \text{Int}$ and this parameter was initially given type $1$, then partition will produce for these two types the set $\{(\text{Int} \to \text{Int}), \neg(\text{Int} \to \text{Int})\}$ which contains a negated arrow. The presence of negated arrows becomes important for the rules [ABS] and [ABSUNTYPABLE].

We explained the rule [ABS] in Section 5. However the rule presented there was a simplified version. Let us pinpoint the differences. As customary, rather than checking the equivalence $\cong$, we use $\simeq$ which transforms the checked type $t$ into its disjunctive normal form. Notice, however, that the rule applies only if the disjunctive normal form does not contain any negated arrow type. Indeed, for a given $\lambda$-abstraction there is no way to ensure that it will have a specific negated arrow type (this is possible in CDuce since $\lambda$-abstractions are explicitly annotated, but here in general we have no annotation in the source language to enforce it). So in case there are any negated arrow types, the type constraint $t$ must be considered not satisfiable and this case is handled by the rule [ABSUNTYPABLE]. The rule [ABS] above uses the operator $t \circ_1 s_i$ given in Appendix A.4 whereas the rule in Section 5 used $t \circ s_i$. The former is defined as $t \circ s_i$ but it returns $1$ when $s_i \notin \text{dom}(t)$. This forces the system to check whether it is possible to type the function under the hypothesis that $x: s_i$ even if $s_i$ is not in the current domain that was deduced for the function. The reason is that we are determining this domain: at the beginning all we know about a function is that, if it is well typed, then it will be of type $0 \to 1$. Clearly we do not want to test for the function only the $0$ domain, but also the domains suggested by the current annotation for $x$ (initially $1$). The annotation $A'$ produced will retain only those for which the test will have succeeded. Still in the rule [ABS], the additional checks $(\Gamma \vdash A) \neq \{\}$ and $\bigvee_{j \in J} s_j \leq \bigvee (\Gamma \vdash A)$ absent in the version of Section 5 are there to ensure that the algorithm will only refine the initial annotations and not enlarge them (this is needed for the—conjectured—termination of the algorithm). The last condition added, namely, $\bigvee_{j \in J} s_j \leq \bigvee \{s' \mid (\Gamma \vdash s') \in A'\}$, is a necessary (but far from sufficient) condition to ensure that the annotated $\lambda$-abstraction produced by the pass has type $t$: if all the types in the produced annotation $A'$ (independently from their guards) do not cover $\text{dom}(t)$ (i.e., $\bigvee_{j \in J} s_j$) then there is no way by which a lambda abstraction of the form $\lambda x:A' \kappa$ could have type $t$.

If any of the conditions added in the rule [ABS] fail, or if the checked type $t$ has any negated arrow type, then there is no way that $\lambda x:A.\kappa$ can be given type $t$ and the pass fails. This is done by the rule [ABSUNTYPABLE]. Notice that for this rule the returned expression is the initial one with all annotations emptied. This is necessary because even if the typing of this term under $\Gamma$ failed, it may succeed under different hypotheses and thus the merging of this atom with the successful one should not perturb the latter.

The rule [UNDEFVAR] is the default case for the typing of atoms. It means that if none of the previous rules can be applied (recall that the rules are given in priority order), then the algorithm must return a failure. We called it [UNDEFVAR] since this happens when one of the variables of $a$ is not in $\text{dom}(\Gamma)$.

The rule [UNDEFVAR] concludes the rules for algorithmic atoms. The rules that follow are for algorithmic expressions, that is, bind-expressions and variables. We already explained in detail the rules for bind-expressions in Section 5 where we gave the complete rules with just two simplifications. First, in the rule [BINDARGSKIP] we omitted to apply the empty function to $a$. As in the case for [ABSUNTYPABLE] this must be done in order to avoid to perturb the merge with other
successful annotations. Second in the rule [BINDARGREFENV], when the typing of the argument *a* needs more refinements, it is not sufficient to forward these refinements to the whole pass, since these refinements may impact the annotations already present in the MSC-form, that are thus refined by applying the *restrict* function.

Finally, the very last rule, [VAR] states that in order to ensure that a variable has type *t* the obvious solution is to refine Γ(*x*) with *t*. Simply notice that if Γ(*x*) is a subtype of *t*, then the rule returns {Γ}, that is success.