[TYPES] System F and Type Generativity

[Matthias Blume]

Have you looked at Derek Dreyer's RTG paper?  (RTG = "Recursive Type  
Generativity")

You might also want to look at "Principal Type Schemes for Modular  
Programs" by Derek and myself.  It uses RTG in the kind of non- 
recursive setting that you probably need.

Matthias

On Sep 8, 2009, at 5:50 PM, George Kuan wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list 
>  ]
>
> 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?
>
> - George