1ML - core and modules united (F-ing first-class modules)
Venue
International Conference on Functional Programming, ACM-SIGPLAN, Vancouver, Canada (2015)
Publication Year
2015
Authors
BibTeX
Abstract
ML is two languages in one: there is the core, with types and expressions, and
there are modules, with signatures, structures and functors. Modules form a
separate, higher-order functional language on top of the core. There are both
practical and technical reasons for this stratification; yet, it creates
substantial duplication in syntax and semantics, and it reduces expressiveness. For
example, selecting a module cannot be made a dynamic decision. Language extensions
allowing modules to be packaged up as first-class values have been proposed and
implemented in different variations. However, they remedy expressiveness only to
some extent, are syntactically cumbersome, and do not alleviate redundancy. We
propose a redesign of ML in which modules are truly first-class values, and core
and module layer are unified into one language. In this "1ML", functions, functors,
and even type constructors are one and the same construct; likewise, no distinction
is made between structures, records, or tuples. Or viewed the other way round,
everything is just ("a mode of use of") modules. Yet, 1ML does not require
dependent types, and its type structure is expressible in terms of plain System Fω,
in a minor variation of our F-ing modules approach. We introduce both an explicitly
typed version of 1ML, and an extension with Damas/Milner-style implicit
quantification. Type inference for this language is not complete, but, we argue,
not substantially worse than for Standard ML. An alternative view is that 1ML is a
user-friendly surface syntax for System Fω that allows combining term and type
abstraction in a more compositional manner than the bare calculus.
