Strange Loop

September 26-28 2018

/

Peabody Opera House

/

St. Louis, MO

Hazel: A Live Functional Programming Environment with Typed Holes

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 various locations in the program. Conventional programming language definitions assign no formal meaning to these incomplete programs, so development tools can at best resort to ad hoc heuristics to provide various useful language services without interruption, including code completion, type inspection, code navigation, and live debugging.

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 conflicted.

We are incorporating this approach into Hazel (hazel.org), a web-based live programming environment for an Elm-like functional language designed from the ground up to support typed hole-driven development. Uniquely, Hazel inserts holes automatically to ensure that every editor state has both static meaning (so we can provide type-based services, like type inspection, without interruption) and dynamic meaning (so we can provide run-time services, like Hazel's novel live debugger, without interruption). We are currently using Hazel to develop interactive course material that introduces functional programming.

Cyrus Omar

University of Chicago

Cyrus Omar got his PhD in programming languages from Carnegie Mellon University in May 2017. He is now a post-doctoral researcher at The University of Chicago, where he leads the Hazel collaboration. In a past life, Cyrus was a computational neurobiologist. That experience motivated him to switch fields and focus on designing a better front-end programming experience for scientists, engineers, artists and other skilled end-users, rooted in the principles in type theory and interaction design.