Pith. sign in

REVIEW 3 major objections 4 minor 35 references

Bidirectional Typing

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Bidirectional typing—alternating checking and synthesis—is a broadly applicable design method that lets languages support undecidable inference features while keeping annotations light.

desk verdict A thorough, well-organized survey that will become a standard reference for bidirectional typing; the formal additions are modest and the abstract overclaims error locality, but it deserves serious refereeing. read the letter →

arxiv 1908.05839 v2 pith:NSP3WWHU submitted 2019-08-16 cs.PL cs.LO

Jana Dunfield , Neel Krishnaswami This is my paper · ORCID
classification cs.PLcs.LO MSC 68N1803B40
keywords bidirectionaltypingtypecheckingsynthesisinferencemode-correctnessPfenningrecipehigher-rankpolymorphisminformationflow
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Bidirectional typing alternates between type checking, where the type is a known input, and type synthesis, where the type is produced as output. This survey argues that the combination is a broadly applicable design method: checking lets a language support features such as dependent types, refinement types, and higher-rank polymorphism even when full inference is undecidable, while synthesis keeps the required annotations light. It distills four design criteria—mode-correctness, completeness (annotatability), rule size, and annotation character—and presents the Pfenning recipe as a reliable starting point for building such systems. It also argues that the essence of bidirectional typing is the management of information flow, not polarized logic, so the technique extends beyond focused proof calculi. A sympathetic reader should come away with a practical recipe and a research agenda, not just a catalogue.

What carries the argument

The load-bearing mechanism is the pair of typing judgments $\Gamma \vdash e \Leftarrow A$ and $\Gamma \vdash e \Rightarrow A$, together with a direction-switching subsumption rule $\Gamma \vdash e \Rightarrow A$ with $A = B$ yielding $\Gamma \vdash e \Leftarrow B$. The Pfenning recipe is the named design procedure that fixes the directions of every judgment: the principal judgment of an introduction rule checks, the principal judgment of an elimination rule synthesizes, and every other judgment checks whenever its type is already known from the inputs. This produces rules that are mode-correct, keeps the system small, guarantees a subformula property, and locates the need for annotations precisely at boundaries where an introduction form meets an elimination form.

What would settle it

A concrete counterexample would settle the thesis: a type system that the community regards as bidirectional but that uses only one judgment (or no mode-switch rule), or a polarized type theory that provably does not admit the two-judgment checking/synthesis structure. A sharper, more quantitative test is to prove whether every system meeting the two-judgment-plus-mode-switch definition is decidable; exhibiting one such system that is undecidable, or proving that all are decidable, would confirm or refute the survey's claim that this structure is the source of bidirectionality's practical power.

Watch

Extended reading notes

Core claim

The central claim is that bidirectional typing is best understood through its judgments: $\Gamma \vdash e \Leftarrow A$ means checking $e$ against a known type $A$, and $\Gamma \vdash e \Rightarrow A$ means synthesizing the type $A$ from $e$. The paper contends that a system built by following the Pfenning recipe—principal judgments of introduction rules check, principal judgments of elimination rules synthesize, and a subsumption rule switches between the two—satisfies the design criteria and, in particular, is always mode-correct and admits a predictable, local annotation discipline. The paper further claims that this is not the only viable structure: backwards bidirectional systems, in which the directions are reversed, and mixed-direction types, in which modes are tracked inside the type syntax, are also genuinely bidirectional. From these examples it concludes that bidirectionality does not arise from polarized logic or focusing, but from the deliberate choice of where type information flows.

Load-bearing premise

The survey's boundary and its main conceptual conclusion rest on an informal definition of bidirectionality as any system with two judgment forms, one checking and one synthesizing, linked by a mode-switch rule; if that definition is too broad or too narrow, the claim that polarized logic is not the essence collapses with it.

Editorial extensions

If this is right

  • A designer who follows the recipe gets a directly implementable type system: mode-correctness fixes a strategy, and syntax-directed rules avoid backtracking.
  • Features whose inference is undecidable—dependent types, refinement types, higher-rank polymorphism—become decidable to check, at the cost of annotations whose placement is locally determined.
  • The subformula property confines risky connectives (unknown types in gradual typing, evaluation-order connectives) to places the programmer explicitly requests.
  • The classification of backwards and mixed-direction systems as bidirectional reframes the design space: the field is defined by information-flow structure, not by adherence to the recipe or by polarization.
  • Proofs of annotatability become a routine induction over type-assignment derivations, with the only nontrivial case being the conversion of a checking derivation into a synthesizing one by adding an annotation.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If information-flow structure is the true essence, then a formal mode calculus describing such flows could unify the surveyed systems and predict when a new two-judgment design will be decidable; the survey itself leaves this as an informal observation.
  • The recipe's correction about variable-binding eliminations suggests a testable conjecture: the annotations required by a bidirectional system are exactly those placed at boundaries where a commuting conversion would otherwise be needed, which could be checked against the surveyed counterexamples.
  • Applying the same two-judgment design to program synthesis (where the term is the output) parallels the survey's mode analysis and could yield a symmetric theory of annotation-light synthesis, a direction the paper only touches on.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The manuscript is a survey of bidirectional typing, presenting the two-judgment checking/synthesis paradigm, design criteria for bidirectional systems, a 'Pfenning recipe' for constructing them, a catalogue of variants (mixed-direction types, backwards bidirectional typing, mode annotations, simultaneous input/output judgments), connections to proof theory and polarized type theory, and historical notes. It argues that bidirectional typing is essentially about managing information flow rather than being a manifestation of polarized logic, and it concludes with open challenges for the field. The paper contains worked examples, several proof sketches (notably annotatability in Section 4.5.3 and a backwards substitution theorem in Section 6.5), and a systematic normalization of notation.

Significance. If its central claims hold, this survey will be a valuable reference for language designers and type theorists. It collects and organizes a large body of work, gives explicit design criteria (mode-correctness, annotatability, rule size, annotation character), and offers a concrete recipe with a falsifiable annotation-character claim. The historical treatment is careful, and the normalized notation across systems is genuinely useful. The manuscript does not ship machine-checked proofs or executable artifacts; the proof sketches are mostly adequate for a survey, but the strongest conceptual claim about polarity is currently under-supported. The paper's main value is as a synthesis and design guide, and its central methodological claims are defensible once appropriately qualified.

major comments (3)
  1. [Section 8.4 and Section 12] The claim that the 'essence of bidirectional typing is the management of information flow' and that the folklore belief in a polarized-logic origin is 'wrong' is not supported by a checkable criterion. The argument classifies the systems of Odersky et al. (Section 6.1), Chlipala et al. (Section 6.5.1), and Zeilberger (Section 6.5) as 'undeniably bidirectional' and outside the Pfenning-recipe/polarity narrative, but the paper gives no formal definition of 'bidirectional' and no criterion for 'arises from polarized logic.' Each of the three exemplars is consistent with a polarized or focused reading: Zeilberger's system is a fragment of multiplicative linear logic, the canonical setting for polarity; Chlipala et al. explicitly draw on relevance logic; Odersky et al.'s inherited/synthesized decorations behave like polarity tags. As written, the conclusion reduces to a definitional preference rather than a supported empirical or mathematical discovery. I request either a precise delimitation of the surveyed class together with a theorem or counterexample showing that it is not faithfully presentable as a polarized/focused calculus, or a softening of the conclusion to 'not necessarily a manifestation of polarized logic.'
  2. [Abstract, Section 3.4, and Section 10] The abstract advertises that 'bidirectional typing improves error locality,' but the manuscript offers no empirical evidence for this causal claim. Section 3.4 explicitly states that 'in the absence of empirical studies' the annotation-discipline claims are hypotheses, and the historical note on Lee and Yi in Section 10 is anecdotal. Because this benefit is advertised in the abstract and used as motivation, it is load-bearing. Either report supporting evidence or hedge the abstract and the relevant passages to say that bidirectional typing 'can improve' or 'is often observed to improve' error locality.
  3. [Section 4.5.4] The claim that under the recipe 'an annotation is required on a subterm if and only if an introduction form meets an elimination form' is not a precise or verifiable statement as written. No syntactic definition of 'meets' is given, and the examples include cases in which an elimination form (a case expression) must be annotated because it cannot synthesize, even though no introduction form directly meets an elimination form at that node. Section 4.1 also documents that the earlier 'redex-only' version of this claim was false. Please either formalize the criterion or present it as a heuristic with explicit exceptions.
minor comments (4)
  1. [Section 6.5, Theorem 1] The backwards substitution theorem is stated but no proof or citation is given for it; either supply a proof sketch or attribute the theorem explicitly to a source.
  2. [Section 9.1] There is a typo: 'bidrectional' should be 'bidirectional.'
  3. [Byline] The second author's name appears as 'NEEL KRISHNASW AMI' with an erroneous space; it should be 'NEEL KRISHNASWAMI.'
  4. [Section 4.5.3] The annotatability proof is described as an induction, but only the two 'into the wind' cases are shown; a sentence summarizing the straightforward cases would make the sketch complete.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the survey's claims are descriptive and historically grounded, not derived from its own conclusions.

full rationale

The paper is a survey and does not present a derivation chain in which a prediction reduces to an input. The central recipe in Section 4 is explicitly attributed to Pfenning via Dunfield and Pfenning [2004], and the paper states 'the recipe was invented by Frank Pfenning, so we call it the Pfenning recipe.' The survey's own prior work (Dunfield and Krishnaswami 2013, 2019) is cited as examples of bidirectional systems, but the load-bearing conceptual claims do not depend on accepting those self-citations as unverified premises. The Section 8.4 claim that 'the essence of bidirectional typing is the management of information flow' is an interpretive conclusion supported by named external systems (Odersky et al. 2001, Chlipala et al. 2005, Zeilberger 2015), not by a fitted parameter or by a self-cited uniqueness theorem. The informal classification of those systems as 'undeniably bidirectional' is contestable and under-supported, but under-support is a correctness concern, not circularity: no equation in the paper is equivalent by construction to an input, and no fitted quantity is renamed as a prediction. The paper is accordingly self-contained as a survey, and no circular step can be exhibited with a specific reduction.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper is a survey, so it mainly relies on standard type theory and design heuristics. There are no numerical fits or invented entities. The most fragile assumptions are the informal definition of bidirectionality and the unsupported empirical claim about error locality.

assumptions (4)
  • domain assumption Standard type assignment systems, such as the simply typed lambda calculus, are the ground truth against which bidirectional systems are measured.
    Section 4.5.2 says the type assignment system is our ground truth; the recipe and annotatability proofs assume this reference semantics.
  • domain assumption Mode-correctness in the logic-programming sense is necessary for a bidirectional type system to be implementable.
    Section 3.1 states that a non-mode-correct system cannot be directly implemented; this is a design principle, not a proved theorem.
  • domain assumption Bidirectional typing improves error locality.
    The abstract asserts this; Section 3.4 admits there are no empirical studies comparing annotation disciplines, and Section 10 only cites indirect evidence from Algorithm M.
  • domain assumption The subformula property is preserved by recipe-based bidirectional systems.
    Section 7.1 argues this informally; the argument covers the recipe but notes exceptions when synthesis rules are added for literals and constants.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Bidirectional Typing." pith.science (2026). https://pith.science/paper/NSP3WWHU

@misc{pith2026190805839,
  author       = {Pith},
  title        = {Pith review of: Bidirectional Typing},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/NSP3WWHU}},
  note         = {Machine review of arXiv:1908.05839}
}
read the original 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.

Figures

Figures reproduced from arXiv: 1908.05839 by the authors.

Figure 1
Figure 1. A simply typed 𝜆-calculus (: judgment) and a bidirectional version (⇒ and ⇐ judgments) (3) Unit introduction unitI 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) Arrow introduction →I checks. This decision is better motivated: to synthesize 𝐴1 → 𝐴2 for 𝜆𝑥. 𝑒 we would … view at source ↗
Figure 2
Figure 2. A bidirectional type system characterizing [PITH_FULL_IMAGE:figures/full_fig_p026_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

35 extracted references · 30 canonical work pages

  1. [20]

    Lecture notes for 15–317: Constructive Logic, Carnegie Mellon University

    Lecture Notes on Harmony. Lecture notes for 15–317: Constructive Logic, Carnegie Mellon University. (Sept. 2009). www.cs.cmu.edu/∼fp/courses/15317-f09/lectures/03-harmony.pdf. Frank Pfenning

    work page 2009

  2. [21]

    Lecture notes for 15–317: Constructive Logic, Carnegie Mellon University

    Lecture Notes on Verifications. Lecture notes for 15–317: Constructive Logic, Carnegie Mellon University. (Sept. 2017). www.cs.cmu.edu/∼crary/317-f18/lectures/05-intercalation.pdf. Frank Pfenning and Rowan Davies

    work page 2017

  3. [23]

    An insider’s look at LF type reconstruction: everything you (n)ever wanted to know. J. Functional Programming 23, 1 (2013), 1–37. https://doi.org/10.1017/S0956796812000408 Brigitte Pientka and Jana Dunfield

    doi:10.1017/s0956796812000408 2013

  4. [26]

    In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 , Giuseppe Castagna and Andrew D

    Deciding equivalence with sums and the empty type. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 , Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 374–386. http://dl.acm.org/citation.cfm?id=3009901 Gabriel Scherer and Andreas Abel

    work page 2017

  5. [30]

    Robert J

    Normal Natural Deduction Proofs (in classical logic).Studia Logica 60, 1 (1998), 67–106. Robert J. Simmons

    work page 1998

  6. [31]

    ACM Trans

    Structural Focalization. ACM Trans. Comput. Logic 15, 3 (Sept. 2014). Vilhelm Sjöberg and Stephanie Weirich

    work page 2014

  7. [34]

    In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18)

    A Theory of Linear Typings As Flows on 3-valent Graphs. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18) . ACM, New York, NY, USA, 919–928. https://doi.org/ 10.1145/3209108.3209121 Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

    arXiv

  8. [35]

    A Mechanical Formalization of Higher-ranked Polymorphic Type Inference. Proc. ACM Program. Lang.3, ICFP, Article 112 (July 2019), 29 pages.https://doi.org/10.1145/3341716 , Vol. 1, No. 1, Article . Publication date: November 2020

    work page doi:10.1145/3341716 2019

Show all 35 references
  1. [242]

    https://doi

    Springer, 136–175. https://doi. org/10.1007/3-540-17184-3_44 Oukseh Lee and Kwangkeun Yi

    doi

  2. [1969]

    The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc. 146 (1969), 29–60. Haruo Hosoya and Benjamin C. Pierce

    1969

  3. [1978]

    A theory of type polymorphism in programming. J. Computer and System Sciences 17, 3 (1978), 348–375. , Vol. 1, No. 1, Article . Publication date: November

    1978

  4. [1983]

    Journal of Symbolic Logic 48, 4 (1983), 931–940

    A Filter Lambda Model and the Completeness of Type Assignment. Journal of Symbolic Logic 48, 4 (1983), 931–940. Luca Cardelli

    1983

  5. [1985]

    Cartesian Closed Categories and Typed Lambda- calculi. InCombinators and Functional Programming Languages, Thirteenth Spring School of the LITP, Val d’Ajol, France, May 6-10, 1985, Proceedings (Lecture Notes in Computer Science), Guy Cousineau, Pierre-Louis Curien, and Bernard...

    1985

  6. [1986]

    Theoretical Computer Science 44, 0 (1986), 51–68

    Typing and computational properties of lambda expressions. Theoretical Computer Science 44, 0 (1986), 51–68. Paul Blain Levy

    1986

  7. [1988]

    Technical Report CMU-CS-88-159

    Preliminary Design of the programming language Forsythe . Technical Report CMU-CS-88-159. Carnegie Mellon University. http://doi.library.cmu.edu/10.1184/OCLC/18612825. John C. Reynolds

  8. [1994]

    ACM Trans

    A Behavioral Notion of Subtyping. ACM Trans. Prog. Lang. Sys. 16, 6 (Nov. 1994), 1811–1841. Conor McBride

    1994

  9. [1996]

    Science of Computer Programming 26, 1–3 (1996), 167–177

    An Algorithm for Type-Checking Dependent Types. Science of Computer Programming 26, 1–3 (1996), 167–177. Luis Damas and Robin Milner

    1996

  10. [1998]

    ACM Trans

    Proofs about a Folklore Let-Polymorphic Type Inference Algorithm. ACM Trans. Prog. Lang. Sys. 20, 4 (July 1998), 707–723. Daniel Leivant

    1998

  11. [2000]

    ACM Trans

    Local Type Inference. ACM Trans. Prog. Lang. Sys. 22 (2000), 1–44. Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama

    2000

  12. [2001]

    Mathematical Structures in Computer Science 11, 4 (2001), 511–540

    A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science 11, 4 (2001), 511–540. Frank Pfenning and Robert J. Simmons

    2001

  13. [2003]

    A Linear Spine Calculus. J. Logic and Computation 13, 5 (2003), 639–688. Adam Chlipala, Leaf Petersen, and Robert Harper

    2003

  14. [2004]

    Lecture notes for 15–317: Constructive Logic, Carnegie Mellon University

    Sequent Calculus. Lecture notes for 15–317: Constructive Logic, Carnegie Mellon University. (Jan. 2004). www.cs.cmu.edu/∼fp/courses/atp/handouts/ch3-seqcalc.pdf. Frank Pfenning

    2004

  15. [2006]

    In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’06)

    Boxy Types: Inference for Higher-rank Types and Impredicativity. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’06). ACM, New York, NY, USA, 251–262. https://doi.org/10.1145/1159803.1159838 David H. D. Warren

  16. [2007]

    Practical type inference for arbitrary- rank types. J. Functional Programming 17, 1 (2007), 1–82. Frank Pfenning

    2007

  17. [2008]

    ACM Trans

    Contextual Modal Type Theory. ACM Trans. Comput. Logic 9, 3, Article 23 (June 2008), 49 pages. Martin Odersky, Matthias Zenger, and Christoph Zenger

    2008

  18. [2009]

    In Proceedings of the 36th Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL ’09)

    Focusing on pattern matching. In Proceedings of the 36th Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL ’09) . ACM, New York, NY, USA, 366–378. https: //doi.org/10.1145/1480881.1480927 Joachim Lambek

  19. [2011]

    OutsideIn(X): Modular type inference with local assumptions. J. Functional Programming 21, 4–5 (2011), 333–412. Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones

    2011

  20. [2012]

    Logical Methods in Computer Science 8 (2012)

    On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8 (2012). Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis

    2012

  21. [2013]

    Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism. In ICFP. ACM Press. arXiv: 1306.6032 [cs.PL] . Jana Dunfield and Neelakantan R. Krishnaswami

    arXiv

  22. [2014]

    Elaborating intersection and union types. J. Functional Programming 24, 2–3 (2014), 133–165. Jana Dunfield

    2014

  23. [2015]

    Elaborating Evaluation-Order Polymorphism. In ICFP. ACM Press. arXiv: 1504.07680 [cs.PL] . Jana Dunfield and Neelakantan R. Krishnaswami

    arXiv

  24. [2017]

    Electronic Notes in Theoretical Computer Science 332 (2017), 149–168

    The Polarized𝜆-calculus. Electronic Notes in Theoretical Computer Science 332 (2017), 149–168. 11th Workshop on Logical and Semantic Frameworks with Applications (LSFA). Tim Freeman and Frank Pfenning

    2017

  25. [2018]

    https://doi.org/10.1145/3192366.3192389 Wilfried Sieg and John Byrnes

    ACM, New York, NY, USA, 783–796. https://doi.org/10.1145/3192366.3192389 Wilfried Sieg and John Byrnes

  26. [2019]

    PACMPL POPL (Jan

    Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types. PACMPL POPL (Jan. 2019). arXiv: 1601.05106 [cs.PL] . Jana Dunfield and Frank Pfenning

    2019 arXiv

  27. [2020]

    A Quick Look at Impredicativity. Proc. ACM Program. Lang. 4, ICFP, Article 89 (2020). https://doi.org/10.1145/3408971 Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones

    2020 doi

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.