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: Cats applied to software development?


view this post on Zulip Bob Haugen (Jun 08 2020 at 12:51):

Has anybody done that or thought about it and wrote down some conjectures?

view this post on Zulip Bob Haugen (Jun 08 2020 at 14:22):

I should probably clarify: I am very aware of the application of category theory to programming languages.
I am asking about application to the process of developing software, especially in teams: coordination of work, carving into modules, interfaces between modules, software repositories, version control, issues, commitments, pull requests, merges, etc.


view this post on Zulip Bob Haugen (Jun 08 2020 at 14:23):

Rongmin Lu thanks a lot for replying. I added my clarification at the time you were asking what aspects I had in mind, so our comments criss-crossed. Hope my clarification helped.

view this post on Zulip Fabrizio Genovese (Jun 08 2020 at 14:36):

Bob Haugen said:

I should probably clarify: I am very aware of the application of category theory to programming languages.
I am asking about application to the process of developing software, especially in teams: coordination of work, carving into modules, interfaces between modules, software repositories, version control, issues, commitments, pull requests, merges, etc.

The programming language we (Statebox) are working on has exactly this kind of goal in mind

view this post on Zulip Jacques Carette (Jun 08 2020 at 23:43):

I am actively working on using category theory to carve things into modules (and give combinators to assemble them). See in particular https://arxiv.org/abs/1812.08079. The work of my PhD students Yasmine (https://scholar.google.ca/citations?user=yl8yHj0AAAAJ&hl=en and the latest work buried in https://github.com/ysharoda/tog) and Musa (https://github.com/alhassy/next-700-module-systems) are suffused with categorical thinking applied to software. The reason I became co-maintainer of agda-categories (https://github.com/agda/agda-categories) was to learn even more CT that I could apply. If you leaf around https://github.com/JacquesCarette/, https://gitlab.cas.mcmaster.ca/MathScheme and http://www.cas.mcmaster.ca/research/mathscheme/ you ought to see lots of 'categorical thinking'.
[Sorry for the self-promotion; but the question was asked, so I guess it's fair game!]

view this post on Zulip Bob Haugen (Jun 10 2020 at 09:40):

Fabrizio Genovese said:

The programming language we (Statebox) are working on has exactly this kind of goal in mind

Thanks, Fabrizio. I have been following Statebox, but alas, am hard at work on a set of projects using more primitive programming languages. Maybe in my next life, or maybe I can find a project using Statebox to manage distributed economic networks (my focus), or maybe somebody involved with Statebox wants to start one?

view this post on Zulip Bob Haugen (Jun 10 2020 at 09:44):

Jacques Carette said:

[Sorry for the self-promotion; but the question was asked, so I guess it's fair game!]

Definitely fair game, Jacques, and thanks for all the links. I see some really interesting and promising ideas amongst them, but mostly over my head given my infant stage of acquaintance with category theory. I will dig into some of them and see if I can understand.