Scale By The Bay 2018 Unconference: Runar Bjarnason

Recording: Scale By The Bay 2018 Unconference: Runar Bjarnason

you great let's say go on okay my name is ruin our I'm gonna be talking about category theory from first principles right from the beginning okay how many people are familiar with category theory like yeah good half alright how many people could tell me what a category is like half of those people great awesome so well I'm just gonna start from the very beginning so everybody familiar with functions yeah we're good okay cool we're good with functions so let's let's talk about the the API of functions like what what is the programming model of functions okay so like in Scala for is this we have a function call it f and it goes from the type a to the type B and we have a function G that goes from the type B to the function C then we also have a function do you compose F that goes from the type A to the type C alright so this is one of the things you can do with functions in fact this is like this is like the only thing you can do with functions so functions compose and they compose in an associative way that is if I say g 'c compose or let's actually want to flip dates just for so I don't confuse myself this is G this is f this is f MSD great so now if I say F compose G compose H compose H like well given that H goes from C to some other type this will always always work and like if I put the parens here or if I put the parens here that should mean the same thing all right it doesn't matter which way I associate this if I compose this function with that one or this function with that one like doesn't matter you obviously can't flip them because then the types won't line up like you can't say G compose F because the types are are incorrect but you can compose them in any any order great so it's associative alright so another thing about function clubs about functions is that for every type a there is a function of type a to a called identity let's call that ID it's ID of a and that has the implementation you know lambda of X goes to X so it's just returns its argument and the property that that this function has with regard to composition is that it's an identity for the composition that is it's a unit so f compose identity is the same thing as identity compose F and that's the same thing as F right so the identity function does nothing with regard to composition ok so that's the sort of abstract API of functions they go from types two types they compose in an associative way there's an identity for every type that does nothing great cool let's now go to the abstract let's talk about categories alright so a category so this is what a category is a category consists of some objects some objects some arrows between those objects and there's a composition of the arrows which is associative and has an identity just like this so this is a category but there are lots of lots of other categories that behave the same way in the abstract all right so this is category theory right so if you didn't know category theory before now you do thank you awesome everybody can go home I mean you know this this is really all of it and it has cool implications that that will that will explore great let's look at some more examples of categories okay let's look at so we're looking at the Scala category here but let's look at how Scala Scala is a category in a different way so something that doesn't involve functions so in this category let's let's so the category we were talking about before push that onto the stack that category is called let's call that category Scala and the literature is something just called set but it's the category of sets and functions between sets but we want to talk about types Scala types and functions between Scylla types but so to a first approximation types are sets of values right so let's talk about how Scala is a category in a different way so I'm going to talk about a category that I'm gonna call Scala seven so in that category the objects so so all we just got to go to our definition of category and we got to provide these things in order to get a category this is the data structure that we need so let's instantiate that data structure here the objects in this category our Scala types okay the arrows in this category are as follows so whereas in the in this category here the arrows were functions between types in this category the arrows are subtype relationships so there is an arrow from A to B and we'll write that like this exactly when a is a subtype of B all right so this is how we construct an arrow in this category if if a is a subtype of B there's an arrow now you'll note that if a is a subtype of B and B is a subtype of C then a is certainly a subtype of C as well right so arrows compose yeah so this is the composition on the arrows that we can reason from here to here right so if we call this arrow F and we call this arrow G then we can call this arrow do you compose F sweet you'll also note that in this category there's at most one arrow between any two objects okay so so these arrows are unique that is if you say that a is a subtype of B and you say it again you can't say it in a different way it's a is a September be in a unique way okay so and also then for every type like we need we need associativity right so if subjectivity is the transitivity relation so if we have you know a being a subtype of a being a subtype of B which is a subtype of C we can reason that C is a super type of a by simply you know saying like well we'll reason this way first a is a subtype of B all right and since a is deceptive of b and b is acceptance of C then a is definitely a subtype of C but we can also reason the other way we can say well B is a subtype of C and then a is accept of B therefore a susceptible to C so composition on the errors is associative here everybody cool with this great and we need the identity for every type a there is an identity arrow which is just the fact that every type is a subtype of itself and that doesn't do anything like it doesn't add any additional information in this composition we said a is a septum of a and a is a subtype of B therefore a deceptive be like the identity doesn't add anything great okay so now we have two examples of categories under our belt here pretty cool let's let's look at some more samples so what I'm going to do is just give you lots of examples of categories so you can sort of start to understand what all this is for so so that was that was a category where where every between any two objects there was at most one arrow and actually such a category is called a poset and we can actually do this in general that whenever we have some set you know we have some host set so a post that is a partially ordered set so if we have a set that has you know it has some some values in it right some type and it has a relationship like you know less than or equal to so for any given for every for any two objects in the set we can ask well is a less than or equal to B and if it is there's an arrow from A to B okay so so the Scala subtype the the Scala type system forms a post set in this way great and so and we can do this in general like for instance we can say int is a category like this where there's an arrow from A to B like the integer a to the integer B exactly when a is less than or equal to B and it works exactly the same way as we did before like every integer you know it's less than or equal to itself that's the identity and it composes it in the same way as we did with Scala sub great so that's a posit category and so a post set we can give a precise definition of what a post that is in category theory terms so a post that is a category with at most one arrow between or from A to B for any two objects a and B cool so you know we can start to like give purely category theoretic definitions just given given this stuff people familiar with mono it's anyone not familiar with mono it's wow that's awesome all right you guys like yeah mono it's great cool okay so what is a mom wait hey Mon would we can say is a set right it's a trait mono I'd we give it some some set m some type right and it has well you know it has append and it has the zero type m and append goes from M and M to M yeah and so in a montoya we can compose the values and composition is associative on the values and there's an identity a zero for composition this is looking like a category right and in fact a mono it is a category I'm annoyed and we can give that in a purely category theoretic terms a mono it is a category with one object okay so how does that work out so we can think of we can think of the the values of type M as being arrows and so they are just arrows from that one object to itself that go from from from from this object itself so this might be let's say this is integer and this might be the arrow one and then this might be the arrow to say and that's going to be the same as one and that composed with one okay and so we can build up the the natural numbers that way when there's going to be an identity arrow which is zero so we can build up the integers by composing arrows this way where we say like oh this is 1 and this is 4 and this is 6 right and this whole thing is the arrow 11 yep no so the object in here is is not really a type so and these arrows are not functions okay so where we've gone from so we're no longer in this category this is not the category when we are in this category here the mono ID M okay where the arrows are the values of type M and the object is just some arbitrary object the only reason that this object exists we can just erase it the only reason it exists is to say that all of these arrows are compatible that is we can compose any two arrows right okay and and be the directionality of the arrow it's saying that this while this is associative and and all that it's not commutative so the direction matters for instance if these are strings this were like foo and then bar and Baz we can't flip the order that the direction of the arrow matters its foo bar Baz not fou Baz bar right cool so a mano it is a category with one object and that this is a precise specification of what mano it is in category theory terms so if you know what a category is and then you say a category with one object is a mano would oh you know what amaro it is cool yeah the one object I mean the whole category is the Maoris right that is a meaningless question like what no I just mean I mean the object has no structure right other than the fact that it has arrows that are tied to it that is the that is all of it yeah it's both the beginning and the end of the arrows yeah it's just it ties all of these errors it simply means that all of these arrows are compatible you can compose any two of them because they go from from that object to the same object and so you can always go back to that object as many times as you want so it means you can build all of the strings from arrows that are all tied to this one object yeah right I did gloss over that that's true yes so so in yeah and category theory it's like if you have again I started out by saying that if you have F that goes from A to B and if you have G that goes from B to C you always have G compose F that goes from A to C like this this always exists it always works and so what the mono and then the types the object have to be the same in order for like this works only if and only if and always if the this the destination of F is the same as the source of G okay so it's like we got a B and C F and G say and and this always exists and only if they agree on this object so in a mono would all of the arrows agree sort of trivially and therefore we can take any two strings and compose them because strings are my lights cool so so composition always works for any for any two heads now let's look at a different category where this is not true so maybe that will be a little illuminating but we can look at that's a good Domino's guys alright so in the game of Domino's there are some there are some objects let's call them 1 through 6 right like they could be what 1 is 0 through 6 I guess well let's ignore that there are zeros because that's but a special rule so 1 through 6 in a sort of a simplified game of Domino's that is an end of a domino like this can have you know between 1 and you know 6 dots on it and for any two Domino's if they agree on the dots or the number of dots on one side they compose on that side cool and they form a new Domino a longer Domino that you can keep keep composing up ok so this is now a category where you don't have one object you have 6 and so the arrows are not all compatible they're only compatible when they agree on the on the on the ends and there's an identity for every you know for every value for every object that is you know the Domino that doesn't change the end cool so that's contrasted with mono age where there's only one object now there are six and so we have this sort of incompatibility and so really you can think of a category as a generalized mono it yeah so it's just it categories is like a mono age where you had just have more capability where not all the arrows or you know but not all of the things that you can compose are compatible with one another there are some rules of compatibility okay like in the types the types have to be the same and the Dominos the the number of dots has to be the same in the post set you know it has to be the same value yeah yeah yeah that there is there's not a finite number of objects in that wait sorry yeah no because there is more than one arrow from that can be more than one arrow from any one type a to another type B yeah a lot of lot of function from string to string a lot of functions from that's it that's a great point yeah you can you can go from here to here like there's an embedding of this in here right like you can you can look at a subtype relationship as a function well all the functions give you the identity function right so oh so it's just like so this has a number of objects right and and and this this thing has fewer objects as it were and sorry arrows this is a number of arrows and this has fewer arrows because like there's at most one here for for any two types but here's there's lots and if you go from you can go from here to here by simply saying well I'm just gonna take the identity functions like if I have a you know a subtype relationship like this a is a subtype of B I can say well I have a function from A to B which is just the identity right sorry it's a then on B yeah so right yeah you just have to like up cast one of them to the larger type and in fact all of the arrows if you if you go from here to here you will take you will get into a category where all of the arrows are identity arrows right and such a category is called a discrete category all arrows are identity alright so then you just have some things some objects and the only arrows are the identity errors that's that's a category you can construct and there are lots of there are lots of little categories you can construct like this like you can construct the category one the category one has one object and it's a discrete category it only has an identity arrow this is the this is a perfectly crumbling category you can also have the category to the category two has two objects and it has an arrow between them and obviously there's an identity arrow for both of these objects and all the hours compose every call this category too and you know this category three with three of them and like they have it has one composite arrow so it's like a triangle like this and there's a zero as well this is a category with no objects at all and no arrows between those objects and that's a perfectly common category as well it's like we could just say well it has zero objects zero arrows and the composition works trivially because we don't have anything any work to do cool so we've done mono AIDS we've gone done like dominoes and stuff let's go let's go higher up so we were talking about embedding this category two into this one we have some kind of operation here right that's kind of weird right so what kind of thing is that kind of thing is a functor so a functor say functor from category c from category C to D we can say it's a functor F it goes from C to D like this and here's what it does it Maps every object and C to one object and D and it Maps every arrow as well so every arrow in situ an arrow in D in such a way that the composition still works so if we say you know F on some object and I'm sorry on some arrow F and we compose that with F of some other ROG both of these arrows are in in C and F of those arrows are indeed that should be the same thing as F of F composed with G the composition is preserved and also the identity should be preserved F of the identity should be the identity yeah in fact this forms a category so we can talk about a category of categories category of categories what's that okay an example of a functor let's do that okay this is an example of a functor whereas embedding scholars of the Scala set can we do another one where we yeah hello so an endo functor endo functor goes from some category c to itself so an endo functor on c it is a functor from C to C endo means within so it's within the category C so we map so every object in C to another object in C or the same one and it Maps every arrow in C to another arrow in C or the same one in such a way that this this works so an example in Scala is list okay list is a funk is an end or functor in Scala so list takes every type t2 well to the type list of T right like we can we can write it we could write it like this list is a type level thing that goes from the type T to the type list of T it's a type constructor like this and and so it Maps every object in in Scala to another I mean every type in Scala to another type in Scala it maps every arrow in Scala to another arrow in ska so it Maps the arrow F takes that to map F so I underscore that map F right that is we go from A to B - that's a list of a list of a - list of me right and it works out that if we map if we first map F over list and then map G over a list that is it has the same result as mapping the composite function f G over the list yeah are you - are you telling me that list is a type level monad I think you're right but yeah I mean that's that would be a cool thing to explore you could definitely - take a look at that okay where were you this yeah yeah yeah so this this endow factor thing is just operating on one category yeah so you can think of you know you can think of this as being like an object in this kind of category where or you know in a category where looks easy on the object sorry what exactly yes so them it's the MA note of all endo vendors yeah so that's good that is it's the it's the mono we're the only object is the category C and then all of the arrows are the end of factors in C yes in fact you know we we have categories of endo factors which we can get to but let's let's talk about let's talk about the category of categories starts that with that so sort of like to understand what what functor sort of means in terms of category theory we can talk about the category category cat of categories so the object in here objects are categories the arrows are functors that is they are mappings from categories the categories that preserve the cat the structure of the category that is they preserve composition and and identities on the arrows cool and what is what is a what is a composition in this thing composition on the arrows if we have a a functor F that goes from C to D and we have a functor G that goes from D to e then we have a functor you know F G like this sorry D F G F like that so the composite funky and composition is associative that is you know if you have h out here doesn't matter whether you compose FG effigy first or H and G first and there's an identity functor which is just you know type no identity functor for every four for every category so that takes the category C to the category C preserving everything identity on see see see all right so it just takes takes all the objects to themselves and all of the the categories sorry it takes all of the objects in the category to themselves and all the arrows in the category to it - of themselves cool yeah we were talking about categories of endo finders right okay let's talk about that category as well do I have time by the way okay cool all right I mean I think the panel isn't about 10 minutes so we'll wrap this up soon okay for any category see we have a category of endo functors in sea call that endo see I guess where the objects are functors from C to C so endo furnitures and see the arrows are transformations between functors they are natural transformations natural transformations okay what does that mean so a natural natural transformation means that if you apply now I'm getting into the weeds here so so natural transformation goes from a functor F to the functor G say so for two functions so this is a natural transformation from F to G we can do this quickly our thing here like we do in Scala sometimes so goes from F to G and in Scala when we're working with endo functors and Scala and natural transformations between them we talked about this being a function that you know given some type a takes you from I guess I'm gonna use like the thottie syntax here given the type a it takes you from F of A to G of a cool so that's your work for for any given type takes you from an F full of a is to a G full of A's and the the rule here is that the how do i express this as a hammam orphism law if you have sorry oh yeah if you have a map from A to B great so these are some objects and see a map from A to B then you can do F of a we have an F of a and then F of B should be able to do sorry wait right GG so I have do you want to I'm just totally blanking here on this don't help me out here yeah help me out I'm thinking in terms of how a morphism law okay that's good right and that should work great that's it exactly thank you that's what I was getting getting right so it's that yet right so you start with a function from A to B call that F and then this is our natural transformation called that H here and then this is f of F for a functor F and this is G of F for a functor G and this is saying that doing this compose you know H composed with G of F is the same as doing F of F composed of H like these two paths through this diagram are the same and we say that the diagram commutes oh so these are objects in the category C right so these are these are all objects in this category here and for for an arrow in the category of endo functors on c to be you know unnatural transformation it needs to satisfy this kind of law that that operates on the objects of the underlying functor I mean underlying category yeah yeah list that had option at one of these and in general I want to say that like the arrows I want to introduce this notion here the arrows here should be Hama morphisms and so what does that mean so for we're here for a first set it just means they're functions that doesn't add any anything additional but if we're talking about say we're talking about a category Mahanoy DS say say a the category category Mon of Monowitz so the objects are mono whites and the arrows our functions just like in here but there's there's special kinds of functions because now we're not in a category of all sets where the category mono Waits and so we have to talk about what's called mono and hama morphism Mahanoy hama morphism and that's just a function but it has to obey this kind of law which said so if we have an arrow in this category let's call it h this should hold that H of X composed with Y should be the same as H of X composed with H of Y right so in order for for a function to be an honest-to-goodness arrow in this category of Monowitz it needs to obey this kind of law it has to preserve that the mono I'd structure okay so for for sets that doesn't that's not very interesting like set hama morphisms are just functions but mono a homomorphisms are functions with this additional property and you'll note that this is also this is the same as the functor law that like you know map F compose G should be the same as map F composed map G right so this looks like the functor law and that's not a coincidence because in the category of endo functors the arrows are category homomorphisms now I'm sorry in the category categories the arrows are a category homomorphisms which are functors cool and it's an example of a monoatomic morphism for instance string lengths so underscore dot length goes from the monoi for Strings to the mono ID for intz in such a way that taking the length of the composite string XY is the same as taking the length of X and adding that to the length of Y right and there are lots of lots and lots of examples like this if you're in a boolean algebra for instance the mono it is like boolean with and you can go to the other one boolean with or through not so not x and y is not X or not Y and that works the other way around as well so that the mono and how a morphism not is a mono it isomorphism so you could it goes both ways anyway I think we'll just stop there we're out of time thank you [Applause] you