A true higher-order module system.
详细信息
文摘
The ML module system is a powerful and expressive language for modular programming and enforcing data abstraction. Several dialects of ML have extended the module system with support for higher-order modules, which improves support for modular programming and elevates the module system to a full functional language. With the exception of Standard ML of New Jersey and MLton, higher-order modules in all these dialects do not obey natural beta-reduction semantics for higher-order functor application true higher-order semantics ). The design space and semantics of a true higher-order module system have not been thoroughly explored. Most of the existing formal accounts of module system semantics neglect true higher-order semantics by separating higher-order functors from type generativity, which limits the flexibility of higher-order functors. The accounts which consider higher-order module semantics neglect to account for interactions between higher-order modules and key core language features such as generative datatype declarations. True higher-order semantics also paradoxically complicates true separate compilation. In this dissertation, I contribute 1) a novel formal account of a module system with true higher-order semantics, 2) a static entity calculus that cleanly isolates and expresses the higher-order semantics, 3) an exploration of the design space of higher-order module semantics including true separate compilation and the signature calculus, and 4) a translation semantics for compiling the module system to a variant of System Fo.