Profunctor Optics: Categorical Foundations with Bartosz Milewski

[00:00:00][Music] [Applause] and I I have to start by apologizing because usually I try to explain everything in great detail very slowly and so on this time I have to like rush into the hardcore category theory because I want to get to a certain point and I have to stick it in in within 45 minutes so bear with me it's okay you know if at some point things get so confusing that you stop understanding and it's perfectly normal in categories here it's always like this you know that you you understand things to a certain level and then the next level seems like a totally weird thing but once you get exposed to it things clear out after a moment so I'm just going to jump directly into pro factor optics so so I don't know I will explain some of the terms but not all of them so here's here's the definition of a lens and the prism and notice okay so first of all for all this is Haskell okay for all means it's a polymorphic function it means that it will work for any P okay but what is P CP is acting on a and B on the right hand side you say PA B PST a B and s and T are types so this is just like taking types and producing new type okay a pro factor is a generalization of a functor takes types it produces a type so so P is really a what we call type constructor because it takes types and produces types okay so when I first saw this kind of formula I was really puzzled because like so this works for any pro functor like you generalize whatever pro functor you give me it'll work and it's a function that takes this type PAB which is generated from two types a and b and produces a new type an element of a type PSD which is produced from s and t moreover so this is not all there is also this strong P and choice B that these are the constraints they say that this is not just any pro functor but this is if these are pro factors that actually satisfy certain constraints okay but the important part of this and this is why it's so useful is that this is just a function you know you see this is a function from PAB to PSD is a simple function no and and the beautiful thing about functions is that you can compose them so if you have two functions like these you know one's going from PA B and the other is going through to PST and you have another that goes from PSD to some p RZ you know whatever you can just compose them and this is why lens is composed with this dot in in Haskell at least because this is AK function compositions just simple function composition right so this is a great representation for composing lenses so lens just gives you a view into a sub object of some object if you compose it with another lens it will give you a sub object of the sub object and so on you can go as deep as you want to telescoping into a data structure so let prism almost identical except that has different constraints it's called choice and here I wrote these two constraints so if P is a profound or then strong means that this Pro factor supports this polymorphic function from P a P to P a comma C that's a pair a C so it's a Cartesian product of a and C right and BC so so it means that if P is you can think of a pro factor as as a relation between two types okay that's that's like one of the ways of of imagining it if P if a is in red in a relation with B right and then also P AC will be in relation with PB see what does it mean that if you have a data structure that can be decomposed into a and some rest called C then you have a relation with being and this rest C as well so a and B are these sub objects and C is like the environment in which they live okay so that's that's the intuition behind it now choice is almost identical except that instead of a Cartesian product pair it has the either which is Cartesian Koch artesian product or some some type right but other than that it's very similar right and the definition of a pro functor is that it's sort of like a functor but it can a factor can lift one function at a time profiler lifts two functions at a time from A to B and from C to D but the funny thing is that a and B are kind of inverted you see PB C goes to P ad that's that's an important thing about pro factors okay so now let me show you some pictures okay let's let's start by read refreshing some ideas about functors so if a functor in category theory is just a mapping between categories so if you have an object a look at this picture you have an object a in one category you map it into an object si in another category you have object B it's mapped into an object FB but in a category you also have these arrows think of them as functions for full-time being right so you have a function from A to B then a functor will also give you a function from FA to FB right so this is the definition of a functor in in Haskell it just says that if you have this type constructor F type constructor means mapping types two types so it's a mapping of objects F not maps functions two functions right takes a function from A to B gives you a function from a FA to FB okay pro functor let's this picture does it with two categories at a time ok so it takes two objects one from one category one from another category I mean in what follows will will stick to the same category but it doesn't matter I mean in principle this could be different categories so it takes two objects a and C and creates a new object PAEC or new type PDC so it's a type constructor that takes two arguments it takes B and D and produces B PBD right now the lifting of functions is funny because it it takes a pair of functions and lifts them right but one of the functions goes in the opposite direction because you can think of this as it's consuming one type and outputting another time so when you are consuming you have to like adjust the input right when you are producing you adjust the output in the opposite direction and in category theory this is just this is really still a functor but it's a functor from a product category and this little op means that it's an opposite category an opposite category means that all the arrows are reversed this is why we have the reversion of where the function goes okay so this is the introduction now when you have two func tours okay you can now think about okay can i map one functor to another and the mapping between factors is called the natural transformation so X is an object in some category right FX is the mapping of this object into the category using the factor f GX maps using factor G so we had two functors right we are two functors and since these functions go into these two objects FX and GX we can take a function from FX - GX for every object X if we take a function like this then we get a natural transformation what does it mean to pick a function for every object or every type it means you have a polymorphic function right the functional except works for any type so in Haskell you can define this type of natural transformation that the squiggly arrow as for all X so for every object X it's a function from FX - GX that's a polymorphic function I mean this for all X usually is omitted because Haskell figures out but but it's it's it's a definition of a natural transformation and here's an example of natural transformation that transforms a list functor list as a functor and maybe is a functor optional for Scala people right and it's defined that on an emptyness gives nothing or and on a non-empty list it just gives the first element of the list so it's a safe way of taking the head of the list right but it's it is a natural transformation between these two factors there is some commuting diagram that goes with natural transformations but I'll skip that part okay ah so now that you see what you know look at the natural toxin it has this for all X right so it's sort of getting similar to the lens but a lens is for all P strong P P AV PSD okay so when I first saw this I was thinking okay but this is this looks like an natural transformation but but it's between something else I mean this is this like in different category how can you have natural transformation where you have profound doors by and then there I figured out that the only place I knew very little about category theory but I knew the the yone dilemma and unita lemma is one place in which you have this for all the it's just like a pattern recognition okay here's for all here's for all that may be own a dilemma is relevant to figuring out the lens okay so let me explain what a yone dilemma is so your knee dilemma says that there is this special factor called the reader factor that is just a type of a function from a to X so it's a functor e in X a is just this parameter is just that there are two types a and X right it's actually a profounder but you know it's looking just at the X part it's a func Tory right and and here's the like the definition of Y why it is a factor instance factor I can define F map for its how to lift a function right now you'll need a lemma says that if you have any factor f then first of all you can get to this functor F from the reader factor so reader factor is a very special factor because it has natural transformations to every other factor and the set of these natural transformations between these two factors so now remember two functors natural transformations which is a polymorphic function between two factors right the set of these natural transformations is equivalent to the value of this factor at the object a okay and here here below its it's written as a natural transformation natural transformations for all X this is the reader of X this is FX and this is equivalent to F of a now quickly the intuition behind this the left hand side is a function that takes a function okay so it's a higher-order function which is polymorphic in X the right hand side is what we call data structure it's like okay could be a list right take type a you get a list of a so there are two very different representation one is this what we could normally call data the others function a polymorphic action polymorphic higher-order function these two representations are totally equivalent and this is this is what is great about the on a dilemma in programming because sometimes you want to use a different representation for your data type for performance reasons or for four reasons like in this case it would be because it composes better okay so that that's that's a great point of your new dilemma and here's a little proof that the UN a dilemma works and actually it's it's kind of in Haskell it's almost almost trivial why this should work okay but I'm not going to go into the details in there because I want this I'm interested is the special case of yone dilemma where the second functor so so it's a natural transform not natural transformations from a reader factor to some arbitrary factor F I can replace this arbitrary factor F in particular with another reader factor right and then I get this formula at the bottom which is the own a dilemma for the reader factor here right it's a it's a different reader it's it's a reader from be the first readers from a the second readers from B right and if ice so this is my FX right if I replace X with a on the right-hand side of the on I dilemma I will get F a is function from B to a alright so it's B to a so so this is this is a really a huge huge simplification you have like a function that takes a function and returns a function it's polymorphic in X and it's totally equivalent to a function from B to a notice that they are reversed like a is here B is here here they are reversed and this is called well this is just a special case of y orn a dilemma but it's used in so-called yone de-embedding so I call it yone time bedding and now remember I wanted a polymorphic thing that's polymorphic in pro functors so let me makes it make the next abstraction and say okay how can I use a uni dilemma so that for all actually takes a functor rather than a type well from the point of view of category theory that's a very simple thing you know functors form a category what kind of category it is functors are objects in this category and arrows in this category are natural transformations that I mentioned before natural transformations go between functors okay so they form a nice category and since they form a nice category the only dilemma applies to them as well so I can take the same you own a dilemma replace my ex with a functor and I have replace my functions with natural transformations I'm not getting in a dilemma in the factored category so above is unity dilemma here's the only element functor category you see what changed i just renamed these things so that they look more like functors I replace them a and X with G and F right and I replace arrows with squiggly arrows right which is natural transformations so the mapping from natural transformations between factor gnf there's a natural transformation between factors to H and F and the result here this is equivalent to an actual transformation from factor H to G okay and I have finally this for all F where F is a funk or okay so I'm getting very very close to lenses but not quite yet right but let's use this little example okay so my first protists let's construct a toy optic you know something really really simple right and and so the trick here is I want to create a very simple optic so I start with the yone dilemma in functor category that's the top line right now these are these squiggly arrows are natural transformations so I'm just writing them explicitly using for all right so a natural transformation from G to F is for all X G X to F X now reflects the second one and the third one so this is just a trivial substitution like definition of natural transformation right and now here's the trick I can pick for G and H I can pick anything I want okay any factor well in particular I can pick a reader functor again right like a standard trick just stick her in there factor so GX is a reader factor based on a HX is the reader factor based on s I replace it and now what look what happens in these internal for all's I have reader from a map to F X but that's yo Naida again reader factor map to ever this is a natural transformation from the reader factor I can replace it with FA here I can replace it F with FS and at the bottom I can replace it with with with the reader from s2 from a2s right so after rewriting this here's the final result okay and I can say this is type toy lands parameterize by si for all F where F is a function FA - FS so that looks very much like you know like if you if you squint this looks very much like one of these profounder lenses except that with a func door right and I'm showing that this is equivalent to just a straight function from a to s okay so I don't know if you--if you see the pattern here's like this is sort of the representation the sort of like pro functor optics type of representation and this is the like simple implementation like like a lens can be represented by setter and getter right this one is just a getter alright it just gets us out of a very simple so I'm on the right track right but now I want to do this for pro factor so yone de for profound tours but pro factors are really from categorical point of view they are they're simple they are just factors from the product category C op C to some other category right but I have to like rethink things a little bit like what's an object in a in a product category it's a prop it's a pair of objects what's a morphism it's a pair of morphisms right so I'm now start I will start working with pairs and what's a what's a reader you know in this category well it will be a pair of functions right like I read there was a function type this is a pair of function except that the first function goes in the opposite direction so I have a pro reader from a pair a B to a pair XY and it's a pair of two functions Y goes from X to a and the other fur goes from b2i the first one is in the opposite direction because it's a pro functor it's the opposite category that's why right yeah and the second line just shows that that pro reader this guy is actually a pro factor because I can lift a pair of functions one by prepending one by pro-bending right and pro yone does again the same thing except that now I have to work with pairs of objects so instead of for all X I have for all XY and I have a pro reader so a pair of functions goes into a pro funked or arbitrary preventer P P XY and pronator says that you know this Pro yo of PAB is isomorphic to PAB so now again I have a representation of a pro functor which is that this datatype kinda in terms of a polymorphic function or in natural transformation right so so this is the this is the bottom line is just rewriting it in this form for all X Y I have a pair of functions I just encourage them and hurried them and going to PA X Y and it's equivalent to PAB so this is really just substituting one thing for another and just figuring out all the direction of arrows have to be changed and so on but but that it's pretty much trivial now that was a you need our four Pro factors now I want to do your own ADA on pro functions I want to go to a pro functor category Pro factors also form a category okay they have natural transformations that are sort of like these two natural turn stories that take pairs right so there are pairs of functions but the idea is exactly the same so I have natural transformations and this is what it is you know this is like the your natal amount pro functors I replaced some letters with P and Q and and I replaced arrows with squiggly arrows like this is actually this kind of anita embedding version of the yin a dilemma right and below I rewrote it using the definition of what what is a natural transformation what is the squiggly arrow for pro functors right so it has for all XY q X Y P X Y and now I have finally my for all P okay that's that the big step I have for old piece so I'm close and I use the same trick as I did before you know I I I replace Q and R which are three parameters in this formula I replace them with my pro readers right so I put pro readers here and when I put pro readers in here I get a unit a lemma for pro factors right so I can reduce this I can replace x and y with a and B and I replace X Y here with SMT you know this these are different x and y's they are scoped within the for all right so if I do this I can now perform the urinator again and I get this formula for all people factor P PA be PST okay that's that's that's my optic pro factor optic right and from this double application of yoni dilemma get that this is actually qst but my Q is a 2xy to be okay so I replaced I just wrote this explicitly so this is a pair of functions from a twist and a function from T to B and if you've seen Pro Factor optics this is the definition of ISO okay and in the Haskell library so like this is the the mote the simplest pro factor optic that there is but I'm still not getting lenses and prisms right so what's the next step the next step so so this is this is what it looks at so I got the first line I saw okay that was kind of easy but now I want to generalize it to get lens and prison but lens and prism have these additional constraints right strong and choice and if you notice that there is a very similarity between strong and choice just replacing Cartesian product with what is called co-product there's some time right so there is actually a category categorical thing that's generalizes product and co product at the same time and it's called a tensor product so a special case of a tensor product is Cartesian product and Cartesian copra that hey so I can just say let me go totally general and combine lenses with with prisms right and in in category theory something like this is actually called the tambura module okay so this is the definition of Tambora module translated to haskell right so I just replaced pair and either with this tensor product and that's it so now I can work with prison and lenses at the same time but how do I get I have to go through a junctions okay so runner explained the junctions I didn't don't have to so we when you have to functors and I actually have an example that's exactly like like guru NARS okay did the a junction between pairing and function space right so I have a functor f going from A to F a we can have a fun to you that takes B to you B if these two sets of arrows are isomorphic then I have an injunction okay which which means sort of that instead of preparing the initial state using F I can modify the final state using you okay so argue you have functions and and they are in one-to-one correspondence the ones that I prepared the input and the ones that I modified the output but of course the preparation of input and modification of the output have to match magically and that's called the injunction right and because of this ad Junction this particular junction between Cartesian product and the function space right this is called currying there is a version of unity dilemmas called Koyanagi lemma that works like this and this is an existential quantifier right Hostel does not really have a notation for existential quantifier but you can fake it using a universal quantifier so I won't go into detail but it's this notation actually is useful so there exists an X so I have a data structure within which X is hidden right I know there there is an X but I don't know what it is some of the gave me this data structure it's a data hiding right and it contains FX which is like a container of X's functor acting on X you can think of a container of axis and there is a function from X to a and either even though I don't know what X is there's one thing that I can do with this I can f map this function over this container and what what happens I get FA right so this is this is the own a cone a dilemma in a nutshell so these two data structures are equivalent so now I want to do a yone de and combine it with injunctions right so I wrote the unit ulema above it and remember a and B are just arbitrary parameters there are external things I can pick something from a and pick something for B okay so the the clever pick is to replace a with FA and replace B with FB where F is a some funk that hasn't it that is enjoying through some you okay so if I replace them I can then use the adjunctive because I can say instead of preparing a with F I can post I can modify X with you right because these two are in one-to-one correspondence right because of the injunction and the same here in same here so I did this a junction I performed this a junction right and and the result of this okay if I do the the junction also in the result of of this identity I get a function from B to you combined with F acting on a now these are two functors a composition of factors again a funk tour right and this composition of two adjoint factors is actually a Mona and rune are also explained that okay so this is this is you Nader with the Junction's and I just want to do the same thing but in pro functor category okay so now a functor in a pro functor category means it takes a pro functor maps it to another pro functor right takes a natural transformation maps it to a natural transformation okay so this is the at the top it's just repetition of of the united Emma in Pro factor category right and this is what we get applying it right so III have just rewritten the urinator lemma right in the profiler category so so the only change is that I suddenly have this you here right I started with something that was with P with F and I I put a new on the right hand side using the a junction right so this is like the same formula as before except that I replaced things with profile doors right now what are the two categories in which I'm working that's very important okay I'm working with the tambura category in which my pro functors are actually Tambora pro factors which means these are these Pro factors that have this additional structure they have this mapping right this mapping from PAB to P a cross C B cross C right you is I take as you as a functor that is a forgetful factor Bruner also talked about this forgetful factor just forgets the structure so if I have a profounder that's a Tambora font or pro factor i can map it into the category of profilers sort of it the same profounder but forgetting it that it has additional property I'm just forgetting about this property nothing else but there is an adjoint factor that will take a any pro factor and make it at umber a pro factor it's called the free functor free functor takes something without structure and makes additional structure on top of it okay so this is my formula for the tamborim oh and I say Tambora P so I'm working in the tambura category right and this is suddenly becoming very lens like because the tambura constraint is exactly what we need for combining lenses with prisms right so here it is this formula from the previous page right and now I'm doing the identical trick as before right I'm replacing Q and R we the pro readers then I do the internal yone das right and I end up with this okay so the the the line before the last one the line before the last one still has these use right but this you means that I take a pro factor with some structure and I map it into a pro factor without this structure but it's the same Pro functor right it's really the same profile I can skip you in Haskell I can just skip it it doesn't do anything right it's a forgetful factor it takes a factor that has some structure but makes it like a regular factor without doing anything right so I have suddenly for all P Tambora P P a be two PS p so this is exactly what I wanted this is my profounder optic that combines lens and prism now let me look at the right hand side ok right hand side has this u F right and I said this is the Monad so I'm I call this monad Phi now I'm not as smart as to figure out what Phi should be but there is a paper by pastro and Street that actually dealt with some Barra modules and they they came up with formula 4 or 5 okay so in categorical language this is like it's it's a KO end this integral sign means ko end this is like tenth tensor product whatever it means it can be translated into Haskell very simply a KO end is translated into existential types like an N this is a universal current is an existential type so it means see x and y these three things that are multiplied there they are just a standard tuple because we are now working in instead so it's a tuple of three things so it's a pair and a as that's a home come home set which is really a function from s to C cross X from C cross y - 2 T so it's a pair of functions and then it's curious so the the property that this Phi has is that you give me any pro factor Q whatever profiler you give me the result Phi Q is the tambura provocateur automatically okay it's freely generative Tambora Pro functor okay now if you remember in the substitution I replace the the Pro functor there the R and Q I replace them with repro readers right so I have to apply this Phi to a pro reader right and if I apply this this factor to a pro reader so the Q XY is the Pro reader right so I replaced Q with this and and then I can use the the Korean a dilemma to eliminate this Q because this Q is just a is a pro reader right Q becomes a pro reader and the pro reader paired with something like this exist cxy exists X Y this is just a a : a dilemma so I can replace x and y with a and B okay so I get five QST exists C and this is I just I'm just left with this pair of functions from s to C cross a from C cross B 2 T ok and now I'm just rewriting this formula for two different tensor products the first one is a pair right and I get a lens right because I get a lens sdab after doing the yone da I get this exist see that s goes into CA CB goes into T do you recognize this as a lens it says that the whole data structure s can be split as into a product of sum see the environment and the focus a and again if I have seen and the focus B then I represent a an existential definition of a lens and prism is exactly the same thing but I replace the tensor product with either right and this is what I get so that shows you that the pro functor representation of lands and prism can be directly translated into our standard you know version of lands and prism using a pair of functions okay this is the picture that illustrates it right that's the lensing or and that's it okay [Music] [Applause]