Document Open Access Logo

Dependent Types for Class-based Mutable Objects

Authors Joana Campos , Vasco T. Vasconcelos

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2018.13.pdf
  • Filesize: 0.51 MB
  • 28 pages

Document Identifiers

Author Details

Joana Campos
  • LASIGE, Faculdade de Ciências, Universidade de Lisboa, Portugal
Vasco T. Vasconcelos
  • LASIGE, Faculdade de Ciências, Universidade de Lisboa, Portugal

Cite AsGet BibTex

Joana Campos and Vasco T. Vasconcelos. Dependent Types for Class-based Mutable Objects. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 13:1-13:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.ECOOP.2018.13

Abstract

We present an imperative object-oriented language featuring a dependent type system designed to support class-based programming and inheritance. Programmers implement classes in the usual imperative style, and may take advantage of a richer dependent type system to express class invariants and restrictions on how objects are allowed to change and be used as arguments to methods. By way of example, we implement insertion and deletion for binary search trees in an imperative style, and come up with types that ensure the binary search tree invariant. This is the first dependently-typed language with mutable objects that we know of to bring classes and index refinements into play, enabling types (classes) to be refined by indices drawn from some constraint domain. We give a declarative type system that supports objects whose types may change, despite being sound. We also give an algorithmic type system that provides a precise account of quantifier instantiation in a bidirectional style, and from which it is straightforward to read off an implementation. Moreover, all the examples in the paper have been run, compiled and executed in a fully functional prototype that includes a plugin for the Eclipse IDE.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Semantics
Keywords
  • dependent types
  • index refinements
  • mutable objects
  • type systems

Metrics

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

Supplementary Materials

References

  1. Nada Amin, Tiark Rompf, and Martin Odersky. Foundations of path-dependent types. In OOPSLA. ACM Press, 2014. Google Scholar
  2. Lennart Augustsson. Cayenne a language with dependent types. In ICFP, pages 239-250. ACM Press, 1998. Google Scholar
  3. Hendrik Pieter Barendregt. The Lambda Calculus - Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984. Google Scholar
  4. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda - A functional language with dependent types. In TPHOLs, volume 5674 of LNCS, pages 73-78. Springer, 2009. Google Scholar
  5. Edwin Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 23:552-593, 2013. Google Scholar
  6. Patrice Chalin and Perry R. James. Non-null references by default in Java: Alleviating the nullity annotation burden. In ECOOP, pages 227-247. Springer, 2007. Google Scholar
  7. Ravi Chugh, David Herman, and Ranjit Jhala. Dependent types for JavaScript. In OOPSLA, pages 587-606. ACM Press, 2012. Google Scholar
  8. Maciej Cielecki, Jȩdrzej Fulara, Krzysztof Jakubczyk, and Lukasz Jancewicz. Propagation of jml non-null annotations in Java programs. In Principles and Practice of Programming in Java, pages 135-140. ACM Press, 2006. Google Scholar
  9. Jeremy Condit, Matthew Harren, Zachary R. Anderson, David Gay, and George C. Necula. Dependent types for low-level programming. In ESOP, volume 4421 of LNCS, pages 520-535. Springer, 2007. Google Scholar
  10. Robert L. Constable, Stuart F. Allen, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, Scott F. Smith, James T. Sasaki, and S. F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice Hall, 1986. Google Scholar
  11. Thierry Coquand and Gérard P. Huet. The calculus of constructions. Inf. Comput., 76(2/3):95-120, 1988. Google Scholar
  12. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of LNCS, pages 337-340. Springer, 2008. Google Scholar
  13. Krishna Kishore Dhara and Gary T. Leavens. Forcing behavioral subtyping through specification inheritance. In International Conference on Software Engineering, pages 258-267, 1996. Google Scholar
  14. Joshua Dunfield. A Unified System of Type Refinements. PhD thesis, Carnegie Mellon University, 2007. CMU-CS-07-129. Google Scholar
  15. Joshua Dunfield and Neelakantan R. Krishnaswami. Complete and easy bidirectional typechecking for higher-rank polymorphism. In ICFP, pages 429-442. ACM Press, 2013. Google Scholar
  16. Joshua Dunfield and Neelakantan R. Krishnaswami. Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types. CoRR, abs/1601.05106, 2016. Google Scholar
  17. Manuel Fähndrich and K. Rustan M. Leino. Declaring and checking non-null types in an object-oriented language. In OOPSLA, pages 302-312. ACM Press, 2003. Google Scholar
  18. Cormac Flanagan. Hybrid type checking. In POPL, pages 245-256, 2006. Google Scholar
  19. Ronald Garcia, Éric Tanter, Roger Wolff, and Jonathan Aldrich. Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst., 36(4):12:1-12:44, 2014. Google Scholar
  20. Vaidas Gasiunas, Mira Mezini, and Klaus Ostermann. Dependent classes. In OOPSLA, pages 133-152. ACM Press, 2007. Google Scholar
  21. Simon J. Gay, Nils Gesbert, António Ravara, and Vasco Thudichum Vasconcelos. Modular session types for objects. Logical Methods in Computer Science, 11(4), 2015. Google Scholar
  22. Robert Harper, Furio Honsell, and Gordon D. Plotkin. A framework for defining logics. J. ACM, 40(1):143-184, 1993. Google Scholar
  23. Tony Hoare. Null references: The billion dollar mistake. QCon, 2009. Google Scholar
  24. Atsushi Igarashi and Hideshi Nagira. Union types for object-oriented programming. In Symposium on Applied Computing, pages 1435-1441. ACM Press, 2006. Google Scholar
  25. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: a minimal core calculus for Java and GJ. TOPLAS, 23(3):396-450, 2001. Google Scholar
  26. Trevor Jim, J. Gregory Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, and Yanling Wang. Cyclone: A safe dialect of C. In USENIX, pages 275-288. USENIX, 2002. Google Scholar
  27. Tetsuo Kamina and Tetsuo Tamai. Lightweight dependent classes. In GPCE, pages 113-124. ACM Press, 2008. Google Scholar
  28. Kenneth L. Knowles. Executable Refinement Types. PhD thesis, University of California, 2014. Google Scholar
  29. Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: A behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes, 31(3):1-38, 2006. Google Scholar
  30. K. Rustan M. Leino. Extended static checking: A ten-year perspective. In Informatics - 10 Years Back. 10 Years Ahead, volume 2000 of LNCS, pages 157-175. Springer, 2001. Google Scholar
  31. Barbara H. Liskov and Jeannette M. Wing. A behavioral notion of subtyping. TOPLAS, 16(6):1811-1841, 1994. Google Scholar
  32. Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis-Napoli, 1984. Google Scholar
  33. Conor McBride. Epigram: Practical programming with dependent types. In Advanced Functional Programming, volume 3622 of LNCS, pages 130-170. Springer, 2004. Google Scholar
  34. Conor McBride. How to keep your neighbours in order. In ICFP, pages 297-309. ACM Press, 2014. Google Scholar
  35. Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: dependent types for imperative programs. In ICFP, pages 229-240, 2008. Google Scholar
  36. Aleksandar Nanevski, J. Gregory Morrisett, and Lars Birkedal. Hoare type theory, polymorphism and separation. Journal of Functional Programming, 18(5-6):865-911, 2008. Google Scholar
  37. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, 2007. Google Scholar
  38. Nathaniel Nystrom, Vijay Saraswat, Jens Palsberg, and Christian Grothoff. Constrained types for object-oriented languages. In OOPSLA, pages 457-474. ACM Press, 2008. Google Scholar
  39. Benjamin C. Pierce and David N. Turner. Local type inference. ACM Trans. Program. Lang. Syst., 22(1):1-44, 2000. Google Scholar
  40. Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. Liquid types. In PLDI, pages 159-169. ACM Press, 2008. Google Scholar
  41. Tim Sheard and Nathan Linger. Programming in Omega. In Central European Functional Programming School, volume 5161 of LNCS, pages 158-227. Springer, 2007. Google Scholar
  42. Frederick Smith, David Walker, and J. Gregory Morrisett. Alias types. In ESOP, volume 1782 of LNCS, pages 366-381. Springer, 2000. Google Scholar
  43. Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. Dependent types and multi-monadic effects in F*. In POPL, pages 256-270. ACM Press, 2016. Google Scholar
  44. Diederik T. van Daalen. The Language Theory of Automath. PhD thesis, Technische Hogeschool Eindhoven,Eindhoven, 1980. Google Scholar
  45. Edwin Westbrook, Aaron Stump, and Ian Wehrman. A language-based approach to functionally correct imperative programming. In ICFP, LNCS, pages 268-279. ACM Press, 2005. Google Scholar
  46. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38-94, 1994. Google Scholar
  47. Hongwei Xi. Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University, Pittsburgh, 1998. Google Scholar
  48. Hongwei Xi. Imperative programming with dependent types. In LICS, pages 375-387. IEEE Press, 2000. Google Scholar
  49. Hongwei Xi. Unifying object-oriented programming with typed functional programming. In PEPM, pages 117-125. ACM Press, 2002. Google Scholar
  50. Hongwei Xi. Applied type system: Extended abstract. In TYPES, pages 394-408. Springer, 2004. Google Scholar
  51. Hongwei Xi. Dependent ML: an approach to practical programming with dependent types. Journal of Functional Programming, 17(2):215-286, 2007. Google Scholar
  52. Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. In PLDI, pages 249-257. ACM Press, 1998. Google Scholar
  53. Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In POPL, pages 214-227. ACM Press, 1999. Google Scholar
  54. Luo Zhaohui and Robert Pollack. The LEGO proof development system: A user’s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, 1992. 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