Rank 2 Intersection Types for Modules

摘要

We propose 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 consider a "plain" notion of module, where a module is just a set of mutually recursive top-level definitions, and illustrate the notions of: module intrachecking (each module is typechecked in isolation and its interface, which 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.