Map fusion for nested datatypes in intensional type theory

AbstractA definitional extension LNGMIt of the Calculus of Inductive Constructions (CIC), that underlies the proof assistant Coq, is presented that allows also to program with nested datatypes that are not legal datatype definitions of CIC since they are “truly nested”. LNGMIt ensures termination of recursively defined functions that follow iteration schemes in the style of N. Mendler. Characteristically for them, termination comes from polymorphic typing instead of structural requirements on recursive calls.LNGMIt comes with an induction principle and generalized Mendler-style iteration that allows a very clean representation of substitution for an untyped lambda calculus with explicit flattening, as an extended case study.On the generic level, a notion of naturality adapted to generalized Mendler-style iteration is developed, and criteria for it are established, in particular, a map fusion theorem for the obtained iterative functions.Concerning the case study, substitution is proven to fulfill two of the three monad laws, the third one only for “hereditarily canonical” terms, but this is rectified by a relativization of the whole construction to those terms. All the generic results and the case study have been fully formalized with the Coq system