Max S. New
Abstract
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 that for any gradual extension of System F that uses dynamic type generation, graduality and parametricity are ``simply incompatible''. However, we argue that it is not graduality and parametricity that are incompatible per se, but instead that combining the syntax of System F with dynamic type generation as in previous work necessitates type-directed computation, which we show has been a common source of graduality and parametricity violations in previous work.
We then show that by modifying the syntax of universal and existential types to make the type name generation explicit, we remove the need for type-directed computation, and get a language that satisfies both graduality and parametricity theorems. The language has a simple runtime semantics, which can be explained by translation to a statically typed language where the dynamic type is interpreted as a dynamically extensible sum type. Far from being in conflict, we show that the parametricity theorem follows as a direct corollary of a relational interpretation of the graduality property.
Supplemental Material
- Amal Ahmed, Derek Dreyer, and Andreas Rossberg. 2009. State-Dependent Representation Independence. In ACM Symposium on Principles of Programming Languages (POPL), Savannah, Georgia.Google Scholar
- Amal Ahmed, Robert Bruce Findler, Jeremy Siek, and Philip Wadler. 2011. Blame for All. In ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas. 201–214.Google Scholar
- 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
- 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
- John Boyland. 2014. The Problem of Structural Type Tests in a Gradually-Typed Language. In 21st Workshop on Foundations of Object-Oriented Languages.Google Scholar
- Giuseppe Castagna and Victor Lanvin. 2017. Gradual Typing with Union and Intersection Types. Proc. ACM Program. Lang. 1, ICFP, Article 41 (Aug. 2017), 28 pages. Google ScholarDigital Library
- Tim Disney and Cormac Flanagan. 2011. Gradual Information Flow Typing. In Workshop on Script-to-Program Evolution (STOP).Google Scholar
- Brian Patrick Dunphy. 2002. Parametricity As a Notion of Uniformity in Reflexive Graphs. Ph.D. Dissertation. Champaign, IL, USA. Advisor(s) Reddy, Uday.Google Scholar
- Matthias Felleisen. 1990. On the expressive power of programming languages. ESOP’90 (1990).Google Scholar
- Luminous Fennell and Peter Thiemann. 2013. Gradual Security Typing with References. In CSF. IEEE Computer Society, 224–239.Google Scholar
- Ronald Garcia and Matteo Cimini. 2015. Principal Type Schemes for Gradual Programs (POPL ’15).Google Scholar
- Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting Gradual Typing. In ACM Symposium on Principles of Programming Languages (POPL).Google Scholar
- Atsushi Igarashi, Peter Thiemann, Vasco Vasconcelos, and Philip Wadler. 2017b. Gradual Session Types. In International Conference on Functional Programming (ICFP).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 ACM Symposium on Principles of Programming Languages (POPL).Google Scholar
- Paul Blain Levy. 2003. Call-By-Push-Value: A Functional/Imperative Synthesis. Springer.Google Scholar
- QingMing Ma and John C. Reynolds. 1991. Types, Abstractions, and Parametric Polymorphism, Part 2. In Mathematical Foundations of Programming Semantics, 7th International Conference, Pittsburgh, PA, USA.Google Scholar
- John C. Mitchell and Gordon D. Plotkin. 1985. Abstract types have existential type. In ACM Symposium on Principles of Programming Languages (POPL), New Orleans, Louisiana.Google Scholar
- Georg Neis, Derek Dreyer, and Andreas Rossberg. 2009. Non-Parametric Parametricity. In International Conference on Functional Programming (ICFP). 135–148.Google Scholar
- Max S. New and Amal Ahmed. 2018. Graduality from Embedding-Projection Pairs. In International Conference on Functional Programming (ICFP), St. Louis, Missouri.Google Scholar
- Max S. New, Dustin Jamner, and Amal Ahmed. 2020. Technical Appendix to Graduality and Parametricity: Together Again for the First Time. http://www.ccs.neu.edu/home/amal/papers/gradparam- tr.pdfGoogle Scholar
- Max S. New, Daniel R. Licata, and Amal Ahmed. 2019. Gradual Type Theory (POPL ’19).Google Scholar
- Gordon Plotkin and Martín Abadi. 1993. A logic for parametric polymorphism. Typed Lambda Calculi and Applications (1993), 361–375.Google Scholar
- John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France.Google Scholar
- Amr Sabry and Matthias Felleisen. 1992. Reasoning about Programs in Continuation-Passing Style. In Conf. on LISP and functional programming, LFP ’92.Google ScholarDigital Library
- Ilya Sergey and Dave Clarke. 2012. Gradual Ownership Types. In ESOP (Lecture Notes in Computer Science), Vol. 7211. Springer, 579–599.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.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 Walid Taha. 2007. Gradual Typing for Objects. In European Conference on Object-Oriented Programming (ECOOP).Google ScholarDigital Library
- Eijiro Sumii and Benjamin C. Pierce. 2004. A Bisimulation for Dynamic Sealing. In ACM Symposium on Principles of Programming Languages (POPL), Venice, Italy.Google Scholar
- Asumu Takikawa, T. Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. 2012. Gradual typing for first-class classes (ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA)).Google Scholar
- 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 Scholar
- Sam Tobin-Hochstadt, Vincent St-Amour, Eric Dobson, and Asumu Takikawa. [n. d.]. Typed Racket Reference. https: //docs.racket- lang.org/ts- reference/Typed_Units.html Accessed: 2019-10-30.Google Scholar
- Matías Toro, Ronald Garcia, and Éric Tanter. 2018. Type-Driven Gradual Security with References. ACM Transactions on Programming Languages and Systems 40, 4 (Dec. 2018). Google ScholarDigital Library
- Matías Toro, Elizabeth Labrada, and Éric Tanter. 2019. Gradual Parametricity, Revisited. Proc. ACM Program. Lang. 3, POPL, Article 17 (Jan. 2019), 30 pages. 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
- 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
- Graduality and parametricity: together again for the first time
Recommendations
Gradual type theory
Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type soundness theorems for these languages aim to show that type-based ...
Gradual parametricity, revisited
Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, while preserving relational parametricity, has proven extremely challenging: first attempts were formulated a decade ago, and several designs were recently ...
Theorems for free for free: parametricity, with and without types
The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamically-typed code should satisfy it once it has been cast to a ...
Comments