Quotients of Polynomial Functors
We assume the following:
P : a polynomial functor
W : its W-type
M : its M-type
F : a functor
We define:
q : qpf data, representing F as a quotient of P
The main goal is to construct:
fix : the initial algebra with structure map F fix → fix.
cofix : the final coalgebra with structure map cofix → F cofix
We also show that the composition of qpfs is a qpf, and that the quotient of a qpf is a qpf.
The present theory focuses on the univariate case for qpfs
References
- [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, Data Types as Quotients of Polynomial Functors][avigad-carneiro-hudon2019]
- P : pfunctor
- abs : Π {α : Type ?}, (qpf.P F).obj α → F α
- repr : Π {α : Type ?}, F α → (qpf.P F).obj α
- abs_repr : ∀ {α : Type ?} (x : F α), qpf.abs (qpf.repr x) = x
- abs_map : ∀ {α β : Type ?} (f : α → β) (p : (qpf.P F).obj α), qpf.abs (f <$> p) = f <$> qpf.abs p
Quotients of polynomial functors.
Roughly speaking, saying that F is a quotient of a polynomial functor means that for each α,
elements of F α are represented by pairs ⟨a, f⟩, where a is the shape of the object and
f indexes the relevant elements of α, in a suitably natural manner.
- ind : ∀ {F : Type u → Type u} [_inst_1 : functor F] [q : qpf F] (a : (qpf.P F).A) (f f' : (qpf.P F).B a → (qpf.P F).W), (∀ (x : (qpf.P F).B a), qpf.Wequiv (f x) (f' x)) → qpf.Wequiv (W.mk a f) (W.mk a f')
- abs : ∀ {F : Type u → Type u} [_inst_1 : functor F] [q : qpf F] (a : (qpf.P F).A) (f : (qpf.P F).B a → (qpf.P F).W) (a' : (qpf.P F).A) (f' : (qpf.P F).B a' → (qpf.P F).W), qpf.abs ⟨a, f⟩ = qpf.abs ⟨a', f'⟩ → qpf.Wequiv (W.mk a f) (W.mk a' f')
- trans : ∀ {F : Type u → Type u} [_inst_1 : functor F] [q : qpf F] (u v w : (qpf.P F).W), qpf.Wequiv u v → qpf.Wequiv v w → qpf.Wequiv u w
two trees are equivalent if their F-abstractions are
recF is insensitive to the representation
Define the fixed point as the quotient of trees under the equivalence relation Wequiv.
Equations
- qpf.W_setoid = {r := qpf.Wequiv q, iseqv := _}
recursor of a type defined by a qpf
Equations
- qpf.fix.rec g = quot.lift (qpf.recF g) _
access the underlying W-type of a fixpoint data type
Equations
- qpf.fix_to_W = quotient.lift qpf.Wrepr qpf.fix_to_W._proof_1
constructor of a type defined by a qpf
Equations
- qpf.fix.mk x = quot.mk setoid.r (pfunctor.W.mk (qpf.fix_to_W <$> qpf.repr x))
destructor of a type defined by a qpf
Equations
does recursion on q.P.M using g : α → F α rather than g : α → P α
Equations
- qpf.corecF g = pfunctor.M.corec (λ (x : α), qpf.repr (g x))
A pre-congruence on q.P.M viewed as an F-coalgebra. Not necessarily symmetric.
coinductive type defined as the final coalgebra of a qpf
Equations
- qpf.cofix F = quot qpf.Mcongr
Equations
- qpf.inhabited = {default := quot.mk qpf.Mcongr (inhabited.default (qpf.P F).M)}
corecursor for type defined by cofix
Equations
- qpf.cofix.corec g x = quot.mk qpf.Mcongr (qpf.corecF g x)
destructor for type defined by cofix
Equations
- qpf.cofix.dest = quot.lift (λ (x : (qpf.P F).M), quot.mk qpf.Mcongr <$> qpf.abs x.dest) qpf.cofix.dest._proof_1
composition of qpfs gives another qpf
Equations
- qpf.comp = {P := (qpf.P F₂).comp (qpf.P F₁), abs := λ (α : Type u), id (λ (p : ((qpf.P F₂).comp (qpf.P F₁)).obj α), qpf.abs ⟨p.fst.fst, λ (x : (qpf.P F₂).B p.fst.fst), qpf.abs ⟨p.fst.snd x, λ (y : (qpf.P F₁).B (p.fst.snd x)), p.snd ⟨x, y⟩⟩⟩), repr := λ (α : Type u), id (λ (y : F₂ (F₁ α)), ⟨⟨(qpf.repr y).fst, λ (u : (qpf.P F₂).B (qpf.repr y).fst), (qpf.repr ((qpf.repr y).snd u)).fst⟩, id (λ (x : Σ (u : (qpf.P F₂).B (qpf.repr y).fst), (qpf.P F₁).B (qpf.repr ((qpf.repr y).snd u)).fst), (qpf.repr ((qpf.repr y).snd x.fst)).snd x.snd)⟩), abs_repr := _, abs_map := _}
Given a qpf F and a well-behaved surjection FG_abs from F α to
functor G α, G is a qpf. We can consider G a quotient on F where
elements x y : F α are in the same equivalence class if
FG_abs x = FG_abs y
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 = ∀ ⦃α : Type u⦄ (p : α → Prop) (x : (qpf.P F).obj α), functor.liftp p (qpf.abs x) ↔ functor.liftp p x
does abs preserve supp?
Equations
- q.supp_preservation = ∀ ⦃α : Type u⦄ (x : (qpf.P F).obj α), functor.supp (qpf.abs x) = functor.supp x