When programming, we spend a substantial amount of our time working on programs that are not yet complete. For example, there can be blank spots, type errors or merge conflicts at multiple locations in the program. Conventional programming language definitions assign no formal meaning to incomplete programs like these, so development tools have no choice but to resort to ad hoc heuristics to provide various useful language services without interruption, including code completion, type inspection, code navigation, and live programming and debugging services.
We are working to develop a more principled approach to working with incomplete programs, rooted in the first principles of type theory. We model incomplete programs as programs with holes, which (1) stand for parts of the program that are missing; and (2) serve as membranes around parts of the program that are erroneous or, in the collaborative setting, conflicted.
We are incorporating our research results into Hazel, a web-based programming environment for an Elm-like functional language. Hazel is designed from the ground up to support typed hole-driven development.
The following paper describes this research vision in more detail.
Hazelnut (POPL 2017)
To start, we have developed a core calculus, called Hazelnut, that provides 1) a type system for expressions with holes in both expression and type position, and 2) a language of type-aware structured edit actions that insert holes automatically.
The following research paper, published at POPL 2017, details Hazelnut.
- Hazelnut: A Bidirectionally Typed Structure Editor Calculus (POPL, Jan. 2017 [.bib])
Hazelnut Live (Draft Paper)
We are now working to understand, from type-theoretic first principles, how we might evaluate the programs with holes that Hazelnut produces (without simply stopping at the first hole), and how we might granularly interleave editing with evaluation (i.e. live programming). The goal is for us to be able to provide both static and dynamic feedback to the programmer about every possible editor state in Hazel.
The following research paper details how we achieve this goal by borrowing machinery from both gradual type theory and contextual modal type theory.
- Live Functional Programming with Typed Holes (draft paper, April 2018)
We have mechanized the metatheory of Hazelnut Live using the Agda proof assistant.
We have implemented the features described in the paper in Hazel.
LIVE 2017 Presentation
Cyrus presented some of this work at the LIVE 2017 workshop.
- Toward a Live Stepper for Typed Expressions with Holes (Extended Abstract, LIVE 2017)
OBT 2017 PresentationIan presented a much earlier take on this work at the Off the Beaten Track (OBT) workshop at POPL 2017.
We have a number of ideas incubating — if you're interested in any of these, definitely get in touch. We would also love to hear about other ideas you might have.
We are thinking about how to specify an edit action semantics that obeys the invariants necessary to make a Hazelnut program a conflict-free replicated data type (CRDT).
Programming by Direct Manipulation of GUIs with Typed Holes
We are thinking about how to integrate GUIs directly into Hazel expressions, and how to integrate Hazel expressions directly into GUIs.
We are thinking about how to use Hazel to programmatically control Hazel.
Edit Action Synthesis and Suggestion
We are thinking about how to suggest useful edit action suggestions for the programmer, using both semantic constraints and machine learning.
As Hazel evolves, we plan to apply it first to teach introductory functional programming courses, and later on we plan to use Hazel to do data analysis, music and visual art. One day, we hope that Hazel will be the foundation for a new kind of programmable wiki.
(h/t Vincent Zeng)