Giuseppe Castagna
Victor Lanvin
Abstract
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 gradual ones and likewise for the subtyping relation. We also show that deciding subtyping for gradual types can be reduced in linear time to deciding subtyping on non-gradual types and that the same holds true for all subtyping-related decision problems that must be solved for type inference. More generally, this work not only enriches gradual type systems with unions and intersections and with the type precision that arise from their use, but also proposes and advocates a new style of gradual types programming where union and intersection types are used by programmers to instruct the system to perform fewer dynamic checks.
Supplemental Material
Available for Download
Appendix containing extra definitions lemmas and proofs
- Véronique Benzaken, Giuseppe Castagna, and Alain Frisch. 2003. CDuce: an XML-centric general-purpose language. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP ’03). ACM, 51–63. Google Scholar
Digital Library
- Giuseppe Castagna. 2015. Covariance and Contravariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers). (2015). Unpublished manuscript, available at the author’s web page.Google Scholar
- Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. 1995. A calculus for overloaded functions with subtyping. Information and Computation 117, 1 (1995), 115–135. 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, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, and Luca Padovani. 2014. Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation. In Proceedings of the 41st ACM Symposium on Principles of Programming Languages (POPL ’14). ACM, 5–17. 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 ’16). ACM, 378–391. Google ScholarDigital Library
- Avik Chaudhuri. 2014. Flow: A static type checker for JavaScript. Facebook. https://flowtype.org .Google Scholar
- Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL ’77). ACM, 238–252. Google ScholarDigital Library
- Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. 2012. Complete Monitors for Behavioral Contracts. In Programming Languages and Systems - 21st European Symposium on Programming, ESOP´’12. 214–233. Google ScholarDigital Library
- Alain Frisch. 2004. Regular Tree Language Recognition with Static Information. In IFIP 18th World Computer Congress TC1, 3rd International Conference on Theoretical Computer Science (TCS2004) (IFIP), Vol. 155. Kluwer/Springer, 661–674. Google ScholarCross Ref
- 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
- 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
- Khurram A. Jafery and Joshua Dunfield. 2017. Sums of Uncertainty: Refinements Go Gradual. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL ’17). ACM, 804–817. Google ScholarDigital Library
- Nico Lehmann and Éric Tanter. 2017. Gradual refinement types. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL ’17). ACM, 18–20. Google ScholarDigital Library
- John C. Reynolds. 1996. Design of the Programming Language Forsythe. Technical Report CMU-CS-96-146. Carnegie Mellon University.Google Scholar
- 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 Sam Tobin-Hochstadt. 2016. The Recursive Union of Some Gradual Types. In A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, Sam Lindley, Conor McBride, Phil Trinder, and Don Sannella (Eds.). Springer, 388–410. Google ScholarCross Ref
- Jeremy G. Siek and Manish Vachharajani. 2008. Gradual typing with unification-based inference. In Proceedings of the 2008 Symposium on Dynamic languages. ACM, 7. Google ScholarDigital Library
- 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, Vol. 32. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.Google Scholar
- Jeremy G. Siek and Philip Wadler. 2010. Threesomes, with and Without Blame. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’10). ACM, 365–376. 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
- Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The Design and Implementation of Typed Scheme. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’08). ACM, 395–406. 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 (LNCS). Springer, 1–16. Google ScholarDigital Library
- Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation 115, 1 (1994), 38 – 94. Google ScholarDigital Library
Index Terms
- Gradual typing with union and intersection types
Recommendations
Gradual typing: a new perspective
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 ...
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 ...
Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types
Subtyping relations are usually defined either syntactically by a formal system or semantically by an interpretation of types into an untyped denotational model. This work shows how to define a subtyping relation semantically in the presence of Boolean ...
Comments