The W construction as a multivariate polynomial functor. #
W types are well-founded tree-like structures. They are defined as the least fixpoint of a polynomial functor.
Main definitions #
W_mk
- constructor- `W_dest - destructor
W_rec
- recursor: basis for defining functions by structural recursion onP.W α
W_rec_eq
- defining equation forW_rec
W_ind
- induction principle forP.W α
Implementation notes #
Three views of M-types:
wp
: polynomial functorW
: data type inductively defined by a triple: shape of the root, data in the root and children of the rootW
: least fixed point of a polynomial functor
Specifically, we define the polynomial functor wp
as:
- A := a tree-like structure without information in the nodes
- B := given the tree-like structure
t
,B t
is a valid path (specified inductively byW_path
) from the root oft
to any given node.
As a result wp.Obj α
is made of a dataless tree and a function from
its valid paths to values of α
Reference #
- Jeremy Avigad, Mario M. Carneiro and Simon Hudon. [Data Types as Quotients of Polynomial Functors][avigad-carneiro-hudon2019]
- root: {n : ℕ} → {P : MvPFunctor (n + 1)} → (a : P.A) → (f : PFunctor.B (MvPFunctor.last P) a → PFunctor.W (MvPFunctor.last P)) → (i : Fin2 n) → MvPFunctor.B (MvPFunctor.drop P) a i → MvPFunctor.WPath P (WType.mk a f) i
- child: {n : ℕ} → {P : MvPFunctor (n + 1)} → (a : P.A) → (f : PFunctor.B (MvPFunctor.last P) a → PFunctor.W (MvPFunctor.last P)) → (i : Fin2 n) → (j : PFunctor.B (MvPFunctor.last P) a) → MvPFunctor.WPath P (f j) i → MvPFunctor.WPath P (WType.mk a f) i
A path from the root of a tree to one of its node
Instances For
Specialized destructor on WPath
Instances For
Specialized destructor on WPath
Instances For
Specialized destructor on WPath
Instances For
Polynomial functor for the W-type of P
. A
is a data-less well-founded
tree whereas, for a given a : A
, B a
is a valid path in tree a
so
that Wp.obj α
is made of a tree and a function from its valid paths to
the values it contains
Instances For
W-type of P
Instances For
First, describe operations on W
as a polynomial functor.
Constructor for wp
Instances For
Equations
- MvPFunctor.wpRec P g (WType.mk a f) f' = g a f f' fun i => MvPFunctor.wpRec P g (f i) (MvPFunctor.wPathDestRight P f' i)
Instances For
Now think of W as defined inductively by the data ⟨a, f', f⟩ where
a : P.A
is the shape of the top nodef' : P.drop.B a ⟹ α
is the contents of the top nodef : P.last.B a → P.last.W
are the subtrees
Constructor for W
Instances For
Recursor for W
Instances For
Defining equation for the recursor of W
Induction principle for W
W-types are functorial
Instances For
Constructor of a value of P.obj (α ::: β)
from components.
Useful to avoid complicated type annotation
Instances For
Yet another view of the W type: as a fixed point for a multivariate polynomial functor.
These are needed to use the W-construction to construct a fixed point of a qpf, since
the qpf axioms are expressed in terms of map
on P
.
Constructor for the W-type of P
Instances For
Destructor for the W-type of P