Hazel
- Hazel は、型付きホールを含む不完全なプログラムを型チェックし、操作し、実行できるライブ関数型プログラミング環境
- 意味を持たないエディタ状態が存在しない
動機
- プログラミングでは、空欄、型エラー、マージ競合などにより、形式的に完全ではないプログラムテキストを扱う時間が多い
- 既存のプログラミング言語の定義は、こうした構造に公式な意味を与えていない
- プログラムエディタやツールは、複雑なその場しのぎの対処に依存せざるを得ない
- Hazel は、不完全なプログラムを型理論に基づいてモデル化する
Hazel の特徴
- Elm/ML に似た関数型プログラミング言語で、Web ベース環境として実装されている
- 不完全なプログラムも静的・動的の両面で適切に定義される
- 研究および教育プラットフォームとして活用できる
ニュースと出版物
- 2025年1月: POPL 2025 で Grove 論文が条件付き採択
- 2024年10月: OOPSLA 2024 で大規模言語モデルと型付きホールを組み合わせた研究を発表
- 2024年10月: HATRA 2024 で Cyrus の基調講演を予定
- 2024年9月: NSF が授業用証明支援ツール開発のための研究費を授与
- 2024年1月: POPL 2024 でエラー局所化と復旧に関する論文を発表
- 2023年10月: OOPSLA 2023 でパターンマッチングに関する研究を発表
- 2023年1月: NSF CAREER 賞を受賞
Team Hazel
- Hazel は、ミシガン大学 Future of Programming Lab が主導するオープンソース研究プロジェクト
- 質問や貢献に関心がある場合は、チームリーダーの Cyrus Omar に連絡できる
GN⁺の要約
- Hazel は、不完全なプログラムを扱う新しいアプローチを提案しており、プログラミング教育と研究に有用なプラットフォーム
- 型理論に基づき、不完全なプログラムも実行可能にすることで、プログラミングの未来を探ることに貢献する
- 類似の機能を持つプロジェクトとしては、Elm、ML、そしてさまざまなプログラミング教育ツールがある
1件のコメント
Hacker Newsのコメント
Eclipseの特徴の1つは、不完全または壊れたコードでも実行できる機能だった。これは、JavaのEclipse Compilerがほぼすべてのファイルに対してバイトコードを生成できたためである。この機能は非常に生産的な環境を提供していたが、他の大規模システムで実装されなかったのが残念。
Haskellには型ホールがあり、それを補完したりケース分割したりするコードアクションを提供するプラグインがある。Agdaにも型ホールがあり、さらに強力な機能を提供する。
Hazelに関する質問に答える用意があり、この4年間、Cyrusの博士課程の学生としてHazelに取り組んできた。現在はHazelでライブプログラミング向けのモルダブルなプロジェクショナルインターフェースを開発中である。
Hazelは型ホールを特徴とするライブ関数型プログラミング環境である。関連情報: Hacker Newsリンク
Tylrはタイルベース編集のデモで、新しい構造編集方式である。関連情報: Hacker Newsリンク
Hazelのコード例は気に入っており、ライブエディタと右側に表示されるドキュメントが良い。ただ、ライブエディタと型チェッカー以上の機能を提供するのか、実際にプログラムを書けるのかが気になる。
エディタUIが美しく、モバイルでもうまく動作する。非常に印象的。
"let"束縛が"in"で終わる文法は興味深い。例:
"in"キーワードの理由を知っている人はいる？
Idrisへの言及はなかったが、このスタイルの開発を最初に見たのはIdrisだった。関連動画: YouTubeリンク
Androidスマホでプレイグラウンドを試したが、キー入力がソースコードに反映されない。カーソルをタップして位置を指定でき、仮想キーボードも表示されるが、入力はできない。これはバグなのか、それともUXの問題なのか気になる。
Hazelは以前からずっと気に入っており、おそらく教育にとって素晴らしいツールになるだろう。Hazelで何が作られているのか気になる。