Map/Reduce as an Example of Programming...

BDSBTB 2015: Matthew Fuchs, Map/Reduce as an Example of Programming with Categories

Recording: BDSBTB 2015: Matthew Fuchs, Map/Reduce as an Example of Programming with Categories

oh thank you very much so um you know everybody's super looking at scala and you know Scott Lasorda's combination of low and functional programming and there seems to be I always feel there's a lurch towards functional programming in the community hear more and more about that and when you start hearing about functional programming particularly stuff coming out of out of haskell which you hear a lot about his categories and and category theory seems to be reduced to monads and monoi de and so I was at a scala days or few months ago and remarked on that that I hear it I hear people talking my categories but I don't get the sense that they really understand what it is and and somebody said okay well why don't you come in and give my group of presentation which I did and this was sort of an outgrowth of that I got a reasonably reasonably dissin feedback from that so that's one one reason I'm giving this and I'm hoping that you know the result you'll get a a little bit of taste of what categories actually are that you could actually do some real work with them and that we could actually use them in practice the other reason is years ago when use of fresh and my son gave me this t-shirt which says that's all well and good in practice but how does it work in theory and I've the moment to give it to me said I have to give a talk to I can wear that paper do so this is that talk so what is a category and categories are really you know at one level is almost trivial you think categories have been presented as as competitor with set theory for the foundation of all mathematics and so a category is a set of objects a set of arrows amongst those objects directed so it's essentially directed graph those arrows are called morphisms every object has at least one arrow called identity arrow which is an automorphism it goes back to itself an arrow is composed so if I have objects ABC and D they have done here and I've got you know F goes from A to B and G goes from B to C and H goes from CD d then then they compose and the composition is associative business e on the bottom the identity morphisms basically you get this law here where if you take the identity morphism omit on a and then follow f that gives you that's essentially this that's identical up to isomorphism which you hear all the time with taking f and then taking the identity morphism on on be so on one level I've told you everything on another level well what you always get when you start reading about this is somebody says well what happened to you have sums what happen to your products what happens you've epi morphisms Mona morphisms Exponential's initial objects terminal objects and on and on and essentially what it is is you get what if you have this particular condition and you work at a bunch of consequences and then you're told oh groups are like this Mona's are like this you know just given all these mathematical constructs that work out that way and the general ideas and you can see this playing out in some areas you know of functional programming such as type classes and so on is once you have this machinery if you can take your problem and map it into this machinery you get everything that anybody's proved about these things for free and category theory has been called abstract nonsense and I don't hang out in these rarified fields but apparently in in in mathematics when when people sort of take a big problem dump into a category theory and say well therefore this is x y&z your true it's basically proof by abstract nonsense in a sense it's like if remember when you're learning about NP completeness and it was all like take this problem and convert it into clicks or take this problem and to convert it into SAT SAT and colleagues have absolutely nothing to do with the problem you were given but if you can do that then you can demonstrate that your problem is np-complete and you can say i give up it can't be done so you know this was all very similar to that and that you get this reduction and then you get the power of whatever you've reduced to so you know the slides will be posted you may want to take a picture so here three really good books the David Spivak book is sort of the book i would suggest for for people like us in the sense of computer people the the sort of grand classic and category theory is category theory for the working mathematician this is really category theory for the working non mathematician conceptual mathematics oh and and there's a version of that there's a PDF of that that's available online it's also been published as a book you can go either way the nice thing there PDF of course is you can wander around with it the nice thing about the printed copy is that he gets paid for his work love you and chanel is a very easy introduction into category theory it's you know mathematical introduction so it doesn't get into the programming stuff the awardee book oh yeah and the there's the second version the second edition of the of conceptual mathematics is out the first version you can get is also there's a PDF available online a category theory also there's a PDF available or you can pay for it that's another intro that is not easy you need a certain amount of you got to be ready to bash your head against a lot of stuff but it's very good so there's this huge menagerie of stuff I should just point out one thing with this to mention Exponential's here and though I won't get into those exponential basically if you have a category with Exponential's then you have the lambda calculus hence you can do anything so at a certain level one can do everything that we want to do programming wise in category theory directly is that what we want to do that's an interesting question but you could so the the part of the menagerie that I want to get into because I want to do certain things and this is what i need for that are these guys products sums functors fibers which kinda like hash tables sort of pull backs push out mo noids which everybody's heard about if you've been tending lectures and free monoids which is a generalization of the notion of a list so we'll see whether or not you can actually do any useful those as we go along so first ones the first two are kind of easy products and if you've learned scholar or Haskell or our languages like that you have two pools and products are basically tuples you bite a bunch of stuff together each thing is of some particular types of a fixed length and you can pull out the different pieces of it the little picture on the right on the right over there is how we deal with things in category theories i mentioned before you've got everything category theories about nodes centrally nodes and edges or objects and morphism so it's one of the things that I like about it it's all very very graphic so a lot of stuff that goes on is you read this thing and they draw out this big crazy graph and they go well if you follow these lines then you get from you to here and if all these other lines you also get from here to there and hence everything has been demonstrated for you ok so in here we've got objects a and B and we have this object C sitting in the middle there which is the product of a and B if you've got if C is the product of a and B then you have these two morphisms called projections one from C to a and one from C to B and it so happens if there is any other object floating around in your category which has a morphism 2a and a morphism 2g I mean and a morphism to be here F and G then there is a unique morphism from d to see where this diagram as we say commute which is to say you can get from DITA a directly over F or you can get from D to a through C now the thing that's interesting and talk about a bit further as we go along is C is a limit which is to say that I've said if there's any other object such as a D which has morphisms to a and B then it has a unique morphism to see which in this case is just basically F and G and since its unique that makes this a limit and I'll get to why that's really interesting later on so one of the other one of the funky things you'd get with category theory is you can always chase take all the arrows in any categorical construct turn them all around to their face in the other way and you get another category concept here you get sums and some well I should have said so products as I said you know this shows up in Scala all over the place Haskell all over the place sums are which you get with case classes and particularly sealed case classes so essentially you've got a and B and rather than have projections that you have an injection going in so that means you you'll see is sort of either an A or a B you have to go look inside to find out which is while you do the match and if it's an air you do something with it if it's Abby you do something at here see rather than being a limited Sacco limit or initial which is to say that if there's some other object that you know if you get from you can get there from a and you can get there from be well then you can always get there from C by essentially figure out which one you have and then taking the appropriate the appropriate morphism across another big thing you have so you're getting really fast intro to category theory so just hoping that at the end of this you go alright he spoke for 40 minutes that wasn't gibberish there is something interesting there so a functor so a morphism is is an arrow between two objects a functor is a morphism between two categories so when you're when you're when you're mapping objects and objects really can be anything so objects can be sets objects can be groups objects can just be sort of random crap you find hanging around there's you don't have the kinds of limits so I gave a lightning lecture version of this last friday because i happened to be the hacker dojo on friday afternoon and they do lightning talks there and the only comment they got was you should tell them that categories you can have a category you have the category of categories which includes as a category the category of categories whereas sets of course you can't have yourself as a member so categories don't have the same same invitations that sets do but those objects could be sets or other things but a functor is a mapping between two categories so you have to map the objects to objects and morphisms to morphisms such that love it that diagram commute which means to say that you can get from a in category C to F of B in category D either going along the top which is to say apply the the functor first to get into D and then and then take the the the mapping of morphism f or go from A to B in category C and then take the front or cross and that they both get you to the same place now sometimes you have a functor going the other direction and even sometimes you have this glorious construct called an ad junction which i'm not going to go into but it's beautiful a very important example of a category of cattle functors that i will pull in again and is really very significant in in in sort of looking at MapReduce from a theory perspective or fibers and the case of a fiber you have two categories I wish I could get down in front of it I'm sorry that I'm gonna have to stand here and way if I really like to stand right in front but other Wi-Fi do that then we lose the mic so here for example on the left you have the category of non-negative integers and non-negative integers you have between each integer and the following interview for success or arrow and then of course you have all the compositions of success or arrows so you can get from zero to anything by following some sequence you know some sequence of arrows which all composed into a single arrow now you can take all of those guys and you can take a functor from that to to a category that has only two objects and which i'm calling you even in odd but since the categories that matter what i call them you have a morphism from each in each direction and you can map so you can take all of the what i've done here is i've said I taking all the even integers and I've put them and I've and I've mapped them in this functor to to the object underneath I'm calling even and they all they all are the fiber over even I've taken all the odd ones and I put them in the fiber over odd and basically all of the successor morphisms from even to odd I map 2g and all the successful morphism from odd to even I'm apt 2f and all of the even even length morphisms I map down to the identity morphisms on the other ones and that's where the fiber is basically I have a functor from one category to another and every and within the fiber over some object all of them were physically identity morphism but to some automorphism on the guy underneath and all of the morphisms that go between one fiber between two fibers have to map to a morphism that go between the underlying objects and in fact if you think about it a bit it's very similar to to a hash table or two or two what you get and when you do a redo step so almost done with with this rapid enumeration of strange things we have pull backs and push ads again all you do is pull back and push out you just the pullback is on the left push out is on the right all they've done is reverse the arrows and essentially what i have your given you've given a B and C so I've got see down in the bottom there I've got a has a morphism to see B has a morphism to see and then there's this object d called the pullback and D has morphisms to a and B and what happens is it commutes so you can get you can follow that the dotted line to be and then down to see or you can follow the dotted line from D down to a and across and you get to the same place you can think those those two composed arrows of upper f and then lower G are the same as we say up to more up to isomorphism if you have any e and yet this is the same sort of limit thing if you have some other object e which has a morphism 2a and a morphism to be such that you you also get this guy does commutativity property then you must by definition have a unique morphism from EDD that you can follow along now here that can be all in the cat exam category what we're going to do is I'm looking at pullbacks in the fight in it in a fibroid category so d and b will be in one category a and C will be in another category in in a fiber yes so yeah so if you have so you're given F and G if you have D to a then you pretty much already have D to B because D to B is is that morphism that makes a commute so it's a morphism is not necessarily a function I mean it's really easy I mean it's really really easy as it one does it all the time to think about these in terms of sets and so you think that oh that's a function but really it's the morphism that makes this commute and that's whatever it needs to be so just a small side note so you when you set up a category you're basically saying there's a whole mess of crap that exists just there are these objects and they have morphisms and they're all just exists if you want to actually do work with this you're going to actually have to go from it all exists to I'm going to find these things that I want that actually do whatever it is that i really need and so in taking something like this and going ok we're going to do work with that you need to come at this eventually some way of executing and walking over all of this and in terms of execution if you think of functional programming and other things wit and another style is a program where the idea is you express what you want now not how to get it somehow you have to get from what the hell I mean you as the programmer get to say what but somebody designing this thing Ernie 'the has to come up with how and what the interesting thing here is that you're in functional programming generally what you really what you're looking for is a fixed point or a or some kind of bound that you can that you know that if i move if i start moving along here i will get eventually get to a fixed point where things stop and when i've gotten to the place where the things stop I can you know thinking where nothing changes anymore I can I i can stop working so recursion you know generally recurs you to get down to it you know if n equals zero then you know then i'm done with Fibonacci or whatever what we get in in category theory are limits you get limits and if you can get finite limits then you're eventually then you essentially have fixed point because the the definition of a finite length of a limit is it's this thing that that everything points to and it has a unique morphism so when you get to it well it has a unique morphism to itself and changing so you know finite limits give you what you need to be able to say I've got some I've got this description of this sort of abstract description declarative description of a a category and I need to get and I want to get from this you know from this object to that object and if I can say there is some operation that gets between them which has a finite limit or a finite cone limit then then I'm good because I know that what that the process that I eventual actually use to do this will terminate so because actually as I was doing this like okay how the hell am I going to ensure termination like what do I have around and it was limits I realize it was you know if I finite limits or finite cone limits then then whatever process i use i can be ensured that it will terminate as long as I have these these finite limits so it's a couple more things and then we'll get into using this to an actual problem how am i doing on time okay great i speaking faster than i thought so the thing that every so the two things that everybody is heard of our most people are here probably fruit of our monads and mon oyed should be mo and asterisk d s right so i'll talk about monads slightly later on and in a bit technical fashion but monoids are essentially this you have a set em you have an operation on that set which is closed so for example you know addition addition and multiplication on integers is nice and closed division is not so you have I didn't you have additive and multiplicative monoids on on integers you do not have a division monoid on integers you have a division monoid on unravels so if I set you have an operation on it and mono h effort you have an identity element where you have this property where you're given given any element to this well he is an element of the set but given any other element to the set that you know that op identity is the same thing is identity that opt out which is the same thing as the object itself so in other words the identity doesn't do anything so you know if you're in addition then they'd entities 0 if your multiplication the identity is one and somebody a couple of people have mentioned said also it's just a semigroup so just for those that that care the difference is so well actually not only good so a semigroup just as I've is set and I have an assessed and I have an associative operator on it that's closed I don't necessarily so if the additive the there's an additive semigroup on on positive integers right so the additives the editors immigrant positive interest doesn't have an identity because I defined it not to include zero so that's a semigroup monoid is just like a semigroup but i added but you have an identity so i just i throw zero went to that semi group and all of a sudden I have a monoid I still have a semigroup as well because it doesn't say you can't have an identity it doesn't have two groups add in vs so you know so if I have as I said you know you can't get a you can't get ammo annoyed with division on integers because I don't they don't divide but if if I say no I'm dealing with the rationals instead all of a sudden now i have now i have a group because every groups are every object for every object a there's another object called the a inverse when you must be milked and if you use the operator and the two of those you get back the identity so groups have inverses mo noids do not mow nights have identity semigroups do not there is a given any set there is it there is always at least one mo noid you conform and that is the free mon right and the free mon oyed is basically a generalization of the notion of a list so sudeikis at and then you know take all finite lists of elements of that set with repetition and you have you have a monoid called the free Monod over that set the identity is the empty list because at well the operator is caught is concatenation alright so you can take any any list of things and concatenate them together yet another list so it's closed over the over the set of lists of the underlying set the identity is as the empty said you concatenate the empty set you get the same set together so that's as that and um the the interesting thing is if you want to relate you know sets monoids and free modes for every first set you have what's called the inclusion function which takes anything and puts it into the the free monoid which is basically lists or just that object and if you have a morphism from A to B you you also sort of automatically get a morphism from from the free mon roi de mayo to the free mode or FB but basically you have a list of you live a list from the set of a you just apply f to everything in it and now you have a list of things that are in B and and you can then in fact get back to your underlying you know if you start off with the monoid and you've said as a moment you can get back to the set by basically taking concat and turning it back into the into the the your monoid your regular monoid operator and that basically gives you your your folder reduce and you're back to a single item and you can just sort of drop the list and you're back to back to the monoid and if you want even back to the set so that is a category a tiny taste of category theory in a nutshell so now how do we can we actually do anything with this actually and any any questions at this point what each list yeah I'm not following and two I do not rich which slide is that here yeah yeah okay simple question if H list is HD small shapeless this part of the product I'm still having to understand up and point to what you're talking about so you define a people of two yes three is also product yes yes yes because if you have if I mean using if you have products and if your category has products then then a product is an object in the category and essentially you know that can be part of a product and you can just sensually ignore the ignore the inner inner brace and go okay so I've got projection of the projection the first projection p1 and then to project the second one is I project that the second item in the first item and that gives me the second one and I can get the third room by taking the second one in the second one right so I basically it's isomorphic to I have I have finite products of any size not just 22 yeah whatever all right so so looking at MapReduce I generically map steps are essentially operations on a free Mon oide so I've got a list of things that I've got scattered around and im gonna apply something to you know essentially play the same thing to every one of those and you can break that up you know and and the reason I look at it as a free Mon I'd rather than just as set is that sometimes order matters if you're lucky order doesn't matter you're anything anywhere you want but sometimes it does so it does so you can't just say it's a set i apply to anything it doesn't matter what what do i do things reduction is essentially you know when you go from a map to reduce your is that you're going to sort on some value and then you're going to do stuff with that that's very much operations on a fiber or a co fiber now so that's the whole the thing in a big nut shell and then when i gave the initial talk i was like okay let me show that you can actually do something with this and i went in a sort of encoded word count in that and then when when sales for said go talk to lawyers the lawyer said that's all well and good give us another problem so one thing that i done which works really well in a MapReduce framework is auto-suggest notice examine you see any basic all sorts of websites have this you know you go to the search box and you start typing and as you start typing you get all these suggestions possible completions to what to whatever weird you're typing in so that's fairly fairly ubiquitous fairly straightforward and and and really very very simple to do using using MapReduce and I said okay let me see how this work how I want to suggest fits into their framework and turns out that that it like it's really nice so if you look at it so to suggest categorically so first you've got some stuff that's got your vocabulary in it that basically is free muy nativist drinks then you're going to throw those into into a fiber where essentially you've got you've got two groups of things on the top you have sets of words and on the bottom you have prefixes and what you're going to do is you're going to start off with those and you're basically going to you treat those as a pull back and then you're going to say well I've got this pullback and it's got its got finite limits so just make it for me and because it's got finite limits you can basically just say that one you make that as a single statement and boom you have it all but what but what I wasn't ready for that was really really nice was basically that's how you build it out and you end up with what you want but if you then want to go you mimic the operation of typing in you essentially reversal the arrows and now you're walking through the co fiber on the bottom so you start off on the top with with a bunch of words and you generate this thing and then you start up in the bottom and you walk your way back and as you walk along the bottom you just look up and in the co fiber and those and those are your your your suggestions so and I will now walk what I just said in in in far more excruciating detail so as I said you've got a fiber the on the top you have you're going to have at each point you for list of strings and just for the sake of beating and beating a horse into the ground you're the list of strings and you have an integer which is the length of the prefix you're looking at and the reason for that is and in actually implementation I don't even bother with that but but basically if you have you could have a set of words and the words you know the same set applies to multiple prefixes but if you actually fix the the you know the length of the prefix you're looking at then there's only one one item that could be in the and the bottom of the bottom category that this could be applying to so on the top you've got you know you've got a product which has a free moyet of strings essentially the list of strings an integer and on the bottom you have a single string which is basically take take any of the words from the free Monod pull off the first and end of them and then you've got a prefix and the functor is just that just take the first guy and you know anything in the first guy and grab 0 to pi/2 and that's your your slice right so as I saying you these morphisms are not necessarily functions I need to be complete that can be relations they can be pretty much anything so essentially all that you have on the top is you're going to decrement the length of the prefix and you know the set of words that you have is going to be a subset of the other words you have which is not a function it's just a relation on the bottom though you do have a function you're going to drop the last letter of the prefix it's interesting is you can look at this as a pull back and you're going to walk you know you basically start off with you know we're going to throw in a bunch of words that have a certain length you just start off with those you can find what prefix they're over and then you just walk along the bottom and each point well it just turns out that that you can you can reverse this so you don't really need the morphism on top you only need the morphisms on the bottom and you can always go back up the functor to get the the thing you've the V the object that you need what's needed is as I said it ends up that you have limits because of course as you start dropping off letters off of any word eventually you're going to get to the empty word which has only successors again the empty words so now you've got a fixed point the operation on the top by the time you got there you've got the union of every word in your universe and again you're you hit you know whatever you do you've hit the end although basically only need to walk along the bottom so and then you know later on you want to reverse it you basically can start off with with that empty string and just walk along the co fiber which essentially as i said just reversal these areas along and as you walk along wherever you know every letter you do you just basically take that morphism to whatever whatever prefix you get next and then just go back up and you've got your list of suggestions so you know and once i was asked can you give us another problem i just sort of randomly pulled one that i thought was you know fairly straightforward i mean you know if i'll design like much more complex pipelines but it's like I wanted one that I could explain it was like oh my god it works it's like perfect so I mean that's basically the the strategy you generate your vocabulary which is a free motorist over strings and then you have a functor from that to to the to the over category and you know and then because that's you got these strings but now you look you're dealing with another data structure so you eventually have a function from that then you know you can build the the rest of it by just having the functor in the fiber which get takes you to do to the prefixes and then just say go go build and I mean ideally you're going to build some you're going to create some stuff underneath that basically just builds it and then when you know after you said here here's the stuff go and do I you just grab the Nicole limit in the co fiber right so you start at the bottom and then you can just walk back along the other the other way so that was you never sort of this viewed categorically now the question was how would you know that I had was okay how can I do this in in Scala and yeah if you're going to do this you want to be able to represent the the categorical piece is basically just operations on category there you go okay but you know what is it what's actually functioning on and go well you know you really ought to be able to if it's that high level you should be able to have it function feel to run it on sparc 129 a doob run it on you know and on a single processor and so on so basically looking at you know an embedded and embedded dsl four categories in Scala and you know what I have is is essentially proof of concept but just walk you through the way I I wanted to do this and what's interesting is I think this as echoes in some of the talks I've heard today and yesterday both in the way I did it and and they're the one of the talks this morning about the functional you know machine learning and functional programming just being able to sort of use mono if you get if you can exploit mo noids if you displayed monads this way the stuff that then essentially you get stuff for free and I think the if there's value to this you know your mo nodes and monads are are nice category constructs and yeah you get stuff for free will be interesting to see and you know having just started looking at this and asking of course people to join in joined in the process is if we look at at sort of the whole menagerie of things that you have in category theory which is you know essentially a lot of very very smart people trying to do some very very sophisticated mathematics building at stuff that is of pretty incredible generosity what can we get if we start taking those and go okay if I can map to this category this category will construct you're not just a monoid not just a monad but fiber or push back or whatever push out pull back you know can can be that can be then build other stuff underneath that gives us a lot of stuff for free so that's the the you know I'm just sort of playing around with that now but that's sort of the the question you know the open question for for this and anything like this going forward so I'm circling around Timon ads so as you said the motion ism goes from object to object and if you want to build you know what we call a categorical program is basically you start you know is a composition of morphism than functors and so on going from summa you're pretty much starting at some object or collection of objects that you want and getting to some other thing but you know that that would that's basically an abstraction so you would really want you want your morphisms to actually operate on wheel unreal stuff so i can describe you know a type but in fact if i'm going to have a run on spark I want it you know I wanted to actually run start with our d DS and have our d DS all the way through so you know the morphisms are are going to be spark methods you're basically are going to be operations on or things you do with with with our d DS or the various kinds of our d DS but but in here with the rd's you know basically needs to represent my categorical type so I don't just want to say r dds a this our DD really implement essentially implements a tray which is you know which is free you know free mon art or this our DD basically implements this type which is you know a product of free monoids and and and integers or it represents represents a fiber Rico fiber essentially you know for this issuer a group by you you're going to get you know either a fiber or cough I that's where you're gonna be so to need a functor from from my abstract little program to you know essentially a concave cratic concrete category it should be the category of things you can do with with our DD so to get just a little more obvious so I want to seal up to my these objects in an executing category and I'm given my abstract morphism let's say a to be on the bottom I want to be able to basically get from you know I handed it I want to get back you know if C of a is essentially an RDD I want to get back see you be I want to get back another r DD so essentially I've got what well be called in the trade a Kleiss Lee arrow which is essentially what you got with monads where I've got you know you have you know a to be but you're going to you get you start off with an end you're going to return something that's in the monett so with the state monad you know it's going to be a to be but you get back you know you get back this pair of state and be so you basically that's what i have here so the idea is that each concrete category is a monad so in spark it simona that basically has rd DS as these sort of sealed objects in there my up my abstract morphisms which go from the the categories that I'm thinking about abstractly are these closely morphisms that basically you know if I say I've start off with the free Monod ova strings and I want to end up with the fiber you know basically promoted strings I'm going to end up with with a representation of fiber that's in the spark Monette and it was a fair amount of work to get this to work because there's all this class tag stuff and all this crazy things that go on in there and yeah I probably should have used arrows but that is um so basically I've got these categories these become traits and at this bar category so I've got a spark for you know spark from Otis barked fiber and spa vibrant so on which have various rdds underneath they always show up surrounded by this body spark m-my spark monad so what happens is i give this this this morphism or object that sort of you know categorical of some sort and and it gets handed is a gente to this thing it says well I have you know a what what scholar says is i have this thing that's in the spark mode monad and everything is a spark monad is supposed to thing which we turn something in the sprag minor but this thing you give me doesn't do that so I'm basically a hand it to bind and bind says this is supposed to return something in this Park Monday it doesn't do that let me look for for an implicit that will do that for me so essentially all of the mapping from these things into the monads turn is done using implicit that are sitting inside on the the object that defines the the Monad itself so you have all these conversions so Aida begets you know I gets injected or we just whatever they all get moved around in in this park moon more an ad with with our dd's sittin all underneath underneath everything so since I think I am Justin too bad 0 you know conclusion is basically I think I've shown there this there's this thing category theory it it's as interesting that you know area of mathematics it's extremely constricted generic as very powerful as a whole mess of different things we can actually do things we can do things of a computational interest you directly in category so the the real question going forward that I don't have an answer to at this point but it's like this is what I'm trying to figure out is if you take a categorical point of view if you actually program using this what does it make easier what can we build so that all you have to do go oh it's a pullback and I'm gonna define this arrow and this arrow i'm going to say yet to pull back on the fiber so all i have to do is this arrow is a functor and this one is in the lower thing and i'm going to give you this now go and build others all the crap i need that i can later use how much you know what do we get how much do we get do we get enough to make it worth wrapping our brains around around the programming paradigm thank you we've got time for questions no no oh if you had the answer let me know save me an awful lot of work you had briefly mentioned at junctions said they were ok so disco but I what's the escalator pet shut I'm so it add junctions is um you know a lot of a lot of stuff that would probably get is the notion i can get you know if i can get from from A to B and I know well and there's a lot of stuff I already know how to do with B then you know sort of I guess it's you know I'm sorted down here and I want to get from here to here but I don't know how to get from here to here but I'm liking how to get from here to here and up here I can do an awful lot of stuff and then I get somewhere here where I can get back and um then it's like oh I can get from here to here for free you're almost for free girl life to do is get sort of all of you do is get from ya do this piece and this piece and all this stuff up there again for free and I think that's a lot of where the value is is that you know people can you can take stuff that's already been done and all you have to do is just get there and once you know and once you're there you get to take advantage all the stuff and then you just got to be able to like sort of get back and that's what a junctions does so the way junctions work let's see this is probably a bad idea but i will try but i will try it anyway so uh so generally they're they're like this where you basically the junction you've got a pair of functors so and one of them is a left function one of them is the right functor and it really does make a difference which one is which a Annie's example it is is free Monod and the forgetful functor which basically you know that that's the money you know on one hand you get the function injection to the Ramona and the other one you have the forgetful functor that basically says I forget what you were i'm just going to teach you with some object in the underlying set i don't know what the operator is but basically what happens is you start off so as I said you know you've got you you're down there at sea and you want to get to something but you don't know how to get there so if you can create these two you know this ad Junction you basically can apply F to see to get up to the to the upper category then you can do whatever you know you can do whatever you need over there and you get to D and then you can get back down by taking g back across and if you do that you've essentially defined the morphism on the bottom by just applying these two things and want and then taking advantage of everything that you know how to do on the top and so you know one example of that's very close to this is co and contravariance in function arguments right because you you know you're going up because you can always uh which way is it yes so you can always cast to it you know substitute a function that uses a that uses a base class as the as the as the argument because it requires less and you can always end up with something that a superclass because you know providing more is fine as well so you can think of contravariance as an example of this so though it's basically in a junction with itself but there's a whole mess of these and the first time I seduced introduced to this the book used Galois gawa junctions as the example are like I don't understand what the hell is going I mean that was just like plead it was like you're already hitting me with with you know your hitter e with this really interesting concept that I don't understand and on top of it you throwing this really this concept that actually is twice as difficult at me as your example go away thank you I think we're about out of time for questions but will take more offline absolutely let's thank you Matthews