Adding Type Constructor Parameterization to Java

Vincent Cremet, France
Philippe Altherr, Switzerland

REFEREED
ARTICLE

Abstract

We present a generalization of Java’s parametric polymorphism that enables parameterization of classes and methods by type constructors, i.e., functions from types to types. Our extension is formalized as a calculus called FGJ_ω. It is implemented in a prototype compiler and its type system is proven safe and decidable. We describe our extension and motivate its introduction in an object-oriented context through two examples: the definition of generic data-types with binary methods and the definition of generalized algebraic data-types. The Coq proof assistant was used to formalize FGJ_ω and to mechanically check its proof of type safety.

Note: Due to the typographical sophistication of this article, no HTML version is available. Please use the PDF version.

About the author

Vincent Cremet received a Ph.D. in Computer Science from EPFL, Switzerland in 2006. His research interests include the design and formal proof of advanced type systems for object-oriented languages. He can be reached at vincent.cremet@gmail.com. See also http://lamp.epfl.ch/~cremet/

Philippe Altherr received a Ph.D. in Computer Science from EPFL, Switzerland in 2006. His research interests include programming language design and compiler implementation techniques. His email address is philippe.altherr@gmail.com.

Vincent Cremet and Philippe Altherr: "Adding Type Constructor Parameterization to Java", in Journal of Object Technology, vol. 7, no. 5, Special Issue: Workshop on FTfJP, ECOOP 07, June 2008, pp.25-65 http://www.jot.fm/issues/issue_2008_06/article2/