how to represent (co)free (co)monads on polynomial functors

Stream: lean4

[André Muricy Santos]

Hi all, I'm following this paper and I'd like to run the examples at the end, so I'm taking a stab at implementing free monads and cofree comonads. I'm using the code here for polynomial functors, but the gist of it is this: polynomial functors are sigma types:

structure Poly where
  pos : Type u
  dir : pos -> Type v

and the free monad is defined for all natural numbers and limit ordinals.
Skärmavbild-2024-07-26-kl.-22.43.28.png

I'm stuck on all avenues I tried to implement this.

First I don't know how to represent limit ordinals or how to pattern match on them, or to get the cardinality of the direction sets (the target types of the field dir), which stops me here:

-- Free monad
def p_aux (n : ℕ) (p : Poly) : Poly := match n with
  | 0 => y
  | Nat.succ n  => y + p ◁ (p_aux n p)
--| ω => colim (a' < a) p -- I could figure out how to compute limits of p as a functor later
def l (n : ℕ) (p : Poly) : (p_aux n p) ⟶ (p_aux (1 + n) p) := match n with
  | 0 => {onPos := λ p ↦ .inl p , onDir := λ _ _ ↦ ()} -- y ⟶ y + p
  | Nat.succ n => coproduct.whiskerLeft (subst.whiskerLeft (l n p))   -- y + p ◁ (p_aux n p) ⟶ y + p ◁ (p_aux (1 + n) p)
--| ω =>  forall a < ω, this is the "natural inclusion" -- no idea how to do thhis

-- Remark A.2. A polynomial  : Poly is κ-small if and only if all of its direction-sets have cardinality
-- less than κ. It is called finitary if and only if it is ω-small.
-- Here I could _assume_ that p is finitary, i.e. all its direction sets are finite, but then
-- how do I "iterate" over all positions to get their cardinality?
def smallness (p : Poly) : ℕ := 10

def freeMonad (p : Poly) : Poly := p_aux (smallness p) p

The same goes for the cofree comonad.

Second, I tried to do it in a naïve way, which is just writing down their recursive expressions, which would require the partial keyword:

partial def free2 (p : Poly) : Poly := y + free2 p

But this complains that

failed to compile partial definition 'CategoryTheory.Poly.free2', failed to show that type is inhabited and non empty

Which is fair enough, because we'd be able to prove False otherwise. But which type needs the instance [Inhabited]? I've tried giving it to p, Poly, y, basically everything that is mentioned in the body:

partial def free2 [inst : Inhabited p] [inst2 : Inhabited Poly] [inst3 : Inhabited y] (p : Poly) : Poly :=
   y + free2 (inst := inst)  p

but nothing works.

Third, I tried to copy this solution on my question in stackoverflow, but I'd need the inductive definition to produce a Poly, not a Type, so that doesn't help me.

inductive Free (f : Poly) (α : Type) where -- Free p should be of type Poly, not Type -> Type
  | pure : α → Free f α
  | free : ∀ x, applyFunctor f x -> (x -> Free f α) → Free f α -- applyFunctor : Poly -> Type -> Type

Help please?

[André Muricy Santos]

(deleted)

[Malcolm Langfield]

Feel free to correct me if I am wrong, but I believe it is the return type of a partial function which needs to be inhabited, hence the error message you're seeing. If I had to guess at a solution, perhaps try actually writing an instance for Poly instead of just adding it as a parameter?

[André Muricy Santos]

I actually fixed the compilation error by writing a different expression on the body of free2 which is just as recursive, but Lean won't reduce a partial expression no matter what it seems, so I can never pattern match on a value of this type :(

[Malcolm Langfield]

Yes, also you'll never be able to unfold such a definition, which makes it somewhat useless for reasoning :woman_shrugging: