Document Open Access Logo

Type-Directed Operational Semantics for Gradual Typing

Authors Wenjia Ye, Bruno C. d. S. Oliveira, Xuejing Huang

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2021.12.pdf
  • Filesize: 0.98 MB
  • 30 pages

Document Identifiers

Author Details

Wenjia Ye
  • The University of Hong Kong, Hong Kong
Bruno C. d. S. Oliveira
  • The University of Hong Kong, Hong Kong
Xuejing Huang
  • The University of Hong Kong, Hong Kong

Funding

This work has been sponsored by Hong Kong Research Grant Council projects number 17209519 and 17209520.

Acknowledgements

We thank the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang. Type-Directed Operational Semantics for Gradual Typing. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 12:1-12:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ECOOP.2021.12

Abstract

The semantics of gradually typed languages is typically given indirectly via an elaboration into a cast calculus. This contrasts with more conventional formulations of programming language semantics, where the semantics of a language is given directly using, for instance, an operational semantics. This paper presents a new approach to give the semantics of gradually typed languages directly. We use a recently proposed variant of small-step operational semantics called type-directed operational semantics (TDOS). In TDOS type annotations become operationally relevant and can affect the result of a program. In the context of a gradually typed language, such type annotations are used to trigger type-based conversions on values. We illustrate how to employ TDOS on gradually typed languages using two calculi. The first calculus, called λ B^g, is inspired by the semantics of the blame calculus, but it has implicit type conversions, enabling it to be used as a gradually typed language. The second calculus, called λ B^r, explores a different design space in the semantics of gradually typed languages. It uses a so-called blame recovery semantics, which enables eliminating some false positives where blame is raised but normal computation could succeed. For both calculi, type safety is proved. Furthermore we show that the semantics of λ B^g is sound with respect to the semantics of the blame calculus, and that λ B^r comes with a gradual guarantee. All the results have been mechanically formalized in the Coq theorem prover.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Software and its engineering → Object oriented languages
  • Software and its engineering → Polymorphism
Keywords
  • Gradual Typing
  • Type Systems
  • Operational Semantics

Metrics

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

Supplementary Materials

References

  1. Martin Abadi and Luca Cardelli. A theory of objects. Springer Science & Business Media, 2012. Google Scholar
  2. Martín Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. Dynamic typing in a statically typed language. ACM transactions on programming languages and systems (TOPLAS), 13(2):237-268, 1991. Google Scholar
  3. Amal Ahmed, Robert Bruce Findler, Jeremy G Siek, and Philip Wadler. Blame for all. In Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 201-214, 2011. Google Scholar
  4. Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. A theory of gradual effect systems. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, pages 283-295, 2014. Google Scholar
  5. Lorenzo Bettini, Viviana Bono, Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri. Java & lambda: a featherweight story. Logical Methods in Computer Science, 14(3), 2018. Google Scholar
  6. Gavin Bierman, Martín Abadi, and Mads Torgersen. Understanding typescript. In European Conference on Object-Oriented Programming, pages 257-281. Springer, 2014. Google Scholar
  7. John Tang Boyland. The problem of structural type tests in a gradual-typed language. Foundations of Object-Oriented Langauges, 2014. Google Scholar
  8. Gilad Bracha. The Dart programming language. Addison-Wesley Professional, 2015. Google Scholar
  9. Giuseppe Castagna and Victor Lanvin. Gradual typing with union and intersection types. Proceedings of the ACM on Programming Languages, 1(ICFP):1-28, 2017. Google Scholar
  10. Craig Chambers. The cecil language, specification and rationale, 1993. Google Scholar
  11. Avik Chaudhuri. Flow: a static type checker for javascript. SPLASH-I In Systems, Programming, Languages and Applications: Software for Humanity, 2015. Google Scholar
  12. Alonzo Church. A formulation of the simple theory of types. The journal of symbolic logic, 5(2):56-68, 1940. Google Scholar
  13. Adriana Compagnoni and Healfdene Goguen. Typed operational semantics for higher-order subtyping. Information and Computation, 184(2):242-297, 2003. Google Scholar
  14. Yangyue Feng and Zhaohui Luo. Typed operational semantics for dependent record types. arXiv preprint arXiv:1103.3321, 2011. Google Scholar
  15. Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, pages 48-59, 2002. Google Scholar
  16. Ronald Garcia. Calculating threesomes, with blame. In Proceedings of the 18th ACM SIGPLAN international conference on Functional programming, pages 417-428, 2013. Google Scholar
  17. Ronald Garcia, Alison M Clark, and Éric Tanter. Abstracting gradual typing. ACM SIGPLAN Notices, 51(1):429-442, 2016. Google Scholar
  18. Healfdene Goguen. A typed operational semantics for type theory, 1994. Google Scholar
  19. Healfdene Goguen. Typed operational semantics. In International Conference on Typed Lambda Calculi and Applications, pages 186-200. Springer, 1995. Google Scholar
  20. Kathryn E Gray, Robert Bruce Findler, and Matthew Flatt. Fine-grained interoperability through mirrors and contracts. ACM SIGPLAN Notices, 40(10):231-245, 2005. Google Scholar
  21. Michael Greenberg. Space-efficient manifest contracts. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 181-194, 2015. Google Scholar
  22. Lars T Hansen. Evolutionary programming and gradual typing in ecmascript 4 (tutorial). Lars, 2007. Google Scholar
  23. Fritz Henglein. Dynamic typing: Syntax and proof theory. Science of Computer Programming, 22(3):197-230, 1994. Google Scholar
  24. David Herman, Aaron Tomb, and Cormac Flanagan. Space-efficient gradual typing. Higher-Order and Symbolic Computation, 23(2):167, 2010. Google Scholar
  25. Xuejing Huang and Bruno C d S Oliveira. A type-directed operational semantics for a calculus with a merge operator. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020. Google Scholar
  26. 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, pages 609-624, 2011. Google Scholar
  27. Andre Kuhlenschmidt, Deyaaeldeen Almahallawi, and Jeremy G Siek. Efficient gradual typing. arXiv preprint arXiv:1802.06375, 2018. Google Scholar
  28. Jacob Matthews and Amal Ahmed. Parametric polymorphism through run-time sealing. In European Symposium on Programming (ESOP), pages 16-31. Citeseer, 2008. Google Scholar
  29. Jacob Matthews and Robert Bruce Findler. Operational semantics for multi-language programs. ACM SIGPLAN Notices, 42(1):3-10, 2007. Google Scholar
  30. 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. Citeseer, 2004. Google Scholar
  31. Andrew Myers. CS 6110 Lecture 8 Evaluation Contexts , Semantics by Translation, 2013. Google Scholar
  32. Georg Neis, Derek Dreyer, and Andreas Rossberg. Non-parametric parametricity. ACM Sigplan Notices, 44(9):135-148, 2009. Google Scholar
  33. Benjamin C Pierce and David N Turner. Local type inference. ACM Transactions on Programming Languages and Systems (TOPLAS), 22(1):1-44, 2000. Google Scholar
  34. Aseem Rastogi, Avik Chaudhuri, and Basil Hosmer. The ins and outs of gradual type inference. ACM SIGPLAN Notices, 47(1):481-494, 2012. Google Scholar
  35. Manuel Serrano and Pierre Weis. Bigloo: a portable and optimizing compiler for strict functional languages. In International Static Analysis Symposium, pages 366-381. Springer, 1995. Google Scholar
  36. Andrew Shalit. The Dylan reference manual: the definitive guide to the new object-oriented dynamic language. Addison Wesley Longman Publishing Co., Inc., 1996. Google Scholar
  37. Jeremy Siek, Ronald Garcia, and Walid Taha. Exploring the design space of higher-order casts. In European Symposium on Programming, pages 17-31. Springer, 2009. Google Scholar
  38. Jeremy Siek and Walid Taha. Gradual typing for objects. In European Conference on Object-Oriented Programming, pages 2-27. Springer, 2007. Google Scholar
  39. Jeremy Siek, Peter Thiemann, and Philip Wadler. Blame and coercion: together again for the first time. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 425-435, 2015. Google Scholar
  40. Jeremy G Siek and Manish Vachharajani. Gradual typing with unification-based inference. In Proceedings of the 2008 symposium on Dynamic languages, pages 1-12, 2008. Google Scholar
  41. 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). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  42. Jeremy G Siek and Philip Wadler. Threesomes, with and without blame. ACM Sigplan Notices, 45(1):365-376, 2010. Google Scholar
  43. G Siek Jeremy and Taha Walid. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, volume 6, pages 81-92, 2006. Google Scholar
  44. Guy Steele. Common LISP: the language. Elsevier, 1990. Google Scholar
  45. T Stephen Strickland, Sam Tobin-Hochstadt, Robert Bruce Findler, and Matthew Flatt. Chaperones and impersonators: run-time support for reasonable interposition. ACM SIGPLAN Notices, 47(10):943-962, 2012. Google Scholar
  46. Nikhil Swamy, Cedric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, and Gavin Bierman. Gradual typing embedded securely in javascript. ACM SIGPLAN Notices, 49(1):425-437, 2014. Google Scholar
  47. Asumu Takikawa, T Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Gradual typing for first-class classes. In Proceedings of the ACM international conference on Object oriented programming systems languages and applications, pages 793-810, 2012. Google Scholar
  48. Satish Thatte. Quasi-static typing. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 367-381, 1989. Google Scholar
  49. Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage migration: from scripts to programs. In Companion to the 21st ACM SIGPLAN symposium on Object-oriented programming systems, languages, and applications, pages 964-974, 2006. Google Scholar
  50. Sam Tobin-Hochstadt and Matthias Felleisen. The design and implementation of typed scheme. ACM SIGPLAN Notices, 43(1):395-406, 2008. Google Scholar
  51. Julien Verlaguet. Facebook: Analyzing php statically. Commercial Users of Functional Programming (CUFP), 13, 2013. Google Scholar
  52. Philip Wadler and Robert Bruce Findler. Well-typed programs can’t be blamed. In European Symposium on Programming, pages 1-16. Springer, 2009. Google Scholar
  53. Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. Gradual typestate. In European Conference on Object-Oriented Programming, pages 459-483. Springer, 2011. Google Scholar
  54. Andrew K Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and computation, 115(1):38-94, 1994. 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 Imprint Privacy Contact