使用Liquid Haskell进行孔驱动开发
Toward Hole-Driven Development with Liquid Haskell
摘要：
Liquid Haskell是对Haskell程序设计语言的扩展，它增加了对细化类型的支持：用SMT可判定的逻辑谓词扩充的数据类型，这些逻辑谓词细化可以驻留在类型中的值集。此外，Liquid Haskell对精化反射的支持使Haskell能够用于通用的机械化定理证明。Liquid Haskell中越来越多的大规模机械化证明开发利用了这种能力。向Haskell这样的“遗留”语言添加定理证明功能，可以让程序员直接验证真实世界Haskell程序的属性（利用现有的高度调优的编译器，运行时系统和库），只需编写Haskell。然而，更成熟的证明助手，如Agda和Coq，为交互式证明开发和对证明状态的洞察提供了更好的支持（例如，为了完成部分完成的证明，还需要证明哪些子目标）。相反，Liquid Haskell只向用户提供粗粒度的反馈--要么报告类型错误，要么不报告--不幸的是，这阻碍了它作为定理证明器的可用性。在本文中，我们建议通过扩展对Agda风格类型化孔的支持和利用它们的交互式编辑命令来提高Liquid Haskell的可用性。在Agda中，类型化的洞允许程序员指出证明中未完成的部分，并在与编译器的对话中逐步完成证明。虽然GHC Haskell已经有了自己的受Agda启发的对类型化孔的支持，但我们认为，如果与Liquid Haskell的细化类型和SMT自动化相结合，类型化孔将特别强大和有用。我们讨论了类型化的洞如何在Liquid Haskell中工作，并考虑了可能的实现方法和后续步骤。
英文摘要：
Liquid Haskell is an extension to the Haskell programming language that adds support for refinement types: data types augmented with SMT-decidable logical predicates that refine the set of values that can inhabit a type. Furthermore, Liquid Haskell's support for refinement reflection enables the use of Haskell for general-purpose mechanized theorem proving. A growing list of large-scale mechanized proof developments in Liquid Haskell take advantage of this capability. Adding theorem-proving capabilities to a "legacy" language like Haskell lets programmers directly verify properties of real-world Haskell programs (taking advantage of the existing highly tuned compiler, run-time system, and libraries), just by writing Haskell. However, more established proof assistants like Agda and Coq offer far better support for interactive proof development and insight into the proof state (for instance, what subgoals still need to be proved to finish a partially-complete proof). In contrast, Liquid Haskell provides only coarse-grained feedback to the user -- either it reports a type error, or not -- unfortunately hindering its usability as a theorem prover. In this paper, we propose improving the usability of Liquid Haskell by extending it with support for Agda-style typed holes and interactive editing commands that take advantage of them. In Agda, typed holes allow programmers to indicate unfinished parts of a proof, and incrementally complete the proof in a dialogue with the compiler. While GHC Haskell already has its own Agda-inspired support for typed holes, we posit that typed holes would be especially powerful and useful if combined with Liquid Haskell's refinement types and SMT automation. We discuss how typed holes might work in Liquid Haskell, and we consider possible implementation approaches and next steps.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
