Gradual parametricity, revisited

Abstract

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 proposed. Among other issues, these proposals can however signal parametricity errors in unexpected situations, and improperly handle type instantiations when imprecise types are involved. These observations further suggest that existing polymorphic cast calculi are not well suited for supporting a gradual counterpart of System F. Consequently, we revisit the challenge of designing a gradual language with explicit parametric polymorphism, exploring the extent to which the Abstracting Gradual Typing methodology helps us derive such a language, GSF. We present the design and metatheory of GSF, and provide a reference implementation. In addition to avoiding the uncovered semantic issues, GSF satisfies all the expected properties of a gradual parametric language, save for one property: the dynamic gradual guarantee, which was left as conjecture in all prior work, is here proven to be simply incompatible with parametricity. We nevertheless establish a weaker property that allows us to disprove several claims about gradual free theorems, clarifying the kind of reasoning supported by gradual parametricity.

References

1. Martin Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. 1991. Dynamic typing in a statically typed language. ACM Transactions on Programming Languages and Systems 13, 2 (April 1991), 237–268.
2. Martin Abadi, Luca Cardelli, Benjamin Pierce, and Didier Rémy. 1995. Dynamic typing in polymorphic languages. Journal of Functional Programming 5, 1 (1995), 111–130.
3. Amal Ahmed, Robert Bruce Findler, Jacob Matthews, and Philip Wadler. 2009. Blame for All. In Workshop on Script to Program Evolution (STOP). Genova, Italy.
4. Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011. Blame for All. In Proceedings of the 38th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2011). ACM Press, Austin, Texas, USA, 201–214.
5. Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for Free for Free: Parametricity, with and Without Types. See{ ICFP 2017 2017 }, 39:1–39:28.
6. Johannes Bader, Jonathan Aldrich, and Éric Tanter. 2018. Gradual Program Verification. In Proceedings of the 19th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2018) (Lecture Notes in Computer Science), Işil Dillig and Jens Palsberg (Eds.), Vol. 10747. Springer-Verlag, Los Angeles, CA, USA, 25–46.
7. Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. 2014. A Theory of Gradual Effect Systems. In Proceedings of the 19th ACM SIGPLAN Conference on Functional Programming (ICFP 2014). ACM Press, Gothenburg, Sweden, 283–295.
8. Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. 2016. Gradual Type-and-Effect Systems. Journal of Functional Programming 26 (Sept. 2016), 19:1–19:69.
9. Gavin Bierman, Erik Meijer, and Mads Torgersen. 2010. Adding Dynamic Types to C # . In Proceedings of the 24th European Conference on Object-oriented Programming (ECOOP 2010) (Lecture Notes in Computer Science), Theo D’Hondt (Ed.). Springer-Verlag, Maribor, Slovenia, 76–100.
10. Robert Cartwright and Mike Fagan. 1991. Soft typing. In Proceedings of the ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI). Toronto, Ontario, Canada, 278–292.
11. Giuseppe Castagna and Victor Lanvin. 2017. Gradual Typing with Union and Intersection Types. See{ ICFP 2017 2017 }, 41:1–41:28.
12. Haskell B. Curry, J. Roger Hindley, and J. P. Seldin. 1972. Combinatory Logic, Volume II. Studies in logic and the foundations of mathematics, Vol. 65. North-Holland Pub. Co.
13. Dominique Devriese, Marco Patrignani, and Frank Piessens. 2018. Parametricity versus the universal type. Proceedings of the ACM on Programming Languages 2, POPL (Jan. 2018), 38:1–38:23.
14. Tim Disney and Cormac Flanagan. 2011. Gradual information flow typing. In International Workshop on Scripts to Programs.
15. Luminous Fennell and Peter Thiemann. 2013. Gradual Security Typing with References. In Proceedings of the 26th Computer Security Foundations Symposium (CSF). 224–239.
16. Luminous Fennell and Peter Thiemann. 2016. LJGS: Gradual Security Types for Object-Oriented Languages. In Proceedings of the 30th European Conference on Object-Oriented Programming (ECOOP 2016) (Leibniz International Proceedings in Informatics (LIPIcs)), Shriram Krishnamurthi and Benjamin S. Lerner (Eds.), Vol. 56. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Rome, Italy, 9:1–9:26.
17. Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting Gradual Typing. In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016). ACM Press, St Petersburg, FL, USA, 429–442.
18. Ronald Garcia and Éric Tanter. 2015. Deriving a Simple Gradual Security Language. eprint arXiv:1511.01399.
19. Ronald Garcia, Éric Tanter, Roger Wolff, and Jonathan Aldrich. 2014. Foundations of Typestate-Oriented Programming. ACM Transactions on Programming Languages and Systems 36, 4, Article 12 (Oct. 2014), 12:1–12:44 pages.
20. Jean-Yves Girard. 1972. Interprétation Fonctionnelle et Élimination des Coupures de l’Arithmétique d’Ordre Supérieur. Ph.D. Dissertation. Université de Paris VII, Paris, France.
21. Arjun Guha, Jacob Matthews, Robert Bruce Findler, and Shriram Krishnamurthi. 2007. Relationally-parametric polymorphic contracts. In Proceedings of the ACM Dynamic Languages Symposium (DLS 2007). ACM Press, Montreal, Canada, 29–40.
22. David Herman, Aaron Tomb, and Cormac Flanagan. 2010. Space-efficient gradual typing. Higher-Order and Sympolic Computation 23, 2 (June 2010), 167–189.
23. Kuen-Bang Hou, Nick Benton, and Robert Harper. 2016. Correctness of Compiling Polymorphism to Dynamic Typing. Journal of Functional Programming 27 (2016), 1:1–1:24.
24. ICFP 2017 2017.
25. Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, and Philip Wadler. 2017b. Gradual Session Types. See{ ICFP 2017 2017 }, 38:1–38:28.
26. Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017a. On Polymorphic Gradual Typing. See{ ICFP 2017 2017 }, 40:1–40:29.
27. Lintaro Ina and Atsushi Igarashi. 2011. Gradual typing for generics. In Proceedings of the 26th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2011). ACM Press, Portland, Oregon, USA, 609–624.
28. Nico Lehmann and Éric Tanter. 2017. Gradual Refinement Types. In Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017). ACM Press, Paris, France, 775–788.
29. Xavier Leroy and Michel Mauny. 1991. Dynamics in ML. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture (FPCA 1991) (Lecture Notes in Computer Science), Vol. 523. Springer-Verlag, 406–426.
30. Jacob Matthews and Amal Ahmed. 2008. Parametric Polymorphism Through Run-Time Sealing, or, Theorems for Low, Low Prices!. In Proceedings of the 17th European Symposium on Programming Languages and Systems (ESOP 2008) (Lecture Notes in Computer Science), Sophia Drossopoulou (Ed.), Vol. 4960. Springer-Verlag, Budapest, Hungary, 16–31.
31. Jacob Matthews and Robert Bruce Findler. 2007. Operational Semantics for Multi-language programs. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007). ACM Press, Nice, France, 3–10.
32. John C. Mitchell. 1988. Polymorphic Type Inference and Containment. Information and Computation 76, 2-3 (Feb. 1988), 211–249.
33. James H. Morris. 1973. Protection in Programming Languages. Commun. ACM 16, 1 (Jan. 1973), 15–21.
34. Fabian Muehlboeck and Ross Tate. 2017. Sound gradual typing is nominally alive and well. , 56:1–56:30 pages.
35. Georg Neis, Derek Dryer, and Andreas Rossberg. 2009. Non-Parametric Parametricity. In Proceedings of the 14th ACM SIGPLAN Conference on Functional Programming (ICFP 2009). ACM Press, Edinburgh, Scotland, UK, 135–148.
36. Max S. New and Amal Ahmed. 2018. Graduality from Embedding-Projection Pairs. , 73:1–73:30 pages.
37. Martin Odersky and Konstantin Läufer. 1996. Putting Type Annotations to Work. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 96). ACM Press, St. Petersburg Beach, Florida, USA, 54–67.
38. Benjamin Pierce and Eijiro Sumii. 2000. Relating Cryptography and Polymorphism. Manuscript.
39. Benjamin C. Pierce. 2002. Types and programming languages. MIT Press, Cambridge, MA, USA.
40. Aseem Rastogi, Avik Chaudhuri, and Basil Hosmer. 2012. The ins and outs of gradual type inference. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012). ACM Press, Philadelphia, USA, 481–494.
41. John C. Reynolds. 1974. Towards a Theory of Type Structure. In Porceedings of the Programming Symposium (Lecture Notes in Computer Science), Vol. 19. Springer-Verlag, 408–423.
42. John C. Reynolds. 1983. Types, abstraction, and parametric polymorphism. In Information Processing 83, R. E. A. Mason (Ed.). Elsevier, 513–523.
43. Andreas Rossberg. 2003. Generativity and dynamic opacity for abstract types. In Proceedings of the 5th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2003). 241–252.
44. Ilya Sergey and Dave Clarke. 2012. Gradual Ownership Types. In Proceedings of the 21st European Symposium on Programming Languages and Systems (ESOP 2012) (Lecture Notes in Computer Science), Helmut Seidl (Ed.), Vol. 7211. Springer-Verlag, Tallinn, Estonia, 579–599.
45. Jeremy Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Proceedings of the Scheme and Functional Programming Workshop. 81–92.
46. Jeremy Siek and Walid Taha. 2007. Gradual Typing for Objects. In Proceedings of the 21st European Conference on Objectoriented Programming (ECOOP 2007) (Lecture Notes in Computer Science), Erik Ernst (Ed.). Springer-Verlag, Berlin, Germany, 2–27.
47. Jeremy 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 2010). ACM Press, Madrid, Spain, 365–376.
48. Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015a. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 32. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Asilomar, California, USA, 274–293.
49. Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. 2015b. Monotonic References for Efficient Gradual Typing. In Proceedings of the 24th European Symposium on Programming Languages and Systems (ESOP 2015) (Lecture Notes in Computer Science), Jan Vitek (Ed.), Vol. 9032. Springer-Verlag, London, UK, 432–456.
50. Sam Tobin-Hochstadt and Matthias Felleisen. 2006. Interlanguage migration: from scripts to programs. In Proceedings of the ACM Dynamic Languages Symposium (DLS 2006). ACM Press, Portland, Oregon, USA, 964–974.
51. Matías Toro, Ronald Garcia, and Éric Tanter. 2018a. Type-Driven Gradual Security with References. ACM Transactions on Programming Languages and Systems 40, 4 (Nov. 2018), 16:1–16:55.
52. Matías Toro, Elizabeth Labrada, and Éric Tanter. 2018b. Gradual Parametricity, Revisited (with Appendix). arXiv:1807.04596 {cs.PL}.
53. 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.
54. Philip Wadler. 1989. Theorems for Free!. In Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture (FPCA ’89). ACM, London, United Kingdom, 347–359.
55. Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. 2011. Gradual Typestate. In Proceedings of the 25th European Conference on Object-oriented Programming (ECOOP 2011) (Lecture Notes in Computer Science), Mira Mezini (Ed.), Vol. 6813. Springer-Verlag, Lancaster, UK, 459–483.
56. Ningning Xie, Xuan Bi, and Bruno C. d. S. Oliveira. 2018. Consistent Subtyping for All. In Proceedings of the 27th European Symposium on Programming Languages and Systems (ESOP 2018) (Lecture Notes in Computer Science), Amal Ahmed (Ed.), Vol. 10801. Springer-Verlag, Thessaloniki, Greece, 3–30.

Index Terms

• Theory of computation

  • Semantics and reasoning

    • Program constructs

      • Type structures

    • Program semantics