Reasonably programmable literal notation
Reasonably programmable literal notation
复制标题
合理可编程的文字表示法
DOI：
10.1145/3236801
复制
发表时间：
2018
影响因子：
--
通讯作者：
Jonathan Aldrich
中科院分区：
文献类型：
--
作者：
Cyrus Omar;Jonathan Aldrich
通用编程语言通常只为少数常见的数据结构（如列表）定义文字表示法。这是不令人满意的，因为有许多其他的数据结构，文字符号可能是有用的，例如有限映射，正则表达式，HTML元素，SQL查询，各种语言的语法树和化学结构。这些数据结构中的每一个也可能在公共接口后面有不同的实现，这些接口都可以从公共文字符号中受益。本文介绍了类型化文字宏（TLM），它允许库提供者在任何指定的类型或参数化的类型族上定义几乎任意设计的新文字符号。与现有的方法相比，TLM是唯一合理的。TLM客户端可以抽象地推理，即不检查语法或生成的扩展，关于类型和绑定。系统只需要通过二级符号向客户端传达每个文字主体的推断分割，这给出了拼接子项的位置和类型。TLM提供者可以根据明确的标准模块化地推理语法歧义和扩展正确性。本文将TLM集成到Reason中，Reason是OCaml的一个新兴的替代前端，并通过几个重要的案例研究演示了TLM如何与OCaml的高级功能集成，包括模式匹配和模块系统。我们还讨论了与MetaOCaml的可选集成，这使得TLM提供者对类型正确性更有信心。最后，我们正式建立这些抽象的推理原则与详细的类型理论帐户的表达和模式TLM的“核心ML”。
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 introduces typed 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 uniquely reasonable. 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 inferred segmentation of 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”.