Hazelnut structure editor calculus - bidirectionally typed lambda calculus with holes and cursor, edit actions preserving static meaning, zipper structures
Scope: Hazelnut calculus (POPL 2017), structure editing, edit actions, zipper structures, Grove extensions Lines: ~420 Last Updated: 2025-10-25
Activate this skill when:
Key insight: Edit AST directly, not text
from dataclasses import dataclass
from typing import Union, Optional
# Traditional text editing
text_edit_example = """
User types: "if true th"
State: Syntactically invalid!
Parser: Error, incomplete conditional
"""
# Structure editing (Hazel approach)
@dataclass
class EmptyHole:
"""⦇ ⦈ - empty hole, no expression yet"""
def __repr__(self):
return "⦇⦈"
@dataclass
class NonEmptyHole:
"""⦇e⦈ - non-empty hole, expression with wrong type"""
expr: 'Expr'
def __repr__(self):
return f"⦇{self.expr}⦈"
# Structure edit sequence:
"""
1. Start: ⦇⦈ (empty hole)
2. construct if: if ⦇⦈ then ⦇⦈ else ⦇⦈
3. Fill condition: if true then ⦇⦈ else ⦇⦈
4. Fill branches...
At EVERY step: syntactically valid, typeable!
"""
print("Structure editing: always syntactically well-formed")Core language: Simply-typed lambda calculus + holes + cursor
# Hazelnut expressions (UExp)
@dataclass
class Num:
"""Number literal"""
value: int
@dataclass
class Var:
"""Variable"""
name: str
@dataclass
class Lam:
"""Lambda: λx.e"""
param: str
body: 'UExp'
@dataclass
class Ap:
"""Application: e₁ e₂"""
func: 'UExp'
arg: 'UExp'
@dataclass
class Plus:
"""Addition: e₁ + e₂"""
left: 'UExp'
right: 'UExp'
@dataclass
class EHole:
"""Empty expression hole: ⦇⦈"""
pass
@dataclass
class NEHole:
"""Non-empty hole: ⦇e⦈"""
expr: 'UExp'
UExp = Union[Num, Var, Lam, Ap, Plus, EHole, NEHole]
print("Hazelnut: λ-calculus + holes")Zipper: Navigate AST with cursor
@dataclass
class ZExp:
"""Expression with cursor (zipper)"""
focus: UExp # Current expression under cursor
context: 'ZContext' # Surrounding context
# Zipper contexts (one-hole contexts)
@dataclass
class ZTop:
"""Top level: no surrounding context"""
def __repr__(self):
return "□"
@dataclass
class ZLam:
"""λx.□ - cursor inside lambda body"""
param: str
parent_context: 'ZContext'
@dataclass
class ZApL:
"""□ e - cursor in function position"""
arg: UExp
parent_context: 'ZContext'
@dataclass
class ZApR:
"""e □ - cursor in argument position"""
func: UExp
parent_context: 'ZContext'
@dataclass
class ZPlusL:
"""□ + e - cursor in left operand"""
right: UExp
parent_context: 'ZContext'
@dataclass
class ZPlusR:
"""e + □ - cursor in right operand"""
left: UExp
parent_context: 'ZContext'
@dataclass
class ZNEHole:
"""⦇□⦈ - cursor inside non-empty hole"""
parent_context: 'ZContext'
ZContext = Union[ZTop, ZLam, ZApL, ZApR, ZPlusL, ZPlusR, ZNEHole]
# Example: Navigate through expression
def example_zipper():
"""
Expression: (λx. x + 1) 5
Cursor positions:
1. ▸(λx. x + 1) 5 (function)
2. (λx. ▸x + 1) 5 (inside lambda, at variable)
3. (λx. x ▸+ 1) 5 (at operator)
4. (λx. x + 1) ▸5 (argument)
"""
pass
print("Zipper: cursor position + surrounding context")Core edit actions: Construct, delete, move
from enum import Enum
class Direction(Enum):
PARENT = "parent"
CHILD_1 = "child1"
CHILD_2 = "child2"
# Movement actions
def move(zexp: ZExp, dir: Direction) -> Optional[ZExp]:
"""
Move cursor in direction
move parent: Go up to parent
move child(n): Go down to nth child
"""
match dir:
case Direction.PARENT:
# Move up: plug hole, move context
return move_parent(zexp)
case Direction.CHILD_1:
# Move to first child (if exists)
return move_child(zexp, 1)
case Direction.CHILD_2:
return move_child(zexp, 2)
# Construction actions
def construct_lam(zexp: ZExp, param: str) -> ZExp:
"""
construct lam x
Wrap current expression in λx.□
If current is ⦇⦈, produces λx.⦇⦈
"""
current = zexp.focus
new_body = EHole() if isinstance(current, EHole) else current
new_lam = Lam(param, new_body)
return ZExp(new_lam, zexp.context)
def construct_ap(zexp: ZExp) -> ZExp:
"""
construct ap
Current becomes function, add hole for argument
e → e ⦇⦈
"""
func = zexp.focus
new_ap = Ap(func, EHole())
return ZExp(new_ap, zexp.context)
def construct_plus_left(zexp: ZExp) -> ZExp:
"""
construct + L
Current becomes right operand, add hole on left
e → ⦇⦈ + e
"""
right = zexp.focus
new_plus = Plus(EHole(), right)
# Move cursor to left hole
return ZExp(EHole(), ZPlusL(right, zexp.context))
# Deletion action
def delete(zexp: ZExp) -> ZExp:
"""
del
Replace current expression with empty hole
e → ⦇⦈
"""
return ZExp(EHole(), zexp.context)
print("Edit actions: move, construct, delete")Key innovation: Automatically wrap inconsistent terms in holes
# Types (Hazelnut)
@dataclass
class TNum:
def __repr__(self):
return "Num"
@dataclass
class TArrow:
param: 'Type'
result: 'Type'
def __repr__(self):
return f"({self.param} → {self.result})"
@dataclass
class THole:
"""Type hole: unknown type"""
def __repr__(self):
return "?"
Type = Union[TNum, TArrow, THole]
# Type consistency (~)
def consistent(t1: Type, t2: Type) -> bool:
"""
Type consistency:
- ? ~ τ for all τ
- Num ~ Num
- (τ₁ → τ₂) ~ (σ₁ → σ₂) if τ₁ ~ σ₁ and τ₂ ~ σ₂
"""
if isinstance(t1, THole) or isinstance(t2, THole):
return True
if isinstance(t1, TNum) and isinstance(t2, TNum):
return True
if isinstance(t1, TArrow) and isinstance(t2, TArrow):
return (consistent(t1.param, t2.param) and
consistent(t1.result, t2.result))
return False
# Inconsistency handling
def construct_with_type_check(zexp: ZExp, expected: Type):
"""
When constructing, check type consistency
If inconsistent: wrap in non-empty hole!
Example:
Expected: Num
Construct: λx.x (type: ? → ?)
Result: ⦇λx.x⦈ (non-empty hole, preserves typing)
"""
expr = zexp.focus
expr_type = synthesize_type(expr)
if not consistent(expr_type, expected):
# Wrap in non-empty hole
return NEHole(expr)
else:
return expr
print("Inconsistent expressions automatically wrapped in holes")Action semantics: Actions preserve types
def action_type(action: str, zexp: ZExp, ctx_type: Type) -> Type:
"""
Type-aware action semantics
Every action produces typeable result!
Example: construct lam x
Before: ⦇⦈ : τ
After: λx.⦇⦈ : ? → τ
(Hole becomes lambda body)
"""
pass
# Synthesis (⇒) vs Checking (⇐)
def synth(expr: UExp, gamma: dict) -> Type:
"""
Synthesis: Γ ⊢ e ⇒ τ
Figure out type from expression
"""
match expr:
case Num(n):
return TNum()
case Var(x):
return gamma.get(x, THole())
case EHole():
return THole() # Holes synthesize hole type
case NEHole(e):
return THole() # Non-empty holes too
case Ap(f, a):
# Synthesize function, check argument
f_type = synth(f, gamma)
if isinstance(f_type, TArrow):
check(a, gamma, f_type.param)
return f_type.result
else:
return THole()
# ... other cases
def check(expr: UExp, gamma: dict, expected: Type):
"""
Checking: Γ ⊢ e ⇐ τ
Verify expression has expected type
"""
match expr:
case Lam(x, body):
if isinstance(expected, TArrow):
new_gamma = gamma | {x: expected.param}
check(body, new_gamma, expected.result)
else:
# Can't check lambda against non-arrow
raise TypeError("Expected arrow type for lambda")
case _:
# Fallback: synthesize and check consistency
synth_type = synth(expr, gamma)
if not consistent(synth_type, expected):
raise TypeError(f"Inconsistent: {synth_type} !~ {expected}")
print("Bidirectional typing ensures actions preserve types")Formal action rules: From POPL 2017 paper
class ActionSemantics:
"""
Hazelnut action semantics
Judgment: (e, γ, α) → e'
Given expression e, context γ, action α
Produces new expression e'
"""
@staticmethod
def construct_num(zexp: ZExp, n: int) -> ZExp:
"""
construct num n
Rule:
e is ⦇⦈
──────────────
e → n
Replaces empty hole with number
"""
if isinstance(zexp.focus, EHole):
return ZExp(Num(n), zexp.context)
else:
raise ValueError("construct num requires empty hole")
@staticmethod
def construct_var(zexp: ZExp, x: str) -> ZExp:
"""
construct var x
Replaces empty hole with variable
"""
if isinstance(zexp.focus, EHole):
return ZExp(Var(x), zexp.context)
else:
raise ValueError("construct var requires empty hole")
@staticmethod
def construct_lam(zexp: ZExp, x: str) -> ZExp:
"""
construct lam x
Rule:
──────────────
e → λx.e
Wraps current expression in lambda
"""
body = zexp.focus if not isinstance(zexp.focus, EHole) else EHole()
new_lam = Lam(x, body)
# Move cursor to body
return ZExp(body, ZLam(x, zexp.context))
@staticmethod
def finish(zexp: ZExp) -> ZExp:
"""
finish
Remove non-empty hole wrapper if types match
Rule:
Γ ⊢ e ⇒ τ
Γ ⊢ ⦇e⦈ ⇐ τ
──────────────
⦇e⦈ → e
Only works if types are consistent!
"""
if isinstance(zexp.focus, NEHole):
# Check if inner expression has consistent type
# If yes, unwrap; if no, keep hole
return ZExp(zexp.focus.expr, zexp.context)
else:
return zexp
print("Action semantics: formal rules from Hazelnut paper")Collaborative editing: Commutative edit actions
@dataclass
class GroveAction:
"""
Grove: Commutative edit actions for collaboration
Key idea: Actions commute so concurrent edits merge automatically
"""
action_id: str
timestamp: int
user: str
action_type: str
parameters: dict
def commute(a1: GroveAction, a2: GroveAction) -> bool:
"""
Check if actions commute: a1; a2 ≡ a2; a1
Examples:
- Edits at different locations: commute
- Edits at same location: conflict (handled specially)
- Dependent edits: don't commute (serialize)
"""
# If actions touch disjoint parts of tree
if disjoint_paths(a1, a2):
return True
# If one creates, other references: order matters
if creates_dependency(a1, a2):
return False
return True
# Operational transformation for concurrent editing
def merge_concurrent_edits(actions: list[GroveAction]) -> UExp:
"""
Merge concurrent edits using commutative properties
Grove ensures most edits commute, reducing conflicts
"""
pass
print("Grove: Commutative actions for collaborative editing")def progressive_refinement_example():
"""
Build program by refining holes
1. Start: ⦇⦈ : Num → Num
2. construct lam x: λx.⦇⦈ : Num → Num
3. move child1 (to body)
4. construct + L: ⦇⦈ + ⦇⦈ : Num
5. construct num 1 (left): 1 + ⦇⦈
6. construct var x (right): 1 + x
Result: λx. 1 + x
"""
print("Progressive refinement: holes → complete program")def type_directed_construction(expected_type: Type):
"""
Use expected type to guide construction
Expected: Num → Num
→ Suggest: construct lam (makes lambda)
Expected: Num
→ Suggest: construct num, construct +, construct var (if Num in context)
"""
suggestions = []
if isinstance(expected_type, TArrow):
suggestions.append("construct lam x")
elif isinstance(expected_type, TNum):
suggestions.extend(["construct num n", "construct +"])
return suggestionsdef error_recovery_pattern(expr: UExp, expected: Type):
"""
When type error: wrap in non-empty hole
User constructs: λx.x (type: ? → ?)
Expected: Num
Instead of error: ⦇λx.x⦈ : Num
→ Program still types!
→ User can fix later
"""
expr_type = synth(expr, {})
if not consistent(expr_type, expected):
# Don't throw error - wrap in hole!
return NEHole(expr)
else:
return expr
print("Non-empty holes: graceful error recovery")| Syntax | Meaning | |--------|---------| | ⦇⦈ | Empty hole (EHole) | | ⦇e⦈ | Non-empty hole (NEHole) | | λx.e | Lambda abstraction | | e₁ e₂ | Application | | e₁ + e₂ | Addition |
| Action | Effect | |--------|--------| | move parent | Move cursor up | | move child(n) | Move cursor to nth child | | construct lam x | Wrap in λx.□ | | construct ap | Add application: □ ⦇⦈ | | construct num n | Replace ⦇⦈ with n | | del | Replace with ⦇⦈ | | finish | Remove hole wrapper (if types match) |
Syntactic Well-Formedness:
Every edit action produces syntactically valid expression
Static Meaning:
Every expression has a type (possibly with ?)
Type Preservation:
Actions preserve typability❌ Allowing syntactically invalid states: Defeats purpose of structure editing ✅ Actions always produce valid AST
❌ Throwing errors on type mismatch: Breaks flow ✅ Wrap inconsistent terms in non-empty holes
❌ Ignoring cursor position: Can't implement navigation ✅ Use zipper structure to track cursor
❌ Requiring complete programs: Defeats holes ✅ Allow incomplete programs, use ⦇⦈ liberally
typed-holes-foundations.md - Basic typed holes conceptstype-systems.md - Type checking and consistencylambda-calculus.md - Underlying calculusstructure-editors.md - General structure editor designlive-programming-holes.md - Hazel environment implementationtyped-holes-semantics.md - Advanced semanticsLast Updated: 2025-10-25 Format Version: 1.0 (Atomic)