Hazel is a live functional programming environment featuring typed holes.

Project Summary

When programming, we spend a substantial amount of our time working with programs that are not yet complete — 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 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 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.

This hole-oriented approach is broadly relevant, but we are incorporating our results into Hazel, a web-based programming environment for an Elm-like functional language that is being designed from the ground 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 solves the gap problem: language services never flicker out or go stale, nor do they need to resort to heuristics. Hazel therefore 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 called Hazelnut that defines 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.

The following research paper, published at POPL 2017, 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 (to appear, POPL 2019)

Next, we wondered: how can we run programs with holes? One approach is to simply stop as soon as we encounter a hole at run-time, but this isn't very informative. Our next paper develops a more informative approach: we continue evaluation as far as possible, producing a result containing hole closures. Hole closures allow Hazel to provide detailed live feedback to the programmer, and to resume evaluation from where it left off 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. The resulting core calculus is called Hazelnut Live.

Live Functional Programming with Typed Holes (draft, July 2018)
C. Omar, I. Voysey, R. Chugh and M. Hammer
POPL 2019 (to appear, Jan 2019)

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.

Live and Direct Functional Programming with Palette Expressions

We are thinking about how to integrate GUIs directly into Hazel expressions, and how to integrate Hazel expressions directly into 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).

Edit-Time Macros

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 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, or want a mentor to help you learn the necessary type theory, get in touch!

News

Oct 2018
May 2018
NSF [1, 2] selected the proposal that Cyrus, Ravi and Matthew wrote for three years of funding!
May 2017
SNAPL 2017 accepted our vision paper.
Jan 2017

Talk Schedule

Jan 2019 (upcoming)
Cyrus will present our Hazelnut Live paper at POPL 2019 in Lisbon.
Nov 2018 (upcoming)
Cyrus will give a talk on live and direct programming in Hazel at the LIVE workshop at SPLASH in Boston.
Oct 2018
Cyrus gave a talk on Hazel at the Midwest PL Summit in Madison.
Sep 2018
Cyrus gave a talk on Hazel at Strange Loop in St. Louis.

(h/t Vincent Zeng)