Giuseppe Castagna
Victor Lanvin
Jeremy G. Siek
Skip Abstract Section
Skip Supplemental Material SectionAbstract
We define a new, more semantic interpretation of gradual types and use it to ``gradualize'' two forms of polymorphism: subtyping polymorphism and implicit parametric polymorphism. In particular, we use the new interpretation to define three gradual type systems ---Hindley-Milner, with subtyping, and with union and intersection types--- in terms of two preorders, subtyping and materialization. We define these systems both declaratively ---by adding two subsumption-like rules--- which yields clearer, more intelligible, and streamlined definitions, and algorithmically by reusing existing techniques such as unification and tallying.
Supplemental Material
Available for Download
zip
popl19main-p128-p-aux.zip (791.1 KB)
Appendix with all the proofs and some auxiliary definitions and results.
- Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011. Blame for all. ACM SIGPLAN Notices 46, 1 (2011), 201–214.Google Scholar
Digital Library
- Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for Free for Free: Parametricity, With and Without Types. In International Conference on Functional Programming (ICFP).Google Scholar
- Alexander Aiken and Edward L. Wimmers. 1993. Type Inclusion Constraints and Type Inference. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture (FPCA ’93). ACM, New York, NY, USA, 31–41. Google ScholarDigital Library
- Alexander Aiken, Edward L. Wimmers, and T. K. Lakshman. 1994. Soft typing with conditional types. In POPL ’94: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM Press, New York, NY, USA, 163–173. Google ScholarDigital Library
- Pedro Ángelo and Mário Florido. 2018. Gradual Intersection Types. In Workshop on Intersection Types and Related Systems.Google Scholar
- Spenser Bauman, Carl Friedrich Bolz-Tereick, Jeremy Siek, and Sam Tobin-Hochstadt. 2017. Sound Gradual Typing: Only Mostly Dead. Proc. ACM Program. Lang. 1, OOPSLA, Article 54 (Oct. 2017), 24 pages. Google ScholarDigital Library
- Gavin Bierman, Martín Abadi, and Mads Torgersen. 2014. Understanding TypeScript. In ECOOP 2014 – Object-Oriented Programming, Richard Jones (Ed.). Lecture Notes in Computer Science, Vol. 8586. Springer Berlin Heidelberg, 257–281. Google ScholarDigital Library
- John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw. 2017. Migrating Gradual Types. Proc. ACM Program. Lang. 2, POPL (Dec. 2017), 15:1–15:29. Google ScholarDigital Library
- Robert Cartwright and Mike Fagan. 1991. Soft typing. In Conference on Programming Language Design and Implementation (PLDI). ACM Press, 278–292. Google ScholarDigital Library
- Giuseppe Castagna. 2005. Semantic subtyping: challenges, perspectives, and open problems. In ICTCS 2005, Italian Conference on Theoretical Computer Science (Lecture Notes in Computer Science). Springer, 1–20. Google ScholarDigital Library
- Giuseppe Castagna. 2018. Covariance and Contravariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers). (2018). First version: 02/2013, last revision: 09/2018. Unpublished manuscript.Google Scholar
- Giuseppe Castagna and Alain Frisch. 2005. A gentle introduction to semantic subtyping. In Proceedings of PPDP ’05, the 7th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming, pages 198-208, ACM Press (full version) and ICALP ’05, 32nd International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science n. 3580, pages 30-34, Springer (summary). Lisboa, Portugal. Joint ICALP-PPDP keynote talk. Google ScholarDigital Library
- Giuseppe Castagna and Victor Lanvin. 2017. Gradual Typing with Union and Intersection Types. Proc. ACM Program. Lang. 1, ICFP ’17, Article 41 (Sept. 2017). Google ScholarDigital Library
- Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, and Pietro Abate. 2015. Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction. In Proceedings of the 42nd ACM Symposium on Principles of Programming Languages (POPL ’15). ACM, 289–302. Google ScholarDigital Library
- Giuseppe Castagna, Tommaso Petrucciani, and Kim Nguyen. 2016. Set-theoretic Types for Polymorphic Variants. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016). ACM, New York, NY, USA, 378–391. Google ScholarDigital Library
- Giuseppe Castagna and Zhiwu Xu. 2011. Set-theoretic Foundation of Parametric Polymorphism and Subtyping. In ICFP ’11: 16th ACM-SIGPLAN International Conference on Functional Programming. 94–106. Google ScholarDigital Library
- Bruno Courcelle. 1983. Fundamental properties of infinite trees. Theoretical Computer Science 25 (1983), 95–169.Google ScholarCross Ref
- Stephen Dolan and Alan Mycroft. 2017. Polymorphism, Subtyping, and Type Inference in MLsub. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). ACM, New York, NY, USA, 60–72. Google ScholarDigital Library
- Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for Higher-Order Functions. Technical Report NU-CCS-02-05. Northeastern University.Google Scholar
- Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. 2008. Semantic Subtyping: dealing set-theoretically with function, union, intersection, and negation types. J. ACM 55, 4 (2008), 1–64. Google ScholarDigital Library
- You-Chin Fuh and Prateek Mishra. 1988. Type inference with subtypes. In ESOP ’88, H. Ganzinger (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 94–114. Google ScholarDigital Library
- Ronald Garcia. 2013. Calculating Threesomes, with Blame. In ICFP ’13: Proceedings of the International Conference on Functional Programming. Google ScholarDigital Library
- Ronald Garcia and Matteo Cimini. 2015. Principal Type Schemes for Gradual Programs. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). ACM, 303–315. Google ScholarDigital Library
- Ronald Garcia, Alison M Clark, and Éric Tanter. 2016. Abstracting gradual typing. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). ACM, 429–442. Google ScholarDigital Library
- Nils Gesbert, Pierre Genevès, and Nabil Layaïda. 2015. A Logical Approach to Deciding Semantic Subtyping. ACM Trans. Program. Lang. Syst. 38, 1 (2015), 3. Google ScholarDigital Library
- Robert Harper. 2006. Programming Languages: Theory and Practice. Carnegie Mellon University. Available on the web: http://fpl.cs.depaul.edu/jriely/547/extras/online.pdf .Google Scholar
- Fritz Henglein. 1994. Dynamic typing: syntax and proof theory. Science of Computer Programming 22, 3 (June 1994), 197–230. Google ScholarDigital Library
- Haruo Hosoya, Jérôme Vouillon, and Benjamin C. Pierce. 2000. Regular Expression Types for XML. In ICFP ’00 (SIGPLAN Notices), Vol. 35(9). http://www.cis.upenn.edu/~hahosoya/papers/regsub.ps Google ScholarDigital Library
- Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017. On Polymorphic Gradual Typing. In International Conference on Functional Programming (ICFP). ACM. Google ScholarDigital Library
- Lintaro Ina and Atsushi Igarashi. 2011. Gradual typing for generics. In Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications (OOPSLA ’11). Google ScholarDigital Library
- Khurram A. Jafery and Joshua Dunfield. 2017. Sums of Uncertainty: Refinements go gradual. In Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Matthias Keil and Peter Thiemann. 2015. Blame Assignment for Higher-order Contracts with Intersection and Union. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015). ACM, New York, NY, USA, 375–386. Google ScholarDigital Library
- Assaf J. Kfoury and Joe B. Wells. 2004. Principality and type inference for intersection types using expansion variables. Theoretical Computer Science 311, 1 (2004), 1 – 70. Google ScholarDigital Library
- Nicolás Lehmann and Éric Tanter. 2017. Gradual Refinement Types. In Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- André Murbach Maidl, Fabio Mascarenhas, and Roberto Ierusalimschy. 2014. Typed Lua: An Optional Type System for Lua. In Proceedings of the Workshop on Dynamic Languages and Applications (Dyla’14). ACM, New York, NY, USA, Article 3, 10 pages. Google ScholarDigital Library
- Alberto Martelli and Ugo Montanari. 1982. An Efficient Unification Algorithm. ACM Trans. Program. Lang. Syst. 4, 2 (1982), 258–282. Google ScholarDigital Library
- John C. Mitchell. 1991. Type inference with simple subtypes. Journal of Functional Programming 1, 3 (1991), 245–285.Google ScholarCross Ref
- Francisco Ortin and Miguel García. 2011. Union and intersection types to support both dynamic and static typing. Inform. Process. Lett. 111, 6 (2011), 278 – 286. Google ScholarDigital Library
- Tommaso Petrucciani, Giuseppe Castagna, Davide Ancona, and Elena Zucca. 2018. Semantic subtyping for non-strict languages. Technical Report. https://arxiv.org/abs/1810.05555 .Google Scholar
- François Pottier. 2001. Simplifying subtyping constraints: a theory. Inf. Comput. 170, 2 (2001), 153–183. Google ScholarDigital Library
- François Pottier and Didier Rémy. 2005. The essence of ML type inference. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). MIT Press, Chapter 10, 389–489.Google Scholar
- Aseem Rastogi, Avik Chaudhuri, and Basil Hosmer. 2012. The ins and outs of gradual type inference. In Symposium on Principles of Programming Languages (POPL). 481–494. Google ScholarDigital Library
- Simona Ronchi Della Rocca. 1988. Principal type scheme and unification for intersection type discipline. Theor. Comput. Sci. 59, 1-2 (1988), 181–209. Google ScholarDigital Library
- Taro Sekiyama, Atsushi Igarashi, and Michael Greenberg. 2017. Polymorphic Manifest Contracts, Revised and Resolved. ACM Trans. Program. Lang. Syst. 39, 1 (Feb. 2017), 3:1–3:36. Google ScholarDigital Library
- Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Proceedings of Scheme and Functional Programming Workshop. ACM, 81–92.Google Scholar
- Jeremy G. Siek and Walid Taha. 2007. Gradual Typing for Objects. In European Conference on Object-Oriented Programming (LCNS), Vol. 4609. 2–27. Google ScholarDigital Library
- Jeremy G. Siek, Peter Thiemann, and Philip Wadler. 2015a. Blame and coercion: together again for the first time. In ACM SIGPLAN Notices, Vol. 50. ACM, 425–435. Google ScholarDigital Library
- Jeremy G. Siek and Manish Vachharajani. 2008a. Gradual typing with unification-based inference. In Proceedings of the 2008 Symposium on Dynamic languages. ACM, 7. Google ScholarDigital Library
- Jeremy G. Siek and Manish Vachharajani. 2008b. Gradual Typing with Unification-based Inference. Technical Report CU-CS-1039-08. University of Colorado at Boulder.Google Scholar
- Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015b. Refined criteria for gradual typing. In LIPIcs-Leibniz International Proceedings in Informatics, Vol. 32. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.Google Scholar
- Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, and Gavin Bierman. 2014. Gradual Typing Embedded Securely in JavaScript. In ACM Conference on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. 2016. Is Sound Gradual Typing Dead?. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). ACM, 456–468. Google ScholarDigital Library
- Matías Toro and Éric Tanter. 2017. A Gradual Interpretation of Union Types. In Proceedings of the 24th Static Analysis Symposium (SAS 2017) (Lecture Notes in Computer Science), Vol. 10422. Springer-Verlag, New York City, NY, USA, 382–404.Google Scholar
- Philip Wadler and Robert Bruce Findler. 2009. Well-typed programs can’t be blamed. In European Symposium on Programming. Springer, 1–16. Google ScholarDigital Library
- Mitchell Wand. 1987. A simple algorithm and proof for type inference. Fundamenta Informaticae 10 (1987), 115–122.Google ScholarCross Ref
- Ningning Xie, Xuan Bi, and Bruno C. d. S. Oliveira. 2018. Consistent Subtyping for All. In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing, Cham, 3–30.Google Scholar
Index Terms
- Gradual typing: a new perspective
Recommendations
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 ...
Gradual typing with union and intersection types
We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to ...
Abstracting gradual typing
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesLanguage researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and static checking. These efforts consistently demonstrate that designing a satisfactory ...
Comments