research-article

Open access

Bidirectional Typing

Authors:

Neel KrishnaswamiAuthors Info & Claims

ACM Computing Surveys (CSUR), Volume 54, Issue 5

Article No.: 98, Pages 1 - 38

https://doi.org/10.1145/3450952

Published: 25 May 2021 Publication History

All formats PDF

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.

References

[1]

João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. 2017. Disjoint polymorphism. In Proceedings of the European Symposium on Programming. Springer, 1--28.

Digital Library

[2]

Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, and N. Oury. 2010. ΠΣ: Dependent types without the sugar. In Proceedings of the International Symposium on Functional and Logic Programming (FLOPS’10). Springer, 40--55.

[3]

Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983. A filter lambda model and the completeness of type assignment. J. Symbol. Logic 48, 4 (1983), 931--940.

[4]

Luca Cardelli. 1993. An Implementation of . Research report 97. DEC/Compaq Systems Research Center.

[5]

Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, and Deepak Garg. 2019. Bidirectional type checking for relational properties. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI’19). ACM Press, 533--547.

[6]

Iliano Cervesato and Frank Pfenning. 2003. A linear spine calculus. J. Logic Comput. 13, 5 (2003), 639--688.

[7]

Adam Chlipala, Leaf Petersen, and Robert Harper. 2005. Strict bidirectional type checking. In Proceedings of the Workshop on Types in Language Design and Implementation (TLDI ’05). ACM Press, 71--78.

Digital Library

[8]

Thierry Coquand. 1996. An algorithm for type-checking dependent types. Sci. Comput. Program. 26, 1--3 (1996), 167--177.

Digital Library

[9]

Luis Damas and Robin Milner. 1982. Principal type-schemes for functional programs. In Proceedings of the Symposium on Principles of Programming Languages (POPL’82). ACM, 207--212.

Digital Library

[10]

Rowan Davies. 2005. Practical Refinement-Type Checking. Ph.D. Dissertation. Carnegie Mellon University. CMU-CS-05-110.

Digital Library

[11]

Rowan Davies and Frank Pfenning. 2000. Intersection types and computational effects. In Proceedings of the International Conference on Functional Programming (ICFP’00). ACM Press, 198--208.

Digital Library

[12]

Stephen Dolan. 2016. Algebraic Subtyping. Ph.D. Dissertation. University of Cambridge.

[13]

Jana Dunfield. 2007. A Unified System of Type Refinements. Ph.D. Dissertation. Carnegie Mellon University. CMU-CS-07-129.

[14]

Jana Dunfield. 2009. Greedy bidirectional polymorphism. In Proceedings of the Machine Learning Workshop (ML’09). ACM Press, 15--26. Retrieved from http://research.cs.queensu.ca/~jana/papers/poly/.

Digital Library

[15]

Jana Dunfield. 2012. Elaborating intersection and union types. In Proceedings of the International Conference on Functional Programming (ICFP’12). ACM Press, 17--28.

Digital Library

[16]

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

[17]

Jana Dunfield. 2015. Elaborating evaluation-order polymorphism. In Proceedings of the International Conference on Functional Programming (ICFP’15). ACM Press, 256--268. arXiv:1504.07680 [cs.PL].

Digital Library

[18]

Jana Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and easy bidirectional typechecking for higher-rank polymorphism. In Proceedings of the International Conference on Functional Programming (ICFP’13). ACM Press, 429--442. arXiv:1306.6032 [cs.PL].

Digital Library

[19]

Jana Dunfield and Neelakantan R. Krishnaswami. 2019. Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types. Proc. ACM Program. Lang. 3, Article 9 (Jan. 2019), 28 pages. arXiv:1601.05106 [cs.PL].

Digital Library

[20]

Jana Dunfield and Frank Pfenning. 2004. Tridirectional typechecking. In Proceedings of the Symposium on Principles of Programming Languages (POPL’04). ACM Press, 281--292.

Digital Library

[21]

Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed. 2016. Visible type application. In Proceedings of the European Symposium on Programming, Vol. 9632. Springer, 229--254.

Digital Library

[22]

José Espírito Santo. 2017. The polarized λ-calculus. Electronic Notes Theor. Comput. Sci. 332 (2017), 149--168.

[23]

Tim Freeman and Frank Pfenning. 1991. Refinement types for ML. In Programming Language Design and Implementation. ACM Press, 268--277.

[24]

Jean-Yves Girard. 1989. Proofs and Types. Cambridge University Press.

[25]

Adam Gundry, Conor McBride, and James McKinna. 2010. Type inference in context. In Proceedings of the Conference on Mathematically Structured Functional Programming (MSFP’10).

Digital Library

[26]

Robert Harper and Frank Pfenning. 2005. On equivalence and canonical forms in the LF type theory. Trans. Comput. Logic 6 (2005), 61--101. Issue 1.

Digital Library

[27]

R. Hindley. 1969. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc. 146 (1969), 29--60.

[28]

Haruo Hosoya and Benjamin C. Pierce. 1999. How Good is Local Type Inference?Technical Report MS-CIS-99-17. University of Pennsylvania.

[29]

Danko Ilik. 2017. The exp-log normal form of types: Decomposing extensional equality and representing terms compactly. In Proceedings of the Symposium on Principles of Programming Languages (POPL’17). ACM Press, 387--399.

Digital Library

[30]

Khurram A. Jafery and Jana Dunfield. 2017. Sums of uncertainty: Refinements go gradual. In Proceedings of the Symposium on Principles of Programming Languages (POPL’17). ACM Press, 804--817.

[31]

Trevor Jim. 1995. What are Principal Typings and What are They Good For?Technical memorandum MIT/LCS/TM-532. MIT.

[32]

Neelakantan R. Krishnaswami. 2009. Focusing on pattern matching. In Proceedings of the Symposium on Principles of Programming Languages (POPL’09). ACM Press, 366--378.

Digital Library

[33]

Joachim Lambek. 1985. Cartesian closed categories and typed lambda-calculi. In Proceedings of the 13th Spring School of the LITP on Combinators and Functional Programming Languages(LNCS, Vol. 242), Guy Cousineau, Pierre-Louis Curien, and Bernard Robinet (Eds.). Springer, 136--175.

[34]

Oukseh Lee and Kwangkeun Yi. 1998. Proofs about a Folklore let-polymorphic type inference algorithm. ACM Trans. Prog. Lang. Sys. 20, 4 (July 1998), 707--723.

Digital Library

[35]

Daniel Leivant. 1986. Typing and computational properties of lambda expressions. Theor. Comput. Sci. 44 (1986), 51--68.

Digital Library

[36]

Paul Blain Levy. 2001. Call-By-Push-Value. Ph.D. Dissertation. Queen Mary and Westfield College, University of London.

[37]

Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do be do be do. In Proceedings of the Symposium on Principles of Programming Languages (POPL’17). ACM Press, 500--514.

Digital Library

[38]

Barbara H. Liskov and Jeannette M. Wing. 1994. A behavioral notion of subtyping. ACM Trans. Prog. Lang. Sys. 16, 6 (Nov. 1994), 1811--1841.

Digital Library

[39]

Conor McBride. 2016. I got plenty o’ nuttin’. In A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, S. Lindley, C. McBride, P. Trinder, and D. Sannella (Eds.). Springer, 207--233.

[40]

Robin Milner. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 3 (1978), 348--375.

[41]

Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual modal type theory. ACM Trans. Comput. Logic 9, 3, Article 23(June 2008), 49 pages.

Digital Library

[42]

Martin Odersky, Matthias Zenger, and Christoph Zenger. 2001. Colored local type inference. In Proceedings of the Symposium on Principles of Programming Languages (POPL’01). ACM Press, 41--53.

Digital Library

[43]

Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. 2016. Disjoint intersection types. In Proceedings of the International Conference on Functional Programming (ICFP’16). ACM Press, 364--377.

Digital Library

[44]

Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical type inference for arbitrary-rank types. J. Function. Program. 17, 1 (2007), 1--82.

Digital Library

[45]

Frank Pfenning. 2004. Sequent Calculus. Lecture notes for 15--317: Constructive Logic, Carnegie Mellon University. Retrieved from https://www.cs.cmu.edu/fp/courses/atp/handouts/ch3-seqcalc.pdf.

[46]

Frank Pfenning. 2009. Lecture Notes on Harmony. Lecture notes for 15--317: Constructive Logic, Carnegie Mellon University. Retrieved from https://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/03-harmony.pdf.

[47]

Frank Pfenning. 2017. Lecture Notes on Verifications. Lecture notes for 15--317: Constructive Logic, Carnegie Mellon University. Retrieved from https://www.cs.cmu.edu/~crary/317-f18/lectures/05-intercalation.pdf.

[48]

Frank Pfenning and Rowan Davies. 2001. A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci. 11, 4 (2001), 511--540.

Digital Library

[49]

Frank Pfenning and Robert J. Simmons. 2009. Substructural operational semantics as ordered logic programming. In Proceedings of the Symposium on Logic in Computer Science (LICS’09). IEEE, 101--110.

Digital Library

[50]

Brigitte Pientka. 2008. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In Proceedings of the Symposium on Principles of Programming Languages (POPL’08). ACM Press, 371--382.

Digital Library

[51]

Brigitte Pientka. 2013. An insider’s look at LF type reconstruction: Everything you (n)ever wanted to know. J. Function. Program. 23, 1 (2013), 1--37.

Digital Library

[52]

Brigitte Pientka and Jana Dunfield. 2008. Programming with proofs and explicit contexts. In Proceedings of the Conference on Principles and Practice of Declarative Programming (PPDP’08). ACM Press, 163--173.

Digital Library

[53]

Benjamin C. Pierce and David N. Turner. 1997. Local type inference. Technical Report CSCI #493. Indiana University.

[54]

Benjamin C. Pierce and David N. Turner. 1998. Local type inference. In Proceedings of the Symposium on Principles of Programming Languages (POPL’98). ACM Press, 252--265. Full version in ACM Trans. Prog. Lang. Sys., 22(1):1--44, 2000.

[55]

Benjamin C. Pierce and David N. Turner. 2000. Local type inference. ACM Trans. Prog. Lang. Sys. 22 (2000), 1--44.

Digital Library

[56]

Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program synthesis from polymorphic refinement types. In Programming Language Design and Implementation. ACM Press, 522--538.

[57]

François Pottier and Yann Régis-Gianas. 2006. Stratified type inference for generalized algebraic data types. In Proceedings of the Symposium on Principles of Programming Languages (POPL’06). ACM Press, 232--244.

Digital Library

[58]

Uday S. Reddy. 1993. A typed foundation for directional logic programming. In Extensions of Logic Programming, E. Lamma and P. Mello (Eds.). Springer, 282--318.

[59]

John C. Reynolds. 1988. 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

[60]

John C. Reynolds. 1996. Design of the Programming Language Forsythe. Technical Report CMU-CS-96-146. Carnegie Mellon University.

[61]

Gabriel Scherer. 2017. Deciding equivalence with sums and the empty type. In Proceedings of the Symposium on Principles of Programming Languages (POPL’17). ACM Press, 374--386.

Digital Library

[62]

Gabriel Scherer and Andreas Abel. 2012. On irrelevance and algorithmic equality in predicative type theory. Logic. Methods Comput. Sci. 8 (2012), 1--29.

[63]

Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis. 2020. A quick look at impredicativity. Proc. ACM Program. Lang. 4, Article 89(2020), 29 pages.

Digital Library

[64]

Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones. 2018. Guarded impredicative polymorphism. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’18). ACM Press, 783--796.

Digital Library

[65]

Wilfried Sieg and John Byrnes. 1998. Normal natural deduction proofs (in classical logic). Studia Logica 60, 1 (1998), 67--106.

[66]

Robert J. Simmons. 2014. Structural focalization. ACM Trans. Comput. Logic 15, 3, Article 21(Sept. 2014), 33 pages.

Digital Library

[67]

Vilhelm Sjöberg and Stephanie Weirich. 2015. Programming up to congruence. In Proceedings of the Symposium on Principles of Programming Languages (POPL’15). ACM Press, 369--382.

Digital Library

[68]

Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. 2011. OutsideIn(X): Modular type inference with local assumptions. J. Funct. Program. 21, 4--5 (2011), 333--412.

Digital Library

[69]

Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones. 2006. Boxy types: Inference for higher-rank types and impredicativity. In Proceedings of the International Conference on Functional Programming (ICFP’06). ACM Press, 251--262.

Digital Library

[70]

David H. D. Warren. 1977. Applied Logic—Its use and implementation as a programming tool. Ph.D. Dissertation. University of Edinburgh.

[71]

Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. 2003. A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101. Carnegie Mellon University.

[72]

J. B. Wells. 2002. The essence of principal typings. In Proceedings of the International Colloquium on Automata, Languages, and Programming. Springer, 913--925.

[73]

Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. 2011. Gradual typestate. In Proceedings of the 25th European Conference on Object-oriented Programming (ECOOP’11). Springer, 459--483.

[74]

Hongwei Xi. 1998. Dependent Types in Practical Programming. Ph.D. Dissertation. Carnegie Mellon University.

Digital Library

[75]

Hongwei Xi, Chiyan Chen, and Gang Chen. 2003. Guarded recursive datatype constructors. In Proceedings of the Symposium on Principles of Programming Languages (POPL’03). ACM Press, 224--235.

Digital Library

[76]

Hongwei Xi and Frank Pfenning. 1999. Dependent types in practical programming. In Proceedings of the Symposium on Principles of Programming Languages (POPL’99). ACM Press, 214--227.

Digital Library

[77]

Ningning Xie, Xuan Bi, and Bruno C. d. S. Oliveira. 2018. Consistent subtyping for all. In Proceedings of the European Symposium on Programming. Springer, 3--30.

[78]

Ningning Xie and Bruno C. d. S. Oliveira. 2018. Let arguments go first. In Proceedings of the European Symposium on Programming. Springer, 272--299.

[79]

Noam Zeilberger. 2015. Balanced polymorphism and linear lambda calculus. In Proceedings of the International Conference on Types for Proofs and Programs (TYPES’15).

[80]

Noam Zeilberger. 2018. 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 Press, 919--928.

Digital Library

[81]

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. A mechanical formalization of higher-ranked polymorphic type inference. Proc. ACM Program. Lang. 3, Article 112(July 2019), 29 pages.

Digital Library

Cited By

Ye WSun YOliveira B(2024)Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional TypingProceedings of the ACM on Programming Languages10.1145/36897828:OOPSLA2(2010-2039)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689782
Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Webbers Rvon Gleissenthall KJhala R(2024)Refinement Type RefutationsProceedings of the ACM on Programming Languages10.1145/36897458:OOPSLA2(962-987)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689745
Show More Cited By

Index Terms

Bidirectional Typing
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
2. Theory of computation
  1. Logic
    1. Type theory

Recommendations

Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94

This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...
Bidirectional typing for Erlang
Erlang 2021: Proceedings of the 20th ACM SIGPLAN International Workshop on Erlang

Erlang is a strict, dynamically typed functional programming language popular for its use in distributed and fault-tolerant applications. The absence of static type checking allows ill-typed programs to cause type errors at run time. The benefits of ...
Recasting MLF

The language ML^F is a proposal for a new type system that supersedes both ML and System F, allows for efficient, predictable, and complete type inference for partially annotated terms. In this work, we revisit the definition of ML^F, following a more ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Computing Surveys

ACM Computing Surveys Volume 54, Issue 5

June 2022

719 pages

ISSN:0360-0300

EISSN:1557-7341

DOI:10.1145/3467690

Editor:
Albert Zomaya
University of Sydney, Australia

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 May 2021

Accepted: 01 February 2021

Revised: 01 February 2021

Received: 01 August 2019

Published in CSUR Volume 54, Issue 5

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Natural Sciences and Engineering Research Council of Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
2,457
Total Downloads

Downloads (Last 12 months)995
Downloads (Last 6 weeks)144

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ye WSun YOliveira B(2024)Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional TypingProceedings of the ACM on Programming Languages10.1145/36897828:OOPSLA2(2010-2039)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689782
Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Webbers Rvon Gleissenthall KJhala R(2024)Refinement Type RefutationsProceedings of the ACM on Programming Languages10.1145/36897458:OOPSLA2(962-987)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689745
Berger FSchimpf ABieniusa AWehr SFernandez-Reyes KVoinea A(2024)Same Same but Different: A Comparative Analysis of Static Type Checkers in ErlangProceedings of the 23rd ACM SIGPLAN International Workshop on Erlang10.1145/3677995.3678189(2-12)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3677995.3678189
Xue XOliveira B(2024)Contextual TypingProceedings of the ACM on Programming Languages10.1145/36746558:ICFP(880-908)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674655
Zhou ZYe QDelaware BJagannathan S(2024)A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite AutomataProceedings of the ACM on Programming Languages10.1145/36564338:PLDI(1387-1411)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656433
Parreaux LBoruch-Gruszecki AFan AChau C(2024)When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class PolymorphismProceedings of the ACM on Programming Languages10.1145/36328908:POPL(1418-1450)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632890
Tallada MDenny JValero-Lara PLee STeranishi KVetter J(2024)eCC++ : A Compiler Construction Framework for Embedded Domain-Specific Languages2024 IEEE International Parallel and Distributed Processing Symposium Workshops (IPDPSW)10.1109/IPDPSW63119.2024.00129(667-677)Online publication date: 27-May-2024
https://doi.org/10.1109/IPDPSW63119.2024.00129
Liesnikov BCockx J(2024)Building a Correct-by-Construction Type Checker for a Dependently Typed Core LanguageProgramming Languages and Systems10.1007/978-981-97-8943-6_4(63-83)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_4
Vasilenko EVazou NBarthe G(2024)OBRA: Oracle-Based, Relational, Algorithmic Type VerificationProgramming Languages and Systems10.1007/978-981-97-8943-6_14(283-302)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_14
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents