paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Ultimate Conditional Syntax

终极条件语法
OOPSLA 8(OOPSLA2)2024匹配度 2/10 · 该论文属于编程语言设计与形式语义,研究模式匹配语法及其去糖和语义保持,但不涉及 LLM/Agent、机器学习系统静态分析、浮点程序分析或贝叶斯程序分析,与用户研究画像的核心交叉方向无关。引用 4 inbox
Luyu Cheng, Lionel Parreaux
dblp: 2026-09-10crossref: 2026-09-10

AI 速览

一句话:提出一种支持并行/嵌套匹配与条件模式流动的新型模式匹配语法,可脱糖到无回溯核心并保持语义。

函数式语言虽已有丰富模式匹配,但现有扩展如视图模式、模式守卫、if-let 等仍难同时表达并行/嵌套匹配与计算穿插。本文提出“终极条件语法”,以带条件分裂机制的嵌套多路 if 表达式和条件模式流动为核心,支持在匹配中插入计算与中间绑定,并共享公共条件前缀。作者在 ML 家族新语言 MLscript 中给出示例,将丰富源语法脱糖为仅含平坦模式的最小核心语法,赋予直观小步语义;再从核心翻译为无回溯的规范化语法,便于覆盖检查与编译,并形式证明该翻译保持语义。该设计可部分或整体集成到现有及未来语言中。

问题
现有模式匹配扩展难以简洁、可读地同时支持并行/嵌套匹配、计算穿插和公共条件前缀复用。
方法
提出终极条件语法,结合嵌套多路 if、条件分裂与条件模式流动,并定义到平坦模式核心及无回溯规范化语法的脱糖/翻译,形式证明语义保持。
评估
在 MLscript 中用大量示例说明表达力与可读性,并给出核心语法小步语义及翻译的语义保持证明,覆盖检查与编译适用性为设计目标。
原文摘要(Abstract)

Functional programming languages typically support expressive pattern-matching syntax allowing programmers to write concise and type-safe code, especially appropriate for manipulating algebraic data types. Many features have been proposed to enhance the expressiveness of stock pattern-matching syntax, such as pattern bindings, pattern alternatives (a.k.a. disjunction), pattern conjunction, view patterns, pattern guards, pattern synonyms, active patterns, ‘if-let’ patterns, multi-way if-expressions, etc. In this paper, we propose a new pattern-matching syntax that is both more expressive and (we argue) simpler and more readable than previous alternatives. Our syntax supports parallel and nested matches interleaved with computations and intermediate bindings. This is achieved through a form of nested multi-way if-expressions with a condition-splitting mechanism to factor common conditional prefixes as well as a binding technique we call conditional pattern flowing . We motivate this new syntax with many examples in the setting of MLscript, a new ML-family programming language. We describe a straightforward desugaring pass from our rich source syntax into a minimal core syntax that only supports flat patterns and has an intuitive small-step semantics. We then provide a translation from the core syntax into a normalized syntax without backtracking, which is more amenable to coverage checking and compilation, and formally prove that our translation is semantics-preserving. We view this work as a step towards rethinking pattern matching to make it more powerful and natural to use. Our syntax can easily be integrated, in part or in whole, into existing as well as future programming language designs.

链接与引用

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

BibTeX
@article{ChengP24,
  title = {The Ultimate Conditional Syntax},
  author = {Luyu Cheng and Lionel Parreaux},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {OOPSLA2},
  year = {2024},
  doi = {10.1145/3689746}
}