paperbot · PL 论文追踪

全部论文 待读 收藏

P2 1ML – Core and modules united

1ML —— 核心与模块的统一
JFP vol.282018匹配度 2/10 · 该论文是编程语言类型系统与模块系统设计的基础理论工作,讨论 1ML 将核心语言与模块统一、用 System Fω 表达类型结构,与用户关注的 LLM/Agent 结合静态分析、浮点程序分析、贝叶斯程序分析等方向没有直接交集。仅作为 PL 类型理论背景有非常间接的参考价值。引用 12 inbox
ANDREAS ROSSBERG
crossref: 2026-09-10

AI 速览

一句话:提出 1ML,将 ML 核心与模块统一为一种语言,使模块成为一等值,并用 System Fω 表达其类型结构。

ML 传统上分为核心语言与模块语言,模块是建立在核心之上的高阶函数式子语言,造成语法语义重复并限制表达力,例如无法动态选择实现某接口的模块。已有把模块打包为一等值的扩展仍较繁重。本文重新设计 ML,提出 1ML:模块真正成为一等值,核心与模块统一为一种语言,函数、函子乃至类型构造器合为同一构造,结构、记录与元组不再区分,一切皆是模块的使用模式。1ML 不依赖依赖类型,其类型结构可用 System Fω 加 F-ing modules 变体表达。文章给出显式类型版本和 Damas–Milner 式隐式量化扩展;类型推断不完全,但论证不比 Standard ML 严重得多。

问题
ML 的核心与模块分层导致语法和语义重复、模块为二等公民,并限制表达力,例如无法动态选择某个接口的实现模块。
方法
将模块提升为一等值,统一核心与模块层,使函数、函子与类型构造器成为同一构造,并用 System Fω 与 F-ing modules 的变体刻画类型结构,提供显式类型与隐式量化两个版本。
评估
评估以语言设计与类型系统形式化论证为主:说明其表达力、System Fω 编码方式,并讨论类型推断的不完全性及其与 Standard ML 的比较。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot342,
  title = {1ML – Core and modules united},
  author = {ANDREAS ROSSBERG},
  journal = {Journal of Functional Programming},
  volume = {28},
  year = {2018},
  doi = {10.1017/s0956796818000205}
}