Scale By The Bay 2021 : James Douglas, Single Serving Values with Linear Types in Scala

Scale By The Bay 2021 : James Douglas, Single Serving Values with Linear Types in Scala

Recording: Scale By The Bay 2021 : James Douglas, Single Serving Values with Linear Types in Scala

[Music] all right thanks eric uh i think i might have rearranged my title uh since you last saw it uh but it's still the same talk uh so yeah like you said uh this is a talk about linear types specifically in scala and the uh the angle that i'm approaching this from is uh finding a way that this can be kind of practical in a work situation so hopefully that's the message that we get across but uh but we'll give it a try uh cool so um before we get started i want to briefly introduce um the concept of linear types what they are and what they're all about uh and then we'll get into uh really get into the meat of it later um so so basically this is sort of the key takeaway framing this whole talk is that linear types ensure that values are used exactly once and and really that's it and so this can help us write code that is more understandable and has fewer bugs as we'll see we'll leave it there for now and get into it in a little bit but first i want to talk just about types in general so again the premise of this talk is that is linear types but really types in general and the types are good because types are restrictive uh so we have this this minsky quote that i really like that types make illegal states unrepresentable so things that we don't want to be able to put into code we use types to uh restrict ourselves from doing so for today for this talk the plan is to extend scala's type system just a little bit to make it a little bit more restrictive we don't want to make it too restrictive we can we can really go overboard there uh until we end up with a theorem prover if we go all the way uh and those aren't too practical it's a little hard to write production code uh in in something like that um so we'll just make a few new uh additional illegal states unrepresentable in scala uh before we do that though i want to take a quick tour of types and uh specifically look at what increasingly strong types can really do for us so we'll look at a function signature uh with no types with the types that most of us are used to i call them normal types here um generic types higher kind of types and then finally we'll start getting into linear types as an incremental evolution uh from from there and oh and actually sorry one thing that i forgot to mention uh this will be there will be some interactivity later um but i highly encourage questions and um if you want to interrupt me please do um it's welcome um i think eric will let me know if there are any questions uh on any of the um stream or discord or uh or any other uh sources uh that he's monitoring so yeah please keep those coming i'm happy to address them as we go because we're going to be looking at a lot of code um and hopefully not too quickly so uh let's start with uh our little progression of types uh in javascript so with no static types at all such as in javascript we know very little about code by just looking at a function signature so in this example we have a function foo it's got a couple of arguments and we can't see its implementation um so we know almost nothing about this just from looking at the signature we know that foo is a function and well that's about it it looks like it takes a couple arguments but because this is javascript that's not necessarily the case the body of this function could could use undeclared arguments because in javascript you have access to an array of of all available arguments um whether or not they were passed um so we don't know if sorry interrupt so quick question for you so um are linear types like your invention or what's what's their background in history yeah good question no no they're definitely not my invention um they are a uh they're just a theory from uh from type theory or they're i guess a topic from type theory uh that you can find in some other languages like haskell has a proposal called linear haskell that introduces um this incremental um type system improvement um really they they go back to um the different kinds of type systems that do exist and there are lots of different ones and i have no expert on them but the the type system that most of us are used to that we just consider normal uh is actually called uh an afine type system and the linear type system is similar uh but it has different rules about how many times different values can be consumed so um so this talk is is basically taking that idea uh which is very much not mine and introducing it into scala which today does not have support for linear types all right so going back to this javascript code we said we know that this is a function and that's pretty much all we know we don't know if foo takes any arguments looks like it does but it might ignore them we don't know the types of those arguments are they strings or numbers or something else we don't know what foo returns if anything or what its type is so the surface area for testing this function is enormous without knowing more about the implementation and then for for normal types or sort of plain old types if if we just add some type annotations to this function uh so now our arguments x and y are both integers and our return type for foo is also an integer um now we know a few more things about foo we know that it's a function and we know that it takes two arguments this is now scala so it definitely takes exactly two arguments those arguments are both numbers and who returns a number is its result that's about all we know we don't know what if anything foo does with those arguments it could do some math on them and return the result or it could just return whatever number it feels like and ignore the arguments or something in between and we really don't know if we make foo generic uh in the type of both its arguments and the return value uh now we're starting to know quite a lot more about what foo could possibly be um so we see that it foo takes two arguments uh just as before they're both type a and type a is unknown uh at least to the author of foo so if i'm writing foo and this is the type um i really have no information about what x and y are uh because i don't know what a will be at the time that it's used and similarly the the return type is also this unknown type a uh but that but that that uh that unknown kind of buys us something interesting and that's that for food to produce an a for any arbitrary a we don't know how to conjure up an a other than throwing an exception or returning null without using either x or y so with this signature we can infer that foo probably just returns x or returns y or you know throws some exception or something like that um but we don't know which which of these two arguments foo actually returns uh so let's go one step further and use a higher kind of type so now if we constrain a which is our type variable to have a monod instance then we know that well foo has access to a monoid for a whatever a might be x and y are both a just as before who returns in a just as before so now we know that just like before phu could return x or could return y but since a has a monoid foo could do some monoidal concatenation of x and y or y and x or x and x or something like that so the um the intent behind foo is starting to become more clear we don't know for sure that it it does some kind of concatenation of x and y although it probably does because why else would the uh the implicit be there and so let's go one further step and now we're going to be in linear types so as i said before linear types ensure that values are used exactly once and so if we constrain foo's arguments to be linear and the way we do that is with this marker interface which comes from a project called linear scala which we'll go over briefly so if we annotate the argument types with this marker interface we're saying that x and y are both a but they are linear meaning x and y both have to be consumed exactly one time in the body of the function foo so that tells us that food definitely uses both arguments if who just returned x then we couldn't say y is linear because y was never used and vice versa so if we use both arguments exactly once uh a has a monoid so really there's only uh a couple of possible implementations of this function and that is to use monoi to concatenate x with y or y with x and return that so from this progression from node types all the way to linear types the point is that types types restrict what our code might be able to do and they increase the space of what our code cannot do and that really gives the reader a lot of information increasingly more information as our types get more and more strong and the reader in this case can be a person it could be a developer maintaining this code or it can be a compiler as we'll see today and and gives that reader just additional information about their code okay so let's go back to what linear types are so i've said it a couple of times and i want to keep drilling this point that um for our purposes linear types ensure that values are used exactly once um but what what does used mean what do i you know in this context uh what are we talking about um so let's look at an example so here we have three little snippets of code and uh the value x so x is bound to uh uh the the integer zero uh and so you could call it a declaration or or a reference um but it's never used uh at least in the context of this talk um so we're never uh reading x and doing something with it um in the second snippet we have y y set to one and we print it and so in that case we we call y uh being used one time by that println uh statement um and then in our third block here we said z equals two and then we print it twice um and so here we say that z is being used uh twice so for our purposes um used really just means dereferenced um every time we dereference a variable or a value or a binding or whatever it might be we consider that a usage and so this is a this is a fairly simple definition of linear types there are actually quite a few different definitions of linear types out there um for for our purposes our definition is most like what you can find on wiki wiki web which in particular says that the reference count of linear objects is always exactly one and that differs so linear haskell for example is a right now it's a proposal i think for extending the haskell compiler it's quite a bit more sophisticated uh and it states that linearity is a property of function arrows rather than of types or references uh like we're doing here um but hey i'll show you yeah sorry to interrupt you real quick and this might be a little bit late of a question but does one say that foo is linear in x and y uh that i think in the haskell definition that is how you would say it um when we're just counting references which is uh how linear scala works i'm not sure if that would be completely correct i would definitely say that x and y in the context of foo are linear actually yeah i think so thinking about it i i don't think i would say foo is linear let me just go back to that slide if you feel like you can circle back to this in the discord later sure yeah yeah i'll just i'll time box it at 10 seconds here i think for for me to say that foo was linear i would want the return type to be linear um but then that gets into some uh some weeds we can actually call foo more than once which isn't very useful as we'll see with haskell so let me jump ahead so back to haskell this is what linear types look like in haskell so they normally uh the type of a function would be a right arrow b for a function that takes a ti takes an a and returns a b um linear haskell again is this proposal to extend haskell and they introduced this uh lollipop operator uh and um that is called like a linear arrow and and so here we say that um uh that f so sorry i'm trying to phrase this based on your question um so that f is a linear function um and so the a key difference here that i'm i'm sort of fumbling to say is that f itself can be many many times it's not that f is will only ever have one reference or one usage it's that the it's f applied to a specific argument that combination is what needs to be linear so for example if i say f of foo and then f of bar so i'm calling the function and passing it two different arguments um f of foo would be linear like that that exact um evaluation would be linear and there would only be one instance of that uh and then f of bar again there would be just one instance of that and so that would be exactly one usage of two different things hopefully that makes a little bit of sense we can take this offline afterward and really get into the weeds and i'm very much not an expert in the the haskell implementation of um linear types um okay so um in the interest of time uh i'm i'm going to skip over a little bit of how these actually work in scala but in a nutshell um uh to implement linear types in scala i just used a custom linting rule in scala fix and called the project linear scala and really all it does is it traverses the syntax tree looks for bindings and variables that have a linear marker interface uh counts those or keeps track of those and then counts d references to them and make sure that all those geo references are equal one that's really all it does so i'd be happy after the talk to dive into how that works um if if anyone would be interested um but the important thing for this talk is what linear types can do for us rather than how this particular implementation was done all right so i have a few oops sorry about that okay so i have a few exercises here that we can go through until we run out of time basically so here's sort of a thought exercise can anyone spot the bug in this code well since i can't see discord right now i'll just uh i'll answer myself so uh we're passing the wrong arguments to the monod instance so here we have we're we're creating a function called concat uh concat takes two arguments of type a where a has a monoid and it returns an argument of type a so we're probably just uh delegating to the concat inside of the monod instance that uh is available for this function called is that x is used twice yeah yeah exactly so we're uh we're conjuring up our uh monoid and we're calling concat and then we're passing x twice so yeah that that compiles just fine um that would run but it's probably not what we meant to do we probably meant to concat uh x and y so if we run this code z will be uh one two three one two three rather than one two three four five six so how can we catch this at compile time that's really what we're going for with linear types well we can make it linear so with linear scala as i said we can mark our we can mark certain types with this linear marker interface and then that requires that values of those types in this case x and y uh must be used exactly once so everything else in this code is the same we've just added these these markers so x is a with linear y is a with linear we still have our bug here um and then i've i've just cast these two lists so that will keep the compiler happy and then we try to concatenate x and y just like before so when we try to compile this with linear scala we get a compile error so the the linter will give us a couple of errors that will say that hey you told me that y is linear but you never used it it was used zero times and it must be used once and similarly you told me that x is linear but you're using it twice and so these are the errors that you'll get from linear scala when you try to compile this code so now this bug is caught at compile time and uh which is great it's a much better time to catch bugs um so now we can fix it uh we got the compile error we fixed the code we changed our x to a y here um and now not only is it correct but now the code will actually compile uh pretty simple example um but uh hopefully it illustrates um that uh there are some types of uh there are some categories of bugs that uh will make the compiler today happy uh that we can catch if we make the compiler a little bit more restrictive so i guess one question is could you alias uh a with linear to something shorter in order to shorten the code yep yeah there are lots of different ways that you can make something be linear here we're mixing in a trait uh you could have a type alias that's like you know l of a equals a with linear that would work you can make your own custom data types that extend linear like case class foo extends linear i was actually wondering like is there a way to sort it to get rid of the as instance of stuff uh probably it's pretty annoying to have to write it but um i think that so one possible improvement i think for linear scala is rather than a marker interface which causes all this casting to be needed you know when we use it uh using a uh an annotation or or something that actually gets erased uh by the compiler and then never even makes it into the bytecode could be a way to make the syntax a little bit cleaner linear scala as it's implemented today is a you know mostly a toy uh to experiment with um with linear types in scala so yeah i definitely don't think that the uh the syntax here is the cleanest um but it at least lets us demonstrate the idea very cool and i guess one more question and i don't understand the question but maybe you do which is does a with linear effectively cast a to an r value reference in c plus plus terms i have no idea okay so what would be nice is what would would be nice is if um making a type linear didn't actually change its type like we are here um so that's why i would love to erase it at compile time maybe make this a macro instead of a scala fix rule um scala fix just made this super easy to implement at the cost of we have to have this marker interface everywhere um cool so we have a bunch more of these examples um and another 10 minutes to get through them so i'd love to show just a few more cases where this can be useful uh so once again uh let's try to spot the bug um in this case it's a more subtle example and we actually it might not even be a bug we don't really know but basically we have x bound to two different values right we have uh x equals six up here and x equals eight uh in the foo uh function um and then foo takes x and y and multiplies them and returns the result so that's fine there's not necessarily anything wrong with this we do this all the time it's just uh shadowing um but uh it could potentially be a code smell it could be something fishy like did the author really mean to use this x or did they want six up here uh or vice versa you know maybe they wanted eight and the six up here is actually unneeded it's unused by anything but it's really unclear just looking at the code uh with no explanation of why there are two x's um which one should be uh used so we can't assume that we can get rid of either one of them but we can force the author to uh to decide by making them linear so let's do that so once again all we've done is change the type of x x and y to be instead of int it's just int with linear and we're just doing that by casting so by making these linear we are telling the compiler well specifically telling linear scala that this x must be used exactly once this x must be used exactly once and this y must be used exactly once and we can see just from the code available that that's true for these two values but this one is never used and sure enough if we try to compile it we get a compile error that says uh this is linear but you never used it anywhere and so to fix it well we at the risk of breaking the code and changing its meaning how we we can we need to get rid of one of the x's so i'll assume that the author actually wanted to use this global x and drop the one inside the foo really you know we would at this point if this were production code i would uh want to go back and figure out what is the use case what is this code actually trying to do and then you know maybe eliminate this one or change some value names or try to figure out well was this x actually supposed to be used somewhere else um or is it just essentially dead code um any of these is possible we don't really know for sure and linear types can't tell us uh what they can tell us is that something might is a little bit off about this code and now that we've removed one of those x's the intent is much more clear uh this in the interest of time i'll go through this one really quickly this is the exact same uh example except rather than a method we're using bindings in four comprehension so we've got x y x there are two x's uh one is bound to six one is bound to eight and the second one shadows the first so when we return uh x times y we're multiplying eight by seven so again you know the reader of this code could say well wait a minute what's the point of this one it's not being used can we get rid of it well if we make it linear the compiler will force us to so if we change our types to be option of uh ant with linear now x y and x must each be used exactly once and our compiler tells us so um and so we can fix it by getting rid of the unused x and so i'm getting rid of the one that's eight again just like i did before so again potentially changing the meaning of this code so i may have actually just introduced a bug by uh changing uh this x to b6 instead of eight so the next step would be to go and find out you know how's this code actually supposed to work and and make sure it does that but at least once we're at that point we can't accidentally reintroduce the same sort of shadowing potential bug okay and i think this will be the last example that we go through at the code level so again let's try to spot the bug here we have a function that takes a source and reads its contents and returns the contents as a string and then closes the the source whatever it might be then we read a file as a source and we read its contents and print it to the screen twice and as you may guess we have a problem here so this code compiles just fine but if we try to run it we get a runtime exception on this line because when we pass s into read the second time s has already been closed and so s dot mixture will throw an exception about the stream being closed so in other words we're trying to do something with a file that whose handle has already been closed and you can imagine um this pattern applies to really anything that's closable network connections database transactions what else uh basically any kind of i o uh really anything with a closable uh interface so once again let's make this linear um all we've changed here is we've made s itself linear so i'll go back one before s was just a source and now s is a source with linear and we just do that by casting so now when we try to compile this code we get compile errors because linear scala tells us that hey you told me s was supposed to be linear but i see you're using it two times uh so we actually get two separate errors on this code and so to fix it we just need to make sure that we're only using s one time uh we're caching that result and then that's what we're printing out twice there are lots of other interesting use cases that um that we don't have time to get into and also are a little bit hard to show in a slide format but um some of those include making sure that the database query is not uh is not run after the underlying connection or transaction has been committed or rolled back that's a bug that i've run into before making sure that a stream of data is fully consumed whether we're pushing or pulling a stream or that some kind of protocol is adhered to this happens before that before doing this and then the other we could use linear types to debounce code that has side effects or should should that is non-item-potent but needs to be item-potent um and then actually as we saw we can detect and prevent dead codes so if there's a variable that's just sitting around unused um that might be important to know because either it should be used somewhere and there's a bug or it doesn't need to be used and we can delete it and we don't have to maintain it um there are lots more examples like this in the linear scala project um so if you dive into this directory which is essentially the tests you can see a bunch of examples all right so so the point of all of this is that linear types are an incremental um increase to the restrictiveness of our type system that ensures that values are used exactly once and that this is a technique that can help us write code that is more understandable and has fewer bugs and that's it so there's no questions in the discord um but i actually have a question which is were you able to implement this entirely within the scope of a library or did you need to write any plugins to get this working so i built this entirely on top of scala fix which is a plug-in that that lets you write linting rules so you can write any kind of custom linting rules and those rules have access at compile time to basically the full ast of your code and so it it kind of sets up all of the uh the underlying infrastructure for me the the author of this rule um to traverse that syntax tree and and look at anything i need to look at so uh yeah this would need to be either a compiler plug-in or a macro or an svt plug-in or something like that so that we can do this sort of meta um analysis of the of the code itself yeah i was i was just thinking that where it's like if you want if i wanted to write this i don't i think i would need to write a compiler plug-in so but it sounds like it it depends on skull effects right right on well then that's all the questions and we're we're good on time so um all right so thank you very much for coming in to talk to us about this james i really appreciate it and this has been really interesting for me and for others as well i'm sure i'm really curious to see like where all this goes and and what the future of the linear types is cool yeah and if you uh if you take a look at these slides i'll post a link uh later in discord there's a whole bunch of further reading and the linear haskell paper and talk that simon peyton jones uh gave is really fascinating um and easy to follow actually and then you can also learn about linear types is just one example of a substructural type system and the wikipedia page on that is pretty helpful we also touched a little bit on theorems for free when i talked about at the beginning the progression of types and what types tell us about what the code can or cannot do so i'd recommend recommend that paper for sure and then linear scholar itself is probably more useful as an example of how to write a scholar fix rule than uh how to implement linear types um but uh uh but it's worth uh browsing around if you're curious would you mind if you could maybe posting those in the uh the discord room yep we'll do awesome cool thank you so much again for for coming and sharing this with us all right thank you [Music] you