When programming, we spend a substantial amount of our time working with program text that is not yet a formally complete program, e.g. because there are blank spots, type errors or merge conflicts at various locations. Conventional programming language definitions assign no formal meaning to structures like these, so program editors and other tools have no choice but to resort to complex and ad hoc heuristics to provide various useful language services (like code completion, type inspection, code navigation, and live programming services) without gaps in service.
We are developing a more principled approach to working with incomplete programs, rooted in (contextual modal and gradual) 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.
This hole-oriented approach is broadly relevant, but we are incorporating our results into Hazel, a web-based programming environment for an Elm/ML-like functional language that is being designed from the ground up around typed hole-driven development.
Uniquely, every incomplete program that you can construct using Hazel's language of type-aware edit actions is both statically and dynamically well-defined, i.e. it has a (possibly incomplete) type, and you can run it to produce a (possibly incomplete) result. Consequently, Hazel serves as an elegant platform for research on the future of programming.
The following paper describes our research vision in more detail.
Hazelnut (POPL 2017)
To start, we developed a core calculus, Hazelnut, that contributes (1) a static semantics (i.e. type system) for expressions with holes in both expression and type position, and (2) a language of edit actions that insert holes automatically to ensure that every edit state has static meaning.
The following research paper details Hazelnut.
C. Omar, I. Voysey, M. Hilton, J. Aldrich and M. Hammer
POPL 2017 [.bib] [slides]
Hazelnut Live (to appear, POPL 2019)
Next, we developed Hazelnut Live, which contributes a dynamic semantics for expressions with holes in both expression and type position. Rather than stopping as soon as we encounter a hole at run-time, we continue evaluation as far as possible, producing a result containing hole closures. Hole closures allow us to continuously provide granular live feedback to the programmer, and to resume evaluation once a hole is filled.
The following research paper details how we achieve this by adapting machinery from gradual type theory and contextual modal type theory.
C. Omar, I. Voysey, R. Chugh and M. Hammer
POPL 2019 (to appear, Jan 2019) [.bib]
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.
Live and Direct Functional Programming with Palette Expressions
We are thinking about how to integrate user-defined GUIs directly into Hazel expressions, and how to integrate Hazel expressions directly into user-defined GUIs.
Collaborative Editing with CRDTs
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).
We are thinking about how to use Hazel to define higher-level semantics-aware edit actions.
Edit Action Synthesis and Suggestion
We are thinking about how to suggest useful edit actions to the programmer by feeding the semantic data that Hazel makes available into program synthesis and machine learning algorithms.
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 (think a next-generation Jupyter). One day, we hope that Hazel will be the foundation for a new kind of computational wiki.
- Cyrus Omar, UChicago
- Ian Voysey, CMU
- Nick Collins, UChicago
- Ravi Chugh, UChicago
- David Moon, CU Boulder
- Matthew A. Hammer, CU Boulder
- Brandon Kase
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!
Recent & Upcoming Talks
(h/t Vincent Zeng)