Home > lambdatheultimate > Adding Type Constructor Parameterization to Java

Adding Type Constructor Parameterization to Java

May 24th, 2010 05:49 admin Leave a comment Go to comments

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.)

Source: Adding Type Constructor Parameterization to Java

Related Articles:

  1. First-class modules: hidden power and tantalizing promises
  2. Erasure and Polymorphism in Pure Type Systems
  3. Recent Apple Java Update Doesn’t Fix Critical Java Flaw Claims Researcher
  4. Amazon Courts Windows Developers by Adding .Net to its Elastic Beanstalk
  5. New Java Vulnerability Found Affecting Java 5, 6, and 7 SE
blog comments powered by Disqus