scale.bythebay.io: Rúnar Bjarnason, Adjunctions in Everyday Life
Recording: scale.bythebay.io: Rúnar Bjarnason, Adjunctions in Everyday Life
you okay my name is ruin our I'm gonna be talking to you about a junctions which is an idea from category theory which is what we really talk about when we talk about monads this talk is very conceptual so you know there's no practical stuff in here at all it's all just totally for fun and and just something to think about in your work and in your everyday life alright so I am a lead engineer at a company called tact I do Haskell full time and we are doing cool stuff with machine learning and Haskell and Scala and purely functional programming and so if you want to work with me contact me I'm a runner at a comm I also wrote this book with my friend Paul it's called functional programming in Scala sometimes affectionately known as the red book and it's really great thank you so yeah if you haven't checked that out you should okay so here's the plan I'm gonna teach you category three step one and it's gonna go kind of fast so you know be alert and try to keep up I'm going to show you this pattern of a junctions over and over again and I'm just gonna say a junction the bunch and then you're gonna start seeing a junctions everywhere in your everyday life and in your work and then you're gonna tweet and blog and tell me about all the cool junctions that you see and in your work cool so that sounds like plan okay so first let's let's talk about categories so a junctions arise in the setting of category theory so I'm gonna teach you all category theory right now all right so when we have functions so this is sort of Haskell syntax when we have a function f and a function G the function f goes from the type A to the type B that is it takes an A and returns a B and then the type function G takes a B and returns the C every time we have two functions like that's that sort of match on the the output of one and the input of the other we can compose them we can compose them into composite functions G compose F that is G after F and the implementation is just you know lambda of X G of f of X so we can compose functions great as long as the types match up and composition is associative that is if we have three functions F G and H it doesn't matter if we consider and we want to compose them into the composite functions H compose G compose F it doesn't matter if we compose F with H compose G or if we compose H with G compose F all right it's all just the one composite function f composed G equals H actually H compose do you compose F sorry so it's H after G after F great and that so all of the arrows all of the routes are the paths through this diagram are the same function and we say that this diagram commutes that is there all the paths through it are the same there a function from A to D great so for every type a we also have an identity function that goes from A to A and sort of does nothing in the sense that if we have another function f the curves are made to be composing that with the identity function that's just F I put composing on either side does nothing right so in general a category is some objects and there could be anything and then there are some arrows between the objects so an arrow has a start object and an end object and then there's some composition of arrows which is associative and has an identity and that's category theory that this is all of categories there in one slide right here so the the category that we just looked at which is the category hask the category of Haskell types and Haskell functions and that's the objects in the category are the Haskell types the arrows between the objects are Haskell functions they have a source type and a destination type right so they're directed arrows and composition is ordinary function composition which is associative because you know the implementation of I've composed decompose H is lambda of X F of G of H of X and the identity is lambda of X goes to X so the identity function alright so so that's the category of Haskell types alright so now let's go back to junctions so what are our junctions well Saunders MacLean famously said that adjoint functors arise everywhere and the Wikipedia definition of a junctions gives us this cool definition that an adjoint functor is a way of giving the most efficient solution to some problem via a method which is formulaic alright so it finds some really efficient solution of the most efficient solution to some problem via a formula and when you hear formula here you should be thinking functor really finds a functor that solves some problem and if we reason about that sort of it the other way we should be able to find the most difficult problem that particular functor or formula can solve go on so that's sort of like why a junctions are cool but I'm not quite gonna just like come out and tell you what they are I'm just gonna give you an example so an example is is one that involves curried and uncrate functions right so what we have is an isomorphism that is we have a one-to-one mapping between curried and uncared functions so curry takes a function that takes a pair so that function takes a pair of a and B and returns the C and we can curry that to turn that into a function that takes an A and returns a function that takes a B and returns to C right so we can partially apply the curried function and then uncor goes the other way if we can take this sort of curried function that can play partially applied and we turn that into a function that returns a pair I'm sorry that takes a pair and returns the sea all right so the implementation is pretty straightforward and if you're not familiar with hospital syntax then the thing to note here is that space is function application so f a B means us send the arguments a and B to the function f I suppose just imagine that they're they're invisible parentheses there in a comma in between if you used to Scala okay so curry and on curry really witness and isomorphism or a one-to-one mapping between these two types so a comma B to C and a to B to C like these two types are the same that is their eyes their isomorphic there's there's a function that goes one way and a function that goes the other way and so there's one of each I mean there's one and in one of them when exactly when there's one in the other right so there's a one-to-one mapping here and really what's going on here I want to say is that this is a relationship between two functors and the functors involved are pair with B and function from B okay so here I'm saying that there's a one-to-one mapping between the arrows or the function types F of a to C and a to G of C all right so when I have one on one side I have exactly one on the other side all right and so I'm gonna have some kind of isomorphism that witnesses that they want to one mapping we can also whenever we have this kind of relationship we have in a junction right and so we can talk about a junctions in Haskell by just using a type class so this is sort of a bit of a bit of Haskell here so type class is sort of like an implicit in scala so we have this this this class a junction that takes two functors F and G so these are type constructors F and G and we say that there's an injunction between F and G when we have a witness to this isomorphism on these types that is the left adjunct we'll take an F of a to be and turn it into an A to G or B and the right adjunct will go the other way right so this is the one-to-one mapping so we just have one function that goes one way and another function that goes the other way okay and then there's a law of a junctions that says that if you you know go left and then right that's the identity right so it's an isomorphism and you go right then unless that's also the identity right great so we can have an instance of a junction using curry and anchoring so a curry an enquiry no witnesses isomorphism that that is our junction between pair with us and function from s and to go back to the sort of the Wikipedia motivation you'll note that the pair with s is sort of an optimal solution to the question posed by a function that takes an S alright so here with s is like a producer of s is and then function from s is like a consumer of S is and those the producer and the consumers are match exactly right and so conversely function from s is like the most difficult problem that you can solve using an S right anyway so this injunction is witnessed by Curie and uncurl so there are there are some other things that fall out of this so whenever we have an injunction like this we also have a unit and a Co unit and the unit goes from from the type A to the type G of F of a so now we have a composite function we can go into that functor right so this turns out to be a unit or a return or a pure for a monad GF all right and that is just taking the identity function across the a junction so so what corresponds to the identity function is going to be this unit and on the other side what corresponds to the identity function is going to be a Co unit for a comonad FG so it's going to take you from F of G of a to a we're going to see that more concretely now oh I just want to say that these these can be defined in terms of each other that is if you want to define on a junction you have to define either the left adjunct and the right adjunct that witness the isomorphism or you have to give the unit and the Co unit and they can be defined in terms of each other okay so the minimal definition is sort of like a combination of the unit and the right adjunct or the Co unit and the left adjunct or the unit and Co unit right so two of these you have to give great so in general we say that F is left adjoint to G when we have a situation like this in in two categories so given the category see in a category D if we have an arrow in C that goes from F of Z to X we're gonna have exactly one arrow in D that goes from set to G of X all right so this is the sort of isomorphism on the on the arrows and in our example with the curried and uncrate functions what's going on here is is the isomorphism between curried and uncrate functions right and the both of the categories here are has the category of Haskell types and Haskell functions okay and the two functors involved are pay with us and function rest and we say that that the pair with us is left adjoint to function for less and so there's another interesting thing that's going on here is that if you start with X in the category C and then you go G into D you get the G of X but then you if you go back into C using F you don't get back to X you get in you get to F of G of X so it's not the same place where you started but there is an arrow out of where you started to where you wait I mean out of where you ended up in to where you started right so and that's the co unit and that corresponds to the identity function you know in the isomorphism and conversely on the other side if you start with with Z and you go F you get F of Z and then you go G you get you get to somewhere that has an arrow into it from where you started all right so it's not sort of an exact inverse it's kind of like it Anna Junction is kind of like an approximate inverse in some sense okay so that's just something to think about so in our particular example of querido and curried functions both of these categories are hask and here the the isomorphism here is so if we have an the identity on the type s to be alright so it takes a function from s to B and returns that same function if we take that across our Junction by uncurling it then we get a function from a pair which takes a function as to be which is a function from s to B and an S and if we take that s and give it to that function we get a B right so so we get sort of a co unit whatever that means and it turns out to be a co unit for a comonad that I'm gonna talk about and then on the other side if we have the identity on pairs a comma s so it's gonna take an A and an S and it's gonna return the same 8 and ask and we curry that identity function we're going to get a unit she's gonna take an A and it's going to return a function that takes an S and it's going to return that a together with that s it's it's pretty simple but I mean the implementation is obvious sort of so what this is what this actually is if you if you are familiar with a state monad this is the unit for the state monad right so a it sort of models a mealy machine so the a is the input to the machine S is the so the input s is the this input state and then the pair a and s is the output State together with the output of the of the machine and so this is going to be a sort of a state machine that does nothing interesting with its state so it's sort of the unit state machine alright so and we can just write that in in Haskell as state si but what's interesting that on the other side we also get a comonad so we get we get the state monad out of this but we also get a store coma net I'm gonna talk about what that is here in a bit okay so a little refresher on the state monad so the the type state si is really just a function so it models the state machine so the input S is the state before the machine runs this the output S is the state after the machine runs and the a in the output is the output of the machine alright if we compose these function functors so pair with us and function from s if we compose them the other way we get a coma not called store and that we can see that as a store full of a's indexed by s that is for every s we can get an a and we have a sort of a current s and we can ask what is the current a but just by passing that s to the function and we can also change what that s is like we can assign it to a different s and then ask what's the a under that right so it's kind of like a you can imagine it was like a forklift where the the position of the forklift is the s and then we can ask okay what's the a right here and then get it yeah for example you can imagine a store index by pairs of integers containing colors as being a two-dimensional bitmap right so if we just sort of turn the crank on our Junction if we take our Co unit for the store cumin add and we map it that is across the the function from s functor we took we end up getting a join for our statement and that's what are annotated that to see like how that that interacts so it takes a a nested state machine and turns it into a regular state machine and the way that works is that it will run the outer machine take the output state of the outer machine pass it as the input state to the to the inner machine and then it returned you know a state machine that does both of those things right so it's a sort of a composition of state machines so that's the joint in the state monad and the implementation is just F map Co unit and remember that Co unit was just you know what was it curry identity great so right so what's a monad all right so a monad takes its two things so it's a functor together with with these two two methods so you have this return sometimes called pure or or unit and that takes an A and turns it into an mfa right and so that's going to be our unit that comes out of our junction and then we get a join which we just saw and that takes nested M so for our Monat M takes an M of M of a and turns it into an mfa so a state machine full that returns a state machine and turns it into a single state machine right or a list of Lists and concatenate all the lists or whatever and usually that's written in Haskell using return and bind and so this you know greater than greater than equal thing is read bind and Scala it's usually called flatmap and that's implementable in terms of unit F map and joint okay so not only we do we get a join for our statement ad we also get a duplicate for a store como net they're just kind of cool so we start with a store we can get a store full of stores and the way that's sort of going to work is that at each index of the store we're going to have a reserve at each location in the store we're gonna have another store that is that has the current sort of index is it's like that location in the store and I sort of annotated that as well and you can you can view the necess store as a state machine that together with sort of an input state and that state machine returns functions that take s's and return a s so basically you have like a state machine that models all of the states of your forklift anyway but that's super cool but why is that useful we're gonna get to that in a minute so first what is the como net well so it's sort of the inverse of a monad so instead of having a return or a unit we have a Co unit or an extract that is if we have a w of a where W is our coma net we can go from W of a to egg we can extract our a out and instead of having a join we have a duplicate that is we can add a layer of w's instead of collapsing two layers of w s-- right and just like where we defined a monad in terms of return and bind usually we redefined coma Nets in terms of extract and Co bind which is that equal greater than greater than thing and that's sort of the you know the dual of the of the flat map operator so and that's implementable in terms of F map and duplicate okay great so why is a coma not useful well so it extends a local computation to a global one so for instance let's go back to our two-dimensional bitmap so you a store full of integers and think of those integers as grayscale values and then the pair type is going to be our x and y coordinates into that bitmap okay so this is sort of an int sized bitmap and so if we know how to take the mean of so we have a particular pixel and we're looking at as we sort of the index into our store if we know how to take the mean of all of the surrounding pixels around that particular pixel we can extend that local computation to a global one to get a low-pass filter of the whole image and we just get that kind of for free in the store coma net and if we sort of do this exercise again if we take the difference of the low-pass filter and X and the identity and we extend that over the whole image we get an edge detector this is kind of cool because what we started with is just a isomorphism between curried and encourage functions but like you know we can do all kinds of cool stuff with just identity curry and on curry right okay so that's one example of an injunction let's go to a totally different example like I said I was just going to show you a bunch of examples all right so let's go to the category of integers so this category is not at all like the high school category the arrows here are not functions the arrows and the objects are not types the whole category is is the category of integers so every object in this category is an integer and there's an arrow from the integer a to the integer B exactly when a is less than or equal to B and then it there's a composite arrow so if a is less than or equal to b and b is less than or equal to C there's a composite arrow a from A to C because a is then less than or equal to C right so arrows composed by the sort of the transitivity property and then there's an identity arrow on every object on every integer a and that identity arrow is just the fact that every integer is less than or equal to itself okay so that's the category of integers and composition of arrows is associative that is it doesn't matter which path we take through this diagram it commutes that is it amounts to the fact that a is less than or equal to D okay so an example of an injunction in this category is between multiplication and division and so this is multiplication and division on the integers so given three integers X Y Z where Y is greater than zero we say that there's this isomorphism or that that Z times y is less than or equal to X exactly when that is less than or equal to X divided by Y okay so that's sort of a specification of what division what integer division actually is so it's going to be some so X divided by Y is going to be some value which is greater than every Z which when the multiplied by Y is less than or equal to X okay alright so we have a unit and a Co unit all right so if we say X and then divided by Y and then multiplied by Y again we get to somewhere that's less than or equal to X that is we may have had some remainder and when we divided we lost that remainder and so we go below where we started right so going across the edge unction and back doesn't give us get us exactly where we started but somewhere where there's an arrow from I'm sorry into where we started so that's our unit and the Co unit is the fact that if we multiply by Y and divided by Y again we go somewhere above where we said cool so that's an injunction and in a in the category of integers and in general when we have on this sort of partial order and a junction on a partial order like this that's called a Galois connection and really what's going on here is that this is a relationship between functions so the functions F and G where where F is multiplied by Y and G is divided by Y so it's a it's a relationship between those functions but those functions are really functors they're functors in this category of integers great let's go take another one so conceptualization as an injunction there's this one sort of from every in everyday life it's another example of a Galois connection okay so consider all the stuff in this room and we're gonna say that there's a category of all the things in this room that is we can take a collection of objects in the room and call that I mean collection of things in the in the room and call that an object in our category for instance like those two chairs over there that's an object in our category and like that column and the carpet that's that's an object in our category and we're going to say that there's an arrow between collection one and collection two when collection two contains all of collection one so this is an order and then we're gonna have another category which is our descriptions of those collections so and that's going to be sort of sets of attributes for instance like the carpet it has the attribute that it's grey and the chairs have the attribute that they're whites and that their chair like or something and so the description the descriptions are going to have this relationship that that this description d1 is below d2 or it has an arrow into d2 exactly when d1 is more specific than d2 that is when it has more attributes okay so I'm going to have two functions or functors so I'm gonna have a functor going from the objects to the descriptions and I'm gonna call that describe and I'm gonna have a functor going from the descriptions to the examples or the the objects and we call that examples and the weight and I'm gonna say that these need to be a junction so what I'm saying is that this my specification for conceptualization is that when I start with some set of objects and I say describe that described thing should be left adjoint to to something that gives me all the examples of that description all right so if I say give me all the examples of the description D and then I say describe all those examples I should get something that is more specific and I actually get a smaller then I know sorry I should get a description that is more specific than the one I started with alright because you know let's say I start with I don't know thing or like person or something and I say well give me all the examples of a person and then I say well describe and I may end up with more specific is like all the people in here might be software engineers and so I end up with the description software engineer which is strictly more specific than then described right something like that and so then when I and the other way when I say well describe this example and then I say give me all the examples I should end up with like a bigger thing because like if I take you know one person and I say describe this person and I get person and I say well give me all the examples of person and I get all the people right so I've lost the so it's not an exact inverse it's an injunction so describe is left adjoint two examples here and it's a relationship between these two functors and this way so yeah let's take a I'm gonna just fly through this real quick so let's solve a simple API design problem using an injunction okay so let's say we want to write this index of thing that takes an a and a list of a and we want to find that a in our list so there's a problem because this should return an integer and the element may not exist in the list right so we have an equality on a we want to compare you know that a with an element in the list and we want to find it but that may not work so what do we return well we can return negative one so we can turn infinity negative infinity not a number or null and you know all of these are things that people have done in the past in api's and you know it's horrible so what what do you wanna do instead so what we actually want is for our return type to have sort of like a special value so we want to say that our type or return type should be a pointed type but it should have a specific point in it that is special and so I'm just gonna say there's a class of pointed types where you know the point is a particular a for a given point to today okay so the question is can we turn any type into a pointy type in a in a universal way that a systematic and works for every type making no ad hoc choices and it works out that there's a functor which forgets that a type is pointed cases where the pointer types from the point it types to the regular types and forgets the point that gives you just the underlying type for instance if you have the integers with a point like negative one you can just forget that negative one is the point and now you just have the integers it turns out that this thing has a left adjoint that takes you from the point types to the point types so that for any type X P of X where P is our this functor which will find us a free pointed type for any type and that's going to be an adjunct on a Junction like this that is it's going to be an isomorphism on these arrows so P finds our free pointer type so the blue stuff is the is the pointer types and the red stuff is the regular types but the forgetful functor thing just forgets that B is a point and so we're we're just going to sort of simplify that into this so it's going to be an isomorphism on these types so turn the crank on the injunction and we just get well we need a right adjunct it looks like this and we left that junk that looks like that and so we get a KO unit and a unit and so for any pointed type B if we have a P of B we get a B etc and so this there we should get a unit for a monad and we should get a ko unit for a komo net in the category pointer types and if we just sort of flip these things around and look at this right i junked that should look familiar to two people who have worked with maybe or option because this is actually turns out to be isomorphic to two option and so this this type will will this free pointer type will just have this method on it that folds the option and that's all right adjoint so it's going to be this function here so it's going to take a maybe a it's going to take a sort of a default B it's going to take a function that that turns the a into B and returns to be right so this is sort of fold on options or on baby's great and we got a joint for a maybe monad and we got a duplicate or maybe comonad in the category of pointed types and so what we really want is for index of to return to maybe integer or an option integer and so this is sort of this idea of option or maybe falls out of junctions like this and we can do this for Mon rights as well like oh can we turn any type into a monarchy yeah we can so I'm honored you know has an append like you can take two A's and put them together and it has an empty a if for for some notion of empty which means that if you append the empty to anything that's just that same thing so can we turn any type into a moderate yes we can we just have a forgetful functor from the mono to the regular types and that turns out to have a left I join that gives us a Fremont wait for any type X and we just turn the crank on the injunction and see what we get and so what we get it is something like this here and that should look kind of familiar that is full map so for any mono dem if I can go from A to M then I can go from T of A to M for any foldable T great so the canonical example of that it's list so my Fremont Fremont is you know really just list so let's fall out of this as well we can do this again can we turn a functor into a monad yes okay so there's a free functor that takes a functor to a monad and it's going to be a left I joined to a forgetful functor that takes a monad to its underlying functor right so for any functor f free of f is going to be a monad all right so we just fill in the types in the injunction and see what we get so we're gonna get this thing here we're gonna get a KO units for a komo net in the category of monads and that is going to go if we have a free of em of a for some monad we're going to get be able to fold that free into an M of it so given that there's a monad and we're gonna have a unit for our our free mo net as well and you know if we just keep turning the crank we get a join for our free monad and we get a duplicate for a coma net which is it's going to be a coma and in category of monads cool so free in general is left adjoint to forgetful functors and we're gonna have also sometimes we're gonna have right adjoints to forgetful functors and those are going to be Co free so we can get Co freako monads this way as well so just as the last thing a junctions can pose so if you have F left I'd join to G and P left I'd run to q yeah FP is left adjunctive GQ and which is really cool because in general if you know one half of an injunction you can find the other one so if you know any two of f PG and Q you can find the other two and this is used in these awesome papers that I'm just a flash up here generic programming with the junctions by Ralph Hensley and calculator functional prototype of a Galois connection based proof assistance these are awesome papers and they talk about how to do generic I sorry yeah generic programming using a junctions okay I don't really have time to go into these sort of philosophical things of a junctions but come talk to me afterwards if you want to talk about a junctions tomorrow so whenever we're looking for a general and natural and elegant solution to to some problem just Express the problem as the functor and find this adjoint it's as simple as that so you know I joined punches are everywhere and we should totally go look for them thank you [Applause]