| 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. |
