一句话:提出 1ML,将 ML 核心与模块统一为一种语言,使模块成为一等值,并用 System Fω 表达其类型结构。
ML 传统上分为核心语言与模块语言,模块是建立在核心之上的高阶函数式子语言,造成语法语义重复并限制表达力,例如无法动态选择实现某接口的模块。已有把模块打包为一等值的扩展仍较繁重。本文重新设计 ML,提出 1ML:模块真正成为一等值,核心与模块统一为一种语言,函数、函子乃至类型构造器合为同一构造,结构、记录与元组不再区分,一切皆是模块的使用模式。1ML 不依赖依赖类型,其类型结构可用 System Fω 加 F-ing modules 变体表达。文章给出显式类型版本和 Damas–Milner 式隐式量化扩展;类型推断不完全,但论证不比 Standard ML 严重得多。
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 imposes seemingly unnecessary limits on expressiveness because it makes modules second-class citizens of the language. For example, selecting one among several possible modules implementing a given interface 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 and tend to be even more syntactically heavyweight than using second-class modules alone. We propose a redesign of ML in which modules are truly first-class values, and core and module layers are unified into one language. In this “1ML”, functions, functors, and even type constructors are one and the same construct; likewise, no distinction is needed 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: its type structure is expressible in terms of plain System F ω , with 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.