Document Open Access Logo

Refined Criteria for Gradual Typing

Authors Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, John Tang Boyland

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2015.274.pdf
  • Filesize: 0.55 MB
  • 20 pages

Document Identifiers

Author Details

Jeremy G. Siek
Michael M. Vitousek
Matteo Cimini
John Tang Boyland

Cite As Get BibTex

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 274-293, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.SNAPL.2015.274

Abstract

Siek and Taha [2006] coined the term gradual typing to describe a theory for integrating static and dynamic typing within a single language that 1) puts the programmer in control of which regions of code are statically or dynamically typed and 2) enables the gradual evolution of code between the two typing disciplines. Since 2006, the term gradual typing has become quite popular but its meaning has become diluted to encompass anything related to the integration of static and dynamic typing. This dilution is partly the fault of the original paper, which provided an incomplete formal characterization of what it means to be gradually typed. In this paper we draw a crisp line in the sand that includes a new formal property, named the gradual guarantee, that relates the behavior of programs that differ only with respect to their type annotations.  We argue that the gradual guarantee provides important guidance for designers of gradually typed languages. We survey the gradual typing literature, critiquing designs in light of the gradual guarantee. We also report on a mechanized proof that the gradual guarantee holds for the Gradually Typed Lambda Calculus.

Subject Classification

Keywords
  • gradual typing
  • type systems
  • semantics
  • dynamic languages

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Martin Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. Dynamic typing in a statically typed language. ACM Transactions on Programming Languages and Systems, 13(2):237-268, April 1991. Google Scholar
  2. Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Blame for All. In Symposium on Principles of Programming Languages, January 2011. Google Scholar
  3. Esteban Allende, Oscar Callaú, Johan Fabry, Éric Tanter, and Marcus Denker. Gradual typing for Smalltalk. Science of Computer Programming, August 2013. Google Scholar
  4. Esteban Allende, Johan Fabry, Ronald Garcia, and Éric Tanter. Confined gradual typing. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA'14, pages 251-270, New York, NY, USA, 2014. ACM. Google Scholar
  5. Christopher Anderson and Sophia Drossopoulou. BabyJ - From Object Based to Class Based Programming via Types. ENTCS, 82(8), 2003. Google Scholar
  6. Gavin Bierman, Martín Abadi, and Mads Torgersen. Understanding typescript. In Richard Jones, editor, ECOOP 2014 - Object-Oriented Programming, volume 8586 of Lecture Notes in Computer Science, pages 257-281. Springer Berlin Heidelberg, 2014. Google Scholar
  7. Andrew P. Black, Kim B. Bruce, Michael Homer, and James Noble. Grace: The absence of (inessential) difficulty. In Proceedings of the ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2012, pages 85-98, New York, NY, USA, 2012. ACM. Google Scholar
  8. Bard Bloom, John Field, Nathaniel Nystrom, Johan Östlund, Gregor Richards, Rok Strniša, Jan Vitek, and Tobias Wrigstad. Thorn: Robust, concurrent, extensible scripting on the jvm. In ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications, pages 117-136, 2009. Google Scholar
  9. John Tang Boyland. The problem of structural type tests in a gradual-typed language. In Foundations of Object-Oriented Langauges, FOOL, 2014. Google Scholar
  10. Gilad Bracha and David Griswold. Strongtalk: typechecking Smalltalk in a production environment. In OOPSLA'93: Proceedings of the eighth annual conference on Object-oriented programming systems, languages, and applications, pages 215-230, New York, NY, USA, 1993. ACM Press. Google Scholar
  11. Luca Cardelli. Handbook of Computer Science and Engineering, chapter Type Systems. CRC Press, 1997. Google Scholar
  12. Luca Cardelli, James Donahue, Lucille Glassman, Mick Jordan, Bill Kalsow, and Greg Nelson. Modula-3 language definition. SIGPLAN Not., 27(8):15-42, August 1992. Google Scholar
  13. Robert Cartwright and Mike Fagan. Soft typing. In PLDI'91: Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, pages 278-292, New York, NY, USA, 1991. ACM Press. Google Scholar
  14. Craig Chambers and the Cecil Group. The Cecil language: Specification and rationale. Technical report, Department of Computer Science and Engineering, University of Washington, Seattle, Washington, 2004. Google Scholar
  15. Olaf Chitil. Practical typed lazy contracts. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP'12, pages 67-76, New York, NY, USA, 2012. ACM. Google Scholar
  16. Christos Dimoulas, Robert Bruce Findler, Cormac Flanagan, and Matthias Felleisen. Correct blame for contracts: no more scapegoating. In Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL'11, pages 215-226, New York, NY, USA, 2011. ACM. Google Scholar
  17. Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Complete monitors for behavioral contracts. In ESOP, 2012. Google Scholar
  18. Tim Disney and Cormac Flanagan. Gradual information flow typing. In Workshop on Script to Program Evolution, 2011. Google Scholar
  19. R. B. Findler and M. Felleisen. Contracts for higher-order functions. In International Conference on Functional Programming, ICFP, pages 48-59, October 2002. Google Scholar
  20. R. B. Findler, M. Flatt, and M. Felleisen. Semantic casts: Contracts and structural subtyping in a nominal world. In European Conference on Object-Oriented Programming, 2004. Google Scholar
  21. Cormac Flanagan and Matthias Felleisen. Componential set-based analysis. ACM Trans. Program. Lang. Syst., 21(2):370-416, 1999. Google Scholar
  22. Ronald Garcia and Matteo Cimini. Principal type schemes for gradual programs. In Symposium on Principles of Programming Languages, POPL, pages 303-315, 2015. Google Scholar
  23. James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Sun Developer Network, 1996. Google Scholar
  24. Kathryn E. Gray, Robert Bruce Findler, and Matthew Flatt. Fine-grained interoperability through mirrors and contracts. In OOPSLA'05: Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming systems languages and applications, pages 231-245, New York, NY, USA, 2005. ACM Press. Google Scholar
  25. Michael Greenberg. Space-efficient manifest contracts. In POPL, 2015. Google Scholar
  26. Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich. Contracts made manifest. In Principles of Programming Languages (POPL) 2010, 2010. Google Scholar
  27. Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop, pages 93-104, 2006. Google Scholar
  28. Arjun Guha, Jacob Matthews, Robert Bruce Findler, and Shriram Krishnamurthi. Relationally-parametric polymorphic contracts. In Dynamic Languages Symposium, 2007. Google Scholar
  29. Łukasz Langa Guido van Rossum, Jukka Lehtosalo. Type hints. https://www.python.org/dev/peps/pep-0484/, September 2014. draft.
  30. Lars T. Hansen. Evolutionary programming and gradual typing in ECMAScript 4 (tutorial). Technical report, ECMA TG1 working group, November 2007. Google Scholar
  31. Anders Hejlsberg. C# 4.0 and beyond by anders hejlsberg. Microsoft Channel 9 Blog, April 2010. Google Scholar
  32. Anders Hejlsberg. Introducing TypeScript. Microsoft Channel 9 Blog, 2012. Google Scholar
  33. Fritz Henglein. Dynamic typing: syntax and proof theory. Science of Computer Programming, 22(3):197-230, June 1994. Google Scholar
  34. David Herman, Aaron Tomb, and Cormac Flanagan. Space-efficient gradual typing. In Trends in Functional Prog. (TFP), page XXVIII, April 2007. Google Scholar
  35. David Herman, Aaron Tomb, and Cormac Flanagan. Space-efficient gradual typing. Higher-Order and Symbolic Computation, 23(2):167-189, 2010. Google Scholar
  36. Lintaro Ina and Atsushi Igarashi. Gradual typing for generics. In Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications, OOPSLA'11, 2011. Google Scholar
  37. International Organization for Standardization. ISO\slash IEC 14882:1998: Programming languages - C++, September 1998. Google Scholar
  38. Barbara Liskov, Russ Atkinson, Toby Bloom, Eliot Moss, Craig Schaffert, Bob Scheifler, and Alan Snyder. CLU reference manual. Technical Report LCS-TR-225, MIT, October 1979. Google Scholar
  39. Jacob Matthews and Amal Ahmed. Parametric polymorphism through run-time sealing, or, theorems for low, low prices! In Proceedings of the 17th European Symposium on Programming (ESOP'08), March 2008. Google Scholar
  40. Jacob Matthews and Robert Bruce Findler. Operational semantics for multi-language programs. In The 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2007. Google Scholar
  41. Erik Meijer and Peter Drayton. Static typing where possible, dynamic typing when needed: The end of the cold war between programming languages. In OOPSLA'04 Workshop on Revival of Dynamic Languages, 2004. Google Scholar
  42. Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348-375, 1978. Google Scholar
  43. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, November 2007. Google Scholar
  44. Aseem Rastogi, Avik Chaudhuri, and Basil Hosmer. The ins and outs of gradual type inference. In Symposium on Principles of Programming Languages, POPL, pages 481-494, January 2012. Google Scholar
  45. Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, and Panagiotis Vekris. Safe & efficient gradual typing for TypeScript. Technical Report MSR-TR-2014-99, Microsoft Research, 2014. Google Scholar
  46. Manuel Serrano. Bigloo: a practical Scheme compiler. Inria-Rocquencourt, April 2002. Google Scholar
  47. Andrew Shalit. The Dylan reference manual: the definitive guide to the new object-oriented dynamic language. Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, USA, 1996. Google Scholar
  48. Jeremy G. Siek. Design and evaluation of gradual typing for Python. https://dl.dropboxusercontent.com/u/10275252/shonan-slides-2014.pdf, May 2014.
  49. Jeremy G. Siek, Ronald Garcia, and Walid Taha. Exploring the design space of higher-order casts. In European Symposium on Programming, ESOP, pages 17-31, March 2009. Google Scholar
  50. Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, pages 81-92, September 2006. Google Scholar
  51. Jeremy G. Siek and Walid Taha. Gradual typing for objects. In European Conference on Object-Oriented Programming, volume 4609 of LCNS, pages 2-27, August 2007. Google Scholar
  52. Jeremy G. Siek and Manish Vachharajani. Gradual typing and unification-based inference. In DLS, 2008. Google Scholar
  53. Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. Monotonic references for efficient gradual typing. In European Symposium on Programming, ESOP, April 2015. Google Scholar
  54. Jeremy G. Siek and Philip Wadler. Threesomes, with and without blame. In Symposium on Principles of Programming Languages, POPL, pages 365-376, January 2010. Google Scholar
  55. Guy L. Steele, Jr. Common LISP: the language (2nd ed.). Digital Press, Newton, MA, USA, 1990. Google Scholar
  56. T. Stephen Strickland, Sam Tobin-Hochstadt, Robert Bruce Findler, and Matthew Flatt. Chaperones and impersonators: run-time support for reasonable interposition. In Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA'12, 2012. Google Scholar
  57. Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, and Gavin Bierman. Gradual typing embedded securely in javascript. In ACM Conference on Principles of Programming Languages (POPL), January 2014. Google Scholar
  58. Asumu Takikawa, T. Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Gradual typing for first-class classes. In Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA'12, pages 793-810, 2012. Google Scholar
  59. The Dart Team. Dart Programming Language Specification. Google, 1.2 edition, March 2014. Google Scholar
  60. Satish Thatte. Quasi-static typing. In POPL 1990, pages 367-381, New York, NY, USA, 1990. ACM Press. Google Scholar
  61. Peter Thiemann and Luminous Fennell. Gradual typing for annotated type systems. In Zhong Shao, editor, Programming Languages and Systems, volume 8410 of Lecture Notes in Computer Science, pages 47-66. Springer Berlin Heidelberg, 2014. Google Scholar
  62. Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage migration: From scripts to programs. In Dynamic Languages Symposium, 2006. Google Scholar
  63. Sam Tobin-Hochstadt and Matthias Felleisen. The design and implementation of Typed Scheme. In Symposium on Principles of Programming Languages, January 2008. Google Scholar
  64. Tom Van Cutsem and Mark S. Miller. Proxies: Design principles for robust object-oriented intercession apis. In Proceedings of the 6th Symposium on Dynamic Languages, DLS'10, pages 59-72, New York, NY, USA, 2010. ACM. Google Scholar
  65. Julien Verlaguet. Facebook: Analyzing PHP statically. In Commercial Users of Functional Programming (CUFP), 2013. Google Scholar
  66. Michael M. Vitousek, Jeremy G. Siek, Andrew Kent, and Jim Baker. Design and evaluation of gradual typing for Python. In Dynamic Languages Symposium, 2014. Google Scholar
  67. Philip Wadler and Robert Bruce Findler. Well-typed programs can't be blamed. In European Symposium on Programming, ESOP, pages 1-16, March 2009. Google Scholar
  68. Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. Gradual typestate. In European Conference on Object-Oriented Programming, ECOOP'11. Springer-Verlag, 2011. Google Scholar
  69. Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, and Jan Vitek. Integrating typed and untyped code in a scripting language. In Symposium on Principles of Programming Languages, POPL, pages 377-388, 2010. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact