nLab bidirectional typechecking

Redirected from "bidirectional type checking".
Bidirectional typechecking

Bidirectional typechecking

Idea

Bidirectional typechecking is both a style of mathematical presentation of a type theory and a kind of algorithm for implementing one. The idea is that the basic judgment t:At:A that a term tt belongs to a type AA is split into two judgments:

  • tAt \Leftarrow A: the term tt can be checked to have the type AA.
  • tAt \Rightarrow A: from the term tt we can infer, or synthesize, the type AA that it has.

The difference is that in tAt\Leftarrow A we regard both tt and AA as “given” or “inputs”, whereas in tAt\Rightarrow A we regard only tt as an “input” and AA as an “output” that is “computed” from tt. When presented as a pure deductive system, these “input/output modes” do not mean anything, but when implemented as an algorithm they mean that we have two mutually recursive functions:

  • check(t,A)check(t,A) which simply succeeds or fails.
  • infer(t)infer(t) which either returns a type AA or fails.

See logic programming.

For example, from an un-annotated λ\lambda-abstraction such as the identity function λx.x\lambda x.x we cannot infer its type: the variable xx, and hence the result, could have any type. But we can check that it has any given endomorphism type: (λx.x)(AA)(\lambda x.x) \Leftarrow (A\to A) for any type AA. On the other hand, if we can infer a type for the function ff, i.e. f(AB)f\Rightarrow (A\to B) (for instance, ff could be a variable, since variables are declared with their types), and we can check that an argument aa has type AA (that is, aAa\Leftarrow A), then we can also infer that the application f(a)f(a) has type BB, that is f(a)Bf(a) \Rightarrow B. These observations correspond to bidirectional refinements of the usual typing rules for abstractions and applications:

Γ,x:AMBΓ(λx.M)(AB)Γf(AB)ΓaAΓf(a)B. \frac{\Gamma,x:A \vdash M \Leftarrow B}{\Gamma\vdash (\lambda x.M) \Leftarrow (A\to B)} \qquad \frac{\Gamma\vdash f \Rightarrow (A\to B) \qquad \Gamma\vdash a \Leftarrow A }{\Gamma \vdash f(a) \Rightarrow B}.

Bidirectional typechecking is closely related to “canonical forms only” presentations of type theories (such as logical frameworks) that involve hereditary substitution?. For instance, because we infer a type for an application f(a)f(a) by inferring a type for ff, but we can only check the type of an un-annotated abstraction λx.M\lambda x.M, an un-augmented bidirectional theory cannot typecheck a β\beta-redex (see beta-reduction (λx.M)(a)(\lambda x.M)(a). Thus it is a natural system in which to describe a type theory in which only canonical forms (no redexes) exist. But it is also easy to augment a bidirectional system with type ascription?, which mediates between the two modes and allows typechecking redexes: if we can check tAt\Leftarrow A, then we can infer the same type of the ascribed term (t:A)A(t:A)\Rightarrow A, allowing a redex to be written as (λx.M:AB)(a)(\lambda x.M : A\to B)(a).

Remark

There are many different notations used in the literature for the bidirectional typing judgments. Sometimes one finds tAt\rightrightarrows A and tAt\leftleftarrows A in place of our tAt\Rightarrow A and tAt\Leftarrow A. Other times the order of the term and the type is reversed, for instance writing tAt\in A for inferring and AtA\ni t for checking. Sometimes upwards and downwards-pointing arrows are used instead of leftwards and rightwards ones (e.g. tAt \uparrow A and tAt \downarrow A, or maybe t: At :^\uparrow A and t: At :^\downarrow A or a dozen other variants) — but unfortunately there is no consensus on which judgment points up and which points down! It seems to be somewhat more common for checking to point up and inference to point down, as this matches the direction that “information flows through the derivation tree”, but the opposite convention is found in plenty of papers too. (It could be that there is a “modern” consensus that only older papers violate.)

References

General

  • Jana Dunfield, Neel Krishnaswami, Bidirectional Typing (Survey), 2019, (pdf)

  • Pierce, B. C., Turner, D. N.: Local Type Inference, ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), San Diego, California, 1998, Full version in ACM Transactions on Programming Languages and Systems (TOPLAS), 22(1), January 2000, pp. 1–44, (pdf). This is usually cited as the “original” paper on bidirectional typechecking.

  • Frank Pfenning, Lecture Notes on Bidirectional Type Checking, pdf

  • Conor McBride, Basics of bidirectionality, blog post

  • David Christiansen, Bidirectional typing rules: a tutorial, pdf

For dependent types

  • Thierry Coquand, An algorithm for type-checking dependent types, 1996, pdf

  • Thierry Coquand and Makoto Takeyama, An Implementation of Type:Type, 2002, springerlink

  • Ulf Norell, Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology and Göteborg University, 2007. web

  • Andreas Abel, Thierry Coquand, Peter Dybjer Verifying a Semantic βη\beta\eta-Conversion Test for Martin-Löf Type Theory (extended version), 2008 semantic scholar (includes pdf)

  • Andreas Abel and Thorsten Altenkirch, A partial type checking algorithm for Type:TypeType:Type, 2008, pdf

  • Andres Löh, Conor McBride and Wouter Swierstra, A Tutorial Implementation of a Dependently Typed Lambda Calculus, 2009, web (includes Haskell code)

  • Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. A bi-directional refinement algorithm for the calculus of (co)inductive constructions, 2012, arxiv

  • Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University, 2002. Revised May 2003, pdf

Other type theories

  • Rowan Davies and Frank Pfenning. Intersection types and computational effects. In P. Wadler, editor, Proceedings of the Fifth International Conference on Functional Programming (ICFP’00), pages 198-208, Montreal, Canada, September 2000. ACM Press. pdf

  • Jana Dunfield and Frank Pfenning. Tridirectional typechecking. In X.Leroy, editor, Conference Record of the 31st Annual Symposium on Principles of Programming Languages (POPL’04), pages 281-292, Venice, Italy, January 2004. ACM Press. Extended version available as Technical Report CMU-CS-04-117, March 2004. pdf

  • Jana Dunfield, Neelakantan R. Krishnaswami, Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism, 2013, arxiv

  • Francisco Ferreira and Brigitte Pientka, Bidirectional Elaboration of Dependently Typed Programs, 2014, pdf. Despite the name, this paper is not about full dependent type theory but only has one level of dependency.

  • Jana Dunfield, Neelakantan R. Krishnaswami, Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types, 2016, arxiv

Last revised on June 4, 2021 at 10:21:20. See the history of this page for a list of all contributions to it.