Recursive type generativity

Existential types provide a simple and elegant foundation for uning generative abstract data types, of the kind supported by the Standard ML module system. However, in attempting to extend ML with support for recursive modules, we have found that the traditional existential account of type generativity does not work well in the presence of mutually recursive module definitions. The key problem is that, in recursive modules, one may wish to define an type in a context where a name for the type already exists, but the existential type mechanism does not allow one to do so. We propose a novel account of recursive type generativity that resolves this problem. The basic idea is to separate the act of generating a name for an abstract type from the act of defining its underpresentation. To define several abstract types recursively, one may first "forward-declare" them by generating their names, and then define each one secretly within its own defining expression. Intuitively, this...

• Type: Conference
• Year: 2005
• Where: ICFP
• Authors: Derek Dreyer
• Keywords: Abstract Data Types, Existential Type Mechanism, ICFP 2005, Programming Languages, Undefined Abstract Type