SBTB 2014, Jared Roesch: Demystifying Shapeless: An Exploration of Dependent Types in Scala
hey everyone uh my name is Jared uh I'm going to be talking about demystifying shapeless so kind of my inter my inspiration for this talk is that for the summer I'm a grad student at UCSB um for the summer I'm working at a ruby shop and I'm writing a lot of Ruby and I'm really really frustrated and so I've been thinking about all these interesting ways about how I can get flexible typing to do crazy things and so one of the main things that I've been struggling is I was porting from one version to another I was dealing with string and cing issues and like as a shapeless programmer I'm like oh I could have strings that statically know they're encoding and so I started to go down this kind of rabbit hole and I realized like if you don't really understand the implementation techniques behind shapeless it's really hard for you to leverage these kind of ideas as a day-to-day programmer and so I wanted to kind of give a talk that was about exploring how is shapeless like kind of implemented what were the ideas behind it and how can you take this back into your normal day-to-day programming to get stronger static guarantees so who am I um I'm currently working in VCA we do um telepan kind of stuff we have C some um uh telephony switch and a bunch of other cool things um it's kind of a fun technical challenge to work on uh the Ruby part I'm not a huge Ruby fan but um I also am a master student at UCSB um I just finished my undergrad there uh while there I've done a bunch of different kinds of research I've worked on a jit compiler I worked on program fuzzing for schola actually we can like Generate random scholar programs um it's pretty cool on top of that I've also taught the undergraduate or help ta the undergraduate programming languages class in schola so I've done a bunch of schola there all most of my research projects have been in Scola uh I write a fair amount of my free time um I'm all over the place uh as you might tell I do all kinds of different things I'm a really big high school programmer I have been writing a ton of Idis which doesn't have a logo as far as I know um I also have been writing a lot of rust um and I also write a ton of Scala and this is where I get to work which is great um so what is shapeless for those you who don't know um it's build a lot of different things at one point on the page miles build it as a um framework for polytypic and generic programming which might sound a little intimidating um really what it is about is pushing the boundaries of what we can do at compile time and providing a lot of interesting abstractions for you to do this um a lot of it tends to kind of go with a lot of the pure functional programming Community um but I kind of think some of these ideas are all a cart you can take them by themselves without having to import all of it in um and it's really become a playground for advanced type f typed FP in Scala so it has a lot lot a lot a lot of features um this is just the like main feature listing that Miles presents um on the project page so polymorphic function values functions that can take different kinds of arguments um so for example we can just peek ahead for a second something something like this um so for example I can declare this polymorphic function it can take an integer this is what I do when I get an integer the second line is what I do when I get a string the third line is when I get a tupo and if for example if we call it on a list like this we'll see for the integer we get one back for the string we get the length of the string for the tupal we get it size and this becomes really really flexible so for uh about a year back I was working on a prototype driver for rethink DB which is one of those not SQL DBS kind of popular on Hacker News or whatever um and I use shapeless to actually their their career language is completely untyped and I use shapeless to get like three quarters of the way of emulating in Scola so it's really really flexible um so a bunch of other cool things the main thing that a lot of things are built on are heterogeneous lists um you guys might have seen this this is a list where every element knows its type um so for example I if I get a h list back like in the previous example we can see I construct an H list on the second to last line then when I map over it I get an H list as a result and the type of this is actually into int int H nail um we'll talk a little bit more about that as we go on um and there's tons and tons of other features um honestly some of these by themselves are probably a 40-minute talk um so I'm going to just kind of go at a high level and again kind of focus on the extracting the wisdom from the implementation of shapeless so um it was kind of inspired by a lot of things um in the has school Community there's the idea of scrap your boiler plate so uh back in about 2003 I want to say there was a paper um by Ralph laml and s p Jones I believe on doing generic programming over many different kinds of uh data types so for example they wanted to implement something like a generic map or a generic fold function and have it be implementable for any data type so their original thing required very very little boilerplate it required you to do one little Declaration of a type class um if not they also wred a tool that would automatically generate that stuff for you um over time it's become more advanced they actually released a series of papers um but with scol macros and a lot of the stuff that Miles has been doing this has become really boilerplate free in Scala um there's also more inspiration from things like generic deriving so this is like um for example there's a simple type class that the scol Ed people use called show which prints a string representation of your type um for example you can have it automatically derive something like that for you but you can also have a derive of quality and so on and so forth or like uh adbert was talking about yesterday you can have a derive a monoid instance you can do all kinds of cool things and then a lot of the insiration has been taking taken from dependently type languages which are usually kind of thought of as these academic esoteric things but there's actually a lot of cool ideas even if you're not programming that language it can be uh imported back so the main thing again I was talking about is static reasoning um and this is really what I'm interested in um if anything my research experience as doing programming languages stuff has taught me that this is really really powerful and then back in the engineering world it's really nice to just say something holds and know it holds instead of reasoning about all right what are the different failure modes and this is something that I've really why kind of the my experience writing Ruby has kind of instructed some of this talk is that there's so many crazy things that can go wrong because everything happens at runtime you can redefine methods you can do all kinds of insanity um but I want to go to the other end and say how much of this can we fix a compile time and have the compiler give us an error message because it's much better to tell have the compiler tell me that I'm an idiot up front then me to like crash a server in the middle of the night and and get hit on pag your duty or whatever um so the way shapeless Works um every almost everything's happening at compile time you pay a minor cost of passing around these proof terms that we'll talk about constructing um and also that you pay it in compile time because the implicit selection takes a while um so I just want to show some more examples a little bit so this is something that I had helped adbert with a few weeks ago probably um where he had a list of any things and he wanted to come up with a type safe cast and just cast it into a case class and if the cast works you'll get an option back that's either the value you wanted or nothing so in this in this case um what we do here is you give me a list if it's castable I can give you a point back or I not and you can do this for an arbitrary case class requires no boiler plate so if you import shap list and you grab this snippet of code right here you can do this just hand me a list and the list typing could also be different um but list of any just here to demonstrate that you don't actually need the typing information right there um there's other things like Joanie Freeman has been working on type SQL um so for example that string is actually checked at compile time it produces a chunk of code that then is a polymorphic function that we can call so for example we can run the query that's what the calling of Q does We Run The query we can map over it and we can get the age for example so in this case we got all the ages from the query that we ran and we get 36 and 14 um you can check out here there's been quite a bit of cool work done um and I encourage people to go look at it um one thing I want to touch on kind of before we continue is a lot of these ideas are pulling from these dependently typed languages and the really only big takeaway is that there's this relaxation of the phase distinction so when you're if you're a Java programmer for example or a scholar programmer you're used to types and values living in very different worlds they're not allowed to mix in any way uh independently type languages are really about easing this and saying hey my types can now talk about values um also I can do comp computation at type checking time um so if you go to Idis for example you can do things like run an arbitrary function in your type signature which is kind of cool um obviously Scola doesn't give us quite as much flexibility um but a lot of these things that are built with typ level programming are actually just kind of stealing ideas from dependent dependently type languages and bringing them over the fence so to kind of illustrate this distinction that I'm talking about you could for example look at something like this VC type so what we really want to write is imagine if we're in this a dependent type version of Scola we could ask for the Constructor for a vector to take a n which is its size so we're using natural numbers here because they're always greater than zero um or zero or above and we also take a type and we return a type so for example you could construct a vector of size one that contains a single integer and it would be you know vect int or sorry vect one int but in Scola if we wanted to write like this is our pseudo Scola right here on the on the third line if we look at that for example those are both types what we're really writing is that this trait is parameterized by type and a type and we get a type back um and so really a lot of what shapeless does and a lot of these techniques is about how do we get around this how do we exploit the language in a way for us to write something like the ideal but we can't so how do we estimate um so one of the important things is a bunch of people Bandy or kind of talk about types of logic um this is only really useful to us as a high level like understanding um we could all again give a 40-minute talk on the implications of this um the in theoretical PL Community there's a lot of research done on this every year um people are turning a lot of new interesting work in this area but really the main idea is that if you view your type system as a logical framework and we can just simply map one to one types to propositions and programs to proofs and you might not follow with me yet but we'll explain it by the end of the talk um but with this caveat a lot of times when people hear me say the word proof they think I'm talking about something interesting right like every proof has to be interesting but for example if I ask for proof of integer I can produce you an integer right that's proof of an integer I just want one integer um they're not always very interesting things so that's something to keep in mind um so if we want to emulate some of these ideas which is kind of my goal because again I think it's actually very much engineering motivated of like I want this thing to fail before the compiler finishes running um we need to get around this phase distinction so the thing is what we really want to do is we want all of our values to also have a type level representation so we can put them in the type and we we'll kind of get into that in the next slide but essentially it's this third line right is that I want to be a to use zero as both a value here and I want to be able to use zero in the type and say hey this Vector has no elements in it so we're going to start with natural numbers because this is like the simplest thing it might sound kind of contr but you actually need them all over the place right like if you want to do indexing numeric constraints like hey I want the size to be less than n um all kinds of things like this the traditional natural representation which comes from math um is kind of an idea of a zero element in a successor function and you apply the successor n number of times to reach the the nthn so if we apply it once we get one if we apply it twice we get two if we apply it three times we get three and so on and so forth um and we're going to first what we're going to do is we're going to concentrate on the value level we're going to look at a value level representation so like typical case class everything something that everyone should be familiar with then we're going to say all right mechanically how do we take this and transform it so that we can use it in this type level uh style and get a lot of benefits so for the value level we can take something really simple like this so we have a value representing a natural number we you know declare a seal trait we have a case object that represents zero we have a case class that represents successor it takes a natural number and is also a natural number itself so this is the function we talked about you know if I apply suck to zero I get one so on and so forth you know you could provide an implicit conversion that deals converts integers to this if you really want it to syntactically be nice um but the real question is how do we go from that initial idea of all right we have this value that looks like a natural number and move it to the type level so the problem really right is that if I give you a value as a knat and you want to use some type information about it I have no way to like compute the type and stick it in in a trait for example or in My Method declaration um so we're going to first cover a few prerequisites so this stuff kind of stretches maybe I I don't know if people think these are the esoteric language features they might be um it kind of stretches in that direction so we're going to cover all of them so that everyone has a good idea of what we're using and why these things are useful we'll cover them first and then as I go through my explanation afterwards I'm going to try to highlight where each of these fit in and why they're useful so implicits everyone knows loves or hates I'm sure um so really simple the way we're going to use them is they allow us to just pretty much demand something and have our demand satisfied so in this case we need something of type int and we're going to go look in the implicit scope at some point and pluck it down um and we're going to use this style all over the place um and I really like to think about it again is like obligation and fulfillment right I how someone owes me an integer please provide it to me and I think this is useful because as we construct these uh types that represent proofs it's really going to be say give me proof of this thing uh and I can do the thing that I'm implementing in My Method so type members are one of the things that we first want to uh cover so type members are useful because it allows us to put some type information in the value and we'll see that as we're talking about merging the value in the type level it's really important that our value has some information about its type so for example this is something contrive we have a user we want to make be hide the type of the email we put it on here they also have an email the important thing we can when we construct these things we also need to set the type member because it's part of the construction of the object um and that should be good the the interesting thing about this though obviously is that the the type is existential and what this means essentially is it's hidden it's abstract right so when I get any user on this last line right here the the type of email is hidden to me be um because it is a type member right all I know it is some type but unless you use structural refinement which we're going to talk about in a slide um you there's no way for you to see it so we can also make use of structural refinement types so this is about um refining them uh taking a type like this and exposing this piece of this information right here so another kind of uh simple example is assume we have some data data store and we want to have some database that backs it U and we want to actually hide that information from most of the users but every once in a while we might want to express that we only take a certain kind or that we only work on something that we know where the database type is so in this case um we can declare if we're going to use postgress the type of DB must be postgress and postgress in the last release just added binary Json for example let's say no other data store has it for sake for the sake of the example um we say all right writing a a binary blob Json requires it to be postgress and as we can see this kind of thing will work and this thing will fail because it won't have enough information to say all right I can prove that this data store where I don't set the type actually has postrest and so this is going to come into play um the other important thing with this is it subtyping um when we deal with subtyping here is if we have this unrefined trade at the top and we refine it with some piece of information in this case we say part of the type is actually the fact that its member T is string this is actually a subtype and this is that for those of you who are not familiar familiar with it this is that weird uh implicit operator that will only return an implicit these two are two things are actually a subtype so in this case this implicit returns it a value and refined is a subtype of unrefined so the subtyping rule is is important really for this reason because we're going to see on the um let's peek ahead for one second so here is our um our natural level representation right so this might look a little weird but what we do is we taken that and we know that all right we have some base cost all we do is reflect its type as part of its Val like as part of the value so now um every single natural number also has a member called n that contains the type of of itself um and in this case we zero is the base case this is equivalent to the zero that we saw a few slides below um for that was a case object and we simply extend it and we set its number to zero itself right that makes sense and then successor is the same thing except instead of operating at the value level it operates at the type level so we have a successor we say any n previous Nat right can be any KN um will provide you that its type representation here is the next number after it and so if I do suck of zero it's equal to one uh and we can see that um like right here for example so we can imagine um and miles does this in shapeless actually except he's gotten a little bit more clever about it has a macro so if you try to do something like turn negative one into a knat it will complain and throw its hands up in the air but the nice thing is here is we have a gat we can actually grab a type out of it here um with n and so in this case that would be equivalent to suck zero which is one for all ofensive purposes and the reason why we want to use these bounds is important is that if we just do something like this when we start looking for implicits every single natural number will give us the same thing back for this but if we use the bound instead we allow it to be some subtype so for example because zero is a distinct type and suck of zero is a distinct type and suck suck of suck of Z is a distinct type and so on and so forth we can actually find distinct proofs for each one of these types so if we have a proof for example that says Z is less than any number that's a successor and we go to look for that we will select it correctly versus if we just looked for natat it would totally fall apart and wouldn't work um so the main thing though is now that we have looked at the type level representation it might not be super clear yet I think once we look at how to implement a proof on top of it it will be we can look at like this value level so if we go back and and Rewind to the value level and we look at less than like this we write a simple algorithm right like this we we match um which I might have inverted I did to writing too much trust um so we match we we do the case um the right the sybol case obviously is zero and some successor is always true right zero is less than any number that is not zero this case right here we just subtract two things we subtract both numbers by one and we continue recursively um and then here we just return false and the reason we're doing this recursively is this is kind of kind of how all the implicit selection is going to have to work in a minute um and it will and it's easier to do it that way so what we really want to do is translate this piece of code and I think this is a relatively mechanical process so in the value level we're returning a Boolean right like we at runtime we want some answer about whether this thing is true or not but really what we want to do at um compile time is we want to provide some implicit if the relationship holds or not provide the implicit and why this is interesting is the compiler will halt when it can't find an implicit right so if we don't if the implicit is not available and or there's no way to manifest said implicit the compilation will fail and so what we first need to do is we need to translate the the thing we want to prove and we can use proven a loose sense here in this case we just want to demonstrate a relationship between two numbers so in this case for any number n and any number M this will represent a relationship that they're less than each other so if you have one of these objects someone has proved to you that n is less M and so now you might ask how do we do this so we've add we have the trade up top that we just looked at just to keep it in scope and you can see that before we had um in the value level algorithm and I'm going to step back to that for a second in the value level algorithm we have three cases right we have we have kind of this base case up here where we terminate we have the recursive case here and then we have the fall through so the cool thing is the fall through disappears because there is no like the failure is there is no implicit right we can't provide that we can't provide you appr proof so the nice thing is is we eliminate the fall through and then we just take these two cases and we're going to mechanically translate them into implicits so the cool thing here is that for the base case right we say for any number M which we need to do this little bit of a trick right here any number M I'll provide you a proof that the successor of that number is greater than zero and the reason why we need to do this is to disclude zero so if we didn't do that if we just said all right give me any number M and I'll prove it for you prove that it's zero that doesn't work right if M can be zero then I can provide a proof of Zer less than zero which is totally not true so the thing is we do this little trick right here to ensure that we're always providing um we're always correct here and this is something kind of I think important to draw attention to is when you're doing this kind of stuff uh doing these kind of things it's really it's hard to make mistakes but you can still make mistakes right like you can encode a proof that is not what you really want to say and then satisfy it so a lot of times when people talk about this stuff it seems immune to these kind of failures but you're still totally have the specific problem right you need to be able to specify what you want to say uh even if you're able to say it uh and then so for the recursive case is pretty easy as well so all we do is say for any n and M find a proof that n is less than M so this was like doing the recursive call before except it happens at the implicit level and then we construct a proof that the successor of N and the successor of M are uh less than each other because obviously if we take 0o and one for example and we add one to both they're still less than each other if we take 0 and 50 and we add one to both they're still less than each other um and so that should kind of be intuitively true then here's the final linking piece um and I'm just returning true because we're not actually doing anything of note here but you can take value so look I take a value representation of a Nat and a value representation of a Nat and then I just simply ask for proof that their type that the type members they have have that relationship and so this is how we tie the knot on moving so now we don't need the value level representation at all we now have a representation that exists both the value level and the type level and when we need to talk about the types we simply just reflect them from the value into the type signature here so we can move on to hlist which is like the bread and butter shape list and I thought I definitely worth talking about a little bit which is also really simple so most of the complexity in shapel list is around encoding these different proofs of like hey can I take four elements off the front can I index into the fifth element of a list that like in that case I need to prove the list is at least five elements long otherwise I can't do that um and things like that or head and which we're going to look at in a second so we start again same kind of pattern seal trait Base Class and we're going to use this again because we want those bounds everywhere to to do selection of subtype um then we're going to declare a case class and the cool thing about the H list is actually that it's covariant so if you have you know um a list of any any any you can pass a list of in int int so on and so forth similar to collections uh and so the nice thing here is that we simply just declare that there's some head type there's some tail type and then see we use the boundary again to say it can be any H list so this is important because with the subtyping relationship is T can be of the precise type so for example if the the end of the list is a single integer followed by nil we recover all that information when we construct it ver we could OB stens throw it away right if we only ask for t to be an H list right like if we remove that type parameter and just say tails an H list we would lose all that extra information so the nice thing is that this bound allows us to recover some Precision here and then we can put the Precision when we construct it so in the Constructor we only take something that types to H and we only take something that types to t uh and then we produce an H list as well uh and then we do this little trick right down here and this is a trick I did earlier in the slides but case objects don't declare a new type so this is again kind of in line of we create a type representation of H nil and then we create a value level representation of H nil so that we can use it both at the type and the value level and if you think back to or I have an example right here um if you see right here the type is int string h n and you can get away with this because um operator like um types with operator names can be or actually all types can be used infix so that's really all that the trick is here you could provide it a more of ver bothos name if if you liked um but you see H nil exists both on this side and this side and that's because we created a type h nil we also created a value H nil um all right so here's a really really simple proof on H list right I want to prove that there's at least a single element right that there's one con cell on the list so this is this is equivalent to statically asserting that my list has one element so the thing here is when I encode a proof object often times what I'll do is I'll insert the functionality directly into the object so I add these type parameter uh type fields and we'll see why these are important on the next slide and then I tell you I say hey if I do provide you this proof object it will have the functionality to call head and it will have the functionality to call tail and they'll be properly typed so the cool thing is then this looks really really hairy but most of this is super mechanical transformation so if we look at the top I've emitted some of the code that is in the actual implementation from shapeless there's this Ox type Alias you can mostly ignore this this is just a convenient way of writing out that long structural type on the second line so instead of writing out is hcon L Type H you know equals something type T equals T every time I can just write this little shorthand you know is hon. ox and then provide the type parameters and it looks a little bit cleaner so the thing here is that I just want to provide there's one case right there's the case where I have at least one element and I don't care about any other cases so you can look that again we take some parameters and this is to allow uh the type inference we're kind of almost programming the type inference in this in way we're getting it to solve some unification so in this case when we have head and tail we declare them we're hopefully going to get solved we say if someone asks for a proof of head cons onto Tails or on the tail will what will happen is those variables will be solved all this other stuff will flow so if I ask ask for a proof of int H nil head will be solved to int H nil will be solved to tail or tail will be solved to uh H nil um and then oh there's Miss indentation but then both of these variables will be set to that so in this case head will be int and I will then provide a method that shows you how to get an INT from that list tail will be H nil and H nil is an H list so this will work out just fine and I'll provide you with a way to return that and we notice that we take the full type so this takes int H nil and this takes in h nil um and the nice thing there is that then on the other side so this is the messy proof implementer side which um you can actually mostly ignore most of the time if you know what the proof relationship is um so in this case this is the like actual method definition on H lless and it's really simple if I want to call head I just ask for a piece of proof and then we use a feature that I mentioned earlier of path dependent types so they path dependent types are sound complicated but it's a very simple form of dependent types in Scola that allow um types happening in the result side to be accessed from value so in this case I get T from C and we notice again we have a type now depending on a value so in this case the return type is determined by the implicit we pick so if I find a proof in this case that I can actually pull the int off the front of our list then I will return you an inch even though it doesn't say that right there and I will invoke the functionality on the list and get it back so on the you could be totally unaware of how a is hcon is implemented and you could ask for this chunk of proof and have it manifested to you and that kind of goes back to one of my main points with shapeless is that most of these proof objects are black boxes and this is something that I missed when I first started programming in shapeless is I found it really complicated but I realized is that anytime you start to write generic code if it can't be completely statically determined you need to ask you need to push it up and say I need a proof obligation before I can run this code um and to kind of illustrate this is for example generic so generic um has had a few different implementations in shapeless the current one is an implicit materialization macro which is really complicated um I don't actually know anything about how it's implemented but I can totally use the functionality of generic unbeknownst because that's the proof part of it is pretty much a black box to me so in this case I ask for uh all of these objects all the companion objects have an apply method that takes a single type argument that will give you back the generic instense so in this case if I want a generic point I can just get a generic instance for a point by asking for it right there so we get the generic and generic is this cool thing that allows you to provid a conversion between product types so like case classes um tupal all that kind of stuff into an hlist representation so what's cool about this is given the hlist repr representation you can do all kinds of generic programming things so you could write serializers on top of this and do a bunch of other um pretty cool generic programming techniques um and Miles actually implements a lot of this in shapeless so if you're interested go look there um but you can see then I I annotate the type here to be kind of clear we're going to get an in an in and hn when we go from um and then we're going to go back to and we're going to Compare Quality and it should be identical so this provides transformation one way or another um and it's pretty cool so for example um one of the things if I have time um is I implemented like a very small chunk of like automatic uh like SQL deriving so like you could just say hey I want a create statement for user and it will just spit out SQL for you um and it's done all generically so any case class Works um it's just like the as example that I showed a little bit earlier about the casting again it's completely generic you just provide an arbitrary case class and it happens um so applying it um this might have seemed more esoteric but again the idea is to get kind of the wisdom um of it is that we can build bunch of cool things so some of the stuff that I played with and other people played with is type SQL um type Json schema uh so this static string encoding is what I've been working on lately I know spray uses it in their routing layer somewhere um and a bunch of other people do so we'll as we're getting closer to time um I think we'll we'll work on this encoding example so this is something I hacked up in the last few days uh as I thought it was really a valuable Insight I don't actually use any shapeless and implementation of this um there's a link to it at the end of my presentation um but I declare a bunch of encoding types and this is pretty much boiler plate like I declared utfa and asky and ISO 8 859 or whatever Latin one is um and I declare in a coded string and we leave the implementation out because it's really not that important store it as a bite array or something like that and convert to and from um and then I also wrote this macro which I'm putting here just um for completion sake um and this will statically assert the encoding of a string um so for example if you say hey this string is asky and then you put utf8 characters it won't compile um which is really really powerful again I don't know how much of you how many of you have had to deal with really annoying encoding issues but if you have ever dealt with encoding issues getting a runtime error somewhere when you try to concatenate two strings together or something like that that they can't be transcoded is incredibly frustrating especially when most of this information is known statically um or if not can be recovered so again I'm just going to show you the proof objects because we don't again the implementations don't actually really matter that much to us so in this case I declare a transcoding um and so I start with some initial encoding I'm going to have some result encoding um and then I provide a way a method to transform from the initial one to the result one so you can come up with some simple IDE like proofs in your head if you think about this something that satisfies this is obviously the identity right if I take something in utf8 I I can always give it back to you in utf8 um but the reason why this is a use building block is that I can start to talk about higher level operations based on this small s of code so assuming that someone has given me um uh a transcoding um oh and I think my code got clipped um this is slightly incorrect sorry um there's an missing implicit here um and so the main idea is that if I take a prefix and a suffix and a result um normally I would take these two things as arguments and then I should also have an implicit argument and and I can pull this s up code up in a second I should have an implicit argument that asks for a transcoding from the both the prefix encoding to the result and both from the suffix encoding to the result so ideally is if I want to concatenate two strings at at compile time when you ask me to concatenate two strings I'm going to search to say can I go from the the encoding of the first thing and the encoding of the second thing to a common encoding and if I can I can add them together and so this is really really powerful because now you've eliminated a whole class of bugs and things that cannot ever be uh merge like binary and utf8 for example um you will not be able to do that um and so and then on the client side if I want to demand this proof I simply just do this thing so I say this is actually the implementation of concat like the one you would type in um and this one says hey there's two encodings um I'm going to take two the two encoded strings you're going to give me proof that I can cat them and if so I'm just going to invoke that functionality and again this shows how simple it is to depend on these things while being ignorant of their implementation um and so I think we still have a few more minutes so I have another extended example so one of the things that I was work when I was working on the SQL stuff is um proving that one H list is a subset of another H list um and you might ask all right is this a useful proof but for example um miles has now come up with this cool thing of Singleton types so for example this ID field now has a unique type so ID the string can be typed different than the the field bogus field um or age or whatever um and this is powerful because then then if I can take like this list of updates for example convert them into a list with precise typing on all of them and then I can ask if they're a subtype of the ones that exist so for example user if we see above has five Fields if I ask for that thing to be converted into um a representation that is the the keys and the values as pairs um and I ask if this set that I want to update are are a subset of that I can now statically assert whether I'm allowed to do an update which is kind of cool if I throw a bogus field in there for example the will reject me and not let me pass so we look at the up drill down into the update example this what I was talking about um and we can then look at the proof so again we declare relationship on types in this case we want one thing to be a um sorry one thing is our subsequence one thing is our super sequence or like um encompassing sequence um and then we encode a set of proofs this is this is a low priority one where we essentially um skip an element and I'm running short on time so I think I'm just going to fast forward word uh so this is like the main the the main one of interest but mostly again I'm just doing the programming instead of matching at the type level I'm programming the unifier to get it to do kind of things that I want so in this case um I need uh this is actually this skipped this SL ahead um so this is a simple case right um when I want to provide a proof that h n is a subset of hn right this is really dumb if I if you ask me a proof of that I can simply just provide you one right the more complicated one is this one where I'm actually going to do computation at this level um and here I for example I take um I want to prove that H and Sh are equal then I want to I need to proof that t is a subsequence of St and then I just then if so I provide you a proof that the whole list is in fact a subsequence of the the the combined list um and it again really looks um it's hard to read the style but it's pretty mechanical and once you get used to it it's easy to transform um and also you get a lot of power so here's a few links um where all my code is and I'll uh in the GitHub repository I think I've pushed everything um I'll probably be polishing some of the code up over the next few days um feel free to bug me on Twitter or email or whatever always happy to help on this kind of stuff um and then acknowledgements I just want to thank miles obviously for working on shapeless is pretty cool it's been fun interesting way of seeing what's possible in Scola um my lab for hosting a practice talk uh and then Adel bird and Pete for uh giving me some notes on my slides um and then questions oh yeah