Amal Ahmed
Jeremy G. Siek
Philip Wadler
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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 universal type. Ahmed et al. (2011) employ runtime type generation in the polymorphic blame calculus to preserve parametricity, but a proof that it does so has been elusive. Matthews and Ahmed (2008) gave a proof of parametricity for a closely related system that combines ML and Scheme, but later found a flaw in their proof. In this paper we present an improved version of the polymorphic blame calculus and we prove that it satisfies relational parametricity. The proof relies on a step-indexed Kripke logical relation. The step-indexing is required to make the logical relation well-defined in the case for the dynamic type. The possible worlds include the mapping of generated type names to their types and the mapping of type names to relations. We prove the Fundamental Property of this logical relation and that it is sound with respect to contextual equivalence. To demonstrate the utility of parametricity in the polymorphic blame calculus, we derive two free theorems.
Supplemental Material
Available for Download
zip
icfp17-main102-s.zip (601.7 MB)
This artifact contains a typechecker and small-step interpreter for the language in the paper. The interpreter is intended to serve as a reference and a tool with which to understand the operational semantics of the language. Specifically, it demonstrates the manner in which the semantics of our type abstractions preserve parametricity.
- Martín 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. Google Scholar
Digital Library
- M. Abadi, L. Cardelli, B. Pierce, and D. Rémy. 1995. Dynamic typing in polymorphic languages. Journal of Functional Programming 5 (1995), 111–130. Google ScholarCross Ref
- Umut A. Acar, Amal Ahmed, and Matthias Blume. 2008. Imperative Self-Adjusting Computation. In ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California. 309–322. Google ScholarDigital Library
- 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, Andrew W. Appel, Christopher D. Richards, Kedar N. Swadi, Gang Tan, and Daniel C. Wang. 2010. Semantic Foundations for Typed Assembly Languages. ACM Transactions on Programming Languages and Systems 32, 3 (March 2010), 1–67. Google ScholarDigital Library
- Amal Ahmed, Andrew W. Appel, and Roberto Virga. 2003. An Indexed Model of Impredicative Polymorphism and Mutable References. (Jan. 2003). Available at http://www.cs.princeton.edu/∼appel/papers/impred.pdf.Google Scholar
- Amal Ahmed, Derek Dreyer, and Andreas Rossberg. 2009. State-Dependent Representation Independence. In ACM Symposium on Principles of Programming Languages (POPL), Savannah, Georgia. Google ScholarDigital Library
- 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 ScholarDigital Library
- Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. 2017. Technical Report: Theorems for Free for Free: Parametricity, With and Without Types. Technical Report. Perma.cc. https://perma.cc/L74G- 6A8WGoogle Scholar
- Amal Ahmed, Lindsey Kuper, and Jacob Matthews. 2011. Parametric polymorphism through run-time sealing, or, Theorems for low, low prices! (April 2011). Available at http://www.ccs.neu.edu/home/amal/papers/paramseal-tr.pdf.Google Scholar
- Amal Ahmed, Jacob Matthews, Robert Bruce Findler, and Philip Wadler. 2009. Blame for all. In Workshop on Script-to-Program Evolution (STOP). 1–13. Google ScholarDigital Library
- Amal Ahmed, James T. Perconti, Jeremy G. Siek, and Philip Wadler. 2014. Blame for All (revised). (August 2014). draft.Google Scholar
- Amal Jamil Ahmed. 2004. Semantics of Types for Mutable State. Ph.D. Dissertation. Princeton University.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 Scholar
- 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
- Gilad Bracha. 2011. Optional Types in Dart. Google.Google Scholar
- Avik Chaudhuri. 2014. Flow: a static type checker for JavaScript. (2014). http://flowtype.org/Google Scholar
- Matteo Cimini and Jeremy G. Siek. 2016. The Gradualizer: a methodology and algorithm for generating gradual type systems. In Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Matteo Cimini and Jeremy G. Siek. 2017. Automatically Generating the Dynamic Semantics of Gradually Typed Languages. In Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. 2012. Complete Monitors for Behavioral Contracts. In European Symposium on Programming (ESOP). 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 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
- Jean-Yves Girard. 1972. Interprétation Fonctionnelle et Élimination des Coupures de l’Arithmétique d’Ordre Supérieur. Thèse de doctorat d’état. Université Paris VII, Paris, France.Google Scholar
- Michael Greenberg. 2013. Manifest Contracts. Ph.D. Dissertation. University of Pennsylvania.Google Scholar
- Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich. 2010. Contracts made manifest. In ACM Symposium on Principles of Programming Languages (POPL), Madrid, Spain. 353–364. 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
- Dan Grossman, Greg Morrisett, and Steve Zdancewic. 2000. Syntactic Type Abstraction. ACM Transactions on Programming Languages and Systems 22, 6 (Nov. 2000), 1037–1080. Google ScholarDigital Library
- Arjun Guha, Jacob Matthews, Robert Bruce Findler, and Shriram Krishnamurthi. 2007. Relationally-Parametric Polymorphic Contracts. In Dynamic Languages Symposium (DLS). 29–40. Google ScholarDigital Library
- Robert Harper. 2013. Practical Foundations for Programming Languages. Cambridge University Press.Google Scholar
- Anders Hejlsberg. 2010. C# 4.0 and beyond by Anders Hejlsberg. Microsoft Channel 9 Blog. (April 2010).Google Scholar
- Anders Hejlsberg. 2012. Introducing TypeScript. Microsoft Channel 9 Blog. (2012).Google Scholar
- Fritz Henglein. 1994. Dynamic typing: syntax and proof theory. Science of Computer Programming 22, 3 (June 1994), 197–230. Google ScholarDigital Library
- Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017. On Polymorphic Gradual Typing. Proc. ACM Program. Lang. 1, ICFP, Article 40 (Sept. 2017), 29 pages. DOI: 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
- Xavier Leroy and Michel Mauny. 1991. Dynamics in ML. Springer Berlin Heidelberg, Berlin, Heidelberg, 406–426. DOI: Google ScholarCross Ref
- Jacob Matthews and Amal Ahmed. 2008. Parametric polymorphism through run-time sealing, or, Theorems for low, low prices!. In European Symposium on Programming (ESOP). 16–31. Google ScholarCross Ref
- Jacob Matthews and Robert Bruce Findler. 2007. Operational Semantics for Multi-Language Programs. In ACM Symposium on Principles of Programming Languages (POPL), Nice, France. 3–10. Google ScholarDigital Library
- James H. Morris. 1968. Lambda-calculus Models of Programming Languages. Ph.D. Dissertation. MIT, Cambridge, MA, USA.Google Scholar
- James H. Morris, Jr. 1973. Protection in Programming Languages. Commun. ACM 16, 1 (Jan. 1973), 15–21. Google ScholarDigital Library
- Georg Neis, Derek Dreyer, and Andreas Rossberg. 2009. Non-Parametric Parametricity. In International Conference on Functional Programming (ICFP), Edinburgh, Scotland. 135–148. Google ScholarDigital Library
- Georg Neis, Derek Dreyer, and Andreas Rossberg. 2011. Non-parametric parametricity. Journal of Functional Programming 21 (2011), 497–562. Google ScholarDigital Library
- Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. 2004. Dynamic Typing with Dependent Types. In IFIP International Conference on Theoretical Computer Science. 437–450. Google ScholarCross Ref
- Benjamin Pierce and Eijiro Sumii. 2000. Relating cryptography and polymorphism. (2000). www.cis.upenn.edu/~bcpierce/ papers/infohide.ps Manuscript.Google Scholar
- Andrew M. Pitts. 1998a. Existential Types: Logical Relations and Operational Equivalence. Lecture Notes in Computer Science 1443 (1998), 309–326. Google ScholarCross Ref
- Andrew M. Pitts. 1998b. Existential types: Logical relations and operational equivalence. Springer Berlin Heidelberg, Berlin, Heidelberg, 309–326. DOI: Google ScholarCross Ref
- Andrew M. Pitts and Ian D. B. Stark. 1993. Observable Properties of Higher Order Functions That Dynamically Create Local Names, or What’s New?. In Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science (MFCS ’93). Springer-Verlag, London, UK, UK, 122–141. Google ScholarCross Ref
- John C. Reynolds. 1974. Towards a Theory of Type Structure. In Programming Symposium (LNCS), Vol. 19. Springer-Verlag, 408–425. Google ScholarCross Ref
- John C. Reynolds. 1983. Types, abstraction, and parametric polymorphism. Information Processing (1983), 513–523.Google Scholar
- Andreas Rossberg. 2003. Generativity and dynamic opacity for abstract types. In ACM Conference on Principles and Practice of Declarative Programming (PPDP). 241–252. Google ScholarDigital Library
- Andreas Rossberg. 2006. The Missing Link: Dynamic Components for ML. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’06). ACM, New York, NY, USA, 99–110. DOI: Google ScholarDigital Library
- Taro Sekiyama, Atsushi Igarashi, and Michael Greenberg. 2017. Polymorphic Manifest Contracts, Revised and Resolved. ACM Trans. Program. Lang. Syst. 39, 1, Article 3 (Feb. 2017), 36 pages. DOI: Google ScholarDigital Library
- Peter Sewell. 2001. Modules, Abstract Types, and Distributed Versioning. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’01). ACM, New York, NY, USA, 236–247. Google ScholarDigital Library
- 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, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In SNAPL: Summit on Advances in Programming Languages (LIPIcs: Leibniz International Proceedings in Informatics).Google Scholar
- Jeremy G. Siek and Philip Wadler. 2010. Threesomes, with and without blame. In ACM Symposium on Principles of Programming Languages (POPL). 365–376. Google ScholarDigital Library
- Jeremy G. Siek and Philip Wadler. 2016. The key to blame: Gradual typing meets cryptography. (July 2016). http://homepages. inf.ed.ac.uk/wadler/topics/blame.html#blame- key (draft).Google Scholar
- Ian Stark. 1995. Names and Higher-Order Functions. Ph.D. Dissertation. University of Cambridge.Google Scholar
- Richard Statman. 1991. A local translation of untyped [lambda] calculus into simply typed [lambda] calculus. Technical Report. Carnegie-Mellon University.Google Scholar
- Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. 2007. System F with type equality coercions. In TLDI ’07: Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation. ACM, New York, NY, USA, 53–66. Google ScholarDigital Library
- Eijiro Sumii and Benjamin Pierce. 2003. Logical relations for encryption. J. Comput. Secur. 11, 4 (July 2003), 521–554. Google ScholarCross Ref
- 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
- Asumu Takikawa, T. Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. 2012. Gradual Typing for First-Class Classes. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA). 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
- Sam Tobin-Hochstadt and Matthias Felleisen. 2010. Logical Types for Untyped Languages. In International Conference on Functional Programming (ICFP). ACM, 117–128. Google ScholarDigital Library
- Jonathan Turner. 2014. TypeScript and the Road to 2.0. (October 2014). https://blogs.msdn.microsoft.com/typescript/2014/ 10/22/typescript- and- the- road- to- 2- 0/Google Scholar
- Julien Verlaguet. 2013. Facebook: Analyzing PHP statically. In Commercial Users of Functional Programming (CUFP).Google Scholar
- Philip Wadler. 1989. Theorems for free!. In ACM Symposium on Functional Programming Languages and Computer Architecture (FPCA). 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
- Andrew K. Wright. 1995. Simple Imperative Polymorphism. Higher-Order and Symbolic Computation 8, 4 (Dec. 1995), 343–355. Google ScholarDigital Library
Index Terms
- Theorems for free for free: parametricity, with and without types
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 ...
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 ...
Equivalences for free: univalent parametricity for effective transport
Homotopy Type Theory promises a unification of the concepts of equality and equivalence in Type Theory, through the introduction of the univalence principle. However, existing proof assistants based on type theory treat this principle as an axiom, and it ...
Comments