Reference. Reasonably programmable literal notation

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”.

Cite

Cite as @omar-2018-reasonably (helia, typst) · \cite{omar-2018-reasonably} (LaTeX)
BibTeX
bibtex · 1 line
@article{omar-2018-reasonably, title={Reasonably programmable literal notation}, volume={2}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3236801}, DOI={10.1145/3236801}, number={ICFP}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Omar, Cyrus and Aldrich, Jonathan}, year={2018}, month=July, pages={1–32} }
hayagriva YAML (typst)
yaml · 16 lines
omar-2018-reasonably:
  type: article
  title: Reasonably programmable literal notation
  author:
  - Omar, Cyrus
  - Aldrich, Jonathan
  date: 2018-07
  page-range: 1-32
  serial-number:
    doi: 10.1145/3236801
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: ICFP
    volume: 2
Cited by (2)

Contextualized Programming Language Documentation potter-2022-contextualized

PDF · DOI · pldb

Filling typed holes with live GUIs omar-2021-filling

PDF · DOI · pldb
Cites 76 works (5 here)
With notes (5)

Hazelnut: a bidirectionally typed structure editor calculus omar-2017-hazelnut

PDF · DOI · arXiv · pldb

Safely Composable Type-Specific Languages omar-2014-safely

DOI · pldb

Validating LR(1) Parsers jourdanValidatingLRParsers2012

An LR(1) parser is a finite-state automaton, equipped with a stack, which uses a combination of its current state and one lookahead symbol in order to determine which action to perform next. We present a validator which, when applied to a context-free grammar G and an automaton A, checks that A and G agree. Validating the parser provides the correctness guarantees required by verified compilers and other high-assurance software that involves parsing. The validation process is independent of which technique was used to construct A. The validator is implemented and proved correct using the Coq proof assistant. As an application, we build a formally-verified parser for the C99 language.
PDF · DOI · pldb

Yacc: Yet another compiler-compiler Johnsonyacc

Computer program input generally has some structure; in fact, every computer program that does input can be thought of as defining an “input language” which it accepts. An input language may be as complex as a programming language, or as simple as a sequence of numbers. Unfortunately, usual input facilities are limited, difficult to use, and often are lax about checking their inputs for validity. Yacc provides a general tool for describing the input to a computer program. The Yacc user specifies the structures of his input, together with code to be invoked as each such structure is recognized. Yacc turns such a specification into a subroutine that handles the input process; frequently, it is convenient and appropriate to have most of the flow of control in the user’s application handled by this subroutine. The input subroutine produced by Yacc calls a user-supplied routine to return the next basic input item. Thus, the user can specify his input in terms of individual input characters, or in terms of higher level constructs such as names and numbers. The user-supplied routine may also handle idiomatic features such as comment and continuation conventions, which typically defy easy grammatical specification. Yacc is written in portable C. The class of specifications accepted is a very general one: LALR(1) grammars with disambiguating rules. In addition to compilers for C, APL, Pascal, RATFOR, etc., Yacc has also been used for less conventional languages, including a phototypesetter language, several desk calculator languages, a document retrieval system, and a Fortran debugging system.
Web

Programming Techniques: Regular expression search algorithm thompsonProgrammingTechniquesRegular1968

A method for locating specific character strings embedded in character text is described and an implementation of this method in the form of a compiler is discussed. The compiler accepts a regular expression as source language and produces an IBM 7094 program as object language. The object program then accepts the text to be searched as input and produces a signal every time an embedded string in the text matches the given regular expression. Examples, problems, and solutions are also presented.
DOI
External (71)
omar-2018-reasonably reference entries/refs/omar-2018-reasonably/omar-2018-reasonably.hel