CHAD for expressive total languages

We show how to apply forward and reversemode Combinatory Homomorphic Automatic Differentiation (CHAD) (Vakar (2021). ESOP, 607-634; Vakar and Smeding (2022). ACM Transactions on Programming Languages and Systems 44 (3) 20:1-20:49.) 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 analyzing 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.