TL;DR
Bidirectional typing combines type checking and synthesis to support undecidable inference, reduce annotation burden, and improve error localization, offering a flexible approach for type systems.
Contribution
This paper surveys the development and principles of bidirectional typing, highlighting its advantages and guiding future research directions.
Findings
Supports features with undecidable inference
Reduces annotation burden in typed languages
Improves error localization
Abstract
Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program. Using checking enables bidirectional typing to support features for which inference is undecidable; using synthesis enables bidirectional typing to avoid the large annotation burden of explicitly typed languages. In addition, bidirectional typing improves error locality. We highlight the design principles that underlie bidirectional type systems, survey the development of bidirectional typing from the prehistoric period before Pierce and Turner's local type inference to the present day, and provide guidance for future investigations.
| checks against | synthesizes | |||||||
| Coquand (1996) | ||||||||
|---|---|---|---|---|---|---|---|---|
| Pierce and Turner (2000) | ||||||||
| Xi and Pfenning (1999); Davies and Pfenning (2000); | ||||||||
| Dunfield and Pfenning (2004); | ||||||||
| Polikarpova et al. (2016); Çiçek et al. (2019) | ||||||||
| Chlipala et al. (2005); Pottier and Régis-Gianas (2006); | ||||||||
| Dunfield (2009) | ||||||||
| Peyton Jones et al. (2007) | ||||||||
| Davies (2005) | ||||||||
|
||||||||
| McBride (2016) | ||||||||
| Lindley et al. (2017) |
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
\mathlig
|-⊢ \mathlig-|⊣ \mathlig->→ \mathlig<<⟨ \mathlig>>⟩ \mathlig<= \mathlig=> \mathlig=>>
Bidirectional Typing
Jana Dunfield
Queen’s UniversitySchool of Computing, Goodwin Hall 557Kingston, ONK7L 3N6Canada
and
Neel Krishnaswami
University of CambridgeComputer Laboratory, William Gates BuildingCambridgeCB3 0FDUnited Kingdom
Abstract.
Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program. Using checking enables bidirectional typing to support features for which inference is undecidable; using synthesis enables bidirectional typing to avoid the large annotation burden of explicitly typed languages. In addition, bidirectional typing improves error locality. We highlight the design principles that underlie bidirectional type systems, survey the development of bidirectional typing from the prehistoric period before Pierce and Turner’s local type inference to the present day, and provide guidance for future investigations.
††copyright: none
1. Introduction
Type systems serve many purposes. They allow programming languages to reject nonsensical programs. They allow programmers to express their intent, and to use a type checker to verify that their programs are consistent with that intent. Type systems can also be used to automatically insert implicit operations, and even to guide program synthesis.
Automated deduction and logic programming give us a useful lens through which to view type systems: modes (Warren, 1977). When we implement a typing judgment, say , is each of the meta-variables (, , ) an input, or an output? If the typing context , the term and the type are inputs, we are implementing type checking. If the type is an output, we are implementing type inference. (If only is input, we are implementing typing inference (Jim, 1995; Wells, 2002); if is output, we are implementing program synthesis.) The status of each meta-variable—input or output—is its mode.
As a general rule, outputs make life more difficult. In complexity theory, it is often relatively easy to check that a given solution is valid, but finding (synthesizing) a solution may be complex or even undecidable. This general rule holds for type systems: synthesizing types may be convenient for the programmer, but computationally intractable.
To go beyond the specific feature set of traditional Damas–Milner typing, it might seem necessary to abandon synthesis111We choose to say synthesis instead of inference. This is less consistent with one established usage, “type inference”, but more consistent with another, “program synthesis”.. Instead, however, we can combine synthesis with checking. In this approach, bidirectional typing, language designers are not forced to choose between a rich set of typing features and a reasonable volume of type annotations: implementations of bidirectional type systems alternate between treating the type as input, and treating the type as output.
The practice of bidirectional typing has, at times, exceeded its foundations: the first commonly cited paper on bidirectional typing appeared in 1997 but mentioned that the idea was known as “folklore” (see Section 10). Over the next few years, several bidirectional systems appeared, but the principles used to design them were not always made clear. Some work did present underlying design principles—but within the setting of some particular type system with other features of interest, rather than focusing on bidirectional typing as such. For example, Dunfield and Pfenning (2004) gave a broadly applicable design recipe for bidirectional typing, but their focus was on an idea—typing rules that decompose evaluation contexts—that has been applied more narrowly.
Our survey has two main goals:
- (1)
to collect and clearly explain the design principles of bidirectional typing, to the extent they have been discovered; and 2. (2)
to provide an organized summary of past research related to bidirectional typing.
We begin by describing a tiny bidirectional type system (Section 2). Section 3 presents some design criteria for bidirectional type systems. Section 4 describes a modified version of the recipe of Dunfield and Pfenning (2004), and relates it to our design criteria. Section 5 discusses work on combining (implicit) polymorphism with bidirectional typing, and Section 6 surveys other variations on bidirectional typing. Sections 7–8 give an account of connections between bidirectional typing and topics such as proof theory, focusing and polarity, and call-by-push-value. Section 9 cites other work that uses bidirectional typing. We conclude with historical notes (Section 10) and a summary of notation (Section 11).
2. Bidirectional Simply Typed Lambda Calculus
To develop our first bidirectional type system, we start with a (non-bidirectional) simply typed lambda calculus (STLC). This STLC is not the smallest possible calculus: we include a term () of type , to elucidate the process of bidirectionalization. We also include a gratuitous “type equality” rule.
Our non-bidirectional STLC (Figure 1, left side) has six rules deriving the judgment : a variable rule, a type equality rule, a rule for type annotations, an introduction rule for , an introduction rule for and an elimination rule for .
These rules are standard except for the type equality rule TypeEq, which says that if has type and equals , then has type . If this rule does not disturb you, you may skip to the next paragraph. If we had polymorphism, we could motivate this rule by arguing that should be considered equal to . Our language of types, however, has only and and so admits no nontrivial equalities. The role of TypeEq is retrospective: it is the type assignment version of a necessary bidirectional rule, allowing us to tell a more uniform story of making type assignment bidirectional. For now, we only note that the type equality rule is sound: for example, if we have derived then , which was already derived.
Given these six STLC typing rules, we produce each bidirectional rule in turn (treating the type equality rule last). Some of our design choices will become clear only in the light of the “recipe” in Section 4, but the recipe would not be clear without seeing a bidirectional type system first.
- (1)
The variable rule Var has no typing premise, so our only decision is whether the conclusion should synthesize or check against . The information that has type is in , so we synthesize . A checking rule would require that the type be known from the enclosing term, a very strong restriction: even would require a type annotation. 2. (2)
From the annotation rule Anno we produce Anno\mathrel{{{\color[rgb]{0.45,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.45,0.0,0.0}{\Rightarrow}}}}, which synthesizes its conclusion: we have the type in , so we do not need to be given as input. In the premise, we check against ; synthesizing would prevent the rule from typing a non-synthesizing , which would defeat the purpose of the annotation. 3. (3)
Unit introduction I checks. At this point in the paper, we prioritize internal consistency: checking () is consistent with the introduction rule for (discussed next), and with the introduction rule for products. 4. (4)
Arrow introduction I checks. This decision is better motivated: to synthesize for we would have to synthesize a type for the body . That raises two issues. First, by requiring that the body synthesize, we would need a second rule to handle s whose body checks but does not synthesize. Second, if we are synthesizing that means we don’t know yet, which prevents us from building the context . (Placeholder mechanisms, which allow building and “solving” later, are described in Section 5.)
Since the conclusion is checking, we know , so we might as well check in the premise. 5. (5)
For arrow elimination E, the principal judgment is the premise , because that premise contains the connective being eliminated. We make that judgment synthesize; this choice is the one suggested by our “recipe”, and happens to work nicely: If synthesizes , we have and can check the argument (so the rule will work even when cannot synthesize), and we have so we can synthesize in the conclusion. (It is possible to have the premise typing be a checking judgment. In that case, the argument must synthesize, because we need to know what is to check against . Similarly, the conclusion must be checking, because we need to know ; see Section 6.5.1.) 6. (6)
Finally, we come to the type equality rule TypeEq. Where the type assignment premise and conclusion are identical (since is exactly equal to ), the duplication of these identical premises enables us to give them different directions in the bidirectional system. Either (1) the conclusion should synthesize (and the premise check), or (2) the conclusion should check (and the premise synthesize).
Option (1) cannot be implemented: If the conclusion synthesizes , that means is not an input; we don’t know , which means we also don’t know for checking.
Option (2) works: If we want to check against a known in the conclusion, and synthesizes a type , we verify that .
Neither Sub\mathrel{{{\color[rgb]{0.0,0.0,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.65}\Leftarrow}}} nor Anno\mathrel{{{\color[rgb]{0.45,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.45,0.0,0.0}{\Rightarrow}}}} is tied to an operational feature (as, for instance, E\mathrel{{{\color[rgb]{0.45,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.45,0.0,0.0}{\Rightarrow}}}} is tied to functions); Anno\mathrel{{{\color[rgb]{0.45,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.45,0.0,0.0}{\Rightarrow}}}} is tied to a syntactic form, but (supposing a type erasure semantics) not to any operational feature. Moreover, Sub\mathrel{{{\color[rgb]{0.0,0.0,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.65}\Leftarrow}}} and Anno\mathrel{{{\color[rgb]{0.45,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.45,0.0,0.0}{\Rightarrow}}}} have a certain symmetry: Sub\mathrel{{{\color[rgb]{0.0,0.0,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.65}\Leftarrow}}} moves from a checking conclusion to a synthesizing premise, while Anno\mathrel{{{\color[rgb]{0.45,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.45,0.0,0.0}{\Rightarrow}}}} moves from a synthesizing conclusion to a checking premise.
3. Elements of Bidirectional Typing
From a rules-crafting perspective, bidirectionality adds a degree of design freedom to every judgment (premises and conclusion) in a rule: should a particular premise or conclusion synthesize a type, or check against a known type? Covering all possibilities with rules that have every combination of synthesis and checking judgments would lead to an excessive number of rules. For example, the following eight rules are superficially valid bidirectional versions of the standard -elimination rule.
[TABLE]
What criteria should guide the designer in crafting a manageable set of rules with good practical (and theoretical) properties?
3.1. First Criterion: Mode-correctness
The first criterion comes from logic programming (Warren, 1977). We want to avoid having to guess types: in an ideal world, whenever we synthesize a type, the type should come from known information—rather than, say, enumerating all possible types. A rule is mode-correct if there is a strategy for recursively deriving the premises such that two conditions hold:
- (1)
The premises are mode-correct: for each premise, every input meta-variable is known (from the inputs to the rule’s conclusion and the outputs of earlier premises). 2. (2)
The conclusion is mode-correct: if all premises have been derived, the outputs of the conclusion are known.
Our last rule, in which every judgment is checking (), is not mode-correct: In the first premise , the context and term are known from the inputs and in the conclusion . However, the type cannot be constructed, because is not known. For the same reason, the second premise is not mode-correct. (The conclusion is mode-correct because all the meta-variables are inputs.)
Only four of the above eight rules are mode-correct:
[TABLE]
The mode-correctness of the fourth rule seems questionable: if we insist on recursively deriving the first premise before the second premise , it is not mode-correct, but if we swap the premises and view the rule as
[TABLE]
it is mode-correct: the subterm synthesizes , and is an input in the conclusion, so is known and can be checked against it.
This seems disturbing: the order of premises should not affect the meaning of the rule, in the sense that a rule determines a set of possible derivations. But mode-correctness is not about meaning in that sense; rather, it is about a particular strategy for applying the rule. For any one strategy, we can say whether the strategy is mode-correct; then we can say that a rule is mode-correct if there exists some strategy that is mode-correct. The set of strategies is the set of permutations of the premises. So the rule above has two strategies, one for each of the two permutations of its premises; since one of the strategies is mode-correct, the rule is mode-correct.
A bidirectional type system that is not mode-correct cannot be directly implemented, defeating the goal that the derivability of a typing judgment should be decidable. Thus, mode-correctness is necessary. However, mode-correctness alone does not always lead to a practical algorithm: if more than one rule is potentially applicable, a direct implementation requires backtracking. When the inputs (the context, the term, and—if in the checking direction—the type) match the conclusion of only one rule, the system is syntax-directed: we can “read off” an implementation from the rules.
3.2. Second Criterion: Completeness (Annotatability)
The empty set of rules satisfies the first criterion: every rule is mode-correct, because there are no rules.
Our second criterion rejects the empty system. A bidirectional system is complete with respect to a type assignment system if every use of a rule in the type assignment system can be “matched” by some rule in the bidirectional system. This matching is approximate, because applying the bidirectional rule might require that we change the term—generally, by adding type annotations (sometimes called ascriptions).
For example, forgetting to include an -elimination rule in a bidirectional type system would make the system incomplete: it would reject all function applications. In general, completeness is easy to achieve, provided we begin with a type assignment system and “bidirectionalize” each rule.
Because the move from a type assignment derivation to a bidirectional derivation may require adding annotations, the related theorem is sometimes called annotatability instead of completeness. A separate criterion considers the quantity and quality of the required annotations (Section 3.4).
Requiring that every type connective have at least one introduction rule and at least one elimination rule would be too strict: the empty type should not have an introduction rule, and the top type and the unit type do not require elimination rules. (We might choose to include an elimination rule for , but our criteria for bidirectional systems should not force this choice.)
3.3. Third Criterion: Size
Our third criterion refers to the number of typing rules. This is not always a reliable measure; by playing games with notation, one can inflate or deflate the number of typing rules. But the measure can be used effectively when comparing two systems in an inclusion relationship: a system of two rules R1 and R2 is clearly smaller than a system that has R1, R2, and a third rule R3. Smaller systems tend to be easier to work with: for example, in a meta-theoretic proof that considers cases of the rule concluding a given derivation, each new rule leads to an additional proof case.
3.4. Fourth Criterion: Annotation Character
A bidirectional system that required an annotation on every subterm would satisfy completeness. To rule out such a system, we need another criterion. We call it annotation character, an umbrella term for attributes that are sometimes in conflict:
- (i)
Annotations should be lightweight: they should constitute a small portion of the program text. 2. (ii)
Annotations should be predictable: programmers should be able to easily determine whether a subterm needs an annotation. That is, there should be a clear annotation discipline. 3. (iii)
Annotations should be stable: a small change to a program should have a small effect on annotation requirements. 4. (iv)
Annotations should be legible: the form of annotation should be easy to understand.
Attribute (i) is the easiest to measure, but that doesn’t make it the most important.
Attribute (ii) is harder to measure, because it depends on the definition of “easily” (alternatively, on the definition of “clear”). In the absence of empirical studies comparing bidirectional type systems with different annotation disciplines, we can form some hypotheses:
- (1)
A discipline that needs only local information is preferable to one that needs global information. That is, we want to know whether a subterm needs annotation from the “neighbourhood” of that subterm, not by looking at the whole program. The Pfenning recipe (Section 4) leads to an annotation discipline in which the syntactic forms of the subterm (e.g. that it is a pair) and the subterm’s immediate context (its parent in the syntax tree) suffice to determine whether the subterm needs an annotation. (The subterm alone is not enough: a subterm that cannot synthesize does not require an annotation if it is being checked, and whether the subterm is checked depends on its position in the program.)
In an annotation discipline that needs only local information, a change to one part of a program cannot affect the need for annotations in distant parts of the program. Hence, such a discipline is stable (attribute (iii)). 2. (2)
A discipline that requires all non-obvious type annotations, and no obvious type annotations, is preferable. Unfortunately, it is not easy to agree on which type annotations are obvious. 3. (3)
A discipline that needs obvious type annotations in certain situations is acceptable, if those situations are rare. For example, we might tolerate annotations on every while loop in SML because SML programmers rarely use while.
These hypotheses can be found, in a different form, in earlier work. The term local type inference (Pierce and Turner, 2000) implies that bidirectional typing should focus on (or even be restricted to) local information, suggesting that annotation disciplines should not need global information. Hypotheses (2) and (3) correspond to this explanation, from the same paper:
The job of a partial type inference algorithm should be to eliminate especially those type annotations that are both common and silly—i.e., those that can be neither justified on the basis of their value as checked documentation nor ignored because they are rare. (Pierce and Turner, 2000, §1.1; emphasis in original)
4. A Bidirectional Recipe
Fortunately, we have a methodical approach that produces bidirectional systems that satisfy many of the above criteria.
We call this approach222Our presentation of the recipe is intended as a more detailed explanation of the original, with one exception. The exception is that, instead of (implicitly) advocating that a case expression (sum elimination) have a single rule with a checking conclusion, our version of the recipe allows for two rules: one checking, one synthesizing. the Pfenning recipe (Dunfield and Pfenning, 2004). It yields a set of bidirectional typing rules that is small (our second criterion) and whose annotation discipline is moderately lightweight and highly predictable (attributes of our fourth criterion). Some disadvantages of the recipe—particularly in terms of a lightweight annotation discipline—can be mitigated, in exchange for a larger set of rules. Thus, the foremost virtue of the recipe is that it gives a starting point for a practical system: it tells you what the ground floor of the building (type system) should look like, allowing a taller building if desired. Even if the recipe is not followed completely, some of its steps are useful in designing bidirectional systems; we use this opportunity to explain those steps. Another virtue of the recipe is that it guarantees a subformula property, which can be of practical as well as theoretical interest; see Section 7.1.
Nonetheless, this recipe is not the only way to design a bidirectional type system. This fact is demonstrated by the wide variety of systems that do not exactly follow the recipe, and by the existence of systems that diverge radically from it (Section 6.5).
4.1. Introduction and Elimination Rules
This part of the recipe pertains to each rule that is an introduction rule (introducing a type connective that occurs in the conclusion) or an elimination rule (eliminating a type connective that occurs in a premise).
Step 1: Find the principal judgment
The principal connective of an introduction (resp. elimination) rule is the connective that is being introduced (resp. eliminated). The principal judgment of a rule is the judgment containing the principal connective; in an introduction rule, the principal judgment is usually333In an introduction rule in which the introduced connective is only available in a lexically scoped subterm, the principal connective is added to the context in a premise. In such a rule, the premise with the extended context—not the conclusion—is the principal judgment. An example is a rule typing a product introduction for a “let-pair” construct: the (highlighted) third premise is the principal judgment, because it contains the introduced connective .
\displaystyle\displaystyle{\hbox{\hskip 101.93796pt\vbox{\hbox{\hskip-101.93796pt\hbox{\hbox{\displaystyle\displaystyle{}\Gamma|-e_{1}:A_{1}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\Gamma|-e_{2}:A_{2}}\hskip 20.00003pt\hbox{\hbox{\displaystyle\displaystyle\text{\hbox{\pagecolor{yellow!40}}}\mathstrut}}}}}\vbox{}}}\over\hbox{\hskip 52.86029pt\vbox{\vbox{}\hbox{\hskip-52.86028pt\hbox{\hbox{\displaystyle\displaystyle\Gamma|-\text{\text{{let}}},x=\langle e_{1},e_{2}\rangle;\text{\text{{in}}},e:B\mathstrut\hskip 1.1pt}}}}}}
the conclusion, and in an elimination rule, the principal judgment is (as far as we know) always the first premise.
Step 2: Bidirectionalize the principal judgment
This is the magic ingredient! If the rule is an introduction rule, make the principal judgment checking. If the rule is an elimination rule, make the principal judgment synthesizing.
Step 3: Bidirectionalize the other judgments
The direction of the principal judgment provides guidance for the other directions. The first question is, in what order should we bidirectionalize the other judgments? If the principal judgment is the conclusion (often true for introduction rules), the only judgments left are the premises, but if the principal judgment is a premise (probably the first premise), we have a choice. The better choice seems to be to bidirectionalize the premises, then the conclusion: this maximizes the chance of having enough information to synthesize the type of the conclusion.
The second question is, which directions should we choose? Here we are guided by our criteria of annotatability and annotation character: the bidirectional system should be complete with respect to “ground truth” (roughly, the given type assignment system) without needing too many annotations.
Therefore, we should utilize known information: If we already know the type of a judgment—the judgment should be checking. Thus, if the conclusion checks against a type and a premise also has type , the premise should be checking. Similarly, if an earlier premise synthesizes then a later premise having type should be checking. Choosing to synthesize would ignore known information, restricting the system’s power for no reason.
Step 3, continued
Unfortunately, what should count as “ground truth” is not always clear. It may not be exactly the set of type assignment rules. In our experience, most type assignment rules can be taken as ground truth and transformed by the recipe with satisfactory results, but certain type assignment rules must be viewed more critically. Consider a standard sum-elimination rule, on a pattern-matching term where is bound in and is bound in :
[TABLE]
If we erase the terms from this rule and rewrite as , we get a logical or-elimination rule:
[TABLE]
This rule is an instance of a fundamental logical principle: reasoning by cases. In a mathematical proof, reasoning by cases works the same regardless of the goal we want to prove: whether we want to conclude “formula is true” or “kind is well-formed” or “real number is negative” or “machine halts”, our proof can consider the two cases ( is true; is true) of the disjunctive formula . So the ground principle from which Elim is instantiated allows for a conclusion that has any form:
[TABLE]
Instantiating to “formula is true” results in Elim, while instantiating to “machine halts” would result in
[TABLE]
If we consider Elim-general to be the basis of Elim, we see that Elim-general should give rise to two bidirectional rules, because a bidirectional system has two judgment forms.
[TABLE]
The original recipe (Dunfield and Pfenning, 2004) resulted in only one typing rule for case, the checking rule; if you can only have one rule, the checking rule is more general and nicely matches the checking premise of Intro. Note that whether we have one rule or two, we are still following Steps 1 and 2 of the recipe: in both versions of the rule, the principal judgment synthesizes. The complication is that making the principal judgment synthesize does not determine the directions of the conclusion and the other premises.
Similar considerations arise in typing a let-expression, with one additional wrinkle: a let-expression is not an elimination form. Thus, we seem to have no guidance at all, beyond mode-correctness. Whether the conclusion checks or synthesizes, we do not yet know the type of the let-bound expression, so the first premise must synthesize (similar to a case expression):
[TABLE]
Now we have the same choice as in case elimination: if a let-expression represents a general reasoning principle, then we may want two rules, one where the second premise and conclusion are checking, and one where they synthesize. If we prioritize a small number of rules, the checking rule is more general than the synthesis rule alone. (It is actually possible to design a system where is checked; we explore that territory in Section 6.5.)
Dunfield and Pfenning (2004) claimed that annotations were needed only on redexes, but that claim was false. The claim holds for elimination forms that do not bind variables, but fails with elimination forms that do bind variables, like case expressions. If we, instead, have both rules for case expressions, using a variable-binding elimination to derive the principal judgment of a variable-binding elimination does not incur an annotation (so, unlike in the original recipe, can be typed if all arms of the inner case can synthesize). However, some combinations of binding and non-binding elimination do incur annotations despite having no redexes.444Admittedly, the truth of the claim depends on the meaning of “redex”; if we include various commuting conversions in our notion of reduction, the claim becomes accurate.
We discuss the details in Section 4.5.4.
4.2. Annotation
Assume we have, in the given type assignment system, the following annotation rule. (If we had no concern for ease of implementation, we might not need such a rule.)
[TABLE]
This is not an introduction or elimination rule, so it has no principal connective and thus no principal judgment. However, the conclusion feels closer to being the principal judgment, because—while the type is not tied to any particular connective—the type must match the type appearing in the term . In contrast, the premise imposes no constraints at all.
Thus, we will start by bidirectionalizing the conclusion. Again, the rule is neither an introduction nor an elimination so we cannot pick a direction based on that. Instead, we follow the principle in Step 3 (above): we should try to use all available knowledge. We know the type because it appears in the term , so synthesizing in the conclusion utilizes this knowledge.
Now we turn to the premise, . Since is known we should utilize it by checking against , resulting in the rule
[TABLE]
It doesn’t really matter whether we start with the conclusion or the premise. If we start with the premise, we notice that is known from and make the premise checking; then we notice that is known in the conclusion.
4.3. Variables
A typing rule for variables is neither an introduction nor elimination rule. Instead, it corresponds to a fundamental principle of deduction: the use of an assumption. Instead of interpreting the assumption to mean that has (is assigned) type , we interpret as : we assume that synthesizes , and so the variable rule is synthesizing:
[TABLE]
It might be more clear for the form of assumptions in to be rather than , making clear that this rule is simply the use of an assumption, but the form is standard.
Since is checked, its argument type is known and can be added to . Assumptions arise in a reversed bidirectional system (Section 6.5).
4.4. Change of Direction (Subsumption)
To see why this part of the recipe is needed, consider the following type assignment derivation.
[TABLE]
Our bidirectional Var rule can synthesize a type for , but cannot derive a checking judgment. So we cannot synthesize a type for applied to , even though both their types are available in the typing context:
[TABLE]
We know, from the type of , that needs to have type . The var rule can tell us that also synthesizes that type. So we need a rule that verifies that a fact ( synthesizes type ) is consistent with a requirement ( needs to check against type ). One version of that rule would be
[TABLE]
However, the recipe prefers an equivalent rule:
[TABLE]
Since is only equality, rule changedir-1 has exactly the same power as changedir-0. Rules changedir-0 and changedir-1 can be implemented in exactly the same way, but the structure of changedir-1 is closer to that implementation: first, make a recursive call to synthesize ; second, check that is equal to the given type . (In logic programming terminology, in changedir-1 the premise has output freeness: the output is unconstrained, with the constraint imposed later by . In changedir-0, the output is constrained to be exactly the type from the conclusion.)
The more significant advantage of changedir-1 is that it can be easily extended to support subtyping. To turn changedir-1 into a subsumption rule, we only have to replace “” with a subtyping relation “\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}”:
[TABLE]
(In a sense, changedir-1 is already a subsumption rule: equality is reflexive and transitive, so it is a sensible—if extremely limited—subtyping relation. If we choose equality as the definition of \mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}, the rule Sub is exactly the rule changedir-1.)
Since is an input, and is an output of the first premise, both and are known: the subtyping judgment can be implemented with both types as input, with no need to “guess” the subtype or supertype.
Subtyping can lead to concerns not addressed solely by the presence of Sub; we discuss these concerns in Section 4.6.
The rule Sub is not syntax-directed: its subject may be any form of expression. Because its premise is synthesizing, however, we have some guidance about when to apply it: when there is a rule whose conclusion can synthesize a type for that form of expression. In some bidirectional type systems, such as Davies and Pfenning (2000), no expression form has a rule with a synthesizing conclusion and a rule with a checked conclusion. In such systems, we can classify the expression forms themselves as checked or synthesizing, and use Sub exactly when checking a synthesizing form. If we have, say, two rules for case expressions, the situation is more complex. It is generally best to apply Sub as late as possible (that is, towards the leaves of the derivation), because that preserves the information provided by the type being checked against.
4.5. Assessing the Recipe
When we design a bidirectional system according to the recipe, which criteria are satisfied?
4.5.1. First criterion: Mode-correctness
All rules are mode-correct:
- •
The variable, annotation and subsumption rules are “pre-cooked” and it is straightforward to verify they are mode-correct.
- •
In the introduction and elimination rules, the judgment directions are chosen to be mode-correct.
4.5.2. Second criterion: Size
For each type assignment rule, the recipe produces exactly one rule. Producing less than one rule is unacceptable, because it would be incomplete with respect to the type assignment system.
If the original type assignment system did not have a subsumption rule, the recipe adds one, but this is unavoidable (see the example in Section 4.4). (An alternative would be to duplicate rules and vary the direction of their premises, but for most type systems, that would lead to more than one additional rule.)
Similarly, the annotation rule is needed to enable a term whose rule has a checking conclusion to be used in a synthesizing position. For example, we cannot type the term because the first premise of SynElim is synthesizing and the conclusion of ChkIntro is checking. We need the annotation rule to allow us to type the annotated term \big{(}(\lambda x.\,e):A->B\big{)}e^{\prime}.
Thus, it is not only impossible to remove a single rule, but there is no alternative approach that can, in general, produce a smaller set of rules. (We assume that the type assignment system is our “ground truth”: we cannot use a prolix type assignment system to argue that its bidirectionalization is too big.)
4.5.3. Third criterion: Annotatability
We write to mean that is a “more annotated” version of . For example, and . Annotatability says that, if (in the type assignment system), then (1) there exists such that , and (2) there exists such that . We prove this by induction on the type assignment derivation of , considering cases of the type assignment rule concluding that derivation.
Each type assignment rule has a single corresponding bidirectional rule. If the conclusion of that bidirectional rule is checking, proving part (1) is completely straightforward: Applying the induction hypothesis to the derivation of each premise (of the type assignment rule) yields a set of annotated subterms; combining these annotated subterms gives us our , which is typed by the bidirectional rule. This approach also works if we are proving part (2) and the conclusion of the bidirectional rule is synthesizing.
Going “into the wind”—proving part (1) with a synthesis rule, or part (2) with a checking rule—needs only a little more work:
- •
If the conclusion of the bidirectional rule corresponding to the type assignment rule is synthesis and we want to prove part (1), we can show part (2) as above to derive
[TABLE]
Now we want to find such that . Assuming subtyping is reflexive (a condition satisfied even by weak subtyping relations, including equality), we can derive A\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}A and use subsumption, giving . In this case, and are the same.
- •
If the conclusion of the bidirectional rule corresponding to the type assignment rule is checking and we want to prove part (2), we can show part (1):
[TABLE]
Now we want to find such that . We cannot reuse , because was derived using a checking rule; since the recipe produces only one corresponding bidirectional rule, we have no rule that can derive . We must add an annotation:
[TABLE]
The last step is to use our annotation rule, deriving .
4.5.4. Fourth criterion: Annotation character
Our notion of annotation character (Section 3.4) posits that annotations should be (i) lightweight, (ii)–(iii) predictable and stable (with a clear annotation discipline), and (iv) legible.
We also argued that a good annotation discipline should require only local information. On this point, the recipe does well: an annotation is required on a subterm if and only if an introduction form meets an elimination form.
To see why, let’s consider how the recipe treats introduction and elimination forms. Introduction rules type introduction forms, like ; elimination rules type elimination forms, like function application. Following the recipe, the principal judgment in an elimination form is synthesizing, so eliminating a variable never requires an annotation. For example, needs no annotation, because synthesizes. Nor does need an annotation, because synthesizes. Variable-binding elimination forms, like case, can also be nested without annotation: the type of the outer case is propagated to the inner case. For example, the type is propagated from the conclusion to the inner case:
[TABLE]
However, we need an annotation at the boundary between introduction and elimination: in , the introduction form meets the elimination form . Since the first premise of SynElim is synthesizing, and the conclusion of ChkIntro is checking, an annotation is needed around .
Similarly, in , the introduction form inj meets the elimination case, so needs an annotation.
In those two examples, we introduced and immediately eliminated the same type ( in the first example and in the second). An introduction that is not immediate also requires an annotation.
[TABLE]
Because the case expression appears as the function part of the application , it needs to synthesize a type (so we can derive the first premise of SynElim). But the case arms and , being introduction forms, do not synthesize. Therefore, we need a type annotation around the case, or—more verbosely—two annotations, one around each .555In the original recipe, the only option would be an annotation around the case. Since the original recipe had only one rule for case, which had a checking conclusion, annotating the individual arms would have no effect: typing could not “pass through” the case to notice the annotations. Note that if we push the application to into each arm, we get a term where eliminations immediately follow introductions (and, therefore, need annotations):
[TABLE]
4.6. Subtyping and Principal Types
In this section, we examine subtyping in a bidirectional system with intersection types. While intersection types are not the most common thing to find in a type system, they are closely related to parametric polymorphism: If a value has type , it has type and type ; if a value has type , it has the type for any type . An intersection type can be seen as a polymorphic type ranging over only two possibilities; the polymorphic type can be seen as an infinite intersection.
A typing rule is stationary (Leivant, 1986, p. 55) if the subject of the premise(s) is the same as the subject of the conclusion—in contrast to (perhaps more familiar) rules where each premise types a proper subterm of the subject of the conclusion. In the stationary rules we consider, the subject is any expression . Thus, these rules are not syntax-directed; if the conclusion of a rule types , the rule is potentially applicable at every step of type checking.
Our rule Sub is stationary, as are the following rules for intersection types and (implicit) parametric polymorphism : the premises type the same as the conclusion.
[TABLE]
With typing rules like these, it makes sense for subtyping to allow A_{1}\mathbin{\land}A_{2}\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}A_{1}: the presence of Elim1 means that every term having type also has type . Similarly, A_{1}\mathbin{\land}A_{2}\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}A_{2} because of Elim2. Observe that both subtyping and Gentzen’s rule notation are forms of implication : by treating types as propositions, A\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}B becomes ; a rule is read as . So we can translate Elim1:
[TABLE]
The rule Elim2 can be treated similarly.
However, the rule Intro cannot be translated in this way: the two premises mean that the rule cannot be read as “ implies ”, but only as “ and together imply ”. A subtyping judgment A\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}B can be read as the sequent , but it is a limited sequent calculus: in addition to allowing only one succedent (which is a common restriction in sequent calculi), subtyping allows only one antecedent . The subtyping rule we would like to construct would need two antecedents, and , which don’t fit:
[TABLE]
The subtyping relation induced by “translating” only the stationary typing rules is weaker (smaller) than we might desire: it yields shallow subtyping. For example, to derive the following through subsumption, we would need (A->(B_{1}\mathbin{\land}B_{2}))\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}(A->B_{2}) because the type of does not literally match . But the rules for are not stationary, letting us forget to add a subtyping rule for : in the subderivation typing , we need to have type but it has only the type .
[TABLE]
Note that if we -expand to , the term can be typed with only shallow subtyping:
[TABLE]
The technique of -expanding to simulate deep subtyping, e.g. for intersection and union types (Dunfield, 2014), is (as far as we know) due to Barendregt et al. (1983); they showed that putting a -expansion rule in a type system made subsumption admissible (see their Lemma 4.2).
Whether we choose a subtyping relation that is shallow or deep, we can “optimize” a type assignment system by dropping stationary rules that are encompassed by subsumption. For example, Elim1 and Elim2 are admissible by using Sub with the appropriate subtyping rules. This engineering optimization is not uniform: since Intro cannot be translated, we end up with a type system that has an introduction rule for , but buries the elimination rules inside subtyping.
Fortunately (if we dislike non-uniform optimizations), in the bidirectional version of intersection typing, the bidirectional versions of Elim1 and Elim2 are not admissible:
[TABLE]
These rules have a synthesizing conclusion, which means that Sub cannot simulate them.
It is worth noting, however, that these rules are mode-correct, but not syntax-directed. With stationary synthesis rules, a term can synthesize many possible types—in this example, can synthesize any of , , and . This is not inherently a bad thing—after all, the whole point of an intersection type discipline is to allow ascribing many types to the same term. However, managing this nondeterminism requires some care both in the design of the type system, and its implementation.
4.6.1. Principal synthesis
A type assignment system has principal types if there always exists a “best type”—a type that represents all possible types. In systems with subtyping, the best type is the smallest type, so the principal typing property says that if is well-typed, there is a principal type such that has type and A\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}B, for all types of :
Definition 0.
A type assignment system has principal types if, for all terms well-typed under , there exists a type such that and for all such that , we have A\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}B.
A type inference system has principal inference if it implements a type assignment system that has principal types (Definition 1) and always infers the principal type. We temporarily write for type inference, to ease the transition to principal synthesis (Definition 3). The definition says that if we can infer , then is principal.
Definition 0.
A type inference system has principal inference if, given , for all such that , we have A\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}B.
That is, every type that can be assigned to is a supertype of the inferred type . (In Damas–Hindley–Milner inference (Hindley, 1969; Damas and Milner, 1982), this property is stated for type schemes; an inferred type scheme for is principal when it can be instantiated to every (monomorphic) type of .)
We can adapt Definition 2 to bidirectional type systems by using checking, rather than type assignment, to define “all possible types”.
Definition 0.
A bidirectional type system has principal synthesis if, given , for all such that , we have A\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}B.
Principal synthesis is sometimes easy: if a bidirectional system has uniqueness of both synthesis and checking, that is, if and then (and respectively for checking), then A\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}B because . (In a system in which synthesis always produces the same type , and checking always works against only a single type for a given term, it had better be the case that !)
For many sophisticated type systems, principal synthesis either does not hold or requires some extra design work. In common formulations of intersection types, such as the one in Section 4.6, synthesis and checking are not unique. For example, if we synthesize , the point of the intersection type is to allow either the behaviour or , so it must be possible to derive both
[TABLE]
as well as . Saying that synthesis should only produce is not compatible with the recipe: If is a function, the rule Elim needs to synthesize a function type; we are not checking against a known type, so we cannot rely on subtyping (which has only a checking conclusion) to eliminate the intersection.
Non-uniqueness means that a straightforward implementation of the rules must do backtracking search, trying all three types , and , even when the choice is irrelevant. Some backtracking is difficult to avoid with intersection types, but naively trying all three choices in all circumstances is excessive.
To address this, the first author’s implementation of a bidirectional intersection and union type system split the synthesis judgment into two: one judgment that “maintains principality”, and one that “wants an ordinary type”. The “maintains principality” judgment lacked rules like Elim1 and Elim2; the “ordinary type” judgment included such rules. The choice of synthesis judgment depended on the rule. The premise of a let rule, synthesizing a type for the let-bound expression, used the “maintains principality” judgment to ensure that the variable typing added in the body of the let was principal. So, for example, if the let-bound expression was simply a variable of type , the typing in the body would also have , with no backtracking between choices of Elim1 and Elim2. However, the premise of Elim used the “wants an ordinary type” judgment, because we may need to apply rules like Elim1 to expose the connective. See Dunfield (2007, §6.7.1 on pp. 186–187).
Davies (2005, §2.10.2) includes a bidirectional typing (sort checking) system with a principal synthesis property. It appears that Davies asserts the property (page 41) without formally stating or proving it, but from our reading of the rules on page 42, it holds as follows: Principal synthesis is achieved through an auxiliary judgment that, when applying a function of type , gathers all the components such that the function argument checks against , and synthesizes the intersection of all such . (Davies (2005, §3.10) also discusses a principal sorts property in a non-bidirectional type inference setting, but this is less relevant to our survey.)
5. Polymorphism
Damas–Milner type inference (Damas and Milner, 1982) allows only prefix polymorphism: the quantifiers in a type must appear on the outside, allowing but not and . This restriction is called prefix or prenex polymorphism. In their terminology, types contain no quantifiers at all; only type schemes can have quantifiers (on the outside). Polymorphism can be introduced only on let expressions.
If programs must indicate both where and how to introduce and eliminate polymorphism, polymorphism is fully explicit. Adding fully explicit polymorphism to a bidirectional system is straightforward: since the term is an input, both the introduction and elimination rules can use the information in the term. However, fully explicit polymorphism is often considered unusable, mostly because of the explicit eliminations: it is burdensome to say how to instantiate every quantifier.
Explicit introduction of polymorphism can readily cope with less restrictive forms of polymorphism: higher-rank polymorphism, which allows quantifiers to be nested anywhere in a type (including to the left of arrows, as in the type mentioned above), and even impredicative polymorphism which allows quantifiers to be instantiated with polymorphic types.
Making eliminations implicit is not easy. Following the recipe, eliminations synthesize, so given we should derive , that is, . Unfortunately, the instantiation (we write , rather than , for monotypes—types containing no quantifiers) is decidedly not an input.
This instantiation problem has been tackled from several directions. The first widely known paper on bidirectional typing (Pierce and Turner, 2000) considered the problem in a setting with subtyping, and answered it by local constraint solving (hence the title Local Type Inference) around function applications. Subtyping leads to considering the upper and lower bounds of a type, rather than equations on types. Pierce and Turner restricted instantiation to prefix polymorphism, though their source language allowed impredicative polymorphism if the programmer explicitly instantiates the quantifier.
Their bidirectional rules are quite different from what our recipe might produce in their setting. They have three rules for -abstractions: S-Abs synthesizes the type of a with an explicit argument type, C-Abs-Inf checks a without an explicit argument type, and C-Abs checks a with an explicit argument type. They have two rules for applications with explicit quantifier instantiation: S-App synthesizes, with the same directionality as our -elimination rule, and C-App checks the application against a type by synthesizing a type for the function and checking that is a subtype of . (Here, we elide substituting the explicit instantiation type .) Applications with inferred instances also have two rules: S-App-InfSpec synthesizes, with a premise that forces the chosen instantiation to produce the best synthesized result type; C-App-UInfSpec checks, and lacks that premise because the needed result type of the application is known. Hosoya and Pierce (1999) discuss the annotation burden of local type inference for several example programs.
One can argue that all type systems have subtyping, where some systems have only trivial subtyping ( is a subtype of iff ). A more moderate perspective is that “most” type systems have subtyping: even in prefix polymorphism, types that are “more polymorphic” can be considered subtypes. By the substitution principle of Liskov and Wing (1994), should be a subtype of : any program context that expects an identity function on —of type —should be satisfied by a polymorphic identity function of type . (In many systems, including Damas–Milner, types cannot contain quantifiers—only type schemes can—but the perspective could be adapted to subtyping on type schemes, and is conceptually useful in any case.) In systems with higher-rank polymorphism, the perspective that polymorphism is a form of subtyping is salient: since quantifiers can appear to the left of arrows, we may want to pass a “more polymorphic” argument to a function that expects something less polymorphic.
5.1. “Complete and Easy” Polymorphism
In this subsection, we explain the key elements of our technique (Dunfield and Krishnaswami, 2013), discuss some typing rules, and describe its history in more detail.
5.1.1. Greedy instantiation
The key idea taken from Cardelli (1993) was that, when eliminating a polymorphic type, we can treat the first plausible solution as the solution. For example, if we are calling a function of type (assuming parametricity, such a function can only return one of its arguments) and pass as the first argument something of type , we instantiate to . This works perfectly well when the second argument has the same type, or when the second argument is of a subtype of (e.g. ), but fails when the second argument is of a larger type. If the first argument has type but the second argument has type , the second argument will fail to check against , since not all cats are tabbies.
In its original setting, this “greedy” method’s vulnerability to argument order was rather unfortunate. In a setting of predicative higher-rank polymorphism without other forms of subtyping, however, it can work nicely. The “tabby-first problem” cannot arise because the only way a type can become strictly smaller is by being strictly more polymorphic, and if the first argument is polymorphic we would be instantiating with a polymorphic type, which would violate predicativity.
5.1.2. Systems and judgments
The paper focused on two bidirectional type systems: a declarative system whose -elimination rule “guesses” types, and an algorithmic system which instead uses greedy instantiation.
Our declarative system followed a looser version of the Pfenning recipe: in addition to the rules produced by the recipe, the declarative system included synthesizing introduction rules for and . A subsumption rule, DeclSub, used a declarative subtyping relation whose “-left” rule—the rule concluding —guessed a monotype to use in the premise .
We also incorporated an application judgment, written
[TABLE]
meaning that under the declarative context , if a function of type is applied to an argument , the entire application will have result type . The rules for this judgment eliminate by substituting an unsolved type variable for .
5.1.3. Ordered typing contexts
Rather than passing along a “bag of constraints”, we can store the (solved and unsolved) type variables (written , , etc.) in an ordered context. Issues of circularity and scope still need care, but the way to handling them is clarified: if appears to the left of and we need to constrain them to be equal, we must solve to , not the other way around. Forcing this single order avoids backtracking.
In our algorithmic system, the three typing judgments—checking, synthesis and application—included an output context . For example, if the input context , meaning that is an unsolved existential variable and has type , checking against will solve :
[TABLE]
More generally, in a derivation of , the output context gains information: any solutions present in are also present in , but unsolved in may gain solutions in .
We made this idea of information gain precise by defining context extension: whenever a judgment is derivable, the output context is an extension of , written . As in the example, information about existential type variables may increase in ; also, new existential variables (unsolved or solved) may appear in . However, the “ordinary” program variable typings must not change.
5.1.4. Contexts as substitutions
In our paper, we allowed contexts to be used as substitutions: if contains , then . This usage pervaded the system. For instance, the subsumption rule applies , the output context of the first premise, to the inputs in the second premise:
[TABLE]
Such applications—found in all our rules with more than one premise—guarantee that whenever the input types in a judgment do not contain existential variables already solved in the input context, the output types do not contain existential variables that are solved in the output context. That is, all types are “solved” as much as possible. While this property made the rules a little more complicated, it seemed to make the system easier to work with.
5.1.5. Historical notes and other approaches
The first author combined the two key elements, greedy instantiation and ordered contexts, in a workshop paper (Dunfield, 2009); the idea of using ordered contexts is due to Brigitte Pientka. Unfortunately, key proofs in the paper were severely flawed. Despite these flaws, the second author liked the key ideas and wanted to use them in a type system with higher kinds and inverse types. We haven’t built that system yet, but the “preliminary” step of shoring up the workshop paper became its own paper (Dunfield and Krishnaswami, 2013). Gundry et al. (2010) offer a reformulation of Algorithm W that is based on information increase over ordered contexts.
We know of several languages that have used our approach or a variant of it: Discus666http://blog.discus-lang.org/2017/10/the-disciplined-disciple-compiler-v051.html, PureScript777http://www.purescript.org/, and Hackett888https://github.com/lexi-lambda/hackett. Xie et al. (2018) extended the approach and its metatheory; their work is discussed in Section 9.2.
The first implementation of higher-rank polymorphism to see widespread use was in GHC Haskell, and was documented in Peyton Jones et al. (2007). The techniques introduced in this paper were quite similar to ours (Dunfield and Krishnaswami, 2013), but as usual we did not understand the closeness of the relationship until after we reinvented our own version. They specified their algorithm in the Hindley–Milner style: in their specification, variables are automatically instantiated when used and re-generalized as needed, via generalization and specialization rules that are not syntax-directed. Their algorithm eagerly instantiates quantifiers, re-generalizing let-bound expressions; it uses subtyping (specialization) only at bidirectional mode switches. Our algorithm is lazy, never instantiating a quantifier unless it has to. Eisenberg et al. (2016) extended the algorithm of Peyton Jones et al. (2007) with explicit quantifier instantiations. Implementing this approach required lazy instantiation so that the algorithm could delay instantiation until user applications had been processed.
Zhao et al. (2019) give a new machine-checked formalization of type inference, using our declarative specification (Dunfield and Krishnaswami, 2013). However, they give a new algorithm for easier machine verification, in a “worklist” style: Type inference is broken into subproblems just as with other bidirectional systems, but instead of writing the type inference algorithm as a simple recursion on the structure of the syntax, the problems are pushed onto a stack as the syntax is decomposed. This technique avoids the need for an output context—as type checking refines the values of the existential variables, this is automatically propagated to all the remaining subproblems. By associating contexts with judgments on the worklist, rather than threading a context through the derivation, they avoid the need for our “scope markers”. The larger tradeoffs are not entirely clear, but we can say that our algorithm solves problems in a more predictable order, while their approach is potentially more powerful: it enables the algorithm to defer solving problems until more information is available.
5.2. Extensions to Polymorphism
Peyton Jones et al. (2007), our 2013 system, and Zhao et al. (2019) support predicative polymorphism, where quantifiers can be instantiated only with monotypes. Inferring instantiations for impredicative polymorphism is undecidable in general. Building on the approach of Peyton Jones et al. (2007), Serrano et al. (2020) support guarded impredicativity, where the quantifier occurs inside a type constructor.
Another extension to polymorphism is generalized algebraic datatypes (GADTs), in which datatypes are not uniformly polymorphic: the type arguments can depend on the constructor (Xi et al., 2003). Pottier and Régis-Gianas (2006) use bidirectional typing to produce GADT-related annotations, which provide the missing information for non-bidirectional type inference. OutsideIn (Vytiniotis et al., 2011) and Dunfield and Krishnaswami (2019) also use bidirectional typing for GADTs. Both use unification to propagate equality information. Our paper has a declarative specification, though our proofs that our algorithm is sound and complete are quite involved. OutsideIn is more liberal about when it can unify two types without an annotation, which makes it more powerful than our system However, formulating a specification for OutsideIn remains an open problem.
6. Variations on Bidirectional Typing
When discussing work that uses different notation from ours, e.g. and instead of and , we replace the original notation with ours. See Section 11.
6.1. Mixed-direction Types
Instead of distinguishing checking from synthesis at the judgment level, Odersky et al. (2001) make a distinction in type syntax: (1) inherited types serve the purpose of the checking judgment, and (2) synthesized types serve the purpose of the synthesis judgment. In their system, general types combine inherited and synthesized types. For example, in the outermost denotes that the connective is inherited (in our terminology, checked), the that precedes denotes that the domain of the function is synthesized, and the that precedes denotes that the range of the function is inherited (checked). Their subtyping judgment does not synthesize nontrivial supertypes: {}^{\lor}{\mathsf{int}}\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}{}_{\land}{\top} is not derivable, but {}^{\lor}{\mathsf{int}}\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}{}_{\land}{\mathsf{int}} is derivable (the supertype is trivial, being equal to the subtype). When the supertype is inherited (checked), as in {}^{\lor}{\mathsf{int}}\mathrel{\texttt{{\color[rgb]{0.5,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.5}<:}}}{}^{\lor}{\top}, subtyping for Odersky et al. corresponds to the bidirectional subsumption rule.
Another approach to pushing these distinctions into the type syntax can be found in the work on boxy types (Vytiniotis et al., 2006). The type syntax of boxy types is simpler than in the work of Odersky et al. (2001), since it does not permit arbitrary interleaving of checked and synthesized type components of a type: inferred types occur in boxes, and boxes are not allowed to nest. In addition, the treatment of variables does not follow the basic bidirectional recipe; instead, variables are checked, which is more similar to the backwards approach to bidirectional typing we discuss in Section 6.5.
6.2. Directional Logic Programming
One lesson that can already be drawn is that the flow of information through the typing judgments is a key choice in the design of bidirectional systems, and that it is often desirable to go beyond the simple view of modes as either inputs or outputs: for example, Odersky et al. (2001) track whether each part of a type is an input or output. So describing bidirectional typing algorithms can require a more subtle notion of mode.
Reddy (1993) adapts ideas from classical linear logic to characterize directional logic programs. Directional logic programming subsumes moded logic programming. For example, a ternary predicate in regular multi-sorted predicate logic might be given the type:
[TABLE]
This says that a proposition of the form has three arguments, with a list of integers, an integer, and a boolean. With an ordinary mode system, each of these three arguments must be classified entirely as an input or output.
However, in directional logic programming, modes become part of the structure of the sorts, which permits giving sorts like:
[TABLE]
Now, in a predicate occurrence of the form , the argument is an input integer, and is an output boolean, with the an output of sort marked as . The argument has the sort , meaning that the list is structurally an input (so its length is known) but its elements are outputs: the type Int denotes an integer that is an input, while denotes an integer that is an output.
The notation corresponds to negation, and the classical nature of the sort structure arises from the fact that outputting an output is the same as an input —i.e., the user must supply a box which will be filled with an .
This more fine-grained structure lets us give sort declarations which capture the fact that (for example) the boxes in boxy types are outputs but the rest of the type is an input.
6.3. Mode Annotations
Davies (2005, pp. 242–243) describes mode annotations that would allow programmers to declare which functions should be typed using synthesis (instead of checking) and whether the entire application should be checking (instead of synthesizing). As far as we know, mode annotations were never implemented.
Davies motivated this annotation form for polymorphic functions like “higher-order case”, which takes as arguments an instance of a datatype (bits) and a series of functions corresponding to case arms. That is, the “first-class” case expression
[TABLE]
is written .
We can declare the type and mode of the function bcase:
[TABLE]
The second line is a mode annotation. It says that the first argument of bcase should synthesize (be inferred), the remaining three arguments should be checked, and the entire application should be checked (the last chk). Synthesizing the type of the first argument corresponds to the synthesizing principal judgment of the elimination rule Elim; checking the other arguments corresponds to the checking premises of Elim; checking the entire application corresponds to the checking conclusion of Elim.
One can view mode annotations as instructions for transforming a type into a “decorated” type—something like Odersky et al. (2001), but where the connective itself is decorated. The recipe’s elimination rule Elim would correspond to a type , matching the scheme where pr1 is the first premise, pr2 is the second premise and conc is the conclusion. Not all such decorations would be mode correct.
6.4. Simultaneous Input and Output
Another way to blend input and output was developed by Pottier and Régis-Gianas (2006) for type inference for GADTs (Xi et al., 2003). The overall structure of their system is unusual (their bidirectional algorithm produces shapes, which are then given to a non-bidirectional type inference algorithm); for brevity, we explain the idea in a more ordinary setting involving types, not shapes. The basic idea is to combine synthesis and checking judgments into a single judgment with two types: means “check against , synthesizing ”, where is a subtype of . The system thus operates in both checking and synthesis modes simultaneously.
A similar idea is used in the program synthesis work of Polikarpova et al. (2016), round-trip type checking: combines a checking judgment with a type strengthening judgment .
For example, the strengthening rule for variables (Polikarpova et al., 2016, Fig. 4) checks against a given type , but utilizes ’s refinement type (base type such that the constraint holds) to produce a strengthened type .
[TABLE]
Synthesis becomes a special case of strengthening: can be written . Since every type is a subtype of top, the synthesized type is stronger than the goal type (top).
6.5. Backwards Bidirectional Typing
In the basic Pfenning recipe, the principal judgment in an introduction rule is checked, and the principal judgment in an elimination rule synthesizes. However, Zeilberger (2015) observed that in a multiplicative linear type theory, bidirectional typing works precisely as well if you did it backwards, changing all occurrences of synthesis to checking, and vice versa. Zeilberger’s observation was made in the context of a theorem relating graph theory and type theory, but it is a sufficiently striking result that it is worth spelling out in its own right. We will not precisely replicate his system, but we will discuss our divergences when relating it to other bidirectional type systems.
First, we give the syntax of multiplicative linear logic.
Types
Terms
Contexts
The types of MLL are the unit type , the tensor product , and the linear function space . Unit and tensor are introduced by () and , and are eliminated by pattern matching. Functions are introduced by and eliminated using applications .
Contexts are a bit unusual—they pair together variables and their types as usual, but instead of treating a variable as a placeholder for a synthesizing term, we treat variables as placeholders for checking terms. This will have substantial implications for the mode discipline of the algorithm, but we will defer discussion of this point until the whole system is presented.
Now we give the typing rules, starting with those for the unit type.
[TABLE]
The introduction rule says that in an empty context, the unit value () synthesizes the type . The pattern-matching style elimination first synthesizes a type for the body , and then checks that the scrutinee has the unit type .
Thus, we synthesize a type for the continuation first, before checking the type of the data we are eliminating; this is the exact reverse of the Pfenning recipe. For the unit type, this is a mere curiosity, but it gets more interesting with the tensor product type .
[TABLE]
The synthesis rule for pairs remains intuitive, though it reverses the direction given by the Pfenning recipe: for a pair , we first synthesize for and for , then conclude that the pair has type .
However, the elimination rule typing is startling. First, it synthesizes the type for the continuation ; we learn from having typed that and need to have types and respectively. This gives us the information we need to check against . The linear function type has a similar character:
[TABLE]
Here, to synthesize a type for the introduction form , we synthesize for the body , and then look up what type the argument needs to have in order for the body to be well typed. To check that an application has the type , we synthesize for the argument , and then check the function against .
The rule for product elimination suggests a reversed rule for let-expressions, which allows us to defer checking the bound expression until we know what type it needs to have.
[TABLE]
Again, the checking/synthesis modes are reversed from most bidirectional type systems. We can see how this reversal plays out for variables below:
[TABLE]
Here, when we check that the variable has type , the context must be such that it requires to have the type . However, the switch between checking and synthesis is standard.
Relative to most bidirectional systems, the information flow in the variable rule (as well as for pattern matching for pairs and lambda-abstraction for functions) is strange. Usually, the context would give the type of each variable. However, in this case the context is told the type of each variable. This system of rules is still well-moded in the logic programming sense, but the moding is more exotic than simple inputs or outputs. Within a given context, the variables are inputs, but their types are outputs. Following Reddy (1993), the moding of checking and synthesis might be given as
[TABLE]
This mode declaration says that for both checking and synthesis, the spine of the context and the variable names are inputs, but the ascribed type for each variable is an output. Similarly, the term is an input in both judgments, but the type is an input in check but an output in synth.
We can relatively easily prove a substitution theorem for the backwards system:
Theorem 1.
(Backwards Substitution)
If {\Delta}\vdash{e}\mathrel{{{\color[rgb]{0.0,0.0,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.65}\Leftarrow}}}{A}, then
- (1)
If {\Gamma,x\Leftarrow A,\Theta}\vdash{e^{\prime}}\mathrel{{{\color[rgb]{0.0,0.0,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.65}\Leftarrow}}}{C} then {\Gamma,\Delta,\Theta}\vdash{[e/x]e^{\prime}}\mathrel{{{\color[rgb]{0.0,0.0,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.65}\Leftarrow}}}{C}. 2. (2)
If {\Gamma,x\Leftarrow A,\Theta}\vdash{e^{\prime}}\mathrel{{{\color[rgb]{0.45,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.45,0.0,0.0}{\Rightarrow}}}}{C} then {\Gamma,\Delta,\Theta}\vdash{[e/x]e^{\prime}}\mathrel{{{\color[rgb]{0.45,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.45,0.0,0.0}{\Rightarrow}}}}{C}
Unfortunately, we do not presently know how to nicely characterize the set of terms that is typable under this discipline, unlike the characterization for the Pfenning recipe that annotation-free terms are the -normal terms.
6.5.1. Applications of Backwards Bidirectional Typing
When designing a bidirectional type system, what approach should we use—the Pfenning recipe, its pure reversal (as presented above), or something else? The most popular answer seems to be “something else”: Many practical systems synthesize types for literals (unit, booleans, etc.) and for pairs, which—being introduction forms—can only be checked under the strict Pfenning recipe. However, a number of papers have used reversed rules in more subtle ways. Which approach to take depends on the choice of tradeoffs: for example, we can require fewer annotations if we complicate the flow of type information.
Drawing inspiration from relevance logic, which requires variables to be used at least once (as opposed to the exactly-once constraint of linear logic), Chlipala et al. (2005) require a let-bound variable to be used at least once. This allows them to reverse the typing rule for let-expressions, reducing the annotation burden of the basic Pfenning recipe: no annotation is needed on the let-bound expression. Their typing contexts contain checking variables, whose moding is similar to the variables in our backwards bidirectional system. Such a variable must occur at least once in a checking position; that occurrence determines the type of the variable, which can be treated as synthesizing in all other occurrences.
Xie and Oliveira (2018) present another bidirectional type system for polymorphism. Their rule for function application is very similar to the backwards rule presented here, with the idea that backwards typing means that applications like do not need a type annotation at the redex. This requires fewer annotations on let-bindings, as in the work of Chlipala et al. (2005), but with support for polymorphism.
Zeilberger (2015) (and its follow-up work Zeilberger (2018)) did not use any type annotations at all. Instead, his bidirectional system was used to deduce a type scheme for the linear lambda terms, in the style of ML type inference, to find a simple proof of the fact every linearly typed term has a most general type, and moreover that the structure of its -normal, -long form is determined by this type scheme.
Intersection types can reconcile multiple occurrences of the same variable at different types; it appears that the type inference algorithm of Dolan (2016) can be viewed as calculating intersections via a computable lattice operation on types.
7. Proof Theory, Normal Forms, and Type Annotations
7.1. Subformula Property
In cut-free sequent calculi, every formula (proposition) that appears in a derivation is a subformula of some formula in the conclusion. For example, in the following sequent calculus derivation, the formulas and are subformulas (subterms) of the conclusion’s assumption .
[TABLE]
Through the Curry–Howard correspondence, a property of formulas becomes a property of types, but the property is still called the subformula property, to avoid confusion with “subtype”.
A consequence of the subformula property is that if a connective appears in a formula, such as the in in the middle step, the connective must appear in the conclusion. This consequence is useful in a number of type systems, because it ensures that problematic type connectives appear only with the programmer’s permission. Bidirectional type systems based on the recipe in Section 4 only synthesize types that are (subformulas of) annotations: to eliminate an , the function subterm must synthesize by reason of being a variable, an annotation, or an elimination form. The type of a variable flows from an annotation on the binding form (e.g. a inside an annotation) or from the synthesizing premise of an elimination rule (e.g. the premise typing the scrutinee of a case).
Consider, for example, intersection and union types. Efficient type-checking for intersections and unions is difficult (Reynolds, 1996; Dunfield, 2007); intersections and unions that come “out of nowhere” in the middle of a derivation—without being requested via a type annotation—would aggravate this difficulty. Another example is found in type systems that encode multiple evaluation strategies: if a programmer generally prefers call-by-value, but occasionally wants to use call-by-name, the subformula property implies that call-by-name connectives appear only when requested (Dunfield, 2015). Risky connectives abound in gradual type systems: unknown or uncertain types should appear only with the programmer’s permission, because they permit more dynamic failures than other type connectives do (Jafery and Dunfield, 2017).
In type inference, all of typing is in a single judgment. Without a checking judgment, there is no goal type; to increase typing power, one must put more and more “cleverness” into inference. Certain kinds of cleverness destroy the subformula property: automatic generalization, for example, creates “for all” connectives out of nowhere.999It can be argued that automatic generalization is acceptable, because “for all” is less problematic. One might still want a weaker version of the subformula property, saying that every type is either a subformula or related by generalization (and instantiation).
If we relax the recipe by including synthesis rules for (), integer literals and similar constructs, we break the subformula property: () synthesizes when the programmer never wrote . However, a weaker—and still interesting—version of the property may hold, since every type appearing in a derivation is either a subformula of a type in the conclusion or the “obvious” type of a literal constant. That is, we can view () as a request for the type . Note that if we think of () and integer literals as constants whose type is given in a primordial context, so that instead of we have
[TABLE]
then the full subformula property holds. In effect, the author of the primordial context (the language designer) has requested that () and all the integer literals be permitted. Other conveniences, such as synthesizing the types of monomorphic functions, can also be justified (with a little more work; one must think of as a sort of polymorphic constant).
In bidirectional systems, the goal in the checking judgment can steer typing and avoid a measure of cleverness. Thus, while the subformula property is not enjoyed by every imaginable bidirectional type system, bidirectionality seems to make the property easier to achieve.
7.2. Verifications and Uses
In the linear simply typed lambda calculus of Cervesato and Pfenning (2003), typing is presented using two judgments: a pre-canonical judgment that “validates precisely the well-typed terms…in -long form” and a pre-atomic judgment that “handles intermediate stages of their [the terms’] construction”. As suggested by the word “validates”, the pre-canonical judgment corresponds to checking, and the pre-atomic judgment corresponds to synthesis.
Their notation differs from most of the early papers on bidirectional typing: they write pre-canonical judgments as and pre-atomic judgments as , which is almost exactly the reverse of (for example) DML (Xi and Pfenning, 1999), which used for synthesis and for checking. (Both notations are reasonable: computer scientists usually write trees with the root at the top, so Xi’s arrows match the flow of type information through a syntax tree; Gentzen put the root of a derivation tree at the bottom, so Cervesato and Pfenning’s arrows match the flow of type information through the typing derivation.)
This division into validation (checking) and handling intermediate values (synthesis) persists, with different terminology, in Frank Pfenning’s teaching on verifications and uses: A verification of a proposition checks that it is true; a use of an assumption decomposes the assumed proposition. We are not aware of a published paper describing verifications and uses, but the idea appears in many of Pfenning’s lecture notes. The earliest seems to be Pfenning (2004, p. 29), with similar notation to Cervesato and Pfenning (2003):
Proposition has a normal deduction, and
Proposition is extracted from a hypothesis.
Later lecture notes introduce the terminology of verifications and uses, writing and respectively (Pfenning, 2009, 2017). Verification is related (Pfenning, 2017, p. 2) to “intercalation” in proof search (Sieg and Byrnes, 1998).
8. Focusing, Polarized Type Theory, and Bidirectional Type Systems
A widespread folklore belief among researchers is that bidirectional typing arises from polarized formulations of logic. This belief is natural, helpful, and (surprisingly) wrong.
8.1. Bidirectional Typing and the Initial Cartesian Closed Category
The naturalness of the connection can be seen from Figure 2, which gives a bidirectional type system that precisely characterizes -normal, -long terms. The only necessary changes from Figure 1 were:
- •
The annotation rule was removed. Since annotations are only required at -redexes, the omission of this rule forces all typable terms to be -normal.
- •
The mode-switch rule from synthesis to checking is restricted to allow mode switches only at base type. This makes it impossible to partially apply a function in the checking mode: if and , then checks but does not. If a partial application is desired, it must be -expanded to .
Together, these two restrictions ensure that only -normal, -long terms typecheck. Moreover, this characterization is easy to extend to products:
[TABLE]
This type system now characterizes normal forms in the STLC with units and products. Recall that the lambda calculus with units, pairs, and functions is a syntax for the initial cartesian closed category, when terms are quotiented by the theory for each type (Lambek, 1985).
Since this bidirectional system requires -normal, -long terms, we can see it as a calculus that presents the initial model of Cartesian closed categories without any quotienting. Morphisms are well-typed terms, and two morphisms are equal when they are -equivalent.
All that remains is to show that identities and composition are definable. In the ordinary presentation of the initial CCC, a morphism is a term with a free variable, and composition is substitution. In the bidirectional system, however, a morphism is a checking term {x:A}\vdash{e}\mathrel{{{\color[rgb]{0.0,0.0,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.65}\Leftarrow}}}{B}, and substituting a checking term for a variable does not preserve the -normal, -long property. However, if we use hereditary substitution (Pfenning and Davies, 2001; Watkins et al., 2003; Nanevski et al., 2008)—a definition of substitution that also inspects the structure of the term being substituted and “re-normalizes” as it goes—then we restore the property that substitution preserves -normal, -long terms.
This means that the bidirectional type system constitutes a term model for the initial CCC, as follows:
- (1)
The objects of the term are the types of the programming language. 2. (2)
Morphisms are terms {x:X}\vdash{e}\mathrel{{{\color[rgb]{0.0,0.0,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.65}\Leftarrow}}}{Y}. 3. (3)
The identity morphism is the -expansion of the single free variable. 4. (4)
Composition of morphisms is given by hereditary substitution.
The usual presentation of the term model requires quotienting terms by -equivalence, but the term model built from the bidirectional system has the property that equality of morphisms is just -equivalence. By interpreting a non-normal term into this category, any two -equal terms will have the same denotation.
8.2. Adding Problems with Sums
This construction is so beautiful that it is essentially irresistible to add sums to the language. Unfortunately, doing so introduces numerous difficulties. These are most simply illustrated by using the basic bidirectional recipe of Dunfield and Pfenning (2004), which yields an introduction and elimination rule for sum types as follows:
[TABLE]
These rules say that both the injection and case rules have a checking conclusion, but that the scrutinee in the case must synthesize a sum type. As we noted in Section 4.1, this imposes some restrictions on which terms are typeable. For example, because the rule for case has a checking conclusion, we cannot use a case in function position without a type annotation:
[TABLE]
Instead of applying an argument to a case expression of function type, we must push the arguments into the branches:
[TABLE]
If we intend to type only normal forms, this seems desirable: these rules are prohibiting certain term forms that correspond to commuting conversions of allowed terms. The need for commuting conversions has never been popular with logicians: witness Girard’s lament (Girard, 1989, p. 79) that “one tends to think that natural deduction should be modified to correct such atrocities.” However, the simple bidirectional system does not completely eliminate the need for commuting conversions. For example, consider the term
[TABLE]
This term is equivalent to the previous one by a commuting conversion, but both terms are still typable.
Note that allowing the case form to synthesize a type (as in Section 4.1) allows more terms to typecheck, which is the opposite of what we want (in this section, anyway). In practice, it can be difficult to support an unannotated case form which synthesizes its type. Concretely, if the arm synthesizes the type and the arm synthesizes the type , we have to check that they are equal. However, in the general case (e.g., in dependent type theory) equality is relative to the context, and the context is different in each branch (with in one branch and in the other). This is why dependent type theories like Coq end up requiring case expressions to be annotated with a return type: this resolves the problem by having the programmer solve it herself.
8.3. A Polarized Type Theory
At this point, we can make the following pair of observations:
- (1)
The simple bidirectional system for the simply typed lambda calculus with products has the property that two terms are -equal if and only if they are the same: it fully characterizes -equality. 2. (2)
Adding sum types to the bidirectional system breaks this property: two terms equivalent up to (some) commuting conversions may both be typable.
To restore this property, two approaches come to mind. The first approach is to find even more restrictive notions of normal form which prohibit the commuting conversions. We will not pursue this direction in this article, but see Scherer (2017) and Ilik (2017) for examples of this approach.
The second approach is to find type theories in which the commuting conversions no longer preserve equality. By adding (abstract) effects to the language, terms that used to be equivalent can now be distinguished, ensuring that term equality once again coincides with semantic equality. This is the key idea embodied in what is variously called polarized type theory, focalization, or call-by-push-value (Levy, 2001).
Now, we give a polarized type theory resembling those of Simmons (2014) and Espírito Santo (2017). Our main change is to adjust the proof term assignment to look more familiar to functional programmers.
Positive types
Negative types
Values
Spines
Terms
Patterns
Contexts
Typing values
{\Gamma}\vdash{v}\mathrel{{{\color[rgb]{0.0,0.0,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.65}\Leftarrow}}}{P}
Typing spines
Typing terms
Typing patterns
The key idea in polarized type theory is to divide types into two categories: positive types (sums, strict products, and suspended computations) and negative types (basically, functions). Positive types are eliminated by pattern matching, and negative types are eliminated by supplying arguments. Negative types can be embedded into positive types using the “downshift” type (representing suspended computations); positive types can be embedded into negative types using the “upshift” (denoting computations producing ’s).
The semantics of call-by-push-value offer insight into the design of this calculus: positive types correspond to objects of a category of values (such as sets and functions), and negative types correspond to objects of a category of computations (objects are algebras of a signature for the computations, and morphisms are algebra homomorphisms). Upshift and downshift form an adjunction between values and computations, and the monads familiar to functional programmers arise via the composite: .
While this calculus arises from meditation upon invariants of proof theory, its syntax is much closer to practical functional programming languages than the pure typed lambda calculus, including features like clausal definitions and pattern matching. But the price we pay is a proliferation of judgments. We usually end up introducing separate categories of values (for introducing positive types) and spines (argument lists for calling functions), as well as terms (how to put values and spines together in computations, as well as introducing negative types) and patterns (how to eliminate positive types).
Contexts have two kinds of variables, for negative variables and for positive variables.
8.3.1. Typing Values
First, we give the typing rules for values. As in the simple bidirectional recipe, we have a judgment {\Gamma}\vdash{v}\mathrel{{{\color[rgb]{0.0,0.0,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.65}\Leftarrow}}}{P} for checking the type of positive values.
[TABLE]
The rules for units, pairs and sums are unchanged from the simple bidirectional recipe. The rule for downshift says that if a term checks at a negative type , then the thunked term will check against the downshifted type . Finally, a variable checks at a type if the context says that has a type equal to . (With subtyping, we would instead check that is a subtype of .)
8.3.2. Typing Spines
Before we give the typing rules for all terms, we will give the rules deriving the spine judgment , read “if spine is applied to a head of type , it will produce a result of type ”. The type is an algorithmic input, and the type is an output.
[TABLE]
The first rule says that an empty argument list does nothing to the type of the head: the result is the same as the input. The second rule says that a non-empty argument list sends the function type to , if is a value of type (i.e., a valid argument to the function), and is an argument list sending to .
8.3.3. Typing Terms
With values and spines in hand, we can talk about terms, in the term typing judgment , which checks that a term has the type .
[TABLE]
The rule for says that we embed a value of type into the upshift type by immediately returning it. Lambda abstractions are pattern-style—instead of a single binder , we give a list of patterns and branches to check at type . As a result, we need a judgment giving the types of the bindings of the pattern , and then we check each against the result type . Then we check each branch against the type in a context extended by .
We face similar issues in the match expression . First, it finds the variable in the context, applies some arguments to it to find a value result of type , and then pattern matches against type . (In typical bidirectional systems, a synthesis judgment would type ; in this polarized system of normal forms, the synthesis judgment is absorbed into the rule for match expressions.) We check that the spine sends to the type , and then check that the patterns yield variables at the type , we can check each against the type . Restricting the type at which we can match forces us to -expand terms of function type.
Both lambdas and application/pattern-matching use the judgment to find the types of the bindings. The rules for these are straightforward:
[TABLE]
Units yield no variables at type , pair patterns return the variables of each component, injections return the variables of the sub-pattern , and thunk patterns at type return that variable at type . Here, we omit a judgment to check whether a set of patterns is complete; see Krishnaswami (2009) for a polarization-based approach.
Value bindings bind a value of type to a variable , which allows values to be pattern-matched without being fully decomposed. Hence, our calculus is weakly focused in the sense of Pfenning and Simmons (2009).
8.4. Discussion
Bidirectional typing integrates very nicely into a perspective based on polarized logic. Indeed, the “application judgment” in Dunfield and Krishnaswami (2013) can be seen as a special case of the spine judgment, and even systems not designed from an explicitly bidirectional perspective, such as Serrano et al. (2018), have found it beneficial to work with entire argument lists. In our view, this is because the spine judgment is well-moded, making it easy to manage the flow of information through the argument list.
This close fit is not limited to argument lists, but also extends to other features where functional languages go beyond kernel calculi, such as pattern matching. Krishnaswami (2009) shows how ML-style pattern matching arises as the proof terms of a focused calculus, and indeed the type system in that paper is bidirectional. This system only covered simple types, but the approach scales well. Our bidirectional type system for generalized algebraic data types (Dunfield and Krishnaswami, 2019) goes much further, including both universal and existential quantification, GADTs, and pattern matching. Nevertheless, it is built upon essentially the same idea of applying bidirectional typing to a focused type theory.
However, despite the fact that the standard recipe of bidirectional typing fits beautifully with focused logics, we should not lose sight of the fact that the essence of bidirectional typing is the management of information flow. Consequently, these techniques apply more broadly than polarized calculi, as fundamental as they may be. In Section 6, we saw a number of systems with a different mode structure, such as the mixed-direction types of Odersky et al. (2001), the strict type inference of Chlipala et al. (2005), and the backwards bidirectional system of Zeilberger (2015). All of these reject the basic bidirectional recipe, but are undeniably bidirectional.
Thus, we would advise designers of new bidirectional systems to seek inspiration from polarized type theory, but not to restrict themselves to it.
9. Other Applications of Bidirectional Typing
9.1. Dependent Types, Refinement Types, and Intersection Types
The DML system (Xi and Pfenning, 1999; Xi, 1998) used bidirectional typing because type inference for index refinements (a form of refinement type) is undecidable. DML followed a “relaxed” version of the Pfenning recipe that allowed some rules that are not strictly necessary, such as an introduction rule that synthesizes a type for if and synthesize.
The first datasort refinement system (Freeman and Pfenning, 1991) used a form of type inference similar to abstract interpretation; the later systems SML-CIDRE (Davies and Pfenning, 2000; Davies, 2005) and Stardust (Dunfield, 2007) used bidirectional typing. In SML-CIDRE, type inference was eschewed in favour of bidirectional typing: type inference finds all behaviours, not only the intended behaviours. The type annotations in bidirectional typing, especially when following the Pfenning recipe as SML-CIDRE did, force programmers to write down the behaviours they intend. In Stardust, the decision to use bidrectional typing was also motivated by the undecidability of type inference for index refinements.
In contextual modal type theory (Nanevski et al., 2008), typing is bidirectional to make type checking decidable in the presence of dependent types. That theory is the main foundation for Beluga, which is bidirectional for the same reason. The original core of Beluga (Pientka, 2008; Pientka and Dunfield, 2008) follows the Pfenning recipe, but the full system (Pientka, 2013) extends the recipe, supporting both checking and synthesis for spines (lists of function arguments).
Bidirectional type checking was folklore among programming language developers since the 1980s, and was known and used by developers of proof assistants since the 1990s: Coquand (1996) presents a type-checking algorithm for a small dependent type system (dependent products, plus let-expressions), in which “type-checking” () and “type inference” () “inductively and simultaneously”. Coquand’s version of a subsumption rule (Coquand, 1996, p. 173, third part of definition) says that checks against if synthesizes and is convertible to . Moreover, by removing the parts related to dependent typing, we see that Coquand’s rule for -application (the fifth part of his definition) is essentially our standard rule: to synthesize a type for , synthesize a type for and check against the domain of that type. Strikingly, the Gofer code in the paper has functions checkExp and inferExp that have the expected type signatures; for example, checkExp returns a boolean.
Scherer and Abel (2012) give a bidirectional algorithm for judgmental equality in dependent type theory. They give a non-bidirectional specification of a dependent type system. Then they give a bidirectional algorithmic system, which defines where to do equality tests and leads to a nice algorithm for how to do judgmental equality. They prove soundness, completeness, and decidability of their algorithm using two intricate logical relations; the combination of soundness and completeness leads to decidability. Judgmental equality is bidirectional: comparison of neutral terms synthesizes, and comparison of normal terms checks. This cleverly exploits the fact that off-diagonal cases (e.g., atomic terms compared against a normal terms) can be omitted, as an atomic term can only equal another term if reduces to another term with the same head variable as .
McBride (2016) advocates a bidirectional system as the specification of a dependent type system. Other bidirectional dependent type systems include PiSigma (Altenkirch et al., 2010), intended as a small core system for dependently typed languages, and Zombie (Sjöberg and Weirich, 2015). As with subtyping, conversion checking is not syntax-directed and is guided by bidirectionality. Taking the bidirectional system as the specification simplifies the metatheory in some ways. However, proving that an algorithmic conversion relation is an equivalence relation, congruent for all the syntactic forms, still seems to require a sophisticated argument.
Intersection types, originally formulated in undecidable type assignment systems, have motivated the use of bidirectional typing in several systems, including refinement intersection types (Dunfield and Pfenning, 2004) and unrestricted intersection types (Dunfield, 2014; Oliveira et al., 2016) with polymorphism (Alpuim et al., 2017). Some of these systems also include union types.
9.2. Gradual Typing
Gradual typestate (Wolff et al., 2011) uses bidirectional typing to structure the flow of information about access permissions, specified in annotations. Their language, descended from Featherweight Java, is imperative in flavour; its expression forms are not easy to classify as introductions or eliminations, making it hard to apply the Pfenning recipe. Our discussion of reasoning by cases (step 3 in Section 4.1) carries over to their typing rules for let, which allow either (1) the body of the let to synthesize, and hence the entire let, or (2) the body to be checked, based on a type against which the entire let is to be checked. (Our judgment form from Section 5 looks similar to the gradual typestate judgment ; moreover, in both settings, the left-hand context is called the input context and the right-hand context is called the output context. However, the meaning is completely different. In gradual typestate, the output context describes the state after running the subject expression, so the output context often has different information than the input context.)
Gradual sum types (Jafery and Dunfield, 2017) are formulated in a functional style, so the Pfenning recipe works. The subformula property ensures that uncertain types—connectives that relax the guarantees of static typing—appear only when the programmer asks for them. In their subsumption rule (ChkCSub), the subtyping judgment is replaced by directed consistency, a relation that contains subtyping but also allows shifts between more precise (less uncertain, more static) and less precise (more uncertain, less static) types.
Xie et al. (2018) develop a gradual type system with consistent subtyping (related to directed consistency) and higher-rank polymorphism. Their bidirectional system closely follows Dunfield and Krishnaswami (2013), discussed in Section 5.1; this approach leads to a subformula property that, as in (Jafery and Dunfield, 2017), ensures that the unknown type appears only by programmer request.
9.3. Other Work
Çiçek et al. (2019) define a relational type system where each judgment has two subject terms (expressions): relates the terms and at type . Their bidirectionalization follows the Pfenning recipe in its original form, for example, their rule alg-r-if for if expressions has a checking conclusion.
10. Historical Notes
Pierce and Turner’s paper “Local Type Inference”—which appeared as a technical report ((1997)), at POPL ((1998)) and in TOPLAS ((2000))—is the earliest frequently cited paper on bidirectional typing, but Pierce noted that “John Reynolds first acquainted us [BCP] with the idea of bidirectional typechecking around 1988”.
That year also saw the first version of the report on Forsythe (Reynolds, 1988), where Reynolds noted that Forsythe’s intersection types would require some type information in the source program. The second version of the report (Reynolds, 1996, Appendix C) describes an algorithm that combines “bottom-up typechecking” and “top-down checking”, but the precise connection to bidirectional typing is not clear to us.
Lee and Yi (1998) present Algorithm , a type inference algorithm used in some versions of Caml Light (the predecessor of OCaml). In contrast to Algorithm (Milner, 1978), if we reformulate Algorithm as a set of typing rules, they are all checking rules: there is an input type to check against. In some situations—for example, when typing a let-bound expression—the input type is a fresh unification variable, but the input type often carries information. They show that can find type errors earlier than , which is consistent with the idea that bidirectional checking provides better error messages.
Dunfield and Pfenning (2004) has two authors, but the recipe was invented by Frank Pfenning, so we call it the Pfenning recipe.
11. Summary of Bidirectional Typing Notation
Table 1 summarizes some of the symbols that have been used to denote checking and synthesis. Until about 2008, most authors used vertical arrows ( for checking and for synthesis), though Pierce and Turner (2000) used for checking and for synthesis. The arrows were meant to represent information flow, but vertical arrows are unclear because syntax trees and derivation trees put the root at opposite ends: does mean that the type flows from a leaf of a syntax tree (at the bottom, away from the root), or from the conclusion of a derivation tree?
Horizontal arrows avoid this confusion: nearly all authors write the subject term to the left of the type in a judgment, so means that the type is flowing from the term and means that the type is flowing “into” the term.
The / notation, used by McBride (2016), has the advantage that information always flows left to right.
12. Conclusion
Bidirectional typing is usually straightforward to implement. However, while the bidirectional approach allows us to prove soundness, completeness and decidability of state-of-the-art typing algorithms, the proofs are often extremely involved. Moreover, the proofs are about type systems that focus on a few features of research interest. Since realistic programming languages combine many typing features, doing the metatheory for a full-scale type system seems intractable using current techniques. A key challenge for future research is to discover techniques to simplify the proofs of soundness, completeness, and decidability, enabling researchers to prove these key properties for complete programming languages.
Another future research direction is that polarity, focusing and call-by-push-value seem to fit nicely with bidirectional typing, but are not the same as bidirectional typing. We would like to understand the actual relationship between these ideas, making it easier to integrate advances in proof theory into language design.
Designers of bidirectional type systems often employ information flow that goes beyond checking (where the entire type is input) and synthesis (where the entire type is output). We would like to have a better understanding of how such information flow interacts with core metatheoretic properties, such as substitution principles, in order to arrive at broadly applicable design principles for type system design.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1(1)
- 2Alpuim et al . (2017) João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. 2017. Disjoint Polymorphism. In European Symposium on Programming , Hongseok Yang (Ed.). Springer, 1–28.
- 3Altenkirch et al . (2010) Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, and N. Oury. 2010. Π Σ Π Σ \Pi\Sigma : Dependent Types without the Sugar. In FLOPS . Springer, 40–55.
- 4Barendregt et al . (1983) Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983. A Filter Lambda Model and the Completeness of Type Assignment. Journal of Symbolic Logic 48, 4 (1983), 931–940.
- 5Cardelli (1993) Luca Cardelli. 1993. An Implementation of F <: subscript F <: {\text{F}}_{\texttt{<:}} . Research report 97. DEC/Compaq Systems Research Center.
- 6Çiçek et al . (2019) Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, and Deepak Garg. 2019. Bidirectional Type Checking for Relational Properties. In Programming Language Design and Implementation (PLDI 2019) . ACM Press, 533–547.
- 7Cervesato and Pfenning (2003) Iliano Cervesato and Frank Pfenning. 2003. A Linear Spine Calculus. J. Logic and Computation 13, 5 (2003), 639–688.
- 8Chlipala et al . (2005) Adam Chlipala, Leaf Petersen, and Robert Harper. 2005. Strict bidirectional type checking. In Workshop on Types in Language Design and Impl. (TLDI ’05) . ACM Press, 71–78.
