Vincent Cremet and Philippe Altherr: Adding Type Constructor Parameterization to Java, JOT vol. 7, no. 5.

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.

FGJ_{Ï‰} is a simple extension of (Featherweight) Java's generics, where type parameters may be type constructors (functions from types to types). This very readable paper finally made me understand GADTs.

(Previously: Generics of a Higher Kind on Scala's support for the same idea.)

## Recent comments

23 min 31 sec ago

1 hour 17 min ago

4 hours 59 min ago

1 day 3 hours ago

1 day 3 hours ago

4 days 16 hours ago

5 days 6 hours ago

5 days 9 hours ago

1 week 7 hours ago

1 week 8 hours ago