Hazel is a live functional programming environment featuring typed holes.

Quick Summary

Hazel is a live functional programming environment that is able to typecheck, manipulate, and even run incomplete programs, i.e. programs with holes. There are no meaningless editor states.

Motivation

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 we are left without live feedback about the behavior of even complete portions of the program. Moreover, 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, and code navigation) 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.

The following paper describes our research vision in more detail.

Hazel

We are first implementing these ideas into Hazel, a web-based programming environment for an Elm/ML-like functional programming language designed around typed-hole-driven development.

Uniquely, every incomplete program that you can construct using Hazel's language of 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 (and programming education).

News

Oct 2021
LIVE 2021 accepted our essay on Restructuring Structure Editing (link pending revisions). David will be presenting it (in person) at SPLASH in October.
June 2021
Aug 2020
ICFP 2020 published Program Sketching with Live Bidirectional Evaluation describing Smyth, a foundational component of the Hazel Assistant.
Jan 2019
POPL 2019 published Live Functional Programming with Typed Holes which develops a rich operational semantics for expressions with typed holes.
Sep 2018
May 2018
NSF selected the research that Cyrus, Ravi and Matthew proposed for funding.
May 2017
SNAPL 2017 published Toward Semantic Foundations for Program Editors describing our broad research vision.
Jan 2017

Hazelnut (POPL 2017)

To start, we developed a core calculus, Hazelnut, that defines (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.

Hazel Assistant (ICFP 2020)

We are developing an intelligent programming assistant that synthesizes code satisfying specifications provided by human programmers in the form of types, tests, and sketches, and further guided by a learned understanding of idiomatic code.

To start with, we developed the Smyth synthesizer, which adds support for sketching to Myth, a type-and-example directed synthesizer, by combining the live programming mechanisms from Hazelnut Live with a novel form of unevaluation, which propagates constraints to where they are relevant. Our approach solves a long-standing problem: we no longer need a trace-complete set of examples.

Program Sketching with Live Bidirectional Evaluation
J. Lubin, N. Collins, C. Omar, and R. Chugh
ICFP 2020 [.bib, tutorial]

We are now working to scale up and integrate Smyth into the Hazel user interface, which requires considering the problems of interactivity, incrementality, and readability. Check out our first demo!

Livelits: Filling Typed Holes with Live GUIs (PLDI 2021)

Symoblic representations are powerful, but some types of expessions are more naturally represented and manipulated non-symbolically. 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.

Filling Typed Holes with Live GUIs
C. Omar, D. Moon, A. Blinn, I. Voysey, N. Collins, and R. Chugh
PLDI 2021 [.bib, demo]

We have mechanized the metatheory of livelits, which operate as live graphical macros, 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 restructuring patterns. We are doing user studies.

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

Authoring with Livelits

We are working on integrating document authoring with programming via livelits: document editing is programming, too.

Hazel Tutor: Guiding Novices Through Type-Driven Development Strategies

We are planning to use Hazel to teach introductory functional programming. We are developing a number of mechanisms to support this, including a type-driven cursor inspector and strategy guide.

Other Applications

As Hazel evolves, 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

Hazel is an open source research project led by the Future of Programming Lab (FP Lab) at the University of Michigan.

If you have questions or are interested in contributing to Hazel, get in touch with the team lead, Cyrus Omar.

(h/t Vincent Zeng)