Duality and How to Delete Half (minus ε)...

Scale By The Bay 2018: Greg Pfeil, Duality and How to Delete Half (minus ε) of Your Code

Recording: Scale By The Bay 2018: Greg Pfeil, Duality and How to Delete Half (minus ε) of Your Code

you all right so I'm gonna start with an apology because this is the title of the talk that you've all seen although the actual content of the talk is a little different it's categories and how to delete 96% minus Epsilon of your code so hopefully you know a little bit more ambitious but is what it'd be nice to be able to delete 96% of your code right I feel like that'd be really helpful so Who am I I'm as mentioned I'm Greg file I work with formation which we're hiring we like Scala people we'd like FP leaning Scala people especially but we will help you lean FP if necessary and I work with a bunch of people you may be familiar with Ross Baker Chris McKinley who gave a talk earlier this conference Chris knotty comb is a well-known speaker as well and Paul Snively who was here and is giving a talk in this room at 3:00 p.m. that's the right time right all right so come to that one too and yeah so so people who know me may know me for my work with recursion schemes and talks have given on recursion schemes the common question I get now is where are the turtles which refers to the name of the library I didn't finish which is a recursion schemes library for cats but thankfully Andy Scott has picked up my slack and he wrote a recursion schemes library for cats called Droste and so you can check that out I'm technically contributor but I haven't actually done anything there so also a Valentin Casas and I have been working on a recursion schemes cookbook to kind of you know answer real world questions that people have about like why they might want to use them or what to do in different cases of like that so hopefully that's helpful people who are trying to get into the idea this talk is not about recursion schemes but it will use them a bit as an example this talk is also a literate Scala presentation so this is the SBT build that builds this talk so it works the kind of stuff that requires it needs a type level compiler uses higher kind kind polymorphism which is a very experimental feature that's only available in type level or dotty and it uses cats and kind projector are people familiar with time projector yeah yeah it makes some some type level syntax a little bit nicer and it's kind of extremely useful if you're doing any kind of FP stuff in Scala and imports are just a bunch of cats imports so that's that's everything you need to do what's in this talk so to begin as everything that I do involves we start with a little katha katha is the the Greek word for algebra basically it basically academies to to collapse something down and an algebra means to reunite pieces right that's what an algebra is is like combining pieces in various ways so they're they're basically the same thing just there's different languages so what is a cat a cat is a generalization of a fold are basically if you're familiar with the foldable type class and anything you have this this notion of you know taking something that basically fold are is very specific to lists you can think you implement foldable for lots of different types right but really what foldable does is it forces you to throw away any additional information and treat your structure as effectively a list of elements and and so this generalizes it so you can actually kind of fold arbitrary tree structures down so fold ours is the specialization of this two lists and so what this does is this takes two types right in this type this is a tight class so it takes two types that have some relationship between each other and that relationship is defined by this this function katha again fold are basically and so what it does is it takes some function that takes that F type and you know gives you some some results from processing that that functor and then can turn that into a function that processes the T type and returns you to a so to give you a simple example of what this is actually useful for I kind of try to pick the simplest thing which is basically natural numbers so natural numbers there's a zero case right and then you could have a successor of some other natural number and so as at the top there you can see the examples the zero is just zero and successors successors successor of zero is three right very simple recursive structure right this is a self-referential structure and and so we can define this kind of we can just say that it's recursive and the way we do it is we associate that natural type with the option functor and so in this case right you can kind of just squint a little bit you see that none and zero are basically the same thing and successor and some are the same thing except in some you have a type parameter where that naturalist so you're kind of removing the recursion from that structure an option is the same as natural where it's not recursive in itself and so so this is the definition well you know it kind of elided that part but but you can do this for any kind of recursive structure whether it's a list or arbitrary tree structures Jason things like that and here's a simplemente ssin of how you would use cata you would handle the two separate cases effectively zero and successor saying what to do in each case and then it would apply it over the full natural number and give you you know the result so this is just to give you an idea of what cata does it's it's really not that important for the talk but you have some context so again we just have this quatre to start with so you make a nice library it has just this one function now you can define these you know these folds for any any kind of interesting types and you have this nice little library then people are like well if I can take this thing and like you know collapse these structures down to some value maybe I can do something that can build up tree structures for me it's like oh yeah that's a good idea we can we can add sort of this other function called an ax sorry for the Greek names but that's what they tend to be called that builds up arbitrary tree star structures okay these two things fit together right these belong in the same library this is a reasonable bit of code so now you know now we feel like gone from cat oh we've added an I we have a slightly bigger library and it's nice because these things feel symmetrical right you get this this extra bit of I don't know just it just feels like a complete library kind of right like these things belong together well then people start wanting to do other things so you have this this cat a morphism and then somebody says like well you know I really I have this thing it's kind of like a cat a morphism sorry all these words have cata at the end or I'm sorry I have morphism at the end so cat is short for cat a morphism and para morphism so they're like oh I have this fold I want to do but in my case I need to kind of look at that original tree structure as I go through I need to maintain that in some way and there's a variation called a perimortem does that or somebody comes along and says like oh well I kind of need to see like some of the results I've previously calculated along the way of traversing this structure and be able to use those again and later likely a shion's and that's this histo morphism where histo is short for history where you get you know the history of all the things you've calculated along the way and so these are different variations and you know they okay cool yeah I've made this family of stuff and for each of these variations there's another variation on Anna so you end up with you know you now have this kind of grid of these operations then again they all fit together they all have similar shapes and they all have these relationships and your library is getting a little bit bigger starting to feel like maybe yeah it is justified that it's its own library and not just like added to cats right and then someone says this is the one that comes up all the time it's like oh well I want to do this but I want to have a menthe add on my you know result basically everybody's using mana ads in like and they're everywhere and and so like oh okay well yeah I guess we can have a monadic version of this where the function that's passed in returns something in a mana and therefore the resulting function returned something in amman AD so now once again you have your another another level rate of things and it's getting it's getting deeper you're like oh okay cool yeah this is definitely a significant piece of work this this project it's uh it's something and you know as you as you add these things every time you want to add one thing right you're now adding like a family of like four things you're like okay I have to add all four variations on this thing and then more stuff comes along and people are like oh well you know I have this recursive structure but only certain things are allowed at certain points in the recursion I want to like restrict like say you have you representing some language you have an if construct you want to make sure the first argument that if construct is something that represents a boolean in some form and so you want to restrict what structure can be in there and things like that so that adds in these other kinds of recursive structures and we don't have to care about what they are too much but that's you know one of the things they allow and so now we have you know okay now we've got another dimension and this one goes off the side of the screen there's a third a third one of these and now again it's like okay oh I had some new idea I want to add to it now I have to add like 24 variations on that thing and it's getting exhausting to keep all these things in sync across like files that are getting larger and larger and and yeah and there's way more right so it goes beyond just this like this level of stuff and quickly there's just this thing called L got algebra is that at another level duplication there's a feeling with cumin add and monadic transformers as well which added another level of duplication so all these things right each one of them like doubles the size of this library and I definitely feel like a really significant piece of code now like and so how do we how do we take this like massive thing that doesn't fit on the screen and and try to get it back to something that that is reasonable basically and and so that's you know that's what I'm trying to do here is show how we can use these things that maybe we think of as you know it's too abstract category theory and and things like that and like how we can actually apply those ideas to you know eliminate tons and tons of effectively duplicated code and yeah so let's see so the first thing we can talk about is early we saw you know there's those variations we talked about in here which is like there's histo katha and the one at the bottom the para is kind of cut off those are different variations that give you different kind of extra information as you're folding something and it turns out like all those structures are are comon ads right so KO Frieza comonad there's tuple at the bottom for Paris a coma ad and so you're like well maybe there's thing we can do we can lie catacomb and I would constraint and just like you know eliminate all of those and treat them all the same way and caddy you can kind of think of us having identity the identity comonad there which is like the know up of of komen ads and monads and so maybe there's some way we can just like abstract over a row comonad right this is something we do all the time right if you're doing functional programming you see these commonalities and you're like oh this the operations we're using on this are just from this like subset you know or some from some abstraction and we can like identify that and replace our concrete types with a type parameter that maybe has some constraint on it and so that's what we like to do here it's a little bit more complicated than that in this case but not much so we have this new thing called aji kata the generalized katha which adds a you know W which has a comb and add constraint on it and so and so you know hopefully we can do this thing but we actually had to add one other little piece which is sort of a generalization of sequence if you're familiar with the the traverse class but it this this allows it to be a bit broader than requiring the particular types of of traverse so basically now a key caddy you have to pass in some way to swap your functor and your your comonad and so with that's this extra parameter though we now have these types here is like cata is just using identity and ID the histo is using Co free and it passes this distributive function for a Co free and the para morphism does the same thing for distributive function for for tuples and so now we've gotten you know collapsed all these into this one definition so if you provide these you can do it just as an alias basically rather than redefining things and so you know so what we had before and now we've managed to kind of like collapse that vertical right and so now we've like oh we shrunk this like this painful part of our library we now have a more manageable set of things and I only have to like you know reimplementation I changed something so great we've made some progress and that this is just Reese tacks it so this is the same thing as on this slide but makes it fit better so what else can we do well this is where we started getting the category theory stuff a little bit a little bit so previously we just subtracted over some some data type we had right and we we lifted it up to a type parameter and gave it some constraint and we can do that same thing some more in this case we abstract over something that that maybe people aren't familiar as familiar with abstracting over which is functions themselves right so we have this recursive type that uses functions write F of a to a and T to a and we have the coma oh sorry the monadic cly's lee variant which is the same thing with mana adds there and what we'd like to do is abstract over what that arrow is in between everything and a function is just a type like anything else right we often don't think of it that way we think of functions that's kind of more more primitive things but really they're not and so we can lift that function into the type grammar just the same way here right so this just and that's a valid identifier it's just like a long unicode arrow and this is just saying for whatever kind of function like thing we specialize to we define an F of a to a and the t of a with that new abstracted notion of a function and then here's where we specialized it again these are just type aliases right and again this all compiles this is like which actually surprises me that some of the things in this talk compiled so if we specialize it the function one which function one is just the way we can refer to that regular arrow this is part of Scala on the standard library so if we specialize the function one we get back our original recursive type with that katha but if we specialize it with this other thing that is function like but has a mana in it called AK lies li arrow this gives us now a way to to get cata M just by specializing on cly's Li instead of on function and so what this does is it says an arrow from say T to a this arrow actually has an M on it so it ends up being t2m of a if that makes sense so the the mon add context magnetic context is actually part of the arrow not part of the result type and it's just it's just a matter of basically cly's li itself it's not the find as an alias but it could just be an alias over you know say like a to M of B and and it works like this and so you can substitute in that cly's li just as you would use the function one here and you get the thematic variance out and so now we've done that you know we had this and now we can see we have those monadic variants and on the other side these are common attic variants which you know how to get into the details and that stuff but now we can like collapse that whole dimension forward and we have a nice smaller thing right and we're we filled all the generality we had right but because we've moved these things to type parameters we don't except to implement like a billion different things so our libraries getting much more reasonable and much more manageable again and now here here's the original title of talk which talks about duality and so we had that recursive and we talked about an ax which is this kind of you know symmetrical thing right where before we were folding things down and an ax is building things up from things and it turns out there's actually as we talked about before abstracting over these categories right which is those function arrows so there's a special kind of arrow called up or the opposite category which given some category and it's objects right so types and on both sides it returns the opposite of that reversed right so if you if you have function one you have an arrow from A to B and that's the same thing as a arrow B if you did the opposite of function one A to B you now have a function B to a right all it does is switch that that function so now it's saying it's required to receive a function and they that you know has the arguments in the opposite order has the argument result domain and codomain in the opposite order so we can use that and actually define here the dual we can define type echo recursive the opposite operation we can define as a type alias saying like whatever that type it whatever that category is just give me the same thing for the opposite category so now you have to find all those other operations that are like dual to two folds unfolds just through this type alias basically now this introduces one particular problem one of the classic problems in computer science the problem of naming so what what is the animal orphism called when you do this it's called katha which is now what people expect and when you see that in code when someone like has something dot katha and they folds like oh this is folded wait no this is totally not folding anything so this is a problem I haven't solved other than to say like you don't really do type aliases in this case you try to like you know basically extend and rename everything and like give those correct those opposite names but man I spent so much time trying to figure out how do I find names that are both a thing and the opposite of that thing it's a really really hard class of thing to find names for it really keeps me up at night like there's got to be some way to just like you know Coke ad I guess we got it but yeah I don't know you need one name for both exactly yeah flammable and inflammable that's the opposite that's the opposite words that both mean the same thing I need one word that new means two different things yeah and so with with this duality we managed to collapse these these you know two sets of things down and now we've gotten down to just one nice small like okay our libraries getting small again maybe it should just be part of cats who knows and so so the last thing I'm gonna talk about is kind polymorphism this looks totally onion you know wait at Scala provides right like you look at the first one that's our regular quatre that we've been working with abstracted over the category and this one there's like all the shapes of the parameters have all changed right and then this one to the shapes of all the parameters have changed we have like no way to like say these things are the same shape so we do actually thanks to Pascal Votto and and Myles Sabin they have added what's called kind polymorphism where you're basically saying there's some parameter here and I don't care what the shape of it is and the shape of it will be kind of at least constrained not fixed entirely but constrained by how these things are used together like F of a the shape of a has to fit into the shape of F they're like those things have to align and that'll be that'll be verified but you can't just throw arbitrary kinds everywhere and have them not line up but this allows you to abstract over those shapes and so now you can define this one function that actually works for the you know the regular case and this this Mutual recursive case and this type of line case and and other things that have different shapes and so now we've taken this and we've gotten back to a library that is just cata and that's the only thing you need and so this is actually what it looks like when you put it all together it's not as pretty it adds a few extra things but this has all the abstractions all combined into one thing it's a little a little messy but it's it's one function but there are problems with this not to the compiler support is not great yet especially I mean like even using type level there's things that you can't can't really get on and then it breaks type inference like crazy way too many type parameters way too many other things so often in practice you do end up specializing and like giving those other names back but again you just defined them as aliases that have like partially applied to type parameters so you don't have to like redefine the operations again and then a library support like some of this stuff requires different slightly different definitions of things like functors and stuff like that not what you would expect from like cats or Scala Zed and so there's there's differences there there's a compile time cost for resolving all these things and finally you know you look at this and this is not what you showed us some new Scala FP introductory right you're like oh here just implement this thing so there's a cognitive load to like to present anything this way but really in the end all you need is a cat uh this is not my arm I promise but but it is a friend of mine uh Valentin Casas who who literally got tattooed that the only thing is the Cata after after realizing this fact for himself that everything comes down to this so yeah so thank you for listening and thanks to all of these people for for various things and contributions and my slides are available there at the bottom I mean the compiled time costs well with the Scala code bases I've worked with this is not that significant of a compile time cost but I would say for other Scala code bases it might seem a significant file time costs but was the stuff has actually resolved and sorted out of compile time and doesn't affect runtime like kind this kind polymorphism stuff for example just kind of the biggest piece is totally erased during compile time yeah yeah there was a there was that was the kind of the introduction of the I maybe didn't say clearly whoa what did i do there where do we get into here how was after this yeah we're stint reduced categories here the idea was that you could use function one or cly's Li as your note this is so this is actually compiles with with type level Scala on 212 [Applause]