[TYPES] System F and Type Generativity

[Andreas Rossberg]

On Sep 9, 2009, at 00.50 h, George Kuan wrote:

> ML datatypes and opaque sealing are the source of type generativity in
> the ML module system. This generativity is sometimes modeled using
> existential types. However, a more direct modeling of generativity
> would be to consider generativity as a special operator G in a variant
> of System F that takes a type expression and produces a new unique
> type unequal to all others. This would be essentially a type-level
> effect. Are there any variants of System F that include such an
> extension?

I described such a system in my PPDP'03 paper [1]. A similar type  
generation construct is used in [2]. An extension of [1] with  
singleton kinds appears in [3].

There also is Derek's RTG calculus [4], which targets recursive  
modules and hence is more flexible, but also more complex.

A streamlined version of the system from [1], called G (sic!), is used  
in our recent ICFP paper [5], and is probably the most minimalist  
extension of F with type generation.

- Andreas


[1] Andreas Rossberg. Generativity and Dynamic Opacity for Abstract  
Types. PPDP'03

[2] Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich. An  
open and shut typecase. TLDI'05

[3] Andreas Rossberg. Dynamic Translucency with Abstraction Kinds and  
Higher-Order Coercions, MFPS'08

[4] Derek Dreyer. Recursive Type Generativity. JFP 17(4+5)

[5] Georg Neis, Derek Dreyer, Andreas Rossberg. Non-Parametric  
Parametricity. ICFP'09.