Typed Holesを特徴とするライブ関数型プログラミング環境 Hazel

• Hazel は typed holes（型付きホール） を中心に据えた Web ベースのライブ関数型プログラミング環境で、未完成のプログラムでも型検査・操作・実行できるようにする
• 空欄、型エラー、マージコンフリクトのような不完全な状態を ホール としてモデル化し、エディタが意味を失う区間を減らすことが中核
• Hazel で作成できる不完全なプログラムは静的・動的に定義され、不完全な型や不完全な実行結果を持ち得る
• 実装対象は Elm/ML 系の関数型言語で、プログラミング教育・共同編集・証明学習・AI コード補完研究の基盤として活用されている
• University of Michigan の Future of Programming Lab が主導するオープンソース研究プロジェクトで、体験用 Web ビルドと GitHub ソースコードが公開されている

---

Hazel の中核アイデア

• Hazel は ライブ関数型プログラミング環境であり、typed holes を中心に構成されている
• 未完成のプログラムでも次の作業を続けられる
  • 型検査
  • 操作
  • 実行
• 目標は、編集中のコードが壊れた状態でも 意味のあるフィードバック を維持する環境を作ること

不完全なプログラムを扱う方法

• 一般的なプログラミング過程では、プログラムテキストが形式的に完成していない状態が頻繁に発生する
  • 空欄
  • 型エラー
  • マージコンフリクト
• 既存のプログラミング言語定義はこのような構造に形式的な意味を与えないため、完成済みの一部コードの動作でさえ ライブフィードバック として扱うのが難しい
• エディタやツールは、コード補完、型検査、コード探索を途切れなく提供するために、複雑なヒューリスティックへ依存することになる
• Hazel は不完全なプログラムを ホールを持つプログラム としてモデル化する
  • ホールは欠けているプログラム部分を表す
  • エラーのある部分や共同作業環境での衝突部分を包む膜のように振る舞う
• このアプローチは、文脈的モーダル型理論と漸進的型理論に基づいている

Hazel の環境と実行モデル

• Hazel は Elm/ML に似た関数型言語向けの Web ベースのプログラミング環境 として実装されている
• Hazel の編集アクション言語で作成できるすべての不完全なプログラムは、静的・動的に定義される
  • 不完全な型を持ち得る
  • 実行すると不完全な結果を生成し得る
• この特性により、Hazel は未来のプログラミング環境とプログラミング教育研究のためのプラットフォームとして使われている

研究ビジョンと関連資料

• Toward Semantic Foundations for Program Editors: プログラムエディタのための意味論的基盤に関する研究ビジョン
• Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine: 大規模計算科学のためのライブで合成可能な協調型計算環境のビジョン
• Hazel 関連の発表は YouTube playlist of Hazel-related talks にまとまっている
• 最近のデモは Topos Institute 発表 で見られる

最近の研究と出版の流れ

• 2025年には Hazel 周辺の研究が複数の学会で発表された
  • Incremental Bidirectional Typing via Order Maintenance: ブラウザのレイアウトシステムの技法を借りて双方向型検査をインクリメンタル化する研究で、OOPSLA 2025 Distinguished Paper Award を受賞
  • Syntactic Completions with Material Obligations: Tylr システムで視覚的に具体化された義務を活用し、構文エラーを修復する理論と実装
  • A FAIR Case for a Live Computational Commons: 大規模ライブプログラミング環境を中心に科学的作業を再構成する提案
  • Decomposable Type Highlighting for Bidirectional Type and Cast Systems: Hazel で静的・動的な型エラーをデバッグするための UI 研究
  • Hazel Deriver: A Live Editor for Constructing Rule-Based Derivations: 自然演繹スタイルの導出過程を構成する教育用ツール
• 2024年には型エラー復旧、LLM 連携、証明学習、気候科学計算環境が主要テーマとして続いた
  • Total Type Error Localization and Recovery with Holes は、誤って型付けされたプログラムのエラー位置特定と復旧を扱い、POPL 2024 Distinguished Paper Award を受賞
  • Statically Contextualizing Large Language Models with Typed Holes は、言語サーバと大規模言語モデルを組み合わせ、AI コード補完性能を大きく改善する取り組み
  • NSF は、Hazel を教室向け証明支援ツールへ転換する研究課題に資金提供している
• 2017年から2023年までの研究は、Hazel の基盤計算、構造編集、ライブ評価、教育支援機能を段階的に発展させた
  • Hazelnut: A Bidirectionally Typed Structure Editor Calculus は、typed holes を自動挿入する編集アクション計算を定義する
  • Live Functional Programming with Typed Holes は、typed holes を持つ式の豊かな操作的意味論を開発する
  • Program Sketching with Live Bidirectional Evaluation は、Hazel Assistant の基盤構成要素である Smyth を扱う
  • Live Pattern Matching with Typed Holes は、パターンホールを持つプログラム推論を扱い、OOPSLA 2023 Distinguished Paper Award を受賞

利用と貢献

• Hazel は直接体験できる Web ビルドを提供している
  • Play with Hazel
• ソースコードは GitHub で公開されている
  • Source code on GitHub
• Hazel は University of Michigan の Future of Programming Lab (FP Lab) が率いる オープンソース研究プロジェクト
• 貢献や質問については、チームリードの Cyrus Omar に連絡できる