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 signature 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 integrates 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 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”.
Mon 24 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
13:00 - 14:30 | Program ConstructionResearch Papers at Stifel Theatre Chair(s): J. Garrett Morris University of Kansas, USA | ||
13:00 22mTalk | Prototyping a Functional Language using Higher-Order Logic Programming: A Functional Pearl on Learning the Ways of λProlog/Makam Research Papers DOI | ||
13:22 22mTalk | A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs Research Papers Guillaume Allais Radboud University Nijmegen, Robert Atkey University of Strathclyde, James Chapman , Conor McBride , James McKinna DOI | ||
13:45 22mTalk | Reasonably Programmable Literal Notation Research Papers Link to publication DOI | ||
14:07 22mTalk | Refunctionalization of Abstract Abstract Machines: Bridging the Gap between Abstract Abstract Machines and Abstract Definitional Interpreters (Functional Pearl) Research Papers DOI |