A foundation for GADTs and inductive families
Makoto Hamana, Marcelo Fiore · 2011
Every Algebraic Datatype (ADT) is characterised as the initial algebra of a polynomial functor on sets. This paper extends the characterisation to the case of more advanced datatypes: Generalised Algebraic Datatypes (GADTs) and Inductive Families. Specifically, we show that GADTs and Inductive Families are characterised as initial algebras of dependent polynomial functors. The theoretical tool we use throughout is an abstract notion of polynomial between sets together with its associated general form of polynomial functor between categories of indexed sets introduced by Gambino and Hyland.