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 u} → PFunctor.Obj (Qpf.P F) α → F α
- repr : {α : Type u} → F α → PFunctor.Obj (Qpf.P F) α
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.
Instances
- ind: ∀ {F : Type u → Type u} [inst : Functor F] [q : Qpf F] (a : (Qpf.P F).A) (f f' : PFunctor.B (Qpf.P F) a → PFunctor.W (Qpf.P F)), (∀ (x : PFunctor.B (Qpf.P F) a), Qpf.Wequiv (f x) (f' x)) → Qpf.Wequiv (WType.mk a f) (WType.mk a f')
- abs: ∀ {F : Type u → Type u} [inst : Functor F] [q : Qpf F] (a : (Qpf.P F).A) (f : PFunctor.B (Qpf.P F) a → PFunctor.W (Qpf.P F)) (a' : (Qpf.P F).A) (f' : PFunctor.B (Qpf.P F) a' → PFunctor.W (Qpf.P F)), Qpf.abs { fst := a, snd := f } = Qpf.abs { fst := a', snd := f' } → Qpf.Wequiv (WType.mk a f) (WType.mk a' f')
- trans: ∀ {F : Type u → Type u} [inst : Functor F] [q : Qpf F] (u v w : PFunctor.W (Qpf.P F)), Qpf.Wequiv u v → Qpf.Wequiv v w → Qpf.Wequiv u w
two trees are equivalent if their F-abstractions are
Instances For
recF
is insensitive to the representation
maps every element of the W type to a canonical representative
Instances For
Define the fixed point as the quotient of trees under the equivalence relation Wequiv
.
Instances For
access the underlying W-type of a fixpoint data type
Instances For
does recursion on q.P.M
using g : α → F α
rather than g : α → P α
Instances For
A pre-congruence on q.P.M
viewed as an F-coalgebra. Not necessarily symmetric.
Instances For
The maximal congruence on q.P.M
.
Instances For
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
.