Document Open Access Logo

A Co-contextual Type Checker for Featherweight Java

Authors Edlira Kuci, Sebastian Erdweg, Oliver Bracevac, Andi Bejleri, Mira Mezini



PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.18.pdf
  • Filesize: 0.64 MB
  • 26 pages

Document Identifiers

Author Details

Edlira Kuci
Sebastian Erdweg
Oliver Bracevac
Andi Bejleri
Mira Mezini

Cite AsGet BibTex

Edlira Kuci, Sebastian Erdweg, Oliver Bracevac, Andi Bejleri, and Mira Mezini. A Co-contextual Type Checker for Featherweight Java. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 18:1-18:26, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ECOOP.2017.18

Abstract

This paper addresses compositional and incremental type checking for object-oriented programming languages. Recent work achieved incremental type checking for structurally typed functional languages through co-contextual typing rules, a constraint-based formulation that removes any context dependency for expression typings. However, that work does not cover key features of object-oriented languages: Subtype polymorphism, nominal typing, and implementation inheritance. Type checkers encode these features in the form of class tables, an additional form of typing context inhibiting incrementalization. In the present work, we demonstrate that an appropriate co-contextual notion to class tables exists, paving the way to efficient incremental type checkers for object-oriented languages. This yields a novel formulation of Igarashi et al.'s Featherweight Java (FJ) type system, where we replace class tables by the dual concept of class table requirements and class table operations by dual operations on class table requirements. We prove the equivalence of FJ's type system and our co-contextual formulation. Based on our formulation, we implemented an incremental FJ type checker and compared its performance against javac on a number of realistic example programs.
Keywords
  • type checking
  • co-contextual
  • constraints
  • class table
  • Featherweight Java

Metrics

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

References

  1. Davide Ancona, Ferruccio Damiani, Sophia Drossopoulou, and Elena Zucca. Polymorphic bytecode: Compositional compilation for Java-like languages. In Proceedings of Symposium on Principles of Programming Languages (POPL), 2005. URL: http://dx.doi.org/10.1145/1040305.1040308.
  2. Davide Ancona and Elena Zucca. Principal typings for Java-like languages. In Proceedings of Symposium on Principles of Programming Languages (POPL), 2004. URL: http://dx.doi.org/10.1145/964001.964027.
  3. Olaf Chitil. Compositional explanation of types and algorithmic debugging of type errors. In Proceedings of International Conference on Functional Programming (ICFP), 2001. URL: http://dx.doi.org/10.1145/507635.507659.
  4. David Raymond Christiansen. Bidirectional typing rules: A tutorial, 2013. Google Scholar
  5. Joshua Dunfield and Neelakantan R. Krishnaswami. Complete and easy bidirectional typechecking for higher-rank polymorphism. In Proceedings of International Conference on Functional Programming (ICFP), 2013. URL: http://dx.doi.org/10.1145/2500365.2500582.
  6. Sebastian Erdweg, Oliver Bračevac, Edlira Kuci, Matthias Krebs, and Mira Mezini. A co-contextual formulation of type rules and its application to incremental type checking. In Proceedings of Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2015. URL: http://dx.doi.org/10.1145/2814270.2814277.
  7. Matthew A. Hammer, Khoo Yit Phang, Michael Hicks, and Jeffrey S. Foster. Adapton: Composable, demand-driven incremental computation. In Proceedings of Conference on Programming Language Design and Implementation (PLDI), 2014. URL: http://dx.doi.org/10.1145/2666356.2594324.
  8. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. Transactions on Programming Languages and Systems (TOPLAS), 2001. URL: http://dx.doi.org/10.1145/503502.503505.
  9. Trevor Jim. What are principal typings and what are they good for? In Proceedings of Symposium on Principles of Programming Languages (POPL), 1996. URL: http://dx.doi.org/10.1145/237721.237728.
  10. Edlira Kuci, Sebastian Erdweg, Oliver Bračevac, Andi Bejleri, and Mira Mezini. A co-contextual type checker for Featherweight Java (incl. proofs). CoRR, abs/1705.05828, 2017. Google Scholar
  11. Benjamin C. Pierce. Types and programming languages. MIT press, 2002. Google Scholar
  12. Benjamin C. Pierce and David N. Turner. Local type inference. In Proceedings of Symposium on Principles of Programming Languages (POPL), 1998. URL: http://dx.doi.org/10.1145/268946.268967.
  13. Zhong Shao and Andrew W. Appel. Smartest recompilation. In Proceedings of Symposium on Principles of Programming Languages (POPL), 1993. URL: http://dx.doi.org/10.1145/158511.158702.
  14. Walter F. Tichy. Smart recompilation. Transactions on Programming Languages and Systems (TOPLAS), 1986. URL: http://dx.doi.org/10.1145/5956.5959.
  15. Frank Tip, Robert M. Fuhrer, Adam Kieżun, Michael D. Ernst, Ittai Balaban, and Bjorn De Sutter. Refactoring using type constraints. Transactions on Programming Languages and Systems (TOPLAS), 2011. URL: http://dx.doi.org/10.1145/1961204.1961205.
  16. Frank Tip, Adam Kiezun, and Dirk Bäumer. Refactoring for generalization using type constraints. In Proceedings of Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2003. URL: http://dx.doi.org/10.1145/949305.949308.
  17. J. B. Wells. The essence of principal typings. In Proceedings of International Colloquium on Automata, Languages and Programming (ICALP), 2002. URL: http://dx.doi.org/10.1007/3-540-45465-9_78.
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