Scale By The Bay 2019 Unconference: Sergei Winitzki, Reasoning about types and code
Recording: Scale By The Bay 2019 Unconference: Sergei Winitzki, Reasoning about types and code
[Music] thank you so I'm going to talk very briefly about reasoning about type of types in code which is based on a book I'm writing right now and the main goal of the book is to describe what are the pieces of theoretical knowledge that functional programmers need in order to be able to reason about their code reasoning about code is something that we often hear a programmer is supposed to be reasoning about code but what does it actually mean everybody is reasoning about everything so I would like to describe that functional programmers have specific ways of reasoning that are not available to other programmers and these are very specific techniques that functional programmers can learn or should learn maybe in order to be effective and these are specific kinds of reasoning about types and about code and examples of this reasoning are that a programmer can design a data type or derive equivalence between types in order to simplify a given data type into an equivalent another type or programmers can use type constructions for instance type product and Co product and so on in order to create data types that have properties they they need and as for reasoning about code the main example of this reasoning is finding whether code satisfies certain laws for instance laws of a monad need to be verified the programmer needs to implement a certain type class that with functions that satisfy these laws and in order to check that they do the programmer performs specific kinds of mathematical reasoning or the programmer checks that certain functions are equivalent they compute the same thing and so you can even derive sometimes a simpler code that is equivalent and very importantly this reasoning is completely mathematical it is rigorous and it is not just some trial and error these are actual mathematical proofs that can be made quite rigorous the amount of mathematical knowledge that you need to be able to do these things is quite limited and certainly not at graduate level at most at the beginner and undergraduate level or even high school mathematics for instance it is similar in complexity to manipulating polynomials symbolically or multiplying say elements in a monoid which are not commutative but it's a very simple kind of calculation now this is my proposed book but I am writing I have eight chapters by now we just had a very interesting talk about how not to pitch your book so I don't so I I did take notes from that talk and I can do everything wrong about pitching this book I don't know who is the manager for the functional programming Theory division at O'Reilly there is no analog for this book its unique there is nothing in on the market that's similar in any way I'm I am completely settled on the title there's no discussion about the title but at the same time I have no data to show that the publisher will benefit and the audience for the book probably is very small and I'm going to have over 700 pages so I basically crossed all the don'ts in the in pitching this book this book will explain what are the techniques of reasoning that are available I will also derive everything symbolically I will derive the laws and I will give motivations for these laws that start from real-life programmer questions about code so my motivation is not coming from theory it comes from code this is the main approach that I am taking with this book so here are examples of reasoning tasks that programmers might need to do given a value of type either of Z and R to a or are to either za can we compute the value of the other type so here are two functions F and G with these type signatures can you implement these functions it turns out that you cannot implement the function f but you can implement the function G so the function f for some reason cannot be implemented but the function G can so here's the code for G the code is very simple so why can't you write something simple also for F it is not obvious that F cannot be implemented you need to reason about it and the reasoning is the example an example of what you need to do I'm not going to go through it right now but the technique of reasoning that will explain to you why F cannot be implemented but G can or the intuition behind it as an engineer you don't necessarily have to derive from first principles from axioms but you need to understand what is correct and have intuition about it another example is that I am writing code where I have a future and I have an either at the same time I'd like to have them at the same time and actually cannot this is not going to compile in Scala because the for yield block cannot have different types if they are not subtypes of the same type but I would like to combine them so how would I combine them and if I don't combine them my code is going to be ugly and actually this kind of situation happens frequently and the programmer needs to know that you can combine like maybe like this or like this the programmer needs to know that only one of them is correct this less way is correct to combine these two types but this one is not correct so why is it not correct so this again is a mathematical statement that can be proved rigorously and the reason is that you cannot implement flatmap correctly for this type but you can implement flatmap for this type proving that you can or cannot implement flat map with the correct laws is an example of the mathematical proof that a programmer at least should have seen at some point if not able to do all the time not necessary to do all the time but the programmer should recognize that this situation has a mathematical reason to exist and so that this is the right solution and it's not just an opinion that it's the right solution it's actually a proof that you can do another example is for instance I can imagine a business logic that tells me my data type must be like this and I would like to implement flatmap for this can I do that the answer is no you cannot implement flatmap for this type in fact you can implement the type signature but it will fail the laws you need to understand that this is not trivial not obvious and again this is an example of reasoning that you can do as a functional programmer let me skip a little and go through some notations that I have developed for from my from my book it turns out that you need to do a lot of computation symbolically with types and with code it is very long and difficult to do these computations if you use the syntax of your programming language it will be very hard to understand where the proof is going and so what we do is we develop special notation that is shorter and this in this table I show the notation for types the tuple for instance is denoted as a product and either as denoted as a sum and the unit type or is denoted like this and type constructors with type parameters are denoted in this way where type parameters are superscripts so then for example this scholar code corresponds to this notation so PA is the type constructor with type parameter a and a superscript is used for type parameters and this is a sign which means equals by definition and this is then the unit part of the option and the product of three A's and similarly a function with the type parameter would be denoted like this for example and this seems to be a convenient notation because you can then show equivalence of types examples I'm showing below where this type is equivalent to this type and this is very similar to polynomials in school algebra equivalents use with function types are not similar to algebra in this notation but sometimes people use exponential notation for this but I found it to be extremely inconvenient in calculate in calculations because you have all the ways a lot of arrows that are nested and exponential notations become very very difficult to use so you need to get used to this notation and I have a similar notation for code in order to reason about properties of functions so for example composition of functions I do not like this where the semicolon symbol denotes the forward composition which is in Scala is like this my favorite composition has small advantages over the backward composition that is usually denoted by the dot one advantage is that it's easier to check types if you type the first function a to be and the second B to C then it's obvious what this compass is doing and it turns out to be also very convenient to use the pipe symbol or this triangle in some languages you actually have the triangle operator for this in Scala it is pipe which substitutes arguments into functions that are on the right so it turns out that a lot of Skylar code looks like this X dot something dot something dot something dot map dot flat map dot filter and these are functions into which you substitute an argument from the left and so reasoning about these functions using this triangle notation turns out to be extremely convenient and also very well adapted to reasoning with the forward composition so people who are familiar with this kind of reasoning have usually seen it in the backward composition without the triangle operator turns out that it's equivalent but it's a little easier to follow so I have these notations and with these notations I would like to show you very quickly examples of what can be done through reasoning now in my book I will explain this in full detail but here I will just zoom very quickly through the results so the free monad has become popular in the scholar community around 2015 and however it was not very clear so people tried to give talks about it to explain to each other what it was and so if you take one of these talks from Gabriel Gonzalez which was in Haskell and he translated it into Scala and you get this code for the free monad and then the talk by rune RB Arneson two years later was in Scala and it showed this code and then two years later still a talk by Kelley Robbins showed this code and they all were talking about the same free monad so then a programmer asks are these definitions different or are these definitions equivalent and how to reason about them what is that that I should use should I use this code or this code or that code reasoning about this is not easy if you use the syntax of the language so the first thing I do is I rewrite these in the type notation so for example the definition and the first talk looks like this and the definition and second talk looks like this now you see there's an existential quantifier in the second definition but it wasn't in the first definition certainly it's not easy to see from the code that you are actually using an existentially quantified type the type parameter a in this code has a very different role from the type parameter T because the trait you're extending does not contain the type parameter a and so in order to create a value of this case class you have to choose the type a somehow so this creates an existentially quantified type but this is not easy to see immediately from the code and reasoning about this is not easy unless you write it in a notation that makes it very clear that you're using an existential quantifier and so with this you're right another formula instead of three case classes I have three parts of the sum so to speak and then I can reason about them and show that they're equivalent so the definitions one and two I'm just going to go very quickly through this can be shown to be equivalent if the type constructor f is a function and to do that you need a property which is called a uni de identity and you neither identity is this property which is for any function f now this you need to show that this is true this is not obvious but this can be shown using code that you can write functions that transform one to the other and they're inverses of each other in in other words you cannot see that these functions will ever give you different results so this you learn as part of studying the theory of functional programming so this is of course an advanced example but it is an example of the specific kind of reasoning that is available when you use functional programming and it is not available for other paradigms of programming and definitions two and three are equivalent if you use Monad laws now this I'm not going to explain all steps in this derivation but this is how much you have to write and you would write that on paper and reason about it as you write to show that these definitions are equivalent you take the first definition you transform it and eventually you arrive at the second definition so this is about as complicated as dealing with some polynomials expanding the brackets rearranging the sums and the products so this level of complexity is about the same as in the school level algebra now I would like to conclude with a more advanced example where I will go very quickly and not at all explain how this was derived and the example is the so called selection monad now this is not a very well known monad but there was a paper that tried to derive the transformer for the selection monad like this and the author of the paper writes that they tried to prove that this transformer satisfies the laws of the monad but they could not prove it neither with a computer program nor by hand and the proof was too hard I am guessing because they tried to do this proof by Haskell syntax and that is not good enough to have proofs of such complexity you write down a program in a Haskell cindex you have no idea how to inform it because the notation does not help you so I developed code notation that specifically helps me to understand where these proofs are going and how to find them Computers don't help you hear so much a formally verified proof usually requires you to know in advance how to do the proof by hand automatic tools cannot find a proof for this because this statement depends on an arbitrary monad M about which you know nothing except that it satisfies the Monad laws and usually computer programs cannot find proofs in such a general way so in the code notation that I developed the proof only takes five lines of calculations and I'm going to show you these five lines this is a definition of the Chrysler product in the new monad and these are the five lines now these lines might appear to be long but they're straightforward we're just writing out an expression you're substituting into it a little simplification and you're done so this line and this line are equal symbol by symbol and this shows the associativity law for the new monad this is the associativity law that the author of that paper was not able to derive either by computer program or by hand I believe because they don't they haven't spent time to develop and with notation that helps to see where the proof might go this is in my view the techniques that are advanced but quite possible for functional programmers to master maybe about some months of learning but once you have gone through this you will be much more effective in all kinds of reasoning tasks so in my book I have everything online the entire source code of the book it is distributed under the GNU license so free to download in the sense of the free software foundation please take a look and let me know what you think thank you all right any questions alright there are no questions thank you again you