Live programming with typed holes - Hazel environment, continuous feedback, live evaluation with indeterminate results, incremental bidirectional typing (OOPSLA 2025), collaborative editing (Grove)
Scope: Hazel environment, live evaluation, incremental typing (OOPSLA 2025), collaborative editing (Grove POPL 2025) Lines: ~420 Last Updated: 2025-10-25
Activate this skill when:
Live programming: Immediate, continuous feedback while editing
from dataclasses import dataclass
from typing import Union, Optional, List
class LiveEnvironment:
"""
Live programming environment characteristics:
1. Edit freely: All intermediate states valid
2. See immediately: Continuous evaluation
3. Inspect anywhere: Click to see types, values
4. No compile step: No edit-compile-run cycle
"""
def __init__(self):
self.program = EmptyHole() # Start with hole
self.evaluation_result = None
self.type_info = {}
def on_edit(self, new_program: 'Expr'):
"""
On every edit:
1. Re-type check (incremental)
2. Re-evaluate (if possible)
3. Update display
"""
# Incremental type checking
self.type_info = self.incremental_typecheck(new_program)
# Live evaluation
try:
self.evaluation_result = self.evaluate(new_program)
except:
self.evaluation_result = IndeterminateResult()
# Update UI immediately
self.update_display()
def update_display(self):
"""
Show:
- Syntax highlighting
- Type annotations (hover)
- Evaluation result
- Hole goals
"""
pass
print("Live programming: edit → type → eval → display (continuously)")Hazel: Web-based live functional programming environment
@dataclass
class HazelState:
"""
Hazel system state
Core components:
- Editor: Structure editor (Hazelnut)
- Type checker: Bidirectional with holes
- Evaluator: Small-step with indeterminate results
- UI: React-based web interface
"""
# Current program (ZExp with cursor)
program: 'ZExp'
# Type information
type_map: dict # Expression → Type
# Evaluation state
eval_state: 'EvalState'
# UI state
cursor_position: tuple
selected_hole: Optional[str]
@dataclass
class EvalState:
"""
Evaluation state for live environment
Multiple evaluation modes:
- Step-by-step: Single reduction steps
- To value: Reduce to normal form
- Lazy: Evaluate on demand
"""
current_expr: 'Expr'
step_count: int
is_indeterminate: bool # Contains holes
# Hazel workflow
def hazel_workflow():
"""
User interaction in Hazel:
1. Edit structure (keyboard/mouse)
→ Hazelnut edit actions
2. Type check continuously
→ Bidirectional type synthesis
3. Evaluate on demand
→ Click "evaluate" or automatic
4. Inspect results
→ Hover for types
→ Click holes to see goals
→ Step through evaluation
Always valid, always typeable, always inspectable!
"""
pass
print("Hazel: Fully integrated live environment")Key insight: Can evaluate programs with holes to indeterminate results
@dataclass
class DeterminateValue:
"""Concrete value"""
value: any
@dataclass
class IndeterminateValue:
"""Value containing holes - we don't know what it is yet"""
hole_id: str
expected_type: 'Type'
context: dict
Result = Union[DeterminateValue, IndeterminateValue]
class LiveEvaluator:
"""Evaluate programs with holes"""
def evaluate_live(self, expr: 'Expr') -> Result:
"""
Evaluate with holes
Examples:
- 2 + 3 → 5 (determinate)
- 2 + ?h → ⊥h (indeterminate)
- if true then 5 else ?h → 5 (determinate! Hole not evaluated)
- if ?h then 1 else 2 → ⊥h (indeterminate, need hole value)
"""
match expr:
case Hole(name, typ, ctx):
# Hole evaluates to indeterminate
return IndeterminateValue(name, typ, ctx)
case Num(n):
return DeterminateValue(n)
case Plus(e1, e2):
v1 = self.evaluate_live(e1)
v2 = self.evaluate_live(e2)
# If either indeterminate, result is indeterminate
if isinstance(v1, IndeterminateValue):
return v1
if isinstance(v2, IndeterminateValue):
return v2
# Both determinate: compute
return DeterminateValue(v1.value + v2.value)
case If(cond, then_branch, else_branch):
cond_val = self.evaluate_live(cond)
if isinstance(cond_val, IndeterminateValue):
# Can't decide which branch
return cond_val
# Determinate condition: choose branch
if cond_val.value:
return self.evaluate_live(then_branch)
else:
return self.evaluate_live(else_branch)
def display_result(self, result: Result) -> str:
"""
Display evaluation result to user
Determinate: Show value
Indeterminate: Show which hole blocked evaluation
"""
match result:
case DeterminateValue(v):
return f"Result: {v}"
case IndeterminateValue(hole_id, typ, _):
return f"⊥{hole_id} : {typ} (indeterminate - depends on hole)"
print("Live evaluation: Results may be indeterminate but still meaningful")Incremental typing: Re-type only what changed (Distinguished Paper!)
class IncrementalTypeChecker:
"""
Incremental bidirectional type checking
Based on OOPSLA 2025 work:
"Incremental Bidirectional Typing via Order Maintenance"
Key idea: Borrow techniques from incremental browser layout
"""
def __init__(self):
self.type_cache = {} # Expression → Type
self.dependency_graph = {} # What depends on what
self.dirty_set = set() # What needs re-checking
def edit(self, old_expr: 'Expr', new_expr: 'Expr', path: List[int]):
"""
Handle edit at path
Instead of re-typing entire program:
1. Mark changed node as dirty
2. Propagate dirtiness up dependencies
3. Re-type only dirty nodes
"""
# Mark affected nodes
self.mark_dirty(path)
# Incremental re-typing
return self.retype_dirty()
def mark_dirty(self, path: List[int]):
"""
Mark node and dependents as dirty
If e changed at path p:
- Mark e as dirty
- Mark parent of e as dirty (dependent)
- Propagate to all ancestors
"""
for node in self.ancestors(path):
self.dirty_set.add(node)
# Mark anything that depends on this node
for dependent in self.dependency_graph.get(node, []):
self.dirty_set.add(dependent)
def retype_dirty(self):
"""
Re-type only dirty nodes
Process in dependency order:
1. Leaves first (no dependencies)
2. Then parents (depend on leaves)
3. Bottom-up to root
"""
# Topological sort of dirty nodes
ordered = self.topo_sort(self.dirty_set)
for node in ordered:
# Re-type this node
new_type = self.typecheck_node(node)
self.type_cache[node] = new_type
self.dirty_set.clear()
def typecheck_node(self, node: 'Expr') -> 'Type':
"""
Type single node
Can use cached types for clean children!
Only re-type dirty subtrees
"""
match node:
case App(f, arg):
# Lookup types (cached if clean, recomputed if dirty)
f_type = self.get_type(f)
arg_type = self.get_type(arg)
# Type application
if isinstance(f_type, TArrow):
check_consistent(arg_type, f_type.param)
return f_type.result
else:
return THole()
# ... other cases
def get_type(self, expr: 'Expr') -> 'Type':
"""
Get type: from cache if clean, recompute if dirty
"""
if expr in self.dirty_set:
return self.typecheck_node(expr)
else:
return self.type_cache.get(expr, THole())
print("Incremental typing: Only re-type what changed")Live pattern editing: See match coverage in real-time
class LivePatternChecker:
"""
Live pattern match analysis
Shows:
- Which patterns are redundant
- Which cases are missing
- Example values that reach each branch
"""
def analyze_match(self, match_expr: Match) -> 'MatchAnalysis':
"""
Analyze pattern match live
Example:
match x : Bool with
| true → 1
| _ → 2
Analysis:
- Pattern 1 (true): Covers {true}
- Pattern 2 (_): Covers {false} (not redundant!)
- Complete: Yes
"""
scrutinee_type = self.get_type(match_expr.scrutinee)
all_values = enumerate_values(scrutinee_type)
coverage = []
for i, (pattern, _) in enumerate(match_expr.branches):
covered = match_values(pattern, all_values)
coverage.append((i, covered))
# Remove covered values
all_values = all_values - covered
return MatchAnalysis(
coverage=coverage,
uncovered=all_values,
redundant=self.find_redundant(coverage)
)
def display_coverage(self, analysis: 'MatchAnalysis'):
"""
Display coverage visually in IDE
- Green: Pattern covers new cases
- Yellow: Pattern is redundant
- Red: Missing cases (uncovered)
"""
pass
print("Live pattern analysis: See coverage and completeness instantly")Grove: Commutative edit actions for real-time collaboration
class GroveCollaboration:
"""
Grove: Bidirectionally Typed Structure Editor Calculus (POPL 2025)
Key innovation: Commutative edit actions
Traditional conflict:
User A: Edit at position 10
User B: Insert at position 5
→ Position 10 is now 15! Conflict!
Grove approach:
Edits reference paths in tree, not positions
Most edits naturally commute
"""
def __init__(self):
self.local_operations = []
self.remote_operations = []
self.program_state = EmptyHole()
def apply_edit(self, edit: 'GroveEdit', source: str):
"""
Apply edit (local or remote)
Grove guarantees:
1. Edits at different paths commute
2. Edits at same path have defined merge
3. Type safety preserved in all merges
"""
if source == "local":
self.local_operations.append(edit)
else:
self.remote_operations.append(edit)
# Apply edit
self.program_state = self.transform_and_apply(edit, self.program_state)
def transform_and_apply(self, edit: 'GroveEdit', state: 'Expr') -> 'Expr':
"""
Operational transformation for Grove
If concurrent edits:
- Transform edit to account for other edits
- Apply transformed edit
- Result: Convergent state (same for all users)
"""
# Transform edit based on concurrent operations
transformed = self.transform(edit, self.get_concurrent_edits(edit))
# Apply transformed edit
return self.apply(transformed, state)
def transform(self, edit: 'GroveEdit', concurrent: List['GroveEdit']) -> 'GroveEdit':
"""
Transform edit to commute with concurrent edits
Example:
Edit A: Insert at path [0, 1]
Edit B: Insert at path [0]
Transform B relative to A:
B' still at [0] (independent paths)
Transform A relative to B:
A' now at [0, 1, 1] (B changed structure)
"""
pass
print("Grove: Conflict-free collaborative structure editing")Making live programming fast enough for interactive use
class PerformanceOptimizations:
"""
Optimizations for live programming
Challenges:
- Type check on every keystroke (can't be slow!)
- Evaluate continuously (can't block UI)
- Large programs (thousands of lines)
"""
@staticmethod
def incremental_everything():
"""
1. Incremental parsing (structure editor: free!)
2. Incremental type checking (OOPSLA 2025)
3. Incremental evaluation (cache results)
4. Incremental rendering (React reconciliation)
"""
pass
@staticmethod
def lazy_evaluation():
"""
Don't evaluate everything immediately
- Evaluate visible parts
- Evaluate on demand (click to expand)
- Cache evaluation results
- Invalidate cache on edit
"""
pass
@staticmethod
def web_workers():
"""
Use Web Workers for heavy computation
Main thread: UI, editor
Worker thread: Type checking, evaluation
Communication:
- Main → Worker: Edit operations
- Worker → Main: Type info, results
"""
pass
@staticmethod
def memoization():
"""
Memoize expensive operations
- Type synthesis
- Constraint solving
- Pattern match analysis
- Evaluation results
"""
pass
print("Performance: Incremental + lazy + parallel + memoized")def example_driven_pattern():
"""
Live programming enables example-driven workflow
1. Write examples first
factorial 0 = 1
factorial 3 = 6
2. See examples fail (holes)
factorial n = ?impl
3. Implement to make examples pass
factorial 0 = 1
factorial n = n * factorial (n - 1)
4. Examples now pass live!
Immediate feedback guides implementation
"""
print("Examples first, then implement to match")def visual_debugging():
"""
Live evaluation enables visual debugging
- Click expression: See value
- Step through evaluation: See each step
- Inspect hole: See why indeterminate
- Trace execution: See call graph
No printf debugging needed!
"""
passdef exploratory_pattern():
"""
Live environment for exploration
1. Import library
2. Create hole: ?explore
3. See available functions (autocomplete)
4. Try function: f ?arg
5. See type error or result immediately
6. Iterate rapidly
Learning by experimentation
"""
pass| Component | Technology | Purpose | |-----------|------------|---------| | Editor | ReasonML + React | Structure editor UI | | Type checker | Bidirectional | Continuous typing | | Evaluator | Small-step | Live evaluation | | Backend | OCaml | Core semantics |
Edit → Mark dirty → Propagate → Re-type only dirty → Cache
Performance: O(size of edit) not O(size of program)Edit → Transform → Apply → Converge
Property: Commutative edits → No conflictsDeterminate: Concrete value
Indeterminate: Contains holes (⊥h)
Error: Type error (⦇e⦈ type mismatch)❌ Re-typing entire program on edit: Too slow ✅ Incremental type checking
❌ Blocking UI during evaluation: Unresponsive ✅ Use web workers, async evaluation
❌ No feedback on indeterminate: Confusing ✅ Show which hole blocked evaluation
❌ Conflicting concurrent edits: Data loss ✅ Use operational transformation (Grove)
hazelnut-calculus.md - Structure editor foundationtyped-holes-foundations.md - Basic holes theorytyped-holes-interaction.md - IDE features for holesstructure-editors.md - Editor design patternsoperational-semantics.md - Evaluation semanticsLast Updated: 2025-10-25 Format Version: 1.0 (Atomic)