Parametricity for Nested Types and GADTs

This paper considers parametricity and its consequent free theorems fornested data types. Rather than representing nested types via their Churchencodings in a higher-kinded or dependently typed extension of System F, weadopt a functional programming perspective and design a Hindley-Milner-stylecalculus with primitives for constructing nested types directly as fixpoints.Our calculus can express all nested types appearing in the literature,including truly nested types. At the level of terms, it supports primitivepattern matching, map functions, and fold combinators for nested types. Ourmain contribution is the construction of a parametric model for our calculus.This is both delicate and challenging. In particular, to ensure the existenceof semantic fixpoints interpreting nested types, and thus to establish asuitable Identity Extension Lemma for our calculus, our type system mustexplicitly track functoriality of types, and cocontinuity conditions on thefunctors interpreting them must be appropriately threaded throughout the modelconstruction. We also prove that our model satisfies an appropriate AbstractionTheorem, as well as that it verifies all standard consequences of parametricityin the presence of primitive nested types. We give several concrete examplesillustrating how our model can be used to derive useful free theorems,including a short cut fusion transformation, for programs over nested types.Finally, we consider generalizing our results to GADTs, and argue that noextension of our parametric model for nested types can give a functorialinterpretation of GADTs in terms of left Kan extensions and still beparametric