Live Pattern Matching with Typed Holes
Live Pattern Matching with Typed Holes
复制标题
与键入的孔进行实时图案匹配
DOI：
10.1145/3586048
复制
发表时间：
2023
影响因子：
--
通讯作者：
Omar, Cyrus
中科院分区：
文献类型：
--
作者：
Yuan, Yongwei;Guest, Scott;Griffis, Eric;Potter, Hannah;Moon, David;Omar, Cyrus
包括GHC Haskell、AGDA、Idris和Hazel在内的几个现代编程系统都支持类型孔。为带有空洞的程序分配静态和不同程度的动态含义允许程序编辑人员和其他工具在整个编辑过程中提供有意义的反馈和帮助，即在实况编辑中。然而，以前的工作只考虑了出现在表达式和类型中的空洞。本文从类型论和逻辑第一原理出发，讨论了类型化的模孔问题。我们面临着两个主要困难，(1)当模式不完全已知时，关于穷举性和无冗余性的静态推理；(2)同时包含模式和表达式漏洞的表达式的实时计算。在这两种情况下，这都需要对所有可能的漏洞进行保守的推理。我们开发了一个类型化的Lambda演算，花生，其中关于穷举和冗余的推理被映射到推导一阶蕴涵的问题。我们为Peanut配备了榛子Live风格的操作语义，允许我们在表达式和模式中计算周围的洞。我们在AGDA中机械化了花生的元理论，并形式化了一个能够决定必要蕴涵的程序。最后，我们在Hazel中扩展并实现了这些机制，Hazel是一个针对ELM方言的编程环境，它在编辑过程中自动插入洞，以最大限度地实时向程序员提供静态和动态反馈，即针对每种可能的编辑状态。Hazel是第一个具有最大生命力的通用函数式语言环境。
Several modern programming systems, including GHC Haskell, Agda, Idris, and Hazel, supporttyped holes. Assigning static and, to varying degree, dynamic meaning to programs with holes allows program editors and other tools to offer meaningful feedback and assistance throughout editing, i.e. in alivemanner. Prior work, however, has considered only holes appearing in expressions and types. This paper considers, from type theoretic and logical first principles, the problem of typed pattern holes. We confront two main difficulties, (1) statically reasoning about exhaustiveness and irredundancy when patterns are not fully known, and (2) live evaluation of expressions containing both pattern and expression holes. In both cases, this requires reasoning conservatively about all possible hole fillings. We develop a typed lambda calculus, Peanut, where reasoning about exhaustiveness and redundancy is mapped to the problem of deriving first order entailments. We equip Peanut with an operational semantics in the style of Hazelnut Live that allows us to evaluate around holes in both expressions and patterns. We mechanize the metatheory of Peanut in Agda and formalize a procedure capable of deciding the necessary entailments. Finally, we scale up and implement these mechanisms within Hazel, a programming environment for a dialect of Elm that automatically inserts holes during editing to provide static and dynamic feedback to the programmer in a maximally live manner, i.e. for every possible editor state. Hazel is the first maximally live environment for a general-purpose functional language.
登录
查看更多内容
GADT 遇到了他们的对手：解释 GADT、守卫和懒惰的模式匹配警告
DOI：
10.1145/2784731.2784748
发表时间：
2015
期刊：
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
G. Karachalias;Tom Schrijvers;Dimitrios Vytiniotis;S. Jones
通讯作者：
S. Jones
专注于模式匹配
DOI：
10.1145/1480881.1480927
发表时间：
2009
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
N. Krishnaswami
通讯作者：
N. Krishnaswami
影响因子：
1.3
作者：
Lennon-Bertrand，Meven;Maillard，Kenji;Tanter，Eric
通讯作者：
Tanter，Eric
为程序编辑奠定语义基础
DOI：
--
发表时间：
2017
期刊：
Summit on Advances in Programming Languages
影响因子：
--
作者：
Cyrus Omar;Ian Voysey;Michael C Hilton;Joshua Sunshine;Claire Le Goues;Jonathan Aldrich;Matthew A. Hammer
通讯作者：
Matthew A. Hammer
嘟比嘟比嘟
影响因子：
1.1
作者：
CONVENT L
通讯作者：
CONVENT L