Hazel is a live functional programming environment organized around 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 papers 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 and Publications

Jan 2025
POPL 2025 conditionally accepted Grove: A Bidirectionally Typed Structure Editor Calculus describing our work on reworking the foundations of collaborative editing around commutative edit actions.
Oct 2024
OOPSLA 2024 published Statically Contextualizing Large Language Models with Typed Holes describing our work on combining language servers with large language models to dramatically improve AI code completion performance.
Oct 2024
HATRA 2024 accepted Learner-Centered Design Criteria for Classroom Proof Assistants describing our goals for using Hazel for teaching and learning proof.
Oct 2024
Sep 2024
NSF awarded Cyrus and Jean-Baptiste Jeannin a grant on Customizing a Classroom Proof Assistant for Mathematical Computing and Engineering Courses. This will focus on turning Hazel into a classroom proof assistant.
Jan 2024
POPL 2024 published Total Type Error Localization and Recovery with Holes describing a principled approach to localizing errors in ill-typed programs. This paper was awarded a Distinguished Paper Award!
Jan 2024
PROPL 2024 accepted Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine describing our vision for tooling for the future of large-scale computational climate science.
Jan 2024
TFP 2024 accepted Polymorphism with Typed Holes, a paper describing our approach to explicitly implicit polymorphism in Hazel.
Oct 2023
OOPSLA 2023 published Live Pattern Matching with Typed Holes describing our work on reasoning about programs with pattern holes. This paper was awarded a Distinguished Paper Award!
Oct 2023
VL/HCC 2023 published Gradual Structure Editing with Obligations describing our work on natural keyboard-driven structure editing.
Jan 2023
Dec 2022
Onward! 2022 published Contextualized Programming Language Documentation describing the ExplainThis service in Hazel.
Sep 2022
VL/HCC 2022 published An Integrative Human-Centered Architecture for Interactive Programming Assistants describing our ongoing work on the Hazel Assistant.
Sep 2022
TyDe 2022 published tylr: A Tiny Tile-Based Structure Editor describing our ongoing work on natural keyboard-driven structure editing interfaces.
June 2021
Oct 2020
HATRA 2020 published Hazel Tutor: Guiding Novices Through Type-Driven Development Strategies describing our work on teaching type-driven development with Hazel.
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
POPL 2017 published Hazelnut: A Bidirectionally Typed Structure Editor Calculus, which defines a calculus of edit actions that insert typed holes automatically.

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)