# Live Functional Programming with Typed Holes

arXiv: https://arxiv.org/abs/1805.00155 · HTML: https://mlsanity.com/paper/1805.00155/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 May 2018.

## Built on by (most cited first, 7 of 7)

- [Constrained Decoding of Diffusion LLMs with Context-Free Grammars](https://mlsanity.com/paper/2508.10111/) (2025)
- [Statically Contextualizing Large Language Models with Typed Holes](https://mlsanity.com/paper/2409.00921/) (2024)
- [LeanTutor: Towards a Verified AI Mathematical Proof Tutor](https://mlsanity.com/paper/2506.08321/) (2025)
- [Report of the Workshop on Program Synthesis for Scientific Computing](https://mlsanity.com/paper/2102.01687/) (2021)
- [LeanTutor: Towards a Verified AI Mathematical Proof Tutor](https://mlsanity.com/paper/2601.17473/) (2026)
- [Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code](https://mlsanity.com/paper/2607.13921/) (2026)
- [A-JIT: Agentic Just-In-Time Software Construction](https://mlsanity.com/paper/2609.10248/) (2026)

## Abstract (arXiv)

This paper develops a dynamic semantics for incomplete functional programs, starting from the static semantics developed in recent work on Hazelnut. We model incomplete functional programs as expressions with holes, with empty holes standing for missing expressions or types, and non-empty holes operating as membranes around static and dynamic type inconsistencies. Rather than aborting when evaluation encounters any of these holes as in some existing systems, evaluation proceeds around holes, tracking the closure around each hole instance as it flows through the remainder of the program. Editor services can use the information in these hole closures to help the programmer develop and confirm their mental model of the behavior of the complete portions of the program as they decide how to fill the remaining holes. Hole closures also enable a fill-and-resume operation that avoids the need to restart evaluation after edits that amount to hole filling. Formally, the semantics borrows machinery from both gradual type theory (which supplies the basis for handling unfilled type holes) and contextual modal type theory (which supplies a logical basis for hole closures), combining these and developing additional machinery necessary to continue evaluation past holes while maintaining type safety. We have mechanized the metatheory of the core calculus, called Hazelnut Live, using the Agda proof assistant. We have also implemented these ideas into the Hazel programming environment. The implementation inserts holes automatically, following the Hazelnut edit action calculus, to guarantee that every editor state has some (possibly incomplete) type. Taken together with this paper's type safety property, the result is a proof-of-concept live programming environment where rich dynamic feedback is truly available without gaps, i.e. for every reachable editor state.