Support for Commutative Diagrams

[jpfairbanks]

Could we represent commutative diagrams in Catlab? Isn't a diagram D in category C just a functor F: D --> C. The data you pass to the functor function specifies a map from objects/homs of D to objects/homs of C. So having a struct for that input (rather than passing it as a tuple of arguments to a function would be a good first step. One of the benefits would be to make drawing commutative diagram as easy as it is currently to draw wiring diagrams.

I'm thinking of the fact that many data structures can be described with a commutative diagram and then an instance of that structure is a functor into Set. Like for example a graph G is a functor G: Gr --> Set where Gr is

We could define julia types diagrams whose instances are functors into Set and then do pushouts to represent a type of multiple inheritance. If you have a functor F:A-->B between diagrams, and interpret S:A-->Set, T:B-->Set as instances of those types and then a natural transformation alpha(F): S-->T. If you build a span of types F:A-->B, G:A-->C then you can do a push G along F to get a type B+C. And you want a functor U: B+C --> Set to be an instance of B+C consistent with S and T

Types that are like graphs with metadata are good candidate for this framework. For example, I want a graph where every edge has a weight, every vertex has a color which in inherits from Graph. Another type of graph has positions on the earth for each vertex and a population for each position. I can combine these types to get "graphs where each edge has a weight and each vertex has a color and position, and those positions have populations."

[epatters]

These are all really nice ideas. I like your illustration too.

You're right that a diagram of shape D in a category C is just a functor D -> C, and that lots of graph-like data structures can be described in this way. For many examples, including labeled/attributed graphs, see Sec. 2 of my 2019 paper and also Spivak's 2009 paper. I'm a big fan of this perspective. I like to think of it as the beginning of categorical logic, where one can already see the fundamental dictionary of categorical logic (categories as theories, functors as models, natural transformations as model homomorphisms) without the complexity of richer logical systems.

I agree that we should develop good data structures for representing diagrams. It would also be fun and useful to draw commutative diagrams algorithmically. We could start with one of Graphviz's undirected layouts, but there is a geometric aspect to drawing satisfying commutative diagrams that I suspect Graphviz will not capture. I wonder if there is any literature on automated layout of commutative diagrams.

[jpfairbanks]

Yeah I was thinking about the talk you gave at Riverside when I came up with that example. If we take the CS perspective on your paper where we treat C as defining a type and C-Insts as the instances. I think we can do a Categorical Type System embedded in Julia you could do arbitrary pushouts to implement multiple inheritance. Maybe this could get implemented using traits to formalize what people are doing when they use traits to communicate information about types that doesn't fit nicely into the inheritance system.