Multivariate quotients of polynomial functors. #
Basic definition of multivariate QPF. QPFs form a compositional framework for defining inductive and coinductive types, their quotients and nesting.
The idea is based on building ever larger functors. For instance, we can define a list using a shape functor:
inductive ListShape (a b : Type) | nil : ListShape | cons : a -> b -> ListShape
This shape can itself be decomposed as a sum of product which are themselves QPFs. It follows that the shape is a QPF and we can take its fixed point and create the list itself:
We can continue and define the quotient on permutation of lists and create the multiset type:
Multiset is also a QPF. We can then create a novel data type (for Lean):
inductive Tree (a : Type) | node : a -> Multiset Tree -> Tree
An unordered tree. This is currently not supported by Lean because it nests an inductive type inside of a quotient. We can go further and define unordered, possibly infinite trees:
coinductive Tree' (a : Type) | node : a -> Multiset Tree' -> Tree'
by using the
cofix construct. Those options can all be mixed and
matched because they preserve the properties of QPF. The latter example,
Tree', combines fixed point, co-fixed point and quotients.
Related modules #
- Sigma / Pi
each proves that some operations on functors preserves the QPF structure
! * [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, Data Types as Quotients of Polynomial Functors][avigad-carneiro-hudon2019]
- P : MvPFunctor n
Multivariate quotients of polynomial functors.