依赖类型启用的编程风格的名称是啥（想想 Coq 或 Agda）？

Posted 2023-05-08

【中文标题】依赖类型启用的编程风格的名称是啥（想想 Coq 或 Agda）？

【英文标题】：What is the name of the programming style enabled by dependent types (think Coq or Agda)?依赖类型启用的编程风格的名称是什么（想想 Coq 或 Agda）？

【发布时间】：2021-04-03 03:12:01

【问题描述】：

有一种编程“风格”（或者可能是范式，我不知道该怎么称呼它）如下：

首先，您编写一个规范：正式描述您的（整个或部分）程序要做什么。这是在编程系统内完成的；它不是一个单独的工件。

然后，您编写程序，但是 - 这是这种编程风格与其他风格之间的关键区别 - 编写任务的每一步都引导在某种程度上由您编写的规范在上一步中。这种指导的具体发生方式千差万别；在 Coq 中，你有一种元编程语言 (Ltac)，它可以让你在幕后构建实际程序的同时“改进”规范，而在 Agda 中，你通过填充“漏洞”来编写程序（我实际上不确定它是如何进入的Agda，因为我主要习惯于 Coq）。

这并不是每个人都喜欢的编程风格，但我想尝试用通用的流行编程语言来练习它。至少在 Coq 中我发现它相当容易上瘾！

...但是我什至如何在证明助手之外寻找方法呢？这就引出了一个问题：我正在为这种编程风格寻找一个名称，以便我可以尝试查找可以让我在其他编程语言中进行类似编程的工具。

请注意，当然更合适的问题是直接询问此类工具的示例，但要求答案列表的 AFAIK 问题不适用于 Stack Exchange 网站。

并且要明确一点，我并不是那么希望我真的会找到很多；这些主要是学术消遣，而您的典型编程语言并不真正适合这种编程风格（例如，规范语言最终可能会变得难以置信地复杂）。但值得一试！

【问题讨论】：

一些零散的想法：1) Idris 可能是这些方面最流行的通用编程语言？ 2) 我知道 Frama-C 与 C 的规范语言有关，也许可以在其中以这种风格进行编程？ 3）Haskell 有一个叫 LiquidHaskell 的东西，它是这种风格的实现吗？

您所描述的似乎接近某种形式的细化演算，这可以在一些关于 Coq 的论文中或多或少明确地找到（例如参见 Sylvain Boulmé 的 Intuitionistic Refinement Calculus）。从广义上讲，该关键字似乎导致了许多软件工程方面的书籍和论文......

【参考方案1】：

称为证明驱动开发（或类型驱动开发）。但是，关于它的信息很少。

【参考方案2】：

您提到的通过 ltac（在 coq 的情况下）或孔（在 Agda 和 Idris 的情况下）缓慢创建程序的过程称为细化。因此，您还可以在文献中找到这种风格的参考，作为细化证明或细化编程。

现在要意识到的最重要的事情是，这种编程风格是更复杂的类型系统所固有的，它将允许您在当前环境中提取尽可能多的信息。所以很自然地发现附加了依赖类型，尽管不一定如此。

正如在另一个回复中提到的，您还将找到将其作为类型驱动开发的引用，有一个关于它的 idris book。

您可能有兴趣研究其他一些项目，例如 Lean、Isabelle、Idris、Agda、Cedille，也许还有 Liquid Haskell、TLA+ 和 SAW。

【参考方案3】：

正如前两个答案所指出的，您提到的程序样式的一个可能名称当然是：类型驱动开发。

从 Coq 的角度来看，您可能对以下两个参考资料感兴趣：

Certified Programming with Dependent Types（CPDT，作者：Adam Chlipala）：Coq 教科书，教授开发依赖类型 Coq 理论和自动化相关证明的高级技术。

经验报告：Coq 中认证树算法的类型驱动开发（作者：Reynald Affeldt、Jacques Garrigue、Xuanrui Qi、Kazunari Tanaka），发表在Coq Workshop 2019 (slides, @ 987654324@):

作者还使用了首字母缩略词 TDD，有趣的是，它在软件工程社区中也有另一个接受：test-driven development（这种广泛使用的方法自然会产生高质量的测试套件）。 实际上，两种对 TDD 的接受都有一个共同的想法：一个系统地从编写规范开始（考虑的单元），然后才编写一些满足规范的代码（使单元测试通过），然后我们循环并增量指定+实现（+重构）其他代码单元。

最后但同样重要的是，this discussion from the Discourse OCaml forum 中有一些额外的指针。