Ningning Xie
Tom Schrijvers
Skip Abstract Section
Abstract
Consistent subtyping is employed in some gradual type systems to validate type conversions. The original definition by Siek and Taha serves as a guideline for designing gradual type systems with subtyping. Polymorphic types à la System F also induce a subtyping relation that relates polymorphic types to their instantiations. However, Siek and Taha’s definition is not adequate for polymorphic subtyping. The first goal of this article is to propose a generalization of consistent subtyping that is adequate for polymorphic subtyping and subsumes the original definition by Siek and Taha. The new definition of consistent subtyping provides novel insights with respect to previous polymorphic gradual type systems, which did not employ consistent subtyping. The second goal of this article is to present a gradually typed calculus for implicit (higher-rank) polymorphism that uses our new notion of consistent subtyping. We develop both declarative and (bidirectional) algorithmic versions for the type system. The algorithmic version employs techniques developed by Dunfield and Krishnaswami for higher-rank polymorphism to deal with instantiation. We prove that the new calculus satisfies all static aspects of the refined criteria for gradual typing. We also study an extension of the type system with static and gradual type parameters, in an attempt to support a variant of the dynamic criterion for gradual typing. Assuming a coherence conjecture for the extended calculus, we show that the dynamic gradual guarantee of our source language can be reduced to that of λ B, which, at the time of writing, is still an open question. Most of the metatheory of this article, except some manual proofs for the algorithmic type system and extensions, has been mechanically formalized using the Coq proof assistant.
- Martin Abadi, Luca Cardelli, Benjamin Pierce, and Didier Rémy. 1995. Dynamic typing in polymorphic languages. J. Funct. Program. 5, 1 (1995), 111--130.Google Scholar
Cross Ref
- Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011. Blame for all. In Proceedings of the 38th Symposium on Principles of Programming Languages.Google ScholarDigital Library
- Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for free for free: Parametricity, with and without types. In Proceedings of the 22nd International Conference on Functional Programming.Google ScholarDigital Library
- Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. 2014. A theory of gradual effect systems. In Proceedings of the 19th International Conference on Functional Programming.Google Scholar
- Gavin Bierman, Martín Abadi, and Mads Torgersen. 2014. Understanding typescript. In Proceedings of the 28th European Conference on Object-Oriented Programming.Google ScholarDigital Library
- Gavin Bierman, Erik Meijer, and Mads Torgersen. 2010. Adding dynamic types to C#. In Proceedings of the European Conference on Object-Oriented Programming.Google Scholar
- Ambrose Bonnaire-Sergeant, Rowan Davies, and Sam Tobin-Hochstadt. 2016. Practical optional types for clojure. In Programming Languages and Systems.Google Scholar
- Luca Cardelli. 1993. An Implementation of FSub. Technical Report. Research Report 97, Digital Equipment Corporation Systems Research Center.Google Scholar
- Giuseppe Castagna and Victor Lanvin. 2017. Gradual typing with union and intersection types. Proc. ACM Program. Lang. 1, Article 41 (Aug. 2017).Google ScholarDigital Library
- Alonzo Church. 1941. The Calculi of Lambda-conversion. Number 6. Princeton University Press.Google Scholar
- Matteo Cimini and Jeremy G. Siek. 2016. The gradualizer: A methodology and algorithm for generating gradual type systems. In Proceedings of the 43rd Symposium on Principles of Programming Languages.Google Scholar
- Matteo Cimini and Jeremy G. Siek. 2017. Automatically generating the dynamic semantics of gradually typed languages. In Proceedings of the 44th Symposium on Principles of Programming Languages.Google Scholar
- Haskell Brooks Curry, Robert Feys, William Craig, J. Roger Hindley, and Jonathan P. Seldin. 1958. Combinatory Logic. Vol. 1. North-Holland Amsterdam.Google Scholar
- Luis Damas and Robin Milner. 1982. Principal type-schemes for functional programs. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL’82). 6.Google ScholarDigital Library
- Rowan Davies and Frank Pfenning. 2000. Intersection types and computational effects. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP’00). ACM, New York, NY, 198--208. DOI:https://doi.org/10.1145/351240.351259Google ScholarDigital Library
- Dominique Devriese, Marco Patrignani, and Frank Piessens. 2017. Parametricity versus the universal type. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL’17), Vol. 2, 38.Google ScholarDigital Library
- Joshua Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and easy bidirectional typechecking for higher-rank polymorphism. In Proceedings of the International Conference on Functional Programming. https://arxiv.org/abs/1306.6032.Google Scholar
- Ronald Garcia and Matteo Cimini. 2015. Principal type schemes for gradual programs. In Proceedings of the 42nd Symposium on Principles of Programming Languages.Google ScholarDigital Library
- Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting gradual typing. In Proceedings of the 43rd Symposium on Principles of Programming Languages.Google ScholarDigital Library
- Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. 2006. Sage: Hybrid checking for flexible specifications. In Proceedings of the Scheme and Functional Programming Workshop.Google Scholar
- J. Roger Hindley. 1969. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc. 146 (1969), 29--60.Google Scholar
- Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017. On polymorphic gradual typing. In Proceedings of the 22nd International Conference on Functional Programming.Google ScholarDigital Library
- Khurram A. Jafery and Joshua Dunfield. 2017. Sums of uncertainty: Refinements go gradual. In Proceedings of the 44th Symposium on Principles of Programming Languages. 14.Google Scholar
- Mark P. Jones. 2000. Type classes with functional dependencies. In Proceedings of the European Symposium on Programming. Springer, 230--244.Google ScholarCross Ref
- Simon Peyton Jones, Mark Jones, and Erik Meijer. 1997. Type classes: Exploring the design space. In Proceedings of the Haskell Workshop, Vol. 1997.Google Scholar
- Oleg Kiselyov, Ralf Lämmel, and Keean Schupke. 2004. Strongly typed heterogeneous collections. In Proceedings of the ACM SIGPLAN Workshop on Haskell. ACM, 96--107.Google ScholarDigital Library
- Didier Le Botlan and Didier Rémy. 2003. MLF: Raising ML to the power of system F. In Proceedings of the International Conference on Functional Programming (ICFP’03). 12.Google ScholarDigital Library
- Didier Le Botlan and Didier Rémy. 2009. Recasting MLF. Info. Comput. 207, 6 (2009), 726--785.Google ScholarDigital Library
- Jukka Lehtosalo et al. 2006. Mypy. Retrieved from http://www.mypy-lang.org/.Google Scholar
- Daan Leijen. 2009. Flexible types: Robust type inference for first-class polymorphism. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL’09). 12.Google ScholarDigital Library
- Jacob Matthews and Amal Ahmed. 2008. Parametric polymorphism through run-time sealing or, theorems for low, low prices! In Proceedings of the European Symposium on Programming. Springer, 16--31.Google Scholar
- Conor McBride. 2002. Faking it simulating dependent types in Haskell. J. Funct. Program. 12, 4--5 (2002), 375--392.Google ScholarDigital Library
- John C. Mitchell. 1990. Polymorphic type inference and containment. In Logical Foundations of Functional Programming. Addison-Wesley, Boston, MA.Google Scholar
- James H. Morris, Jr. 1973. Types are not sets. In Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL’73). ACM, New York, NY, 120--124. DOI:https://doi.org/10.1145/512927.512938Google ScholarDigital Library
- James Hiram Morris Jr. 1969. Lambda-calculus Models of Programming Languages. Ph.D. Dissertation. Massachusetts Institute of Technology.Google Scholar
- Georg Neis, Derek Dreyer, and Andreas Rossberg. 2009. Non-parametric parametricity. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP’09). ACM, New York, NY, 135--148. DOI:https://doi.org/10.1145/1596550.1596572Google ScholarDigital Library
- Martin Odersky and Konstantin Läufer. 1996. Putting type annotations to work. In Proceedings of the 23rd Symposium on Principles of Programming Languages.Google ScholarDigital Library
- Michel Parigot. 1992. Recursive programming with proofs. Theor. Comput. Sci. 94, 2 (1992), 335--356.Google ScholarDigital Library
- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical type inference for arbitrary-rank types. J. Funct. Program. 17, 1 (2007), 1--82.Google ScholarDigital Library
- Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press.Google ScholarDigital Library
- Didier Rémy and Boris Yakobowski. 2008. From ML to MLF: Graphic type constraints with efficient type inference. In Proceedings of the International Conference on Functional Programming (ICFP’08). 12.Google ScholarDigital Library
- John C. Reynolds. 1983. Types, abstraction and parametric polymorphism. In Proceedings of the IFIP 9th World Computer Congress.Google Scholar
- John C. Reynolds. 1991. The coherence of languages with intersection types. In Proceedings of the International Conference on Theoretical Aspects of Computer Software.Google ScholarDigital Library
- Jeremy Siek, Ronald Garcia, and Walid Taha. 2009. Exploring the design space of higher-order casts. In Proceedings of the European Symposium on Programming. 17--31.Google ScholarDigital Library
- Jeremy G. Siek and Walid Taha. 2006. Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop.Google Scholar
- Jeremy G. Siek and Walid Taha. 2007. Gradual typing for objects. In Proceedings of the European Conference on Object-Oriented Programming.Google Scholar
- Jeremy G. Siek and Manish Vachharajani. 2008. Gradual typing with unification-based inference. In Proceedings of the Symposium on Dynamic Languages.Google Scholar
- Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined criteria for gradual typing. In LIPIcs-Leibniz International Proceedings in Informatics.Google Scholar
- Jeremy G. Siek and Philip Wadler. 2016. The Key to Blame: Gradual Typing Meets Cryptography (draft).Google Scholar
- Julien Verlaguet. 2013. Facebook: Analyzing PHP statically. In Proceedings of Commercial Users of Functional Programming.Google Scholar
- Michael M. Vitousek, Andrew M. Kent, Jeremy G. Siek, and Jim Baker. 2014. Design and evaluation of gradual typing for Python. In Proceedings of the 10th Symposium on Dynamic Languages.Google ScholarDigital Library
- Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. 2008. FPH: First-class Polymorphism for Haskell. In Proceedings of the International Conference on Functional Programming (ICFP’08). 12.Google ScholarDigital Library
- Philip Wadler and Robert Bruce Findler. 2009. Well-typed programs can’t be blamed. In Proceedings of the 18th European Symposium on Programming Languages and Systems.Google ScholarDigital Library
- J. B. Wells. 1999. Typability and type checking in System F are equivalent and undecidable. Ann. Pure Appl. Logic 98, 1 (1999), 111--156. DOI:https://doi.org/10.1016/S0168-0072(98)00047-5Google ScholarCross Ref
- Ningning Xie, Xuan Bi, and Bruno C. d. S. Oliveira. 2018. Consistent subtyping for all. In Proceedings of the European Symposium on Programming. 3--30.Google Scholar
Index Terms
- Consistent Subtyping for All
Recommendations
Graduality from embedding-projection pairs
Gradually typed languages allow statically typed and dynamically typed code to interact while maintaining benefits of both styles. The key to reasoning about these mixed programs is Siek-Vitousek-Cimini-Boyland’s (dynamic) gradual guarantee, which says ...
On polymorphic gradual typing
We study an extension of gradual typing—a method to integrate dynamic typing and static typing smoothly in a single language—to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically ...
Principal Type Schemes for Gradual Programs
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesGradual typing is a discipline for integrating dynamic checking into a static type system. Since its introduction in functional languages, it has been adapted to a variety of type systems, including object-oriented, security, and substructural. This ...
Comments