Yusuke Miyazaki
Abstract
Garcia and Cimini study a type inference problem for the ITGL, an implicitly and gradually typed language with let-polymorphism, and develop a sound and complete inference algorithm for it. Soundness and completeness mean that, if the algorithm succeeds, the input term can be translated to a well-typed term of an explicitly typed blame calculus by cast insertion and vice versa. However, in general, there are many possible translations depending on how type variables that were left undecided by static type inference are instantiated with concrete static types. Worse, the translated terms may behave differently—some evaluate to values but others raise blame.
In this paper, we propose and formalize a new blame calculus λBDTI that avoids such divergence as an intermediate language for the ITGL. A main idea is to allow a term to contain type variables (that have not been instantiated during static type inference) and defer instantiation of these type variables to run time. We introduce dynamic type inference (DTI) into the semantics of λBDTI so that type variables are instantiated along reduction. The DTI-based semantics not only avoids the divergence described above but also is sound and complete with respect to the semantics of fully instantiated terms in the following sense: if the evaluation of a term succeeds (i.e., terminates with a value) in the DTI-based semantics, then there is a fully instantiated version of the term that also succeeds in the explicitly typed blame calculus and vice versa.
Finally, we prove the gradual guarantee, which is an important correctness criterion of a gradually typed language, for the ITGL.
Supplemental Material
- Martín Abadi, Luca Cardelli, Benjamin C. Pierce, and Gordon D. Plotkin. 1991. Dynamic Typing in a Statically Typed Language. ACM Transactions on Programming Languages and Systems 13, 2 (1991), 237–268. Google Scholar
Digital Library
- Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011. Blame for all. In Proc. of ACM POPL. 201–214.Google ScholarDigital Library
- Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for free for free: parametricity, with and without types. PACMPL 1, ICFP (2017), 39:1–39:28. Google ScholarDigital Library
- Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. 2014. A theory of gradual effect systems. In Proc. of ACM ICFP. 283–295. Google ScholarDigital Library
- Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. 2016. Gradual type-and-effect systems. Journal of Functional Programming 26 (2016), e19.Google ScholarCross Ref
- Alan Bawden. 1999. Quasiquotation in Lisp. In Proc. of ACM PEPM. 4–12.Google Scholar
- Nikolaj Skallerud Bjørner. 1994. Minimal Typing Derivations. In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications. 120–126.Google Scholar
- Gilad Bracha and David Griswold. 1993. Strongtalk: Typechecking Smalltalk in a Production Environment. In Proc. of ACM OOPSLA. 215–230. Google ScholarDigital Library
- Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. 1991. Inheritance as Implicit Coercion. Inf. Comput. 93, 1 (1991), 172–221. Google ScholarDigital Library
- Robert Cartwright and Mike Fagan. 1991. Soft Typing. In Proc. of ACM PLDI. 278–292. Google ScholarDigital Library
- Matteo Cimini and Jeremy G. Siek. 2016. The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems. In Proc. of ACM POPL. 443–455. Google ScholarDigital Library
- Matteo Cimini and Jeremy G. Siek. 2017. Automatically generating the dynamic semantics of gradually typed languages. In Proc. of ACM POPL. 789–803. http://dl.acm.org/citation.cfm?id=3009863 Google ScholarDigital Library
- Rowan Davies. 1996. A Temporal-Logic Approach to Binding-Time Analysis. In Proc. of IEEE LICS. 184–195. Google ScholarDigital Library
- Rowan Davies and Frank Pfenning. 2001. A Modal Analysis of Staged Computation. J. ACM 48, 3 (2001), 555–604. Google ScholarDigital Library
- Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for higher-order functions. In Proc. of ACM ICFP. 48–59. Google ScholarDigital Library
- Cormac Flanagan and Matthias Felleisen. 1999. Componential Set-Based Analysis. ACM Transactions on Programming Languages and Systems 21, 2 (1999), 370–416. Google ScholarDigital Library
- Ronald Garcia and Matteo Cimini. 2015. Principal Type Schemes for Gradual Programs. In Proc. of ACM POPL. 303–315. Google ScholarDigital Library
- Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting gradual typing. In Proc. of ACM POPL. 429–442. Google ScholarDigital Library
- Jacques Garrigue. 2004. Relaxing the Value Restriction. In Proc. of FLOPS (LNCS), Vol. 2998. Springer, 196–213.Google Scholar
- Jean-Yves Girard. 1972. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Thèse d’état. Université Paris VII. Summary in Proc. of the Second Scandinavian Logic Symposium, 1971 (63–92).Google Scholar
- Robert Harper and John C. Mitchell. 1993. On The Type structure of Standard ML. ACM Transactions on Programming Languages and Systems 15, 2 (1993), 211–252. Google ScholarDigital Library
- Fritz Henglein. 1994. Dynamic Typing: Syntax and Proof Theory. Sci. Comput. Program. 22, 3 (1994), 197–230. Google ScholarDigital Library
- Fritz Henglein and Jakob Rehof. 1995. Safe polymorphic type inference for a Dynamically Typed Language: Translating Scheme to ML. In ACM Conference on Functional Programming and Computer Architecture. 192–203. Google ScholarDigital Library
- David Herman, Aaron Tomb, and Cormac Flanagan. 2007. Space-Efficient Gradual Typing. In Proc. of TFP (Trends in Functional Programming), Vol. 8. Intellect, 1–18.Google Scholar
- David Herman, Aaron Tomb, and Cormac Flanagan. 2010. Space-efficient gradual typing. Higher-Order and Symbolic Computation 23, 2 (2010), 167–189. Google ScholarDigital Library
- Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017. On polymorphic gradual typing. PACMPL 1, ICFP (2017), 40:1–40:29. Google ScholarDigital Library
- Lintaro Ina and Atsushi Igarashi. 2011. Gradual typing for generics. In Proc. of ACM OOPSLA. 609–624. Google ScholarDigital Library
- Ik-Soon Kim, Kwangkeun Yi, and Cristiano Calcagno. 2006. A polymorphic modal type system for Lisp-like multi-staged languages. In Proc. of ACM POPL. 257–268. Google ScholarDigital Library
- Xavier Leroy. 1993. Polymorphism by Name for References and Continuations. In Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, USA, January 1993. 220–231. Google ScholarDigital Library
- Robin Milner. 1978. A Theory of Type Polymorphism in Programming. J. Comput. System Sci. 17 (1978), 348–375.Google ScholarCross Ref
- Martin Odersky and Konstantin Läufer. 1996. Putting Type Annotations to Work. In Conference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996. 54–67. Google ScholarDigital Library
- Willard Van Orman Quine. 1981. Mathematical Logic (revised edition ed.). Harvard University Press.Google Scholar
- Aseem Rastogi, Avik Chaudhuri, and Basil Hosmer. 2012. The ins and outs of gradual type inference. In Proc. of ACM POPL. 481–494. Google ScholarDigital Library
- John Reynolds. 1974. Towards a Theory of Type Structure. In Proc. Colloque sur la Programmation (LNCS), Vol. 19. Springer, 408–425. Google ScholarDigital Library
- John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In IFIP Congress. 513–523.Google Scholar
- Ilya Sergey and Dave Clarke. 2012. Gradual Ownership Types. In Proc. of ESOP (LNCS), Vol. 7211. Springer, 579–599. Google ScholarDigital Library
- Mark Shields, Tim Sheard, and Simon L. Peyton Jones. 1998. Dynamic Typing as Staged Type Inference. In Proc. of ACM POPL. 289–302. Google ScholarDigital Library
- Jeremy G. Siek and Walid Taha. 2006. Gradual typing for functional languages. In Proc. of Workshop on Scheme and Functional Programming. 81–92.Google Scholar
- Jeremy G. Siek and Walid Taha. 2007. Gradual Typing for Objects. In Proc. of ECOOP (LNCS), Vol. 4609. Springer, 2–27. Google ScholarDigital Library
- Jeremy G. Siek and Manish Vachharajani. 2008. Gradual typing with unification-based inference. In Proc. of DLS. 7. Google ScholarDigital Library
- 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 (LIPIcs), Vol. 32. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 274–293.Google Scholar
- Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. 2015b. Monotonic References for Efficient Gradual Typing. In Proc. of ESOP (LNCS), Vol. 9032. Springer, 432–456. Google ScholarDigital Library
- Jeremy G. Siek and Philip Wadler. 2010. Threesomes, with and without blame. In Proc. of ACM POPL. 365–376. Google ScholarDigital Library
- Guy L. Steele, Jr. 1990. Common LISP: the language, 2nd Edition. Digital Pr. http://www.worldcat.org/oclc/20631879 Google ScholarDigital Library
- Walid Taha and Michael Florentin Nielsen. 2003. Environment classifiers. In Proc. of ACM POPL. 26–37. Google ScholarDigital Library
- Walid Taha and Tim Sheard. 2000. MetaML and multi-stage programming with explicit annotations. Theoretical Computer Science 248, 1-2 (2000), 211–242. Google ScholarDigital Library
- Satish R. Thatte. 1990. Quasi-Static Typing. In Proc. of ACM POPL. 367–381. Google ScholarDigital Library
- Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The design and implementation of typed Scheme. In Proc. of ACM POPL. 395–406. Google ScholarDigital Library
- Takeshi Tsukada and Atsushi Igarashi. 2010. A Logical Foundation for Environment Classifiers. Logical Methods in Computer Science 6, 4:8 (2010), 1–43.Google ScholarCross Ref
- Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can’t Be Blamed. In Proc. of ESOP (LNCS), Vol. 5502. Springer, 1–16. Google ScholarDigital Library
- Andrew K. Wright. 1995. Simple Imperative Polymorphism. Lisp and Symbolic Computation 8, 4 (1995), 343–355. 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
- Ningning Xie, Xuan Bi, and Bruno C. d. S. Oliveira. 2018. Consistent Subtyping for All. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. 3–30.Google Scholar
Index Terms
- Dynamic type inference for gradual Hindley–Milner typing
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 ...
Gradual typing with unification-based inference
DLS '08: Proceedings of the 2008 symposium on Dynamic languagesStatic and dynamic type systems have well-known strengths and weaknesses. Gradual typing provides the benefits of both in a single language by giving the programmer control over which portions of the program are statically checked based on the presence ...
Comments