We show how to apply forward and reverse mode Combinatory Homomorphic Automatic Differentiation (CHAD) to total functional programming languages with expressive type systems featuring the combination of - tuple types; - sum types; - inductive types; - coinductive types; - function types. We achieve this by analysing the categorical semantics of such types in $\Sigma$-types (Grothendieck constructions) of suitable categories. Using a novel categorical logical relations technique for such expressive type systems, we give a correctness proof of CHAD in this setting by showing that it computes the usual mathematical derivative of the function that the original program implements. The result is a principled, purely functional and provably correct method for performing forward and reverse mode automatic differentiation (AD) on total functional programming languages with expressive type systems.

翻译：我们展示了如何将前向与反向模式的组合同态自动微分（CHAD）应用于具有表达性类型系统的全函数式编程语言，这些系统结合了以下类型：元组类型、和类型、归纳类型、共归纳类型以及函数类型。我们通过分析此类类型在适当范畴的Σ-类型（Grothendieck构造）中的范畴语义来实现这一点。针对此类表达性类型系统，我们采用一种新颖的范畴逻辑关系技术，给出了CHAD在此设定下的正确性证明，表明其能够计算原始程序所实现函数的通常数学导数。研究结果提供了一种 principled（基于原则的）、纯函数式的且可证明正确的方法，用于对具有表达性类型系统的全函数式编程语言执行前向与反向模式自动微分（AD）。