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:
def List (a : Type) := fix ListShape a -- not the actual notation
We can continue and define the quotient on permutation of lists and create the multiset type:
def Multiset (a : Type) := QPF.quot List.perm List a -- not the actual notion
And 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 #
- constructions
- Fix
- Cofix
- Quot
- Comp
- Sigma / Pi
- Prj
- Const
each proves that some operations on functors preserves the QPF structure
Reference #
! * [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, Data Types as Quotients of Polynomial Functors][avigad-carneiro-hudon2019]
- P : MvPFunctor n
- abs : {α : TypeVec n} → MvPFunctor.Obj (MvQPF.P F) α → F α
- repr : {α : TypeVec n} → F α → MvPFunctor.Obj (MvQPF.P F) α
- abs_repr : ∀ {α : TypeVec n} (x : F α), MvQPF.abs (MvQPF.repr x) = x
- abs_map : ∀ {α β : TypeVec n} (f : TypeVec.Arrow α β) (p : MvPFunctor.Obj (MvQPF.P F) α), MvQPF.abs (MvFunctor.map f p) = MvFunctor.map f (MvQPF.abs p)
Multivariate quotients of polynomial functors.