Hazel：一个以类型化孔为特色的实时函数式编程环境

Hazel是一个活动的函数式编程环境，能够检查、操作甚至运行不完整的程序，即有漏洞的程序。没有毫无意义的编辑状态。

在编程时，我们花费大量时间处理尚未正式完成的程序文本，例如，因为在各个位置存在空白点、键入错误或合并冲突。传统的编程语言定义没有为这样的结构赋予正式含义，因此程序编辑器和其他工具别无选择，只能求助于复杂和特别的试探法，以提供各种有用的语言服务(如代码完成、类型检查、代码导航和实时编程服务)，而不会出现服务空白。

我们正在开发一种更有原则的方法来处理不完整的程序，植根于(上下文模态和渐进式)类型理论。我们将不完整的程序建模为有洞的程序，这些洞(1)代表程序中缺失的部分；(2)充当程序中错误或在协作环境中冲突的部分的薄膜。

我们正在将这些想法落实到Hazel中，这是一个基于Web的编程环境，用于一种类似ELM/ML的函数式编程语言，正在围绕类型化的洞驱动开发从头开始设计。

唯一的是，您可以使用Hazel的类型感知编辑操作语言构建的每个不完整的程序都是静态和动态定义良好的，即它具有(可能不完整的)类型，并且您可以运行它来产生(可能不完整的)结果。因此，Hazel为研究编程的未来提供了一个优雅的平台。

首先，我们开发了一个核心演算Hazelut，它提供了(1)表达式和类型位置都有空洞的表达式的静态语义(即类型系统)，以及(2)自动插入空洞的编辑动作语言，以确保每个编辑状态都有静态含义。

榛子：双向类型结构编辑器Calculus C.Omar，I.Voysey，M.Hilton，J.Aldrich和M.Hammer POPL 2017[.bib][幻灯片]。

接下来，我们开发了榛子Live，它为表达式和类型位置上都有空洞的表达式提供了动态语义。我们不会在运行时遇到漏洞时立即停止，而是尽可能地继续计算，生成包含漏洞关闭的结果。漏洞关闭使我们能够持续向程序员提供细粒度的实时反馈，并在填补漏洞后恢复评估。

本文从渐进型理论和语境情态型理论两个方面详细介绍了我们是如何运用机制来实现这一点的。用打字孔进行实时函数编程C.Omar，I.Voysey，R.Chugh和M.Hammer POPL 2019[.bib]。

我们有很多正在酝酿中的想法--如果你对其中任何一个感兴趣，一定要与他们联系。我们也很想听听您可能有的其他想法。

我们正在开发一种键盘驱动的编辑体验，它建立在您对文本编辑的直觉之上，并且支持复杂的代码重组模式。我们正在做用户研究。

我们正在努力允许程序员通过直接操作带有洞的实时GUI来填补漏洞。

我们正在考虑如何指定编辑动作语义，该语义遵守使Hazelut程序成为收敛复制数据类型(CRDT)所必需的不变量。

我们正在考虑如何构建一个编程助手，通过将Hazel提供给程序合成和机器学习算法的语义数据提供给程序员建议有用的编辑操作。

随着Hazel的发展，我们计划首先应用它来教授函数式编程入门课程，然后我们计划使用Hazel来支持数据分析(设想下一代Jupyter)。总有一天，我们希望Hazel会成为一种新型计算维基的基础。

Hazel是密歇根大学未来编程实验室(FP Lab)领导的一个开源项目。

如果你有兴趣为黑兹尔做贡献，或者你想加入松弛会，在那里我们帮助人们学习必要的类型理论并讨论项目方向，请与赛勒斯联系！

赛勒斯一开始是密歇根大学的助理教授。大卫·穆恩(David Moon)作为博士生加入了他的行列。迈克尔·D·亚当斯(Michael D.Adams)也以研究科学家的身份加入。

NSF选择了Cyrus、Ravi和Matthew提出的为期三年的研究资金。

Cyrus和David在普渡举行的中西部PL峰会上介绍了Hazel编辑经验和生动的进展。

David介绍了Hazel编辑经验的进展[扩展摘要]，Cyrus在柏林ICFP 2019年的Tyde研讨会上用Hazel[幻灯片，扩展摘要]展示了生动的图片。