Lightweight dependent classes

ABSTRACT

Extensive research efforts have been devoted to implement a group of type-safe mutually recursive classes; recently, proposals for separating each member of the group as a reusable and composable programming unit have also been presented. One problem of these proposals is verbosity of the source programs; we have to declare a recursive type parameter to parameterize each mutually recursive class within each class declaration, and we have to declare a fixed-point class with empty class body for each parameterized class. Therefore, even though the underlying type system is simple, programs written in these languages tend to be rather complex and hard to understand. In this paper, we propose a language with lightweight dependent classes that forms a simple type system built on top of generic Java. In this language, we can implement each member of type-safe mutually recursive classes in a separate source file without writing a lot of complex boilerplate code. To carefully investigate type soundness of our proposal, we develop X.FGJ, a simple extension of FGJ supporting lightweight dependent classes. This type system is proved to be sound.

REFERENCES

• 1: Ole Agesen , Stephen N. Freund , John C. Mitchell, Adding type parameterization to the Java language, Proceedings of the 12th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.49-65, October 05-09, 1997, Atlanta, Georgia, United States
• 2: Eric Allen , Jonathan Bannet , Robert Cartwright, A first-class approach to genericity, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 3: Gilad Bracha , Martin Odersky , David Stoutamire , Philip Wadler, Making the future safe for the past: adding genericity to the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.183-200, October 18-22, 1998, Vancouver, British Columbia, Canada
• 4: Kim B. Bruce , Angela Schuett , Robert van Gent , Adrian Fiech, PolyTOIL: A type-safe polymorphic object-oriented language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.2, p.225-290, March 2003 [doi>10.1145/641888.641891]
• 5: Kim B. Bruce. Some challenging typing issues in object-oriented languages. Electronic Notes in Theoretical Computer Science, 82(8), 2003.
• 6: Kim B. Bruce, Adrian Fiech, and Leaf Peterson. Subtyping is not a good "match" for object-oriented languages. In ECOOP'97, volume 1241 of LNCS, pages 104--127, 1997.
• 7: Kim B. Bruce and J. Nathan Foster. LOOJ: Weaving LOOM into Java. In ECOOP'04, volume 3086 of LNCS, pages 389--413, 2004.
• 8: Kim B. Bruce , Martin Odersky , Philip Wadler, A Statically Safe Alternative to Virtual Types, Proceedings of the 12th European Conference on Object-Oriented Programming, p.523-549, July 20-24, 1998
• 9: Robert Cartwright , Guy L. Steele, Jr., Compatible genericity with run-time types for the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.201-215, October 18-22, 1998, Vancouver, British Columbia, Canada
• 10: Torbjörn Ekman , Görel Hedin, The jastadd extensible java compiler, Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 11: Erik Ernst, Family Polymorphism, Proceedings of the 15th European Conference on Object-Oriented Programming, p.303-326, June 18-22, 2001
• 12: Erik Ernst, Propagating Class and Method Combination, Proceedings of the 13th European Conference on Object-Oriented Programming, p.67-91, June 14-18, 1999
• 13: Erik Ernst. Higher-order hierarchies. In ECOOP'01, volume 2743 of LNCS, pages 303--326, 2003.
• 14: Erik Ernst , Klaus Ostermann , William R. Cook, A virtual class calculus, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.270-282, January 11-13, 2006, Charleston, South Carolina, USA
• 15: Vaidas Gasiunas , Mira Mezini , Klaus Ostermann, Dependent classes, Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 16: Stephan Herrmann, Object Teams: Improving Modularity for Crosscutting Collaborations, Revised Papers from the International Conference NetObjectDays on Objects, Components, Architectures, Services, and Applications for a Networked World, p.248-264, October 07-10, 2002
• 17: Atsushi Igarashi , Benjamin C. Pierce , Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.396-450, May 2001 [doi>10.1145/503502.503505]
• 18: Atsushi Igarashi and Benjamin C. Pierce. Foundations for virtual types. Information and Computation, 175(1):34--49, 2003.
• 19: Paul Jolly, Sophia Drossopoulou, Christopher Anderson, and Klaus Ostermann. Simple dependent types: Concord. In ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP 2004), 2004.
• 20: Tetsuo Kamina , Tetsuo Tamai, Lightweight scalable components, Proceedings of the 6th international conference on Generative programming and component engineering, October 01-03, 2007, Salzburg, Austria [doi>10.1145/1289971.1289996]
• 21: O. L. Madsen , B. Moller-Pedersen, Virtual classes: a powerful mechanism in object-oriented programming, Conference proceedings on Object-oriented programming systems, languages and applications, p.397-406, October 02-06, 1989, New Orleans, Louisiana, United States
• 22: Mira Mezini , Klaus Ostermann, Integrating independent components with on-demand remodularization, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 23: Nathaniel Nystrom , Stephen Chong , Andrew C. Myers, Scalable extensibility via nested inheritance, Proceedings of the 19th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 24-28, 2004, Vancouver, BC, Canada
• 24: Nathaniel Nystrom, Michael R. Clarkson, and Andrew C. Myers. Polyglot: An extensible compiler framework for Java. In Proceedings of 12th International Conference on Compiler Construction, volume 2622 of LNCS, pages 138--152, 2003.
• 25: Nathaniel Nystrom , Xin Qi , Andrew C. Myers, J&: nested intersection for scalable software composition, Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA
• 26: Martin Odersky, Vincent Cremet, Christine Rockl, and Matthias Zenger. A nominal theory of objects with dependent types. In ECOOP'03, volume 2743 of LNCS, pages 201--224, 2003.
• 27: Martin Odersky , Philip Wadler, Pizza into Java: translating theory into practice, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.146-159, January 15-17, 1997, Paris, France [doi>10.1145/263699.263715]
• 28: Martin Odersky , Matthias Zenger, Scalable component abstractions, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 29: Klaus Ostermann, Dynamically Composable Collaborations with Delegation Layers, Proceedings of the 16th European Conference on Object-Oriented Programming, p.89-110, June 10-14, 2002
• 30: Chieri Saito , Atsushi Igarashi , Mirko Viroli, Lightweight family polymorphism*, Journal of Functional Programming, v.18 n.3, p.285-331, May 2008 [doi>10.1017/S0956796807006405]
• 31: Chieri Saito , Atsushi Igarashi , Mirko Viroli, Lightweight family polymorphism*, Journal of Functional Programming, v.18 n.3, p.285-331, May 2008 [doi>10.1017/S0956796807006405]
• 32: Kresten Krab Thorup , Mads Torgersen, Unifying Genericity - Combining the Benefits of Virtual Types and Parameterized Classes, Proceedings of the 13th European Conference on Object-Oriented Programming, p.186-204, June 14-18, 1999
• 33: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.5 Object-oriented Programming

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
      D.3.3 Language Constructs and Features

General Terms:
Languages

Keywords:
class-based languages, dependent classes, generics, mutually recursive extensions, type safety