Why I am learning category theory • Hacker News Board

Re: Why I am learning category theory

#201

Post by solomatov » Thu, Dec 01, 2022, 12:54 PM UTC

khazhoux wrote: post #148

solomatov wrote: post #117

Earlier quoted context omitted.

There are a lot of interesting properties: - Adjoints preserve limits/colimits. - Adjoint functors give rise to a monad - They are connected to universal morphisms

My problem with category theory (my limited study of it, several years ago) was that it describes and defines a list of properties , but those properties don't combine to reveal any unexpected, exciting results. Again, with my abstract algebra example from above: after just a couple of basic abstract algebra definitions, you learn about subgroups. Simple enough, and not particularly exciting so far. But then you quic…

>My problem with category theory (my limited study of it, several years ago) was that it describes and defines a list of properties, but those properties don't combine to reveal any unexpected, exciting results.

IMO, the main value of category theory is unifying existing math knowledge in one theory. I.e. it helps you see connections between seemingly unrelated areas of math. I.e. in some sense it's a pure abstraction.

Re: Why I am learning category theory

#202

Post by solomatov » Thu, Dec 01, 2022, 1:01 PM UTC

ogogmad wrote: post #199

solomatov wrote: post #117

Earlier quoted context omitted.

There are a lot of interesting properties: - Adjoints preserve limits/colimits. - Adjoint functors give rise to a monad - They are connected to universal morphisms

Where do adjoint functors occur in CS? They occur in advanced algebra, and they occur in topology, but where else? And indeed, the fact that they preserve limits/colimits may help speed up communication and thinking. But I'm not seeing CS connections here. https://en.wikipedia.org/wiki/Adjoint_functors

They literally occur everywhere. Here're a couple more examples, not from what you said:

- Adjoint between integers and real numbers: https://math.stackexchange.com/questions/598075/find-the-lef...

- Adjoint between lattices in abstract interpretation. I.e. abstraction relation between abstract and real interpreter.

Re: Why I am learning category theory

#203

Post by zasdffaa » Thu, Dec 01, 2022, 1:30 PM UTC

wisnesky wrote: post #197

charcircuit wrote: post #133

Earlier quoted context omitted.

So what is coevaluation and why is it useful? Please don't just point at the paper again.

Bi-directional data exchange has many uses. For example, given a set of conjunctive queries Q, because coeval_Q is left adjoint to eval_Q, the composition coeval_Q o eval_Q forms a monad, whose unit can be used to quantify the extent to which the original query Q is "information preserving" on a particular source (so query/data quality). As another example, we use the technique to load data into OWL ontologies from S…

Can you point to some examples of owl/sql transforms being flipped? I have trouble believing that an invertible transformation is hard (presumably each step is invertible, right), and certainly "never would have been able to discover" seems inconceivable to me.

Looking at the paper it is very dense and abstract, also 50 pages long.

Edit: on reflection I am doing a bit of sealioning which was not my intention but it does look that way. I'll try to read your paper but if you assure me cat theory really allowed you to do those things you claim, I'll accept you at your word.

Re: Why I am learning category theory

#204

Post by solomatov » Thu, Dec 01, 2022, 1:49 PM UTC

ogogmad wrote: post #199

solomatov wrote: post #117

Earlier quoted context omitted.

There are a lot of interesting properties: - Adjoints preserve limits/colimits. - Adjoint functors give rise to a monad - They are connected to universal morphisms

Where do adjoint functors occur in CS? They occur in advanced algebra, and they occur in topology, but where else? And indeed, the fact that they preserve limits/colimits may help speed up communication and thinking. But I'm not seeing CS connections here. https://en.wikipedia.org/wiki/Adjoint_functors

Another one is a free monoid. With pair of forgetful/free monoid functors. It sounds a bit mathematical but for type T free monoid is a List in a programming language with generics.

Re: Why I am learning category theory

#205

Post by larve » Thu, Dec 01, 2022, 1:51 PM UTC

matteocapucci wrote: post #195

khazhoux wrote: post #72

As a programmer and hobbyist math reader, I found category theory to be very unrewarding (and I gave up on it) because of the lack of interesting theorems and lemmas. My takeaway was that there's Yoneda lemma and really nothing interesting before you reach that. Like, CT describes a set of rules but very little emerges from those rules. My complaint has nothing to do with whether CT is useful or practical. By contras…

> As a programmer and hobbyist math reader, I found category theory to be very unrewarding (and I gave up on it) because of the lack of interesting theorems and lemmas. My takeaway was that there's Yoneda lemma and really nothing interesting before you reach that. Like, CT describes a set of rules but very little emerges from those rules. The fact it's so rare to find a counterintuitive fact in CT, so that you rarely…

My formulation is "if it's not trivial, it's probably not good" when I implement the necessary functions for the "type class" (to take a haskellism) to work. If your `bind` implementation monad doesn't look like it could have been written by someone who just used the function types, it's probably not right. Thanks for the link to the mcbride-ism:

https://personal.cis.strath.ac.uk/conor.mcbride/PolyTest.pdf

Re: Why I am learning category theory

#206

Post by ogogmad » Thu, Dec 01, 2022, 2:00 PM UTC

solomatov wrote: post #204

ogogmad wrote: post #199

Earlier quoted context omitted.

Where do adjoint functors occur in CS? They occur in advanced algebra, and they occur in topology, but where else? And indeed, the fact that they preserve limits/colimits may help speed up communication and thinking. But I'm not seeing CS connections here. https://en.wikipedia.org/wiki/Adjoint_functors

Another one is a free monoid. With pair of forgetful/free monoid functors. It sounds a bit mathematical but for type T free monoid is a List in a programming language with generics.

But why do you need category theory to understand lists and monoids? They're so basic and elementary.

Re: Why I am learning category theory

#207

Post by ogogmad » Thu, Dec 01, 2022, 2:04 PM UTC

solomatov wrote: post #202

ogogmad wrote: post #199

Earlier quoted context omitted.

Where do adjoint functors occur in CS? They occur in advanced algebra, and they occur in topology, but where else? And indeed, the fact that they preserve limits/colimits may help speed up communication and thinking. But I'm not seeing CS connections here. https://en.wikipedia.org/wiki/Adjoint_functors

They literally occur everywhere. Here're a couple more examples, not from what you said: - Adjoint between integers and real numbers: https://math.stackexchange.com/questions/598075/find-the-lef... - Adjoint between lattices in abstract interpretation. I.e. abstraction relation between abstract and real interpreter.

The first example is trivial, and serves as an illustrative but useless example (which I don't need).

I don't know enough about the second example.

Re: Why I am learning category theory

#208

Post by rssoconnor » Thu, Dec 01, 2022, 2:52 PM UTC

q7xvh97o2pDhNrh wrote: post #180

rssoconnor wrote: post #78

Earlier quoted context omitted.

I agree with you. CT seems mostly useful as a way of devising entirely new abstractions, but once those abstractions are developed, you don't need CT to use them. For example if it were 2008 and you want to be inventor Applicative functors for use in Haskell, then knowing lax monoidal functors from CT might be helpful. But if you want to just use Applicative functors, you don't need to learn lax monoidal functors fir…

Do you have any recommended reading for learning CT from the perspective of an engineer who does want to make their own abstractions? Your description is the single best sales pitch for learning it that I've ever heard. I'm legitimately interested now — in a way that I simply wasn't before your comment. Everyone else who tries to hype up CT is always like, "Whoa, bro, don't you know that addition is actually a monoid…

My method was to spend 25 years listening to colleagues mumble about Category Theory and slowly picking up the basics. Even I didn't really use Category Theory in my abstraction work. It's just that after months of effort to crack my problem, I showed my pages of work to the Category Theory folks and they were like "oh, it's simply Yoneda this and Yoneda that and your proof can be done in 4 lines.".

That said, if I had to guess at what would be effective at getting up to speed without spending 25 years, would be to checkout https://github.com/hmemcpy/milewski-ctfp-pdf Category Theory for Programmers. Milewski was one of those people who were like "Oh, it's simply Yoneda this and Yoneda that", and he figured it out all himself in parallel without seeing my proof.

But I doubt it will be like, knowing Category Theory will enable you to have super powers for abstraction design. Rather it will be a matter of having enough mathematical tools at your disposal plus the right inspiration at the right time to realize that ones of those tools can happen to solve your abstraction programming problem you happen to be facing at some moment, in a way that is not obvious, if you are lucky. In fact, you likely have to first guess at what the right abstraction is and then fall back on Category Theory to verify the sanity of your guess.

Re: Why I am learning category theory

#209

Post by solomatov » Thu, Dec 01, 2022, 3:13 PM UTC

ogogmad wrote: post #206

solomatov wrote: post #204

Earlier quoted context omitted.

Another one is a free monoid. With pair of forgetful/free monoid functors. It sounds a bit mathematical but for type T free monoid is a List in a programming language with generics.

But why do you need category theory to understand lists and monoids? They're so basic and elementary.

You don't. You don't need category theory to understand, you need it to unify your understanding.

P.S. I don't believe programmers need to know category theory. However, it's beautiful by itself like many art.

Re: Why I am learning category theory

#210

Post by solomatov » Thu, Dec 01, 2022, 3:14 PM UTC

ogogmad wrote: post #207

solomatov wrote: post #202

Earlier quoted context omitted.

They literally occur everywhere. Here're a couple more examples, not from what you said: - Adjoint between integers and real numbers: https://math.stackexchange.com/questions/598075/find-the-lef... - Adjoint between lattices in abstract interpretation. I.e. abstraction relation between abstract and real interpreter.

The first example is trivial, and serves as an illustrative but useless example (which I don't need). I don't know enough about the second example.

>The first example is trivial, and serves as an illustrative but useless example (which I don't need).

Yep. Most of the example of adjoints trivial if you know the field of math where they are used. The interesting part is why it happens almost everywhere.