SBTB 2015: Adam Pingel, An overview of Axle: a Scala-embedded DSL
Recording: SBTB 2015: Adam Pingel, An overview of Axle: a Scala-embedded DSL
just waiting to connect the laptop to the screen may take a minute see but I can I can get going so I'm going to talk about my project called axle which has been on github since sometime early 2011 published just artifacts to sonu type I think about two and a half years ago the main the main goal of the project to the in priority order are to have a diverse set of algorithms that cover a lot of different domains so examples are bio informatics natural language processing machine learning and then to be able to run those things on a diverse number of platforms so of course it has to run on the JVM being written in Scala but I'd like to be able to run these things on spark on GPUs someday on different linear algebra libraries that's what i mean by platform great and then the next the next goal is to have these things really well documented i think this has been discussed a lot in the scala community especially in the last year the the way I'm approaching that is I've got a hand-rolled documentation tool and I published those examples to axel axel dashlane org and the idea is that every code snippet you can take and cut and paste into a rebel and it should work sorry I guess there's few more goals here of course we want it to be correct the code coverage is still ongoing a little more work to do there and then these next three are definitely haven't really gotten to those just yet I mean the stuff that's documented is complete and works but there's a lot of code in there that sort of partially implemented a lot of triple question marks for the most part I'm counting on the platform to give me a speed and then I want to supply enough sample data sets in the project to to make the the examples work so example of that is the irises data set that gets used for for clustering algorithms just to get this out of the way there's there's also some visualizations the work well enough to sort of help me you write the rest of the code that I'm working on those have been around for a few years initially they were all for java.awt couple months ago I added some SVG visualizations here we just have a time series of some random data so I've got way more content than I can cover but I'm hoping to at least sort of give one story here in the first 10 minutes and that is sort of the the relationship between property based testing and precision and this is the old Reese's Peanut Butter Cup commercial two great tastes that taste great together the commercial is even more ridiculous than I remember these two guys or these two people are walking around on the sidewalk with headphones on they bump into each other one is for some reason eating a tub of peanut butter and the other is eating some chocolate and they invent a new a new candy so it's about precision and and the jvm we've all been in this situation at point 1 2.1 we get point to add another one and we get this this imprecision we've learned this early on in our in our careers we know how to deal with it but i just want to remind people how how jarring this is for new programmers to encounter that you have to explain this kind of stuff that there are 11 bits for an exponent and 52 for the mantissa and then maybe you have to start talking about an arithmetic logic unit and really that the wheels come off pretty quickly so I be nice to avoid that so I'm going to give an example here of a metric space so this project axle is built on spire I went to a couple talks at any Scala two and a half years ago where Eric and tom were introducing the project and I just caught my imagination I said this you know I really want to spend some time experimenting with what it's like to build software on top of this thing so this is a metric space metric space is one of the many type classes provided by spire and this is just the definition from Wikipedia so there are a few axioms therefore axioms on wikipedia that define the metrics based behavior it turns out the first one can be deduced from the from the last three and those are identity so if the distance between any two points is 0 then this two points must be the same point and end vice versa and symmetry so point from A to B the distance is the same as from B to a and then we have the triangle inequality so go the going through a detour can only increase the distance between two points and it turns out those are those are those appear in a very similar form in the metric space laws inspire so that's the sort of comforting to know that we can translate between this mathematical notation and and these scholar check properties and typically we think of the first example of a metric space we think of is points on the real plane and this is again just from a Wikipedia illustration of the triangle inequality but we can the metric spaces exist for other kinds of types so an example is the the Levenstein edit distance which is a string metric so you can this is two examples one of the distance between kitten and sitting and the other example is the distance between Saturday and Sunday and you can see it in both cases if you read the number on the bottom right it's three meaning that there are three edits required to go from one word to the other in both of these cases and the way this is a dynamic program you sort of the algorithm starts at the upper left and it fills into the lower right and the number at the lower right is the answer so you can actually write that as a distance as a metric space and you can use some aspires syntactic sugar to get this in fixed distance operator so we can say the distance between the quick brown fox and the quick brown fox with the missing see is two edits and we can test it as such so we can throw a bunch of random strings and see that all three of these axioms hold now random strings may not be the best input they're not not going to be representative the cuts and things that you're going to be measuring distances from so that's a possible improvement but it's at least nice to know that this passes so a newer example that I've played with is geo coordinates so here i show that i'll show a metrics based on the but there's also here I'm showing that a geo coordinates is basically a pair a latitude and longitude and each of those things is is an angle has to be an angle so this thing called the unit United quantity which is just a case class enforces that anything you pass to it must be an angle so it can be a degree it can be a Radian it doesn't matter it'll work but you can't pass to at a distance or a time so you get that kind of check at compile-time and then this this number type parameter has been abstracted out so i'll show some examples using both doubles and reels engine just to remind folks if you haven't seen this or taken you know long flights this is an illustration that the triangle inequality holds for these coordinates the the path on the top is from SFO to the Helsinki Airport you can see it goes over Greenland and then the other path is is service just go to Helsinki via Miami and just sort of visually it looks like they're about the same but in fact the lower path is a couple thousand miles longer and in fact the Miami to Helsinki is about the same it's a little bit shorter than SFO to Helsinki so there's a there's a formula you can you can get just google for this great circle distance and it it's you find on the internet as some navigation sites have these kinds of things and it's really just a bunch of trigonometry and you can see that in this case I'm the distance returned is also an angle so it'll it'll be in radians but we can you can convert it to degrees if that's if that's more convenient and then there's also utility function to convert that to a distance by multiple multiplying it by the Earth's radius if that's what you want which often is the case so I wrote this thing up and tried to test it as a metric space and the test didn't pass symmetry didn't hold and it Scala check as it does provided a nice counter example and it said yeah these two I don't know where these are on the globe but these two coordinates show that symmetry fails and I sure enough I fired up a rebel and the distance from one from the first one to the second one is that number of radians on that line and then in Reverse it's almost exactly the same number but it's just a little bit different it's it's different enough that the test fails that that turns out to be something like a nanometer difference so for all practical purposes this does not matter but the point is that the tests fail and be nice to use these axioms and do this property testing methodology and and have everything work and you know this is apart from the fact that that the earth is not a perfect sphere anyways so you've got its it's an it's some sort of an ellipsoid and it's not even really that and you've got plate tectonics and all kinds of stuff going on and topography of the earth so yeah the point is not that this is sort of important for any practical purposes but we want these tests to pass and so I was trying to figure out how to get around this and I remembered I had been to a talk in in Portland Eric awesomes talk about spire and real numbers and I wondered if what real would do the job so it's a great slide in that talk where I showed that the oil identity works so e to the I PI plus 1 is 0 and it's it's sort of beyond the scope of this talk and beyond my Ken to to explain why that's true but it does involve Taylor series approximation if you remember from calculus class so these these formulas allow us to get as much precision as we have time to wait it's important part of the of the technique and so by simply replacing double with real the test started passing so you can see we got a lot more precision when measuring these are the same two points 1 and 2 so that you get a lot more precision but more importantly they're equal and the test pass so a related type class this is one that's an axle is a length space so a metric space tells you about the distance between points but it doesn't tell you anything about the path if you want the path you need to rely on something else and not to go over all of this fitting the important part here is this little lowercase gamma function so this gamma can take you know the number from 0 to 1 representing the portion of the way along the path you want to find the point for and we'll return the point and so the implementation looks like this again this was just something I found on some kind of a navigation website that involves a lot of trigonometry so it takes two points and returns another point or it takes two points and then a F which is that number that represents along the path and note we've got a couple different kinds of units here to some of these are onion itted coefficients others are angles and then in the end we were going to pass along coming out of the arc tangent function these these angles are measured in radians so the the coordinates that are returned if you want to consume them in degrees you can do that but that conversion will happen later by the consumer and here's just a proof that it works we're just generating you know from 0 to 10 you know by on by tenths the way points along the way so these are all actually equidistant but you can see they kind of spread out and just like the earlier slide they they arc over Greenland and so that was just a lot of fun and I this this Mars climate orbiter gets cited a lot by by the strongly typed camp and yet I think a lot of us end up writing web services and ETL processes and that kind of thing so this was fun just to sort of have a chance to to think about this this problem there's something that's a little closer to this problem and you can see here again just from Wikipedia that the the planned trajectory is the white line on top and because there was a disagreement about whether some quantities were measured in s non-si units or metric units they got something horribly wrong and the orbiter smashed into the planet on September 23rd 1999 so it's an off-site an example of where you using a type system to to capture the constraints around units and conversions can be really helpful just check on time here okay so the other interesting number type inspire there was a number of them but the the one I'm going to talk about is rational so often times the numbers that we're working with really can just be represented as fractions with whole numbers so here we have a third and below we can see that 50 over 200 is simplified to one fourth so of course that doesn't come for free but but I think in many cases the small performance hit is worth the precision so just 11 easy example taking the mean or the harmonic mean of some fractions it's it's nice to not lose precision in that operation harmonic mean is useful when you're averaging rates I'm going to skip over this one but so this is a type signature of a naive Bayes constructor see it's got a lot of type parameters point I wanted to make about it was that we evaluate these things we create performance metrics to evaluate classifiers and the most common ones are precision recall and there's some other ones specificity accuracy f1 score those are actually just sort of tally's and fractions internally that's how they're computed and so it's kind of nice to to not lose any of the precision there so recall in this particular case this is a canonical example of predicting whether or not two people go out and play tennis so in this in this case the predictions were you know 100 there was hundred percent recall meaning that everything that should have been in the query was in the query results set and and then precision is everything that was in the results that should have been in the result set so you could maybe make an argument that when you're displaying this sort of a metric you might want to convert it to double because they're more easily comparable just you can visually inspect them but at least internally it's nice to represent these things as rationals same thing is true for a joint probability table again this is sort of a canonical example from Asian Network literature of five variables there's an an earthquake may or may not happen a burglary may or may not happen and then there's an alarm which which may or may not go off and it can even just spontaneously go off and then there are two people John and Mary which may or may not call the police or the fire department and you can see one of these this is sort of in a lighted example here but the odds are one in 20 billion that both an earthquake and the burglary happened but the alarm doesn't go off and yet John and Mary both call the police it's pretty outlandish but it's sort of nice to capture exactly how you know how frequently that might happen and then summing out all of the variables from this joint probability table to get one to get exactly one is really nice yeah another example of where fractions come in handy is in calculating odds and games so here I'm calculating the odds of snake eyes so the this die is basically just a uniform distribution on the numbers from one to six and I've got this little bit of syntactic sugar that make it look like probability notations so the odds that the first one is one and and the second one is one there's nothing suits too sophisticated going on there but but it's nice that the answer comes out as 136th I think as a double that's something like point zero two seven seven etc it's not something I would recognize whereas if we write it as 1 36 it that's more obviously correct to me so I think there's even like a user interface argument for using fractions and rational numbers and another dice example is to you know throw two dice add them and calculate the distribution so here we all know seven is the most common number when you need total two dice throne there's only one way to get to and there's only one way to get 12 so you see this nicely formed triangle the nice thing about computing it with this distribution Mont at is is these numbers are precise we could do 10,000 see me you can simulate 10,000 rolls and get a distribution looks a lot like this but it's nice to have the exact numbers in many situations so you know this is a little more forward looking with the project but how many people are familiar with the Monty Hall problem okay so it's a majority solid majority there okay so it's been too much time on this but you know this how many people are familiar with this the sort of scandal around it 25 years ago with the the parade ok coy so there was a there was a woman who wrote for Parade magazine reader had written in a task about the Monty Hall problem so the reader asked you know should I change my decision you know I've and just to recap there's a car behind one of these doors the contestant pics 1 Monty Hall reveals one of the other doors and there's a goat behind it and offers the contestant a chance to switch should the contestants which the answer is yes but that's it's really counterintuitive so explaining this is notoriously challenging and this woman from Parade magazine wrote it up had the right answer but these thousands of people wrote in just blasting her many of them with sexist comments but in the end she was vindicated it was a good story so I wanted to take a crack at this given what i had done with Axl and here's the the closest I could get which is this outcome function is a function from the probability of switching to to the distribution of boolean's which indicate whether or not the car was one and then I can create a just a chance of winning given a given that probability as a single number and then I can make these two assertions and these assertions pass right now so I can say that the chance of winning given that the contestant always switches is one-half the chance of winning given that the that the contestant always sticks with the original choice is one-third so that's probably enough to convince most people that that's the right strategy but it's not a proof and so I think looking forward with the project I'd like to I'd like to spend some time generalizing this making this more declarative making this less ad hoc and work for for general purpose games and this is particularly interesting because it's unlike chess and checkers that there's imperfect information here so the the agents have have different views of what reality is that's what makes it especially hard and so sort of wrap up with a couple of really dense slides I think one of the ways to about this it can be found in this this paper it was presented in pople 2002 by Ramsey and pfeffer that described a stochastic lambda calculus and the mountains of probability distributions so this is like a way of baking in distributions not only into values but into all the above the branching logic of a program and I you know haven't really parsed this and rocked all of this but it's something I'd like to do in the in the next year if anybody's interested in collaborating on that it would be I'd be very interesting hear about that and then in that same paper they present this this wall of notation measure terms which is a more efficient way of calculating the same thing so this I suspect that a lot of this stuff exists in a already in a project called Figaro which was written by by avi pfeffer want to take a closer look at that but I think just sort of the the idea of taking spires abstractions and number types and bringing them to some of these other algorithms these other libraries I think can kind of unlock if nothing else at least more thorough test coverage but I also think it's it's a little bit enlightening to see how the precision of these numbers interact with the semantics of the of the algorithms themselves so I'll leave it at that and I would love to hear from you if your alleged in this I just published a new version of this a few nights ago it's up on the source codes on github and the artifacts are on sonatype and yeah as a Lexie mention on now heading into a new job in a few weeks as vp of engineering a travel so we'd hopefully doing a lot of hiring soon so if your interests in that let me know so yeah thanks any questions I don't know if we have much time but no no that was not their distributions yeah there that's all axel could yeah yeah this this does exist in the source code on github you can find this example it runs every time I come in a change yeah yeah in the questions so as I'll turn it over cool well thank you