Constrained types for object-oriented languages

ABSTRACT

X10 is a modern object-oriented language designed for productivity and performance in concurrent and distributed systems. In this setting, dependent types offer significant opportunities for detecting design errors statically, documenting design decisions, eliminating costly run-time checks (e.g., for array bounds, null values), and improving the quality of generated code.

We present the design and implementation of constrained types, a natural, simple, clean, and expressive extension to object-oriented programming: A type C{c} names a class or interface C and a constraint c on the immutable state of C and in-scope final variables. Constraints may also be associated with class definitions (representing class invariants) and with method and constructor definitions (representing preconditions). Dynamic casting is permitted. The system is parametric on the underlying constraint system: the compiler supports a simple equality-based constraint system but, in addition, supports extension with new constraint systems using compiler plugins.

REFERENCES

• 1: Alexander Aiken , Edward L. Wimmers , T. K. Lakshman, Soft typing with conditional types, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177847]
• 2: Hassan Ait-Kaci, A lattice theoretic approach to computation based on a calculus of partially ordered type structures (property inheritance, semantic nets, graph unification), University of Pennsylvania, Philadelphia, PA, 1984
• 3: Thorsten Altenkirch, Conor McBride, and James McKinna. Why dependent types matter. http://www.e-pig.org/downloads/ydtm.pdf, April 2005.
• 4: Chris Andreae , James Noble , Shane Markstrum , Todd Millstein, A framework for implementing pluggable type systems, Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA
• 5: David Aspinall and Martin Hofmann. Dependent Types, chapter 2. In Pierce {52}, 2004.
• 6: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 7: Clark Barrett and Sergey Berezin. CVC Lite: A new implementation of the cooperating validity checker. In Rajeev Alur and Doron A. Peled, editors, Proceedings of the $16^th$ International Conference on Computer Aided Verification (CAV '04), volume 3114 of Lecture Notes in Computer Science, pages 515--518. Springer-Verlag, July 2004. Boston, Massachusetts.
• 8: Clark Barrett, Cesare Tinelli, Alexander Fuchs, Yeting Ge, George Hagen, and Dejan Jovanovic. CVC3. http://www.cs.nyu.edu/acsys/cvc3.
• 9: Gilad Bracha. Pluggable type systems. In OOPSLA'04 Workshop on Revival of Dynamic Languages, October 2004.
• 10: Bradford L. Chamberlain, Sung-Eun Choi, Steven J. Deitz, and Lawrence Snyder. The high-level parallel language ZPL improves productivity and performance. In Proceedings of the IEEE International Workshop on Productivity and Performance in High-End Computing, 2004.
• 11: Craig Chambers, Predicate Classes, Proceedings of the 7th European Conference on Object-Oriented Programming, p.268-296, July 26-30, 1993
• 12: Brian Chin , Shane Markstrum , Todd Millstein, Semantic type qualifiers, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 13: Stephen Chong, Andrew C. Myers, K. Vikram, and Lantian Zheng. Jif reference manual, Jif 3.0.0 version. http://www.cs.cornell.edu/jif, June 2006.
• 14: Dave Clarke , Sophia Drossopoulou , James Noble , Tobias Wrigstad, Tribe: a simple virtual class calculus, Proceedings of the 6th international conference on Aspect-oriented software development, March 12-16, 2007, Vancouver, British Columbia, Canada [doi>10.1145/1218563.1218578]
• 15: The Coq proof assistant: Reference manual, version 8.1. http://coq.inria.fr/, 2006.
• 16: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 17: Erik Ernst. gbeta: A Language with Virtual Attributes, Block Structure, and Propagating, Dynamic Inheritance. PhD thesis, Department of Computer Science, University of Aarhus, Århus, Denmark, 1999.
• 18: 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
• 19: Cormac Flanagan, Hybrid type checking, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-256, January 11-13, 2006, Charleston, South Carolina, USA
• 20: Cormac Flanagan, Stephen N. Freund, and Aaron Tomb. Hybrid types, invariants, and refinements for imperative objects. In International Workshop on Foundations of Object-Oriented Programming (FOOL), 2006.
• 21: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 22: Seth Fogarty , Emir Pasalic , Jeremy Siek , Walid Taha, Concoqtion: indexed types now!, Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 15-16, 2007, Nice, France [doi>10.1145/1244381.1244400]
• 23: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 24: Tim Freeman , Frank Pfenning, Refinement types for ML, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.268-277, June 24-28, 1991, Toronto, Ontario, Canada
• 25: 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
• 26: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java(TM) Language Specification, The (3rd Edition) (Java (Addison-Wesley)), Addison-Wesley Professional, 2005
• 27: Christian Grothoff, Jens Palsberg, and Vijay Saraswat. Safe arrays via regions and dependent types. Technical Report RC23911, IBM T.J. Watson Research Center, 2006.
• 28: John Hughes , Lars Pareto , Amr Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.410-423, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.240882]
• 29: Atshushi Igarashi , Benjamin Pierce , Philip Wadler, Featherwieght Java: a minimal core calculus for Java and GJ, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.132-146, November 01-05, 1999, Denver, Colorado, United States
• 30: J. Jaffar , J.-L. Lassez, Constraint logic programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.111-119, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41635]
• 31: Radha Jagadeesan, Gopalan Nadathur, and Vijay A. Saraswat. Testing concurrent systems: An interpretation of intuitionistic logic. In Ramaswamy Ramanujam and Sandeep Sen, editors, FSTTCS, volume 3821 of Lecture Notes in Computer Science, pages 517--528. Springer, 2005.
• 32: Mark P. Jones, Qualified types: theory and practice, Cambridge University Press, New York, NY, 1995
• 33: JSR 308: Annotations on Java types. http://jcp.org/en/jsr/detail?id=308.
• 34: Xavier Leroy et al. The Objective Caml system. http://caml.inria.fr/ocaml/.
• 35: Ole Lehrmann Madsen , Birger Mø-Pedersen , Kristen Nygaard, Object-oriented programming in the BETA programming language, ACM Press/Addison-Wesley Publishing Co., New York, NY, 1993
• 36: 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
• 37: Per Martin-Löf. A Theory of Types. 1971.
• 38: Conor McBride , James McKinna, The view from the left, Journal of Functional Programming, v.14 n.1, p.69-111, January 2004 [doi>10.1017/S0956796803004829]
• 39: Todd Millstein, Practical predicate dispatch, Proceedings of the 19th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 24-28, 2004, Vancouver, BC, Canada
• 40: John C. Mitchell, Coercion and type inference, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.175-185, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800529]
• 41: Andrew C. Myers, JFlow: practical mostly-static information flow control, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-241, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292561]
• 42: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 43: Flemming Nielson , Hanne Riis Nielson, Two-level functional languages, Cambridge University Press, New York, NY, 1992
• 44: Nathaniel Nystrom, Michael R. Clarkson, and Andrew C. Myers. Polyglot: An extensible compiler framework for Java. In Görel Hedin, editor, Compiler Construction, 12th International Conference, CC 2003, number 2622 in LNCS, pages 138--152. Springer-Verlag, April 2003.
• 45: 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
• 46: Nathaniel Nystrom and Vijay Saraswat. An annotation and compiler plugin system for X10. Technical Report RC24198, IBM T.J. Watson Research Center, 2007.
• 47: Martin Odersky. Report on the programming language Scala. Technical report, EPFL, 2006.
• 48: Martin Odersky, Philippe Altherr, Vincent Cremet, Burak Emir, Sebastian Maneth, Stéphane Micheloud, Nikolay Mihaylov, Michel Schinz, Erik Stenman, and Matthias Zenger. An overview of the Scala programming language, June 2004. http://scala.epfl.ch/docu/files/ScalaOverview.pdf.
• 49: Martin Odersky, Vincent Cremet, Christine Röckl, and Matthias Zenger. A nominal theory of objects with dependent types. In Proceedings of 17th European Conference on Object-Oriented Programming (ECOOP 2003), number 2743 in Lecture Notes in Computer Science, pages 201--224. Springer-Verlag, July 2003.
• 50: Martin Odersky and Christoph Zenger. Nested types. In 8th Workshop on Foundations of Object-Oriented Languages (FOOL), 2001.
• 51: 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
• 52: Benjamin C. Pierce, Advanced Topics in Types and Programming Languages, The MIT Press, 2004
• 53: François Pottier, Simplifying subtyping constraints, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.122-133, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 54: William H. Press , Saul A. Teukolsky , William T. Vetterling , Brian P. Flannery, Numerical recipes in FORTRAN (2nd ed.): the art of scientific computing, Cambridge University Press, New York, NY, 1992
• 55: J C Reynolds, Three approaches to type structure, Proc. of the international joint conference on theory and practice of software development (TAPSOFT) Berlin, March 25-29, 1985 on Mathematical foundations of software development, Vol. 1: Colloquium on trees in algebra and programming (CAAP'85), p.97-138, April 1985, Berlin, Germany
• 56: Patrick M. Rondon , Ming Kawaguci , Ranjit Jhala, Liquid types, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 57: Vijay Saraswat. The category of constraint systems is Cartesian closed. In LICS '92, pages 341--345, 1992.
• 58: Vijay Saraswat et al. The X10 language specification. Technical report, IBM T.J. Watson Research Center, 2006.
• 59: Martin Sulzmann, Martin Odersky, and Martin Wehr. Type inference with constrained types. In Fourth International Workshop on Foundations of Object-Oriented Programming (FOOL 4), 1997.
• 60: Martin Sulzmann , Peter j. Stuckey, Hm(x) type inference is clp(x) solving, Journal of Functional Programming, v.18 n.2, p.251-283, March 2008 [doi>10.1017/S0956796807006569]
• 61: Walid Taha , Tim Sheard, Multi-stage programming with explicit annotations, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.203-217, June 12-13, 1997, Amsterdam, The Netherlands
• 62: Valery Trifonov , Scott F. Smith, Subtyping Constrained Types, Proceedings of the Third International Symposium on Static Analysis, p.349-365, September 24-26, 1996
• 63: Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.249-257, June 17-19, 1998, Montreal, Quebec, Canada
• 64: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Object-oriented languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Constraints; Classes and objects

General Terms:
Languages

Keywords:
constraints, dependent types, object-oriented programming languages