Reasoning with Types

SBTB 2014, Adelbert Chang: Reasoning with Types

Recording: SBTB 2014, Adelbert Chang: Reasoning with Types

all right so uh hi my name is delbert chang i'm a software engineer at box i work on the search and analytics team there where i do a bit of data mining and machine learning stuff and today i wanted to talk to you guys about reasoning with types oftentimes when we think about a type system we work in it can be easy to think about it as maybe just something the compiler needs to turn our source code into bytecode maybe it's something that may be helpful to just ensure the inputs to our function are sane but we can actually do much more with it to help us not only write the software to guide us toward the implementation that we want but also to formally prove certain properties of our programs and throughout this talk i'll be exploring some libraries from the type level project uh as examples of how we can use them to uh to essentially apply how we can use types of reasons about our programs so here's how our envisions for the next 40 minutes are going to go down i'm going to first talk about some assumptions scala is a very flexible language it allows us to write code in a very in various different ways so i'm going to talk i'm going to lay down some ground rules about how we're going to approach our scholar development for the duration of this talk then i'll move into the first part of my talk which will be on parametricity the general idea here is how we can use parametric polymorphism or what java calls generics to guess at what a function can and cannot do based solely on its type signature then i'll sort of switch gears a little bit and talk about logic and type specifically how we can use the type system we work in and treat it as a sort of logical framework to formally prove properties about our programs and how we can sort of encode proofs as programs and hopefully at the end i'll have 5-10 minutes for q a so some assumptions for the duration of this talk we will be subscribing to your thesis of functional programming and what this means is a few things first our functions will be total we will not be throwing exceptions anywhere as long as the input is valid as long as the input to a function is valid that is the types of line we will return some value back every single one of our inputs will relate to exactly one output which means that at any point in our program we call the same function with the exact same arguments we should get the exact same value back and finally we'll require expressions in our program to be referentially transparent and what this means is we can take any expression in our program replace it with what the expression will eventually evaluate to and not change the behavior of the program all right so parametricity the idea of parametricity came about in 1989 in a paper called theorems for free written by a famous computer scientist called phillip wadler and the general idea of the paper is types are documentation oftentimes when we think about documentation we think about doc strings right things like scala doc but doc strings can erode easily as our function grows as it changes uh maybe even if the function gets deleted the scalar dot can stay there as far as as far as the compiler is concerned it more or less does not exist it completely ignores it so it's plausible to think that we change the spec of our function or we change the type signature of our function our scalable doc is out of date and the compiler doesn't really care whereas if we use our types in a precise enough manner hopefully as our function grows and changes the compiler will catch us if we try to do something bad or we try to lie about the type signature so types are something that the whole program has to go through in order for it to actually compile and so it can't really erode as long as we use it in a precise enough manner so as a demonstration of this i have some examples so first we have a function here called whose name suggests uh that it reverses a list and it takes in a list of integers and returns a list of integers and based on just a type signature how many valid implementations are there for this well certainly we can think it can return the identity of the list it might return to empty list or indeed actually return the reverse of the list but by virtue of the fact that we know it's a list of integer and we know how to manifest say 2 to 32 different kinds of integers we can just manifest arbitrary terms of type list of end right so a valid implementation of the function of this function as far as the compiler is concerned is we can completely ignore the input and just return a constant list of integers maybe we take the size of the input list and turn and just wrap it up in a list maybe we dispatch on the size of the input list and then return a different constant list based on that right so we can do a bunch of weird things given just as type signature so what can we do better well when we reverse the list of ends we don't really care that we have a list of ins right we just care that we have a list of something i don't care what it is as long as the list is something i can reverse it so we removed the idea of having an integer so now what this function says is give me a list of a i don't care what kind of a and i will return to you a list of a well now we've removed the idea that we have a list of integer and we don't we no longer know how to just manifest arbitrary instances of a right the free theorem here now is any a that appears in the output list must have come from the input list so our implementations are now restricted to say the empty list or some permutation of the input list we can no longer just dispatch on a size list to return maybe a different constant list we can't just ignore the input unless we return to empty list so we've reduced our search space dramatically let's try a different example what about reducing down collection here we're taking a list of ants and we're producing an int certainly the name suggests that we should be summing this list of events and the implementation here certainly does that however there are some problems with this as before uh we can still cheat with our knowledge of int right as far as the compiler is concerned i can return any integer that i want and it will be happy because i returned a ninth additionally uh it's not quite generic enough right what if we wanted to sum a list of doubles or a list of longs or a list of biggins we'd be writing effectively the exact same function uh however for however many types that we want to do it so being the good programmers that we are we're going to abstract out this behavior so we're going to solve the second problem first i'm going to say now give me a list of a such that a conforms to this numeric type class right numeric is this type class in the standard library that attempts to abstract over the behavior of all our numeric types and here i'm doing the exact same thing because i'm just delegating to the zero in the plus method uh in the numeric type class and hopefully now we've uh we've now made it more generic and that we can sum a list of long lists of big and all with the exact same function but uh have we solved the problem of knowing too much well hopefully the we don't know enough to just manifest arbitrary instances of a right hopefully whatever a we eventually return is some function of the input however if you look in the numeric type class we have this kind of strange method called fromint that will take an end and is supposedly produced to you some value of t right that corresponds to that integer value so we're now still able to manifest terms of type of type a using this numeric from in so we haven't quite solved our problem yet and additionally it's not quite as generic as we like it to be because you can imagine what if we wanted to reduce down a list of string right in the case of empty list we return to empty string in the case of non-empty we just concatenate all strings together or a list of sets where we return to empty set in the case of empty list or we union all the sets together in the case of a non-empty list so as before let's think about what we actually need right when we reverse the function we didn't really care we had a list of end we cared that we had a list of something the list was the important part here what we actually care about is that we have a zero value of type a for the case of an empty list and it sort of act as the initial seed for our accumulation and we need some binary operation to do the accumulator right so as it turns out we have a notion of this and this is captured in libraries like scala zed and spire which are part of the type level project uh and this trait called a monoid right this is a type class that basically encompasses the idea of having some binary operation and some zero value an example of the moderate of int is simply to just add the two integers and the zero would just be uh the number zero so we change our function and we now say give me a list of a it's just that a forms a monoid and i will give to you an a and now we've drastically reduced our search space again right and no longer can we do anything like fro like numeric from int anything we know about a sort of comes from the fact that it's a monoid so the first argument to fold left says give me an arbitrary give me some a to start with and the best place to sort of get that a is one with zero and now the second argument to fold left says give me a binary operation to do the accumulation and indeed we can get this from monoi depend so we've now not only made the function extremely generic in that we can now not only some list of numeric types but also list of strings list of sets even list of maps uh we can also we've also made our function so general that we've sort of been guided toward the implementation that we actually care about we can go further right a lot of you might have heard of these things called functors of particulatives and monads i've written a function here that says give me a list of a a function from a to b and a function from b to c and i will get you a list of c by virtue of the fact that we know we're returning a list of something we can do some weird things right we can return just an empty list we can do what we actually care about where we map the composition of the two functions or we might reverse the list and then perform the map and potentially other weird things so let's look at the trade functor function abstracts over uh sort of some context and all you know about functor is that you can map over it right so if you have some f of a and a function a to b it can get you an f of b and now i modify my function not to say give me a list of a and a to b and b to c i say give me some f such that f forms a functor and an f of a to b and an f from b to c and i will get you an f of c so now all we know about f is not that it's a list by virtue of the fact that we knew was list we could do some stuff with it all we know that all we know about f is that we can map over it so it's sort of the only reasonable thing to do here and perhaps the only thing we can do here is to incent map f dot map g which is exactly what we want here so parametricity is nice with parametricity we can write extremely generic functions and we can also guide ourselves towards implementation of a function and sort of rule out things a particular function can or cannot do based on solely's type signature however there is some sadness here if we look at this function i'm saying give me an a and i can produce to you a b so for the past few examples the only place we sort of we were able to produce an output is by some function of input here we're saying i'm going to return to you a b well i don't know anything about b so hopefully you're giving me a b for me to sort of return or operate on to return to you but you've given me an a and as far as this function is concerned there's no relationship between a and b so if you see a function like this you would expect it to simply not exist it should not compile but you can do some weird things by virtue of scala being this very flexible language you can do a senseless cast do an as instance of or you can completely subvert uh i guess subvert the type system and use just simply throw an exception right as far as compower is concerned exception throwing is fine and you can do other things that break parametricity perhaps not in the context of this particular example but in general uh things like null type casing and type casting you can do side effects and you can use methods on a javalink object and uh thankfully for a lot of these things in fact i believe all of these things we are able to if not restrict ourselves from using them but have the compiler stop us in the tracks if we try to use these and there is a project in the type level project called wart remover which is a compiler plugin that will essentially analyze the ast and make sure you're not doing any of these things and if you are essentially fails to compile or at least generate some warning for you however there is still one more implementation that is valid and it looks like this we simply recurse on itself and as far as the compiler is concerned this is fine right you're calling a function with the correct argument that function returns a b and you want to give a b back so everything type checks and it's fine uh this unfortunately the compiler can't really catch for us because to catch this problem is essentially to solve the halting problem and as we know a halting problem is undecidable in the presence of turning completeness and skull is a turning complete language so we're sort of stuck uh with not having complete totality checking as sort of a fun fact many theorem proving languages or many dependently typed languages give up during completeness in favor of totality checking because a lot of these theorem proving languages are based around the fact of if your program type checks you've essentially proved your theorem and i'll get there's a story related to the second half of my talk and if you were able to make something like this absurd function compile then you've now basically broken the logical framework in which your theorem prover lives in so to give during completeness to make sure that your functions do terminate before we leave the world of parametricity let's go to a fancier example so earlier i mentioned the idea of ammonoid and mono is sort of a weird word some of you might be thinking that i just made up the idea of a manual that just happened to suit my needs for this particular presentation but actually it comes from it's a very well-defined idea a very well-defined concept and it comes from the wonderful field of abstract algebra and there's many more cool things we can take from it right we have things with other weird names like semi groups semi rings rings and fields and we can use these ideas in the same way that we use monoid earlier to write not only very generic code but to also ensure our implementation does not lie in regards to what our function can and cannot do so we have this library called spire that i mentioned earlier in type level that attempts to encode all these wonderful things so for instance a semigroup is just something that has a binary operation we have a monoid that's basically a semi group plus a zero value we have a group that allows us to essentially not only add two things but also subtract two things and many other and much more so how can we use these things well in my line of work where we do a lot of data mining and machine learning dealing with vectors is a very common practice right we have various feature vectors we want to do vector addition vector subtraction normalization all this fancy linear algebra so what sort of things do we do as i mentioned addition and subtraction scale and multiplication this is called a module if you want scalar division does it call a vector space you can do normalization and you can do dot products right these are pretty common linear algebra operations we expect to be able to do with vectors now the naive way of doing things is to maybe just fix things uh fix your vec your modules as like a vector double right vector here is the collection vector double sort of encaps encompasses anything we would really ever want to do with a number we can add doubles subtract them divide take the square root take the factorial whatever or maybe not factorial but yeah but just as before why do we specialize to double and in fact why do we specialize to vector uh we know a lot of things uh we can do a lot of weird things to double we can do a lot of weird things with vector so what do we really care about again there's gonna be a common thing uh what do we really care about when we work with modules and vector spaces well we only care that we can add subtract and multiply the inner type right the scalar type so put another way we require the scalar type not that it's a double but that it forms something called a ring and here we have the definition for the ring type class you can negate which gives us the ability to subtract we can plus which is add times for scalar multiplication and now our module isn't fixed as a vector of double but it's parameterized over two types of v which is the vector type and r which is the scalar type and here the implicit abstract depth says we require our scalar type to form a ring and now given a module we know how to add two two modules together subtract your modules together and perform scale and multiplication what if we want scalar division that's something reasonable that we want to do uh rings support negation addition and multiplication as demonstrated earlier but not division and to ask for division is to essentially ask for more power so for example integers are closed over uh the ring operations right if you take any two integers and you subtract or add or multiply them you will definitely get an integer back whereas if you take two arbitrary integers and as you divide them you can't guarantee that the result you get back is an integer right if i took two divided by four that's sort of that's a rational number not an integer so division is asking for more power and the wonderful field of abstract algebra and encoded by spire gives us the notion of a field and a field is simply a ring an addition with uh with the ability to divide things and now we have a vector space which is basically a module that allows us to do scalar division and we now require not that the scalar forms just a ring but also that the scalar type forms a field uh and as as before this this uh all of these type checks because if you have a field you certainly have a ring you just sort of ignore the fact that you can do division at this point i'm going to switch gears a little bit that's that sort of ends the parametricity side of my talk now i'm going to talk about logic and types and how we can use type systems as a sort of logical framework you think about our programs so there's a profound relationship between proofs and computation for the next next few minutes for this part of the talk i want to emphasize that we should not only look at the code as code we deal with every day but also as a sort of thing that encodes a logical framework and codes propositions and a sort of mathematical proof so this relationship is known as the curry howard correspondence or the curry howard isomorphism and essentially it boils down to the more expressive your type system is the more expressive the proof that your program corresponds to becomes so an example of how this correspondence works i put some in this table here the very basic unit you have in logic is sort of a proposition and that is simply just a type in our program if you want to prove the proposition you create a term of that type so if your proposition is provable it must have at least one term of that type if you want to take the conjunction of two propositions that's simply the type uh pair of pq right and you can think about how do we prove pnq how do we create a term of p and q we have to create a term of p that is to prove p and we have to create a term of q that is to prove q and then we have the famous modus ponens which is ifp and q and here that's just a function give me a p and i can produce you a q right i have to prove p first i'll give it to this function this function will take my proof of p and then prove to me q so as an example let's get the head of a list uh i have a function that takes in a list of a and produces to me an a or we can think of this in the context of curry howard and more specifically modus ponens if you can prove to me a list of a i can prove to you a if list a then a here if i i'm doing a pattern match if i have an empty list i'm simply going to just throw an exception and if it's not empty i'm just going to return to you the head of the list like you expected uh the problem with this is that head is partial right earlier when i laid down the ground rules we don't want to throw exceptions exceptions sort of subvert the type system and by subverting the type system you're subverting the logical framework in which your program lives in so we don't want that we want to return some value since nil is a valid input into our function so okay we'll return null null is a valid value as far as the compiler is concerned now the problem with this is null is evil let me convince you of this uh tony horror who sort of invented null calls null his billion dollar mistake and the problem with noel is that it is inhabits every single type so what this means in the context of curry howard is that any proposition can be proved trivially right if a proposition can be proved if a proposition is provable there must be a term of that type no is a term of that type so every proposition is provable to actually prove it we have to create a term of that type as far as the compiler is concerned null is a valid term of any type so null essentially just destroys the logical frame the nice logical framework in which our program lives in what this means computationally is that developers are sort of left to their own devices to handle null right at any point in your program if you have some sort of object that object may or may not be null and you're sort of left to doing null checks and your code starts marching marching off the right the right side of your screen and and nobody wants to see that and if at some point you screw up the compiler doesn't really care and at runtime you get a nice null pointer exception so let's try again again what are we really trying to do here well here we're trying to say if list of a then a right give me a list of a and i can prove to you and a well clearly we can't quite do that because if it's the empty list then we have no a to give back so what we're really trying to do is say uh given the list of a i may or may not be able to prove to you a so we try to do that with null but null since it inhabits every single type it's not exactly what we want so we want some sort of type that encapsulates the idea of i may or may not have a value and this should sound familiar to a lot of you this is precisely option in scala right so we either have none which is an absence of a value or we have sum which is the value that you care about and if you uh you can note that the number of inhabitants of option are precisely the number of inhabitants of a plus one and it's this plus one that gives us the i couldn't prove it part so we read our uh we rewrite our function and we say if list of a then option of a or give me a list of a and i may or may not be able to prove to you a and so when it's an empty list i give you none i wasn't able to prove it if it's a non-empty list then i was able to prove it and here is the head of your list however at this point a lot of people will say well i know my list will not be empty right maybe they did at the call side they did a side check if list dot size is greater than or equal to one then call this head well i got an option i don't want to deal with it i'm just going to call get on the option well option get throws an exception and now you're sort of back to where we started with just calling unsafe head on a list so what do we do well if you truly know your list will never be empty you can think of that as saying well i'm proposing i have a proposition that says my list will not be empty and curry howard says well if you have a proposition well let's create a type that corresponds to that proposition so we have a type called non-empty list and this is actually available in the scala z library and its constructor says give me at least one element of a and that's the way that's how it guarantees that your list is not empty and in the tail you can just give me a plain list and now your head function says if you can prove to me a non-empty list if you can statically construct a non-empty list statically prove that your list is not empty then sure i can prove to you a by simply giving you the head right because we know not by virtue of of having a non-empty list at construction you had an a to give me now the idea the notion of a non-empty list is sort of weird right maybe i concocted this just so i could prove a point here but there are uses of this uh in scholar said we have this notion of validation and specifically we have an alias called validation at nell nella's non-empty list and you can think of validation as a sort of either right validation is either successful or or it fails just like how either has uh left or right the trick with or the nice part about validation is that if you execute this validation against several inputs it should be able to collect all your outputs and if at any point uh one or more of your uh one or more of your inputs fail then it will collect any and all errors right sort of with either or try sort of short circuit that stops at the very first failure you give it validation is able to accumulate all these errors and oftentimes you will accumulate these errors in the form of a list by virtue of the fact that you know if at runtime you you know you got a failure by virtue of having a failure you know that at least one thing went wrong so if instead of non-empty list we use list well i now have a failure of a list i sort of know that the list is not empty but the semantics the typed list doesn't encode the fact that uh i have a non-empty list right list delicious semantics say give me any size list whether it's empty or not empty so we provide non-empty lists so when you have a failure of a non-empty list indeed you know by virtue of having a failure there's at least one error and the fact that you have a non-empty list of these error types proves that yes there was indeed one failure similarly we have a function group by in the standard library that takes a list of a and then essentially sorts these a's by the function that you pass in and it gives you a map from b to list of a in the standard library well if you know that b exists by virtue of b even existing in a map you sort of know that the value corresponding to b is not empty because for that b to exist they had that function this b was a result of some function result applied to one of the inputs so list isn't quite what you want since list can be empty but you know sort of that it's not empty so instead we could imagine a group by that returns a non-empty list instead we can statically prove that uh by virtue of b being this map you have at least one element whose result when you pass it into a function is this b so we're going to slightly switch gears a little bit and we're going to talk about curry howard and type classes and this sort of ties back to uh the earlier sum function that we had uh given a list of a so that a forms a monoid i can give you an a or put a different way give me uh if you can prove list of a and a uh forms a monoid then i can prove to you a now how do you prove that something a forms monitor what does it mean for a to form of monoid well we're proposing the idea to propose a notion of a monoid we're essentially saying well we have a type monoid that has a an append and a zero method and to prove a is a monoid is to create a term of type monoid of a right so in a case where we want to prove that integer forms a monomial we create a monoid of int so our proposition is simply the trait the type class monoid and the proof of int is uh simply to implement modulated event and usually this proof will be like an implicit value inside an object maybe the companion object of monoid and one of the reasons you can think about why it's implicit is basically once we've proved it we're sort of done we don't want to pass around this proof all around our program right we've proved that in forms of monoid the rest of the program should be able to say each time something expects a model it should be able to find this proof so in our sum function when we call sum with say a list of integers when the compiler goes to do the implicit search to look for something of monoid int you can think of it as proof search so in using scala zed if i just call sum of list of int with just the skeleton monoid import uh it will give you could not find implicit value and you can sort of think of this as i couldn't find proof that it performs a moderate right there's no implicit value of monoid and scope so what do we do we import the implicit value from a particular object and now when we call sum with our list of end what the compiler will do is say okay let's try to prove that informs a monoid by looking for an implicit monoid end in scope uh it finds it finds the thing that we imported we've proved if it's satisfied with the proof and everything compiles and everything runs we can go a bit further with the idea of a monoid so many of the type classes in libraries such as skulls that inspire right earlier i mentioned we have monoi semi groups rings fields functors they are inspired by mathematics right especially abstract algebra and group theory and category theory and mathematics as we all know is very much governed by the idea of laws so for instance the notion of a monoid we don't care just that it has a binary operation we care that it has an associative binary operation so the type classes that we derive from these things should abide by these laws for example monois have an associative binary operation and a zero that is an identity in relation to this binary operation and this is useful for two reasons one is that it further restricts the behavior of the type right so this sort of aids parametricity which is the first half of the talk and it also allows us to exploit these laws so for example if you have some list of monoids since you know it's associative you can sort of partition this list into several chunks fan it out to different machines or different cores and bring it all back and then merge them all using this associative binary operation and you sort of know that this is sound because the operation is associative unfortunately in the presence of a non-dependently typed type system we can't statically enforce that operation is associative the compiler just checks that we took in two ways and produce an a or that zero is just some a however laws are perfect for what are called property based testing right in traditional unit testing we sort of feed in fixed inputs and we say we expect this output out for these inputs of course for properties-based testing we're sort of asserting properties uh that are that the output will have for all inputs and so for instance of for a case of onenoids we say well for any three integers the addition operation is associative and for uh for the zero case for any integer x plus zero is the same as zero plus x which is the same as x and when you run this test using a library like scholarship and discipline again libraries from the type level project it will essentially just generate random values of integers run it against uh against monoi depend on this monolith zero and make sure that your properties hold and so we're sort of satisfy ourselves and saying well we ran a function for a bunch of random inputs the property holds let's just uh let's just assume that we now have a valid onenoid so our code now becomes even more strictly specified uh by just the types and the properties right our code was already fairly specified uh by virtue of using typewrite using parametric polymorphism and thinking about our program in the context of curry howard now in addition with the properties that we assert we can so our program becomes even more strictly specified so we're now moving away from an idea of say our our unit test test for the few inputs that we did for our unit test the prop uh this particular output was expected and it matches or that our scala dock says so so in summary types are robust they're a form of documentation and you shouldn't think of them as something just for the compiler they're a tool for you to use to help you reason about your program to help you implement your program you should be able to use types to hint at what a function can do but perhaps more importantly what a function cannot do types are a static property of your program in that if you try to subvert the type system you've now introduced not only a whole an escape patch in your program but also in a logical inconsistency in of your program in the context of curry howard and in general the general theme is recognize the difference between trust me i'm a nice person i will or will not do this and the compiler would not have compiled or would only have compiled it if it did or did not do this that's it any questions um so one example of the top of my head right now would be in our sum example the only reason the sum function worked the way it did was because the identity was related to the binary operation uh if i sum if i use zero as like one as the integer one instead the sum function wouldn't have really been a sum same thing with like set union if instead of the empty set i return like some arbitrary set as a zero that's not really said union so that's one case off top of my head uh up here i can't really think clearly so maybe yeah in the hallway we can talk right so there's nothing as far as compiler is concerned uh doesn't there's nothing preventing you from zero the idea here is we've uh the goal isn't exactly to just say we have only one valid implementation of this function the goal the general idea is how we can uh narrow down the state the search space for our implementation right uh if we use numeric we could have done a lot of weird things with numeric by virtue of using from end whereas here we have a more limited subset of things we can do with the function but yes if we just return 1.0 as far as the compiler is concerned everything is fine but if we use something like uh like scholarship or discipline use property-based testing we can gain more confidence not only from the types but also from the property that we specify machine learning programs like i eventually gave it use uh so in terms of machine learning i know there's this really interesting project at least so it's not something that we use directly but something i'm sort of looking into there's this really interesting project in haskell called h-learn where they basically exploit uh the monoi properties of certain machine learning algorithms and what they're able to do with this is you can write you can write a particular workflow and then you can run it and sequence sequentially on one cpu and once you wanted to distribute it to several machines or something it was it's able to do that extremely easily and sort of in a free way because by virtue of it being a monoid it can do it can run it serially if it wants to but it can also fan out to several machines uh at box the way we do machine learning is uh our all our vector types that we're dealing with aren't just uh monoids we do do the whole ring field thing that we described about and this has helped a lot of people even those who aren't as familiar with scala to help it helps them write the correct implementation that they intend to because by virtue of the fact that they only know that the scalar forms like a field they can't do things like oh if this thing does not equal zero or something like that all they can do with it is the operation specified on this particular field thank you