The M construction as a multivariate polynomial functor. #
M types are potentially infinite tree-like structures. They are defined as the greatest fixpoint of a polynomial functor.
Main definitions #
M.mk
- constructorM.dest
- destructorM.corec
- corecursor: useful for formulating infinite, productive computationsM.bisim
- bisimulation: proof technique to show the equality of infinite objects
Implementation notes #
Dual view of M-types:
Mp
: polynomial functorM
: greatest fixed point of a polynomial functor
Specifically, we define the polynomial functor Mp
as:
- A := a possibly infinite tree-like structure without information in the nodes
- B := given the tree-like structure
t
,B t
is a valid path from the root oft
to any given node.
As a result Mp.obj α
is made of a dataless tree and a function from
its valid paths to values of α
The difference with the polynomial functor of an initial algebra is
that A
is a possibly infinite tree.
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)} → (x : PFunctor.M (MvPFunctor.last P)) → (a : P.A) → (f : PFunctor.B (MvPFunctor.last P) a → PFunctor.M (MvPFunctor.last P)) → PFunctor.M.dest x = { fst := a, snd := f } → (i : Fin2 n) → MvPFunctor.B (MvPFunctor.drop P) a i → MvPFunctor.M.Path P x i
- child: {n : ℕ} → {P : MvPFunctor (n + 1)} → (x : PFunctor.M (MvPFunctor.last P)) → (a : P.A) → (f : PFunctor.B (MvPFunctor.last P) a → PFunctor.M (MvPFunctor.last P)) → PFunctor.M.dest x = { fst := a, snd := f } → (j : PFunctor.B (MvPFunctor.last P) a) → (i : Fin2 n) → MvPFunctor.M.Path P (f j) i → MvPFunctor.M.Path P x i
A path from the root of a tree to one of its node
Instances For
Polynomial functor of the M-type of P
. A
is a data-less
possibly infinite tree whereas, for a given a : A
, B a
is a valid
path in tree a
so that mp.Obj α
is made of a tree and a function
from its valid paths to the values it contains
Instances For
n
-ary M-type for P
Instances For
construct through corecursion the shape of an M-type without its contents
Instances For
Proof of type equality as an arrow
Instances For
Proof of type equality as a function
Instances For
Using corecursion, construct the contents of an M-type
Equations
- One or more equations did not get rendered due to their size.
- MvPFunctor.M.corecContents P g₀ g₁ g₂ x b h x (MvPFunctor.M.Path.root x a f h' x c) = let_fun this := (_ : a = g₀ b); g₁ b x (MvPFunctor.castDropB P this x c)
Instances For
Corecursor for M-type of P
Instances For
Corecursor for M-type of P
Instances For
Implementation of destructor for M-type of P
Instances For
Implementation of destructor for M-type of P
Instances For
Destructor for M-type of P
Instances For
Destructor for M-types
Instances For
Constructor for M-types