Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: How to understand this structure in Category Theory?

Davi Sales Barreira (Jul 14 2023 at 13:42):

In Functional Programming, I've see tree structures defined as the following:

data Tree a t = Leaf a | Empty | Compose (Tree t a) (Tree t a) | Application t Tree (t a)

This structure is recursive up to the leafs, which is where every tree must end... I'm trying to understand what this structure is in Category Theory. Fixing a t, my hypothesis was that this data structure was to be interpreted as the initial algebra for a functor
$F_t a := a + 1 + a \times a + a$. But I'm not sure if this is the case.

How can I interpret this types of "expression" constructions within Category Theory?

Chris Grossack (they/them) (Jul 14 2023 at 14:19):

Do you mean for the order of t and a to switch between the data definition and the clauses?

Chris Grossack (they/them) (Jul 14 2023 at 14:22):

And do you want your last clause to be Application t (Tree t a)?

Jencel Panic (Jul 14 2023 at 19:16):

In general, every generic type is an endofunctor, provided that it has some implementation of map (if it doesn't it is not anything categorically, I think). Then it can be also an applicative, monad etc.

Mike Shulman (Jul 14 2023 at 20:12):

If you do want the order of arguments to stay the same and be present at all uses:

data Tree a t = Leaf a | Empty | Compose (Tree a t) (Tree a t) | Application t (Tree a t)

then Tree a t is the initial algebra of the endofunctor

$$F_{a,t}(x) = a + 1 + (x\times x) + t \times x.$$

The argument $x$ of the endofunctor corresponds to the recursive appearances of the type being defined in its own constructors; the other types $a,t$ are parameters that determine the functor.

Davi Sales Barreira (Jul 18 2023 at 14:39):

Thanks, @Mike Shulman . I've been digging through this, and I got to this conclusion. Good to see that what I was thinking was correct.

Davi Sales Barreira (Jul 18 2023 at 14:41):

I'm trying to implement the catamorphism for this strucutre. If I understood correctly, in the $$F_{a,t}$, the $a$ is actually a constant functor. I mean, $fmap(f, x::Leaf) = x$. Right?

Davi Sales Barreira (Jul 18 2023 at 14:43):

I mean, if a catamorphism is:

cata alg = alg . fmap (cata alg) . unFix

Then I need a base case for cata alg where fmap (cata alg) Leaf 10 is the fixed point... Hence, fmap (cata alg) Leaf 10 should return Leaf 10... Makes sense?

Mike Shulman (Jul 18 2023 at 16:07):

I don't quite understand your notation, but there is no recursion in the case for Leaf if that's what you mean.