kirancodes.me
To Proof Maintenance & Beyond!

Higher-Order Functors with Transparent Signatures

Sandip K. Biswas

Abstract

The programming language Standard ML provides first-order functors, i.e. modules parameterized by modules. First-order functors in the language have a simple and elegant static semantics. The type structure of higher-order modules, i.e. modules parameterized by functors, is well understood. But it is only in the recent past that we have seen an implementation of higher-order functors with a formally defined static semantics in a dialect of Standard ML, SML/NJ. A study of this static semantics shows it to be much more complicated than the static semantics of first-order functors. This paper investigates whether we can trade some semantic features in the module language to obtain a simpler static semantics, closer in spirit to that of first-order functors. This work helps in a conceptual understanding of the semantics of higher-order modules.

Related papers