Live data from Hacker News

Applied Category Theory Course

math.ucr.edu

51–60 of 100 posts

Re: Applied Category Theory Course

#51

Earlier quoted context omitted.

here you go: https://arxiv.org/pdf/1009.1166.pdf

This paper is actually interesting and talks about real-world schemas. I particularly like the concept of distinguishable nulls that define a sane equality operator, unlike the traditional SQL NULL. The paper I was referring to used the category Poly, and literally just stated that Poly could be used for database migrations without elaborating further.

We've used Poly to prove results about functorial data migration.

Re: Applied Category Theory Course

#52

Earlier quoted context omitted.

This paper is actually interesting and talks about real-world schemas. I particularly like the concept of distinguishable nulls that define a sane equality operator, unlike the traditional SQL NULL. The paper I was referring to used the category Poly, and literally just stated that Poly could be used for database migrations without elaborating further.

We've used Poly to prove results about functorial data migration.

Hey you might be interested in this work-in-progress type theory for Poly: https://github.com/toposInstitute/polytt

Re: Applied Category Theory Course

#53
post #48
post #31

Earlier quoted context omitted.

If CT is used to connect different parts of math and software is basically math proofs, then it makes sense programmers find CT interesting. It let's you connect your software to math concepts.

> software is basically math proofs But it's not.

Not all software but by the curry-howard correspondence you can arrive at programs as proofs.

Re: Applied Category Theory Course

#54
post #21
post #11

I'm writing a book [1] about "bona fide" applications of mathematics to practical programming problems, where bona fide is my own personal definition [2]. I've had my eye on claims of applications of category theory for many years, and none of them have quite fit the bill (sorry, John, if you're reading this). When they talk about applications to databases it seems quite unrealistic or lacking in sufficient detail to…

Loved your previous book, will the new book "Practical Math for Programmers" will be released this year?

Sorry, but no. I've got too much going on. But I am at ~200 pages of a draft

Re: Applied Category Theory Course

#55

Earlier quoted context omitted.

This paper is actually interesting and talks about real-world schemas. I particularly like the concept of distinguishable nulls that define a sane equality operator, unlike the traditional SQL NULL. The paper I was referring to used the category Poly, and literally just stated that Poly could be used for database migrations without elaborating further.

I don't know the paper you are talking about but the author of this one (David Spivak) does a ton of research on Polynomial Functors and he has a whole book on them: https://topos.site/poly-book.pdf Poly is an incredibly rich category which can be used to describe a ton of stuff such as finite state machines, neural networks, game interactions, wiring diagrams and dynamical systems more generally. I wouldn't be surpr…

> can be used to describe a ton of stuff such as

One thing that bothers me about applied category theory is that this (being able to describe stuff) always seems to be sufficient for people to claim it is applied. But if the people doing the applying don't find that framing particularly useful, then to me it does not count.

Re: Applied Category Theory Course

#56
post #11

I'm writing a book [1] about "bona fide" applications of mathematics to practical programming problems, where bona fide is my own personal definition [2]. I've had my eye on claims of applications of category theory for many years, and none of them have quite fit the bill (sorry, John, if you're reading this). When they talk about applications to databases it seems quite unrealistic or lacking in sufficient detail to…

It really depends on what your idea of applied is, but Conal Elliot's work is really interesting. His paper on Compiling to Categories [1] pitches programming language semantics as a cartesian closed category [2] allows for really cool stuff by mapping typical evaluation semantics to alternatives like building a computational graph visualization, a pretty printer, and imbuing the original program with automatic diffe…

This does not appear to pass the criterion I gave:

> used by someone in a production software setting to solve a problem not related to category theory

If this stuff or its derivative work is used in production in a mainstream compiler (GHC, perhaps?), then I would see it differently.

Re: Applied Category Theory Course

#57
post #47
post #11

I'm writing a book [1] about "bona fide" applications of mathematics to practical programming problems, where bona fide is my own personal definition [2]. I've had my eye on claims of applications of category theory for many years, and none of them have quite fit the bill (sorry, John, if you're reading this). When they talk about applications to databases it seems quite unrealistic or lacking in sufficient detail to…

It’s a bit tough, on one hand John Baez is a great messenger because he’s such a fantastic communicator. But on the other hand, he’s a pretty horrible spokesperson for ACT because the man did theoretical physics and higher category theory for 30 years and now has decided to do “applied” work. It’s pretty evident in this course, he’s just setting up the frameworks people talk about using but isn’t going for any actual…

All "applied category theory" books seem to be like this: they start by talking about how great the applications will be, but then instead of getting to the applications, they never stop developing the category theory for its own sake. A lot of math does similar things, to be fair, but I also don't count those as applied.

Re: Applied Category Theory Course

#58
post #11

I'm writing a book [1] about "bona fide" applications of mathematics to practical programming problems, where bona fide is my own personal definition [2]. I've had my eye on claims of applications of category theory for many years, and none of them have quite fit the bill (sorry, John, if you're reading this). When they talk about applications to databases it seems quite unrealistic or lacking in sufficient detail to…

> And when I talk to people who are actually on the front lines that try to use category theory to solve some problem, they tell me that it ended up being completely useless. I'm open to having my mind changed. I aim to provide an example of applied category theory in computer science. Your understanding may differ due to the encompassing time frame, however, I ensure that even the most recent findings can rapidly tr…

I understand those concepts well, but I find the casual chain of events questionable, especially when the story is told by category theorists. For example, I was once told by a prominent category theorist that certain aspects of the API design for C++ futures was informed by category theory. When I spoke to the people who actually wrote the RFCs, they said category theory had no part in their thinking.

This is what it seems category theorists tend to do: they build a framework, express existing ideas within that framework, and then claim that the existing work is an application of category theory.

I think that sort of retcon CAN be done. Many math topics like Fourier Analysis have taken practical results, built a math theory behind it, and then converted the entire field to the theory as standard domain knowledge. But the evidence that category theorists have done this, even in the realm of programming language APIs, seems slim.

Even if you agree that the APIs align and the people designing the API know their thing is secretly a monad, still calling that a "success" of category theory is rather weak. By comparison, just because something has addition, units, and inverses, it doesn't mean that group theory is being applied in a meaningful way. The nontrivial results about groups that DO seem to lead to "real" applications are related to the structure of particular groups, as used in cryptography. But I have seen little similar in the way of category theory. Porting concepts from category theory to Haskell is nice, maybe, but it's not clear to me that doing so isn't creating as many problems as its solving (e.g., lenses solve a problem that no other language has, and most Haskell programs seem to me to be completely unreadable by anyone except the author, despite me being no stranger to Haskell).

Re: Applied Category Theory Course

#59
post #35
post #11

I'm writing a book [1] about "bona fide" applications of mathematics to practical programming problems, where bona fide is my own personal definition [2]. I've had my eye on claims of applications of category theory for many years, and none of them have quite fit the bill (sorry, John, if you're reading this). When they talk about applications to databases it seems quite unrealistic or lacking in sufficient detail to…

I mostly agree. Category theory is typically 1-2 steps separated from what programmers do. Category theory is useful for thinking about X, X is super useful for modelling and designing Y. X in {Petri net, relational algebra, feedback diagrams, type system, ... } and Y in {communication protocol, database, programming language, ... }

Being 2 steps separated is no problem for me. Can you point to any specific production software systems, for which the author of those systems says they used CT for designing stuff, and that it helped in a meaningful way? The only one I have heard of is UMAP, and it was closer to "plain ol' category theory" rather than Petri nets or any of the stuff the applied CT folks do.

Re: Applied Category Theory Course

#60
post #11

I'm writing a book [1] about "bona fide" applications of mathematics to practical programming problems, where bona fide is my own personal definition [2]. I've had my eye on claims of applications of category theory for many years, and none of them have quite fit the bill (sorry, John, if you're reading this). When they talk about applications to databases it seems quite unrealistic or lacking in sufficient detail to…

I completely agree. I have been looking for a long while and I haven’t found any examples where using CT made sense. There seems to be a lot of “look at me I am a mathematician!” usage of CT to obfuscate what is really very simple ideas that could otherwise have been explained much simpler without requiring the reader to know an obscure subset of CT. So your basic idea happens to be a Co-Variant Non-Infinitoid Subspa…

I would care if, e.g., some prior approaches did it poorly, and the category theory helped clarify it among the engineers who then agreed it was a good way to think about their problem.
Post reply on HN