外延相等性保持与验证的泛型编程
Extensional equality preservation and verified generic programming
AI总结：
本文提出在马丁-洛夫内涵类型理论中，通过极简方法利用外延相等性保持原则，实现验证的泛型编程，从而简化单子定律及动力系统与控制理论的证明，避免代码重复。
摘要：
在验证的泛型编程中，人们无法利用具体数据类型的结构，而必须依赖于精心选择的规范集或抽象数据类型（ADT）。函子和单子是函数式编程许多应用的核心。这引出了一个问题：对于验证的函子和单子，有用的抽象数据类型可能是什么样子。许多重要单子的函子映射保持外延相等性。例如，如果 $f, g : A \rightarrow B$ 是外延相等的，即 $\forall x \in A, \\ f \\ x = g \\ x$，那么 $map \\ f : List \\ A \rightarrow List \\ B$ 和 $map \\ g$ 也是外延相等的。这表明外延相等性的保持可能是验证的泛型编程中的一个有用原则。我们以一种极简主义的方法探索这种可能性：我们在马丁-洛夫的内涵类型理论中处理（缺乏）外延相等性的问题，而不扩展这些理论或使用完整的集合体。也许令人惊讶的是，这种极简方法被证明极其有用。它允许推导出单子定律的简单泛型证明，以及动力系统和控制理论中的验证的、泛型的结果。反过来，这些结果避免了繁琐的代码重复和特设证明。因此，我们的工作是对实用的、验证的泛型编程的一个贡献。
英文摘要：
In verified generic programming, one cannot exploit the structure of concrete data types but has to rely on well chosen sets of specifications or abstract data types (ADTs). Functors and monads are at the core of many applications of functional programming. This raises the question of what useful ADTs for verified functors and monads could look like. The functorial map of many important monads preserves extensional equality. For instance, if $f, g : A \rightarrow B$ are extensionally equal, that is, $\forall x \in A, \ f \ x = g \ x$, then $map \ f : List \ A \rightarrow List \ B$ and $map \ g$ are also extensionally equal. This suggests that preservation of extensional equality could be a useful principle in verified generic programming. We explore this possibility with a minimalist approach: we deal with (the lack of) extensional equality in Martin-Löf's intensional type theories without extending the theories or using full-fledged setoids. Perhaps surprisingly, this minimal approach turns out to be extremely useful. It allows one to derive simple generic proofs of monadic laws but also verified, generic results in dynamical systems and control theory. In turn, these results avoid tedious code duplication and ad-hoc proofs. Thus, our work is a contribution towards pragmatic, verified generic programming.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
