F. Damiani
Rank 2 intersection types for modules
In Proc. 5th Int'l Conf. Principles & Practice Declarative
Programming, pages 67-78, 2003
We
present a rank 2 intersection type system for a language of modules built
on a core ML-like language. The principal typing property of the rank
2 intersection type system for the core language plays a crucial role in the
design of the type system for the module language. We first considers a
``plain'' notion of module, where a module is just a set of mutually recursive
top-level definitions, and illustrates the notions of:
module intrachecking (each module is typechecked in isolation and its
interface, that is the set of typings of the defined identifiers,
is inferred);
interface interchecking
(when linking modules, typechecking is done just by looking at the interfaces);
interface specialization (interface intrachecking may require to
specialize the typing listed in the interfaces);
principal interfaces (the principal typing property for the type system
of modules);
and separate typechecking (looking at the code of the modules does not
provide more type information than looking at their interfaces).
Then we illustrate some limitations of the ``plain'' framework and extend the
module language and the type system in order to overcome these limitations.
The decidability of the system is shown by providing
algorithms for the fundamental operations involved in module intrachecking
and interface interchecking.
[ bib |
.pdf |
.html ]
Back
This file has been generated by
bibtex2html 1.43