扩展性等式保持与验证泛型编程
摘要：验证泛型编程中，我们不能利用具体数据结构的结构，而必须依赖于精心选择的规范集或抽象数据类型（ADTs）。函数器和单子是函数式编程许多应用的核心。这引发了一个问题，即验证的函数器和单子的有用ADTs可以是什么样子。许多重要单子的函子映射保留外延等价。例如，如果$f，g：A \rightarrow B$在外延上相等，也就是说，对于$A$中的每个$x$，有$f x = g x$，那么$map f：List A \rightarrow List B$和$map g$也是外延等价的。这表明，保留外延等价可能是验证的泛型编程中一个有用的原则。我们以一种最简方法探讨了这个可能性：我们处理（缺乏）马丁-罗夫的内涵类型理论中的外延等价，而不扩展理论或使用完整的集合。也许令人惊讶的是，这种最小方法非常有用。它可以推导出单子定律的简单泛型证明，但也是验证的、泛型的动态系统和控制理论结果。反过来，这些结果避免了乏味的代码重复和特定于场景的证明。因此，我们的工作是朝着实用的、验证的泛型编程做出的贡献。
作者：Nicola Botta and Nuria Brede and Patrik Jansson and Tim Richter
论文ID：2008.02123
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22