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.

• Toward Semantic Foundations for Program Editors (SNAPL, May 2017 [.bib])
• Slides

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.

• Hazelnut: A Bidirectionally Typed Structure Editor Calculus (POPL, Jan. 2017 [.bib])
• Slides

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.

• Play with HZ online
• Source code on GitHub

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.

• Live Functional Programming with Typed Holes (draft paper, July 2018)

Mechanization

We are mechanizing the metatheory of Hazelnut Live using the Agda proof assistant.

Implementation

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.