Devreal

Scale By The Bay 2020: Juan Pablo Romero, A tour of String diagrams and Monoidal categories

Scale By The Bay 2020: Juan Pablo Romero, A tour of String diagrams and Monoidal categories

Recording: Scale By The Bay 2020: Juan Pablo Romero, A tour of String diagrams and Monoidal categories

[Music] so hello my name is juan pablo romero i would like to take you on a tour on string diagrams and monetile categories i have a few goals on this talk first of all i'd like to show you why manuela categories are a good modeling tool for certain class of domains also i'd like to show how many other categories can be represented graphically via string diagrams and given the time constraint i'll go rather quickly but please don't hesitate to ask questions after the presentation before starting i would like to mention four exceptional resources in my opinion um the first of all first one is applied category theory by fong and spivak i think this is more or less well known in the community has a broad range of applications databases resource management etc the second one i don't think it's it's as well known personally because it's not specifically about um you know computer science but i think it's fascinating it really shows the power of model categories to model like a broad range of um phenomena ranging from linear algebra logic physics um computer science etc i put the full reference um at the end of the presentation i also this is an interesting book as well um if you're interested in quantum computation presented in a non-traditional way uh this book starts very slowly building the length the diamatic language that we're going to use and then eventually it just swaps into um quantum computation and this is this is the the the phd this is this is from one of the authors it's much faster just goes for it's hardcore but it goes straight to the to the point anyway so let's talk about processes first consider the following examples a this is a scala function just sort consider also this mathematical function or also a cooking recipe some ingredients and there's an output um a two by three matrix such as this and a usb cord right taking a um an input device and not into an output device all these examples can be described in a very general way as processes so we will define a process as anything that has zero or more inputs and zero more outputs and it can be represented by a box uh with two set of wires right inputs on the left and outputs on the right the examples that we saw before can be represented as diagrams in this way so this is the certain function this is the mathematical function cooking is clearly a process right taking some some material so some ingredients into a dish a usb chord which is not a process per se as we normally consider it and the matrix so in general boxes represent processes occurring over time um a machine a mathematical function for example wires on their hand they have labels and they represent flow of data systems ingredients supplies data types or even actual physical wires such as the usb cord now there are um processes can be combined in different ways right perhaps the simplest possible way is basically by putting one diagram on top of each other such as in this case this is called a parallel composition and it should be noted that parallel in this case means simply logically independent that's it so we can see how two diagrams we have a combined diagram on the right they can also be composed sequentially but with a caveat that the the input and output wires have too much in this case we see a process with two wires on the right b and d and the other process same wires as inputs so we can combine them to form a composite diagram such as this right and given a diagram constructed by sequential and parallel composition such as this we can decompose it in individual elements but it should be noted that the composition is not necessarily unique here's an example of one such decomposition um yeah this is one possible but there might be others so a by a process theory we will understand an interpretation of a diagram in terms of a concrete class of processes in particular it provides an interpretation of wires the boxes and also the composition operation of the diagrams some examples are functions and sets linear maps and vector spaces and matrices and natural numbers um we will consider diagrams that can be deformed into each other as equal right as long as the boxes are connected in the same way such as in this case you can we can move them around as long as we don't change the connectivity so the morale is only connectivity matters here's another example in this case we just move internally up and down but same thing the connectivity didn't change these kind of graphical equations that we have here that always hold are are called diagram equations on the other hand uh on each concrete process theory there will be certain equations that are only valid for for this particular theory for example in this case this diagram is valid it's a valid equation but only when talking about computer programs and and it's not a valid you know it's not a valid equation in all possible interpretations right this in fact that this those two um diagrams are equal relies on the fact that we are thinking on uh the sort function the in the in in the programming in a computer program here's another example of a valid equation uh in the domain of natural numbers in addition right in both cases we have different diagrams that correspond to the same process in particular theory this this kind of equations are called process equations so with this introduction out of the way let's explore some of the bright aspects of diagrams this this diagrammatic language that we discussed can be formalized using category theory specifically in monocarrios so here's our plan we will describe each of those structures categories level categories practitione and symmetric metal categories and each one of them will give rise to a little language with certain operations so first of all let's let's do a quick recap on categories um a category is a set of objects each object has a loop around it we call this an identity at this object we also have given any two objects we have a set of arrows between those objects and the arrows can be concatenated can be composed by concatenation so you can think of a of a category as a directed multi graph where the edges are allowed to have multiple nodes now in terms of string diagrams arrows are processes and they're represented as boxes as we discussed before and um the objects are the short wires attached to the left and on the right right they're usually attached to the boxes the identities have a special symbol um and they were they're represented as full wires and um arrow the composition can be depicted in in this way all right so this is just adding we're establishing a new vocabulary of pictures right or icons and we also require that certain conditions are satisfied first of all we need that the identities behave as neutral elements with respect to the to the composition um on the left are on the right and we also need that the composition is associative so it doesn't really matter which order we apply the operation uh the end result is the same so we just ignore the parenthesis as a running example consider the category of matrices and natural numbers so in this case the objects will be natural numbers arrows from n to m will be matrices of dimension m by n so you can see here two two matrices a and b and just as uh as a number as a trick to remember uh you know the the input corresponds to the input dimension corresponds to the number of columns and the output dimension corresponds to the number of rows um and then the composition is will be matrix multiplication so which is represented uh like like so so we have in this case um a multiplied by by b we have a another matrix going from from the number p to the number m the identity at the number n is just uh the the identity matrix so this example is interesting because um normally we consider objects as as kind of like systems right like i don't know the category of groups or vector spaces but in this case it shows that you know objects can be something much more simpler they're simply um compatibility conditions that allows us to compose multiple arrows nothing more than that so um after having defined uh categories let's talk about uh something called strict model categories which is the simplest version of manual categories is just a category with a monitor structure on the objects and arrows um so just to explain all the details um the idea of parallel composition that we discussed before is captured by the so-called tensor product um which is a an associative binary operation uh it's also called sometimes the monado product uh and it's uh we use this this uh this this up times with a circle operator and it has to be defined in both the objects as wires here and also on the arrows and it matches what we saw before right it just means placing either two wires on top of each other or two two boxes in the popular we also need a neutral or unit object which is represented as the empty box both the object and the unit arrow on on i is represented as the empty box and we can see here that it behaves as a neutral limit with respect to the parallel composition and here's an example of this is amorphism from i to b and since we are using this special symbol we're using the empty space to indicate the i this is how you would represent a a morphism or an arrow from i to b right as something that only produces uh something of type b and one more this is one of the most important laws this law guarantees or establishes the relationship between the sequential and parallel composition and it basically says that we can compose sequentially if you look at the at the picture here uh there's two ways we can create this diagram right we can either compose sequentially f1 and then g1 and gives us the top part and then we can compose f2 and then g2 and then we can stack them on top of each other that's one way the other way is to stack f1 on top of f2 and then g1 on top of g2 and then we just compose sequentially those two together so this law or equation basically guarantees that it doesn't really matter which order we do the composition the results should be the same going back to our example of matrices um matrixes can be uh they form a monolithic category if we use uh what it's called as known as the kronecker product as the parallel composition of arrows and it operates as multiplication on natural numbers so given two matrices a and b like this from n to m and and q to b the chronicle product it's this big matrix here um i'm not going to dwell on this but just notice that this is a um this is this is a block matrix right so each entry is not actually a number for example rather this is just a symbolic form to express that each entry is a copy of b multiplied with the corresponding entry of a and so you can see how the dimensions end up like this right so basically we are just multiplying the input dimensions and the output dimensions and you have a really big matrix and of course the the zero the number zero would be the unit element right it corresponds to the empty matrix so um you know this is all good but unfortunately many situations the money loss a sensitivity and identity element are not strictly satisfied right so this so this kind of equation is not strictly satisfied um as a very simple example right in scala if we take the tuple on the left and the table on the right they have different types even though they're clearly isomorphic and this is a common um a common situation um so instead we have to relax our conditions and instead of requiring the quality we will require isomorphisms between uh composition the two ways to associate the the tensor product uh this isomorphism is called the associator and depends on three objects and we also need um uh those isomorphisms the left and right junitors are called like this and they satisfy certain laws that i'm going to gloss over for now so this was a monado categories the next gadget that we're gonna explore is uh what is called a cartesian category in this type of category we have a few more operations we have a way to extract the first and second components and it is represented like this we also have a way to duplicate information given an a we can just you know output two two copies of the input and we can also discard information given an a we just ignore it right finally in a symmetric model category we have what is called a swap operation and the icon here it's just in carefully like this so when you see these two crossing um wires it means that it is specifically the swap operation on um on a symmetrical category the inference is depicted like this so it's very similar but notice how the wires are in different um let's say uh different order and well this representation is chosen so that you know this diagram kind of makes sense the idea is that if you look at this diagram right our graphical or geometrical intuition tells us that we can just like straighten those wires together and we should get two wires right and this is true because we're depicting the inverse in this way so this is one of the i guess themes of uh string diagrams try to utilize our existing geometrical intuition to kind of like make it easy to understand some algebraic equations or properties and furthermore um in a symmetrical category specifically we require that the swap satisfies this equation and with this equation it's pretty much the same as establishing this solid equation right so you know we swap with with the swap operation we can we can twist or break and if we do it two times we get back the identity like this or you know two wires so this is um the diagrams that have been discussing so far if you notice they contain no loops and to be more precise they're normally called circuit diagrams um feedback loops can be introduced by using what is known as compact closed categories which we'll be discussing here but the the morale is that there's a zoo of different um extensions right to to to the basic model category definition with different requirements and uh basically depending on what the application is you can reach out to different different um different cases uh okay let's talk about string diagrams in scala as another running example application consider an airflow like process manager um if you have us if you haven't used it airflow allows you to create a graph of nodes such as the one depicted here and each node you know performs certain operation um so in this toy example imagine that this each node represents the an action such as making an sp call or maybe running a program and the wires in this example represent um type information moving from one process to another uh by type i mean that it would be an error to maybe feed you know uh something of the incorrect type to the to the next uh to the next box so um here's how a dsl created for this purpose would be used in this uh would be used so we will we will describe this later but this is one way way to to use it um i'm using the double plus to indicate parallel composition so you can see also by the by the lines here how you would compose this this um this diagram right you have the identity arrow and then put it on top of p1 which is something that outputs c and then in this case p2 it's a process that takes two inputs and you know outputs uh something of type d and we just do we just use sequential composition uh at this point we can use one of our existing operators the first to discard the second and just keep the first uh the first um input so we can fit it to the next so this is this is how would you compose these operations um so next this is another uh this is part of the diagram right another piece of diagram or fragment this is another part of the diagram this is this example uh the delta here it it's just the duplicate information sorry the duplicate operation so presumably if we have an input of type a we can just you know duplicate as many as times as we like um and just so that all the wires are connected properly and finally we have this um this hypothetical node uh t so the whole thing becomes a a building block block or a graph that takes an input a and has an output of type b right and this is our program so we can we can use you know the titles encoding uh to create uh a process uh dsl with all the operations neither needed in our domain um since we want something very general right we want to be able to actually interpret this diagram in multiple cases uh we we would like to pass a um an abstract type function like process in this case um parameterized by the input and the output and we so you know the first set of operations that we need are the ones given by the categorical structure the identity and then and then the comp the composite is useful mostly because a lot of the you know if you're trying to capture a lot of the questions in the literature they are expressed using the compose operation um so it's useful to have them like this like that we also would like to add some operations taken from the categorical the sort of the cartesian structure first second uh this separation merging input on top of which we can define duplicates as a derived operation we we need what is known as internal object and to be um to indicate that we are basically ignoring the input and so so we have the discard operation and we also have this we need this uh a few combinators from the monolith structure uh the first one allows us to reassociate right uh to the right and then the inverse allows us to reassociate uh to the left we also need a way to inject x in a tuple and to inject on the right and on the left and this is our tensor operation this is this is the combined operation so just as a note here um if you remember the tensor operates in both the arrows and and the wires right so uh in this particular example um we are using the tuple tuple two as as the tensor product and we're using the plus plus combinator or operation to to to to describe uh parallel composition of processes finally we have the swap operation and the swap inverse like this now [Music] the cool part of this is that we have a bunch of ready-made we have a specific specification already made for us basically the algebraic loss uh that all those operations satisfied all the things that we glossed over at the beginning uh so we have you know each of those gadgets the character the you know the the category category it has a few operations but also it has a few laws to ver to be very precise about the logical properties so for the for the category loss we need a sensitivity we need that the identity satisfies this you know left and right um identity from the tensor loss this is what i described briefly uh this this this explains the reference between the um horizontal sorry sequential and parallel composition we also need this tensor operation to satisfy this identity law and there's a few other laws that come from the monetal structure and the symmetric metal structure um i'm just gonna i'm not gonna even try to to go into explain those um they're called the triangle equation pentagon equation hexagon equation and the symmetry operation um in any case uh the the idea is that those equations um gives us strong guarantees that no matter which um you know which interpretation we as long as the the concrete instances satisfy those laws then we're good to go so as a first concrete example um you know let's let's let's let's write um um right a few interpreters uh and interpreters in this case means basically just uh type class instances so uh the first one would be uh we're gonna show um we need an executable interpreter of course using zeo and zeo if you are not familiar it comes with this type called rio and it's for all practical purposes you can think of it as a function from a to either of trouble or b so it allows us to capture side effects but it keeps the the error type fixed right but it has an input channel and an output channel which is what you want in this case and i'm using this scala 3 new syntax for typeclass instances so we need the identity um we need the operation the which is the sequential composition uh first and second to extract uh components uh merge input discard we're gonna use we're gonna succeed with an empty tuple uh the associate right and associate left you know it's exactly what we would imagine just literally transform one two point to the other uh we also need to provide a way to inject on the right and inject on the left and uh the the parallel composition um there's a few ways to define it but we can use this zip with par operation or combinator that actually runs things um you know concurrently so basically this z interpreter mostly will mostly delegate all the implementations uh to see a built-ins oh and swap of course now so what we have so far is we have our process dsl ops we describe the the the zeo instance and of course one of the main goals of this kind of if you go this way so so you can easily create you know for example graphical presentations or many kind of representations but um for rendering instead of jumping straight from the dsl into something low level like graphics for example or d3 it is very convenient to use intermediate presentation that still maintains the categorical uh structure so the idea is to to try to keep to maintain the categorical structure as much as possible and only you know rendered or discarded at the last minute so for that we will use um what is called um the category of photographs following uh sliver and fun this is a slightly modified version of what they described so it is a category where the arrows are case classes such as port graph or basically any data structure representing graphs so i chose to use a case class with the following elements so first of all it has um a map an order map of boxes so if you can see here um the keys are correspond to the to the boxes abc and then the values are a list of ports so for example the box a has three ports uh with these labels a on the left and b c d on the right although i'm not rendering the the labels the internal labels and then b has three ports on the left and three ports on the right and c has two parts on the left and one port and right this is just uh the ports of the of the boxes and then we have incoming boxes um this is just saying that the whole graph has two input boxes the first the first input port will connect to the first entry of a and the second to the third range of b we have also all the connectivity between the inner elements uh all the outgoing ports here's another example of a since there's no internal connectivity there's only one box i'm running out of time i'm just going to go quickly and this is what i meant we we can just define a categorical structure here so we have a combined graph such as this and by the way the identity arrow in this category it's just uh wires right uh there's one identity for each number of wires and finally uh with this structure in place it becomes much much manageable manageable to actually you know render into something like graphics which can be very messy um so this is just a way to to make it much much easier right and that's it that's what i have