Hazel is a live functional programming environment featuring typed holes.

Project Summary

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.

We are implementing these ideas into Hazel, a web-based programming environment for an Elm/ML-like functional programming language 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.

Hazelnut: A Bidirectionally Typed Structure Editor Calculus
C. Omar, I. Voysey, M. Hilton, J. Aldrich and M. Hammer
POPL 2017 [.bib] [slides]

We have mechanized the metatheory of Hazelnut using the Agda proof assistant.

Hazelnut Live (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.

Live Functional Programming with Typed Holes
C. Omar, I. Voysey, R. Chugh and M. Hammer
POPL 2019 [.bib]

We have mechanized the metatheory of Hazelnut Live using the Agda proof assistant.

Incubating Ideas

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.

Linearly Editing Typed Trees

We are working on a keyboard-driven editing experience that builds on your intuitions from text editing and that supports complex code reorganization patterns. We are doing user studies.

Livelits: Filling Typed Holes with Live GUIs

We are working on allowing programmers to fill holes by direct manipulation of live GUIs with holes.

Collaborative Structure 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).

Hazel Assistant

We are thinking about how to build a programming assistant that suggests useful edit actions to the programmer by feeding the semantic data that Hazel makes available into program synthesis and machine learning algorithms.

Applications

As Hazel evolves, we plan to apply it first to teach introductory functional programming, and later on we plan to use Hazel to support data analysis (think a next-generation Jupyter). One day, we hope that Hazel will be the foundation for a new kind of computational wiki.

Team Hazel

Cyrus Omar University of Michigan
David Moon University of Michigan
Michael D. Adams University of Michigan
Yongwei Yuan University of Michigan
Ian Voysey Carnegie Mellon University
Nick Collins University of Chicago
Ravi Chugh University of Chicago
Peter-Michael Osera Grinnell College
Ben Shapiro University of Colorado Boulder
Xuanrui (Ray) Qi Nagoya University
Charles Chamberlain Open Source Contributor
Nick Smith Open Source Contributor
Walter Litwinczyk Open Source Contributor

If you are interested in working on Hazel, or you'd like a mentor to help you learn the necessary type theory, or you just want to join the discussion on our Slack, get in touch with Cyrus!

News

Sep 2019
Cyrus will start as an Assistant Professor at the University of Michigan in the Fall. David Moon will join him as a PhD student. Michael D. Adams will also be joining as a Research Scientist.
Jan 2019
May 2018
NSF selected the research that Cyrus, Ravi and Matthew proposed for three years of funding.
May 2017
SNAPL 2017 published our vision paper.
Jan 2017
POPL 2017 published our Hazelnut paper.

Recent & Upcoming Talks

Aug 18, 2019
David presented progress on the Hazel editing experience [extended abstract] and Cyrus presented livelits in Hazel [slides, extended abstract] at the TyDe workshop at ICFP 2019 in Berlin.
Jan 17, 2019
Cyrus presented our Hazelnut Live paper at POPL 2019 in Lisbon.
Nov 6, 2018
Cyrus presented Hazel at the LIVE workshop at SPLASH in Boston.
Oct 31, 2018
Cyrus gave a POP seminar at CMU.
Oct 2018
Cyrus presented Hazel at the Midwest PL Summit in Madison.
Sep 2018
Cyrus presented Hazel at Strange Loop in St. Louis.

(h/t Vincent Zeng)