Let Arguments Go First
Abstract
Bidirectional type checking has proved to be an extremely useful and versatile tool for type checking and type inference. The conventional presentation of bidirectional type checking consists of two modes: inference mode and checked mode. In traditional bidirectional typechecking, type annotations are used to guide (via the checked mode) the type inference/checking procedure to determine the type of an expression, and type information flows from functions to arguments.
This paper presents a variant of bidirectional type checking where the type information flows from arguments to functions. This variant retains the inference mode, but adds a socalled application mode. Such design can remove annotations that basic bidirectional type checking cannot, and is useful when type information from arguments is required to typecheck the functions being applied. We present two applications and develop the metatheory (mostly verified in Coq) of the application mode.
1 Introduction
Bidirectional type checking has been known in the folklore of type systems for a long time. It was popularized by Pierce and Turner’s work on local type inference [29]. Local type inference was introduced as an alternative to HindleyMilner (henceforth HM system) type systems [11, 17], which could easily deal with polymorphic languages with subtyping. Bidirectional type checking is one component of local type inference that, aided by some type annotations, enables type inference in an expressive language with polymorphism and subtyping. Since Pierce and Turner’s work, various other authors have proved the effectiveness of bidirectional type checking in several other settings, including many different systems with subtyping [12, 14, 15], systems with dependent types [2, 3, 10, 21, 37], and various other works [1, 7, 13, 22, 28]. Furthermore, bidirectional type checking has also been combined with HMstyle techniques for providing type inference in the presence of higherranked types [14, 27].
In the above rule, which is a standard bidirectional rule for checking applications, the two modes are used. First we synthesize ( Open image in new window ) the type \(A \rightarrow B\) from \(e_1\), and then check ( Open image in new window ) \(e_2\) against A, returning B as the type for the application.
In this rule, there are two kinds of judgments. The first judgment is just the usual inference mode, which is used to infer the type of the argument \(e_2\). The second judgment, the application mode, is similar to the inference mode, but it has an additional context \(\varPsi \). The context \(\varPsi \) is a stack that tracks the types of the arguments of outer applications. In the rule for application, the type of the argument \(e_2\) is inferred first, and then pushed into \(\varPsi \) for inferring the type of \(e_1\). Applications are themselves in the application mode, since they can be in the context of an outer application. With the application mode it is possible to infer the type for expressions such as Open image in new window without additional annotations.
Bidirectional type checking with an application mode may still require type annotations and it gives different tradeoffs with respect to the checked mode in terms of type annotations. However the different tradeoffs open paths to different designs of type checking/inference algorithms. To illustrate the utility of the application mode, we present two different calculi as applications. The first calculus is a higher ranked implicit polymorphic type system, which infers higherranked types, generalizes the HM type system, and has polymorphic let as syntactic sugar. As far as we are aware, no previous work enables an HMstyle let construct to be expressed as syntactic sugar. For this calculus many results are proved using the Coq proof assistant [9], including typesafety. Moreover a sound and complete algorithmic system, inspired by Peyton Jones et al. [27], is also developed. A second calculus with explicit polymorphism illustrates how the application mode is compatible with type applications, and how it adds expressiveness by enabling an encoding of type declarations in a SystemFlike calculus. For this calculus, all proofs (including type soundness), are mechanized in Coq.
We believe that, similarly to standard bidirectional type checking, bidirectional type checking with an application mode can be applied to a wide range of type systems. Our work shows two particular and nontrivial applications. Other potential areas of applications are other type systems with subtyping, static overloading, implicit parameters or dependent types.

A variant of bidirectional type checking where the inference mode is combined with a new, socalled, application mode. The application mode naturally propagates type information from arguments to the functions.

A new design for type inference of higherranked types which generalizes the HM type system, supports a polymorphic \(\mathbf{let}\) as syntactic sugar, and infers higher rank types. We present a syntaxdirected specification, an elaboration semantics to System F, some metatheory in Coq, and an algorithmic type system with completeness and soundness proofs.

A SystemFlike calculus as a theoretical response to the challenge noted by Pierce and Turner [29]. It shows that the application mode is compatible with type applications, which also enables encoding type declarations. We present a type system and metatheory, including proofs of type safety and uniqueness of typing in Coq.
2 Overview
2.1 Background: Bidirectional Type Checking
Specifically, if we know that the type of \(e_1\) is a function from Open image in new window , we can check that \(e_2\) has type Open image in new window . Notice that here the type information flows from functions to arguments.
Unfortunately, this means that the trivial program Open image in new window cannot typecheck, which in this case has to be rewritten to Open image in new window .
In this particular case, bidirectional type checking goes against its original intention of removing burden from programmers, since a seemingly unnecessary annotation is needed. Therefore, in practice, bidirectional type systems do not strictly follow the guideline, and usually have additional inference rules for the introduction form of constructs. For pairs, the corresponding rule is PairI.
Now we can type check Open image in new window , but the price to pay is that two typing rules for pairs are needed. Worse still, the same criticism applies to other constructs. This shows one drawback of bidirectional type checking: often to minimize annotations, many rules are duplicated for having both inference and checked mode, which scales up with the typing rules in a type system.
2.2 Bidirectional Type Checking with the Application Mode
We propose a variant of bidirectional type checking with a new application mode. The application mode preserves the advantage of bidirectional type checking, namely many redundant annotations are removed, while certain programs can type check with even fewer annotations. Also, with our proposal, the inference mode is a special case of the application mode, so it does not produce duplications of rules in the type system. Additionally, the checked mode can still be easily combined into the system (see Sect. 5.1 for details). The essential idea of the application mode is to enable the type information flow in applications to propagate from arguments to functions (instead of from functions to arguments as in traditional bidirectional type checking).
This expression cannot type check in traditional bidirectional type checking because unannotated abstractions only have a checked mode, so annotations are required. For example, Open image in new window .
In this example we can observe that if the type of the argument is accounted for in inferring the type of Open image in new window , then it is actually possible to deduce that the lambda expression has type Open image in new window , from the argument Open image in new window .
The type Open image in new window that appears last in the application context serves as the type for Open image in new window , and type checking continues with a smaller application context and Open image in new window in the typing context. Therefore, using the rule App and Lam, the expression Open image in new window can typecheck without annotations, since the type Open image in new window of the argument Open image in new window is used as the type of the binding Open image in new window .
Note that, since the examples so far are based on simple types, obviously they can be solved by integrating type inference and relying on techniques like unification or constraint solving. However, here the point is that the application mode helps to reduce the number of annotations without requiring such sophisticated techniques. Also, the application mode helps with situations where those techniques cannot be easily applied, such as type systems with subtyping.
Interpretation of the Application Mode. As we have seen, the guideline for designing bidirectional type checking [15], based on introduction and elimination rules, is often not enough in practice. This leads to extra introduction rules in the inference mode. The application mode does not distinguish between introduction rules and elimination rules. Instead, to decide whether a rule should be in inference or application mode, we need to think whether the expression can be applied or not. Variables, lambda expressions and applications are all examples of expressions that can be applied, and they should have application mode rules. However pairs or literals cannot be applied and should have inference rules. For example, type checking pairs would simply lead to the rule PairI. Nevertheless elimination rules of pairs could have nonempty application contexts (see Sect. 5.2 for details). In the application mode, arguments are always inferred first in applications and propagated through application contexts. An empty application context means that an expression is not being applied to anything, which allows us to model the inference mode as a particular case^{2}.
Partial Type Checking. The inference mode synthesizes the type of an expression, and the checked mode checks an expression against some type. A natural question is how do these modes compare to application mode. An answer is that, in some sense: the application mode is stronger than inference mode, but weaker than checked mode. Specifically, the inference mode means that we know nothing about the type an expression before hand. The checked mode means that the whole type of the expression is already known before hand. With the application mode we know some partial type information about the type of an expression: we know some of its argument types (since it must be a function type when the application context is nonempty), but not the return type.
Instead of nothing or all, this partialness gives us a finer grain notion on how much we know about the type of an expression. For example, assume \({e: A \rightarrow B \rightarrow C}\). In the inference mode, we only have e. In the checked mode, we have both e and \({A \rightarrow B \rightarrow C}\). In the application mode, we have e, and maybe an empty context (which degenerates into inference mode), or an application context A (we know the type of first argument), or an application context B, A (we know the types of both arguments).
Tradeoffs. Note that the application mode is not conservative over traditional bidirectional type checking due to the different information flow. However, it provides a new design choice for type inference/checking algorithms, especially for those where the information about arguments is useful. Therefore we next discuss some benefits of the application mode for two interesting cases where functions are either variables; or lambda (or type) abstractions.
2.3 Benefits of Information Flowing from Arguments to Functions
Local Constraint Solver for Function Variables. Many type systems, including type systems with implicit polymorphism and/or static overloading, need information about the types of the arguments when type checking function variables. For example, in conventional functional languages with implicit polymorphism, function calls such as Open image in new window where Open image in new window , are pervasive. In such a function call the type system must instantiate a to \(\mathsf {Int}\). Dealing with such implicit instantiation gets trickier in systems with higherranked types. For example, Peyton Jones et al. [27] require additional syntactic forms and relations, whereas Dunfield and Krishnaswami [14] add a special purpose application judgment.
With the application mode, all the type information about the arguments being applied is available in application contexts and can be used to solve instantiation constraints. To exploit such information, the type system employs a special subtyping judgment called application subtyping, with the form \(\varPsi \vdash A \le B\). Unlike conventional subtyping, computationally \(\varPsi \) and A are interpreted as inputs and B as output. In above example, we have that \(\mathsf {Int}\vdash \forall a. a \rightarrow a \le B\) and we can determine that \(a = \mathsf {Int}\) and \(B = \mathsf {Int}\rightarrow \mathsf {Int}\). In this way, type system is able to solve the constraints locally according to the application contexts since we no longer need to propagate the instantiation constraints to the typing process.
Such syntactic sugar for Open image in new window is, of course, standard. However, in the context of implementations of typed languages it normally requires extra type annotations or a more sophisticated typedirected translation. Type checking \((\lambda x.~e_2)~e_1\) would normally require annotations (for example an annotation for x), or otherwise such annotation should be inferred first. Nevertheless, with the application mode no extra annotations/inference is required, since from the type of the argument \(e_1\) it is possible to deduce the type of x. Generally speaking, with the application mode annotations are never needed for applied lambdas. Thus Open image in new window can be the usual sugar from the untyped lambda calculus, including HMstyle Open image in new window expression and even type declarations.
2.4 Application 1: Type Inference of HigherRanked Types
As a first illustration of the utility of the application mode, we present a calculus with implicit predicative higherranked polymorphism.
HigherRanked Types. Type systems with higherranked types generalize the traditional HM type system, and are useful in practice in languages like Haskell or other MLlike languages. Essentially higherranked types enable much of the expressive power of System F, with the advantage of implicit polymorphism. Complete type inference for System F is known to be undecidable [36]. Therefore, several partial type inference algorithms, exploiting additional type annotations, have been proposed in the past instead [15, 25, 27, 31].
Generalization. Generalization is famous for its application in let polymorphism in the HM system, where generalization is adopted at let bindings. Let polymorphism is a useful component to introduce toplevel quantifiers (rank 1 types) into a polymorphic type system. The previous example becomes typeable in the HM system if we rewrite it to: Open image in new window .
Type Inference for HigherRanked Types with the Application Mode. Using our bidirectional type system with an application mode, the original expression can type check without annotations or rewrites: Open image in new window .
With this approach, nested lets can lead to types which are more general than HM. For example, Open image in new window . The type of Open image in new window is Open image in new window after generalization. Because Open image in new window returns Open image in new window as a result, we might expect Open image in new window , which is what our system will return. However, HM will return type Open image in new window , as it can only return rank 1 types, which is less general than the previous one according to Odersky and Läufer’s subtyping relation for polymorphic types [24].
Conservativity over the HindleyMilner Type System. Our type system is a conservative extension over the HindleyMilner type system, in the sense that every program that can typecheck in HM is accepted in our type system, which is explained in detail in Sect. 3.2. This result is not surprising: after desugaring Open image in new window into a lambda and an application, programs remain typeable.
Comparing Predicative HigherRanked Type Inference Systems. We will give a full discussion and comparison of related work in Sect. 6. Among those works, we believe the work by Dunfield and Krishnaswami [14], and the work by Peyton Jones et al. [27] are the most closely related work to our system. Both their systems and ours are based on a predicative type system: universal quantifiers can only be instantiated by monotypes. So we would like to emphasize our system’s properties in relation to those works. In particular, here we discuss two interesting differences, and also briefly (and informally) discuss how the works compare in terms of expressiveness.

(1) Inference of higherranked types. In both works, every polymorphic type inferred by the system must correspond to one annotation provided by the programmer. However, in our system, some higherranked types can be inferred from the expression itself without any annotation. The motivating expression above provides an example of this.

(2) Where are annotations needed? Since type annotations are useful for inferring higher rank types, a clear answer to the question where annotations are needed is necessary so that programmers know when they are required to write annotations. To this question, previous systems give a concrete answer: only on the binding of polymorphic types. Our answer is slightly different: only on the bindings of polymorphic types in abstractions that are not applied to arguments. Roughly speaking this means that our system ends up with fewer or smaller annotations.

(3) Expressiveness. Based on these two answers, it may seem that our system should accept all expressions that are typeable in their system. However, this is not true because the application mode is not conservative over traditional bidirectional type checking. Consider the expression Open image in new window , which is typeable in their system. In this case, even if g is a polymorphic binding without a type annotation the expression can still typecheck. This is because the original application rule propagates the information from the outer binding into the inner expressions. Note that the fact that such expression typechecks does not contradict their guideline of providing type annotations for every polymorphic binder. Programmers that strictly follow their guideline can still add a polymorphic type annotation for g. However it does mean that it is a little harder to understand where annotations for polymorphic binders can be omitted in their system. This requires understanding how the applications in checked mode operate.
In our system the above expression is not typeable, as a consequence of the information flow in the application mode. However, following our guideline for annotations leads to a program that can be typechecked with a smaller annotation: Open image in new window . This means that our work is not conservative over their work, which is due to the design choice of the application typing rule. Nevertheless, we can always rewrite programs using our guideline, which often leads to fewer/smaller annotations.
2.5 Application 2: More Expressive Type Applications
Therefore, as a response to this challenge, our second application is a variant of System F. Our development of the calculus shows that the application mode can actually work well with calculi with explicit type applications. To explain the new design, consider the expression:“It is possible, of course, to come up with examples where it would be beneficial to synthesize the argument types first and then use the resulting information to avoid type annotations in the function part of an application expression....Unfortunately this refinement does not help infer the type of polymorphic functions. For example, we cannot uniquely determine the type of x in the expression \((fun[X](x) ~ e) ~ [\mathsf {Int}] ~ 3\).” [29]
which is not typeable in the traditional type system for System F. In System F the lambda abstractions do not account for the context of possible function applications. Therefore when type checking the inner body of the lambda abstraction, the expression Open image in new window is illtyped, because all that is known is that Open image in new window has the (abstract) type Open image in new window .
If we are allowed to propagate type information from arguments to functions, then we can verify that Open image in new window and Open image in new window is welltyped. The key insight in the new type system is to use application contexts to track type equalities induced by type applications. This enables us to type check expressions such as the body of the lambda above ( Open image in new window ). Therefore, back to the problematic expression \((fun[X](x) ~ e) ~ [\mathsf {Int}] ~ 3\), the type of Open image in new window can be inferred as either Open image in new window or Open image in new window since they are actually equivalent.
(after desugaring) does not typecheck, as in a SystemF like language. In our type system lambda abstractions that are immediatelly applied to an argument, and unapplied lambda abstractions behave differently. Unapplied lambda abstractions are just like System F abstractions and retain type abstraction. The example above illustrates this. In contrast the typeable example Open image in new window , which uses a lambda abstraction directly applied to an argument, can be regarded as the desugared expression for Open image in new window .
3 A Polymorphic Language with HigherRanked Types
This section first presents a declarative, syntaxdirected type system for a lambda calculus with implicit higherranked polymorphism. The interesting aspects about the new type system are: (1) the typing rules, which employ a combination of inference and application modes; (2) the novel subtyping relation under an application context. Later, we prove our type system is typesafe by a type directed translation to System F [16, 27] in Sect. 3.4. Finally an algorithmic type system is discussed in Sect. 3.5.
3.1 Syntax
Types. Types include type variables (a), functions (\(A \rightarrow B\)), polymorphic types (\(\forall a. A\)) and integers (\(\mathsf {Int}\)). We use capital letters (A, B) for types, and small letters (a, b) for type variables. Monotypes are types without universal quantifiers.
3.2 Type System
The top part of Fig. 1 gives the typing rules for our language. The judgment Open image in new window is read as: under typing context \(\varGamma \), and application context \(\varPsi \), e has type B. The standard inference mode Open image in new window can be regarded as a special case when the application context is empty. Note that the variable names are assumed to be fresh enough when new variables are added into the typing context, or when generating new type variables.
Rule TVar says that if x : A is in the typing context, and A is a subtype of B under application context \(\varPsi \), then x has type B. It depends on the subtyping rules that are explained in Sect. 3.3. Rule TInt shows that integer literals are only inferred to have type \(\mathsf {Int}\) under an empty application context. This is obvious since an integer cannot accept any arguments.
TLam shows the strength of application contexts. It states that, without annotations, if the application context is nonempty, a type can be popped from the application context to serve as the type for x. Inference of the body then continues with the rest of the application context. This is possible, because the expression \(\lambda {x}.~ e\) is being applied to an argument of type A, which is the type at the top of the application context stack. Rule TLam2 deals with the case when the application context is empty. In this situation, a monotype \(\tau \) is guessed for the argument, just like the HindleyMilner system.
Rule TLamAnn1 works as expected with an empty application context: a new variable x is put with its type A into the typing context, and inference continues on the abstraction body. If the application context is nonempty, then the rule TLamAnn2 applies. It checks that C is a subtype of A before putting x : A in the typing context. However, note that it is always possible to remove annotations in an abstraction if it has been applied to some arguments.
Rule TApp pushes types into the application context. The application rule first infers the type of the argument \(e_2\) with type A. Then the type A is generalized in the same way that types in \(\mathbf{let}\) expressions are generalized in the HM type system. The resulting generalized type is B. The generalization is shown in rule TGen, where all free type variables are extracted to quantifiers. Thus the type of \(e_1\) is now inferred under an application context extended with type B. The generalization step is important to infer higher ranked types: since B is a possibly polymorphic type, which is the argument type of \(e_1\), then \(e_1\) is of possibly a higher rank type.
The type \(A_2\) is now pushed into application context in rule TApp, and then assigned to x in TLam. Comparing this with the typing derivations with rule TLet, we now have same preconditions. Thus we can see that the rules in Fig. 1 are sufficient to express an HMstyle polymorphic let construct.
MetaTheory. The type system enjoys several interesting properties, especially lemmas about application contexts. Before we present those lemmas, we need a helper definition of what it means to use arrows on application contexts.
Definition 1
(\(\varPsi \rightarrow B\)). If \(\varPsi = A_1, A_2, ..., A_n\), then \(\varPsi \rightarrow B\) means the function type \(A_n \rightarrow ... \rightarrow A_2 \rightarrow A_1 \rightarrow B\).
Such definition is useful to reason about the typing result with application contexts. One specific property is that the application context determines the form of the typing result.
Lemma 1
(\(\varPsi \) Coincides with Typing Results). If Open image in new window , then for some \(A'\), we have \(A = \varPsi \rightarrow A'\).
Having this lemma, we can always use the judgment Open image in new window instead of Open image in new window .
In traditional bidirectional type checking, we often have one subsumption rule that transfers between inference and checked mode, which states that if an expression can be inferred to some type, then it can be checked with this type. In our system, we regard the normal inference mode Open image in new window as a special case, when the application context is empty. We can also turn from normal inference mode into application mode with an application context.
Lemma 2
(Subsumption). If Open image in new window , then Open image in new window .
The relationship between our system and standard Hindley Milner type system can be established through the desugaring of let expressions. Namely, if e is typeable in Hindley Milner system, then the desugared expression e is typeable in our system, with a more general typing result.
Lemma 3
(Conservative over HM). If Open image in new window , then for some B, we have Open image in new window , and Open image in new window .
3.3 Subtyping
We present our subtyping rules at the bottom of Fig. 1. Interestingly, our subtyping has two different forms.
Subtyping. The first judgment follows Odersky and Läufer [24]. Open image in new window means that A is more polymorphic than B and, equivalently, A is a subtype of B. Rules SInt and SVar are trivial. Rule SForallR states A is subtype of \(\forall a. B\) only if A is a subtype of B, with the assumption a is a fresh variable. Rule SForallL says \(\forall a. A\) is a subtype of B if we can instantiate it with some \(\tau \) and show the result is a subtype of B. In rule SFun, we see that subtyping is contravariant on the argument type, and covariant on the return type.
Here we know that \(\mathsf {id}:\forall a. a \rightarrow a\) and also, from the application context, that \(\mathsf {id}\) is applied to an argument of type \(\mathsf {Int}\). Thus we need a mechanism for solving the instantiation \(a=\mathsf {Int}\) and return a supertype \(\mathsf {Int}\rightarrow \mathsf {Int}\) as the type of \(\mathsf {id}\). This is precisely what the application subtyping achieves: resolve instantiation constraints according to the application context. Notice that unlike existing works [14, 27], application subtyping provides a way to solve instantiation more locally, since it does not mutually depend on typing.
Back to the rules in Fig. 1, one way to understand the judgment Open image in new window from a computational pointofview is that the type B is a computed output, rather than an input. In other words B is determined from \(\varPsi \) and A. This is unlike the judgment Open image in new window , where both A and B would be computationally interpreted as inputs. Therefore it is not possible to view Open image in new window as a special case of Open image in new window where \(\varPsi \) is empty.
Our system does not need Inst, because in applications, type information flows from arguments to the function, instead of function to arguments. In the latter case, Inst is needed because a function type is wanted instead of a polymorphic type. In our approach, instantiation of type variables is avoided unless necessary.
The two remaining rules apply when the application context is nonempty, for polymorphic and function types respectively. Note that we only need to deal with these two cases because \(\mathsf {Int}\) or type variables a cannot have a nonempty application context. In rule SForall2, we instantiate the polymorphic type with some \(\tau \), and continue. This instantiation is forced by the application context. In rule SFun2, one function of type \(A \rightarrow B\) is now being applied to an argument of type C. So we check Open image in new window . Then we continue with B and the rest application context, and return \(C \rightarrow D\) as the result type of the function.
MetaTheory. Application subtyping is novel in our system, and it enjoys some interesting properties. For example, similarly to typing, the application context decides the form of the supertype.
Lemma 4
(\(\varPsi \) Coincides with Subtyping Results). If Open image in new window , then for some \(B'\), \(B = \varPsi \rightarrow B'\).
Therefore we can always use the judgment Open image in new window , instead of Open image in new window . Application subtyping is also reflexive and transitive. Interestingly, in those lemmas, if we remove all applications contexts, they are exactly the reflexivity and transitivity of traditional subtyping.
Lemma 5
(Reflexivity). Open image in new window .
Lemma 6
(Transitivity). If Open image in new window , and Open image in new window , then Open image in new window .
Finally, we can convert between subtyping and application subtyping. We can remove the application context and still get a subtyping relation:
Lemma 7
( Open image in new window to Open image in new window ). If Open image in new window , then Open image in new window .
Transferring from subtyping to application subtyping will result in a more general type.
Lemma 8
( Open image in new window to Open image in new window ). If Open image in new window , then for some \(B_2\), we have Open image in new window , and Open image in new window .
This lemma may not seem intuitive at first glance. Consider a concrete example Open image in new window , and Open image in new window . The former one, holds because we have Open image in new window in the return type. But in the latter one, after \(\mathsf {Int}\) is consumed from application context, we eventually reach SEmpty, which always returns the original type back.
3.4 Translation to System F, Coherence and TypeSafety
We translate the source language into a variant of System F that is also used in Peyton Jones et al. [27]. The translation is shown to be coherent and type safe. Due to space limitations, we only summarize the key aspects of the translation. Full details can be found in the supplementary materials of the paper.
In the translation, we use f to refer to the coercion function produced by the subtyping translation, and s to refer to the translated term in System F. We write \(\varGamma \vdash ^Fs : A\) to mean the term s has type A in System F.
Lemma 9
(Typing Soundness). If Open image in new window , then \(\varGamma \vdash ^Fs: A\).
However, there could be multiple targets corresponding to one expression due to the multiple choices for \(\tau \). To prove that the translation is coherent, we prove that all the translations for one expression have the same operational semantics. We write e for the expressions after type erasure since types are useless after type checking. Because multiple targets could have different number of coercion functions, we use \(\eta \)id equality [5] instead of syntactic equality, where two expressions are regarded as equivalent if they can turn into the same expression through \(\eta \)reduction or removal of redundant identity functions. We then prove that our translation actually generates a unique target:
Lemma 10
(Coherence). If Open image in new window , and Open image in new window , then Open image in new window .
3.5 Algorithmic System
Even though our specification is syntaxdirected, it does not directly lead to an algorithm, because there are still many guesses in the system, such as in rule TLam2. This subsection presents a brief introduction of the algorithm, which essentially follows the approach by Peyton Jones et al. [27]. Full details can be found in the supplementary materials.
Having the name supply and substitutions, the algorithmic system is a direct extension of the specification in Fig. 1, with a process to do unifications that solve meta type variables. Such unification process is quite standard and similar to the one used in the HindleyMilner system. We proved our algorithm is sound and complete with respect to the specification.
Theorem 1
(Soundness). If Open image in new window , then for any substitution V with \(dom(V) = \) fmv \((S_1 \varGamma , S_1 A)\), we have Open image in new window .
Theorem 2
(Completeness). If Open image in new window , then for a fresh \(N_0\), we have Open image in new window , and for some \(S_2\), we have Open image in new window .
4 More Expressive Type Applications
This section presents a SystemFlike calculus, which shows that the application mode not only does work well for calculi with explicit type applications, but it also adds interesting expressive power, while at the same time retaining uniqueness of types for explicitly polymorphic functions. One additional novelty in this section is to present another possible variant of typing and subtyping rules for the application mode, by exploiting the lemmas presented in Sects. 3.2 and 3.3.
4.1 Syntax
The syntax is mostly standard. Expressions include variables x, integers n, annotated abstractions \(\lambda x:A.~ s\), unannotated abstractions \(\lambda {x}.~ e\), applications \(e_1 ~ e_2\), type abstractions \(\varLambda a. s\), and type applications \(e_1 ~ [A]\). Types includes type variable a, integers \(\mathsf {Int}\), function types \(A \rightarrow B\), and polymorphic types \(\forall a. A\).
WellFormedness. The type wellformedness under typing contexts is given in Fig. 3, which is quite straightforward. Notice that there is no rule corresponding to type variables in type equations. For example, a is not a wellformed type under typing context \(a=\mathsf {Int}\), instead, \(\langle {a=\mathsf {Int}} \rangle a\) is. In other words, we keep the invariant: types are always fully substituted under the typing context.
4.2 Type System
We have \(B = \varPsi \rightarrow C\) for some C by Lemma 1. Instead of B, we can directly return C as the output type, since we can derive from the application context that e is of type \(\varPsi \rightarrow C\), and \(\lambda {x}.~ e\) is of type \((\varPsi , A) \rightarrow C\). Thus we obtain the TLamAlt rule.
Note that the choice of the style of the rules is only a matter of taste in the language in Sect. 3. However, it turns out to be very useful for our variant of System F, since it helps avoiding introducing types like \(\forall a = \mathsf {Int}. a\). Therefore, we adopt the new form of judgment. Now the judgment Open image in new window is interpreted as: under the typing context \(\varGamma \), and the application context \(\varPsi \), the return type of e applied to the arguments whose types are in \(\varPsi \) is A.
Typing Rules. Using the new interpretation of the typing judgment, we give the typing rules in the top of Fig. 4. SFVar depends on the subtyping rules. Rule SFInt always infers integer types. Rule SFLamAnn1 first applies current context on A, then puts \(x: \langle {\varGamma } \rangle A\) into the typing context to infer e. The return type is a function type because the application context is empty. Rule SFLamAnn2 has a nonempty application context, so it requests that the type at the top of the application context is equivalent to \(\langle {\varGamma } \rangle A\). The output type is B instead of a function type. Notice how the invariant that types are fully substituted under the typing context is preserved in these two rules.
Rule SFLam pops the type A from the application context, puts x : A into the typing context, and returns only the return type B. In rule SFApp, the argument type A is pushed into the application context for inferring \(e_1\), so the output type B is the type of \(e_1\) under application context (\(\varPsi , A\)), which is exactly the return type of \(e_1 ~ e_2\) under \(\varPsi \).
Rule SFTLam1 is for type abstractions. The type variable a is pushed into the typing context, and the return type is a polymorphic type. In rule SFTLam2, the application context has the type argument A at its top, which means the type abstraction is applied to A. We then put the type equation \(a = A\) into the typing context to infer e. Like termlevel applications, here we only return the type B instead of a polymorphic type. In rule SFTApp, we first apply the typing context on the type argument A, then we put the applied type argument \(\langle {\varGamma } \rangle A\) into the application context to infer e, and return B as the output type.
Subtyping. The definition of subtyping is given at the bottom of Fig. 4. As with the typing rules, the part of argument types corresponding to the application context is omitted in the output. We interpret the rule form Open image in new window as, under the application context \(\varPsi \), A is a subtype of the type whose type arguments are \(\varPsi \) and the return type is B.
Rule SFSEmpty returns the input type under the empty application context. Rule SFSTApp instantiates a with the type argument A, and returns C. Note how application subtyping can be extended naturally to deal with type applications. Rule SFSApp requests that the argument type is the same as the top type in the application context, and returns C.
4.3 Meta Theory
Applying the idea of the application mode to System F results in a wellbehaved type system. For example, subtyping transitivity becomes more concise:
Lemma 11
(Subtyping transitivity). If Open image in new window , and Open image in new window , then Open image in new window .
Also, we still have the interesting subsumption lemma that transfers from the inference mode to the application mode:
Lemma 12
(Subsumption). If Open image in new window , and Open image in new window , and Open image in new window , then Open image in new window .
Furthermore, we prove the type safety by proving the progress lemma and the preservation lemma. The detailed definitions of operational semantics and values can be found in the supplementary materials.
Lemma 13
(Progress). If Open image in new window , then either e is a value, or there exists \(e'\), such that \(e \longrightarrow e'\).
Lemma 14
(Preservation). If Open image in new window , and \(e \longrightarrow e'\), then Open image in new window .
Moreover, introducing type equality preserves unique types:
Lemma 15
(Uniqueness of typing). If Open image in new window , and Open image in new window , then \(A = B\).
5 Discussion
This section discusses possible design choices regarding bidirectional type checking with the application mode, and talks about possible future work.
5.1 Combining Application and Checked Modes
Although the application mode provides us with alternative design choices in a bidirectional type system, a checked mode can still be easily added. One motivation for the checked mode would be annotated expressions e : A, where the type of expressions is known and is therefore used to check expressions.
Here, e is checked using its annotation A, and then we instantiate A to B using subtyping with application context \(\varPsi \).
Note that adding expression annotations might bring convenience for programmers, since annotations can be more freely placed in a program. For example, Open image in new window becomes valid. However this does not add expressive power, since programs that are typeable under expression annotations, would remain typeable after moving the annotations to bindings. For example the previous program is equivalent to Open image in new window
This discussion is a sketch. We have not defined the corresponding declarative system nor algorithm. However we believe that the addition of a checked mode will not bring surprises to the metatheory.
5.2 Additional Constructs
In this section, we show that the application mode is compatible with other constructs, by discussing how to add support for pairs in the language given in Sect. 3. A similar methodology would apply to other constructs like sum types, data types, ifthenelse expressions and so on.
Note that another way to model those two rules would be to simply have an initial typing environment \(\Gamma _{initial} \equiv \mathbf {fst}: (\forall a b. (a, b) \rightarrow a), \mathbf {snd}: (\forall a b. (a, b) \rightarrow b)\). In this case the elimination of pairs be dealt directly by the rule for variables.
An extended version of the calculus presented in Sect. 3, which includes the rules for pairs (TPair, SPair, TFst2 and TSnd2), has been formally studied. All the theorems presented in Sect. 3 hold with the extension of pairs.
5.3 Dependent Type Systems
One remark about the application mode is that the same idea is possibly applicable to systems with advanced features, where type inference is sophisticated or even undecidable. One promising application is, for instance, dependent type systems [2, 3, 10, 21, 37]. Type systems with dependent types usually unify the syntax for terms and types, with a single lambda abstraction generalizing both type and lambda abstractions. Unfortunately, this means that the let desugar is not valid in those systems. As a concrete example, consider desugaring the expression \(\mathbf {let}\,{a} = {\mathsf {Int}}\, \mathbf {in} \,{\lambda x:a.~ {x + 1}}\) into Open image in new window \(\mathsf {Int}\), which is illtyped because the type of x in the abstraction body is a and not \(\mathsf {Int}\).
Because let cannot be encoded, declarations cannot be encoded either. Modeling declarations in dependently typed languages is a subtle matter, and normally requires some additional complexity [34].
6 Related Work
6.1 Bidirectional Type Checking
Bidirectional type checking was popularized by the work of Pierce and Turner [29]. It has since been applied to many type systems with advanced features. The alternative application mode introduced by us enables a variant of bidirectional type checking. There are many other efforts to refine bidirectional type checking.
Colored local type inference [25] refines local type inference for explicit polymorphism by propagating partial type information. Their work is built on distinguishing inherited types (known from the context) and synthesized types (inferred from terms). A similar distinction is achieved in our algorithm by manipulating type variables [14]. Also, their information flow is from functions to arguments, which is fundamentally different from the application mode.
The system of tridirectional type checking [15] is based on bidirectional type checking and has a rich set of property types including intersections, unions and quantified dependent types, but without parametric polymorphism. Tridirectional type checking has a new direction for supporting type checking unions and existential quantification. Their third mode is basically unrelated to our application mode, which propagates information from outer applications.
Greedy bidirectional polymorphism [13] adopts a greedy idea from Cardelli [4] on bidirectional type checking with higher ranked types, where the type variables in instantiations are determined by the first constraint. In this way, they support some uses of impredicative polymorphism. However, the greediness also makes many obvious programs rejected.
6.2 Type Inference for HigherRanked Types
As a reference, Fig. 5 [14, 20] gives a highlevel comparison between related works and our system.
Predicative Systems. Peyton Jones et al. [27] developed an approach for type inference for higher rank types using traditional bidirectional type checking based on Odersky and Läufer [24]. However in their system, in order to do instantiation on higher rank types, they are forced to have an additional type category (\(\rho \) types) as a special kind of higher rank type without toplevel quantifiers. This complicates their system since they need to have additional rule sets for such types. They also combine a variant of the containment relation from Mitchell [23] for deep skolemisation in subsumption rules, which we believe is compatible with our subtyping definition.
Impredicative Systems. \( ML^F \) [18, 19, 32] generalizes ML with firstclass polymorphism. \( ML^F \) introduces a new type of bounded quantification (either rigid or flexible) for polymorphic types so that instantiation of polymorphic bindings is delayed until a principal type is found. The HML system [20] is proposed as a simplification and restriction of \( ML^F \). HML only uses flexible types, which simplifies the type inference algorithm, but retains many interesting properties and features.
The FPH system [35] introduces boxy monotypes into System F types. One critique of boxy type inference is that the impredicativity is deeply hidden in the algorithmic type inference rules, which makes it hard to understand the interaction between its predicative constraints and impredicative instantiations [31].
6.3 Tracking Type Equalities
Tracking type equalities is useful in various situations. Here we discuss specifically two related cases where tracking equalities plays an important role.
Type Equalities in Type Checking. Tracking type equalities is one essential part for type checking algorithms involving Generalized Algebraic Data Types (GADTs) [6, 26, 33]. For example, Peyton Jones et al. [26] propose a type inference algorithm based on unification for GADTs, where type equalities only apply to userspecified types. However, reasoning about type equalities in GADTs is essentially different from the approach in Sect. 4: type equalities are introduced by pattern matches in GADTs, while they are introduced through type applications in our system. Also, type equalities in GADTs are local, in the sense different branches in pattern matches have different type equalities for the same type variable. In our system, a type equality is introduced globally and is never changed. However, we believe that they can be made compatible by distinguishing different kinds of equalities.
Equalities in Declarations. In systems supporting dependent types, type equalities can be introduced by declarations. In the variant of pure type systems proposed by Severi and Poll [34], expressions \(x = a :A~\mathbf {in}~b\) generate an equality \(x = a : A\) in the typing context, which can be fetched later through \(\delta \)reduction. However, \(\delta \)reduction rules require careful design, and the conversion rule of \(\delta \)reduction makes the type system nondeterministic. One potential usage of the application mode is to help reduce the complexity for introducing declarations in those type systems, as briefly discussed in Sect. 5.3.
7 Conclusion
We proposed a variant of bidirectional type checking with a new \(application \) mode, where type information flows from arguments to functions in applications. The application mode is essentially a generalization of the inference mode, can therefore work naturally with inference mode, and avoid the rule duplication that is often needed in traditional bidirectional type checking. The application mode can also be combined with the checked mode, but this often does not add expressiveness. Compared to traditional bidirectional type checking, the application mode opens a new path to the design of type inference/checking.
We have adopted the application mode in two type systems. Those two systems enjoy many interesting properties and features. However as bidirectional type checking can be applied to many type systems, we believe application mode is applicable to various type systems. One obvious potential future work is to investigate more systems where the application mode brings benefits. This includes systems with subtyping, intersection types [8, 30], static overloading, or dependent types.
Footnotes
 1.
All supplementary materials are available in https://bitbucket.org/ningningxie/letargumentsgofirst.
 2.
Although the application mode generalizes the inference mode, we refer to them as two different modes. Thus the variant of bidirectional type checking in this paper is interpreted as a type system with both inference and application modes.
Notes
Acknowledgements
We thank the anonymous reviewers for their helpful comments. This work has been sponsored by the Hong Kong Research Grant Council projects number 17210617 and 17258816.
References
 1.Abel, A.: Termination checking with types. RAIROTheor. Inform. Appl. 38(4), 277–319 (2004)MathSciNetCrossRefGoogle Scholar
 2.Abel, A., Coquand, T., Dybjer, P.: Verifying a semantic \({\beta \eta }\)conversion test for MartinLöf type theory. In: Audebaud, P., PaulinMohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 29–56. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540705949_4CrossRefGoogle Scholar
 3.Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: A bidirectional refinement algorithm for the calculus of (co) inductive constructions. Log. Meth. Comput. Sci. 8, 1–49 (2012)MathSciNetCrossRefGoogle Scholar
 4.Cardelli, L.: An implementation of FSub. Technical report, Research report 97. Digital Equipment Corporation Systems Research Center (1993)Google Scholar
 5.Chen, G.: Coercive subtyping for the calculus of constructions. In: POPL 2003 (2003)Google Scholar
 6.Cheney, J., Hinze, R.: Firstclass phantom types. Technical Report CUCIS TR20031901. Cornell University (2003)Google Scholar
 7.Chlipala, A., Petersen, L., Harper, R.: Strict bidirectional type checking. In: International Workshop on Types in Languages Design and Implementation (2005)Google Scholar
 8.Coppo, M., DezaniCiancaglini, M., Venneri, B.: Functional characters of solvable terms. Math. Log. Q. 27(2–6), 45–58 (1981)MathSciNetCrossRefGoogle Scholar
 9.Coq Development Team: The Coq proof assistant, Documentation, system download (2015)Google Scholar
 10.Coquand, T.: An algorithm for typechecking dependent types. Sci. Comput. Program. 26(1–3), 167–177 (1996)MathSciNetCrossRefGoogle Scholar
 11.Damas, L., Milner, R.: Principal typeschemes for functional programs. In: POPL 1982 (1982)Google Scholar
 12.Davies, R., Pfenning, F.: Intersection types and computational effects. In: ICFP 2000 (2000)Google Scholar
 13.Dunfield, J.: Greedy bidirectional polymorphism. In: Workshop on ML (2009)Google Scholar
 14.Dunfield, J., Krishnaswami, N.R.: Complete and easy bidirectional typechecking for higherrank polymorphism. In: ICFP 2013 (2013)Google Scholar
 15.Dunfield, J., Pfenning, F.: Tridirectional typechecking. In: POPL 2004 (2004)Google Scholar
 16.Girard, J.Y.: The system F of variable types, fifteen years later. Theor. Comput. Sci. 45, 159–192 (1986)MathSciNetCrossRefGoogle Scholar
 17.Hindley, J.R.: The principal typescheme of an object in combinatory logic. Trans. Am. Math. Soc. 146, 29–60 (1969)MathSciNetMATHGoogle Scholar
 18.Le Botlan, D., Rémy, D.: MLF: Raising ML to the power of system F. In: ICFP 2003 (2003)Google Scholar
 19.Le Botlan, D., Rémy, D.: Recasting MLF. Inform. Comput. 207(6), 726–785 (2009)MathSciNetCrossRefGoogle Scholar
 20.Leijen, D.: Flexible types: robust type inference for firstclass polymorphism. In: POPL 2009 (2009)CrossRefGoogle Scholar
 21.Löh, A., McBride, C., Swierstra, W.: A tutorial implementation of a dependently typed lambda calculus. Fundamenta informaticae 102(2), 177–207 (2010)MathSciNetMATHGoogle Scholar
 22.Lovas, W.: Refinement types for logical frameworks. Ph.D. thesis, Carnegie Mellon University (2010). AAI3456011Google Scholar
 23.Mitchell, J.C.: Polymorphic type inference and containment. Inform. Comput. 76(2–3), 211–249 (1988)MathSciNetCrossRefGoogle Scholar
 24.Odersky, M., Läufer, K.: Putting type annotations to work. In: POPL 1996 (1996)Google Scholar
 25.Odersky, M., Zenger, C., Zenger, M.: Colored local type inference. In: POPL 2001 (2001)Google Scholar
 26.Peyton Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unificationbased type inference for gadts. In: ICFP 2006 (2006)CrossRefGoogle Scholar
 27.Peyton Jones, S., Vytiniotis, D., Weirich, S., Shields, M.: Practical type inference for arbitraryrank types. J. Funct. Program. 17(01), 1–82 (2007)MathSciNetCrossRefGoogle Scholar
 28.Pientka, B.: A typetheoretic foundation for programming with higherorder abstract syntax and firstclass substitutions. In: POPL 2008 (2008)Google Scholar
 29.Pierce, B.C., Turner, D.N.: Local type inference. TOPLAS 22(1), 1–44 (2000)CrossRefGoogle Scholar
 30.Pottinger, G.: A type assignment for the strongly normalizable \(\lambda \)terms. In: To HB Curry: essays on combinatory logic, lambda calculus and formalism. pp. 561–577 (1980)Google Scholar
 31.Rémy, D.: Simple, partial typeinference for system F based on typecontainment. In: ICFP 2005 (2005)Google Scholar
 32.Rémy, D., Yakobowski, B.: From ML to MLF: graphic type constraints with efficient type inference. In: ICFP 2008 (2008)Google Scholar
 33.Schrijvers, T., Peyton Jones, S., Sulzmann, M., Vytiniotis, D.: Complete and decidable type inference for gadts. In: ICFP 2009 (2009)CrossRefGoogle Scholar
 34.Severi, P., Poll, E.: Pure type systems with definitions. In: Nerode, A., Matiyasevich, Y.V. (eds.) LFCS 1994. LNCS, vol. 813, pp. 316–328. Springer, Heidelberg (1994). https://doi.org/10.1007/3540581405_30CrossRefGoogle Scholar
 35.Vytiniotis, D., Weirich, S., Peyton Jones, S.: FPH: Firstclass polymorphism for haskell. In: ICFP 2008 (2008)Google Scholar
 36.Wells, J.B.: Typability and type checking in system F are equivalent and undecidable. Ann. Pure Appl. Log. 98(1–3), 111–156 (1999)MathSciNetCrossRefGoogle Scholar
 37.Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL 1999 (1999)Google Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.