Hazel is a live functional programming environment featuring typed holes.

Project Summary

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.

Research Paper

The following research paper, published at POPL 2017, details Hazelnut.


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


HZ is a very simple reference implementation of Hazelnut, written in OCaml and compiled to JavaScript using js_of_ocaml. Hazel is derived from HZ.

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.

Research Paper

The following research paper details how we achieve this goal by borrowing machinery from both gradual type theory and contextual modal type theory.


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.

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.

Collaborative Editing

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.

Edit-Time Macros

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.


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!


Nov 2018 (upcoming)
Cyrus will be giving a talk on live and direct programming in Hazel at the LIVE workshop during SPLASH in Boston.
Sep 2018 (upcoming)
Cyrus will be giving a talk on Hazel at Strange Loop in St. Louis.
July 2018
An updated draft paper on live programming is available.
May 2018
NSF will fund the research that Cyrus, Ravi and Matthew proposed! [1, 2]
Jan 2018
Operators now re-associate dynamically during editing and cursor movement is now textual!
Oct 2017
Cyrus gave a talk about live programming in Hazel at the LIVE workshop at SPLASH.
Sep 2017
Cyrus moved from CMU to UChicago to start a postdoc with Ravi.
May 2017
Cyrus and Matthew attended SNAPL and talked about the vision for the Hazel project.
Jan 2017

(h/t Vincent Zeng)