Scale By The Bay 2021 : Sergei Winitzki, What I Learned about FP when Writing a Book About It
[Music] so uh what i'm going to talk about is this very interesting perspective on functional programming that i developed while writing a book on it so first uh my background um i used to write academic papers with lots of formulas and diagrams that looks like this but um in 2010 i repented and turned to software engineering functional programming attracted my attention around 2008 as far as i remember with programming languages such as ocamo haskell and a bit later scala i was learning from papers books online tutorials and uh especially meetups in san francisco where i worked uh i've been attending this scale by the bay conference since 2014 and i'm using scala at my job since 2015. while i was attending various meetups i found that the f for functional programming community is very much unlike other communities of programmers like java python and so on because those other communities focused on designing and using libraries frameworks and they talk like use let's override this method use this annotation make this config let's call this function and so on so quite uh typical for a program well the functional programming community talks in a very different way they talk like referential transparency and algebraic data types and monoid laws and and and and so on actually uh john the ghost uh has oops should open it so this is not um john the ghost uh made a glossary i'm showing the link here of functional programming terminology with more than 100 terms of this kind and this is not just some graduate students showing off these are programmers they're using these things for programming um from the scale by the bay conference in 2018 one of the talks was called the functive monad talk and this means uh note this title the function replicative monotok it means everyone expects to hear these concepts uh mentioned and so this is a kind of a standard and accepted part of functional programming community that you talk about those things here's an example of an actual scala error message [Music] found one thing and required something else where this type blah blah blah is like gadt's colon now this is quite interesting so why do they talk like this and to do functional programming should i learn all of this like for example catamorphisms else do i have to learn are there dogomorphisms or only catamorphisms and how do i learn about this so these were my questions my main questions were which is the theoretical knowledge because this looks obviously like some math uh some knowledge of mathematics or something like this so which of this knowledge actually will help me write scholar code now it's not like i cannot learn a lot of new things but do i have to i have i have my life you know not so much time i don't want to spend time learning about something that will not help me and where can i learn it what are the books or or tutorials or something where can i find this uh uh the material that will allow me to learn this so the questions that i had for instance i started learning this well what do the monad laws ensure why why are they imposed how do i verify that those laws hold when is a data structure a functor a moon a replica so there is this talk about function mode and implicative but it doesn't answer those questions um i kept reading and those materials gave me more answers than questions and more questions and answers um for instance a lot of materials a lot of books have heuristic implications explanations without derivations and without proofs here's an example a recently published book to the book of moon ads which i looked forward to it's a very good and interesting book but it does not actually prove the moonlight loss for any of the moments it shows you the laws but it never proves them so for instance if you know there is a monad such as a statement or continuation monad or some other such monad but so it shows those monado how to code them but it doesn't prove that they satisfy the laws of the moon and uh and to me this was a first question so is this correct um how do i know that and a few books like for example the haskell wiki books or these books the introduction to programming with haskell and functional programming in scala they show some proofs but only simple ones and that actually creates a false impression that all proofs are simple and to me this is a red flag other papers that i found were far too abstract far too academic pure theory for the sake of theory with no applications in programming and i don't want that i'm not interested in this i've spent a lot of time in my life doing academic theory with no applications so now i would like to have a cut at some point i want to decrease the scope of theory that needs to be learned so here are examples of pure theory with no applications now this is a joke in the functional programming community that monads are just monoids in the category vendor factors what's the problem obviously this phrase doesn't explain anything and there are lots of problems with understanding oneness but this doesn't help you to to understand um and if you understand why this is true so you study enough category theory to understand why this is true this will help you not at all in using one ads in implementing monets for example if you have a data structure in your code that you want to make into a moment will not help you at all to know this thing so this is in my view an example of purely academic knowledge that i would like to avoid or another example this is from [Music] wikipedia any monad comes from an explicit adjunction of some functors well great at some point i thought this was a very important theoretical result that will help me do some something like mona transformers but no actually i went through a lot of calculations and i found zero use of this information so this is this is what uh motivated me to write a book i want to show the correct scope of theory that is necessary that is helpful and i want to avoid theory that is not helpful so the only way to do this is to derive all results from scratch and motivate everything so you have to before you say monad has to satisfy monad laws you have to motivate why these laws are necessary what if you don't satisfy them is your program going to crash or what um you have to show that uh some something like this and another thing i found is that just by chance i found that there is a way to system to organize systematically all this theory all this practice relevant part of functional programming theory it can be organized in a way that is quite systematic and it at the same time it tells you what is not necessary and what is necessary so i will tell you how this is so this book i'm writing is called the science of functional programming uh it talks about theory of applications uh of functional programming in a theoretical way but it is focused on that part of theory which is useful for practice it gives you the techniques for deriving and verifying the properties of code and gives you practical motivations for everything so 12.5 out of 14 chapters of this book are ready i'm working this book in my spare time which means slowly but it's pretty much almost done should be done next year so now the first thing that struck me when i got into functional programming is that in functional programming there are certain questions about code that can be answered rigorously not a matter of opinion but a matter of mathematical derivation and reasoning and these answers are directly helpful when you write the code when you design the types that your application is using that's where those answers help you so this is quite unusual because in other paradigms you don't have like an object-oriented program we don't have this here are examples of questions that are um [Music] uh that have unambiguous answers um suppose you are given a value of type either z of r to a um or you're given the value of type r to either z of a can you compute the other value of another of the other type so a r and z are type parameters or arbitrary unknown types so i can think uh of two functions one the function f that goes from one type to the other and the function g that goes from either of this into this can i implement these functions it turns out that you can implement g and pretty much in only one way so the code of g is like this but f cannot be implemented and it is not because we are not clever enough that we don't know some tricks of scala or functional programming that um we're not uh able to implement f it's because it's mathematically impossible to implement f now this is quite amazing in some sense um how can it be that uh it's mathematically impossible to implement a function with a certain type signature this doesn't happen in other programming paradigms so programmers need to develop intuition about why this is so um the theory behind these results about being able to implement or not is called the curry howard isomorphism and there is the ljt algorithm so-called that allows you to develop code automatically so you can derive or generate code for the function g automatically just from the type signature at the same time this algorithm will tell you that the function f cannot be implemented and that's rigorous second example i want to combine future and either together how do i combine them um well i need to write code like this maybe i have a future even either this of course won't compile so what do i do how do i combine either in future do i combine them like this or i combine them like this and i want to implement flat map for this type so that i can write for yield block it turns out that this is wrong and this is correct this is rigorous programmers need need to develop intuition about why this is so they don't have to test this or prove that themselves but there is a theory behind it which actually proves that this is true and this is a theory of monet transformers and their laws third example suppose you have this data structure can you implement flat map for it it will be this type signature just a standard type signature of flatmap turns out that you can implement this type signature but it will always fail the moon laws whatever you implement you also implement pure for this data type and it will always fail the moon and loss now programmers need to develop intuition about it how do we modify this what is wrong with this type how do you what what else does it need in order to be able to have a moon add an instance uh for example this if you just change the option into an either it's a very small change this becomes a lawful moon add this is not obvious at all i'm not trying to say that this is obvious and finding this requires quite a bit of work but i already have done this work and i have written it all up so you don't have to test this you can look it up in my book and in principle you could study the theory as well it's all explained and derived so the result is that the functional programming paradigm is similar in some ways to engineering and that was another realization that hit me at some point why is it so different it's because it's not like other programming paradigms that are similar to artisanship trades and crafts in artisanship people work according to theory and not a theory to tradition to experience they learn by doing and that's how most programmers learn in functional programming uh there is theory that you can study and this theory gives you rigorous answers to certain questions relevant to your design and this is exactly the situation in engineering some engineering knowledge is based on rigorous science um of course not all some engineering knowledge is not science it is tradition and experience but a lot of it is based on science and in this way you can see uh functional programming is also based on science my book is an attempt to figure out what that science is what is the scope i'm not inventing anything new i'm figuring out what is the scope of these theories that a functional programmer could study in order to answer the questions they have another similarity between engineering and functional programming is that engineers use special terminology just like functional programmers do here are examples uh rank for tensors yeah functional programmers use rank in types i'm not saying that they're similar not similar in any way but this is a kind of special terminology we have fourier transform we have delta function and in functional programming have lambda functions or here you have gibbs free energy i'm showing links where these uh terms are being used in engineering presentations or books and here are where these terms are being used in functional programming presentations or discussions so for example gibbs free energy and they have free monads the word free does not have the usual meaning here it's terminology it is not self-explanatory you have to learn what this means in every case finally it turns out that the main system behind functional programming is the map filter reduce um and if you just look at map filter reduce and if you study that you will be forced into doing all of what i did all of what i was telling you before and more so what does map filter reduce well we know that it is a very powerful method of programming where you write iterations without loops and you generalize from there so you have certain functions that operate on entire data sets and produce new entire data sets at least conceptually and the implementations of these could be very different for example some of them could work with clusters parallel processing or even relational databases and so on the map filter reduce programming style is a success story of functional programming and it forces you to use nameless functions like these uh it forces you to find out what the essential methods are and they are map filter flat map zip and fold the natural question is what are the data types that support these methods these are for example the algae drag data types that you're talking about trees or for example a perfect shape tree that always has to be perfectly balanced like this which methods can i define for this data type can i define like for this data type say let's say this is my business logic can i define map for it filter flat map zip fold it turns out that you can't define some of these methods but not all for certain data types and that gives me a systematic approach to describing and understanding functional programming you determine the required laws of map filter flat maps you can fold these laws express the programmers expectations about what these methods should do so you motivate them you write them down you define the corresponding type classes and then you find all the type constructions of preserved type class laws here are some examples of these type constructions that i'm talking about if p and q are filterable functors then so is either p of a q of h that is also a filterable factor so filterable is something that has a filter function if p of a is a moon adds then either a of p of a is also a moment if p and a and q on a are no nets then the pair is a moment if p of a is a contravariant function then this function type is the moon add if these two are applicative then either p and the pair of a q of a is applicative now it's not just a pair of p and q that's not true it is not necessarily applicative but this does work so i found many more constructions of this sort and sometimes when i found what type constructions are necessary i had to define new type classes such as contravarian functor or contravariant filterable control variant duplicative necessary to find out what are the possible data types that have these properties and that is my system essentially in one slide so this is the systematic approach to determining what is a practically relevant theory this is obviously the practically relevant functional programming style what are its theoretical properties so that i can describe all possible data types that can have those methods this helps me develop intuition about how to implement these methods what data types can and cannot have those methods and how to check how to prove the laws another thing that i realized while doing this is that types play a central role in functional programming as it is practiced today it's not just programming with functions it is not just immutable values and and functions that maybe was 40 years ago when they only had lisp today types play a central role and not just that they are checked at compile time although that's important but that specific types are being used so functional programming today is programming with functions with mapreduce filter and with specific kinds of types and i can list what types those are unit types generics or type parameters product types co-product or disjunctive union function types and recursive types which are defined in scala maybe like this it's not necessarily practical but theoretically for any recursion scheme you have a recursive type so given just these six type constructions i can do pretty much all of functional programming but as practice today i can then enumerate all possible type classes like all possible functions monads applicatives traversables filterables that are made up of these types and typed instructions and in some cases i can automatically generate type class instances for them another little detail is that uh these types correspond to logical propositions uh for example coproduct response to a or b product corresponds to a to b and so on and not all programming languages support these so if a programming language doesn't support say co-products it means that the logic of its types is incomplete and you cannot express certain things in the types and it turns out this is practically relevant it's important that the programming language should support co-products and pattern matching on them um languages that don't support co-products like the go language where they decided not to support co-products will make you suffer they will write codes there will be a lot of boilerplate error-prone and you will not be able to rewrite it or refactor it in any way whereas in scala you would return try or either in order to return error or result and the error here the design error in the programming language is that instead of returning a disjunction they return a conjunction so instead of returning a or b they return a and b it's just a logical mistake in the design of the language don't do this um finally in the little remaining time uh do we have a chat question in this zoom or is it um something that i can go over later um there are no questions uh yet okay i see i see something in the zoom chat okay so um i have five minutes left or four let me uh just go very quickly over little things that i've found the surprises the thing is when you go from scratch and derive everything then you're bound to find things that you didn't expect because science is unforgiving it doesn't know what you expected it has its own logic there are many things that i believed to be true and i tried to prove them and i couldn't because they were incorrect and there were other things that i didn't think were true but turned out to be true so let me just go very quickly over those surprises there are too many of them actually each chapter gave me at least one surprise when i went through it for example there's a perfect shape tree type like this and you can define a type installer where you can only have perfect shape trees the usual tree allows you to have different branches of different places this type does not and you can define it by recursive um algebraic data type which i didn't expect you could but yes you could it's not obvious but you can do this i'll skip other things um a fun thing i found is that type inference exists which is determining type signature from given code but there is also code inference determining code from given type signature i already touched upon it i was able to implement this lgt algorithm as a library in scholar and then i can write code like this i write a type signature and say equals implement and there is a macro here which will find the necessary code and compile it and then i can use it right away and this can do a type signature like this which is artificial and quite complicated not obvious and if the type signature cannot be implemented it tells you another funny thing i found is that when i write proofs i would like to write proofs in a shorter notation not in code and i found that matrices can be used to represent algebraic data types called products so functions from a coproduct to coproducts can be written very well as a matrix and you can write the types as rows and columns rows for types of inputs and columns for type of output and you put functions in there it's a very terse notation it allows you to use matrices for proofs very nice notation where you can use matrix multiplication rules for function composition a very interesting unusual thing that i found but help help save me time filterable functors is a neglected type class not usually described but it's an important one um another thing i found is that um certain data types just cannot be movements well it's not obvious why i don't think anybody really knows a deep reason why anyway but the programmer needs to understand that this is not always possible to have a moon add um bread first traversal of the tree so you can define special version of fold and traverse that do breadth first traversal three type classes so there's free applicative free functor but there is no free foldable or free traversable interesting isn't it but the programmer needs to notice how to define free type classes another funny thing i found tagless final is just the church encoding of the free monad what is the problem no another joke of course church encoding is a pretty difficult thing to prove to that it works correctly so i had to go through quite a lot of work to prove it mona transformers are just pointed and the factors in the category of monads i'll stop here functional programming does have a steep learning curve because it is engineering engineering means you have to learn some theory some science and then you can design much more complicated machinery without science you can design good working machinery but not too complicated that's the whole difference between engineering and partisanship doesn't mean that artisan shape is bad it's just not as powerful at the same time you can benefit already from the simplest techniques like map filter reduce adts for yield and you can stop there you will reap the low hanging fruit my book is free on the web with full source code and it will be hopefully finished next year thank you very much [Music] you