# 1ML

1ML -- core and modules united (F-ing first-class modules). 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.par 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 $mathrm{F}_{omega}$, 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.par An alternative view is that 1ML is a user-friendly surface syntax for System $mathrm{F}_{omega}$ that allows combining term and type abstraction in a more compositional manner than the bare calculus.

## Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

## References in zbMATH (referenced in 4 articles , 1 standard article )

Showing results 1 to 4 of 4.
Sorted by year (citations)