Code editors provide essential services that help developers understand, navigate, and modify programs. However, these services often fail in the presence of syntax errors. Existing syntax error recovery techniques, like panic mode and multi-option repairs, are either too coarse, e.g. in deleting large swathes of code, or lead to a proliferation of possible completions. This paper introduces tall tylr , an error-handling parser and editor generator that completes malformed code with syntactic obligations that abstract over many possible completions. These obligations generalize the familiar notion of holes in structure editors to cover missing operands, operators, delimiters, and sort transitions. tall tylr is backed by a novel theory of tile-based parsing, conceptually organized around a molder that turns tokens into tiles and a melder that completes and parses tiles into terms using an error-handling generalization of operator-precedence parsing. We formalize melding as a parsing calculus, meldr, that completes input tiles with additional obligations such that it can be parsed into a well-formed term, with success guaranteed over all inputs. We further describe how tall tylr implements molding and completionranking using the principle of minimizing obligations . Obligations offer a useful way to scaffold internal program representations, but in tall tylr we go further to investigate the potential of materializing these obligations visually to the programmer. We conduct a user study to evaluate the extent to which an editor like tall tylr that materializes syntactic obligations might be usable and useful, finding both points of positivity and interesting new avenues for future work.

Structure editors have long promised to facilitate a continuous dialogue between programmer and system-one uninterrupted by syntax errors, such that vital program analyses and editor services are always available. Unfortunately, structure editors are notoriously slow or difficult to use, particularly when it comes to modifying existing code. Prior designs often struggle to resolve the tension between maintaining a program's hierarchical structure and supporting the editing affordances expected of its linear projection. We propose the paradigm of gradual structure editing, which mitigates this tension by allowing for temporary disassembly of hierarchical structures as needed for text-like editing, while scaffolding these interactions by generating syntactic obligations that, once discharged, guarantee proper reassembly. This paper contributes the design and evaluation of a gradual structure editor called teen tylr. We conducted a lab study comparing teen tylr to a text editor and a traditional structure editor on structurally complex program editing tasks, and found that teen tylr helped resolve most usability problems we identified in prior work, though not all, while achieving competitive performance with text editing on most tasks. We conclude with a discussion of teen tylr's remaining limitations and design implications for future code editors and parsers.

Several modern programming systems, including GHC Haskell, Agda, Idris, and Hazel, support typed holes . Assigning static and, to varying degree, dynamic meaning to programs with holes allows program editors and other tools to offer meaningful feedback and assistance throughout editing, i.e. in a live manner. Prior work, however, has considered only holes appearing in expressions and types. This paper considers, from type theoretic and logical first principles, the problem of typed pattern holes. We confront two main difficulties, (1) statically reasoning about exhaustiveness and irredundancy when patterns are not fully known, and (2) live evaluation of expressions containing both pattern and expression holes. In both cases, this requires reasoning conservatively about all possible hole fillings. We develop a typed lambda calculus, Peanut, where reasoning about exhaustiveness and redundancy is mapped to the problem of deriving first order entailments. We equip Peanut with an operational semantics in the style of Hazelnut Live that allows us to evaluate around holes in both expressions and patterns. We mechanize the metatheory of Peanut in Agda and formalize a procedure capable of deciding the necessary entailments. Finally, we scale up and implement these mechanisms within Hazel, a programming environment for a dialect of Elm that automatically inserts holes during editing to provide static and dynamic feedback to the programmer in a maximally live manner, i.e. for every possible editor state. Hazel is the first maximally live environment for a general-purpose functional language.

Programming has become a collaboration between human programmers, who drive intent, and interactive assistants that suggest contextually relevant editor actions. There has been considerable work on suggestion synthesis strategies—from semantic autocomplete to modern program synthesis, repair, and machine learning research. This diversity of contextually viable strategies creates a need for an integrative, human-centered perspective on the problem of programming assistant design that (1) confronts the problem of integrating a variety of synthesis strategies, fed by shared semantic analyses capable of operating on program sketches, and (2) centers the needs of the human programmer: comprehending, comparing, ranking, and filtering suggestions generated by various synthesizers, and in some cases participating in a synthesizer’s search by supplying additional expressions of intent. This paper contributes a conceptual architecture and API to guide programming assistant designers as they confront these integration and human-centered design challenges. We then instantiate this architecture with two prototype end-to-end assistant designs, both developed for the Hazel programming environment, that emphasize understudied design aspects, namely continuity, explainability, human-in-the-loop synthesis, and the integration of multiple analyses with multiple synthesis strategies.

Text editing is powerful, but some types of expressions are more naturally represented and manipulated graphically. Examples include expressions that compute colors, music, animations, tabular data, plots, diagrams, and other domain-specific data structures. This paper introduces live literals, or livelits, which allow clients to fill holes of types like these by directly manipulating a user-defined GUI embedded persistently into code. Uniquely, livelits are compositional: a livelit GUI can itself embed spliced expressions, which are typed, lexically scoped, and can in turn embed other livelits. Livelits are also uniquely live: a livelit can provide continuous feedback about the run-time implications of the client’s choices even when splices mention bound variables, because the system continuously gathers closures associated with the hole that the livelit is filling. We integrate livelits into Hazel, a live hole-driven programming environment, and describe case studies that exercise these novel capabilities. We then define a simply typed livelit calculus, which specifies how livelits operate as live graphical macros. The metatheory of macro expansion has been mechanized in Agda.