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: theory: applied category theory

Topic: Concrete examples of application in industry


view this post on Zulip Ryan Schwiebert (Feb 09 2024 at 19:37):

Hello. I have a mathematics background, but now I work in the software industry. Based on my earlier pass through Seven Sketches and my current attempts to make it through Fong's 2016 thesis, I suspect our software and/or product deployment would benefit from something out of the idea of open systems and hypergraph categories (and/or string diagrams). Unfortunately, (probably because I have not studied it long enough) I cannot see where the rubber meets the road with this stuff yet. It's all "that looks really neat but what decisions can I do differently knowing that?" at this point.

In this thread, it would be really nice to have replies something like: "Today at work I framed our system in terms of (some method from Applied Category Theory (preferably one from the literature I mentioned above)) and discovered (some problem) " and after that hopefully something like "using (some idea from applied category theory) suggested the way to update the system."

Perhaps that last paragraph makes it clear that I do not even understand what form "solutions" from applied category will take. I speculate that it could be of the form of some sort of static analysis of systems, or possibly also computation of suggested solutions (based on my reading of Fong's chapter on electric circuits which hints at systems described by generalized Lagrangian formalisms.) Any help understanding what one can expect to get out of framing problems with open systems would be very helpful!

view this post on Zulip John Baez (Feb 10 2024 at 17:38):

You might check out our software for epidemiological modeling designed using Fong's ideas on decorated cospans. It's not "industry" - but it could be, since it's a practical product: it just so happens that governments more than companies spend money modeling the spread of disease for public health purposes. This talk might help explain it:

and then this paper written for non-mathematicians:

and then, if you want, this paper with all the hardcore math:

view this post on Zulip John Baez (Feb 10 2024 at 17:49):

One lesson from all this is that the AlgebraicJulia project really helps translate ideas for software involving category theory into actual working software. But you still need to have the ideas!

view this post on Zulip Ryan Schwiebert (Feb 10 2024 at 23:33):

@John Baez Thanks for the leads, John! I'll queue these in my reading list.

Does the epidemiological application seem like it would translate to something like "management of interoperating systems"? That's sort of the ecosystem I'm in right now. I'm hoping to find tools to evaluate performance and refine design of interoperating processes. I'm don't think epidemiology is my cup of tea but if you say there's something there I'll try it.

I'm hoping there's something here concerning ability to keep control over flow between systems, and to catch race conditions in the system before they cause problems. I imagine there are rewards to be reaped that I am not even anticipating. If you can think of any "hooks" in these publications that I can grab onto to get going on this sort of thing, I'd appreciate the pointers!

view this post on Zulip John Baez (Feb 11 2024 at 06:30):

Epidemiology is just one application of these ideas; they're quite general. So don't read this stuff thinking it's ultimately about epidemiology. It's about stocks and flows. My talk explains what that means.

view this post on Zulip Jules Hedges (Feb 11 2024 at 18:45):

Besides the epidemiology project at Topos, other people you should talk to who have experience of the rubber hitting the road are

view this post on Zulip Ryan Wisnesky (Feb 11 2024 at 20:37):

We at Conexus AI do data migration, data integration, pretty typical industry stuff, but we do it using category theory instead of relational algebra. Profunctors instead of SQL, lifting problems instead of horn clause logic, theorem proving instead of 'guess and check', etc. We don't use open systems but do have a list of like two dozen common industry use cases if you'd like to check them out.

view this post on Zulip Ryan Schwiebert (Feb 11 2024 at 21:05):

@Jules Hedges @Ryan Wisnesky Thank you both for the info. I will definitely reach out as I (maddeningly slowly) learn more.

view this post on Zulip Peva Blanchard (Feb 13 2024 at 10:48):

Hi, I am also a software engineer with mathematical background (still learning about CT/ACT).

Not sure if it counts as a relevant example, but, at my company, we are developing a DSL for life-cycle analysis modeling. Roughly speaking, LCA is a standardized set of methods and practices to assess the environmental impacts of a product. The goal is to bring software engineering practices to the LCA field through code reuse (aka composable models), version control, testing, etc. We are currently testing it with European cloud providers to model the environmental impacts of the usage of their services.

I drew inspiration and intuition from what the ACT community has provided (especially, Catlab.jl, Stock and Flow). Behind the scene, the models are living in something close to parametrized linear relations. I wanted to properly put the math on paper, but my background knowledge is still too feeble for that. (eventually, I'll figure it out I guess).

view this post on Zulip John Baez (Feb 13 2024 at 20:58):

That sounds cool, Peva. Do you have any intiuitons telling you that bringing category theory more explicitly into your project could be helpful?

view this post on Zulip Peva Blanchard (Feb 14 2024 at 15:17):

Yes, sure!

Why I think category theory would be helpful?

My main concern with the dsl design is making sure that the language features we introduce will not claw back at me. The graal would be a formal semantics, but it is quite out of my league (my original background is distributed algorithms, not really programming language theory).

Now, why category theory?

It turns out people in LCA do really work with (informal) string diagrams. An example here (the circular footprint formula)

image.png

What happens then is people manually "compile" this diagram to a formula, e.g., like that

image.png

which is then translated into excel sheets: this approach does not scale well.

So CT/ACT seems to be the right candidate to enable people to work with executable string diagrams, so they don't worry about the "compilation" stuff, and can reliably scale things up. The motivation seems to be the same as the one from your work on epidemiology modelling: users should focus on what they care about and not worry about writing down the differential equations.

ps: I do remember that I promised you (John) a more detailed account but I could not figure out how to model some aspects of the dsl and did not want to bother you with half-baked material. But now that I know it's ok to publish posts on the zulip server, I can simply post my questions under another topic so people interested can reply.

view this post on Zulip John Baez (Feb 14 2024 at 17:29):

Thanks for the example! I think it should be possible to use ideas from applied category theory, many already implemented in AlgebraicJulia, to handle this problem. A few points:

1) I don't know if AlgebraicJulia provides a graphical user interface for manipulating diagrams suited to your needs; I think you should ask @Owen Lynch about that, because he's been working on something called Semagrams which might do what you need. For our epidemiology project we've developed a separate web-based interface called ModelCollab, specialized for working with stock and flow diagrams.

2) I would be cautious about calling these diagrams 'string diagrams', because string diagrams are just one of the many kinds of diagrams we need in this game: for example our epidemiological models use two other kinds: 'stock and flow diagrams' and 'Petri nets with rates'. They're different, and we've developed different software for them. You'll need to formalize your particular kind of diagrams (or fit them in as a special case of some already studied kind), developing their syntax (e.g. treating them as morphisms in a structured cospan category) and semantics (how you interpret them as giving equations). This looks pretty easy to me, if your example is representative. Then someone smarter than me could actually program it in to AlgebraicJulia.

3) Turning to the semantics, what do you want to do with the equations once you have them? Presumably more than just look at them. Solve them, presumably? What do you typically know and what do you want to solve for? Does it vary a lot?

view this post on Zulip John Baez (Feb 14 2024 at 17:33):

4) Since I started working on applied category theory in order to develop green mathematics, life cycle analysis sounds like a good thing and I'd like to help a little.