<p>The question isn't totally clear but the existence of <em>any</em> <span class="math-container">$F$</span>-algebra certainly does not imply the existence of an initial <span class="math-container">$F$</span>-algebra. A concrete example would be the powerset functor on Set, which has no initial algebras by Cantor's theorem (because we would have <span class="math-container">$\mathcal P(X) \cong X$</span>) but you can easily make many algebras such as the unique map <span class="math-container">$\mathcal P(1) \to 1$</span>.</p>

CC BY-SA 4.0
2024-10-04T12:53:13.573Z
2024-10-04T12:53:13.573Z
Max New
<p>Proving a catamorphism exists amounts to showing that there is an initial F-algebra. I know there are some discussions about this, e.g. in the article on Functional Programming with Bananas, etc., but I'm confused by the fact the entire development proceeds from within some form of equational theory where endofunctors don't seem to fully satisfy the definition of categorical functors and no discussion is involved about how exactly recursion works (e.g. in the bananas article it is assumed to be well-defined in the metalanguage).</p>
<p>I ask about these because I'd be interested in trying to formalize the bananas article in Lean in such a way that I could use it for general programming.</p>

CC BY-SA 4.0
2024-10-04T05:55:43.650Z
Could anyone confirm, the articles presenting recursion schemes usually model maps between types as polynomial endofunctors in a cartesian closed category right? this might be enough to answer both questions affirmatively
shintuku
CC BY-SA 4.0
2024-10-07T08:39:17.573Z
If you only consider polynomial functors $F$ then their initial algebras are recursive polynomial data types (finite lists, finite trees, etc., - "finite" in the sense that any value of a `List` has a finite number of values even though there is no a priori bound on the length of a list). I think most of the time recursion schemes are used for polynomial data types. One can define the initial F-algebra via the Church encoding $\forall R. ~(F ~R \to R)\to R$ and then one can prove that for any $F$-algebra there exists a catamorphism, and write its code explicitly.
winitzki
<type-theory><ct.category-theory><recursion><monad>
Given endofunctor F over an inductive type and a non-initial F-algebra can we prove a catamorphism exists, and can it be automatically computed?
shintuku
# Given endofunctor F over an inductive type and a non-initial F-algebra can we prove a catamorphism exists, and can it be automatically computed?

(Asked by: username_0 on 2024-10-04)

Proving a catamorphism exists amounts to showing that there is an initial F-algebra. I know there are some discussions about this, e.g. in the article on Functional Programming with Bananas, etc., but I'm confused by the fact the entire development proceeds from within some form of equational theory where endofunctors don't seem to fully satisfy the definition of categorical functors and no discussion is involved about how exactly recursion works (e.g. in the bananas article it is assumed to be well-defined in the metalanguage).

I ask about these because I'd be interested in trying to formalize the bananas article in Lean in such a way that I could use it for general programming.

**Tags:** type-theory, ct.category-theory, recursion, monad

> **Comments:**
> **username_0**: Could anyone confirm, the articles presenting recursion schemes usually model maps between types as polynomial endofunctors in a cartesian closed category right? this might be enough to answer both questions affirmatively  
> **username_1**: If you only consider polynomial functors $F$ then their initial algebras are recursive polynomial data types (finite lists, finite trees, etc., - "finite" in the sense that any value of a `List` has a finite number of values even though there is no a priori bound on the length of a list). I think most of the time recursion schemes are used for polynomial data types. One can define the initial F-algebra via the Church encoding $\forall R. ~(F ~R \to R)\to R$ and then one can prove that for any $F$-algebra there exists a catamorphism, and write its code explicitly.  

---

## 1 answers

### Answer by username_2 on 2024-10-04. Score: 2 | Accepted answer

The question isn't totally clear but the existence of *any* $F$-algebra certainly does not imply the existence of an initial $F$-algebra. A concrete example would be the powerset functor on Set, which has no initial algebras by Cantor's theorem (because we would have $\mathcal P(X) \cong X$) but you can easily make many algebras such as the unique map $\mathcal P(1) \to 1$.


---

