Quick SummaryHazel 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.
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.
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
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.
Linearly Editing Typed Trees
We are working on a keyboard-driven editing experience that builds on your intuitions from text editing and that supports complex code restructuring patterns. We are doing user studies.
Collaborative Structure 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).
Authoring with Livelits
We are working on integrating document authoring with programming via livelits: document editing is programming, too.
Hazel Tutor: Guiding Novices Through Type-Driven Development Strategies
We are planning to use Hazel to teach introductory functional programming. We are developing a number of mechanisms to support this, including a type-driven cursor inspector and strategy guide.
As Hazel evolves, we plan to use Hazel to support data analysis (think a next-generation Jupyter). One day, we hope that Hazel will be the foundation for a new kind of computational wiki.