Abstract
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 that giving components of a program more precise types only adds runtime type checking, and does not otherwise change behavior. In this paper, we give a semantic reformulation of the gradual guarantee called graduality. We change the name to promote the analogy that graduality is to gradual typing what parametricity is to polymorphism. Each gives a local-to-global, syntactic-to-semantic reasoning principle that is formulated in terms of a kind of observational approximation.
Utilizing the analogy, we develop a novel logical relation for proving graduality. We show that embedding-projection pairs (ep pairs) are to graduality what relations are to parametricity. We argue that casts between two types where one is “more dynamic” (less precise) than the other necessarily form an ep pair, and we use this to cleanly prove the graduality cases for casts from the ep-pair property. To construct ep pairs, we give an analysis of the type dynamism relation—also known as type precision or naïve subtyping—that interprets the rules for type dynamism as compositional constructions on ep pairs, analogous to the coercion interpretation of subtyping.
Supplemental Material
- Amal Ahmed. 2006. Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In European Symposium on Programming (ESOP). 69–83. 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 International Conference on Functional Programming (ICFP), Oxford, United Kingdom.Google Scholar
- Esteban Allende, Oscar Callaú, Johan Fabry, Éric Tanter, and Marcus Denker. 2013. Gradual Typing for Smalltalk. Science of Computer Programming (Aug. 2013). Available online. Google ScholarDigital Library
- Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. 2014. A Theory of Gradual Effect Systems. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP ’14). 283–295. Google ScholarDigital Library
- Nick Benton. 2005. Embedded Interpreters. Journal of Functional Programming 15, 04 (2005), 503–542. Google ScholarDigital Library
- John Tang Boyland. 2014. The Problem of Structural Type Tests in a Gradual-Typed Language. In Workshop on Foundations of Object-Oriented Languages (FOOL), informal proceedings.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 Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). Google ScholarDigital Library
- Matteo Cimini and Jeremy G. Siek. 2017. Automatically Generating the Dynamic Semantics of Gradually Typed Languages. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). 789–803. Google ScholarDigital Library
- Pierre-Evariste Dagand, Nicolas Tabareau, and Éric Tanter. 2016. Partial Type Equivalences for Verified Dependent Interoperability (ICFP 2016). 298–310. Google ScholarDigital Library
- Pierr-Évariste Dagand, Nicolas Tabareau, and Éric Tanter. 2018. Foundations of dependent interoperability. Journal of Functional Programming 28 (2018), e9.Google ScholarCross Ref
- Keun-Bang Hou (Favonia), Nick Benton, and Robert Harper. 2017. Correctness of compiling polymorphism to dynamic typing. Journal of Functional Programming 27 (2017).Google Scholar
- Matthias Felleisen and Robert Hieb. 1992. A Revised Report on the Syntactic Theories of Sequential Control and State. Theor. Comput. Sci. 103, 2 (1992), 235–271. Google ScholarDigital Library
- Robby Findler and Matthias Blume. 2006. Contracts as Pairs of Projections. In International Symposium on Functional and Logic Programming (FLOPS). Google ScholarDigital Library
- Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for higher-order functions. In International Conference on Functional Programming (ICFP), Pittsburgh, Pennsylvania. 48–59. Google ScholarDigital Library
- Ronald Garcia, Alison M. Clark, and Eric Tanter. 2016a. Abstracting Gradual Typing. In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg, Florida. Google ScholarDigital Library
- Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016b. Abstracting Gradual Typing. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). Google ScholarDigital Library
- Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. 2006. Sage: Hybrid Checking for Flexible Specifications. In Scheme and Functional Programming Workshop (Scheme). 93–104.Google Scholar
- Fritz Henglein. 1994. Dynamic Typing: Syntax and Proof Theory. Science of Computer Programming 22, 3 (1994), 197–230. Google ScholarDigital Library
- David Herman, Aaron Tomb, and Cormac Flanagan. 2010. Space-efficient Gradual Typing. Higher Order Symbol. Comput. 23, 2 (June 2010). Google ScholarDigital Library
- Atsushi Igarashi, Peter Thiemann, Vasco Vasconcelos, and Philip Wadler. 2017b. Gradual Session Types. In International Conference on Functional Programming (ICFP), Oxford, United Kingdom.Google Scholar
- Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017a. On Polymorphic Gradual Typing. In International Conference on Functional Programming (ICFP), Oxford, United Kingdom.Google Scholar
- 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
- Nico Lehmann and Éric Tanter. 2017. Gradual Refinement Types. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). 775–788. Google ScholarDigital Library
- Max S. New and Amal Ahmed. 2018. Graduality from Embedding-Projection Pairs (Extended Version). ArXiv e-prints (July 2018). arXiv: 1807.02786Google Scholar
- Max S. New and Daniel R. Licata. 2018. Call-by-Name Gradual Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) (Leibniz International Proceedings in Informatics (LIPIcs)), Hélène Kirchner (Ed.), Vol. 108. http://drops.dagstuhl.de/opus/volltexte/2018/9194Google Scholar
- Dana Scott. 1972. Continuous lattices. In Toposes, algebraic geometry and logic. 97–136.Google Scholar
- Jeremy Siek, Micahel Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015).Google Scholar
- Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop (Scheme). 81–92.Google Scholar
- Jeremy G. Siek and Philip Wadler. 2010. Threesomes, with and without blame. In ACM Symposium on Principles of Programming Languages (POPL), Madrid, Spain. 365–376. Google ScholarDigital Library
- Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, and Gavin M. Bierman. 2014. Gradual typing embedded securely in JavaScript. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, California. 425–438. Google ScholarDigital Library
- Satish Thatte. 1990. Quasi-static typing. In ACM Symposium on Principles of Programming Languages (POPL). 367–381. Google ScholarDigital Library
- Sam Tobin-Hochstadt and Matthias Felleisen. 2006. Interlanguage Migration: From Scripts to Programs. In Dynamic Languages Symposium (DLS). 964–974.Google ScholarDigital Library
- Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The Design and Implementation of Typed Scheme. In ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California. Google ScholarDigital Library
- Philip Wadler and Robert Bruce Findler. 2009. Well-typed programs can’t be blamed. In European Symposium on Programming (ESOP). 1–16. Google ScholarDigital Library
- Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. 2011. Gradual Typestate. In Proceedings of the 25th European Conference on Object-oriented Programming (ECOOP’11). Google ScholarDigital Library
Index Terms
- Graduality from embedding-projection pairs
Recommendations
Graduality and parametricity: together again for the first time
Parametric polymorphism and gradual typing have proven to be a difficult combination, with no language yet produced that satisfies the fundamental theorems of each: parametricity and graduality. Notably, Toro, Labrada, and Tanter (POPL 2019) conjecture ...
Consistent Subtyping for All
Special Issue on ESOP 2018Consistent 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 ...
Gradually Typed Languages Should Be Vigilant!
In gradual typing, different languages perform different dynamic type checks for the same program even though the languages have the same static type system. This raises the question of whether, given a gradually typed language, the combination of the ...
Comments