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