Abstracting gradual typing

Abstract

Language researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and static checking. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs. In this paper, we propose a new formal foundation for gradual typing, drawing on principles from abstract interpretation to give gradual types a semantics in terms of pre-existing static types. Abstracting Gradual Typing (AGT for short) yields a formal account of consistency---one of the cornerstones of the gradual typing approach---that subsumes existing notions of consistency, which were developed through intuition and ad hoc reasoning. Given a syntax-directed static typing judgment, the AGT approach induces a corresponding gradual typing judgment. Then the type safety proof for the underlying static discipline induces a dynamic semantics for gradual programs defined over source-language typing derivations. The AGT approach does not resort to an externally justified cast calculus: instead, run-time checks naturally arise by deducing evidence for consistent judgments during proof reduction. To illustrate the approach, we develop a novel gradually-typed counterpart for a language with record subtyping. Gradual languages designed with the AGT approach satisfy by construction the refined criteria for gradual typing set forth by Siek and colleagues.

References

1. A. Ahmed, R. B. Findler, J. Siek, and P. Wadler. Blame for all. In 38th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2011), pages 201–214, Austin, Texas, USA, Jan. 2011. ACM Press. C. Anderson and S. Drossopoulou. BabyJ: from object based to class based programming via types. Electronic Notes in Theoretical Computer Science, 82(8), 2003.
2. F. Ba˜nados Schwerter, R. Garcia, and É. Tanter. A theory of gradual effect systems. In 19th ACM SIGPLAN Conference on Functional Programming (ICFP 2014), pages 283–295, Gothenburg, Sweden, Sept. 2014. ACM Press. A. Church. A formulation of the simple theory of types. J. Symbolic Logic, 5(2):56–68, 06 1940.
3. M. Cimini and J. G. Siek. The gradualizer: a methodology and algorithm for generating gradual type systems. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), St Petersburg, FL, USA, Jan. 2016. ACM Press. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symposium on Principles of Programming Languages (POPL 77), pages 238–252, Los Angeles, CA, USA, Jan. 1977.
4. ACM Press. P. Cousot and R. Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), invited paper. In 1994 International Conference on Computer Languages, pages 95–112, Toulouse, France, 16–19 May 1994. IEEE Computer Society Press, Los Alamitos, California. T. Disney and C. Flanagan. Gradual information flow typing. In International Workshop on Scripts to Programs, 2011.
5. L. Fennell and P. Thiemann. Gradual security typing with references. In Computer Security Foundations Symposium, pages 224–239, June 2013.
6. R. B. Findler and M. Felleisen. Contracts for higher-order functions. In 7th ACM SIGPLAN Conference on Functional Programming (ICFP 2002), pages 48–59, Pittsburgh, PA, USA, Sept. 2002. ACM Press. R. Garcia and M. Cimini. Principal type schemes for gradual programs. In 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015), pages 303–315. ACM Press, Jan. 2015.
7. R. Garcia and É. Tanter. Deriving a simple gradual security language. available on arXiv, 2015. URL http://arxiv.org/abs/1511.01399.
8. R. Garcia, É. Tanter, R. Wolff, and J. Aldrich. Foundations of typestateoriented programming. ACM Transactions on Programming Languages and Systems, 36(4):12:1–12:44, Oct. 2014.
9. R. Giacobazzi and E. Quintarelli. Incompleteness, counterexamples, and refinements in abstract model-checking. In P. Cousot, editor, Static Analysis, volume 2126 of LNCS, pages 356–373. Springer-Verlag, 2001.
10. D. Herman, A. Tomb, and C. Flanagan. Space-efficient gradual typing. In Trends in Functional Programming, page XXVIII, April 2007.
11. W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479–490. Academic Press, New York, 1980. Reprint of 1969 article. L. Ina and A. Igarashi. Gradual typing for generics. In 26th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2011), pages 609–624. ACM Press, Oct. 2011.
12. B. C. Pierce. Types and programming languages. MIT Press, Cambridge, MA, USA, 2002. ISBN 0-262-16209-1. A. Rastogi, A. Chaudhuri, and B. Hosmer. The ins and outs of gradual type inference. In 39th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), pages 481–494, Philadelphia, USA, Jan. 2012. ACM Press. A. Rastogi, N. Swamy, C. Fournet, G. Bierman, and P. Vekris. Safe & efficient gradual typing for typescript. In 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015), pages 167–180. ACM Press, Jan. 2015.
13. D. Rémy. Type checking records and variants as a natural extension of ML. In 16th ACM Symposium on Principles of Programming Languages (POPL 89), pages 77–88, Austin, TX, USA, Jan. 1989. ACM Press. D. Schmidt. Internal and external logics of abstract interpretations. In F. Logozzo, D. Peled, and L. Zuck, editors, Verification, Model Checking, and Abstract Interpretation, volume 4905 of LNCS, pages 263–278. Springer-Verlag, 2008.
14. I. Sergey and D. Clarke. Gradual ownership types. In H. Seidl, editor, 21st European Symposium on Programming Languages and Systems (ESOP 2012), volume 7211 of LNCS, pages 579–599, Tallinn, Estonia, 2012. Springer-Verlag. J. Siek and W. Taha. Gradual typing for objects. In E. Ernst, editor, 21st European Conference on Object-oriented Programming (ECOOP 2007), number 4609 in LNCS, pages 2–27, Berlin, Germany, July 2007. Springer-Verlag. J. Siek and P. Wadler. Threesomes, with and without blame. In 37th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), pages 365–376. ACM Press, Jan. 2010.
15. J. Siek, R. Garcia, and W. Taha. Exploring the design space of higherorder casts. In G. Castagna, editor, 18th European Symposium on Programming Languages and Systems (ESOP 2009), volume 5502 of LNCS, pages 17–31, York, UK, 2009. Springer-Verlag. J. Siek, P. Thiemann, and P. Wadler. Blame and coercion: Together again for the first time. In 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015), pages 425–435, Portland, OR, USA, June 2015a. ACM Press. J. G. Siek and R. Garcia. Interpretations of the gradually-typed lambda calculus. In Scheme and Functional Programming Workshop, pages 68– 80, 2012.
16. J. G. Siek and W. Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, pages 81–92, Sept. 2006.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

• Theory of computation

  • Formal languages and automata theory