Document Open Access Logo

Call-by-Name Gradual Type Theory

Authors Max S. New, Daniel R. Licata

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.24.pdf
  • Filesize: 0.49 MB
  • 17 pages

Document Identifiers

Author Details

Max S. New
  • Northeastern University, Boston, USA
Daniel R. Licata
  • Wesleyan University, Middletown, USA

Funding

  • New, Max S.: This material is based upon work supported by the National Science Foundation under grant CCF-1453796. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.
  • Licata, Daniel R.: This research was partially supported by the United States Air Force Research Laboratory under agreement numbers FA-95501210370 and FA-95501510053. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of the United States Air Force Research Laboratory, the U.S. Government or Carnegie Mellon University.

Cite As Get BibTex

Max S. New and Daniel R. Licata. Call-by-Name Gradual Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSCD.2018.24

Abstract

We present gradual type theory, a logic and type theory for call-by-name gradual typing. We define the central constructions of gradual typing (the dynamic type, type casts and type error) in a novel way, by universal properties relative to new judgments for gradual type and term dynamism. These dynamism judgements build on prior work in blame calculi and on the "gradual guarantee" theorem of gradual typing. Combined with the ordinary extensionality (eta) principles that type theory provides, we show that most of the standard operational behavior of casts is uniquely determined by the gradual guarantee. This provides a semantic justification for the definitions of casts, and shows that non-standard definitions of casts must violate these principles. Our type theory is the internal language of a certain class of preorder categories called equipments. We give a general construction of an equipment interpreting gradual type theory from a 2-category representing non-gradual types and programs, which is a semantic analogue of the interpretation of gradual typing using contracts, and use it to build some concrete domain-theoretic models of gradual typing.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Theory of computation → Axiomatic semantics
  • Theory of computation → Categorical semantics
  • Theory of computation → Type theory
  • Theory of computation → Denotational semantics
Keywords
  • Gradual Typing
  • Type Systems
  • Program Logics
  • Category Theory
  • Denotational Semantics

Metrics

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

Related Versions

References

  1. Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. Theorems for free for free: Parametricity, with and without types. In International Conference on Functional Programming (ICFP), 2017. Google Scholar
  2. 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, ICFP '14, pages 283-295, 2014. Google Scholar
  3. Matteo Cimini and Jeremy G. Siek. Automatically generating the dynamic semantics of gradually typed languages. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 789-803, 2017. Google Scholar
  4. G. S. H. Cruttwell and Michael A. Shulman. A unified framework for generalized multicategories. Theory and Applications of Categories, 24(21), 2009. URL: http://arxiv.org/abs/arXiv:0907.2460.
  5. Pierre-Evariste Dagand, Nicolas Tabareau, and Éric Tanter. Foundations of Dependent Interoperability. working paper or preprint, 2017. URL: https://hal.inria.fr/hal-01629909.
  6. Matthias Felleisen. On the expressive power of programming languages. ESOP'90, 1990. Google Scholar
  7. Robby Findler and Matthias Blume. Contracts as pairs of projections. In International Symposium on Functional and Logic Programming (FLOPS), 2006. Google Scholar
  8. Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In International Conference on Functional Programming (ICFP), pages 48-59, sep 2002. Google Scholar
  9. Ronald Garcia, Alison M. Clark, and Éric Tanter. Abstracting gradual typing. In ACM Symposium on Principles of Programming Languages (POPL), 2016. Google Scholar
  10. Fritz Henglein. Dynamic typing: Syntax and proof theory. Sci. Comput. Program., 22(3):197-230, 1994. Google Scholar
  11. Atsushi Igarashi, Peter Thiemann, Vasco Vasconcelos, and Philip Wadler. Gradual session types. In International Conference on Functional Programming (ICFP), 2017. Google Scholar
  12. Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. On polymorphic gradual typing. In International Conference on Functional Programming (ICFP), Oxford, United Kingdom, 2017. Google Scholar
  13. J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, 1986. Google Scholar
  14. Nico Lehmann and Éric Tanter. Gradual refinement types. In ACM Symposium on Principles of Programming Languages (POPL), 2017. Google Scholar
  15. Paul Blain Levy. Call-by-Push-Value. Ph. D. dissertation, Queen Mary, University of London, London, UK, mar 2001. Google Scholar
  16. Per Martin-Löf. On the meanings of the logical constants and the justifications of the logical laws (sienna lectures). Nordic Journal of Philosophical Logic, 1(1):11-60, 1983/1996. Google Scholar
  17. Jacob Matthews and Amal Ahmed. Parametric polymorphism through run-time sealing, or, theorems for low, low prices! In European Symposium on Programming (ESOP), mar 2008. Google Scholar
  18. Eugenio Moggi. Notions of computation and monads. Inform. And Computation, 93(1), 1991. Google Scholar
  19. Georg Neis, Derek Dreyer, and Andreas Rossberg. Non-parametric parametricity. In International Conference on Functional Programming (ICFP), pages 135-148, sep 2009. Google Scholar
  20. Max S. New and Daniel R. Licata. Call-by-name gradual type theory. CoRR, 2018. URL: http://arxiv.org/abs/1802.00061.
  21. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11:511-540, 2001. Google Scholar
  22. Dana Scott. Data types as lattices. Siam Journal on computing, 5(3):522-587, 1976. Google Scholar
  23. Michael Shulman. Framed bicategories and monoidal fibrations. Theory and Applications of Categories, 20(18):650-738, 2008. Google Scholar
  24. Jeremy Siek, Micahel Vitousek, Matteo Cimini, and John Tang Boyland. Refined criteria for gradual typing. In 1st Summit on Advances in Programming Languages, SNAPL 2015, 2015. Google Scholar
  25. Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop (Scheme), pages 81-92, 2006. Google Scholar
  26. Jeremy G. Siek and Philip Wadler. Threesomes, with and without blame. In ACM Symposium on Principles of Programming Languages (POPL), pages 365-376, 2010. Google Scholar
  27. Michael B Smyth and Gordon D Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal on Computing, 11(4), 1982. Google Scholar
  28. Sam Staton and Paul Blain Levy. Universal properties of impure programming languages. In ACM Symposium on Principles of Programming Languages (POPL), 2013. Google Scholar
  29. Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage migration: From scripts to programs. In Dynamic Languages Symposium (DLS), pages 964-974, 2006. Google Scholar
  30. Sam Tobin-Hochstadt and Matthias Felleisen. The design and implementation of typed scheme. In ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California, 2008. Google Scholar
  31. Philip Wadler and Robert Bruce Findler. Well-typed programs can't be blamed. In European Symposium on Programming (ESOP), pages 1-16, 2009. Google Scholar
  32. Mitchell Wand. Fixed-point constructions in order-enriched categories. Theoretical Computer Science, 8(1):13-30, 1979. Google Scholar
  33. Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. Gradual typestate. In Proceedings of the 25th European Conference on Object-oriented Programming, ECOOP'11, 2011. 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