Scale By The Bay 2019 UnConference: Sergei Winitzki, What did category theory do for us?

Scale By The Bay 2019 UnConference: Sergei Winitzki, What did category theory do for us?

Recording: Scale By The Bay 2019 UnConference: Sergei Winitzki, What did category theory do for us?

[Music] my talk is going to be not an introduction to category theory but actually an answer to this question so why would I as a functional programmer ever care about category theory what did what did it do for me what is the advantage that I get out of it is there any advantage or is it just hi talk about it you know I actually write code and then after I write my code somehow I'm talking about it in this language but nobody really cares because I already written my code maybe it's like this then I don't care then I don't I don't want to ever study this but if there are actual advantages to category theory and if I will be a better programmer write better code then I want it so that's what I mean by an extreme pragmatic and uh nakida me approach all right so just a few words about myself I have a degree in physics and I am a previous imprint my previous career on academic I know very well I can hear it right away when something is purely academic with no applications just to make you feel better I I can see that I don't want that I want actual answers to this actual question and to begin I would I would say well what do functional programmers actually do most often what kind of things do they benefit from and there are these things so there are actually five things that they do which makes functional programming a beneficial thing to do for most programs first work with collections using methods that just map filter fold flat map second use what I call disjunctive types so there are types of describe a disjunctive set of values or situations so these are called case classes or algae Gregg datatypes although there's not a lot of algebraic stuff about them but so these are already hugely beneficial if you use them in your code third using type constructors with type parameters and the flexibility that this gives you here I gave an example oops I gave an example of an extremes declaration where you have a flow of Kafka message of my data Kafka message of my result and not used so all these things are type parameters and some of them have further type parameters so the flexibility that this gives you is the extremely useful benefit so you can describe a lot just by this type prevent lots of errors just by having this type forth people use what I call functor blocks so these are the four yield constructions or called sometimes for comprehension so that name doesn't describe anything really so functor blocks are used like this and they make code much easier to read much easier to refactor so they have concrete benefits although there's a little bit of a more advanced feature for beginners but this is a very useful thing and finally curried functions so functions that return functions so powerful feature which is used less often may be in ordinary code but it is used still nevertheless for example in akka streams something like this it has a curried function right there so far we need no category theory a new programmer can learn these features of Scala and become proficient and they don't need to learn any category theory and this is what I believe is true you can know how to use say future in a for yield construction and so on and you don't need to even hear the word monad to do that so where is it that you actually get any benefit from category theory so first use of category theory is that when you start working with type classes that have laws now type constructors with methods such as map filter fold and flat map are not just accidentally having a certain type signature and so on they actually must satisfy certain laws in order to be useful and these laws are for example for the map function identity and composition for the filter function therefore laws for the fold or Traverse functions there are three laws for flat map functions there are three laws actually actually for if there are two natural allottee laws now where did these laws come from and why are they important these laws can be motivated purely from programmers perspective by requirements about what code should one write and how this code should behave so these for example the map law of composition is something that tells you that when you map with one function and then you map with another function is the same as when you map with a composition of the two functions if that were not so you would write code that is wrong but it would be very hard to see why and I give you an example of an incorrect implementation of these type classes so the case class Bad has implementations written right here for map flatmap and filter this compiles this code compiles and once I have this I can write code that's I that I'm showing below with four yield it will compile but this code will not not give you a result you expect for example in the code that I was I'm just showing I expect that the result is the same as the value B because I'm just going over the values and B and Y is equal to X so that it shouldn't should be any any different from what it was before so this I expect to be just equal to a B but it's not as you see it's if you call some method it has a different result now looking at this code I don't see where this has happened where did I replace the value incorrectly so it will be very hard for me to find the bug I this is of course a very artificial example but imagine that there is a custom data type for which you implemented map incorrectly that does not satisfy laws it will be very hard for you to find your bugs because it will mostly work sometimes it will not work it will be not easy to see why and the reason is that you violated laws so these methods that you implemented are not lawful unless you know that unless you know how to check these laws you will not be able to implement your type classes correctly for some custom data types so this is important for library authors but it is also important for application programmers who would like to implement these methods for their custom data so your custom data could be dictated by business logic your product manager dictates it's essentially not you you need to implement the type class correctly so that's where you start looking at these laws no category theory so far but you start looking at something that's a little more more abstract now or what are these laws so in fact is not easy to reason about these laws they're all different but with some work one can transform and simplify these laws into a common pattern which I call lifting so you need to derive mathematically equivalent formulations of these laws so this is some work that let's say take it two months of calculations so every day you do calculations for two months and two months later you end up with this table and not joking by the way you end up with this table so this table formulates the type classes on the left with certain methods which is not this method maybe you thought about but it is equivalent and its type signature is shown on the right in this table so for example for the function type class instead of map you use F map you need to swap arguments in map so that the signature looks like this for the Contra functor you need to do C map which is again you need to swap arguments and it should be like this for the filter you should not look at the filter function you should define a function called that I call lift opt with this type signature but this function is actually equivalent to the filter function which requires you to derive all that and prove for the Monad to use the flat map for the placated functor use app and for comonad you use a co flat map so once you do that you start noticing a lot of similarity between all of these functions so the type signatures are very similar you have some kind of function which is not necessarily a to be some kind of twisted type A to F of be a to option B or B to a or some kind of other thing and that function is mapped into a function f of A to F of B which is again kind of a little twisted but it's always this mapping so first you you start looking at this and you're thinking why is that why are all these things that kind of the same except for these little twistings but it's it's not the end because actually you see the law has also followed the same pattern there are two laws identity and composition always just two laws if you look at this table and you see I'm using as I said specific functions F maps e map lifts opt you need to use them if you use them their laws are just two laws identity and composition in each case there is some kind of composition of this twisted function that again gives you a twisted function and there is some kind of identity function which is also twisted which is then lifted into an identity function now I'm not going through these derivations because that will take two months but I'm giving you the results the result is that you have this heuristic picture of lifting all these laws and all these functions look like liftings you have some kind of types a B that are lifted into F of a F of B and so on and you have functions that have twisted function type and they're lifted into this F of A to F of B so if you look at the type signatures you see how that how that works and if you if you lift identity you get identity if you lift composition you get composition but the composition needs to be defined specially because you see there's no way to compose these two functions directly because the types don't match so there's a twisted composition operation that you need to use however it's always once you define that it's always going to be the same thing so now you're saying I've been writing the same law all over again in these guys what is that law what am i doing and that's what category theory says you're doing so there is an abstract picture of this lifting and this lifting in category theory is a functor between two categories and there's an abstract picture of the twisted function type which is called a morphism so morphisms between a and b are functions with some twisted type for example b2 option of a or F of a to b or something but these are always similar in very important ways in fact the category has laws that there must be an identity morphism and there must be a composition operation and there must be identity and associativity laws for these operations and this is true for every one of those examples the same laws hold for them and then the factor is a description of how to map types and functions or morphisms from one category to another and you see functors have two laws a lot of identity and composition and so that's what we've been doing here all this time so every one of these type signatures is a lifting corresponding to a certain factor in the category theory language which means that once I learned those definitions I need to learn only once this definition of category definition of factor I can just say you know what I don't really remember the laws for applicative functor but i remember this is a lifting from a functor from this category to this category so that's much easier to remember everything else will just follow automatically the laws are the same once I know what what twisting I apply on the left and what twisting I apply on the right that's it I'm done so this is a great economy of thinking so that's what mathematics is very strong at you abstract away details and you find common patterns and you you understand where all this comes from so to speak so here are examples of categories so the plane category is just plain types ABC and so on and functions A to B the F lifted category where the types are wrapped into F and morphisms are also wrapped so F of A to F of B then there is an F class Li category where morphisms have this signature a to F of B so I just remind you we have a two of them here this one and this one of this kind where the twisting is of the of the type a to something of B so then let's call this F closely the identity morphism is the pure method and the composition is this operation that i denote by the diamond which is implemented using flat map so the classic composition has this type signature a to f of b composed with B to F of C gives you a to F of C and if you write down the laws for this composition which means that identity law on the Left identity law on the right and associativity law these three laws are both equivalent to the laws of monads again this is a derivation that should occupy you for some hours but at least it's it's something that you can do F a pricket of category the morphisms so the types are just again ABC but morphisms are wrapped in the factor like this so not not like this as in the Kleiss li but like this and so here the composition is defined differently using the map to operation of applicative factor and the pure is defined differently other than that everything is the same so the difference is in the twisting what the laws are the same so you have this twisted function which is in the category theory language called morphism and you have this twisted composition other than that everything is the same for all these examples there are examples of the same construction contra functors you just reverse the order of the arguments of the function and that's it you have the graph exactly the same law is exactly the same results now the big advantage comes when you start to ask well what can I do to existing monads to get a new monad or what do I do to existing functors to get a new functor and category theory tells you there are general constructions about that and you can just copy from some book and you have assurance that it will work in your code that your laws will be correct because this is proved once and for all in this abstract language of morphisms and objects it will equally apply to functors moon as applicatives and so on filterable contra functor contra filterable whatever you want will be as long as you can find this formulation you know all these results automatically apply so this is a great advantage if what you want is to talk about properties of all type classes at once now how often do you in your programming work need to do that to talk about properties of all type classes at once or you have a function that's parameter I parameterize by an unknown type class I don't think I've seen an example of that but if you wanted to do that that's what category theory is for an example with filterable factors now filterable is the type class that is not often explained it's it's just the filter function everybody knows but there's no type class for it usually and there is no laws that people talk about usually but actually it's it's an omission there is a a very well-defined categorical formulation of a functor from an option Class D category to the F lifted category and then you just check everything works it's not exactly the same thing and because the laws of the filterable functor are not well known you might be unsure that you have guessed them correctly because you first as I said you take your programmers experience and you translate that into your expectations as to what the laws must be you know I have a filter dot filter dot filter what should it be well I expect as a programmer to have this to simplify this code like that for example filter with a predicate that's come that's identically true I expect that to be our identity function because it's a filter that never filters out anything so it should not change my my container that I'm filtering so that's one of the laws but you don't know that you guessed all these laws correctly category theory assures that your laws are consistent useful very general once you make contact with that you have great assurance that your library is correct your your laws are correct and so on category theory also suggests generalizations what you can do more than this so for example here in this construction you see the option plays a prominent role but actually this can be replaced by any other monad and I have something that I call em filterable functor maybe it's useful maybe not but it's a suggestion that you can explore another suggestion why don't I use the opposite category here instead of a to option B I get beta option A in this function or here instead of F of A to F of B F of B to F of a why don't I do that and I explore what happens and I get again something possibly useful so category theory gives you these suggestions it doesn't show which one of them will come out to be useful for you it doesn't show how to derive or prove anything that's your work that's going to be not easy so the second major situations were situation where you want to use category theory is if you make a library that you could call a type constructor library a library that's parameterize by type constructors an example is various libraries that give you a free functor free applicative free monad you can have a free of any of these type constructors type classes that i listed over there free filterable free contra functor you can't have all of that free and that is a function in the library that's parameterize by a type constructor now once you are working with that kind of thing you better understand what your laws are you better understand how to implement this correctly it's not obvious at all these constructions are not easy to just wing you have to understand that you do derive the laws correctly for your implementation and so on that's where category theory helps because all these things are general constructions that follow from some generalized functors in some generalized category so now at least you know where to look the second example is the church encoding of a free monad which is currently known under the name tagless final now his name means nothing there's nothing useful about that name so I would prefer to call it a church encoding of a free monad again church encoding is a general construction that you can look at in arbitrary category and prove its properties and apply as necessary free monad as already said so if you're writing a library for this you better know which laws you need you better know what categories need to be checked for consistency another example is the church encoding of recursive type struktur which will make it non-recursive now this is parameterize by a type constructor and also by recursion scheme so there might be different recursion schemes and you you might have different implementations so I'm not going to go into details here but basically these are examples where I would suggest going into category yes lists for example it's a type constructor whose definition uses itself that's a list is a nil or accounts with the list inside or tree all right a tree has a tree in that so any kind of constructor of that kind is a recursive type constructor now if you're writing a library that works with these type constructors in general parameterize by arbitrary type constructor with arbitrary properties or for all monads or for all applicatives or something like that that's the first sign that you might need to look a little bit at the definitions of functor category try to see if your laws are correct and you chose them correctly that's kind of the first time unless you work with this category theory isn't going to help you much now even if you work with it category theory will not help you derive any of these laws actually for your for your code category theory it doesn't know about your code it's too general category theory talks about properties that are in common between monads functors applicatives filter balls and contra factors what kind of properties can this be certainly not something that's in your code your code is extremely specific to all these things it so category theory cannot possibly know how to talk to talk about your code and so it will not help you deriving or proving these laws you need special techniques if you want to derive or prove that your implementation is correct so in order to teach people how to do this I'm writing a new book which I call a science of functional programming and this book will explain with all kinds of examples and exercises and diagrams and calculations how to do computations how to show this how to derive these laws so I talked about category theory a little bit in this book but it's by no means a book about category theory because like I said unless you're going into such territory that you're working with type constructors that are arbitrary and that have type class laws or something you don't need category theory at all so let me summarize functional programming needs to be learned as such not as a application of category theory that's my main topic that's my main main statement category Theory helps understand where the type class laws come from does not help you derive these laws prove these laws or write code correctly category theory helps you to understand how to write these general type constructor libraries now this is not often that something like this needs to be done in your in your work but if you're doing this yes you need to understand so yet even then a library author gets inspired by category theory but needs to do country symbolic reasoning by hand in order to see that the code is correct category theory won't help there and learning how to do that takes a lot of time so this is part of why I'm writing this book this knowledge is never explained you will not find a tutorial a book an article that tells you why the state monad satisfies its laws I challenge you show me who it writes out this proof nobody I don't even know how to write it so that you don't fall asleep because it's it's very difficult to use color syntax or Haskell syntax or something like this you need special techniques so that's part of what my book is about so right now the entire book is going to be free it's available on this github chapters 1 to 8 are ready and I'm going to continue working in it but so I hope I explained what category theory gives us and what it doesn't give us and where you might want to look into it and where you might want to stay away from thank you questions please category theory helped some awesome alright let's review very interesting things but I see them as patterns right so the same way like oval like object-oriented programming has patterns and I feel like sometimes people use too much better right so you have something that could be just like a straightforward quote and then you have like a como mat and like crazy things like how do you see you like that they may talk like how much you should use of the pattern and how much you should like just right so the question is how much is it reasonable to use these patterns of functional programming monad comonad and so on how much advantage doesn't give right so yeah this is a very good question so I would say it is harder to change code that has been written with a pattern that you don't really need so it will it will bite you eventually because you I would say that right now the community has found certain cases where it is certainly beneficial to use say a for yield which is which not not necessarily very complicated but it's something that once you start using you can't stop using so I think there are certain situations where it has beneficial to use it and people gradually understand that this is good for certain things but if your fur yield is one line maybe it's not so good to use it right maybe if you have a comonad just because you feel like having a comonad you should try to write the code without it and see how much shorter it becomes if it becomes shorter you're not getting gaining anything if your code without the comonad is is easy but with the comonad becomes harder then okay what are you really gaining right so there are certain situations where right now the functional programming community does not yet know when to use these things so right now for instance some people say you should always use Kats effect are you--oh and so on and other people don't do that they just use ordinary effect for non pure code with a bit of monads thrown in right I don't think that it is right now very obvious which doing which patterns to use in which case but in some cases it is clear so some cases very clear for instance if you have a lot of code with error handling right you or you want to make sure that your code writes a transaction to the database of the right places right you should have it in the moniz use a free monad and you guarantee that it will never make a mistake in that kind of that kind so I think it is clear by by now that we have these figured out but there are many other places where it's still experimental so you should not think that somehow this is a silver bullet whenever something comes from category theory should be used always in your code because that's the question still not clear and it will take maybe another decade until we are completely comfortable making that call questions so yeah so the question is tagless final is opposed to free monad when should we use free monad and when should we use toggle is final so tagless final is equivalent to freeman at first of all so you're not gaining anything in functionality you might be gaining in architecture of your code so you can in other words you can rewrite one into the other and back but the code will change it will become maybe less maintainable now if you are just using one DSL and there's nothing nothing else you'll ever use so the one free monad and you never use another one and there's only one interpret interpreter for it you only only do one thing then you don't need to use tag tygris final the church encoding of a free monad first of all it is it is slower it has more code but it gives you a lot of flexibility in how you use the program so if you have a program that is only used once in your course we have this free monad make a program in the free monad and you run it and that's only there's only once in your code there's no advantage in making a flexible encoding that is parameterize by arbitrary output monads which is what Douglas final does so I don't think that would be advantage but if you have a lot of little pieces that could be interpreted in different monads intermediate representations and and so on lot of flexibility that you need yes you might you might do it so in any other case there is no clear-cut recipe here you need to look at your speed cific code and sometimes you refactor the code and you see that it becomes simpler even though you're not using this fancy thing maybe it's okay so I would say most importantly they're equivalent you need to understand that this is just the same thing from the point of view of power of what you're doing it's just that your code is going to be organized differently with a little more flexibility in one place and a little less flexibility in another place so that's what you need to look at there is no there's no recipe sorry how did helps you okay so the question is for question is what does it okay here's that here's this thing because the question is what do we gain by rewriting filter as lift opt with this other type signature so for programming you should never use this function lift opt should always use filter it is pretty much useless to coding with this lift op very inconvenient around about its equivalent though it's completely equivalent but it's inconvenient for actual coding their gain that you get out of lift opt is about understanding the laws only in that you have gain so if you ask what are the laws of the filter function I'm pretty sure nobody will tell you because nobody knows and I can tell you well it's not an easy thing to derive them but if you understand that it's equivalent to lift up lift opt has this very suggestive type signature from which it kind of begs to say Oh on the Left I have a two option B this is a Kleiss Li of option on the right I have F of A to F of B this is just lifted to F I know what the laws must be Oscar thank you so I will just repeat that in in Oscars experience they have use of this function when they validate or are check presence or absence of data - so it's kind of a combination of map and filter in a single function right well true so there in my view in my view most of the time you don't need this but certainly I might I might not have that you don't want some empty monad or bad state exceptions or whatever it is but you you can't do anything with the value that you filtered out such as to recover by using that value or even just as a side effect to say this is why you fail and so in some cases I wanted something so the question is is there some other type class that allows you to filter but continue to see or to have access to the values that you rejected because filter drops these values and you cannot have any access to them yeah I don't know so there are functions like partition were you partitioned by it by a predicate and you have two collections as a result right so you have all all the ones you rejected if you want them so I think you need a monad that gives you pass/fail with an error information and then you can put all that into the error information or you can try to do something else but I don't I don't know offhand what yeah transform into an either and then have some kind of recovery that sometimes recovers an error full either into a known error and so you don't use filter your transform into because filter will drop right so you want something else will transform into and either and then sometimes you can recover that so it's like a pass/fail or you sometimes recover the failure failure in the context of the thing that I threw out not just right well yeah because you can have that value in there in the in the left part of either you can have still whatever you need to maybe say maybe something like this all right well thank you I think we're out of time thank you very much [Applause] you