paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Reasonably programmable literal notation

可合理编程的字面量记法
ICFP 2(ICFP)2018匹配度 1/10 · 该论文属于编程语言设计与类型论范畴,研究可编程字面量宏及其形式化,不涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析。与用户当前核心研究方向几乎没有交集,仅可视为广义 PL 领域的背景知识。引用 7 inbox
Cyrus Omar, Jonathan Aldrich
crossref: 2026-09-10

AI 速览

一句话:提出类型化字面量宏(TLM),让库在 Reason/OCaml 中定义可抽象推理的新字面量记法,并给出类型论形式化。

通用语言只为少数常见数据结构提供字面量记法,但有限映射、正则表达式、SQL、语法树等也需要。论文提出类型化字面量宏(TLM),允许库提供者在指定类型或参数化类型族上定义任意设计的新记法。相比已有方法,TLM 的“合理”性在于:客户端可抽象推理类型与绑定,无需检查语法或展开;系统仅通过次级记法传达字面量体的推断分割,标明拼接子项位置与类型;提供者可按清晰标准模块化推理歧义与正确性。作者将 TLM 集成到 Reason(OCaml 新前端),用非平凡案例展示其与模式匹配、模块系统等特性结合,并讨论与 MetaOCaml 的可选集成。最后为“core ML”的表达式与模式 TLM 建立类型论,形式化抽象推理原则。

问题
通用编程语言的 literal notation 通常只覆盖少量常见数据结构,缺少让库定义任意新字面量记法、同时让客户端抽象推理类型与绑定、提供者模块化保证正确性的机制。
方法
提出 typed literal macros(TLM),将其集成到 Reason/OCaml,通过次级记法暴露字面量体的推断分割,并为 core ML 的表达式与模式 TLM 建立类型论形式化。
评估
通过若干非平凡案例研究展示 TLM 与 OCaml 模式匹配、模块系统等高级特性集成,讨论与 MetaOCaml 的可选集成,并以类型论形式化论证抽象推理原则。
原文摘要(Abstract)

General-purpose programming languages typically define literal notation for only a small number of common data structures, like lists. This is unsatisfying because there are many other data structures for which literal notation might be useful, e.g. finite maps, regular expressions, HTML elements, SQL queries, syntax trees for various languages and chemical structures. There may also be different implementations of each of these data structures behind a common interface that could all benefit from common literal notation. This paper introducestyped literal macros (TLMs), which allow library providers to define new literal notation of nearly arbitrary design at any specified type or parameterized family of types. Compared to existing approaches, TLMs are uniquelyreasonable. TLM clients can reason abstractly, i.e. without examining grammars or generated expansions, about types and binding. The system only needs to convey to clients, via secondary notation, the inferredsegmentationof each literal body, which gives the locations and types of spliced subterms. TLM providers can reason modularly about syntactic ambiguity and expansion correctness according to clear criteria. This paper incorporates TLMs into Reason, an emerging alternative front-end for OCaml, and demonstrates, through several non-trivial case studies, how TLMs integrate with the advanced features of OCaml, including pattern matching and the module system. We also discuss optional integration with MetaOCaml, which allows TLM providers to be more confident about type correctness. Finally, we establish these abstract reasoning principles formally with a detailed type-theoretic account of expression and pattern TLMs for “core ML”.

链接与引用

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

BibTeX
@article{paperbot269,
  title = {Reasonably programmable literal notation},
  author = {Cyrus Omar and Jonathan Aldrich},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {ICFP},
  year = {2018},
  doi = {10.1145/3236801}
}