coq - Coq 中的一流模块

Question

谁能给我更多关于 Coq 中一流模块的信息？我知道 Coq 中的模块不是一流的。我想知道为什么？将来 Coq 中的模块有可能成为一流的吗？

非常感谢你

Answer 1

我不确定，但据我了解，它基本上来自两点：

1. Coq 是保守的。因为它的一些主要应用是在验证中，所以 Coq 主要将自己限制在语义被合理理解的构造中。

2. 在依赖类型设置中，一流的模块相当微妙且没有被完全理解。 特别是，您希望在模块之外看到多少定义的计算/简化行为？如果根本没有，那么这已经是可用的，作为记录类型。但是，如果部分或全部减少行为是可见的，那么很难准确量化到底有多少，因此很难分析结果模块的语义。

我不是相关文献的专家，所以我对2可能是错误的，但我的印象是这是基本情况。