Loading...
Please wait, while we are loading the content...
Similar Documents
1ML – Core and Modules United (F-ing First-class Modules)
| Content Provider | CiteSeerX |
|---|---|
| Author | Rossberg, Andreas |
| Abstract | ML is two languages in one: there is the core, with types and ex-pressions, and there are modules, with signatures, structures and functors. Modules form a separate, higher-order functional lan-guage 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 exam-ple, selecting a module cannot be made a dynamic decision. Lan-guage 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 syn-tactically 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 lan-guage. In this “1ML”, functions, functors, and even type construc-tors 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 express-ible 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 quan-tification. 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. |
| File Format | |
| Access Restriction | Open |
| Content Type | Text |
