Proper way to define an algebra for a catamorphism?

Stream: lean4

[nrs]

inductive Algebra [Functor f] (f : Type -> Type) (α : Type)
  | mk : f α -> α -> Algebra f α

inductive Mu (f : Type → Type)  where
  | mkMu : {α : Type} → (f α → α) → Mu f

def cata [Functor f] {α : Type} : Algebra f α -> Mu f -> α  := sorry

Attempting to define an algebra as above produces the error "typeclass instance problem is stuck", but it typechecks if I omit enforcing that f be a functor. Should I omit this constraint or is there a way to fix typeclass resolution for such an algebra?

[Jannis Limperg]

Remove the [Functor f] from the type signature of Algebra. It's unused anyway.

[nrs]

Jannis Limperg said:

Remove the [Functor f] from the type signature of Algebra. It's unused anyway.

Thank you for the feedback!

[Tom]

Even though there is value in constraining f, right?

I would suggest moving [Functor f] after the definition of f, like this:

inductive Algebra (f : Type -> Type) [Functor f] (α : Type)

[Tom]

Try hovering over "both f's" in the before and after case: You will see that in your original code, the Functor f is is Type u_1 -> Type u_2 and then your f: ... introduces a type variable. Hence why the metavariables cannot be resolved.

[Tom]

I have recently asked about this in two related guises: Here.

I think the reason why this happens is related to the following (I still claim :smile: ) counterintuitive behavior: Here

[Tom]

You could have avoided this issue by setting set_option autoImplicit false, btw. I now just paste it above my code to just check my implicits are "what I think they are".

[Tom]

Btw, cool project. I was just recently thinking if I could practice some metaprogramming and get lean to generate the "algebra carriers" automatically.

[nrs]

Tom said:

Btw, cool project. I was just recently thinking if I could practice some metaprogramming and get lean to generate the "algebra carriers" automatically.

Thanks for the comments! I will be mulling these over. If you're working on something similar absolutely tag me if you make progress! Will do likewise

[nrs]

Tom said:

set_option autoImplicit false

woah I've been playing around with set_option autoImplicit false and it's extremely helpful! thanks a lot for that tip

[Tom]

Just passing on what others told me :smile:

[nrs]

Tom said:

Even though there is value in constraining f, right?

I would suggest moving [Functor f] after the definition of f, like this:

inductive Algebra (f : Type -> Type) [Functor f] (α : Type)

a thought about this: if Lean's -> corresponds to a polynomial endofunctor in a locally cartesian closed category, it may actually be accurate to use it simply so without any additional constraint, since the articles presenting recursion schemes seem to be reasoning in that category

[DSB]

@nrs did you get the catamorphism to work?

[DSB]

It seems that I'm trying to do something similar to you. I'm trying to translate some of the Category Theory concepts applied to Programming from Bartosz book.

[nrs]

I was just working on this, I haven't tested it extensively but I think it might be a start:

structure P where
  α : Type _
  β : α -> Type _


def sum : P -> P -> P
| ⟨a, b⟩, ⟨aa, bb⟩ => ⟨a ⊕ aa, Sum.elim b bb⟩


structure Ext (F : P) (T : Type _) where
  a : F.α
  f : F.β a -> T

def Ext.map (f : T -> TA) : Ext F T -> Ext F TA
| ⟨a, g⟩ => ⟨a, f ∘ g⟩

inductive W (F : P)
| sup : Ext F (W F) -> W F

def Alg (F : P) (T : Type _) := Ext F T -> T

def Alg.comp : Alg F T -> Alg G T -> Alg (sum F G) T
| alga, algb => fun | ⟨a, f⟩ => match a with
  | .inl val => alga ⟨val, f⟩
  | .inr val => algb ⟨val, f⟩

def cata (alg : Alg F T) : W F -> T
| ⟨a, f⟩ => alg ⟨a, fun e => cata alg (f e)⟩

def ListP {X : Type} : P := ⟨Unit ⊕ X, fun | .inl _ => Empty | .inr _ => Unit⟩

def TreeP {X : Type} : P := ⟨Unit ⊕ X, fun | .inl _ => Empty | .inr _ => Unit ⊕ Unit⟩

def ListWtoTreeWR {X : Type} : Alg (@ListP X) (W (@TreeP X)) :=
  fun | ⟨a, g⟩ => match a with
    | .inl _ => ⟨.inl .unit, fun e => nomatch e⟩
    | .inr val => ⟨.inr val, fun e => match e with
      | .inl _ => ⟨.inl .unit, fun e => nomatch e⟩
      | .inr _ => g .unit⟩

[nrs]

it requires using the w-type form of the inductive type however

[DSB]

Hmm, I'm not aware of w-types. First type I hear about it. Is there a reason for not wanting to model it using this?

[nrs]

it might not be possible otherwise, the main issue is that haskell can evaluate type-level fixpoints while this is not possible in lean due to it being eagerly evaluated

[DSB]

Yeah, I was having trouble trying to figure out how to define the fixed point type.

[DSB]

I see that in your code you use W F where one would have Fix F. Right?

[nrs]

in the above W (which is the type of w-types) is the fixed point type used to make the cata work

[nrs]

yeah that's right

[nrs]

the theoretical statement at play here is that W is the "least fixed point", or the initial algebra, of a given polynomial functor

[DSB]

Yeah, I imagine that the issue with Fix F is that it is not guaranteed to exist.

[DSB]

Hence, since Lean requires termination, it would not be allowed.

[DSB]

Yet, if F is polynomial, it is guaranteed to exists...

[nrs]

i think however that there's a Fix type in mathlib, and a computable Fix type somewhere in either Batteries, or Std. might be worth checking if they have any use here

[nrs]

DSB said:

Yet, if F is polynomial, it is guaranteed to exists...

yes another issue you might encounter is that in haskell inductive and coinductive types coincide, so the greatest and least fixed points coincide, which is not the case in lean. here our least fixed point generates an inductive type

[DSB]

I'm veeery new to Lean. I'm trying to adapt some of the functional (categorical) stuff as I learn.

[nrs]

polynomial functors and w-types are good search terms to figure out how to adapt haskell fp to lean, the libraries for these are still very new

[Edward van de Meent]

as a side note, a "general" Fix type is not consistent, see this issue

[DSB]

I can understand the idea behind the fixed point Fix, and how in mathematics a fixed point does not always exist, hence why Lean would not allow such naive implementation.

I'm intrigued by this W though.

[DSB]

I mean, what is it doing so that one could use it instead of Fix?

[DSB]

nrs said:

polynomial functors and w-types are good search terms to figure out how to adapt haskell fp to lean, the libraries for these are still very new

Thanks, I'll try to take a look.