Category Theory 6.1: Functors Explained for Programmers

[00:00:08]so today I want to talk about functors and functors are really really important so you can actually think of like all the previous lectures they were just the introduction to functors okay because functors are really what's important I mean mathematicians will tell you that really what's important is natural Transformations that you need functors in order to Define natural Transformations okay and that's true right so but but first we have to get to factors um and why are factors so important and I I will again maybe start with a little bit of philosophy about why I personally think functors are important um because I I I told you that there there are things in Cate theory that formalized stuff that uh we haven't even thought was formalizable like certain Notions that are really not even mathematical so for instance this this whole idea of um Universal construction right I mean what is really Universal construction about it's about being able to Define what it means to be like a perfect embodiment of an idea an ideal right it's like we say how do we Define a product well we have all these possibilities Millions Infinity of possibilities to define a product right how do we pick one and and and uh and then we say well we'll just pick the best one something that's the the the ideal and it turns out that if this ideal of a product exists it's actually unique well unique up to a unique isomorphism but that's as as much as uniqueness as as you want in category Theory so really something that you know like artists and scientists were always uh wondering you know what's this what what's an ideal thing you know do do IDE all things exist and and so on this is just like formalizing category Theory with a bunch of arrows and dots you know so that's for me this is this is really astonishing that that you can do this right and we have these two types of uh Universal construction the one for product and and the other for co-product and uh and they sort of Define uh slightly different ways of saying what is more ideal than another thing like because we have all these candidates and then we are saying well there is one of them that's perfect and the property of this perfect thing is that there is a morphism coming from any other candidate right so that's that that that's what we use in the definition of a product which sort of mean that anything else that you throw at me can be distilled to this ideal of a product give me any two objects with these uh projections right give me any two any object with Pro two projections to two objects right and I can distill it to this perfect thing called a product right because I will find a unique morphism and this is like you know just finding a unique morphism it it means this is better than the other thing and with with a co-product we did the opposite sort of but it also makes a lot of sense it means that you know here's this ideal co-product and any other candidate has in it an image of it right because there is a morphism from this perfect ideal thing down to any you know know candidate that's not perfect right there is this morphism that kind of embeds it finds it inside this imperfect thing finds this element of perfection right so functors now functors um mathematically speaking that's a rather simple idea you know you you take uh two categories and the functor is just mapping from one category to another right so why is it so important well when when we talked about um products and co-products right I used the um a little loose language about saying uh you know we are looking for a pattern right so we have we have this pattern which consists for for instance of a single object that was for initial and terminal objects right or an object and two morphisms that was for product and co-product right and now we are trying to find this pattern match this pattern in our big category right we get a lot of matches and then we find the best right but and and you didn't protest right like like what is he talking about what does it mean to to find a match for a pattern right because this is so obvious right pattern matching is something that that we do the moment we wake up until we go to sleep and maybe even in our dreams we do pattern matching pattern matching is like the most important thing in understanding the world you know we build this image of the world this model of the world and we match it into reality you know and we try to find patterns everywhere and recognize them right sometimes we find patterns where they don't exist even because we are so tuned it's better to recognize a pattern of a predator's eyes when there aren't any Predators then to not recognize when there are right because that eliminates Us From Evolution so pattern recognition so again category Theory tells us how to formalize this thing of called pattern recognition okay it says okay so if you want to recognize a pattern inside a category well then obviously you have to Define what you mean by the pattern a pattern must must be some kind of structure right some something you know like you know this um object with two arrows or maybe some more complex pattern or so on and uh you sort of have to map this pattern into this category but you have to map it in such a way that you can recognize this as a pattern which means you have to preserve the structure of this pattern right so what does it mean to have structure well category is a definition really of structure this like structure abstracted to their Essentials that's what category is it's pure structure it's just these dots and arrows and that's structure right so if you want to say I want to recognize a certain structure in inside a category it means you want to Define your pattern as a category itself you know I mean if if if it's a tiny pattern well it will be a tiny category you know I mean you can have a category that has one object in it right that's a category too and it's a pattern or you can have a category in which you have one object and two arrows three objects right and that's a pattern so being able to recognize one category inside of another category is the definition definition of pattern recognition and we'll come back to this when when we Define a more General thing called limits and colimits where we actually do this using these patterns and you'll see then that actually uh product and co-product are just examples of limits and colimits but that will come later when we actually uh learn about natural Transformations but anyway this this is so this is what's what's important being able to Define mappings between categories so we we can think of one category as being this pattern or the model and we map it into another category and we recognize a match for this model or you know embed this model inside another category so now that we have motivation let's think about about um how we can Define the mapping between categories and obviously uh to to the first approximation a category is just a bunch of objects right that was like the original simpleminded definition it's a bunch of objects right so we have to be be able to map these objects right and I said that these objects not necessarily form a set it could be something bigger than a set right so there are these complications with being a set or being something bigger than Set uh and so on but just just for Simplicity just to get the the idea uh of of what we are doing let's let's just consider small categories the small category is one in when in which objects form a set so if you want to map one category into another category first thing you have to map objects and since objects form a set in a small category it's just a mapping of sets what's a mapping of sets it's a function so it boils down to this to this idea that we already studied right we we studied functions and we have a lot of of new intuitions about functions you know we know the functions can can do things like collapse things right be non injective by collapsing things be non surjective but by just covering on the part of the uh Co domain right so all these things that we learned about functions they translate directly into this one part of the definition of a functor okay so the definition of fun contains several Clauses right and I go through them one by one um but there is something funny about functions um that I have not mentioned and and maybe a lot of people don't realize that that that functions are sort of uh primitive trivial they what what we really are interested in in in mathematics and and and in more more General in this in this world is mappings that preserve structure right and it so happens that functions are mappings between sets and sets have no structure it's like by definition a set is this thing that has no structure right it just has a bunch of elements and that's it there is no order of these elements right I mean this is maybe this is why it's so hard to implement a set in programming right because we are trying to map it into into hardware and Hardware is highly organized right and set is disorganized it's really hard to to implement something that's totally disorganized in in on top of Hardware that's that's highly organized so people Implement sets as as trees really right uh but in order to implement a a a tree or a binary tree right you you need be able to compare elements right and so so it's really a set can be defined only when you can compare elements that's that's not good or if you define it as a list then then there is an order in which they get into the list so you have to like think about this and and say it's actually all these list that differ only by order uh represent the same set and so on so so it's it's really a pain in the neck but from the point of view of mathematics set is perfect it says it has no structure and since we learn about functions we rarely think about you know mappings that preserve structure but in all the rest of mathematics what is the most important thing is find these map that preserve some structure because we are dealing in mathematics with structured things things like monoids algebras uh you know uh geometrical figures and so on things that that they have some kind of structure so so we are not really used to thinking about what does it what what does it mean to preserve structure okay so we have to like start thinking in terms of preserving structure and in fact you know since since I said you know structure is really a category embodies structure so um since since category embodies structure you know is there a category that embodies the lack of structure like if you wanted to represent a set as a category right how would you do that yeah dot well but the set has bunch of elements right a single set right elements could be ar I think you discussed this like constant how to represent constants so you could just use the same idea [Music] okay arrows unfortunately arrows have structure because you know if you say arrows then you are saying arrows in a category and arrows in a category compose they compose damn it right so there is a structure there so yeah what do you think category with no arrows ex the idty category with with no arrows right except identity morphisms because we have to have identity morphisms right that's granted right but other than that if we have no no arrows we have no structure right so the category is just a bunch of dots right with this little squiggly you know the the identity morphisms right it's a category that that has a name it you know it's a discrete category discrete category is a category that has no morphisms other than the the ones that have to be there right so a discrete category has no structure in this sense and indeed it corresponds to a set well maybe it corresponds to something bigger than a set because a category in in theory can be bigger than a set but if it's if it's a small category then it's just a set so we can represent a set as as a category right a single set we talked already about a category of sets in which you know every object represents a set here we are saying let's take one set and represent it as a category so that can be done with a discrete category but any category that's not discrete by definition has structure so if we want to preserve structure our mapping has to also map arrows right so what does it mean let's say we want to define a functor from some category C to another category D all right so first of all we Define this mapping of objects so we have object a and object B the functor will map this let's call this functor F let's say capital f so this is fa the mapping of a goes into f a b goes into FB right now in this category we may or may not depending on how this category is defined we may have an arrow from A to B right let's call it f little F Okay so the functor should map this F into some Arrow here in this category well where should it put this Arrow right it should it should map it into an arrow between some other objects but what object right I mean this obviously it must map it to an arrow between fa and FB right so so there is an additional mapping of morphisms that has this property that if you have a morphism between A and B then the fun Maps this morphism into a morphism between fa and FB okay it has to must otherwise you are not defining a functor so if you want to define a functor you have to specify how these uh arrows are marked and notice that arrows between two objects A and B they form a set right let's called the homet and this is the homet c a and arrows from fa to FB form a hom set in D right in in category D they form a homet f a comma FB but it's a set of arrows right so this is a set and this is a set so a functor defines a mapping between these two sets and what's a what's a mapping of sets it's a function right so here we have again a function so for every home set we have to define a function on this homet into the corresponding homet so this is the Corr responding H set for this one right so a functor is really a huge potentially number of separate functions right there's one big function that Maps objects and then there is one function per every homet okay so that's a lot of functions and I haven't even started talking about preserving structure because how is structure defined in a in in a category through composition right so if I want to preserve structure in my category I have to map composition right so let's let's say I have another third object C right here I'll just try to make this picture better right so if I have another morphism let's say G from B to C it will be mapped into FG here right so I'm mapping this morphism I'm mapping this morphism but now in this category I can and compose these guys and I get G after F right now what does g after f ma do well it will be mapped since it's a it's it's an an element from the homet from a to c it will be mapped into an element from the homet fa to FC right so this will be F acting on G F but what about the composition of these two guys I can compose FF FG after FF right see I can compose these two guys what should I get should I get another morphism from F2 FC the same right you have to get the same morphism that's then that's what we call preservation of structure that then what was multiplied here we call this multiplication of of morphisms right then it has to be mapped into multiplication of morphisms here so F of G after F has to be the same as FG after F okay so that's a condition that's an additional condition so I have to Define these mappings on homet cleverly not every mapping will work most of them won't only those will work that satisfy this condition okay so I have to be careful to satisfy this condition otherwise it won't be called a functor it will be called something else it will be called some kind of mapping that does not preserve structure okay and the other thing so what is category about what is category about it's about composition and identity right so obviously if I have an idea that it has to be marked into ID of f right so ID the mapping F of ID La a must be an identity at F A but that's a condition that I have to impose right if if I were just mapping these things really nearly you know the the hom set um like this is this is a homet CAA yeah I'm mapping it into the homet d f a fa a not every mapping is okay I have to be make sure that one particular element of CA namely the identity is mapped into one particular element of this homet namely the identity of this homet right every homet contains every homet that uh is one point homet has to contain the identity okay so this is the definition of a functor a functor is this kind of mapping of objects and morphisms that preserves compos position and identity okay this is sort of obvious way of defining a functor like anything else just doesn't make sense if you want to preserve the structure and this [Music] also formalizes this idea of what does it mean to preserve a structure right because a category is structure so functor is by definition by this definition is something that preserves structure what else can we say about this functor and this is maybe very important thing is is that whenever objects are connected in uh the source category they will always be connected in the Target category right because every fun every morphism has to be mapped into a morphism it's possible that there will be a bunch of morphisms here mapped into a single morphism here it's fine right because it's a function it can squish things together right it doesn't mean that every morphism between fa and FB will have a corresponding morphism between a and b because it doesn't have to be subjective this mapping doesn't have to be injective doesn't have to be subjective we don't require that right so we can drop some information when we are when we are going from one category to another through a fun right but we can never destroy connections and that's very important things so so right you know like if you are mapping as stick figure you know in which you have something between the the you know the body and the head you know if you map it into an actual person suppos this is an actual person you cannot cut off their neck right because there is a connection here there has to be a connection here and vice versa if you were mapping out person into into a stick figure right you cannot break this connection you can squeeze it you know you can but but you cannot break it so sort of like it it reminds you I mean if if you've done a little bit of calculus right it reminds you sort of of continuous Transformations right in topology you don't break connection you're not supposed to break connection so so this sort of is like continuous transformation but there is something like continuous functors and they are more precisely defined functors that preserve LS but essentially thinking about this continuity you know like what what has been connected here has to be connected here canot okay but otherwise you can break you can you can uh like shrink things you can collapse things and uh and in particular you might Define functors that don't break things just like we defined um don't shrink things like like just like we Define functions that don't collapse stuff right we call them injections right so if if a function is so if the mapping of Pal set is injective then we call such functor faithful okay so another name for this stuff faithful faithful so a faithful functor is injective on all homest sets Okay and obviously there has to be another notion um when it's surjective right so surjective then it's called full so a functor is full when it's subjective on H set and faithful if it's injective on homet but notice this why this is why we have to have new names for this not just injective and subjective we have to call it faithful and and four because it's only talking about H set right it's not talking about objects that's very important it's not talking about objects so it actually you know can uh like uh collapse objects and still be um injective on morphisms right or it can uh map the whole category into a tiny subset of this category and still be uh subjective on H sets right so this is only about homets it's not and and of course the the most uh the most beautiful fun is one that's fully faithful fully Faithful functor Is is the one that just you know preserves hom sets as they are it's it's uh it's an isomorphism of homets right so a homet here msing perfectly into the homet here uh subjectively injectivity isomorphically right we we'll sometimes hear about fully faithful FS so they they are they are sort of the the best possible [Music] Mings okay but as far as as as um mapping of object goes you know you can go from one extreme to another extreme you can say okay I'm starting with a with a category that has only one object right what's a what's a functor that whose uh source is just a one object category right I mean one object category will have to have an ID right that's all but this is the category we called one the category one object one morphism that's it so if we take this category and we map it into into inside another category right we have to do the mapping of objects so we'll pick one object right and what is this mapped into well it has to be mapped into an identity here as well right because of functoriality functor must ma identity to Identity so once we say what object we pick here uh the mapping of morphisms is automatic nothing more so a mapping from from a Singleton category let's call it right Singleton category to another another categories equivalent of just picking an object in that category right there are many such mappings because there are many objects to pick know there is another functor that picks this object and so on so it's just just like we had with functions you know functions from from the terminal object from the Singleton object right into any other set pick an element of a set same can be done in categories no problem uh the other way around is is is is a bit interesting right so a a functor that just Maps every object in this category into one single object let's call it C in the sky so it collapses every single you know the whole category into a single object it's like a black hole right total collapse the whole universe collapses into one black hole and all the morphisms here you know they collapse into one identity morphism this is an important fun Factor this is called a constant Factor um and um and of course there are many such constant fact factors depending on on this which objects we take here right so this this constant factor is called Delta C where C is the object where it collapses the stuff that's the black hole right so this this object totally defines the fun every object is mapped into this object every morphisms is mapped into identity morphism period okay so constant Factor very important we'll see it okay now what does all this have to do with programming this is like the the the really interesting part for us programmers right um so first of all most functors well I don't know most but the the most common functors in uh in programming will just deal with a single category right because that's the category of types and functions that's what we have right but but I never said that C and D have to be different categories right it's just looks better as a picture right doesn't confuse you too much right but in principle it has it can be the same C atory you know so objects in this category can be mapped into objects in the same category right and morphisms in this category can be mapped into morphisms in this category right and that that's called an endofunctor it's like endoscopy you know when they go inside your esophagus then endoor goes inside your [Music] category so we well we can have Endo functors in uh programming languages right and uh like in in hll these Endo functors are just called functors because it's sort of assumed that there's only one category so why why mention even right so so what is a functor then translating this let's let's just take this and translate into so objects become types morphisms become functions so first of all um a functor has to be a mapping of types okay and it's a total mapping right I mean we take this whole category and every object in this category has to have an image there right so it's a total mapping of of of types which which means it's it's a u type Constructor in hus we call it type Constructor in other languages you know you might call it a parameterized data type right or a template type or something generic type right we have all these names for um like a whole family of types that is parameterized by other type okay but that's just one part of a function right the type Constructor is the mapping of types so that's that's this one function that works on objects but it also has to map morphisms which means it has to mount functions right so it has to be defined for functions okay so let's let's uh let's just grab some examples and see how we can Define uh we can starting with a with a type Constructor how can we Define the mapping on on function so our friend maybe right and in other languages it's called option or optional right depending on the language data may be of a so a is the parameter it's the type that we are parameterizing of a can be integer can be Boolean can can be whatever right so for every type A we are defining a new type called maybe a okay so we are mapping types two types so a the functor may be Maps a into maybe a that's our mapping of types right so if this is an integer this is maybe of integer Boolean maybe of Boolean and so on right so we have a mapping of types now this is defined as in hus um as nothing or just a that's the definition right it's a it's a co-product of unit and identity right so um is this a functor well what what would it mean to for this to be a functor it would mean that we have to Define some kind of mapping of functions uh between hom sets right so if we have a and we have and some B right B will go into maybe B we have to Define now a function that will go from maybe a to maybe B so if this is F this is the mapping of f using the fun okay now this mapping of functions at least in hcal is called FM it has like the same name for all functors fmap of f okay and so fmap of f is a mapping between maybe a and maybe B and that corresponds to what we are defining here right so let's see what I can erase here uh I can erase this we might need this stuff okay so let's let's just see oh so F map is a function that takes a function from A to B so a function from A to B has the type A R O B and produces another function that goes from maybe a to maybe B okay so this is the type signature of fmap for the maybe functor okay so like if in in in husk we don't have to specify which fmap we mean but in in mathematics maybe we would say fmap maybe okay because fmap is defined differently for every functor in hus we just give it a name fmap for every factor and you will'll see in a moment how we can do this so that we have this kind of polymorphism right but fmap for maybe must be of this signature and let's try to Define it okay let's try to implement it so how do we Implement F map a function that takes um okay so fmap takes some function f so that's the function from A to B that's this guy and produces a function that goes from maybe a to maybe B so let's give it a May a and produce a May B right so and maybe a can be either nothing or just so we have to consider two cases right so let's consider nothing case and separately the second case will be F of just some X right we have to Define these two cases and it's trivial really right right I mean so what what is this it has to be maybe of B maybe B nothing nothing can we put anything else here here yeah instead of nothing could we put something else here bottom bottom okay let's not take a talk about bottom okay uh yeah that's always in h because it's a lazy language it's always possible to put a bottom here but let's let's let's pretend we are in ml huh no bottom so and and they have some optional that so is there anything else we can put here any ideas are we really really forced to put nothing here is it because we our imagination is bad or yeah I mean we could be silly and just put just just FX just to screw things up just what oh just we don't have anything that's right just what yeah damn it we because we don't have an A we don't have a b yes did you stupid weird stuff with Ober recursion that would be more like if infinite recursion that would give us a bottom right non Infinity recursion would give us some type which is not maybe be right so so that we have a mental block as programmers here right we cannot imagine anything else but nothing right uh but but the the truth is we could we could say You' say okay well um let's say it's nothing unless the type A is in integer just zero or something like that just zero just 10 just yeah if if B is an integer just zero right why not it's a what's wrong with that is there something wrong with that silly yeah breaks polymorphism but what's polymorphism yeah we have to do it for all all of these well so I said for all A's you know just like for all A's it's nothing except for one right now you you are on the right track in in the sense that um we want to use polymorphic functions in a language and the language hle kind of tells us that the function should be parametrically polymorph okay so if we say we are in system F which is parametrically polymorphic right that we have only certain ways of constructing polymorphic functions using a single formula then this is the only answer okay but there is something called ad hoc polymorphism right there is parametric polymorphism which will prevent us from from doing anything else but there is also something called ad hoc polymorphism and ad hoc polymorphism is is one which we say well for everything except for integer do this and for integer do something else and it's a perfectly legitimate kind of polymorphism except that we don't want to use it here right but it's it's really important to understand that we are kind of when we are doing programming even in programming in hasal we are straying from mathematics a bit right we are actually imposing a stronger condition than being a functor we are imposing this condition of parametric polymorphism once we impose this condition that it has to be parametrically polymorphic we are making it much more restrictive okay and it's so restricted that it actually leads to the so-called theorems for free right I don't know if you guys heard something this this people talk about theorems for free and so so so this is something that that says because in hcal we actually uh can only Implement polymorphic functions of some limited kind right that are uh a certain type of polymorphism right then that imposes additional conditions on what we can do okay but it's important to to to remember this right but for a moment let's forget about it so indeed this is like the OM chice right for parametric polymorphism this is the only choice now for this guy we have a little bit more choices even if it's parametrically polymorphic we could say this is nothing right we could say it's nothing it's still polymorphic now probably I I don't know maybe this is the homework like figure out if we put nothing here will this actually uh be a good um functor or no yeah Will composition work will functor laws work I don't know so I'm just I'm just like teasing you right I I don't want to talk about this uh but but the obvious choice is is of course say yeah just and let's act with f on this F X because X is of type A F turns a into B so let's add with f on this next and reconstruct adj right and this is a typical way of implementing functors you know just a functor usually has something of type A in it right a functor on a will have something of type A inside and you can just apply this function to the insides of a function and in a moment I'll talk about this and um in in a little bit more detail okay so is this a functor now so we Define the mapping of types that's the mapping of types right or objects let's let's say objects object mapping and this is um morphism there is still something missing right I mean that's that's full definition of mapping but we still don't know whether this is a fun right we don't know is it mapping identity into identity kind of obvious that it does right uh and doesn't Preserve composition that's a little bit less trivial right so maybe we should take a break now and come back to this question later okay