Classical Category Theory in Plain Scala

Scale By The Bay 2018: Vlad Patryshev, Classical Category Theory in Plain Scala

Recording: Scale By The Bay 2018: Vlad Patryshev, Classical Category Theory in Plain Scala

so 20 years ago I've worked in Google and exactly 10 years ago and my manager discovered something on my computer and shared like what did this what kind of project is it and I said it's a category theory and calculations in it category theory of the reaction so the role has changed since so like everybody knows category theory and we've been having bay area categories and types for for about 12 years now a meet-up so you can look it up and join so like half of today's talks or maybe like the bigger half of today's talks were connected with categories so I'm not going to explain what a category is you know categories you know the category of sets like all sets although it's not exactly specified like what kind of sets we are talking about and what axiomatic and so on you know what categories like Haskell well there's much more than one hostel category hostel with exactly pure function that's it our hostel where functions are personal like head is not a function ap or front rim head is a partial function Oh hostel with closely where we do something about like things that don't happen like it's similar to partial function in Scala we have at least like kind of Scour category where two functions can be composed or two methods also we have another category in Scour with inheritance where like one type using subtype is a subtype from another so from that you can also build categories and when you talk about covariant factors that's about this second category to color with inheritance and you type class you use a category well that's arguable but that's just my personal view and there are more categories like Greg files today his talk about the oil tea on how to delete delete half well more than half actually because like he showed how to delete not only up but also partials class there whatever so he showed a lot of categories to us and there are a little bit more categories around so here are some that I like started building in I built it in Java I do them in Scala so the first category is called zero and this is that category it's invisible because it has zero objects and zero arrows in the Scala code that is available on github it's denoted as underscore zero that so it's a category where object science arrows are pairs intended Jack just a segment zero means like there are no element category one consists of one object and I don't draw identity arrows so it consists of just one object and that's it well this one plus means 1 plus 1 so it's rendering issue we just oh my god no ok so I'll explain the problems with rendering so this is the category 1 plus 1 just two objects and no errors between them it's like this and the objects are named a and B the rest is built out those identities category 2 is displayed here this it has two object 0 and 1 and an arrow from 0 to 1 and also to identity that's it so that's how it's defined here because it's a segment it's just a partial order category 3 is another segment 3 element 0 1 2 and it consists of this segment can build like any partial linear partial order numbers from 0 to so the class for category for this kind of categories not big ones like we have like in your compiler that understands composition and so on but this class of tiny categories looks like this it's a class category types of object type of object type of arrows and it has a graph inside and it also extends a graph a graph inside serves for providing storing objects and storing arrows so that's how it is it's not-- it's known as no it's in graph but it's not known as objects in categories we have unit every object has a unit and multiple composition em from for two pairs of arrows they can be composed but not all of them I have the method called equals but category theory is not equational so equality of two categories is like and the question I just had to have it for running unit tests but what does it mean it's a graph so what is a graph a graph is defined like this so we have nodes we have arrows D 0 D 1 means domain and codomain of an arrow and basically it extends a set of nodes but we like some things so one of the things is home meaning a set world like it's kind of question of why is it a cell but that's a different story so set in skeletons not in set theory sense so from all arrows from one object to another and how it is built like it's settled all errors were refuted them such the domain is from and codomain is too so that's it it's a regular trivial set of set quote-unquote of arrows from one object to another so more of those tiny categories category form consists of just it's a linear order consists of four objects parallel pair to object zero and one and two arrows a and B we don't need any composition except with identity but identity composition when you build the categories being a built so here the constructor of this category like I pass a string and it's being parsed so we have object 0 1 arrows from 0 1 and from 0 1 and no composition provided well the composition with identities is kind of category that is called pull back for some like categorical reasons so we have three objects C D and D and an arrow from C to D from B to D and it's defined like this so we have object BCD arrows begin arrow thingy and again like we don't care about composition a category called square so here I also drawn this diagonal that is kind of assumed to exist so for objects ABCD arrows a to C A to D a to be B to D and their composition and it's a commutative Square and their composition from A to D if the square were not commutative we would have to ask so here we have the same collection of arrows and we needed to define a composition so a B followed by B G is AG and AC followed by C D is a D so the same ad so that's it and when when this category class went apart or parcels it and the categories been built so all the things are being validated so that we won't have like a a bad category that is not a category like associated has been checked and all these remove so this is a small category that are good for experimenting with like categorical constructions we'll get there later but I also needed bigger categories like set category where objects ourselves so then I couldn't use Scour set type because colored tape is kind of not good enough for this purpose if you have like imagine you have a set of all six strings right so what the size of it how can we well ok strings you can iterate but generally speaking you cannot iterate always like real numbers right so this is things that are too big so I had to introduce a class called big set which has less features than scallops like Scala regular sets and basically you can override some method like equals or whatever and some of them are innumerable some not so asset category is a category where objects are set in any sense because it's in set theory certain don't have types so that's the kind of special kind of sets not our regular like programmer sets were like everything has a type so instead function mean just functions from one set to another again like totally ignoring types they are all any and so we have to pass a graph of sets with some objects that we have there and we provide the composition and again like what are these two compositions composition F composed a composition G set function it's something like a regular function like a arrow be in Scala except that well we have to make sure we're dealing with sets and ignoring the types so this compose is defined more or less like regular composition of functions in Scala and so we have unit to string just settle a category all of all callouses so it's our ZFC our terminal of ranking set in Scala and whom we had to redefine it specifically because like we cannot rename real enumerate everything it just a construction from a given one set and another we build an exponent so like Y to the power of X all possible function assuming that we can build it right some sets are too big so maybe we won't list all these elements so of course although it's a set it's like its GK and again we don't know the size so what's a set function a set function like again we are dealing with the category of sets right so it has a domain it has academe then take the edge of specific cells become the mapping that like the underlying the hidden think that maps values elements who once said two elements of another cell and tag is just for like for better disambiguation when you do printer well right so like what what function is this so for instance if you compose one function with another we don't like composed with everything with everything so the domain should be the same I asked a domain of another and the tag would be like this tag composed with the next tag so if you couldn't do it so our domain cut the main of this next function and the mapping is just this taken X and returned like G applied to G of f of X so that's the regular composition of a regular function but the thing is we also wrap provide domain and codomain and they are not typed they took sense and otherwise if we couldn't compose it we return none so this is like a partial function of composition so what is it big set from our point of view it's the same set and for like JVM Java libraries by Java libraries convention we say that site is max value it's a signal to some software in Java in Java library that this is an infinite set so you want you are not supposed to list all the elements and like given a set within the big set and because the set is given so we assume are it's an enumerable enumerable set so the method contains is the same what we and iterator is something that we inhaled or we can build a set because we talked about like any possible sets we can just provide a predicate so here the predicate like your number like has support we deal with a real number so if it's a real number so the tens digit is 7 so like any predicate can be provided by default it's true meaning like anything is in that set so it's a set of all set of all scholarships to this set so this big set is not enumerable and contains only mean this we apply this predicate so basically this is the set that is defined by a predicate so what's an awning you enumerable set it's a set where you cannot enumerate values so in Scala it's kind of we are in an interesting situation so we have a set you have a head of set what's ahead of set is it like our choice axiom automatically providing like the first element of a set even of an empty set not here so we have this like tag method they're not enumerable so anything you do that like causes an attempt to enumerate we'll throw this like is it empty we don't know we don't know that we don't compare them so iterator like if it extends the set so it's supposed to have a method iterated not enumerable no no don't you try to array so not enumerable like you cannot enumerate real numbers in Scala in Java or whatever there's no way of course I can in the middle like all possible combination of bytes but well we're more like idealistic in this relation so we assume that there is a totally like infinite number of real numbers although it's in real life it's not but okay so these are categories right next we build what factors to defy the factor we need what like the main category that case like objects of X the main category X with objects and arrows called the main category with objects and arrows a morphism from objects of the first category to object another category and object from the first a morphism from arrows of the first category to arrow in the second category and this means it's a regular scalar mapping nothing special there because we have a type so for this step we define something and I added the tag just because like I like doing println not everything is like done by just so so I tagged the factors and of course we can define a composition with another factor and we also have to define identity finder and so on so composition is defined like this so given two factors like G from so given one hour factor from X to Y and G from Y to Z so we produce a factor from X to Z we have to check that our same kind of main so it even thrown right so this composition what it doesn't it returns the factor not an option so what do we need we need to compose arrows compose like mapping on objects so on aka on nodes and mappings on arrows so look at these two mappings like nodes from the first from X goes to Y goes to Z so that's what it is right this compose means it's a regular color campus compose and we produce a new factor from X object X arrow to this category with the objects and the arrows that had this arrow motion not morphism the main is the original the main cada magnet the codomain of the second factor and the tag is like this again like we just showed that this is a composition of the thing that's it any questions no trillion I hope so a constant factor is defined like this given a category she and a category G and any object object in category G object Y we can define a constant factor by just as a factor that Maps any object in the original in the domain category into that object why and any error to identity on that object so that's what's happening comfort so what do we provide we provide the first category we provide the second category and an object in this category way so it will be a factor from X to Y this you find right so it's defined like this on arrows it's a unit all the time every error from X maps to a unit on object Y so but we had to provide set morphine so that's how it is with we are dealing with sets right so on object we just map everything to object Y and tag say that we'll use this the value of this object Y here so if it's called like X well if it's called object a so it will like this is object a as a constant factor and X will be the domain of this factor and Y will be a condiment of this factor that's a pretty trivial right why do we need constant phantoms we'll see pretty soon again like next step mappings between factors they are called natural transformations so they are consistent mappings from one country to another given factor f gain factor G alpha is called the natural transformation from F to G and they have the same dominica domain if this picture is compatible like we have for that pullback diagram that we had before she be d right so we have this FG - FG f b2 FD and we have G B D G GG and G c2 GE and we have mappings for each component so this I wouldn't call them squares but like if you rotate the diagram they will be squares right so all the square should be commutative so that's the definition of natural transformation that's it so how do we like implement it in Scala so we need we need to what we need the one factor from X to Y another factor from X to Y and we need their transformation per object for each object we need like something from FC to GC so that what we have like set morphine because again we are talking about like set category so it's a morphism well I'm not doing their selves like the main would be one factor kademan is another factor and so that's how it is like d0 is the domain and dy is gonna main and basically that's it but when you build it also this compatibility this consistency is being chipped meaning like if you check it on an infinite category so it may fail if you build like big factors so one specific case of natural transformation from one point to another is a natural transformation from a constant factor to another so if you is just an object in our category so any object in a category can be considered as a factor from like from some other category and if we have a bunch of consistent arrows so you can look at it as well it's called a cone cone is like in the opposite direction it's called the cone from you to factor f but it can also be considered as a natural transformation from a constant factor to factor F so we have this class called from object this like you is called epochs so what we need to provide for a call we need to give the ethics and for every X for every element of this target category we need to have an arrow from know for every object of the original that the main category C D and F we need an arrow from you to FC from you to F G from you to FB and so on so that's why it is like an arrow for every see every be every day so that consists of that's what the cone is and again like we can look at it as a natural transformation from a constant factor so out of all of those cones like given a factor so find specific I specified objects like in the Academy in category with all these arrows so out of all those cones there is a best one that best one is called the limit so what's the feature of the best one like in this picture V is a cone I don't draw this middle arrow because like it should be a composition anyway so we could start with like with the basic babe base object so we have a couple of arrows from V a couple of arrows from you but the best one X is the one that has a unique arrow from V a unique arrow from you and a unique arrow from anything that has this compatible matting such that these things commute like v2x and goes like this in the same and things we chose here in the same entities and the same for you so this is the definition of a limit limit can be defined as a cone and if we take all these cones right we can just find the one that is a limit well maybe it doesn't exist right so limits don't always exist categories so I have this radical is limited so take a candidate and how do we know it's a limit we scan through all possible cones and see that it factors on right meaning like it goes here through this this one goes here through this how do we know it does well we have to find all possible arrows so an example cartesian product is a limit so what is what is the factor for which we build a Cartesian product if we have two objects a and B we can consider we can look at it as just a factor from 1 plus 1 to object that's it no errors so a Cartesian product in the universal code between all these possible cones right so it has two projections and that's it so a diagram of a category C like in general is just a factor from C to D so if we have a category like like the CBD whatever so and we have a diagram of cells like set B set decent such BCD and two functions right so we can look at it as a factor from this category to category of sets so it's called diagram so if you build a Cartesian product or like a limit of this diagram you can as well look at it as a limit of a factor so we can take like a category of diagram given a factor given a domain of the main category we can build all this so this is a diagram this is the diagram their factors right and we can build the category of such diagrams providing like all these things through natural transformations object in this category fun touch that these diagrams and arrows are natural transformations so that's we build it for bigger things for bigger domains like not the life that we had we can throw in a category of natural numbers in just a category a partial or the complete partial is it completely linear partial order of all natural numbers so we can define it like this create personal or the natural and so on and what's in em is the object of natural numbers so it's a big set its innumerable natural numbers are innumerable so we have all these and so the category of natural numbers gives us this and what's so good about the category of natural numbers it's clearly plus till a plus it's built on set theory but it's actually built above and it considered diagrams transitions from one set another set state set so basically the whole TLA plus is the formalization of diagrams with the domain and M so we can beam like a little bit smaller set a set of a category of finance cells so not just all scholar set but finite sets which is easy because well like what's a finite set it's something that we're size is less than this so we define this it's traditionally called in category series at F and then we can do define something that you cannot like really implement in bigger category so like Cartesian product so we can build this well this this code exists so we take this set and this set and if the product can be built because it's it may not exist we don't know right it's a category then we can check this this is a unit test for that so that what we had categories financial transformation limits limits like all limits are being calculated then column it's to which is kind of hard and deal dealing with big sets and tli plus is an example so if you are interested in like participating in this well because like I have some plans by calculating topological based on this and so that would be cool and references are here so this is a github repo categories and Bartos book is like it's good for programmers and this book like once you get through this one you can read this one and read it again and so I read it like I did it three times no probably four so any questions like when people ask me like what's the use of Mona's right I usually stop answering it so this thing like why I did this so that could be like a more precise answering why I did this I actually wanted to implement diagrams in sets so a diagram itself is actually a category of pre-shift like strictly speaking so if you have pre shifts you can start throwing in sheaves and gratin dick topologies in sheets and consider all kinds of tapas logic and see how it is and some like diagrams are good for like introducing for logic so for instance if there are loops so it's a problem well everybody knows that now like so if there are no loops like if it's a three so it's less than a problem because we can always locate like where the trouble but again it's intuitionistic logic so basically that the purpose it makes it to add the self reference like want a list of references so yeah I'll updated [Music] [Applause]