Scale By The Bay 2018 Unconference: Sergei Winitzki

Scale By The Bay 2018 Unconference: Sergei Winitzki

Recording: Scale By The Bay 2018 Unconference: Sergei Winitzki

you all right so this is about how to generate code from type signatures of functions and I actually will just it is a presentation that I've given before I will just show the library that I implemented and explain how it works and so I'm just going to load a dependency let me see I've done this presentation okay so I'm just importing this library and the necessary symbols and then I'm going to start by implementing a function with a type signature that is reasonably easy I mean let me just do that ah okay just for convenience okay so imagine you have a function that has two type parameters and it has the type signature that looks like this okay so how would you write code for this function well you are supposed to return a pair of a and a types so and it's a type parameter so how can you get the value of that type well you can't really unless you have it already and we only have one here which is X so the only way to implement this type signature is to return a pair of X and X so why do I need to do this if there's only one wait of implementing this type signature I just do this and a Scala macro called implement examines my type signature and expands into the Scala code that I want to store let me test this so f is a polymorphic function alright so I'm going to test it so I'm giving it two arguments and I can interchange these arguments and so that's the code we expect let me give you another example I'm I can define functions in many different ways type signatures can be written in different ways so for example I can write a type signature like this as well as a curried function and again in this case there's only one way that you can write this code you must ignore the second argument it's the same as the first one you must ignore the second argument and you must return the first argument so this should work as well you see if the type is correct so yeah so basically it replaces the need of writing code that is uniquely following from the type signature let me give you another example which is in my slide here which is this so you're familiar with the reader moment so this type signature is basically the map function for the reader moment I'm just close whatever so it can implement this but if I try to define if a function that has a type signature that cannot be implemented such as this one and this cannot be implemented because basically I screwed up with types and I'm I thought I was defining map for the reader munna but I used the wrong type parameter I'm trying to map on the contravariant type parameter and that doesn't work and so you cannot actually generate code for this function because in order to generate an A you need to call this function on an e and you don't get an e anywhere so if I try to do this EI e f f/a then it's an error and it's a compile-time error and it tells me that the type cannot be implemented another example where there's an error let me call this whatever x2 it's not going to be defined so it's not going to work anyway so this in this case it can be implemented but there are two different ways of implementing it I can return X or I can return Y and there is no obvious way of choosing one over the other so they're both equally good somehow so if I do that it tells me this type can be implemented at two different ways in like this and like this and there's no so in fact this library tries to be more intelligent and it tries to assign scores to different implementations the score as you see here is a tuple of numbers and it doesn't matter what these numbers are but this score is actually penalty for for for losing information and that's a heuristic that the library uses so the idea is that you can you can have different deployment ations so let me let me show you a case when this works well okay so a case where it works well is if you have an option of a and you want to map it over to B and you want to get an option of B oops what's oh I forgot the type parameter sorry about that so so this works okay so I can I can generate the code for a map function for option let me check that it's works actually let me see some 1 2 3 and X going to X plus 1 and see what happens here some 1 2 4 so that's what you expect right but actually this function could have been implemented by simply always returning none and the type would be correct there's no no question the type is correct but this is not what we expected to do and actually the such a function will be kind of useless so the library is trying to figure out which implementation is useful and the score the science is the information loss score so the heuristic is that if you implement this function by always returning none then you're discarding all the information in the arguments you're not using the arguments at all and another implementation uses both arguments and that's better that's the heuristic it's better not to discard arguments and the number of arguments that you have discarded is a penalty which you have seen here in the score equal to 1 0 0 0 0 so this one is one argument that you have discarded in this implementation now sometimes you cannot but discard arguments you can't help it but that's fine because it's just a score and you choose this best score and that's your implementation so another example of when when this works kind of the well that kind of the way you expect is let me define some function [Music] where X is a tuple a a and you return to pull a a so what does it do oh it's identity function but why doesn't it interchange them that would be another implementation of the same type because there's a penalty on losing the order in which you had the two pool elements and that's another heuristic of course but so there are some heuristics like this so you don't want to lose information that you're given I will give you another example where this works so this function can be implemented in infinitely many different ways yeah you can you can ignore F and just return X or you can apply F to X or you can apply it twice to X right now again heuristics here do not allow you to ignore arguments because you have another implementation that doesn't ignore arguments but it does not look at the implementations that apply the same function many times for no particular reason if you don't have to apply that function so this this implementation is basically applying F to X so that's the kind of thing that it can do it can also do it supports case classes it supports all kinds of type signatures and it also supports specific types like int and string but it treats them as opaque type parameters it doesn't know anything about int it won't try to guess for you what you want so the question is is it is it does it have access to other values available in the scope that is not easy to do in macros so the only thing it knows is that if you're defining a class method and a class has some things in its constructor it can see those things and it also can see other class methods that you defined previously not the ones that you defined later but the ones that you defined before you can use those so yeah so that's that's how it works yes yeah so the question the question is if I had the mono it would it know that it can combine things from a mono ed and use operations No so that kind of thing I believe is beyond the scope of what should be done using this mechanism because once you start doing those computations there those are not specified in the type so there are many different ways that you can do things with mono words once you have a mono it first of all you can always return its empty element and there's no type information that prevents you from doing that well you might have these heuristics that tell you that you are not using some information but then there are too many options and also it doesn't know about monoids doesn't know about any type classes it doesn't know anything it just looks at plane types because there is no theory that tells you how to derive implementations from types for some kind of general type classes so now I'd like to talk about theory behind this very briefly what is the algorithm so yeah this is this is another another API there are several API so this API is an expression like API is not a function definition IP I but it is an expression so of type and then a type parameter and then arguments it's an expression that only it returns a result so there's no type signature except you have to give it here so on the left there is no type signature so it's not a method so basically you say given these things can I get a value of type result so here's an example I'm given a string ABC I'm given a function from string boolean to int and I'm given a true can I get a value of type result which is a case class having an integer and the string inside you can because you have a string and an integer you can get from a string and a boolean and you have also a boolean so all you need to do is you put F apply to this ABC and to true you get an int you put it this end here and you could put the ABC here and then you construct the case class and that is again derive Abel from types and so that's kind of a expression oriented API that you can also use if you have a bunch of values and you think you can just combine them somehow you know to put all the type classes maybe you know option whatever you don't care then it is going to do this and again if there is more than one implementation it will be a compile time error to do that sorry it will it will rank them it's the same it's the same idea sorry I I yes I should have said that yes so it will again try to rank them but if there's even besides ranking if there's still ambiguity then it will be an error now there there are other things that I tried to do here I wanted to actually reason about lambda terms here but let me let me go through first let me go through through the algorithm of these are other examples let me go through the through the theory behind it so there's the curry Howard correspondence which is that propositions are types and proofs are programs and the correspondence looks like this basically that if you have some proposition in logic where you have say for all a from a follows true or something like this then there are corresponds to it a type signature of a function or some type signature where instead of true you have the unit type instead of entailment implication you have a function type instead of disjunction you have the either type and instead of conjunction you have the tuple type so let me see if I have this in a previous slide are you familiar with the Curie Howard correspondence okay so maybe I don't have to explain this you know so anyway so here's what the library does you give it a type signature like this on the right hand side it's a macro this macro can read the type that is inferred for it by the compiler the type is this entire type signature 3 type parameters survival flexion the macro can introspect on the type and come up with a syntax tree for the type expression which will have these type parameters and then there will be this this and this so then it will be some kind of type expression containing function types products and Co products and type parameters and ground types like integers string and so on so this is the first step so you have this type type expression as a syntax tree then it's translated mechanically into the logic expression where you for every ground type and for every type parameter you introduce a new proposition variable and then function types become implications products become conjunction and co-products become disjunctions then you have a logical expression and then and then you add these quantifiers for all type variables so so then you have a theorem like this out of out of this kind of type signature the next step is to run a proof search for this theorem so there is a formalism and an algorithm for finding possible proofs and this is the intuitionistic logic so this algorithm is this intuitionistic propositional logic prover which I'll also see if I have if I have a pointer to the paper I'm not sure I have it here anyway and there's there's one particular algorithm that everybody's using which is called ljt and it took a very long time for mathematicians to come up with that so I'm not trying it would be kind of hopeless to try to invent it again so this is a set of rules for inference such that they generate a finite search space for you to go through so this is can you read this notation or is or not so well so okay so gamma is a context which is any number of other things assumptions so at the top there are assumptions at the bottom there is what you get derived from them so these are derivation so at the top there are two assumptions here and the bottom is what you derive from these assumptions which means that if you're looking for a proof of something and you look at the bottom is any of these rules such that the bottom looks like what you have and if so then you need to prove these things of talk first and then you can prove the thing at the bottom and then you look at these things at top and that may be more than one thing that you have to prove now so they have then more things to search for it and that's a kind of a tree or maybe just one thing that you now have to search for so then it generated this tree of post of things that you have to prove until and but every time they're getting simpler because you're kind of everything on on top is always simpler than what's on the bottom so every there may be more assumptions more things that you need to prove but each one of them is shorter and finally you would have very short things to prove like prove a and I have a and as you can do so once you get there you go back and you actually assemble all these proofs into one giant proof and then the next step or I'm going to skip this and the next step is to generate code from the proof so here's how it works each rule let me just go back here so for example this is the this is a rule if you want to prove a or B then you have to prove a sorry you have to prove from a of B from A or B follows C that's what your on the proof then you have to prove that from a fallacy and you have to prove that from be fallacy but suppose you prove that these two how would you get a proof of this well a proof of this is an expression of type a to see a function a to see because this symbol is basically this plays the same role as function function arrow because it's on the left of this symbol our assumptions and the right of this symbol are things that we prove from those assumptions and so you have a function from A to C and you have a function from B to C how can you make a function from either a B to C well that's a case expression you match on either a B and if you have an A then you use that first function that you already have to get a C or use the second one now the case expression is a specific piece of code that you have to insert at this place and in the case expression you also insert the proofs that you had before which are previous pieces of code that you assembled so in this way you assemble a lambda terms these by piece as you go from the proof to the code and so finally each rule of this calculus or whatever each rule corresponds to a specific construction of the code of the lambda calculus so this is a this is a case expression this is a function application because we have a function from from A to B follows C and then from A to B follows a from be full of C so you have an A and you put that a into there you get you get a B and you finally get a C so it's a functional application that's lambda abstraction that's a projection of a to pole and so on so basically you have little pieces of code that you assemble as you found the proof you can then build up this code that corresponds to it and by definition what happens is that the type of this code expression will be the same as the logic of formula that you proved because the whole point here is that the proof means that you can write code of this type because that's what the Curie Howard proposition is to each type there corresponds a proposition that you can write an expression of this type and that is a proof that you can you're writing it so my library then assembles this lambda term piece by piece simplifies it so it gets something like this and then so here's an example this is the formula that I want to implement this is the type that I want to implement and this is the lambda term that has this type and then I transformed it back into Scala code from pure lambda calculus which is again it's just a mechanical step but I have to put in all these syntax and constructors and you know case classes and case objects and so on and so all this is not present in the lambda calculus and it has extra it has to be put in so that's the last step and finally for each proof that I find I have also a score because I have symbolic information about the code and I can see how many arguments I'm dropping or there are other heuristics like do I generate every possible case class from a sealed trait or only some of them and something like that so because if I don't generate some seal some case classes from a sealed trade that's then I'm maybe not using all the information I had right because I had some information now I'm supposed to generate one of these case classes and I always generate one of them maybe another implementation generates all of them and that's better that's all heuristic but anyway so big I can do this because I have symbolic information about the Kroll it's not it's not compiled yet it's a syntax tree still so I can walk it and analyze it in all kinds of ways before I put it back and let it be compiled so that's how it works so finally I have a list of possible implementations ranked by the score and I see if there is just one with the top score or more than one and then I make a decision or maybe there are none maybe there is no implementation and then I make a decision and that's all happening at compile time so all right so that's basically all I have oh yeah here are these articles so are these papers that explain how how this algorithm works and this is the only paper that makes sense to anyone really this is another useful paper that basically explains a little more about how to implement this but again these people don't necessarily they they don't explain everything very well so it's but anyway so that's that's what it is this algorithm allows you to generate oh yeah that's what I wanted to say this algorithm allows you to generate code from type signatures as long as the type signatures are built up from these three constructions product code product and function there is no notion of recursion we cannot generate recursive code there is no notion of type class you cannot generate functor code or monad or anything like this you cannot say oh this is a monad therefore I can use flat map or something there's no such no such thing there is no way to even encode that you know because it's not prepositional it's higher order type you know it's a it's a type class on a type constructor so it's not just a specific type that has specific operations because you could you could have included these as your values from which you build but those values are not just values for amana these are actually type constructors the flat map has type parameters itself and there's no algorithm that can solve those problems so there are these limitations certainly another thing that I have implemented is reasoning with lambda terms with one of the calculus directly because what I wanted is to generate type classes that obey the laws so for example option we just saw I can generate map for option so I can try to generate flat map for option as well it works but how do I know it's correct so that I had some heuristics that's very nice but what if it's wrong despite the heuristics maybe the heuristics didn't work correctly in this case I want to choose the correct implementation I want to check that this implementation is correct so if M oh that is ads not going to work like this oh let me try something else option a a option B let's let me do it like this so I implemented something called lambda term and this is basically a utility so so this fm1 actually it looks like a function but actually it is a subclass of function secretly that has this lambda term property so actually I put the symbolic lambda term right there next to the compiled function code and then I can reason about it at runtime but symbolically and so I can print it and and the lambda term itself is a bunch of case classes let me try to tell you I'll show you what it is yeah this is a bunch of case classes which represent the lambda calculus these are string representations of varying prettiness that you can use for debugging and basically you can write code that will symbolically verify the laws of a monad for this code so if you don't think that this code is necessarily correct then you can write symbolic verification of the of the Monad laws so because it's because all the code you you have it symbolically it is not just compiled it is compiled for you to use so it's fully compiled and and fast and all that but it's a class that has an extra value in it which is this case classes representation of the lambda term and you can it's a tree that you can reason about so that was my that's that's the extent of what I have done and that's that's it so we're out of time okay so the question is did I try to use kilometer to generate scour source code no I don't know enough about that and I don't know enough about how I could do something with kilometer I'm generating Scala code in the macro in a usual way using quotes and I don't know what else I can do and why are we do use kilometer right right well if you're interested let's work on it I don't know much about how to do this but it will be very nice to have an IDE plugin that could do this yes well so they have an algorithm that's very similar to this one and I believe with similar limitations unfortunately I don't think there's an algorithm that will do what you want in a lot of cases also the proofs space is very large sometimes and it's it's it's it's a very slow algorithm because it goes through all possible proofs because it wants to find the best implementation so it doesn't just take one and stop if you just want one it can cut or cut all kinds of corners but if if you want to find the best implementation maybe I don't know what interest does I think it is just finds up to the next type hole or something and yes right yeah so the question is can i paralyze the proof with chemists oh I can probably but I didn't want to do it at this stage because for all its right now it's kind of a proof-of-concept thing also it's a macro it runs at compile time so I could certainly make multi-threaded search and it actually makes sense it's a search tree and chemists can very easily express that kind of thing it's a parallel tree that does something and then comes back I didn't I didn't do that yet and I will I'll think about where this is this entire thing is going before you know sometimes the the IntelliJ is just completely stuck trying to do this and Scala compiler is doing a lot of work at compile time here yes it could be parallelized sometimes it would be good actually I win but yeah so chemist chemist is very easy to use for a computation like this where we have a tree however well I I didn't have enough time to do that yet the fork/join is certainly about ten lines or sorry on the entire for during yeah implementation just the functions that you do in forking and joining of course can be very large but the parallel logic itself is quite small right well you could certainly try to so the question is well interests knows about the standard library and offers you implementations that are in the standard library yes so it risk maybe does this for various reasons I didn't try to do this kind of search based on type know you have a type is there something in a standard library with this type I didn't try to do this actually my next step was to reason about the laws and to generate type classes that automatically satisfy the laws so that you you say you know how in cats you say a new functor and then you have to write the stuff I want to say equals implement you know new new functor new monad whatever type class can be generated I don't want to write all that boilerplate macro can read this it can know about cats and can the understand that you're trying to derive a type class instance and that all can be derived automatically in many many cases automatic derivation of type class is way easier than this because there is no search tree in most cases in some cases there is but it's very short it's not exponential so in some cases you have to search through certain things but nowhere as complicated as this search tree but you know I can I can just make it die very easily and if I you know I I just derived for you the flat map for option right if I put some complicated type here like this okay good it's it found that it's a problem but if I make it if I make it a a C and so on if I try to just to make it a complicated type which is conceptually as simple as this but it just got more option inside more tuples inside and so on this exponentially blows up the search space and since it has no idea what I'm trying to get it doesn't know that what flat map means so it doesn't know oh you're just doing flat map for this complicated thing let me do it in one second he doesn't know that so it will just mechanically go through all possible implementations there could be a lot of them that sometimes ignore some part of the option and they are going to be higher there will be discarded so none of that and then it's just going to go out of memory anyway I think we're out of time so thank you very much yeah thank you