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 - constructor
• M.dest - destructor
• M.corec - corecursor: useful for formulating infinite, productive computations
• M.bisim - bisimulation: proof technique to show the equality of infinite objects

Implementation notes

Dual view of M-types:

• mp: polynomial functor
• M: 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 of t to any given node.

As a result mp α 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]

inductive MvPFunctor.M.Path {n : ℕ} (P : MvPFunctor.{u} (n + 1)) : PFunctor.M (MvPFunctor.last P) → Fin2 n → Type u

A path from the root of a tree to one of its node

• root: {n : ℕ} → {P : MvPFunctor.{u} (n + 1)} → (x : PFunctor.M (MvPFunctor.last P)) → (a : P.A) → (f : (MvPFunctor.last P).B a → PFunctor.M (MvPFunctor.last P)) → PFunctor.M.dest x = { fst := a, snd := f } → (i : Fin2 n) → (MvPFunctor.drop P).B a i → MvPFunctor.M.Path P x i
• child: {n : ℕ} → {P : MvPFunctor.{u} (n + 1)} → (x : PFunctor.M (MvPFunctor.last P)) → (a : P.A) → (f : (MvPFunctor.last P).B a → PFunctor.M (MvPFunctor.last P)) → PFunctor.M.dest x = { fst := a, snd := f } → (j : (MvPFunctor.last P).B a) → (i : Fin2 n) → MvPFunctor.M.Path P (f j) i → MvPFunctor.M.Path P x i

instance MvPFunctor.M.Path.inhabited {n : ℕ} (P : MvPFunctor.{u} (n + 1)) (x : PFunctor.M (MvPFunctor.last P)) {i : Fin2 n} [Inhabited ((MvPFunctor.drop P).B (PFunctor.M.head x) i)] : Inhabited (MvPFunctor.M.Path P x i)

Equations

• MvPFunctor.M.Path.inhabited P x = let a := PFunctor.M.head x; let f := PFunctor.M.children x; { default := MvPFunctor.M.Path.root x a f ⋯ i default }

def MvPFunctor.mp {n : ℕ} (P : MvPFunctor.{u} (n + 1)) : MvPFunctor.{u} n

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 α is made of a tree and a function from its valid paths to the values it contains

Equations

• MvPFunctor.mp P = { A := PFunctor.M (MvPFunctor.last P), B := MvPFunctor.M.Path P }

def MvPFunctor.M {n : ℕ} (P : MvPFunctor.{u} (n + 1)) (α : TypeVec.{u} n) : Type u

n-ary M-type for P

Equations

• MvPFunctor.M P α = ↑(MvPFunctor.mp P) α

instance MvPFunctor.mvfunctorM {n : ℕ} (P : MvPFunctor.{u} (n + 1)) : MvFunctor (MvPFunctor.M P)

Equations

• MvPFunctor.mvfunctorM P = id inferInstance

instance MvPFunctor.inhabitedM {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} [I : Inhabited P.A] [(i : Fin2 n) → Inhabited (α i)] : Inhabited (MvPFunctor.M P α)

Equations

• MvPFunctor.inhabitedM P = MvPFunctor.Obj.inhabited (MvPFunctor.mp P)

def MvPFunctor.M.corecShape {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {β : Type u} (g₀ : β → P.A) (g₂ : (b : β) → (MvPFunctor.last P).B (g₀ b) → β) : β → PFunctor.M (MvPFunctor.last P)

construct through corecursion the shape of an M-type without its contents

Equations

• MvPFunctor.M.corecShape P g₀ g₂ = PFunctor.M.corec fun (b : β) => { fst := g₀ b, snd := g₂ b }

def MvPFunctor.castDropB {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {a : P.A} {a' : P.A} (h : a = a') : TypeVec.Arrow ((MvPFunctor.drop P).B a) ((MvPFunctor.drop P).B a')

Proof of type equality as an arrow

Equations

• MvPFunctor.castDropB P h _i b = Eq.recOn h b

def MvPFunctor.castLastB {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {a : P.A} {a' : P.A} (h : a = a') : (MvPFunctor.last P).B a → (MvPFunctor.last P).B a'

Proof of type equality as a function

Equations

• MvPFunctor.castLastB P h b = Eq.recOn h b

def MvPFunctor.M.corecContents {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (g₀ : β → P.A) (g₁ : (b : β) → TypeVec.Arrow ((MvPFunctor.drop P).B (g₀ b)) α) (g₂ : (b : β) → (MvPFunctor.last P).B (g₀ b) → β) (x : PFunctor.M (MvPFunctor.last P)) (b : β) (h : x = MvPFunctor.M.corecShape P g₀ g₂ b) : TypeVec.Arrow (MvPFunctor.M.Path P x) α

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 := ⋯; g₁ b x (MvPFunctor.castDropB P this x c)

def MvPFunctor.M.corec' {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (g₀ : β → P.A) (g₁ : (b : β) → TypeVec.Arrow ((MvPFunctor.drop P).B (g₀ b)) α) (g₂ : (b : β) → (MvPFunctor.last P).B (g₀ b) → β) : β → MvPFunctor.M P α

Corecursor for M-type of P

Equations

• MvPFunctor.M.corec' P g₀ g₁ g₂ b = { fst := MvPFunctor.M.corecShape P g₀ g₂ b, snd := MvPFunctor.M.corecContents P g₀ g₁ g₂ (MvPFunctor.M.corecShape P g₀ g₂ b) b ⋯ }

def MvPFunctor.M.corec {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (g : β → ↑P (α ::: β)) : β → MvPFunctor.M P α

Corecursor for M-type of P

Equations

• MvPFunctor.M.corec P g = MvPFunctor.M.corec' P (fun (b : β) => (g b).fst) (fun (b : β) => TypeVec.dropFun (g b).snd) fun (b : β) => TypeVec.lastFun (g b).snd

def MvPFunctor.M.pathDestLeft {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {x : PFunctor.M (MvPFunctor.last P)} {a : P.A} {f : (MvPFunctor.last P).B a → PFunctor.M (MvPFunctor.last P)} (h : PFunctor.M.dest x = { fst := a, snd := f }) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) : TypeVec.Arrow ((MvPFunctor.drop P).B a) α

Implementation of destructor for M-type of P

Equations

• MvPFunctor.M.pathDestLeft P h f' i c = f' i (MvPFunctor.M.Path.root x a f h i c)

def MvPFunctor.M.pathDestRight {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {x : PFunctor.M (MvPFunctor.last P)} {a : P.A} {f : (MvPFunctor.last P).B a → PFunctor.M (MvPFunctor.last P)} (h : PFunctor.M.dest x = { fst := a, snd := f }) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) (j : (MvPFunctor.last P).B a) : TypeVec.Arrow (MvPFunctor.M.Path P (f j)) α

Implementation of destructor for M-type of P

Equations

• MvPFunctor.M.pathDestRight P h f' j i c = f' i (MvPFunctor.M.Path.child x a f h j i c)

def MvPFunctor.M.dest' {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {x : PFunctor.M (MvPFunctor.last P)} {a : P.A} {f : (MvPFunctor.last P).B a → PFunctor.M (MvPFunctor.last P)} (h : PFunctor.M.dest x = { fst := a, snd := f }) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) : ↑P (α ::: MvPFunctor.M P α)

Destructor for M-type of P

Equations

• One or more equations did not get rendered due to their size.

def MvPFunctor.M.dest {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (x : MvPFunctor.M P α) : ↑P (α ::: MvPFunctor.M P α)

Destructor for M-types

Equations

• MvPFunctor.M.dest P x = MvPFunctor.M.dest' P ⋯ x.snd

def MvPFunctor.M.mk {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} : ↑P (α ::: MvPFunctor.M P α) → MvPFunctor.M P α

Constructor for M-types

Equations

• MvPFunctor.M.mk P = MvPFunctor.M.corec P fun (i : ↑P (α ::: MvPFunctor.M P α)) => MvFunctor.map (TypeVec.id ::: MvPFunctor.M.dest P) i

theorem MvPFunctor.M.dest'_eq_dest' {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {x : PFunctor.M (MvPFunctor.last P)} {a₁ : P.A} {f₁ : (MvPFunctor.last P).B a₁ → PFunctor.M (MvPFunctor.last P)} (h₁ : PFunctor.M.dest x = { fst := a₁, snd := f₁ }) {a₂ : P.A} {f₂ : (MvPFunctor.last P).B a₂ → PFunctor.M (MvPFunctor.last P)} (h₂ : PFunctor.M.dest x = { fst := a₂, snd := f₂ }) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) : MvPFunctor.M.dest' P h₁ f' = MvPFunctor.M.dest' P h₂ f'

theorem MvPFunctor.M.dest_eq_dest' {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {x : PFunctor.M (MvPFunctor.last P)} {a : P.A} {f : (MvPFunctor.last P).B a → PFunctor.M (MvPFunctor.last P)} (h : PFunctor.M.dest x = { fst := a, snd := f }) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) : MvPFunctor.M.dest P { fst := x, snd := f' } = MvPFunctor.M.dest' P h f'

theorem MvPFunctor.M.dest_corec' {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (g₀ : β → P.A) (g₁ : (b : β) → TypeVec.Arrow ((MvPFunctor.drop P).B (g₀ b)) α) (g₂ : (b : β) → (MvPFunctor.last P).B (g₀ b) → β) (x : β) : MvPFunctor.M.dest P (MvPFunctor.M.corec' P g₀ g₁ g₂ x) = { fst := g₀ x, snd := TypeVec.splitFun (g₁ x) (MvPFunctor.M.corec' P g₀ g₁ g₂ ∘ g₂ x) }

theorem MvPFunctor.M.dest_corec {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (g : β → ↑P (α ::: β)) (x : β) : MvPFunctor.M.dest P (MvPFunctor.M.corec P g x) = MvFunctor.map (TypeVec.id ::: MvPFunctor.M.corec P g) (g x)

theorem MvPFunctor.M.bisim_lemma {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {a₁ : (MvPFunctor.mp P).A} {f₁ : TypeVec.Arrow ((MvPFunctor.mp P).B a₁) α} {a' : P.A} {f' : TypeVec.Arrow (TypeVec.drop (P.B a')) α} {f₁' : TypeVec.last (P.B a') → MvPFunctor.M P α} (e₁ : MvPFunctor.M.dest P { fst := a₁, snd := f₁ } = { fst := a', snd := TypeVec.splitFun f' f₁' }) : ∃ (g₁' : (MvPFunctor.last P).B a' → PFunctor.M (MvPFunctor.last P)) (e₁' : PFunctor.M.dest a₁ = { fst := a', snd := g₁' }), f' = MvPFunctor.M.pathDestLeft P e₁' f₁ ∧ f₁' = fun (x : (MvPFunctor.last P).B a') => { fst := g₁' x, snd := MvPFunctor.M.pathDestRight P e₁' f₁ x }

theorem MvPFunctor.M.bisim {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (R : MvPFunctor.M P α → MvPFunctor.M P α → Prop) (h : ∀ (x y : MvPFunctor.M P α), R x y → ∃ (a : P.A) (f : TypeVec.Arrow (TypeVec.drop (P.B a)) (TypeVec.drop (α ::: MvPFunctor.M P α))) (f₁ : TypeVec.last (P.B a) → TypeVec.last (α ::: MvPFunctor.M P α)) (f₂ : TypeVec.last (P.B a) → TypeVec.last (α ::: MvPFunctor.M P α)), MvPFunctor.M.dest P x = { fst := a, snd := TypeVec.splitFun f f₁ } ∧ MvPFunctor.M.dest P y = { fst := a, snd := TypeVec.splitFun f f₂ } ∧ ∀ (i : TypeVec.last (P.B a)), R (f₁ i) (f₂ i)) (x : MvPFunctor.M P α) (y : MvPFunctor.M P α) (r : R x y) : x = y

theorem MvPFunctor.M.bisim₀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (R : MvPFunctor.M P α → MvPFunctor.M P α → Prop) (h₀ : Equivalence R) (h : ∀ (x y : MvPFunctor.M P α), R x y → MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P x) = MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P y)) (x : MvPFunctor.M P α) (y : MvPFunctor.M P α) (r : R x y) : x = y

theorem MvPFunctor.M.bisim' {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (R : MvPFunctor.M P α → MvPFunctor.M P α → Prop) (h : ∀ (x y : MvPFunctor.M P α), R x y → MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P x) = MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P y)) (x : MvPFunctor.M P α) (y : MvPFunctor.M P α) (r : R x y) : x = y

theorem MvPFunctor.M.dest_map {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : TypeVec.Arrow α β) (x : MvPFunctor.M P α) : MvPFunctor.M.dest P (MvFunctor.map g x) = MvFunctor.map (g ::: fun (x : MvPFunctor.M P α) => MvFunctor.map g x) (MvPFunctor.M.dest P x)

theorem MvPFunctor.M.map_dest {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : TypeVec.Arrow (α ::: MvPFunctor.M P α) (β ::: MvPFunctor.M P β)) (x : MvPFunctor.M P α) (h : ∀ (x : MvPFunctor.M P α), TypeVec.lastFun g x = MvFunctor.map (TypeVec.dropFun g) x) : MvFunctor.map g (MvPFunctor.M.dest P x) = MvPFunctor.M.dest P (MvFunctor.map (TypeVec.dropFun g) x)