paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Explicit Effects and Effect Constraints in ReML

ReML 中的显式效应与效应约束
POPL 8(POPL)2024匹配度 2/10 · 论文属于类型系统、效应系统与区域内存管理的基础 PL 工作,虽涉及静态推断,但未涉及 LLM/Agent、ML/Agentic 程序静态分析、浮点程序分析或贝叶斯程序分析,与用户当前追踪的核心交叉方向匹配度低。引用 3 inbox
Martin Elsman
crossref: 2026-09-10

AI 速览

一句话:提出 ReML 语言,通过显式效应与效应约束支持区域基内存管理,并集成多态区域推断。

在受限硬件或专用硬件上构建健壮系统时,控制程序效应(尤其是内存管理相关效应)至关重要。本文提出 ReML——一种高阶、静态类型函数式语言,允许程序员显式声明代码执行的效应、值所在的区域以及代码执行所满足的约束。这种显式性使程序对源代码修改和编译器更新(包括优化)更具鲁棒性。ReML 集成了一个多态推断系统,该系统建立在区域推断之上,并已在 MLKit(一个以区域基内存管理为主要内存管理方案的 Standard ML 编译器)中实现,从而说明显式效应与约束有助于在受限环境中实现可预测的代码行为。

问题
在受限或专用硬件上构建健壮系统时,需要显式控制程序代码所执行的效应,尤其是内存管理相关效应,而现有语言对此缺乏显式表达与约束机制。
方法
设计高阶静态类型函数式语言 ReML,让程序员显式声明效应、值所在区域及执行约束,并在区域推断之上构建多态推断系统,集成到 MLKit 中。
评估
在 MLKit(以区域基内存管理为主要方案的 Standard ML 编译器)中实现 ReML,论证显式效应与约束可使程序对源码修改和编译器优化保持稳健。
原文摘要(Abstract)

An important aspect of building robust systems that execute on dedicated hardware and perhaps in constrained environments is to control and manage the effects performed by program code. We present ReML, a higher-order statically-typed functional language, which allows programmers to be explicit about the effects performed by program code and in particular effects related to memory management Allowing programmers to be explicit about effects, the regions in which values reside, and the constraints under which code execute, makes programs robust to changes in the program source code and to compiler updates, including compiler optimisations. ReML is integrated with a polymorphic inference system that builds on top of region-inference, as it is implemented in the MLKit, a Standard ML compiler that uses region-based memory management as its primary memory management scheme.

链接与引用

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

BibTeX
@article{paperbot2588,
  title = {Explicit Effects and Effect Constraints in ReML},
  author = {Martin Elsman},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {POPL},
  year = {2024},
  doi = {10.1145/3632921}
}