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: Really applied ACT


view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 14:57):

I would really like to see Michael more involved in the ACT community. I think he would really have a lot to contribute!

view this post on Zulip (=_=) (Jun 09 2020 at 14:59):

The ACT community is still on the pure side, whereas he's pretty applied. I think ACT needs to move more towards the applied side before you'll see more applied maths people.

view this post on Zulip (=_=) (Jun 09 2020 at 15:00):

Then again, here's an excerpt from his research page:

Reaction-diffusion equations are of substantial importance to the understanding of many chemical and biological phenomena. I have been studying the dynamics of a scalar reaction-diffusion equation that arise from adding diffusion and spatial variation to the carrying capacity of the logistic equation. [...] Future work in this project aims to mimic Floer's construction of a homology theory for Hamiltonian systems by leveraging an important topological index discovered in my dissertation work.

Floer theory! OMG!

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:01):

Rongmin Lu said:

The ACT community is still on the pure side, whereas he's pretty applied. I think ACT needs to move more towards the applied side before you'll see more applied maths people.

This is something I'm trying to push towards myself. Every year I hear people saying that they want more applied stuff, but then everything gets evaluated according to some pretty pure mathematical standards

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:03):

For instance, in reviewing for ACT this year I felt that some papers I was reviewing were really being penalized for having provided stuff like "code". I had to fight quite a bit to actually prove a point that such "more practical stuff" should be considered as a plus, and not as a minus

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:04):

Yes!

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:04):

Also, there's still quite a bit of disconnect with the "real" stuff. That is, sometimes we take practical stuff, abstract it, model it with category theory, and get a categorical model capturing exactly the property no one working in the real world gives an f about

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:05):

I noticed this too, it made me wonder if ACT2021 should be split into 2 streams or something like that..... (but this side topic should be in a different thread)

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:05):

But really, it's sad to say but if I were to give some tips for publishing in the ACT community i'd say "do not provide any code, it will just give you throuble". For sure it gave me nothing but throuble in the last two years.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:06):

Jules Hedges said:

I noticed this too, it made me wonder if ACT2021 should be split into 2 streams or something like that..... (but this side topic should be in a different thread)

You'll just get an even bigger disconnect

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:07):

Yeah. The postponed NIST workshop this year was being informally called "applied applied category theory"

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:08):

In the end I think that the main problem is that researchers tend to get entrenched in their own research. That's everything they care about. Good luck telling them "yes, but actually this is what matters for the real world". Academia has a way to let people grow comfortable in their own biases.

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:08):

I think after the conference is over this year we should start a dialogue with the committee about reviewing guidelines

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:08):

I think the review guidelines this year were "murky" at best

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:09):

Which is understandable, given how fast the community is growing. but that's not the only thing we should discuss.

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:09):

Our tool demo proposal had one reviewer say "this contains no category theory". Which when I thought about it, is the point. I want to demonstrate exactly what the end user should see, which isn't category theory

view this post on Zulip (=_=) (Jun 09 2020 at 15:09):

I feel like on the theory side, many people aren't sure of the IRL problems, or that the IRL problems are just a bit out of reach of their capability.

view this post on Zulip (=_=) (Jun 09 2020 at 15:09):

Also, a lot of pure people are really not comfortable with being confronted with code.

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:10):

Yes, but then I'm not comfortable with being confronted with algebraic topology, but I still put up with it

view this post on Zulip (=_=) (Jun 09 2020 at 15:10):

Jules Hedges said:

Our tool demo proposal had one reviewer say "this contains no category theory". Which when I thought about it, is the point. I want to demonstrate exactly what the end user should see, which isn't category theory

That's kind of the problem. The theory people are concerned with the "back-end". You're more concerned with the UI/UX, i.e. the "front-end".

view this post on Zulip (=_=) (Jun 09 2020 at 15:11):

Jules Hedges said:

Yes, but then I'm not comfortable with being confronted with algebraic topology, but I still put up with it

That's because you're not being stubborn enough. :sweat_smile:

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:11):

I think a very important discussion we should have is about "where do we put the bar". Do we want a really high-standard conference, or something where it's easier to get in? I'd strongly lean towards the second category. High standard conferences give prestige, but I really do not want something akin to LiCS, it's a nightmare. On the contrary, we have examples such as QPL, where traditionally people have pushed to keep it more inclusive. It's easier to get in, so less prestige, but:

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:12):

Rongmin Lu said:

Also, a lot of pure people are really not comfortable with being confronted with code.

As Jules said, you can not be comfortable with code, but in this case just ignore it or say "I'm not fit to review this". Don't bash it.

view this post on Zulip (=_=) (Jun 09 2020 at 15:13):

Fabrizio Genovese said:

As Jules said, you can not be comfortable with code, but in this case just ignore it or say "I'm not fit to review this". Don't bash it.

Sorry, the older generation of pure people do it all the time. Like, it's just banter to them.

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:13):

Fabrizio Genovese said:

Which is understandable, given how fast the community is growing. but that's not the only thing we should discuss.

What else do we need to discuss?

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:14):

I have to say that, being for the first time part of the reviewing committee, the whole thing felt pretty depressing to me. Maybe that's just how reviewing works tho, I'm not an expert

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:14):

I think QPL is something like the ultimate conference, we couldn't do any better than aspiring to be like it

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:14):

Fabrizio Genovese said:

I think a very important discussion we should have is about "where do we put the bar". Do we want a really high-standard conference, or something where it's easier to get in? I'd strongly lean towards the second category. High standard conferences give prestige, but I really do not want something akin to LiCS, it's a nightmare. On the contrary, we have examples such as QPL, where traditionally people have pushed to keep it more inclusive. It's easier to get in, so less prestige, but:

I was referring to this

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:14):

Ah, got it

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:14):

Well, then we should already make some corrections, imho.

view this post on Zulip (=_=) (Jun 09 2020 at 15:17):

Fabrizio Genovese said:

On the contrary, we have examples such as QPL, where traditionally people have pushed to keep it more inclusive. It's easier to get in, so less prestige, but:

A "family reunion" is how I'd think of an inclusive conference.

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:17):

I think it could be a lot worse, this is a community that's barely 2 years old and pretty interdisciplinary. The confusion over last year's proceedings is the kind of breakdown of communication that I'd expect given the circumstances

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:18):

For sure it could be worse. Still, it could be also much better, which is what we should strive for

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:18):

A nice thing I noticed this year is that people are starting to provide datasets for experiments.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:19):

I think this should be made into a mandatory requirement. Also, this raises another problem: We need reviewers that can understand datasets.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:19):

Like, I'm not an expert with data, so I'd just ignore it most likely. It would be nice to have a list of people that qualified to analyze such data

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:20):

This will become especially relevant once the AI/Linguistics stuff starts getting really applied.

view this post on Zulip (=_=) (Jun 09 2020 at 15:21):

Fabrizio Genovese said:

A nice thing I noticed this year is that people are starting to provide datasets for experiments.

There was a huge debate a while ago about whether or not experimental mathematics was actually "proper" maths, which was provoked by Doron Zeilberger. Lots of pure people just thought Zeilberger was a bit crazy and ignored the merits of his arguments.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:21):

Woa, that tshirt in his wiki page is dope.

view this post on Zulip (=_=) (Jun 09 2020 at 15:23):

He is quite a character and has a lot of opinions.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:23):

Lol, and he numbered them!

view this post on Zulip (=_=) (Jun 09 2020 at 15:24):

But yeah, it's really a culture thing. I don't think the pure maths community has quite recovered from the user experience disaster that was the proof by computer of the four colour theorem.

view this post on Zulip (=_=) (Jun 09 2020 at 15:26):

The four colour theorem is also an example of a "useless IRL" theorem:

Despite the motivation from coloring political maps of countries, the theorem is not of particular interest to cartographers. According to an article by the math historian Kenneth May, "Maps utilizing only four colors are rare, and those that do usually require only three. Books on cartography and the history of mapmaking do not mention the four-color property".

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:27):

I think the problem of reviewing in our situation goes like this: "Is it better to be open minded, risking to say that something is right when it's wrong, or evaluating things from one's point of view and without leaving one's comfort zone, risking to reject ideas that can prove to be very valuable, but ensuring that everything is formally right?"

view this post on Zulip Reid Barton (Jun 09 2020 at 15:27):

Fabrizio Genovese said:

Lol, and he numbered them!

Hopefully he doesn't run out of numbers.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:28):

Again, I'm personally leaning towards open-mindedness. Systematizing everything should be more a journal business, I believe

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:29):

In any case I hope that the amount of software, industrial experience reports and other assorted not-a-paper stuff will increase over time, it will be a symptom of ACT being successful. So this needs to be addressed

view this post on Zulip (=_=) (Jun 09 2020 at 15:29):

Fabrizio Genovese said:

I think the problem of reviewing in our situation goes like this: [...]

I think it's probably essential to have two streams for the moment, as Jules said. Pure and applied have rather different research goals in mind, which leads to culture shock when one is asked to evaluate something outside of one's usual paradigm.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:30):

I think we may not need this. We should just put a disclaimer for reviewers: If you think this is too applied for you, or if you are out of your comfort zone when it comes to code, simply refuse to review this paper

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:30):

I don't know if literally having 2 formally-identified streams is necessary. But the reviewing guidelines should be much more detailed and at least say informally "there are 2 different sorts of good papers"

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:31):

The QPL Vs LiCS also needs to be spelled out. This really is very important

view this post on Zulip (=_=) (Jun 09 2020 at 15:31):

Fabrizio Genovese said:

risking to say that something is right when it's wrong

This is the applied mindset, but is anathema to the pure mindset. John has said this once before, that he'd prefer mathematicians who say things that are not wrong.

risking to reject ideas that can prove to be very valuable, but ensuring that everything is formally right

And this is the pure mindset, which makes sense within pure maths.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:32):

Precisely

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:32):

Fabrizio Genovese said:

The QPL Vs LiCS also needs to be spelled out. This really is very important

It's more like QPL vs LiCS vs.... TAC? Acta Mathematica?

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:33):

Those are journals. They should really be left out of the picture. The main aim of a conference is meeting other people to discuss

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:34):

Yeah, I mean at least half the community has a vastly different culture for conferences

view this post on Zulip (=_=) (Jun 09 2020 at 15:34):

Any annual conference of a maths society.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:34):

"conference" comes from "conferre", literally "bringing together, to confront"

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:34):

Half the committee are mathematicians trying to figure out what a "conference proceedings" is

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:34):

So Latin is on my side

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:34):

At least I'm in good company xD

view this post on Zulip (=_=) (Jun 09 2020 at 15:35):

Right, let's call it a symposium instead. I hope the promise of beverages is inclusive enough.

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:35):

Presumably the LiCS model (reject if it looks at you funny) is much more instinctive to mathematicians, who have only ever reviewed for journals before

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:35):

That's "drinking together", yes

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:36):

Jules Hedges said:

Presumably the LiCS model (reject if it looks at you funny) is much more instinctive to mathematicians, who have only ever reviewed for journals before

We could just add a banner to easychair. "Don't be grumpy. Life can be beautiful if you allow it to be"

view this post on Zulip (=_=) (Jun 09 2020 at 15:37):

Fabrizio Genovese said:

Life can be beautiful if you allow it to be

I once heard a string theorist say, only half in jest, that grad school involves taking a pledge of poverty and chastity. So...

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:44):

Very early on I wrote on general that everyone can feel free to go off topic if they feel like they need to

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:44):

I think this is not off topic

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:44):

That was (for me) early in the lockdown

view this post on Zulip (=_=) (Jun 09 2020 at 15:44):

Jules Hedges said:

Very early on I wrote on general that everyone can feel free to go off topic if they feel like they need to

Well, that's how I feel as well, but some people clearly thought otherwise.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:45):

Actually, I think we sould consider this stuff in writing the ACT guidelines. I'd like ACT to represent the opposite of "hell" for the people involved in it.

view this post on Zulip (=_=) (Jun 09 2020 at 15:46):

Hell is our own creation, I think.

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:46):

Well, the ACT guidelines were written by (I think) Jamie, not by God

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:46):

Jules Hedges said:

That was (for me) early in the lockdown

I got way more depressed after the lockdown. Basically you come out and it's the same shit as before. Now that feels depressing

view this post on Zulip (=_=) (Jun 09 2020 at 15:47):

Jules Hedges said:

Well, the ACT guidelines were written by (I think) Jamie, not by God

Reason enough to be optimistic, because that means they can be changed by humans.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:48):

I don't know what the process is for writing the guidelines, but I noticed quite a lot of things that can be improved, so I'd like to contribute if I can

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:48):

Sure, we can start a dialogue, I think if we word our ""demands"" a little bit carefully there's a good chance of the committee agreeing

view this post on Zulip (=_=) (Jun 09 2020 at 15:50):

Like I've said, applied and pure people have different research paradigms. To be inclusive, you need reviewers with the appropriate appreciation of the paradigms to evaluate the submissions properly.

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:52):

Just checked, the ACT steering committee is made of John, Bob, David and Christina. So 3 pure (??) mathematicians and Bob

view this post on Zulip (=_=) (Jun 09 2020 at 15:52):

It seems to me that pure people may need more detailed guidelines on what to expect of a submission, so maybe work on that.

view this post on Zulip (=_=) (Jun 09 2020 at 15:52):

Jules Hedges said:

So 3 pure (??) mathematicians and Bob

Well, there you go.

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:53):

For some reason I thought Jamie was sort of in charge

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:53):

I think Jamie and David took care of organizing ACT2020

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:53):

Jules Hedges said:

Just checked, the ACT steering committee is made of John, Bob, David and Christina. So 3 pure (??) mathematicians and Bob

Well, if there's Bob then for sure our pleads won't be unheard. :slight_smile:

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:54):

Ah, the co-chairs [insert joke here] of the PC are David and Jamie

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:56):

Thing is, I think the ACT guidelines were already by far the most detailed reviewing guidelines I've ever received

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:56):

Just.... not detailed in the right places, maybe

view this post on Zulip (=_=) (Jun 09 2020 at 15:57):

Jules Hedges said:

Thing is, I think the ACT guidelines were already by far the most detailed reviewing guidelines I've ever received

I didn't use an adjective to modify "guidelines".

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:58):

Ok, here's what the guidelines actually said:
Please have them finished by 31 May. Ultimately, for each paper, we must decide together whether it should be rejected, accepted for a regular presentation, or accepted for a longer "keynote" presentation. These decisions will be made in early June after all the reviews are in.

Particularly for those of you who may not have reviewed for a conference before, here are some guidelines.

• Your review should focus on the quality, significance, originality and rigour of the paper, as well as its "fit" to the Applied Category Theory community, as described in the call for papers. The best papers will be excellent as articles, and also lead to compelling conference presentations.

• You are encouraged to use the "subreviewing" functionality to delegate your reviews to other members of the community who you trust to complete the task diligently, perhaps such as postdocs or experienced PhD students you know well.

• While reviews are expected to be reasonably comprehensive, it is recognized that we all have a limited amount of time, and reviewers may not have enough time to verify the correctness of complex proofs in full detail.

• Beyond completion of reviews for your assigned papers, you are welcome to submit additional reviews for other papers not assigned to you.

• For each paper assigned to you, after you have submitted your review, you will be able to see the other reviews that may already have been submitted. Please then use the discussion functionality underneath the reviews to discuss the paper with the other reviewers. You are welcome to get involved with discussions even for papers that have not been assigned to you. It's great to focus these discussions on papers with a divergence of review scores, in an attempt to reach a consensus. You are welcome to start engaging with these discussions immediately after submitting your review, although this phase will likely only get into full swing in early June.

• You are free to update your review, and your chosen score, at any time after submitting the review. In particular, if your opinion changes following a discussion, updating your review is the best way to indicate that.

Best wishes,
Jamie (co-chair)

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:58):

Yes, the meaning of "fit" was left to anyone's interpretation

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 15:59):

that is the heart of the problem, I think

view this post on Zulip Jules Hedges (Jun 09 2020 at 15:59):

Yes, I think I agree

view this post on Zulip (=_=) (Jun 09 2020 at 15:59):

Fabrizio Genovese said:

Yes, the meaning of "fit" was left to anyone's interpretation

What was in the call for papers, which is apparently the authority for what "fit" means?

view this post on Zulip Jules Hedges (Jun 09 2020 at 16:03):

Rongmin Lu said:

What was in the call for papers, which is apparently the authority for what "fit" means?

We're definitely approaching this problem like academics...... If there was ever a call for papers, it's not there now

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 16:04):

Jules Hedges said:

Rongmin Lu said:

What was in the call for papers, which is apparently the authority for what "fit" means?

We're definitely approaching this problem like academics...... If there was ever a call for papers, it's not there now

Yes, also all reviewers will have forgotten what was in there by the time reviewing started

view this post on Zulip (=_=) (Jun 09 2020 at 16:05):

Fabrizio Genovese said:

Yes, also all reviewers will have forgotten what was in there by the time reviewing started

Good point there. Yup, terrible UX as usual.

view this post on Zulip Jules Hedges (Jun 09 2020 at 16:05):

Right. One concrete thing I would propose is that next year's cfp explicitly says that tool demos are on-topic

view this post on Zulip Joe Moeller (Jun 09 2020 at 16:07):

When we organized the ACT session of the AMS meeting in Riverside last year, we roughly divided submissions into leaning-theory and leaning-applied. We gave them different days. This seemed to create a good synergy, imo. People talking on one day stuck around to listen on the next day for the most part. I mention it I guess to contribute one anecdote of success of this as a strategy.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 16:12):

I am not a fan of dividing submission because this puts one more burden on the authors. Do I really know if what I do is applied applied or theory applied?

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 16:12):

Like, one could seriously risk to get reviews along the lines of "this is too applied for this track" and "this is too pure for this track"

view this post on Zulip Joe Moeller (Jun 09 2020 at 16:13):

When we did it, we did not ask the authors to choose. We just did it ourselves. First what we did was decide which we like the most, then we did the scheduling using this divide. So this is slightly different from what was being discussed here I guess.

view this post on Zulip Joe Moeller (Jun 09 2020 at 16:14):

There were papers that didn't clearly fit one or the other on their own, but seemed to gel better with the other talks in one or the other, usually.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 16:14):

Joe Moeller said:

When we did it, we did not ask the authors to choose. We just did it ourselves. First what we did was decide which we like the most, then we did the scheduling using this divide. So this is slightly different from what was being discussed here I guess.

Then I approve :D

view this post on Zulip Blake Pollard (Jun 09 2020 at 16:19):

AACT for lyfe

view this post on Zulip Blake Pollard (Jun 09 2020 at 16:21):

I thought the way the AMS sessions went down was great in terms of the applied/less applied corepresentation.

view this post on Zulip Blake Pollard (Jun 09 2020 at 16:28):

I'd love to see the A in the ACT community grow, but there is definitely a huge challenge making more applied folks feel welcome. I used to think the challenge was in getting applied folk to engage with basic category theory, but it seems the really hard thing is to get more mathematically minded folks to engage with more messy, real-world problems. It is really a matter of taste and forcing yourself to try something new and force yourself to engage with flavors that seem quite funky at first, and for a while.

view this post on Zulip Blake Pollard (Jun 09 2020 at 16:31):

I like to think that what we're trying to do is really 'operationalize' a lot of great ideas/mathematics that is already out there and lines up really well with important real-world problems, but yea where ultimately a lot of that gets hidden 'under the hood' for the end user.

view this post on Zulip Jules Hedges (Jun 09 2020 at 16:33):

Blake Pollard said:

I used to think the challenge was in getting applied folk to engage with basic category theory, but it seems the really hard thing is to get more mathematically minded folks to engage with more messy, real-world problems.

This is a good point!

view this post on Zulip Jules Hedges (Jun 09 2020 at 16:34):

I don't want to force anyone to engage with the messy real world if they don't want to, even within ACT. But I do want to prevent them from writing reviews as though the real world being messy is somehow the author's fault

view this post on Zulip Morgan Rogers (he/him) (Jun 09 2020 at 16:43):

I can also imagine the opposite being a problem, that we pure folks can lose sight of motivation for long enough that when theory is applied to the problems it was developed to solve, and the tools make the solution to that problem seem easy, we can miss the significance of the results. Or that we know the abstract theory well enough that when we see someone put a lot of work into computing something that we can see a nice shortcut to calculating, the actual result gets ignored in the face of a "this is trivial" attitude.

view this post on Zulip Jules Hedges (Jun 09 2020 at 16:54):

I wonder if anything like this happened at QPL when the previously-neat world of CQM started being applied to NISQ and other nasty things coming from the engineering side

view this post on Zulip John Baez (Jun 09 2020 at 19:49):

Jules Hedges said:

Just checked, the ACT steering committee is made of John, Bob, David and Christina. So 3 pure (??) mathematicians and Bob

I'm glad you at least included three question marks. I don't think nonlinear PDE, quantum field theory, chemical reaction networks and Markov processes count as "pure math". Maybe you were referring to my purity of spirit?

I've always called myself a "mathematical physicist". In academia this is not considered "applied mathematics", but it's also definitely not considered "pure mathematics".

view this post on Zulip John Baez (Jun 09 2020 at 19:53):

More seriously: as category theory gets more "really applied", and we get more work that uses category theory but focuses on the nitty-gritty details of applications, I think we'll get people who become "stars" for doing that successfully - because everyone in the ACT community is looking for such work. And those people will be pulled into organizing the ACT conferences, and choosing speakers and so on.

view this post on Zulip Joachim Kock (Jun 09 2020 at 21:56):

Hi Fabrizio and Jules,
thanks for raising all these points. It is a very interesting thread.

I agree that it would be great to see more 'really applied' category theory. Hopefully it will come with time. There is still a wide span between the most applied end (some still struggling with elementary definitions of category theory) and the most theoretical end, which could rather be called 'pure category theory inspired by applied category theory' (some of us still dreaming of making contact with the real world).

In the context of ACT I am myself on the rather theoretical side, so it is very interesting for me to read the conversation in this thread. I agree about openness. But it seems to me that many of the points are not really about appliedness, but rather about the conference format...

view this post on Zulip Joachim Kock (Jun 09 2020 at 22:00):

Fabrizio Genovese said:

But really, it's sad to say but if I were to give some tips for publishing in the ACT community i'd say "do not provide any code, it will just give you trouble".

I would give this advice for any oral presentation (except perhaps at computer-science conferences), just as it is often a good idea to avoid proofs :-) But it is indeed sad if you were to give the no-code advice for publishing.

view this post on Zulip John Baez (Jun 09 2020 at 22:03):

The "wide span between between the most applied end and the most theoretical end" will probably never go away, and I don't even know if it should.

view this post on Zulip John Baez (Jun 09 2020 at 22:05):

I think of physics, an old discipline, which has practitioners ranging from Ed Witten at one end to the people who build apparatus for experiments at the other. Both have huge amounts of expertise - Ed Witten probably wouldn't do so well if you put him in a lab - but people occupying these extremes can often barely talk to each other.

view this post on Zulip John Baez (Jun 09 2020 at 22:06):

The reason it works is that there's a whole chain of people linking the two extremes.

view this post on Zulip John Baez (Jun 09 2020 at 22:07):

What I love about applied category theory is that we're trying to set up chains linking category theorists to people in many other subjects.

view this post on Zulip Joachim Kock (Jun 09 2020 at 22:08):

Fabrizio Genovese said:

Those are journals. They should really be left out of the picture. The main aim of a conference is meeting other people to discuss.

I very much agree.

But many people regard a conference primarily as a venue for papers -- that the main goal is to present papers rather than giving talks.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 22:11):

So this ties in with the idea of how much high we want to draw the acceptance line. Higher means more prestige, but also less opportunities to use the conference as a meeting space for all the people working in the field

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 22:12):

One of the best experiences in QPL was, as a PhD student, to meet other PhD students. So there was a constant exchange of ideas, and feedback about how their PhD experience was. Many of them wouldn't be there probably if the acceptance criteria were set to be higher

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 22:13):

It really feels nice when you are at your first publication, you get there and you are "formally introduced to the community".

view this post on Zulip Joachim Kock (Jun 09 2020 at 22:14):

Rongmin Lu said:

Also, a lot of pure people are really not comfortable with being confronted with code.

That's probably true, but I think that's not the point. We are all comfortable with being confronted with proofs. Yet we gain very very little from seeing a proof in a talk.

When choosing a topic for a talk, we do not necessarily choose our latest technical achievement, but rather something that has a fair chance of getting across to the audience. Technical proofs, code, implementation details are rarely the best suited. They can still be of great practical interest and value, of course!

When advocating code and data sets you are probably thinking about papers, not talks :-)

view this post on Zulip Joachim Kock (Jun 09 2020 at 22:16):

Sorry for writing out of synch -- I am still reading further up in the thread.

view this post on Zulip James Fairbanks (Jun 09 2020 at 22:28):

I think that the Non-proceedings track (NPT) vs Proceedings track (PT) was a good idea. My material wasn't ready for a full paper yet so I submitted as a NPT talk with a 3 page abstract. In order to fulfill the goal of having Math, CS, and Science/Engineering come together we need to maintain these two tracks. Nobody in Math or Biology is going to get tenure points for a conference paper no matter how competitive and CS people can't get tenure points for a conference that isn't based on 8-12 page competitively reviewed papers. Since this is an artifact of the Tenure & Promotion system, once the refereeing happens we don't need to distinguish between the tracks at the physical conference.

view this post on Zulip Joachim Kock (Jun 09 2020 at 22:31):

Jules Hedges said:

Half the committee are mathematicians trying to figure out what a "conference proceedings" is

Indeed :-) It is a mystery (to me) why this publication form exists. It is a mystery why one should bundle together talks and papers, and why it should be reasonable to give a single evaluation for talk proposal and paper quality. Talks and papers are very different media. A talk is something of the moment, an exchange of ideas between people present. A paper is supposed to be a lasting account of something, something that has already been digested, ironed out, streamlined, a reference for technical details -- something worth reading also 2 or 10 years from now. It seems silly to publish something that has been rushed to meet a deadline and has been forced into a 12-page format not dictated by the material. Either it will soon be superseded by a better account of the theory, or worse: the preliminary account will prevent the final version :-( The author will move on, instead of finish what he started.

(Of course, sometimes the perfect match between a talk and a paper does exist.)

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 22:31):

A very confusing thing is that Jamie said that the quality standard for the NPT track had to be the same standard for the PT track.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 22:32):

Joachim Kock said:

Jules Hedges said:

Half the committee are mathematicians trying to figure out what a "conference proceedings" is

Indeed :-) It is a mystery (to me) why this publication form exists. It is a mystery why one should bundle together talks and papers, and why it should be reasonable to give a single evaluation for talk proposal and paper quality. Talks and papers are very different media. A talk is something of the moment, an exchange of ideas between people present. A paper is supposed to be a lasting account of something, something that has already been digested, ironed out, streamlined, a reference for technical details -- something worth reading also 2 or 10 years from now. It seems silly to publish something that has been rushed to meet a deadline and has been forced into a 12-page format not dictated by the material. Either it will soon be superseded by a better account of the theory, or worse: the preliminary account will prevent the final version :-( The author will move on, instead of finish what he started.

(Of course, sometimes the perfect match between a talk and a paper does exist.)

I guess it's reasonable to evaluate a paper to decide if someone deserves to have or not a talk. The whole proceedings thing feels a bit outdated since everything is already on the arxiv tho

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 22:33):

I guess what we really want is just some DOI attached to an arxiv paper that means "someone bothered to read this and it doesn't contain any wild claim. Plus it's interesting enough that we decided this person should give a talk in this place. Cheers"

view this post on Zulip James Fairbanks (Jun 09 2020 at 22:36):

The idea that you could hold a 12 page paper to the same standard as a 1 page abstract is a type error.

view this post on Zulip Fabrizio Genovese (Jun 09 2020 at 22:38):

Well, I got two non proceding papers: One was a 3 pages paper and the other one was Profunctor optics a categorical update. You can imagine my confusion when I was asked to evaluate all the papers according to the same quality standards xD

view this post on Zulip (=_=) (Jun 10 2020 at 00:31):

Joachim Kock said:

Rongmin Lu said:

Also, a lot of pure people are really not comfortable with being confronted with code.

That's probably true, but I think that's not the point. We are all comfortable with being confronted with proofs. Yet we gain very very little from seeing a proof in a talk.

I think we agree on the Curry-Howard correspondence, i.e. that proofs are really "just" programs, but I have seen/heard firsthand the reluctance of

The aversion is shared and real, the Curry-Howard correspondence notwithstanding.

view this post on Zulip Jules Hedges (Jun 10 2020 at 09:32):

Joachim Kock said:

Jules Hedges said:

Half the committee are mathematicians trying to figure out what a "conference proceedings" is

Indeed :-) It is a mystery (to me) why this publication form exists. It is a mystery why one should bundle together talks and papers, and why it should be reasonable to give a single evaluation for talk proposal and paper quality.

For major cs conferences like LiCS, I think it's reasonable to say that the only reason anyone submits there is for the publication. There is a talk attached for the same reason that humans have a tail bone

view this post on Zulip (=_=) (Jun 10 2020 at 09:47):

Jules Hedges said:

Joachim Kock said:

Indeed :-) It is a mystery (to me) why this publication form exists. It is a mystery why one should bundle together talks and papers, and why it should be reasonable to give a single evaluation for talk proposal and paper quality.

For major cs conferences like LiCS, I think it's reasonable to say that the only reason anyone submits there is for the publication. There is a talk attached for the same reason that humans have a tail bone

Some papers are accepted as "posters", which means they don't even have talks attached because they're not considered important enough by the organisers.

view this post on Zulip John van de Wetering (Jun 11 2020 at 10:54):

To but in on the question of what is "too applied": Pretty much everyone working with the ZX-calculus right now is not a category theorist anymore (I know I am certainly not). So even though this started from CQM and the theory of interacting Frobenius algebras, right now it really feels more like a quantum information topic. So would a ZX-calculus paper be considered in-scope for ACT? (I guess this question is kind of hypothetical as I think almost all ZX people would submit to QPL rather than ACT, but I hope you catch my drift)

view this post on Zulip John van de Wetering (Jun 11 2020 at 10:55):

Also, +1 on QPL feeling like a reunion. It is by far my favorite conference of the year for this reason

view this post on Zulip John van de Wetering (Jun 11 2020 at 10:59):

Jules Hedges said:

I wonder if anything like this happened at QPL when the previously-neat world of CQM started being applied to NISQ and other nasty things coming from the engineering side

QPL2019 had a whole slew of papers about circuit optimisation and NISQ stuff, and I heard from several people that they felt QPL had really drifted from what it once was.
I also heard several people complain (including me) that there were more and more people submitting non-proceedings talks, which were preventing good proceedings submissions from getting in. This is a shame because QPL is a really good venue for a particular type of work, and it is often hard or not worthwhile to recast a paper for a different venue if it doesn't get accepted.

view this post on Zulip Jules Hedges (Jun 11 2020 at 10:59):

Interesting.... it sounds like it's a victim of its own success

view this post on Zulip Jules Hedges (Jun 11 2020 at 11:00):

John van de Wetering said:

So even though this started from CQM and the theory of interacting Frobenius algebras, right now it really feels more like a quantum information topic. So would a ZX-calculus paper be considered in-scope for ACT?

If anyone says ZX isn't in scope for ACT I'll fight them

view this post on Zulip John van de Wetering (Jun 11 2020 at 11:04):

Okay, but for instance, there are now several papers doing circuit optimisation using the ZX-calculus. This is as applied as it gets, but it really doesn't contain anything resembling category theory (at least on the surface).
Would you say that is still suitable for ACT?

view this post on Zulip Fabrizio Genovese (Jun 11 2020 at 11:05):

I don't know if I would. For sure I think it would be beneficial for the ACT community to come into contact with similar stuff tho

view this post on Zulip Jules Hedges (Jun 11 2020 at 11:06):

I would. ZX is the prop of interacting frobenius algebras plus some stuff, it's category theory. Just because there is now advanced technology that means it can be presented entirely using string diagrams without any classical syntax, doesn't make it any less category theory

view this post on Zulip John van de Wetering (Jun 11 2020 at 11:14):

Okay, but to play devils advocate: algebraic geometry is also really just category theory if you squint hard enough, but I don't think you would feel a pure algebraic geometry paper would be a good fit for ACT, right?

view this post on Zulip Jules Hedges (Jun 11 2020 at 11:17):

Yes. There's 2 considerations: 1. "applications" to pure maths don't count as applied category theory (that's the only constraint I personally consider on ACT), and 2. algebraic geometry has its own community, venues etc - also the case for ZX as you said

view this post on Zulip Morgan Rogers (he/him) (Jun 11 2020 at 11:24):

I don't see community mitosis as a bad thing, personally. What begins as ACT is bound to become more specialised over time. If it ends up with its own platform that's more suitable, great! If it needs the continued support of the community is grew from, that's also fine - but perhaps in that case there should be some concerted effort on the part of speakers to emphasise links to that community, because that's the most reliable way to draw incoming members of the community into their branch which can eventually became independent.

view this post on Zulip Morgan Rogers (he/him) (Jun 11 2020 at 11:26):

I should qualify that "independent" needn't mean "separate", just that the obligation to pander to the 'parent' community is lifted.

view this post on Zulip Fabrizio Genovese (Jun 11 2020 at 12:00):

So the way I envision things would be the following:

From this point of view, I'm very happy to see some ZX paper presented to ACT, provided that the paper is not just incremental, but a milestone. For instance the proof of ZX completeness could qualify as such. It is also true that if you prove a big result in ZX calculus probably you want to publish it in a more specialized venue. In this case it would be nice to have such a result presented as a non-proceedings paper, as this year has been the case for Profunctor Optics.

view this post on Zulip Fabrizio Genovese (Jun 11 2020 at 12:02):

Clearly it is not to be excluded that at some point different communities will grow so mature to become independent. This is in a way the case for CQM: I do not see many of the people working fulltime in CQM also involved here. But this sort of things tend to happen spontaneously, so we'll get aware of this when it happens. :slight_smile:

view this post on Zulip Jules Hedges (Jun 11 2020 at 12:05):

This is a good balance, I like it

view this post on Zulip Jules Hedges (Jun 11 2020 at 12:05):

In reality the recent milestone papers in ZX were published in LiCS

view this post on Zulip Fabrizio Genovese (Jun 11 2020 at 12:26):

Well, LiCS is the same "umbrella conference" but for the whole of theoretical computer science, hence yes, when you have something really dope you should probably drop it there.

view this post on Zulip John van de Wetering (Jun 11 2020 at 15:39):

You could publish the paper in LICS for the carreer credits and then send a non-proceedings talk to ACT to talk to people actually potentially interested in your research, I guess

view this post on Zulip Fabrizio Genovese (Jun 11 2020 at 15:46):

This is precisely what I would do. Also because, for what Jules said multiple times, it doesn't look like the LiCS crowd is much interested in other people's talks. Everyone submits there just for the glory and the tenure track points that come with it. So if you want to actually spread you ideas that doesn't strike me as a very receptive audience.

view this post on Zulip John Baez (Jun 11 2020 at 15:51):

There were a bunch of ZX-calculus talks at the last ACT.

view this post on Zulip Fabrizio Genovese (Jun 11 2020 at 15:52):

John Baez said:

There were a bunch of ZX-calculus talks at the last ACT.

This is also because last ACT was in Oxford which is heavily CQM, so a natural bias towards CQM material was expected (mainly due to Oxford people being encouraged to submit because of 0 costs in attending the conference) :slight_smile:

view this post on Zulip Fabrizio Genovese (Jun 11 2020 at 15:53):

Similarly QPL2019, held in Cali, saw quite a few submission in Network theory, I imagine also because of the proximity to UCR. I think this kind of things is natural.

view this post on Zulip John Baez (Jun 11 2020 at 15:53):

Yes, that's true. I haven't seen ZX-calculus papers submitted to ACT2020.

view this post on Zulip John Baez (Jun 11 2020 at 15:53):

There could be some, maybe I just didn't notice.

view this post on Zulip Fabrizio Genovese (Jun 11 2020 at 15:54):

I think this is again due to the "family reuinion" thing. If I have a limited budget to travel I will attend the conferences where I know there are more people working in my field. In this respect for sure QPL beats ACT if one works in CQM

view this post on Zulip Joe Moeller (Jun 11 2020 at 15:54):

I think I've heard people say something along the lines of "something is only considered philosophy until we actually get a handle on understanding it, then it becomes science". Maybe something similar is true of ACT.

view this post on Zulip John Baez (Jun 11 2020 at 15:55):

I keep saying that thing you quote. I do it to defend philosophy against charges that it never makes any progress.

view this post on Zulip John Baez (Jun 11 2020 at 15:56):

So yeah, maybe someday people will say ACT never makes any progress because the ZX-calculus and category-theoretic ideas in machine learning and ... lot of other things that might happen... don't get counted as ACT.

view this post on Zulip Joe Moeller (Jun 11 2020 at 15:57):

Just like some people don't count homotopy theory and algebraic geometry as CT...

view this post on Zulip John van de Wetering (Jun 11 2020 at 16:15):

John Baez said:

There were a bunch of ZX-calculus talks at the last ACT.

There were three submissions that could be considered to be about ZX, but of those, 2 were actually about general graphical languages.
The one other submission was by Bob and Harny, and was a completeness result, which is probably the most interesting part of ZX from a CT perspective.

view this post on Zulip John van de Wetering (Jun 11 2020 at 16:17):

Now that basically all completeness results that can be proven have been proven regarding ZX I don't see many ZX papers coming to ACT soon. Perhaps some general "from abstract category theory to concrete applications" history talk about ZX would be interesting though...

view this post on Zulip John Baez (Jun 11 2020 at 16:26):

Maybe someone will get a new idea that uses category theory to do something with the ZX calculus. There's more to life than completeness, after all.

view this post on Zulip Jules Hedges (Jun 11 2020 at 16:33):

Yeah, I think another factor last year was that 2018-19 was a really crazy time in ZX. As far as I know there was nothing equivalent this year

view this post on Zulip Fabrizio Genovese (Jun 11 2020 at 17:21):

Jules Hedges said:

Yeah, I think another factor last year was that 2018-19 was a really crazy time in ZX. As far as I know there was nothing equivalent this year

Yes. Completeness in this framework actually means "We can use ZX to program quantum computers"

view this post on Zulip Cole Comfort (Jun 11 2020 at 19:14):

John van de Wetering said:

To but in on the question of what is "too applied": Pretty much everyone working with the ZX-calculus right now is not a category theorist anymore (I know I am certainly not). So even though this started from CQM and the theory of interacting Frobenius algebras, right now it really feels more like a quantum information topic. So would a ZX-calculus paper be considered in-scope for ACT? (I guess this question is kind of hypothetical as I think almost all ZX people would submit to QPL rather than ACT, but I hope you catch my drift)

My ZX paper at QPL was about spans so I would say that this is squarely in the scope of ACT. There is still more work to be done even though full completeness is proven,

view this post on Zulip Cole Comfort (Jun 11 2020 at 19:19):

In particular, the axioms of various fragments of the ZX calculus are very ad hoc, and actually figuring out what is really going on at a fundemental level is still open. Even though this is much more vague than just asking for completness proofs of some presentation of the ZX calculus, at least from a categorical perspective, I think that there is still more to be done here. Like finding the right presentation that actually reveals some fundemental algebraic structure that is hiding there.

view this post on Zulip Cole Comfort (Jun 11 2020 at 19:22):

I think that there is still work to be done in terms of building fragments of the ZX calculus by composings smaller props, for example. This kind of thing is actively being studied by Sobocinski and his colleagues from the perspective of concurrent systems (instead of quantum circuits) and the work there is not finished either. I think there is still work to be done in unifying both research programmes.

view this post on Zulip Cole Comfort (Jun 11 2020 at 19:38):

I think what the concurrency people are doing is in a very similar spirit to the older ZX papers, even if the motivation is different.

view this post on Zulip Jules Hedges (Jun 11 2020 at 21:43):

I definitely wouldn't be surprised if there's a much deeper story going on, that explains "why" the same structures come up in quantum computing as in concurrency theory for example

view this post on Zulip Cole Comfort (Jun 11 2020 at 23:01):

Jules Hedges said:

I definitely wouldn't be surprised if there's a much deeper story going on, that explains "why" the same structures come up in quantum computing as in concurrency theory for example

The thing is, that they things diverge from each other when one considers full ZX. Because on the concurrency side, they are using the direct sum as a tensor; but on the ZX side, they are using the bilinear tensor. So they only really can agree when the ZX calculus is restricted to the Clifford fragment because of the dimension blowup.

view this post on Zulip (=_=) (Jun 12 2020 at 09:12):

Joe Moeller said:

Just like some people don't count homotopy theory and algebraic geometry as CT...

Errr... algebraic geometry has existed long before CT came into the picture, and some theorems in homotopy theory pre-date CT. That's quite the opposite situation from what John was describing in relation to ACT and its spin-offs (ZX-calculus, CT in ML, etc).

view this post on Zulip Amar Hadzihasanovic (Jun 12 2020 at 09:25):

Well, soundness and completeness results have been done in model-theoretic language long before CT. I think the role of CT in the ZX-calculus is in the background, having prepared the conceptual shift of universal algebra over categories that are not Set and not even Set-like, and the idea of diagrams as a generalisation of terms for non-cartesian semantics.

view this post on Zulip Amar Hadzihasanovic (Jun 12 2020 at 09:27):

Once that's established, I don't think there's anything particularly category-theoretic in the completeness proofs.

view this post on Zulip Amar Hadzihasanovic (Jun 12 2020 at 09:47):

I think maybe the difference is more of “social” nature -- whereas algebraic geometers and homotopy theorists have adopted CT to the extent that every specialist has a working knowledge of it, the same has not happened with logicians and model theorists... In another universe where categorical universal algebra has conquered the world, the ZX-calculus would perhaps have been presented at the “Non-cartesian model theory” conference...

view this post on Zulip Georgios Bakirtzis (Jun 12 2020 at 18:55):

ACT will be really applied when it used as Set theory is currently, without any recognition that it is being used (as a language of science and engineering).

view this post on Zulip Joe Moeller (Jun 12 2020 at 23:01):

Rongmin Lu said:

Joe Moeller said:

Just like some people don't count homotopy theory and algebraic geometry as CT...

Errr... algebraic geometry has existed long before CT came into the picture, and some theorems in homotopy theory pre-date CT. That's quite the opposite situation from what John was describing in relation to ACT and its spin-offs (ZX-calculus, CT in ML, etc).

I know. I just meant people are doing loads of CT, but at the end of the day, people ignore the role it played. I didn't mean to imply I think these branches are fully under the CT umbrella.

view this post on Zulip Jules Hedges (Jun 13 2020 at 10:00):

This made me start thinking about what I consider an "application of set theory". I don't think formulating things in the language of sets counts as an application of set theory. I think the simplest thing I'd consider an application of set theory would be a use of Zorn's lemma or the Ultrafilter lemma. Don't know whether anyone else shares an opinion like that though...

view this post on Zulip Fabrizio Genovese (Jun 13 2020 at 10:37):

I think the main difference here is between "using sets to formalize something" and "developing new set-theoretic tools to deal with a problem"

view this post on Zulip Fabrizio Genovese (Jun 13 2020 at 10:38):

I think the main difference here is between "using sets to formalize something" and "developing new set-theoretic tools to deal with a problem"

view this post on Zulip Fabrizio Genovese (Jun 13 2020 at 10:39):

Many people doing algebraic geometry "do loads of CT" not only because they use categories to formalize their work, but also because they constantly invent new categorical gadgets to make their work manageable (see Grothendieck). Because of CT intrinsic compositionality, it's much easier then to export these gadgets to other fields that use CT than it is to do the same with set-theoretic things. Still, I think it's safe to say that many logicians - especially those working in model theory - do a lot of set theory.

view this post on Zulip (=_=) (Jun 13 2020 at 12:13):

Fabrizio Genovese said:

Many people doing algebraic geometry "do loads of CT" not only because they use categories to formalize their work, but also because they constantly invent new categorical gadgets to make their work manageable

I don't disagree, but I refer you to the analogy of physicists doing loads of DEs: I think it'd be a bit of a stretch to "count physics as the study of DEs", because physics is more than that. There are surely also algebraic geometers out there who don't generate new CT gadgets "constantly" in their work.

view this post on Zulip James Fairbanks (Jun 13 2020 at 14:31):

I think if you had a conference for “applied diffeqs” and excluded physicists, because “physics is more than just applying diffeqs” that would be bad.

view this post on Zulip (=_=) (Jun 14 2020 at 01:53):

James Fairbanks said:

I think if you had a conference for “applied diffeqs” and excluded physicists, because “physics is more than just applying diffeqs” that would be bad.

Sure. Your comment harks back to that time when Tom Leinster took John to task for apparently excluding CS from ACT. I have that in mind, but from a different angle, which I'll try to explain below.

view this post on Zulip (=_=) (Jun 14 2020 at 01:53):

I wholeheartedly agree that if we had a conference for "applied DEs" (ADE), then anyone who uses DEs in their work should be welcome. What's not appropriate, in my view, is to then claim, as the "domain" of the theory of DEs, all the disciplines that use DEs. This is the sentiment conveyed by the semantics of Joe's comment, even though he clarified that that wasn't the intent. This mismatch between the semantics and the intent was what I wanted to point out.

It's silly at best, because if you think about it, what can number theory be "counted as"? Algebra? Analysis? Geometry? DEs too, perhaps? No, it's "number theory": we had to invent a name for it because it's none of the above. The same reasoning goes for "homotopy theory" and "algebraic geometry".

I get that John has his own grievances with US professors not identifying themselves with CT, but there can also be grievances arising in people working in other areas of maths due to sentiments similar to that expressed in the semantics of Joe's comment. This will become especially important when ACT proves to be good at getting grants, because that would put ACT in a privileged position, compared to other areas of maths. I personally know group theorists who are already very dismissive of CT on technical grounds: I can only imagine what kind of bile may arise from professional jealousy. So I'd like to hope that such sentiments stay in Zulip and don't get aired publicly, because it can do ACT no favours at all.

view this post on Zulip Jules Hedges (Jun 14 2020 at 10:27):

Rongmin Lu said:

Sure. Your comment harks back to that time when Tom Leinster took John to task for excluding CS from the definition of ACT. I have that in mind, but from a different angle, which I'll try to explain below.

Wow, this thread is fascinating... I'm glad that things worked out the way they have, and not in any of the alternative ways suggested here

view this post on Zulip Jules Hedges (Jun 14 2020 at 10:33):

Incidentally: If I remember correctly, the first ACT school avoided cs applications (*) and then for the second one we explicitly reversed that while still agreeing that it was the right thing to do for the first one. In order to "bootstrap" ACT as a research community it was necessary to appear distinct from the huge beast that is categories in computer science

view this post on Zulip Jules Hedges (Jun 14 2020 at 10:33):

view this post on Zulip Jules Hedges (Jun 14 2020 at 10:35):

This is because mathematics is culturally "closed world" - there is a fixed-for-all-time list of things that "count" as mathematics. Whereas computer science is culturally "open world" - you can invent something totally new that has never been seen before, and it will probably be welcome in computer science departments

view this post on Zulip James Fairbanks (Jun 15 2020 at 02:19):

I think that ACT should include applications in CS with the exception of straight up functional programming. FP is definitely the most widespread application of CT in CS and has a research community that predates ACT as a community. Applying CT/FP ideas to some other area of Applied Math, Science, Engineering, or CS would be in ACT but applications of CT to pure math or applications of CT to pure PL would both be out of scope to me. But I’m in favor of more inclusivity than hate keeping.

view this post on Zulip (=_=) (Jun 15 2020 at 02:45):

Jules Hedges said:

This is because mathematics is culturally "closed world" - there is a fixed-for-all-time list of things that "count" as mathematics. Whereas computer science is culturally "open world" - you can invent something totally new that has never been seen before, and it will probably be welcome in computer science departments

And guess whose tweet just blew up? :upside_down:

Mathematics is culturally "closed world" - there is a fixed-for-all-time list of things that "count" as mathematics. Computer science is culturally "open world" - you can invent something totally new that has never been seen before, and probably be welcome in cs departments

- julesh (@_julesh_)

view this post on Zulip (=_=) (Jun 15 2020 at 02:53):

I wouldn't say that "there is a fixed-for-all-time list" of subjects that count as mathematics: it's just that the list changes rather slowly, reflecting the slower rate of "progress" in maths compared to many other subjects, e.g. CS. It's been said that it takes about a decade before a piece of new maths can be digested, and probably even longer than that for some substantive new maths to be built on top of that earlier piece of maths. This is, of course, part of my motivation for wanting to see more automation in how research in maths is being done: to see if that period of digestion can be shortened.

view this post on Zulip John Baez (Jun 15 2020 at 06:30):

To clarify a bit: Tom Leinster was taking me to task about the first lecture I gave in my online category theory course in 2018. In that lecture, I wanted to emphasize that my online course on applied category theory would focus on applications other than computer science because there were tons of Haskell programmers expecting me to explain monads, and I wasn't going to do that. I made the mistake of phrasing my remark as if I were giving a "definition" of ACT. Actually I don't give a fuck about definitions of subjects. As I tried to clarify later, boundaries between disciplines are mainly things I want to cross.

Also in 2018, I wanted the first ACT conference to focus on applications outside computer science because there was already such a thriving set of conferences on applications of category theory to computer science that I was afraid ACT might become just another one of those.

view this post on Zulip John Baez (Jun 15 2020 at 06:31):

By now I'm not worried about that because I feel "ACT" has its own life.

view this post on Zulip John Baez (Jun 15 2020 at 06:35):

For example, now we see things like the "Categorical Probability and Statistics" conference.

view this post on Zulip John Baez (Jun 15 2020 at 06:43):

In short, I now think "ACT" can take care of itself and I have no interest in defining it. If someone wants to define it I will do my best to ignore any limitations that might impose.

view this post on Zulip (=_=) (Jun 15 2020 at 10:16):

I think that these days, "everyone's a critic" and "the death of the author" is de rigeur, so it's more important than ever to care deeply about the semantics of what one writes, because one's detractors will examine one's words with just as much vigour as a mathematician might examine a proof.

view this post on Zulip (=_=) (Jun 15 2020 at 10:23):

I mean, just today, Noah Snyder snapped at this tweet of Jules Hedges, which led to a very testy exchange between him and Bob Coecke that included this rather colourful characterisation of pure maths.

@_julesh_ @nic_kup @coecke Wait, what? This is a truly bizarre description of the history of string diagrams...

- Noah Snyder (@NoahJSnyder)

@nic_kup To me the most obvious thing is diagrammatic algebra. Quantum algebra (Hopf & Frobenius algebras etc) was already a major topic in mathematics but @coecke's group in Oxford took string diagrams seriously and totally left the mathematicians in the dust. Now it's spread all over

- julesh (@_julesh_)

@NoahJSnyder @_julesh_ @nic_kup Have you ever talked to a quantum foundations person, a practical NLP person, anyone in social sciences, they wouldn't be able to read digit 1 or of what you talk about, nor get anything from it. This is macho math culture...

- bOb cOeCke (@coecke)

view this post on Zulip (=_=) (Jun 15 2020 at 10:32):

Rongmin Lu said:

it's more important than ever to care deeply about the semantics of what one writes

And who knows? Maybe CQM/QNLP can help with this?

view this post on Zulip Jules Hedges (Jun 15 2020 at 10:35):

Nah, it's only twitter. Disagreement drives the analytics more than anything else

view this post on Zulip Blake Pollard (Jun 24 2020 at 14:11):

John van de Wetering said:

Now that basically all completeness results that can be proven have been proven regarding ZX I don't see many ZX papers coming to ACT soon. Perhaps some general "from abstract category theory to concrete applications" history talk about ZX would be interesting though...

What are some examples of incomplete diagrammatic languages/calculi?

view this post on Zulip Jules Hedges (Jun 24 2020 at 14:14):

Lots! E.g. string diagrams for the cartesian monoidal category of sets

view this post on Zulip Jules Hedges (Jun 24 2020 at 14:14):

There are true facts about sets and functions that can't be proved by string diagrams

view this post on Zulip Jules Hedges (Jun 24 2020 at 14:17):

A random other example: The string diagram language I invented for doing game theory is hopelessly incomplete for game theory - but still extremely useful for it - it turned out later to be complete for lenses

view this post on Zulip Blake Pollard (Jun 24 2020 at 15:30):

Jules Hedges said:

There are true facts about sets and functions that can't be proved by string diagrams

Can you give an example?

view this post on Zulip Cole Comfort (Jun 24 2020 at 15:43):

Blake Pollard said:

John van de Wetering said:

Now that basically all completeness results that can be proven have been proven regarding ZX I don't see many ZX papers coming to ACT soon. Perhaps some general "from abstract category theory to concrete applications" history talk about ZX would be interesting though...

What are some examples of incomplete diagrammatic languages/calculi?

There are many, but because they haven't been proven complete they aren't written down. For example, nearly all qudit fragments are not proven to be complete; however, completeness for qudit stabilizer circuits would probably be the easiest to do.

Similarly, for linear relations over arbitrary rings (instead of fields or whatever).

view this post on Zulip Aleks Kissinger (Jun 24 2020 at 15:45):

Jules Hedges said:

Lots! E.g. string diagrams for the cartesian monoidal category of sets

That would be somewhat surprising to me. I always had in mind that cartesian categories were complete for sets and functions, in the sense of Plotkin/Hasegawa/Selinger-style completeness for traced and compact closed categories. That is, if all the boxes and wires are treated generically, i.e. as "black boxes" that could be any function between any sets, the only equations that hold in generality are copying and deleting boxes by commuting through Δ\Delta and !!.

view this post on Zulip Cole Comfort (Jun 24 2020 at 15:52):

Jules Hedges said:

Lots! E.g. string diagrams for the cartesian monoidal category of sets

I mean finite sets and functions (op) is just a Lawvere theory (and the initial one at that), so what more is there to do?

view this post on Zulip Amar Hadzihasanovic (Jun 24 2020 at 15:57):

That's op of the cocartesian category (FinSet, +)...

view this post on Zulip Amar Hadzihasanovic (Jun 24 2020 at 15:58):

I think Jules would like a presentation of ((Fin?)Set, ×).

view this post on Zulip Amar Hadzihasanovic (Jun 24 2020 at 16:01):

Which is also different from the Plotkin/Hasegawa/Selinger sense of completeness, ie "two diagrams in the language of cartesian categories are equal for every interpretation in (Set, ×) iff they are equal by the axioms of cartesian categories".

view this post on Zulip Amar Hadzihasanovic (Jun 24 2020 at 16:04):

For a while I have been replacing eg "the ZX calculus is complete for..." with "the ZX calculus is an equational presentation of..." to avoid this kind of confusion, but I don't think it has caught on ;)

view this post on Zulip Aleks Kissinger (Jun 24 2020 at 16:05):

that's indeed more accurate, but doesn't quite have the same ring to it

view this post on Zulip Aleks Kissinger (Jun 24 2020 at 16:07):

i think its too much to ask for to get a finite presentation for all of (Fin)Set, but if you fix objects to finite sets of the form BN\mathbb B^N with B\mathbb B the 2-element set, then boolean logic does the job.

view this post on Zulip Cole Comfort (Jun 24 2020 at 16:22):

Aleks Kissinger said:

that's indeed more accurate, but doesn't quite have the same ring to it

Yes , this is what Lafont does in his paper, "Towards an Algebraic Theory of Boolean Circuits."

I imagine that this works just as well for any finite set othe than 2.

view this post on Zulip Cole Comfort (Jun 24 2020 at 16:27):

Although, I am having trouble proving completeness for qudit spans (other than for the case of d=2), because you don't have nice things like projections anymore.

view this post on Zulip Jules Hedges (Jun 24 2020 at 16:45):

Amar Hadzihasanovic said:

I think Jules would like a presentation of ((Fin?)Set, ×).

Right. My gut feeling says that (FinSet,+)(FinSet, +) can be presented by string diagrams in a complete way, but (FinSet,×)(FinSet, \times) can't

view this post on Zulip Jules Hedges (Jun 24 2020 at 16:46):

On the other hand I don't have a good intuition for why completeness (eg. for ZX) is so important. I work almost always with incomplete diagrammatic languages, and have no problem at all with that

view this post on Zulip Jules Hedges (Jun 24 2020 at 16:48):

I guess it leads to syntax-based algorithms for semantic questions, which is important when your semantics is computationally hard. In game theory I do the equivalent of just thinking of ZX diagrams as a notation for matrices, and then just calculate the matrices when you need to do anything outside the diagrammatic language

view this post on Zulip Cole Comfort (Jun 24 2020 at 17:19):

Jules Hedges said:

On the other hand I don't have a good intuition for why completeness (eg. for ZX) is so important. I work almost always with incomplete diagrammatic languages, and have no problem at all with that

Without regard to computational complexity; I think it is important because finding a universal and complete representation of some concrete thing in terms of string diagrams is, in a sense, reformulating the definition of that concrete thing in this different, more compositional paradigm. Like if you want to compute a result that is of "compositional" nature , about a certain class of circuits, this alternative presentation will often be useful.

If you don't know if the presentation you are working with is complete then doing mathematics with it could be like doing mathematics about rings without the axiom for additive inverses, for example.

view this post on Zulip Amar Hadzihasanovic (Jun 24 2020 at 18:05):

Another important application of completeness is the definition of algebraic invariants. You define the invariant on the generators of your presentation and check that it is preserved by all the equations. If you have completeness, now that's an invariant of the things that you are modelling.

view this post on Zulip Amar Hadzihasanovic (Jun 24 2020 at 18:06):

Very little modern knot theory would exist if you didn't have completeness of the Reidemeister moves...

view this post on Zulip Amar Hadzihasanovic (Jun 24 2020 at 18:12):

The original purpose of pursuing completeness of the ZW calculus was to seek this kind of approach to finding invariants of classes of entangled states.

view this post on Zulip John van de Wetering (Jun 24 2020 at 21:10):

I didn't know that that was one of the original purposes of ZW. Did that programme ever succeed? As in, did ZW result in finding some such invariants?

view this post on Zulip John van de Wetering (Jun 24 2020 at 21:12):

Cole Comfort said:

Jules Hedges said:

On the other hand I don't have a good intuition for why completeness (eg. for ZX) is so important. I work almost always with incomplete diagrammatic languages, and have no problem at all with that

Without regard to computational complexity; I think it is important because finding a universal and complete representation of some concrete thing in terms of string diagrams is, in a sense, reformulating the definition of that concrete thing in this different, more compositional paradigm. Like if you want to compute a result that is of "compositional" nature , about a certain class of circuits, this alternative presentation will often be useful.

+1 for this. Knowing that Clifford ZX + Euler decomposition = completeness, is very satisfying from a foundational standpoint, as it shows what the crucial structure is that is present in qubit quantum computing

view this post on Zulip Chad Nester (Jun 25 2020 at 07:55):

I've found it difficult to convince many people that "really applied" category theory is worthwhile. Those working in the application domain don't understand what it is or why they would want it, and mathematicians tend not to be interested because it doesn't usually involve novel mathematics (which is a good thing for applications).

view this post on Zulip Jules Hedges (Jun 25 2020 at 09:12):

Chad Nester said:

I've found it difficult to convince many people that "really applied" category theory is worthwhile. Those working in the application domain don't understand what it is or why they would want it, and mathematicians tend not to be interested because it doesn't usually involve novel mathematics (which is a good thing for applications).

Right. The burden of proof is very much on us to do something useful

view this post on Zulip Jules Hedges (Jun 25 2020 at 09:13):

We would like to be toolsmiths, but for social reasons we can't just create a new type of tool and have people buy it, we have to be competent enough users of our own tools to demonstrate they are useful to people

view this post on Zulip Morgan Rogers (he/him) (Jun 25 2020 at 09:55):

That rings true in many branches of category theory, and in the wider mathematics community. People can get so invested in their subjects and methods due to this "burden of proof" overhead cost that they ultimately lose sight of the actual limitations of their work, so that the cycle repeats when the next generation has to innovate and demonstrate the value of their own methods by overcoming those limitations...
I guessed that intellectual inertia would be a good name for this phenomenon, and having looked it up, it seems that that is a legitimate term for it.

view this post on Zulip Jules Hedges (Jun 25 2020 at 09:58):

I don't think all ACTists (or in any other subject) need to worry about this. A few people getting their hands dirty can support many more "in the back"

view this post on Zulip Jules Hedges (Jun 25 2020 at 09:59):

There does seem to be 3 distinct groups now, because behind them are all the pure category theorists who couldn't care less about applications

view this post on Zulip Jules Hedges (Jun 25 2020 at 10:00):

I think that's an entirely reasonable way to organise a subject

view this post on Zulip Jules Hedges (Jun 25 2020 at 10:03):

E.g. I've never seen an algebraic geometry grant application, but I would imagine that a few people doing applications of AG (eg. in computer graphics, number theory, cryptography etc) are able to support a much bigger population doing pure theory. Same for algebraic topology, and probably most pure maths fields

view this post on Zulip Bob Haugen (Jun 25 2020 at 11:08):

Chad Nester said:

I've found it difficult to convince many people that "really applied" category theory is worthwhile. Those working in the application domain don't understand what it is or why they would want it, and mathematicians tend not to be interested because it doesn't usually involve novel mathematics (which is a good thing for applications).

I'll try to explain my own case a bit and see if it makes sense to y'all.

I work in two application domains: economic networks and software for same. I want to be convinced, and am picking my way toward being convinced very very slowly. To be fully convinced, I will need to be able to translate applied cats to something that makes sense to me and other practitioners in economic networks.

String diagrams do make sense to me and my colleagues, so we are using those, naively and possibly incorrectly at times, but they fit and they work for us as a visual language.

I have two main impediments to moving faster in applying and translating more category theory to me and them.

  1. I don't have a good enough mathematical education to be able to read the language of symbolic math fluently or often at all without tedious effort. I am slowly making the effort (eg picking my way thru https://www.abstractmath.org/MM/MMSymLang.htm ) but I also have actual work to do.
  2. Category theory abounds with jargon. This is all normal for a complex specialized field, and I am not really complaining about it, but there's a lot or it to learn.

One possible avenue of improvement would be for category theorists to work with domain specialists. I think some of that is happening now and find those efforts to be educational for me even if they are not in one of my domains.

view this post on Zulip Jules Hedges (Jun 25 2020 at 11:19):

Bob Haugen said:

One possible avenue of improvement would be for category theorists to work with domain specialists. I think some of that is happening now and find those efforts to be educational for me even if they are not in one of my domains.

Yes, this. I'd go as far as to claim this is the only reasonable way for most ACT projects to make real progress, deeply understand both category theory and an application domain is just too heavy a demand for one human brain (possibly except for the occasional genius, but they are exceptions). If you haven't seen it, I talked specifically about this at the end of my ACT@UCR seminar recently

view this post on Zulip Jules Hedges (Jun 25 2020 at 11:21):

Ah, I thought I was quoting myself. This thought is from a blog post I wrote back in the dark ages, ie. early 2018, https://julesh.com/2018/02/27/the-rising-sea-in-applied-mathematics/ : "The emerging field of applied category theory is attempting to close the gap from both sides between category theory and (certain) applications. This is hard because the same person needs to know about both category theory and the problem domain, which is quite a heavy demand on a human brain. One part of this is to present category theory itself in more down-to-earth terms that emphasise intuition over structure. If you want to prove theorems it might be useful to know that something is just a left Kan extension in the category of who-knows-what, but if you want to apply it to a problem domain that has never heard of category theory, something different is needed."

view this post on Zulip Bob Haugen (Jun 25 2020 at 11:26):

Jules Hedges said:

If you haven't seen it, I talked specifically about this at the end of my ACT@UCR seminar recently

This one? https://www.youtube.com/watch?v=Kwflmrd2AfM

view this post on Zulip Jules Hedges (Jun 25 2020 at 11:27):

That's it

view this post on Zulip Jules Hedges (Jun 25 2020 at 11:27):

Go to the conclusions section, a bit before the end

view this post on Zulip Jules Hedges (Jun 25 2020 at 11:30):

tl;dr I was mostly pessimistic, partly because I'm me, and partly because interdisciplinary work is really hard

view this post on Zulip Bob Haugen (Jun 25 2020 at 12:24):

Jules Hedges said:

tl;dr I was mostly pessimistic, partly because I'm me, and partly because interdisciplinary work is really hard

True that, but they might also be coming together....(the cats and some app domains)

view this post on Zulip Fabrizio Genovese (Jun 25 2020 at 12:36):

Jules Hedges said:

tl;dr I was mostly pessimistic, partly because I'm me, and partly because interdisciplinary work is really hard

I share your pessimism.

view this post on Zulip Blake Pollard (Jun 25 2020 at 16:25):

It is also really fun! At first when I started at NIST trying to force category theory on smart gird/power systems people, I was very discouraged because it felt like i) I was selling snake-oil and ii) I was starting another PhD in a new field, but where you only have a year to do anything (which is typical of postdocs I guess). Then came laser interferometers and their control systems, additive manufacturing (aka zapping powders with lasers), industrial robot programming paradigms, and today I'm reading about NASA's efforts on an model based systems engineering approach to designing interplanetary spacecraft powered by nuclear thermal propulsion systems. Of course, sometimes interactions with domain folks don't pan out or lead to anything groundbreaking on either the math or application side, but now there are a few more people out there who aren't as scared of functors and I can talk reasonably intelligibly with folks (as mired in jargon as we are) trying to soup up our grid to enable a much cooler society.

view this post on Zulip Blake Pollard (Jun 25 2020 at 16:28):

That said, despite hanging around in the ACT world for a number of years now, my CT knowledge truncates pretty low and I still struggle to parse a lot of what gets said on here and I still have to talk to folks whose brains are capable of climbing higher on the CT ladder and ask 'dumb' questions every 15 seconds. I'd also say that my physics background helps a lot with dealing with some of the quirks of some of the domains.

view this post on Zulip Blake Pollard (Jun 25 2020 at 16:29):

But it sounds like @Bob Haugen has a great opportunity for someone coming a bit more from the category theory side to embed a bit in an organization/collaboration and see what happens.

view this post on Zulip James Fairbanks (Jun 25 2020 at 16:31):

Yeah I think that the killer app for ACT is going to be software that deals with hierarchical complexity because it gets the abstractions right. CT provides tools for understanding why a piece of math works the way it does, and that understanding is essential to getting useful software abstractions. Software design is the art of abstraction, abstraction before understanding is doomed to failure. CT makes understanding easier so it makes software design easier.

view this post on Zulip Bob Haugen (Jun 25 2020 at 16:42):

Blake Pollard said:

It is also really fun! At first when I started at NIST trying to force category theory on smart gird/power systems people, I was very discouraged because it felt like i) I was selling snake-oil and ii) I was starting another PhD in a new field, but where you only have a year to do anything (which is typical of postdocs I guess). Then came laser interferometers and their control systems, additive manufacturing (aka zapping powders with lasers), industrial robot programming paradigms, and today I'm reading about NASA's efforts on an model based systems engineering approach to designing interplanetary spacecraft powered by nuclear thermal propulsion systems. Of course, sometimes interactions with domain folks don't pan out or lead to anything groundbreaking on either the math or application side, but now there are a few more people out there who aren't as scared of functors and I can talk reasonably intelligibly with folks (as mired in jargon as we are) trying to soup up our grid to enable a much cooler society.

We read your paper "Compositional models for power systems" sent to us by a guy who works for the EPA so you must have gotten through to some people.... ;-)

view this post on Zulip Bob Haugen (Jun 25 2020 at 18:24):

Jules Hedges said:

Ah, I thought I was quoting myself.... from a blog post I wrote back in the dark ages, ie. early 2018, https://julesh.com/2018/02/27/the-rising-sea-in-applied-mathematics/...

Reading the blog post before watching the video. It's wonderful! I'm swimming in it for awhile...
Thank you!

view this post on Zulip Blake Pollard (Jun 25 2020 at 19:39):

Great to hear folks are reading our work! There is still a lot more to be said about using CT in the context of model-driven engineering. Hopefully more papers to follow touching smart grid, but other domains as well.

view this post on Zulip Jules Hedges (Jun 25 2020 at 21:18):

This blog post was the product of a very short moment in time, when ACT existed but practically nobody had heard of it

view this post on Zulip Chad Nester (Sep 09 2020 at 08:19):

This has been on my mind again recently. I think the proposed benefit of categorical methods is conceptual, in the sense that I see two main reasons to rework something in the language of category theory:

First, describing your application domain categorically makes it conceptually interoperable with everything else so described. This has (largely) been the effect of category theory on mathematics, to celebrated effect.

Second is the related idea that category theory has the potential to make things conceptually tractable. Thanks in part to the rise of computing, the systems in our lives are tending towards complete incomprehensibility, to the detriment of most. I hope that taking these application domains seriously will lead to better understanding and abstraction of them, which ought to help a litttle.

view this post on Zulip Chad Nester (Sep 09 2020 at 08:31):

The first idea, conceptual interoperability, strikes me as the more marketable one. Interoperability of systems is a massive research area with real-world effects. Whether or not conceptual interoperability leads to actual interoperability remains to be seen, but I'd guess it's at least a necessary condition.

view this post on Zulip Chad Nester (Sep 09 2020 at 08:33):

Also important is to point out that this is less of a magic pill for interoperability than a form extremely invasive and painful surgery with a long recovery time.

view this post on Zulip Chad Nester (Sep 09 2020 at 08:50):

Jules Hedges said:

Right. The burden of proof is very much on us to do something useful

We would like to be toolsmiths, but for social reasons we can't just create a new type of tool and have people buy it, we have to be competent enough users of our own tools to demonstrate they are useful to people

I'm not sure that "tool" is the right word to use here. I propose instead that what we create are ways of seeing.

view this post on Zulip Morgan Rogers (he/him) (Sep 09 2020 at 09:24):

A telescope is a tool that gives the user a new way of seeing, and some categorical gadgets are called lenses; that is, the terminology is not incompatible :stuck_out_tongue_wink:

view this post on Zulip Jules Hedges (Sep 09 2020 at 10:04):

It's definitely true that category theory is super useful conceptually. But I try not to evangelise it from that point of view. I feel like because this benefit can't be quantified or pinned down, this is leading to the hype thing where lots of people seem to think that they ought to learn category theory but don't really know why. I try to only talk about instances where category theory does actual concrete work for me that couldn't be replaced with a different tool

view this post on Zulip Jules Hedges (Sep 09 2020 at 10:09):

The boundary between "conceptual" and "concrete work" is a bit blurry obviously. For example I consider soundness & completeness of string diagrams to be "concrete work"