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: practice: industry

Topic: visual programming

Antonin Delpeuch (Apr 21 2020 at 12:11):

Let's talk about visual programming! It is still popular in my industry (Extract-Transform-Load systems). This pipes.digital tool (https://www.pipes.digital/) was just launched and is inspired by Yahoo Pipes, which pioneered the concept years ago. Their graphs are just string diagrams for cartesian categories, so it's really in the scope of ACT. Statebox has been advocating for visual programming too: https://blog.statebox.org/why-visual-programming-doesnt-suck-2c1ece2a414e?gi=8bc316e16e3c @Jelle Herold @Fabrizio Genovese

Antonin Delpeuch (Apr 21 2020 at 12:14):

I am currently working on implementing similar ideas in OpenRefine (https://github.com/OpenRefine/OpenRefine), based on a categorical model I presented last year at ACT: https://arxiv.org/abs/1906.05937

Blake Pollard (Apr 21 2020 at 14:26):

Very cool! We (the NIST crew) have started to use 'plumbing' as an analogy for explaining to folks the way we see ACT being useful in broader data wrangling and model-based system engineering contexts.

For starters, if everything is working nicely, you can't see the pipes and don't ever really think about them. For old systems, the pipes could be really screwed up, leaking a bunch, letting in groundwater etc. (like most oldish cities in the US), but for the most part water comes out when you turn the faucet on... so who cares. For critical systems, it might be time for an upgrade.

When you want to build or design something, you typically don't start designing new pipes. The pipes are already out there, you just might need someone more knowledgeable about plumbing to figure out which pipes to use where. I guess here the existing pipes are existing gizmos in CT and really wherever. Also, just because the two ends of a pipe type-check with a missing piece of your system, it doesn't mean you should just shove that pipe in there.

Blake Pollard (Apr 21 2020 at 14:30):

Maybe the part of this perspective that is relevant for visual programming is in regard to considering who the 'user' is. I guess we'd like to see tools with wide audiences where there is very little required knowledge of CT (maybe some programming etc.), but we also have been thinking about tools for the toolsmiths, and perhaps those folks know some more CT in order to figure out which new features might be useful in the tools and how to add them sanely and without breaking other stuff.

Blake Pollard (Apr 21 2020 at 14:34):

I remember your talk on dataflow diagrams in Oxford with all the fancy sheets.

Fabrizio Genovese (Apr 21 2020 at 14:39):

I think there are two things that are essential in visual programming:
1 - It still needs a text interface. I think visual programming is great for visual debugging but experienced programmers will feel very much hindered in having to use drag&drop features to draw diagrams
2 - It needs powerful abstractions. Visual programming usually does not work because plumbing becomes very quickly spaghetti, and at that point all the benefits of having a visual perspective are lost. This is one of the main reasons why we deal with brick diagrams more than string diagrams. In any case, the real deal is being able to box/compose stuff, so that the piping can be hidden.

Blake Pollard (Apr 21 2020 at 14:39):

Is there some kind of repository of serialization formats for various flavors of CT gizmo, diagrams in particular? I'm thinking of the k-d trees stuff for brick diagrams and their relationship to string diagrams a la @Jules Hedges and @Jelle Herold . I gather Catlab.jl has various levels of exchange formats, maybe bottoming out in JSON @Evan Patterson ?

Fabrizio Genovese (Apr 21 2020 at 14:39):

Point 2 is actually why the only kind of visual programming that does not suck is act based programming. Abstraction capabilities will literally explode in your face if they do not live in a well defined formal environment :slight_smile:

Fabrizio Genovese (Apr 21 2020 at 14:40):

Anyway we will have some awesome news about our programming language by the end of the month, stay tuned :D

Jules Hedges (Apr 21 2020 at 14:42):

There is no repository. The current state of the art is just to ask people, I think

Fabrizio Genovese (Apr 21 2020 at 14:43):

We are actively maintaining one, Typedefs.

Fabrizio Genovese (Apr 21 2020 at 14:44):

typedefs.com

Fabrizio Genovese (Apr 21 2020 at 14:45):

The idea of typedefs is that it's a universal format for types and terms. We support all the types recursively made using variables, products, coproducts and $\mu$

Fabrizio Genovese (Apr 21 2020 at 14:45):

Then for all these types you automagically get a serialization/deserialization format, as well as other exchange formats (we implemented JSon recently)

Fabrizio Genovese (Apr 21 2020 at 14:47):

We also have a specialization backend. This means that in typedefs you define natural numbers as being $\mu(1 + X)$ but actually if you gave this the name list then it gets automatically interpreted as List in languages that have this type, such as Haskell

Fabrizio Genovese (Apr 21 2020 at 14:47):

We also support serialization for types using type variables, such as List a, but in this case we don't support terms since the very concept of term doesn't make much sense until you fix the variables

Fabrizio Genovese (Apr 21 2020 at 14:49):

So for instance we are using JSON to communicate with our typed core. But actually the JSON we feed is jsut the JSON version of typedefs, which gets internally converted to typedefs first and to Idris terms then, automatically

Fabrizio Genovese (Apr 21 2020 at 14:50):

@Alex Gryzlov, @marcosh and @Sjoerd Visscher will be able to tell you way better than me how this works from a programmer perspective :slight_smile:

Blake Pollard (Apr 21 2020 at 14:52):

Where do brick diagrams sit? As typedef terms?

Fabrizio Genovese (Apr 21 2020 at 14:53):

The idea is that in typdefs you can express trees of terms, so if you give to every brick of your diagram a Tdef and a term, then you can pass the whole tree as a Tdef term

Fabrizio Genovese (Apr 21 2020 at 14:53):

Where the nodes tell you if the composition is horizontal or vertical

Fabrizio Genovese (Apr 21 2020 at 14:54):

For instance, in Idris you can do:

data Tree o m = Tensor (Tree o m) (Tree o m)
              | Sequence (Tree o m) (Tree o m)
              | Sym o o
              | Id o
              | Mor m

Fabrizio Genovese (Apr 21 2020 at 14:55):

Now this is easily convertible to a Tdef and vice-versa. Clearly this is the inductive definition for a string diagram, where m represents a morphism and o represents an object.

Jules Hedges (Apr 21 2020 at 14:55):

This is representative of one family of representations of diagrams. Another family of representations is the graphical ones, eg Quantomatic. Another one again is the ones based on foliations, like homotopy.io

Reid Barton (Apr 21 2020 at 14:55):

What is a brick diagram?

Fabrizio Genovese (Apr 21 2020 at 14:56):

So, for instance, using Tdefs we are able to exchange these things back and forth with our graphical editor, and evaluating the brick diagrams in a given semantic category

Fabrizio Genovese (Apr 21 2020 at 14:56):

Intuitively, a string diagrams with no wires

Reid Barton (Apr 21 2020 at 14:56):

OK, I think I see.

Jules Hedges (Apr 21 2020 at 14:56):

Brick diagrams: https://arxiv.org/abs/1908.10660

Fabrizio Genovese (Apr 21 2020 at 14:57):

Jules Hedges said:

This is representative of one family of representations of diagrams. Another family of representations is the graphical ones, eg Quantomatic. Another one again is the ones based on foliations, like homotopy.io

I am pretty sure you can represent homotopy.io diagrams as trees as well

Fabrizio Genovese (Apr 21 2020 at 14:57):

you just have more decorations on the nodes, but in the end you can still read surface diagram as a composition of morphisms

Fabrizio Genovese (Apr 21 2020 at 14:58):

This obviously is wrt to the conceptual information encoded in the diagram. If you also want to store positioning etc then you'll need more complicated stuff

Fabrizio Genovese (Apr 21 2020 at 14:59):

But in general I don't see why you couldn't store quantomatic and homotopy.io diagrams using an inductive type. In the worst case, you just store them as a string, trivializing the problem

Jules Hedges (Apr 21 2020 at 14:59):

Making graphs into an inductive datatype is a bit of a notorious problem, but I think it's been worked out now

Fabrizio Genovese (Apr 21 2020 at 15:00):

Well, yes and no. I am not sugggesting to convert a given graph to an inductive datatype. I am suggesting to make the datatype along with whatever you do

Fabrizio Genovese (Apr 21 2020 at 15:00):

For instance in homotopy.io you literally "make" diagrams by composing stuff. every time you compose, you can "update" your term in the inductive type

Fabrizio Genovese (Apr 21 2020 at 15:01):

This is also how our editor works btw. As you change the diagram, the tree view is updated in real time to reflect this

Fabrizio Genovese (Apr 21 2020 at 15:01):

(and if homotopy.io and quantomatic are implemented modularly and wisely, i don't think it would be a huge problem to actually implement this functionality there)

Fabrizio Genovese (Apr 21 2020 at 15:03):

Anyway we'd be superhappy if you would like to try Tdefs. All the work we do on it is public. Feel free to make pull requests/whatever :D

Jules Hedges (Apr 21 2020 at 15:05):

Is the main thing needed new backends? (Is that the right terminology?)

Jules Hedges (Apr 21 2020 at 15:06):

Teaching it about a bunch of different formats?

Fabrizio Genovese (Apr 21 2020 at 15:07):

Well, if you implement a TDef backend in a new language, then you can exchange terms and types between that language and the ones already supported

Fabrizio Genovese (Apr 21 2020 at 15:07):

so yes, I'd say that's the most important thing

Blake Pollard (Apr 21 2020 at 15:09):

So a 'backend' for TDefs is the same as a semantics for the string diagrams as rendered by your editor?

Fabrizio Genovese (Apr 21 2020 at 15:10):

Hm, not really. A backend for TDefs is a programming language in which TDefs is implemented

Fabrizio Genovese (Apr 21 2020 at 15:10):

the idea is that since you can represent a string diagram as a typedef, you can literally define a StringDiagram TDef and then exchange terms of type StringDiagram between all such languages.

Blake Pollard (Apr 21 2020 at 15:10):

Gotcha. So Idris is kind of the self-referential one, but you can also currently go from TDefs to Haskell?

Fabrizio Genovese (Apr 21 2020 at 15:11):

There is a Hakell backend, yes. So, in principle, you should be able to exchange string diagrams between Idris and Haskell, or Haskell and Haskell, or Idris and Idris

Fabrizio Genovese (Apr 21 2020 at 15:11):

In whatever serialization format is implemented, e.g. JSON, binary, S-expression

Fabrizio Genovese (Apr 21 2020 at 15:14):

Example: I have some Haskell visual thing that manipulates string diagrams. But I am all about formal verification so I want to actually evaluate them in Idris, even if I draw them in Haskell. Then I can use TDefs, create an appropriate StringDiagram TDef, and exchange the string diagrams I draw in Haskell as StringDiagram terms. This is better than exchanging this information "raw" since it comes with guarantees. That is, if the term is bad or the typedefinition you gave me is bad, TDef will throw errors

Fabrizio Genovese (Apr 21 2020 at 15:16):

I can also define an EvaluatedDiagram TDef so that Idris can give the result back to Haskell. Then again, the actual communication between the two can be done in any of the serialization formats TDefs supports. So you don't have to come up with a serialization format and a parser yourself, as long as what you do can be expressed as a type of an inductive term

Blake Pollard (Apr 21 2020 at 15:17):

Ok, gotcha. So that would be an example of using TDef to make your life easier in 'verifying' some Haskell code, at least up to the sanity of the StringDiagram TDef you created.

Fabrizio Genovese (Apr 21 2020 at 15:19):

Yes. So you can define that Tree o m as above, for instance, both in Haskell and Idris. And then exchange string diagrams as terms of that Tree o m thing. Clearly Idris won't be able to say if the diagram you made in Haskell is what it should be, but you can be sure that "non well-formed diagrams" basically won't be exchangeable

Blake Pollard (Apr 21 2020 at 15:19):

Fabrizio Genovese said:

For instance, in Idris you can do:

data Tree o m = Tensor (Tree o m) (Tree o m)
              | Sequence (Tree o m) (Tree o m)
              | Sym o o
              | Id o
              | Mor m

So you're saying this is an inductive datatype for a string diagram in Idris, or very similarly a Tdef.

Fabrizio Genovese (Apr 21 2020 at 15:20):

This is the thing the TDefs will convert to in IdrisLand

Fabrizio Genovese (Apr 21 2020 at 15:20):

Actually, we are going live and stream about this in 40 mins

Fabrizio Genovese (Apr 21 2020 at 15:20):

We have exactly to implement the Tdef for that thing today

Fabrizio Genovese (Apr 21 2020 at 15:20):

So you can just join if you want to :D

Blake Pollard (Apr 21 2020 at 15:21):

And the brick diagram stuff is a way to specify trees that almost give you string diagrams up to some annoyingness about identities (related to the recursion stopping with one thing per brick?) and pinwheels.

Fabrizio Genovese (Apr 21 2020 at 15:22):

So the idea is that this is the internal Idris def we are using to represent a string diagram. It somehow matches the one we use in our editor. Today we will put Tdefs on top of it, so that inbound TDef terms in Json will convert to the corresponding TDef first and to that thing then

Blake Pollard (Apr 21 2020 at 15:22):

Haha ok, sounds good. I'll do that.

Fabrizio Genovese (Apr 21 2020 at 15:22):

Blake Pollard said:

And the brick diagram stuff is a way to specify trees that almost give you string diagrams up to some annoyingness about identities (related to the recursion stopping with one thing per brick?) and pinwheels.

I guess so, yea

Fabrizio Genovese (Apr 21 2020 at 15:23):

The thing is that string diagrams are invariant wrt topological deformation, but when you actually write them down you wanna keep these things distinct

Fabrizio Genovese (Apr 21 2020 at 15:23):

Like, I am looking at _a_ string diagram, that is, a representative of its class. But different representatives are displayed differently, obviously

Fabrizio Genovese (Apr 21 2020 at 15:24):

So the tree format, which is not invariant wrt topological deformation, is an ok way to ship these over to idris. Then in idris we have a formally verified implementation of free SMCs for which these structures are invariant.

Fabrizio Genovese (Apr 21 2020 at 15:25):

So, when interpreted as a morphism in the freeSMC, it will be actually "squashed" to be equal to any other representative. But for very obvious reasons we want this step to be done _inside_ Idris, which is formally verified, and not outside it :D

Blake Pollard (Apr 21 2020 at 15:28):

Gotcha. Is it easy to see what happens to the trees when you do certain topological moves on the string diagrams?

Fabrizio Genovese (Apr 21 2020 at 15:28):

Hm, that I do not know. What I can guarantee you is that two trees expressing equivalent string diagrams will become the same morphism in our SMC implementation :slight_smile:

Jules Hedges (Apr 21 2020 at 15:28):

They're called "commuting conversions" if you see them as proof trees in a fragment of linear logic

Jules Hedges (Apr 21 2020 at 15:29):

They're the tree rotations that come from cut elimination

Blake Pollard (Apr 21 2020 at 15:30):

Gotcha. Very cool. Still a little fuzzy in my mind, but I think I'm getting it. So you guys taught Idris how to squash these things coherently.

Fabrizio Genovese (Apr 21 2020 at 15:30):

Yes, and that has been literally a nightmare

Jules Hedges (Apr 21 2020 at 15:31):

(I think you can also find the same things in computational geometry, as rebalancing operations on kd trees)

Fabrizio Genovese (Apr 21 2020 at 15:31):

Basically we are using cartographer as a data structure, which represents string diagrams up to isomorphisms, and then we used some (very reasonable and innocent) postulates about their structure to obtain a strict equality

Blake Pollard (Apr 21 2020 at 15:32):

Yea, I can imagine how the computational geometry people are holding all kinds of secrets.

Jules Hedges (Apr 21 2020 at 15:33):

This topic is (higher) category theory + algebraic topology + combinatorics + computational geometry + .......

Jules Hedges (Apr 21 2020 at 15:36):

One thing I'd really like to do after moving the Strathclyde is taking Malin Altmüller's existing Agda code for the operad of rotation systems, and hire a UI programmer to plug a nice javascript front end into it. I have high hopes for that representation...

Jules Hedges (Apr 21 2020 at 15:38):

Thinking about compiling from that representation to kd trees is on my todo list

Blake Pollard (Apr 21 2020 at 15:40):

Never heard of the 'operad of roatation systems.'

Jules Hedges (Apr 21 2020 at 15:43):

Rotation systems are an existing combinatorial representation of 2-dimensional polygonal cell complexes. Where for each vertex you associate a circular list of the vertices that it is joined to by an edge, going clockwise. Malin (she's Ross Duncan's PhD student) worked out a version with open boundaries, for representing string diagrams, and apparently proved in Agda that it defines an operad (which sounds extremely hard to me)

Jules Hedges (Apr 21 2020 at 15:44):

Course "2 dimensional polygonal cell complex" is the same thing as a planar graph

Jules Hedges (Apr 21 2020 at 15:46):

Part of the reason I like this representation is that I nearly reinvented it, or rather I was trying to invent its graph dual, where you list the faces and then give a circular list of the faces that share an edge with it

Jules Hedges (Apr 21 2020 at 15:48):

It's arguably the most natural representation for diagrams for non-symmetric monoidal categories with the additional property that scalars commute with everything. (If you don't have that technical condition then things get very nasty)

Blake Pollard (Apr 21 2020 at 15:51):

What are the scalars? I gather they're the 0-d things in cell complex world, but I'm imagining swinging around a node with a bunch of wires sticking out.

Jules Hedges (Apr 21 2020 at 15:53):

By scalar I mean a sub-diagram with empty boundary, so it's topologically disconnected

Jules Hedges (Apr 21 2020 at 15:55):

You want the property that they can all be pulled to the outside, otherwise you get a multiset of them hanging around inside each face of the diagram and can be nested arbitrarily deeply, which is a pretty disgusting situation

Blake Pollard (Apr 21 2020 at 15:56):

Gotcha. So is composition in this operard sticking entire 2d cell complexes in others so that the wires match, kind of wiring diagram style?

Jules Hedges (Apr 21 2020 at 15:56):

Yeah, think so

Jules Hedges (Apr 21 2020 at 15:57):

She had the extremely nice idea of imagining a "node at infinity" in every string diagram, with both the left boundary and right boundary connecting to it. Apparently that's an old trick in combinatorics

Blake Pollard (Apr 21 2020 at 15:58):

Haha cool. Like some projective business.

Blake Pollard (Apr 21 2020 at 15:59):

That also reminds me a bit of stuff Daniel Cicala was doing in ZX-world by just adding a 'boundary type.'

Fabrizio Genovese (Apr 21 2020 at 16:00):

twitch.tv/statebox

Blake Pollard (Apr 21 2020 at 16:00):

So things are coming and going from/to infinity until you compose and then those things are in your scope.

Blake Pollard (Apr 21 2020 at 16:01):

Nice. Thanks @Fabrizio Genovese !

Fabrizio Genovese (Apr 21 2020 at 16:01):

We'll start soon

Reid Barton (Apr 21 2020 at 16:01):

Is there a writeup of Malin's work available?

Reid Barton (Apr 21 2020 at 16:02):

Also, is there anything written about the Idris SMC implementation?

Jules Hedges (Apr 21 2020 at 16:02):

Last time I asked no. There should be a paper some time

Fabrizio Genovese (Apr 21 2020 at 16:02):

web session read only: tmate.io/t/ro-qf7R4SM6MCpGCzZvCUBMv5Cck
ssh session read only: ssh ro-qf7R4SM6MCpGCzZvCUBMv5Cck@lon1.tmate.io

Fabrizio Genovese (Apr 21 2020 at 16:03):

If you wanna look at the code :slight_smile:

Fabrizio Genovese (Apr 21 2020 at 16:03):

We are on :slight_smile:

Jules Hedges (Apr 21 2020 at 16:03):

She talked about it at SYCO.... 5? There should be a video in existence, but sadly it's hiding somewhere on the Uni.Birmingham's heavily over engineered video platform

Reid Barton (Apr 21 2020 at 16:04):

Ah yes :video_camera: :locked:

Jules Hedges (Apr 21 2020 at 16:06):

https://bham.cloud.panopto.eu/Panopto/Pages/Viewer.aspx?id=c8b3d06e-ad8e-4778-b284-aabe01002bf1

Reid Barton (Apr 21 2020 at 16:10):

Ah, thanks!

Georgios Bakirtzis (Jun 02 2020 at 15:32):

I'm leaving this classic here for some important things a visual language must overcome (i.e., the problems with visual languages) to be truly useful
http://www.cs.cmu.edu/~bam/papers/vltax2.pdf

keorn (Jun 07 2021 at 08:22):

https://enso.org/ has relatively clean formalism under the hood. Even if one does not use the language they developed, their open source visual IDE framework may be interesting.

Bob Coecke (Apr 15 2022 at 09:20):

I had two interviews with Moor Strategy and Insight on our uses oof category theory in industry:

Bob Coecke (Apr 15 2022 at 09:21):

https://www.youtube.com/watch?v=EBPd8UyllfQ&t=2s

Bob Coecke (Apr 15 2022 at 09:21):

https://www.youtube.com/watch?v=y-Vt5HXBga4

Bob Coecke (Apr 15 2022 at 09:22):

The same work also appeared twice in Forbes, with a a focus on lambeq:

Bob Coecke (Apr 15 2022 at 09:23):

https://www.forbes.com/sites/moorinsights/2021/10/13/cambridge-quantum-makes-quantum-natural-language-processing-a-reality/

Bob Coecke (Apr 15 2022 at 09:23):

https://www.forbes.com/sites/moorinsights/2022/04/12/quantinuum-enhances-the-worlds-first-quantum-natural-language-processing-toolkit-making-it-even-more-powerful/

Bob Coecke (Apr 15 2022 at 09:25):

Happy to share more info about the broad use of categorical quantum mechanics (at least 6 companies) & DisCoCat (at least 3 companies) in quantum industry, or the state of quantum industry more generally.