[TYPES] System F and Type Generativity

[Xavier Leroy]

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?

You might be interested in recent work by Benoît Montagu and Didier Rémy:

"Modeling Abstract Types in Modules with Open Existential Types".
In Proceedings of the 36th ACM Symposium on Principles of Programming
Languages (POPL'09), pages 63-74, Savannah, Georgia, USA, January
2009.

http://gallium.inria.fr/~remy/modules/Montagu-Remy@popl09:fzip.pdf

- Xavier Leroy