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: Expression, algebra and coalgebra

Davi Sales Barreira (Mar 16 2024 at 22:01):

In my PhD, I'm using category theory to interpret the code in a package I'm developing. It is more of a "soft interpretation", something that Dominc Orchard called "categorical programming".
As I was grappling with some functionalities in my code, I came up with the following triple:

$$expr: S \to T\\ alg: F T \to T\\ coalg: S \to FS$$

Where I compute:

$$alg \circ F expr \circ coalg$$

Does this construction have a name? Does it form a category?

Eric M Downes (Mar 16 2024 at 22:11):

Have you looked at Kleisli categories and monads?
From your functIon signatures, that comes to mind first.
https://youtu.be/i9CU4CuHADQ?si=bTgosVh--GBrkpn7
https://blog.ploeh.dk/2022/04/04/kleisli-composition/

I could recommend more resources if I know what language you're working in, or comfortable with.

(Also, does $\mathrm{expr}$ map from $S$ or $FS$? I can't tell if your composition is strict or implicitly Kleisli.)

Eric M Downes (Mar 16 2024 at 22:12):

Oh I see, you mean $F$ as a functor. Yes, definitely monads then

Davi Sales Barreira (Mar 16 2024 at 22:50):

I know monads, but I'm not seeing how this is a monad...

Davi Sales Barreira (Mar 16 2024 at 22:51):

Are the $alg$ and $coalg$ the $\mu$ and $\eta$? I can see how $coalg$ could be $\eta$, but not $alg$ be $\mu$, since $\mu: F\circ F \to F$...

Eric M Downes (Mar 16 2024 at 23:26):

The unit etc. are factored into coalg and $F$ already. That's fine! But if you want to make them explicit, you could.

$\mathrm{coalg}$ is built around a morphism (possibly the identity) in some (unidentified) category $\mathsf{C}$? So you are changing the output type to $FS$ instead of just $S$ and presumably using some kind of default / a priori function for type $F$?

Like, by default I mean, if you wanted to count internal loops: you'd pass 0:int, or error messages: a default Exception type, or handle NULL values: a nullary function that outputs the desired response in case a NULL is encountered. That "default value" is the unit and its implicit in your coalgebra.

The monad $F$ usually occurs "behind the scenes" in forming the Kleisli category $\mathsf{C}_F$; Bartosz' youtube video I linked has good concrete examples. Here's the geist:

Instead of handling the type $F$ explicitly in your code
$F\mathrm{expr}\circ\mathrm{coalg}: S\to FS\to FT$
you just write $expr:S\to T$ and $c:S\to S$, and then use the Kleisli category $\mathsf{C}_F$ built from the monad $F$ to handle composition
$\mathrm{expr}\circ_F c$

That's not just a formal trick. In a functional language like Scala etc. you'd declare $c$ to be Kleisli with $F$ and the compiler does all the work for you.

So in terms of identifying what you have... Kleisli morphism $\pm\epsilon$ is the closest I can get without more info.

Davi Sales Barreira (Mar 16 2024 at 23:32):

Thanks, @Eric M Downes .

Davi Sales Barreira (Mar 16 2024 at 23:33):

What about the $alg$? That is what has me thrown off. I mean, I can see how the Kleisli composition works for the coalg.

Davi Sales Barreira (Mar 16 2024 at 23:34):

In my code, the functor $F$ is just the list functor.

Eric M Downes (Mar 16 2024 at 23:36):

Perfect! List is a perfect example of a monad. The unit creates the empty list [] out of thin air.

And then, yes to get out of $\mathsf{C}_F$ back to your familiar $\mathsf{C}$ you use the counit to extract the value(s) from the list. Like you would pop the end, and then do something, and pop again, etc. That popping is the counit, which here is factored into $\mathrm{alg}$.

Eric M Downes (Mar 16 2024 at 23:38):

List is also a monoid, as "a monad is a ... " well you have probably heard the Haskell joke before? :)

Davi Sales Barreira (Mar 16 2024 at 23:39):

sure. a monad is a monoid in the functor category.

Davi Sales Barreira (Mar 16 2024 at 23:39):

I guess what I'm confused about is the fact that $\mu:F\circ F \to F$, while $alg:FT\to T$.

Davi Sales Barreira (Mar 16 2024 at 23:40):

They do sound very similar. But this distinction in the behavior of the $\mu$ and the $alg$ is what I'm not able to square off.

Davi Sales Barreira (Mar 16 2024 at 23:40):

Makes sense?

Davi Sales Barreira (Mar 16 2024 at 23:41):

If I'm not mistaken, the list monad has the $\mu$ that unwraps lists of lists into single lists.

Davi Sales Barreira (Mar 16 2024 at 23:42):

But in my situation, I just have a list (not a list of lists), which I then apply an algebra to it.

Eric M Downes (Mar 16 2024 at 23:42):

yep, endofunctor (e.g. functors from a cat to itself)

I think you mean $\mu:F\times F\to F$? But yes, you are taking in two values List[T] and eliminating one of them, probably by concatenation.

Eric M Downes (Mar 16 2024 at 23:43):

Yeah ut all depends on what the monad is. Here it seems like you are just simply sticking values in a list, manipulating that, and then at the very end returning a value instead of a list.

Davi Sales Barreira (Mar 16 2024 at 23:44):

Something like, suppose that $S=\texttt{String}$ and $T=\texttt{Int}$. Then, we define:

$$alg(x::[Int]) = reduce(+, x)\\ coalg(s::String) = [s]\\ expr = length(s)$$

Eric M Downes (Mar 16 2024 at 23:45):

Yes! Exactly. The unit and counit are factored into alg and coalg to deal with the type changes for you.

Davi Sales Barreira (Mar 16 2024 at 23:46):

Hmm, just so I'm not understand things wrongly, what do you mean by "factored into"?

Davi Sales Barreira (Mar 16 2024 at 23:46):

Do you mean that alg and coalg are equal to the unit and conuit?

Eric M Downes (Mar 16 2024 at 23:46):

I mean they are in the code inside those functions, instead of being explicit outside the functions

Eric M Downes (Mar 16 2024 at 23:46):

No not equal.

Eric M Downes (Mar 16 2024 at 23:47):

Like alg is also doing other stuff than just type conversion. I assume reduce changes your int's value by
1 or something

Davi Sales Barreira (Mar 16 2024 at 23:48):

reduce is just a foldr. In this case, it is adding the integers in the list.

Davi Sales Barreira (Mar 16 2024 at 23:48):

Thanks for the answers.

Eric M Downes (Mar 16 2024 at 23:48):

Sure! And good luck.

Eric M Downes (Mar 16 2024 at 23:51):

(To be explicit, if you didnt have a natural typecast from $FT\to T$ you'd return [sum]::List[int] instead of sum::int)

Dylan Braithwaite (Mar 16 2024 at 23:52):

It might be interesting that in functional programming lingo a map from an $F$-coalgebra to an $F$-algebra gets called a 'hylomorphism' if it satisfies an equation $\mathsf{alg} \circ F(\mathsf{expr}) \circ \mathsf{coalg} = \mathsf{expr}$.

The intuition is that these maps can be computed recursively by a divide-and-conquer algorithm by using the coalgebra map to decompose the input, then operating on each constituent part and reassembling the data with the algebra map.

There's some references for this in [[recursion schemes]]

Davi Sales Barreira (Mar 16 2024 at 23:53):

Thanks, @Dylan Braithwaite
Indeed, this seems to be what I'm doing.

Davi Sales Barreira (Mar 16 2024 at 23:54):

In my code, the coalg is used to split a list of data, the expr applies a transformation and the alg computes a thing back again.

Davi Sales Barreira (Mar 16 2024 at 23:54):

I've read the recursion schemes paper, but with so many examples, I guess I just forgot about hylomorphism.

Eric M Downes (Mar 17 2024 at 00:10):

Thanks @Dylan Braithwaite Interesting that there is not a ready resource I can google easily that lays out the similarities and subtle differences between the Kleisli and hylo = ana ⨾ cata perspectives.... onto the todo pile lol. I guess hylomorphisms are more natural with ADTs whereas a Kleisli category appears ever so slightly more general and maybe less turnkey, as it includes "less algebraic" things like Exceptions...

Morgan Rogers (he/him) (Mar 17 2024 at 16:33):

Eric M Downes said:

Perfect! List is a perfect example of a monad. The unit creates the empty list [] out of thin air.

And then, yes to get out of $\mathsf{C}_F$ back to your familiar $\mathsf{C}$ you use the counit to extract the value(s) from the list. Like you would pop the end, and then do something, and pop again, etc. That popping is the counit, which here is factored into $\mathrm{alg}$.

I feel like you're conflating some things here. A monad doesn't have a counit.

Eric M Downes (Mar 17 2024 at 17:10):

Thank you @Morgan Rogers (he/him) ... let me try for a correct statement.

The picture I have in my head is to get back "out" of the Kleisli category, you need a comonad that is right-adjoint to the monad used to define the category, so its not the reduce operation $\mu$ of the monad but $\eta^{co}$ that would be used to eliminate the list, once it is empty. Is that correct?

Morgan Rogers (he/him) (Mar 17 2024 at 17:28):

It sounds like it could work mathematically, but I would caution to try to keep use of terminology precise when responding to someone asking for the name of a structure. What Davi described in the original post isn't a monad and the presumed functor F needn't be a monad for his construction to work, even if it happens to be in the particular case mentioned later. What we need is:

• An endofunctor on some category (of types, I presume), $F$
• A morphism $S \to T$
• An algebra structure for $F$ on an object $T$,
• A coalgebra structure for $F$ on an object $S$

Note that these need not be an algebra/coalgebra structure for any given monad structure on $F$; in the example Davi gives, the algebra structure is an algebra for the list monad and the coalgebra map is the unit for the monad, so I understand the apparent relationship, but it's clear that the symmetry is broken in this example compared with the general situation of Davi's original post.
Incidentally, List is not a comonad because the collection of lists on the empty set is not empty, so we can't be asking for a comonad structure on $F$; I would argue that a monad structure is also superfluous.

Eric M Downes (Mar 17 2024 at 17:38):

Okay, thanks. Agreed its really important to not confuse people, though I'll have to think about why there is no comonad here....

I was under the impression that for every monad there is a unique comonad that reverses its effect, and eliminating the empty list is a counit of that comonad.
https://ncatlab.org/nlab/show/adjoint+monad

I think I'll leave responding to learning: questions to the experts, in the future. I use this stuff regularly but the way I think of things is inherently very messy, and I'm identifying concepts that are merely very similar which is bad thing to do in this kind of math. It's not like there are not enough people around to engage.

Morgan Rogers (he/him) (Mar 17 2024 at 18:08):

Eric M Downes said:

I was under the impression that for every monad there is a unique comonad that reverses its effect, and eliminating the empty list is a counit of that comonad.

On the contrary, the existence of an adjoint to a monad is a very strong property! In particular, the existence of a right adjoint forces the functor to preserve all small colimits (note that the list monad doesn't preserve the initial object, which is one of the obstructions to it also being a comonad, although being simultaneously a monad and comonad is different to being adjoint to a comonad).

I think I'll leave responding to learning: questions to the experts, in the future. I use this stuff regularly but the way I think of things is inherently very messy, and I'm identifying concepts that are merely very similar which is bad thing to do in this kind of math. It's not like there are not enough people around to engage.

I didn't correct you to discourage you from responding to questions!!! I've learned many things here by answering questions incorrectly or imprecisely and having my assumptions challenged by people with more specific knowledge :grinning_face_with_smiling_eyes: I understand that being contradicted 'publicly' like this can be uncomfortable, but no one is judging you for contributing what you know or for sharing the intuitive connections you make between concepts; it's actually greatly appreciated!

Eric M Downes (Mar 17 2024 at 18:10):

No I'm not uncomfortable! Though I appreciate that. I just would feel bad if I led to someone trying to understand category theory having a worse time at it. God knows its hard enough already.

Eric M Downes (Mar 17 2024 at 18:12):

And thanks for the correction! Okay I will think more deeply about this.

Davi Sales Barreira (Mar 17 2024 at 21:32):

Btw, would anyone know about a category involving hylomorphisms? I mean, catamorphisms are the universal morphism from the initial algebra in the F-algebra category. The anamorphism is the universal morphism from the terminal object in the CoAlgebra category... What about the hylomorphism?