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