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 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/