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.

We are incorporating our research results into Hazel, a web-based programming environment for an Elm-like functional language. Hazel is designed from the ground up to support typed hole-driven development.

The following paper describes this research vision in more detail.

Research Results

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.

Mechanization

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

Implementation

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.

Hazelnut Live (Draft Paper)

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.

Mechanization

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

Implementation

We have implemented the features described in the paper in Hazel.

LIVE 2017 Presentation

Cyrus presented some of this work at the LIVE 2017 workshop.

OBT 2017 Presentation

Ian presented a much earlier take on this work at the Off the Beaten Track (OBT) workshop at POPL 2017.

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 conflict-free 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.

Applications

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.

Contributors

If you're interested in working on Hazel, in any capacity, get in touch!

News

Apr 2018
Jan 2018
Cursor movement in Hazel 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)