A foundation for GADTs and inductive families: dependent polynomial functor approach

Every Algebraic Datatype (ADT) is characterised as the initial al-gebra of a polynomial functor on sets. This paper extends the char-acterisation to the case of more advanced datatypes: Generalised Algebraic Datatypes (GADTs) and Inductive Families. Specifi-cally, we show that GADTs and Inductive Families are charac-terised as initial algebras of dependent polynomial functors. The theoretical tool we use throughout is an abstract notion of poly-nomial between sets together with its associated general form of polynomial functor between categories of indexed sets introduced by Gambino and Hyland. In the context of ADTs, this fundamental result is the basis for various generic functional programming techniques. To estab-lish the usefulness of our approach for such developments in the broader context of inductively defined dependent types, we apply the theory to construct zippers for Inductive Families