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 list_shape (a b : Type)
| nil : list_shape
| cons : a -> b -> list_shape
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 list_shape a -- not the actual notation
We can continue and define the quotient on permutation of lists and create the multiset type:
And multiset
is also a QPF. We can then create a novel data type (for Lean):
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 #
- P : mvpfunctor n
- abs : Π {α : typevec n}, (mvqpf.P F).obj α → F α
- repr : Π {α : typevec n}, F α → (mvqpf.P F).obj α
- abs_repr : ∀ {α : typevec n} (x : F α), mvqpf.abs (mvqpf.repr x) = x
- abs_map : ∀ {α β : typevec n} (f : α.arrow β) (p : (mvqpf.P F).obj α), mvqpf.abs (mvfunctor.map f p) = mvfunctor.map f (mvqpf.abs p)
Multivariate quotients of polynomial functors.
Instances of this typeclass
Instances of other typeclasses for mvqpf
- mvqpf.has_sizeof_inst
Show that every mvqpf is a lawful mvfunctor. #
A qpf is said to be uniform if every polynomial functor representing a single value all have the same range.
does abs
preserve liftp
?
Equations
- q.liftp_preservation = ∀ ⦃α : typevec n⦄ (p : Π ⦃i : fin2 n⦄, α i → Prop) (x : (mvqpf.P F).obj α), mvfunctor.liftp p (mvqpf.abs x) ↔ mvfunctor.liftp p x
does abs
preserve supp
?
Equations
- q.supp_preservation = ∀ ⦃α : typevec n⦄ (x : (mvqpf.P F).obj α), mvfunctor.supp (mvqpf.abs x) = mvfunctor.supp x