一句话：提出外延相等保持原则，在内涵类型论中无需扩展理论或完整 setoid 即可进行已验证泛型编程。
已验证泛型编程需要在抽象数据类型之上推理，无法依赖具体数据类型结构。函子与单子是函数式编程的核心，但许多重要单子的函子映射保持外延相等：若 f 与 g 外延相等，则 map f 与 map g 也外延相等。本文探索将这一性质作为已验证泛型编程的基本原则。作者采用极简方法，在 Martin-Löf 内涵类型论中处理外延相等的缺失，不扩展理论，也不使用完整的 setoid。结果表明，这一极简方法非常有用：既能给出单子律的简单泛型证明，也能在动力系统与控制理论中获得已验证的泛型结果，从而避免繁琐的代码重复与专门证明。该工作推动了实用化的已验证泛型编程。
Abstract 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 \, \to \, B$$ are extensionally equal, that is, $$\forall x \in A$$ , $$f \, x = g \, x$$ , then $$map \, f \, : \, List \, A \to 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 toward pragmatic, verified generic programming.
@article{paperbot1241,
title = {Extensional equality preservation and verified generic programming},
author = {NICOLA BOTTA and NURIA BREDE and PATRIK JANSSON and TIM RICHTER},
journal = {Journal of Functional Programming},
volume = {31},
year = {2021},
doi = {10.1017/s0956796821000204}
}