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.
Our results are broadly applicable, but we are incorporating them into Hazel, a web-based programming environment for an Elm-like functional language that is being designed from the ground up to support typed hole-driven development. The Hazel implementation is a work-in-progress. As Hazel evolves, we plan to apply it first to teach introductory functional programming.
The following paper describes this research vision in more detail.
Research Result: 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])
Draft Paper: Hazelnut Live
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, July 2018)
We are mechanizing the metatheory of Hazelnut Live using the Agda proof assistant.
We have implemented the user interface elements described in the paper in Hazel.
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 convergent 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.
- Cyrus Omar, UChicago
- Ian Voysey, CMU
- Matthew A. Hammer, CU Boulder
- Ravi Chugh, UChicago
- Brandon Kase
- Nick Collins, UChicago
If you're interested in working on Hazel, in any capacity, or want a mentor to help you learn the necessary type theory, get in touch!
(h/t Vincent Zeng)