Jana Dunfield
ABSTRACT
Bidirectional 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 systems), its error reporting, and its relative ease of implementation. Following design principles from proof theory, bidirectional typing can be applied to many type constructs. The principles underlying a bidirectional approach to polymorphism, however, are less obvious. We give a declarative, bidirectional account of higher-rank polymorphism, grounded in proof theory; this calculus enjoys many properties such as eta-reduction and predictability of annotations. We give an algorithm for implementing the declarative system; our algorithm is remarkably simple and well-behaved, despite being both sound and complete.
Supplemental Material
Available for Download
zip
icfp016.zip (496.1 KB)
Contents: DunfieldKrishnaswami13_proofs.pdf - Lemmas and proofs omitted from the main paper.
- Andreas Abel. Termination checking with types. RAIRO--Theoretical Informatics and Applications, 38 (4): 277--319, 2004. Special Issue: Fixed Points in Computer Science (FICS'03).Google Scholar
Cross Ref
- Andreas Abel, Thierry Coquand, and Peter Dybjer. Verifying a semantic βη-conversion test for Martin-Löf type theory. In Mathematics of Program Construction (MPC'08), volume 5133 of LNCS, pages 29--56, 2008. Google ScholarDigital Library
- Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. Logic and Computation, 2 (3): 297--347, 1992.Google ScholarCross Ref
- Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. A bi-directional refinement algorithm for the calculus of (co)inductive constructions. Logical Methods in Computer Science, 8 (1), 2012.Google Scholar
- Gavin M. Bierman, Erik Meijer, and Mads Torgersen. Lost in translation: formalizing proposed extensions toCsharp. In OOPSLA, 2007. Google ScholarDigital Library
- Luca Cardelli. An implementation ofFsub. Research report 97, DEC/Compaq Systems Research Center, February 1993.Google Scholar
- Iliano Cervesato and Frank Pfenning. A linear spine calculus. J. Logic and Computation, 13 (5): 639--688, 2003.Google ScholarCross Ref
- Adam Chlipala, Leaf Petersen, and Robert Harper. Strict bidirectional type checking. In Workshop on Types in Language Design and Impl. (TLDI '05), pages 71--78, 2005. Google ScholarDigital Library
- Jacek Chrzaszcz. Polymorphic subtyping without distributivity. In Mathematical Foundations of Computer Science, volume 1450 of LNCS, pages 346--355. Springer, 1998. Google ScholarDigital Library
- Thierry Coquand. An algorithm for type-checking dependent types. Science of Computer Programming, 26 (1--3): 167--177, 1996. Google ScholarDigital Library
- Luis Damas and Robin Milner. Principal type-schemes for functional programs. In POPL, pages 207--212. ACM, 1982. Google ScholarDigital Library
- Rowan Davies and Frank Pfenning. Intersection types and computational effects. In ICFP, pages 198--208, 2000. Google ScholarDigital Library
- Jana Dunfield. A Unified System of Type Refinements. PhD thesis, Carnegie Mellon University, 2007. Carnegie Mellon University-CS-07-129.Google Scholar
- Jana Dunfield. Greedy bidirectional polymorphism. In ML Workshop, pages 15--26, 2009. https://research.cs.queensu.ca/home/jana/papers/poly/. Google ScholarDigital Library
- Jana Dunfield and Frank Pfenning. Tridirectional typechecking. In POPL, pages 281--292, January 2004. Google ScholarDigital Library
- Adam Gundry, Conor McBride, and James McKinna. Type inference in context. In Mathematically Structured Functional Programming (MSFP), 2010. Google ScholarDigital Library
- Didier Le Botlan and Didier Rémy.MLF: raising ML to the power of System F. In ICFP, pages 27--38, 2003. Google ScholarDigital Library
- Didier Le Botlan and Didier Rémy. RecastingMLF. Information and Computation, 207: 726--785, 2009. Google ScholarDigital Library
- Daan Leijen. Flexible types: robust type inference for first-class polymorphism. In POPL, pages 66--77, 2009. Google ScholarDigital Library
- Andres Löh, Conor McBride, and Wouter Swierstra. A tutorial implementation of a dependently typed lambda calculus. Unpublished draft, http://people.cs.uu.nl/andres/LambdaPi/index.html, 2008.Google Scholar
- William Lovas. Refinement Types for Logical Frameworks. PhD thesis, Carnegie Mellon University, 2010. Carnegie Mellon University-CS-10-138. Google ScholarDigital Library
- Dale Miller. Unification under a mixed prefix. J. Symbolic Computation, 14: 321--358, 1992. Google ScholarDigital Library
- John C. Mitchell. Polymorphic type inference and containment. Information and Computation, 76: 211--249, 1988. Google ScholarDigital Library
- Martin Odersky and Konstantin Laufer. Putting type annotations to work. In POPL, 1996. Google ScholarDigital Library
- Martin Odersky, Matthias Zenger, and Christoph Zenger. Colored local type inference. In POPL, pages 41--53, 2001. Google ScholarDigital Library
- Simon Peyton Jones and Mark Shields. Lexically scoped type variables. Technical report, Microsoft Research, 2004.Google Scholar
- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types. J. Functional Programming, 17 (1): 1--82, 2007. Google ScholarDigital Library
- Frank Pfenning. Church and Curry: Combining intrinsic and extrinsic typing. In Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday. College Publications, 2008.Google Scholar
- Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In POPL, pages 371--382, 2008. Google ScholarDigital Library
- Benjamin C. Pierce and David N. Turner. Local type inference. ACM Trans. Prog. Lang. Sys., 22: 1--44, 2000. Google ScholarDigital Library
- Didier Rémy. Extension of ML type system with a sorted equational theory on types. Research Report 1766, INRIA, 1992.Google Scholar
- Didier Rémy and Boris Yakobowski. From ML toMLF: graphic type constraints with efficient type inference. In ICFP, pages 63--74, 2008.Google ScholarDigital Library
- Robert J. Simmons. Structural focalization. http://arxiv.org/abs/1109.6273v4arXiv: 1109.6273v4 {cs.LO}, 2012.Google Scholar
- Jerzy Tiuryn and Paweł Urzyczyn. The subtyping problem for second-order types is undecidable. In LICS, 1996. Google ScholarDigital Library
- Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones. Boxy types: inference for higher-rank types and impredicativity. In ICFP, pages 251--262, 2006. Google ScholarDigital Library
- Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones. FPH: First-class polymorphism for Haskell. In ICFP, pages 295--306, 2008. Google ScholarDigital Library
- Dimitrios Vytiniotis, Simon Peyton Jones, and Tom Schrijvers. Let should not be generalised. In Workshop on Types in Language Design and Impl. (TLDI '10), pages 39--50, 2010. Google ScholarDigital Library
- Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework: The propositional fragment. In Types for Proofs and Programs, pages 355--377. Springer-Verlag LNCS 3085, 2004.Google ScholarCross Ref
- J. B. Wells. Typability and type checking in System F are equivalent and undecidable. Annals of Pure and Applied Logic, 98: 111--156, 1999.Google ScholarCross Ref
- Hongwei Xi. Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University, 1998. Google ScholarDigital Library
Index Terms
- Complete and easy bidirectional typechecking for higher-rank polymorphism
Recommendations
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 ...
Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types
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 ...
A mechanical formalization of higher-ranked polymorphic type inference
Modern functional programming languages, such as Haskell or OCaml, use sophisticated forms of type inference. While an important topic in the Programming Languages research, there is little work on the mechanization of the metatheory of type inference in ...
Comments