Authors: Andreas Lochbihler and Joshua Schneider
Paper Information
Title: | Relational parametricity and quotient preservation for modular (co)datatypes |
Authors: | Andreas Lochbihler and Joshua Schneider |
Proceedings: | ITP Papers |
Editors: | Jeremy Avigad and Assia Mahboubi |
Keywords: | Isabelle/HOL, datatypes, parametricity, functor, quotients, polytyptic programming |
Abstract: | ABSTRACT. Bounded natural functors (BNFs) provide a modular framework for the construction of (co)datatypes in higher-order logic. Their functorial operations, the mapper and relator, are restricted to a subset of the parameters, namely those where recursion can take place. For certain applications, such as free theorems, representation independence, data refinement, and quotients, it is desirable if these operations do not ignore the other parameters. In this paper, we generalise BNFs to distinguished co- and contravariant parameters that the mapper and relator act on. Crucially, our generalisation BNFCC is closed under functor composition and least and greatest fixpoints. In particular, every (co)datatype is also a BNFCC. Moreover, we prove that subtypes inherit the BNFCC structure under conditions that generalise those for the BNF case. We also identify sufficient conditions under which a BNFCC preserves quotients and the relator distributes over relation composition. Our development is formalised abstractly in Isabelle/HOL in such a way that it integrates seamlessly with the existing parametricity infrastructure. |
Pages: | 19 |
Talk: | Jul 11 11:00 (Session 64C) |
Paper: |