Jana Dunfield
Abstract
Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its applicability to a variety of type systems, its error reporting, and its ease of implementation. Following principles from proof theory, bidirectional typing can be applied to many type constructs. The principles underlying a bidirectional approach to indexed types (generalized algebraic datatypes) are less clear. Building on proof-theoretic treatments of equality, we give a declarative specification of typing based on focalization. This approach permits declarative rules for coverage of pattern matching, as well as support for first-class existential types using a focalized subtyping judgment. We use refinement types to avoid explicitly passing equality proofs in our term syntax, making our calculus similar to languages such as Haskell and OCaml. We also extend the declarative specification with an explicit rules for deducing when a type is principal, permitting us to give a complete declarative specification for a rich type system with significant type inference. We also give a set of algorithmic typing rules, and prove that it is sound and complete with respect to the declarative system. The proof requires a number of technical innovations, including proving soundness and completeness in a mutually recursive fashion.
Supplemental Material
- Andreas Abel. 2006. Towards Generic Programming with Sized Types. In Mathematics of Program Construction (LNCS), Tarmo Uustalu (Ed.), Vol. 4014. Springer, 10–28. Google Scholar
Digital Library
- Andreas Abel, Thierry Coquand, and Peter Dybjer. 2008. Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory. In Mathematics of Program Construction (MPC’08) (LNCS), Vol. 5133. Springer, 29–56. Google ScholarDigital Library
- Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983. A Filter Lambda Model and the Completeness of Type Assignment. J. Symbolic Logic 48, 4 (1983), 931–940.Google ScholarCross Ref
- Matthias Blume. 2001. No-Longer-Foreign: Teaching an ML compiler to speak C “natively”. Electronic Notes in Theoretical Computer Science 59, 1 (2001).Google Scholar
- James Cheney and Ralf Hinze. 2003. First-Class Phantom Types. Technical Report CUCIS TR2003-1901. Cornell University.Google Scholar
- Jacek Chrząszcz. 1998. Polymorphic Subtyping Without Distributivity. In Mathematical Foundations of Computer Science (LNCS), Vol. 1450. Springer, 346–355. Google ScholarDigital Library
- Thierry Coquand. 1996. An Algorithm for Type-Checking Dependent Types. Science of Computer Programming 26, 1–3 (1996), 167–177. Google ScholarDigital Library
- Luis Damas and Robin Milner. 1982. Principal type-schemes for functional programs. In POPL. ACM Press, 207–212. Google ScholarDigital Library
- Rowan Davies and Frank Pfenning. 2000. Intersection Types and Computational Effects. In ICFP. ACM Press, 198–208. Google ScholarDigital Library
- Stephen Dolan and Alan Mycroft. 2017. Polymorphism, Subtyping, and Type Inference in MLsub. In POPL. ACM Press, 60–72. Google ScholarDigital Library
- Jana Dunfield. 2007a. Refined typechecking with Stardust. In Programming Languages meets Programming Verification (PLPV ’07). ACM Press, 21–32. Google ScholarDigital Library
- Jana Dunfield. 2007b. A Unified System of Type Refinements. Ph.D. Dissertation. Carnegie Mellon University. CMU-CS-07-129.Google Scholar
- Jana Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism. In ICFP. ACM Press, 429–442. arXiv: 1306.6032 {cs.PL} . Google ScholarDigital Library
- Jana Dunfield and Frank Pfenning. 2003. Type Assignment for Intersections and Unions in Call-by-Value Languages. In FoSSaCS. Springer, 250–266. Google ScholarDigital Library
- Matthew Fluet and Riccardo Pucella. 2006. Phantom types and subtyping. (2006). arXiv: cs/0403034 {cs.PL} . Google ScholarDigital Library
- Jacques Garrigue and Jacques Le Normand. 2015. GADTs and Exhaustiveness: Looking for the Impossible. In Proceedings ML Family / OCaml Users and Developers workshops, ML Family/OCaml 2015 (EPTCS). 23–35.Google Scholar
- Jacques Garrigue and Didier Rémy. 2013. Ambivalent Types for Principal Type Inference with GADTs. In APLAS. Springer, 257–272. Google ScholarDigital Library
- Jean-Yves Girard. 1992. A Fixpoint Theorem in Linear Logic. (1992). Post to Linear Logic mailing list, http://www.seas. upenn.edu/~sweirich/types/archive/1992/msg00030.html .Google Scholar
- Robert Harper and Greg Morrisett. 1995. Compiling polymorphism using intensional type analysis. In POPL. ACM Press, 130–141. Google ScholarDigital Library
- Georgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis, and Simon Peyton Jones. 2015. GADTs Meet Their Match: pattern-matching warnings that account for GADTs, guards, and laziness. In ICFP. ACM Press, 424–436. Google ScholarDigital Library
- Neelakantan R. Krishnaswami. 2009. Focusing on Pattern Matching. In POPL. ACM Press, 366–378. Google ScholarDigital Library
- Konstantin Läufer and Martin Odersky. 1994. Polymorphic type inference and abstract data types. ACM Trans. Prog. Lang. Sys. 16, 5 (1994), 1411–1430. Google ScholarDigital Library
- Daan Leijen and Erik Meijer. 1999. Domain specific embedded compilers. In USENIX Conf. Domain-Specific Languages (DSL ’99). ACM Press, 109–122. Google ScholarDigital Library
- Martin Odersky, Matthias Zenger, and Christoph Zenger. 2001. Colored Local Type Inference. In POPL. ACM Press, 41–53. Google ScholarDigital Library
- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical type inference for arbitraryrank types. J. Functional Programming 17, 1 (2007), 1–82. Google ScholarDigital Library
- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. 2006. Simple unification-based type inference for GADTs. In ICFP. ACM Press, 50–61. Google ScholarDigital Library
- Brigitte Pientka. 2008. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In POPL. ACM Press, 371–382. Google ScholarDigital Library
- Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press. Google ScholarDigital Library
- Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Trans. Prog. Lang. Sys. 22 (2000), 1–44. Google ScholarDigital Library
- François Pottier and Yann Régis-Gianas. 2006. Stratified type inference for generalized algebraic data types. In POPL. ACM Press, 232–244. Google ScholarDigital Library
- Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008. Liquid types. In PLDI. ACM Press, 159–169. Google ScholarDigital Library
- Peter Schroeder-Heister. 1994. Definitional reflection and the completion. In Extensions of Logic Programming (LNCS). Springer, 333–347. Google ScholarDigital Library
- Vincent Simonet and François Pottier. 2007. A constraint-based approach to guarded algebraic data types. ACM Transactions on Programming Languages and Systems (TOPLAS) 29, 1 (2007), 1. Google ScholarDigital Library
- Jerzy Tiuryn and Paweł Urzyczyn. 1996. The Subtyping Problem for Second-Order Types is Undecidable. In LICS. IEEE Press. Google ScholarDigital Library
- Dimitrios Vytiniotis, Simon Peyton Jones, and Tom Schrijvers. 2010. Let should not be generalised. In Workshop on Types in Language Design and Impl. (TLDI ’10). ACM Press, 39–50. Google ScholarDigital Library
- Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. 2011. OutsideIn(X): Modular type inference with local assumptions. J. Functional Programming 21, 4–5 (2011), 333–412. Google ScholarDigital Library
- Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. 2004. A Concurrent Logical Framework: The Propositional Fragment. In Types for Proofs and Programs. Springer LNCS 3085, 355–377.Google ScholarCross Ref
- Hongwei Xi, Chiyan Chen, and Gang Chen. 2003. Guarded recursive datatype constructors. In POPL. ACM Press, 224–235. Google ScholarDigital Library
- Hongwei Xi and Frank Pfenning. 1999. Dependent Types in Practical Programming. In POPL. ACM Press, 214–227. Google ScholarDigital Library
- Noam Zeilberger. 2009. Refinement Types and Computational Duality. In Programming Languages meets Programming Verification (PLPV ’09). ACM Press, 15–26. Google ScholarDigital Library
Index Terms
- Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types
Recommendations
Complete and easy bidirectional typechecking for higher-rank polymorphism
ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programmingBidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its scalability (unlike Damas-Milner type inference, bidirectional typing remains decidable even for very expressive type ...
Complete and easy bidirectional typechecking for higher-rank polymorphism
ICFP '13Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its scalability (unlike Damas-Milner type inference, bidirectional typing remains decidable even for very expressive type ...
Greedy bidirectional polymorphism
ML '09: Proceedings of the 2009 ACM SIGPLAN workshop on MLBidirectional typechecking has become popular in advanced type systems because it works in many situations where inference is undecidable. In this paper, I show how to cleanly handle parametric polymorphism in a bidirectional setting. The key ...
Comments