Discrete generalised polynomial functors (extended abstract)

Abstract

We study generalised polynomial functors between presheaf categories, developing their mathematical theory together with computational applications. The main theoretical contribution is the introduction of discrete generalised polynomial functors, a class that lies in between the classes of cocontinuous and finitary functors, and is closed under composition, sums, finite products, and differentiation. A variety of applications are given: to the theory of nominal algebraic effects; to the algebraic modelling of languages, and equational theories there of, with variable binding and polymorphism; and to the synthesis of dependent zippers. © 2012 Springer-Verlag Berlin Heidelberg.