Embedded Logic Programming in Scala

scala.bythebay.io: Stewart Stewart, Embedded Logic Programming in Scala

Recording: scala.bythebay.io: Stewart Stewart, Embedded Logic Programming in Scala

I you right hello everyone thank you for coming to my talk well we'll be having a bit of fun here but it's gonna go pretty fast let's let's get started my name is Stuart Stuart I work for I work for this company driver might have noticed we are sponsoring yeah so it's so here's a website you could visit on driver XYZ basically impacts what we're doing is a you know we we analyze tumors and we take the DNA RNA protein information use that to match patients with personalized cancer therapies right so target therapies are specific to their disease and ultimately we're you know we're building a platform that educates them about their disease and connects them with you know real therapies that extend their lives so yeah fun exciting stuff so yeah check that out when you have a moment great so who this 1024 x 768 let me figure this out okay so who likes who likes logic puzzles yeah oh just like 10 people here really this is a okay yeah I'll believe you all liked puzzles cuz your programmers yeah so I like I like logic puzzles um this is a this is a reference to a well-known one real quickly who can who can tell me what happens if you actually ask that question journey I mean so they both you know assuming a bad boy always lies and they'd always they both say yes I'm a good boy so the solution to this I'll let you dwell on it but you'd ask what would you say if I asked you who's a good boy or a fast you if you're a good boy anyway so I'm talking today about logic programming in in Scala so this track is called functional programming we're going to ignore that today in fact i'm also going to throw out type safety and this whole talk its secretly about closure and lisp and all that stuff so it's against the whole it sheep's clothing here all right um so yeah what is what is a logic programming this is a programming paradigm you know an alternative or you know sibling of functional programming where it's declarative and you program by writing constraints and enrolls right so you'll state facts like say a or b must be true or if c is true then d is also true at the same time and you just build a question these facts and then you let the runtime take those packs and give you a solution so you program by asking questions or you know by basically translating a questions directly into code yeah so it's a very declarative high level you know you're using first-order logic to to encode to encode knowledge and code your program and like the runtime solve it for you great so specifically we're talking about mini can rent which is a relational programming language so in a relational programming language you're working with relations as opposed to functions so a function has inputs and outputs so a function add might take two inputs and return and return some sort of output so in a relation in the relational version of add here we have we have three three things there we're not specify ignore the weather their inputs or outputs and we can we can do things like this so we can we can say given that three plus a is seven what is a right so normally we'd only be able to so we would give three and four and ask for the output seven right here we can we can give whatever those you want and then see if not put comes from a so that's a that's a relation and that's what we'll be working with today so Minnie can ran appeared first in 2005 the book The Regent schemer you know to descend into the little whisper and that whole series it was originally imbedded in scheme and it was it was it's more of a research language made to to explore pure relational programming so you know relational programming or logic programming without without impure operators cuts and and so forth and you know there's there's fascinating things happening in this area have researched this world but we're not going to talk about that we're going to go talk about you know fun stuff and solving puzzles with it so okay so I'm just going to go quickly over the basics of a mini-camera so first thing we have here is our unification so this gives you some variable here we're saying so given some Q we're saying that Q must equals 3 so this thing here returns a goal or this is a constraint so when you run that constraint then you get you get all possible solutions for Q and in this case you're only possible solution is three right makes sense yeah that's straightforward cool here is a disjunction so either q is equal to three or q is equal to four so if we run that we get a list of three four these are the possible solutions for Q in a sense in a sense we'll get there so next one here so here's a conjunction so here we're asking is our solution for q where q is equal to three and q is equal to four so what might you expect this to be empty yeah empty list cool so we run that and we get an empty list like like predicted so yeah fairly straightforward and we're getting more interesting here we have a did someone have a question okay yeah gain more interest in here we have this unification so that's this part right here we're saying q cannot bind to three so this is you know the almost the opposite of unification there are some caveats so here I'm saying q is three or q is for but also q can't be three so in that case there's only one possible solution for Q and that would be for ya okay everyone seems to be nodding with me cool um just a few more basics so here's a failing goal no matter what value of Q you'll get yeah well you won't get an answer so if you run that you get an empty list yeah and here's a succeeding goal so this says no matter what value of Q you have it will succeed your goal just succeeds um so what might the answer be for this one everything right so yes so if we print that we're going to see this underscore 0 so this is the value for Q what so what actually happened here is that Q didn't bind to anything there was no solution I mean it absolutely anything could be the value for cute so all we have is that there's this unbound variable and we just give it a name underscore 0 but you know note that that's distinct from in the failed case this is an empty list and this is a list of you know empty variables okay so like if i were to i am with this with this function i could also introduce multiple variables so q r s t if i were to run that i get i get a four tuple of these of these four variables and they've all been named underscore 0 1 2 & 3 I'm just naming them as they go all of them unbound right so next one here if we if we were to unify to those unbound logic variables so if we it is exactly the same thing except now we have that q is the same t so if we run that now this gets a little bit more interesting we have 0 1 to 0 so it knows that all of these are inbound but it also knows that these two are the same unbound variable they're all other both zero yeah cool let's see I have this keyword here exists that lets me you know in a sub-goal create new variables so you know running that you get 0 1 2 and this there's this all helper that says all of those things must be true together there's also this any oops and he says any of those goals might be true be sure to run that you get three possible solutions right Q R or s has a value for this Q and yeah that that's it with basic so was that clear to everyone we're we're feeling pretty good about it okay I'm seeing a lot nodding so we'll we'll go ahead and start to use that so here I have a definition of a pen this takes two lists and cat and concatenate some so let's a less be returns a list this isn't this isn't you know normally I guess how you might like to define this in your own code I have it this way for a reason so let's go of it very quickly you know if the first list is empty we can just return the second one otherwise we pattern match on that list we you know we D structure and take the first element and then we take that element and bind it recursively to you know well so we append the tail to the second list and then bind that recursively yeah so it's a it's a typical recursive definition so going to so I have it here and what I'm going to do here is translate that append function in to append oh so as a convention relations are just named like their functional counterparts but with an O at the end so I'm just following in the spirit of that so great already you can see a pen has two inputs and an output here we have three three inputs and you know the return type here is a goal or a constraint great so I'm going to translate that if now any of two cases can be true right so in that first case we have that la is empty and when that's true it's also true that out is the same as lb ok straightforward so in that second case we have to introduce a few variables so i'm going to say exists there exists some a and a s and weaken the structure la so a cons onto a s is the same as la and actually I'm gonna put all here because all of these can things need to be true together ok so a onto a s is LA and then we have a recursive call so append oh and what we have so a s lb is Rick let me introduce that variable actually right there we go and then we have that the out is equal to a cons on to wreak great so you know those two those two look very similar it's and for the most part like translating functional to relational is it's not is not not too difficult they're the edge cases here but it gets tricky there's one well there's here's an edge case I'm going to take this and I'm going to change the order of these two because a pendo is a recursive relation in the conjunction I mean you just wanna put them at the end so you don't stack overflow but that's that's something you kind of learn over time all right so we had that definition let's let's try to let's try to work with it let me just run these okay so here I'm just going to demonstrate the functional append so start is 125 and is 6 through 10 and if you append you get the full list 1 through 10 so like expected well we can do that in relations to so here's a pen doe start end and then our variable well I've been calling q earlier it's just an underscore now our variable is what we're going to print so let's let's run that and yes we get the list 1 through 10 so we're using it just like a function but since this is a relation we can write backwards to write so i'm gonna i'm going to this time i'm gonna specify the output and say there's a full list of 1 to 10 and we don't know what start and end our right so let's let's run that and see what happens and now this is a lot more interesting right so you have a you have a all possible solutions of you know to list that can combine to make the third list you know one through four and six through ten so forth yeah and it gets even more interesting so here it's a bit complicated but just take my word for it that this is a this is saying that's for some list cube we're getting we have that queue starts with one through five and ends with six through ten so this will start generating all those lists if you're to run it yes the cost of the calculation um yeah okay so in my particular implementation so this is a this is you know a fairly green project in my particular implementation it's it's it's slow not performing but this is a the this this the system as a whole is its complexity is better than say brute force comet oriole complexity right because as its as its searching through the through through the solution tree it's true it's pruning off all those wrong answers right it's checking those constraints as it rates over recursively through the tree so it's better complexity I mean it's never gonna be as nice as the ads hand to dalga written so you wouldn't do this necessarily for performance but you'd do it so that you can write something that's concise that you know was correct you know easy to verify and it's more for exploratory stuff right I'll get onto more to use cases later on but yes so here here this is interesting because this is a this is an infinite solution now or this this is an image solution space so if you run that we get the first obvious one right so one through ten and we have all of these these longer and longer lists and they have these these unbound variables in the middle so underscore 0 1 2 3 we don't know anything about these except that they exist in the middle of the list and their distinct from each other or possibly distinct from each other right and they're certainly not the same variable cool so that lets you know that's a quick briefing on like the difference between a function in relation so let's let's try it out somewhere oh so that doesn't print too well I'm going to okay no I could do more great just to forgive me for all right so let's do that reload this slide it's gonna be okay there we go cool so it's hacky I know so here's a here's a classic puzzle found it in and the sick be classic functional programming book I'm also Lisp mary i morris father has yacht and so as each of his four friends and then each of his friends has named their yacht after a daughter of one of the other friends so now we were given all these facts we're giving our names were given you know the barnacles yacht is the Gabriella mr. moomer Owens Lorna the Melissa owned by criminal down and is named after Sir barnacles daughter and so forth so we take all these facts and given that we have to figure out who is Lauren's father great so right now I could a solution to that I've already set it up a little bit so let's see what do we have great side my list of fathers and I right now I'm only asking this one question you know start who is Lauren's father so I have to help of functions sires this says a father you know sired the daughter and owns this boat here so I I do that by saying that the position of F and fathers is the same as a position of d and daughters and you know this is a this is plain skala I'm defining functions inside of a I'm defining helper functions inside of my relation here or inside of the inside this whole goal and you know binding to you know closing over daughters and yachts which these at this point we don't know anything about them they're both they're both just logic variables that we introduced in and here so already running sires we know a few things about this so here I have it running and just printing constantly on every compile so here on the left hand we have potential fathers on the right hand we have two lists we have the list of the list of daughters in order and then the list of boats in order right now it doesn't even know that the books are lists right so you get the underscore one here if more were the father Lorna would be positioned one in the list right and then so forth if Barker birth father should be the fifth decision you'll notice that it doesn't even know that that the list terminates at five elements so it says you know content on 24 there might be something that follows that we don't know yet great so let's start let's start feeding that with facts and see what we can learn um let's see we don't have a lot of room here I'm just mess back and forth okay so Marianne Moore's father so we can see the already Mary you've learned more Mary there we go so let's look at that real quickly so more was first in the list so now Mary is there you'll notice the we only have four four sets of solutions now right Lorna can no longer populate the first element of this list so let's keep going so Mary animals father has a yacht and so has each of his friends okay so let's let's include that by saying there are the same number of shots as they're our fathers so there's a yacht / father great ok so we learned that yachts is a list of five elements of some sort okay let's keep going each has named his yacht after one of the other daughters okay so uh let's see I had this permute Oh goal here so I'll say that yachts is the some permutation of daughters or either way and great so now we're getting many more possibilities we're getting like a all these 01 in different possible orders and so forth and we now know that there are only five daughters right so we're learning more and more to go let's let's keep going back to the problem okay so sure I could I'm going to do this okay so sir barnacles yacht is Gabrielle so owns barnacle owns the Gabrielle morons alarna whoops more understood hmm long where'd that come from autocomplete love it yeah all right there we go we're on to Lorna hall owns the Rosalind okay so I'll keep doing that Hall phone see Rosalind okay um have a pair well with that okay Melissa owned by downing okay so own downing the Melissa the Millstone by downing is named after Sir barnacles daughter so let's put that in there too so this is now sires sires yeah you there we go let's see how we're doing cool so you've been we've been learning all these facts mmm that's not that's ok uh let's just you run that okay there we go so yeah we've learned by now we've learned the names of all the daughters and there are three potential fathers for Lorna it's downing hall or Parker right and for each of those are two different orderings of boats and daughters great so let's just keep looking at this um a final goal we have Gabriel's father owns the yacht that's named after dr. Parker's daughter all right let's see if we can tackle that so if we have a okay so we have Gabriel's father I'm going to create a variable for that so we have a garrulous father and Parker's daughter okay so a few things are true let's let's make sure we know who Gabriel's father is so sires Gabrielle spotters yours Gabrielle and then Parker sires Parker's daughter and what else what's it say it said owns the yacht that is named okay so g/f owns the yacht that has named ash brokerage daughter so Parker's daughter's name Great Khan there we go so let's run that that's all of the I think that's all of the constraints laid out in a problem so when we go back to the repple hopefully we'll see who the father is yeah and okay yeah so great we have that downing as a father and you have all these there's only one order all these in order so we have more more as a father of Mary and owned Lorna so forth hmm Rosalyn where's ruolan okay this fifth one must have been downing and owns a merry tada all right okay so yeah so why am I doing this Oh actually they there are many more puzzles we don't have time to get through this one but this is also fun so I'll at least give you a problem statement and leave that to your imagination so there there schoolgirls I I guess presumably at a boarding school their parents are really you know they they I supposed to say ask too much I'll just read the prompt statement how does it say they show an undue degree of interest in a result they therefore agreed that in writing home about the examination each gold make one true statement and one untrue one so these are the passages from editor from their letters you know Betty says kitty was second in the examination as only third Joanne says I was third and eighth was bottom and so forth you have all these one line one truth and from all those you're supposed to figure out like what was the actual order who and you know who who did best who you know who has the best daughter or something like that but let's get that for now but you know I'll tell you can do that with this equality constraints and having having the ends and the oars but yeah so why am I am I telling you all about logic programming well why might you do it in the first place so what what was nice about the solution right here this here is concise it's what 12 14 lines of code yeah 13 lines of code yeah and you can look at that and you can say ok if each of those you know resuming each of those like helper functions that it was built off of were defined correctly then that's that solution there is probably correct right i mean the the it's pretty unlikely i made a mistake while translating that the problem definition so it's it's it's concise it's easy to verify i did not have to write my own search strategy so I didn't have to say you know let's iterate over these and on each iteration want to check these a constraint you know I'd not to think about that and I mean it's it's still it's still technically you know it's it's better complexity than then comet Oriole yeah it's not brute force and it's it's it's good enough to use for exploration and and and well other things so let's say let's say let me go back to slides yeah and you can use alongside scholar so if you want to use prologue maybe you would have had to write strings and then I don't know do something like slick does right have it translate and run in some other runtime or do some foreign function interface so this is this embedded it's it's it's small and easy to embed so it was not if not too difficult to implement this like 200 lines so far and what would you use this for okay yeah yeah three minutes you'd use this for things like scheduling layout constraints you can use for type inference so if you're to write a relational type checker so remember these can run back or backwards if you were to write a relational type checker then it's also a type in furniture or a type in habiter right the relation theme theory improver can also generate proofs and theorems a relational sudoku solver can also generate Sudoku puzzles yeah or you could do like partially solved and you know you can just explore the whole problem space it's quite fun ah yeah so just solving generating exploring what else and why so this is also fun because it's it's it's fun to make this so like if you're a person who's in two languages different fathers whatnot you can this is this is a this is very small you can read you can read the papers say there's a there's a micro can rent which is which is just the kind of core of mini can run it's a it's an easy five page paper you know each other I just in a lot of academic papers and you can go from there and there there are many different ways that this is an extended so it you know taking all those papers and implanting them is is it's fun so you might you know be interest helping me for that or whatever great so what's gonna happen next after this you might go add more constraints besides the disequilibrium and which is a you know saying a variable belongs to arrange and then I can do some basic arithmetic nominal logic programming lets you bind names to values of course user interface macros pattern matching of course the back end of it could use improvement and and this would be really cool is the unification of arbitrary case classes and H lists and being able to you know unify the case class that you're creating in Scala and and and generate possible values of those yeah and of course yeah type safety I didn't mention I was throwing out type safety earlier today right so I mean if you're actually so the term you are seeing earlier in the repple is right now it's Navy us for any and it's actually quite tricky it gets very verbose to do it type safe because you now have lists of either bounder and bound variables and to unify recursively gets gets gets you know very verbose and tricky and then you need to have you need to have a polymorphic map for storing variables and so forth in but that's another interesting implementation challenge you might like to help with yes all the possible I mean it's a stream of terms right so it's it's a stream of any thing um okay enumerations ready so so these things are interleaving so like that any constraints checks each of these in order and I guess sometimes you have to be clever about how you order these goals anyway I think I have time so I I'll leave out questions huh yeah yeah so um yeah that's it i'll i'll be posting more about this later shoutouts to those things thanks everyone no time for questions that there's contacts and so all right thank you [Applause]