Inductive Type Schemas as Functors

Abstract

Parametric inductive types can be seen as functions taking type parameters as arguments and returning the instantiated inductive types. Given functions between parameters one can construct a function between the instantiated inductive types representing the change of parameters along these functions. It is well known that it is not a functor w.r.t. intensional equality based on standard reductions. We investigate a simple type system with inductive types and iteration and show by modular rewriting techniques that new reductions can be safely added to make this construction a functor, while the decidability of the internal conversion relation based on the strong normalization and confluence properties is preserved. Possible applications: new categorical and computational structures on λ-calculus, certified computation.