∂ is for Dialectica: typing differentiable programming
This abstract has two aims. The first is to highlight the fact that the Dialectica transformation is a differential transformation. We will insist that it has a reverse-mode flavor. The second object of this abstract is work in progress, refining the use of linear types in differentiable programming by introducing positive and negative types, and showing that distribution theory offers a syntax for a typed higher-order principled differentiable programming language, in which algorithms of automatic differentiation are expressed as reduction strategies.