Future of Coding - Joining Logic, Relational, and Functional Programming: Michael Arntzenius

Episode Date: June 13, 2019

This episode explores the intersections between various flavors of math and programming, and the ways in which they can be mixed, matched, and combined. Michael Arntzenius, "rntz" for short, is a PhD student at the University of Birmingham building a programming language that combines some of the best features of logic, relational, and functional programming. The goal of the project is "to find a sweet spot of something that is more powerful than Datalog, but still constrained enough that we can apply existing optimizations to it and imitate what has been done in the database community and the Datalog community." The challenge is combining the key part of Datalog (simple relational computations without worrying too much underlying representations) and of functional programming (being able to abstract out repeated patterns) in a way that is reasonably performant. This is a wide-ranging conversation including: Lisp macros, FRP, Eve, miniKanren, decidability, computability, higher-order logics and their correspondence to higher-order types, lattices, partial orders, avoiding logical paradoxes by disallowing negation (or requiring monotonicity) in self reference (or recursion), modal logic, CRDTS (which are semi-lattices), and the place for formalism is programming. This was a great opportunity for me to brush up on (or learn for the first time) some useful mathematical and type theory key words. Hope you get a lot out of it as well -- enjoy! The transcript for this episode was sponsored by Repl.it and can be found at https://futureofcoding.org/episodes/040#full-transcriptSupport us on Patreon: https://www.patreon.com/futureofcodingSee omnystudio.com/listener for privacy information.

Hello, and welcome to the Future of Coding. This is Steve Krause. So this episode of the podcast explores the intersections between various flavors of mathematics and programming, and the ways in which they can be mixed, matched, and combined. Michael, or RNTZ, pronounced Ernst for short, is a PhD student at the University of Birmingham, building a programming language that combines some of the best features of logic, relational, and functional programming. The goal of the project is to find a sweet spot between something more powerful than Datalog, but still constrained enough that they can use existing optimizations from the literature on database optimizations to make it fast enough to be like a query engine, but also include some of the features of functional programming.

So yeah, the key is to not include all the features of a functional programming language, because then it's hard to apply those query optimizations. So yeah, we get into all those details in the conversation. So this is a very wide ranging conversation. We talked about Lisp macros, FRP, EVE, which is actually where he found out about Datalog in the first place, which is really funny. Decidability, computability, higher order logics and their correspondence to higher order types, lattices, partial orders, avoiding logical paradoxes by disallowing negation or requiring monotonicity, which is kind of the same thing as disallowing negation, but only you need to do that in case of self-reference or recursion. And he does this

with modal logics. We talk about CRDTs a bit, which are semi-lattices, which he explained earlier. For those of us like me who need to brush up or learn for the first time some of these mathematical and type theory concepts. So anyways, this was a long, really interesting, rich conversation, and I got a lot out of it, and I hope you do too. Now a message from our sponsor. Repl.it is an online REPL for over 30 languages. It started out as a code playground, but now it scales up to a full development environment where you can do everything from deploying web servers to training ML models, all driven by the REPL. They're a small startup in San Francisco, but they reach millions of programmers, students, and teachers all over the world.

They're looking for hackers interested in the future of coding and making software tools more accessible and enjoyable. So email jobs at REPL.it if you're interested in learning more. And without any further ado, here is Ernst. So welcome, Michael. Hello. So you go by Michael, yeah? Yeah. Because your online username is RNTZ?

Yes, Ernst. And that's how it's pronounced, Ernst? That's how it's pronounced, Ernst. And where did you go to undergrad? Carnegie Mellon. And you studied CS? Yeah, computer science. And so when did you get into programming languages specifically in computer science? Very shortly after I got into programming. Oh, interesting. So I think the thing that I sort of vaguely wanted to do when I started programming was make video games.

Which I think is a common one. Yeah. But I sort of very quickly got frustrated with the tools available to me, right? And started bouncing through programming languages. I think the programming language did I start with? Might have been Python, might have been Visual Basic, might have been... I don't even remember now. But anyway, I eventually found my way to Lisp and to Scheme and that was really sort of a revelation. I really enjoyed Lisp and Scheme.

And I just sort of started going down the building tools for making your own tools rabbit hole. Because any time I would try to do something concrete I would get frustrated that it was hard and I would think how could I make it easier to do this thing. And start thinking about building a tool for that thing. And if you keep doing that you end up at programming languages. And I've been going down that rabbit hole for, I guess, more than a decade now. You just never stopped yak shaving. Yeah. Yeah, sort of.

I've, like, narrowed my scope a lot, right? Which academia will do to you, right? Like, you have to focus if you're going to get anything done. Yep, yep, well said. So I find that a lot of us go through various paradigms and topics like block space programming or structured editors or logic programming or functional programming, you know, databases, you know. There are like a bunch of different ways to improve programming.

What was your arc through all those topics, or was it not as windy? Did you kind of know early on? No, I mean, there's been some ramblings. I mean, so the first place I embarked with was Lisp and Scheme, right? Which is sort of... It's a common starting place for programming languages people. Right, and Lisp and Scheme have sort of a couple of interesting ideas in them that have stayed with me. I mean, Lisp, when it first came out, had dozens of ideas that other languages didn't have, like garbage collection.

But nowadays, garbage collection is really common. So garbage collection didn't leave a lasting impact on me, other than that, like, yeah, I don't like having to manually memorize memory. But that's a soul, you know, we know how to do that now. But the things that are even now not entirely mainstream about it are S-expressions and using S-expressions to represent all of your data, right, or most of your data. Functional programming, that's obviously getting much more traction nowadays, but it's still not entirely mainstream. I don't know, I guess it depends on who you ask. And macros. And sort of early on, the one that seemed most exciting to me and most cool was macros.

Yeah, I guess it goes hand-in-hand with the S expressions thing. I guess it's almost less the S expressions and more the homo-iconicity. That's another phrase that I... You don't like the phrase? Well, I find it kind of ambiguous. People make a big deal out of it, but they can never define exactly what counts as being homo-iconic. The thing that I think is important is it has a built-in data structure for representing the syntax of your language. But that's not unique to it. Python also has this. Most people don't know it, but Python has an AST

data type in the standard library. Oh wow. But also this data type is S expressions, is the data, is sort of the thing you use to represent almost everything, right? It's not a special purpose data type, S expressions. You use its building blocks everywhere else. You use lists, you use symbols, you use numbers, right? It's not a special purpose data type, S-expressions. You use its building blocks everywhere else. You use lists, you use symbols, you use numbers, right? And you know, in Python, if I want to understand the AST, I have to go read the documentation specifically for the AST. In Lisp, I'm already, you know, there's very little distance between the tools that you familiarize yourself with for general programming and the tools that you use to write macros.

Right. And so that's sort of what I think of as making macros easy or is what homoiconicity is. It's that the same data structures and concepts that you use to write ordinary code are the ones you use to write macros. There's not a huge gulf between them, which makes it really easy to get started writing macros. Yeah, that's really wellulf between them, which makes it really easy to get started writing macros. Yeah, that's really well said. I think that captures part of what's really powerful about the S expressions macros pairing. You can turn the tool on itself and use it in the same way you've been using it to do other things, but on itself. Yeah. Yeah. I guess it, um, it's quite empowering because it, it, I think it, like it's in the theme of blurring the line between a creator of a tool and a user of a tool.

Yeah, definitely. I mean, it's kind of intoxicatingly powerful, right? Like everybody gets turned on to, I don't know about everybody, but a lot of people, you know, get turned on to macros, right? And then, you know, some never stop trying to use macros to solve every problem, right? It's really fun to write a macro that gives you a little language for solving a particular problem. So right. Oh and also the other thing that's relevant, I applied to work at my dream job which was working on Eve.

Oh with Chris Granger and yeah. Chris Granger and Jamie Branson and I should remember the names of the other people who were working on it but I don't. Corey and yeah. I think Corey was after my after i applied yeah i also sent an email like i don't know if applied is the right word for like i want to work for you even in an email uh so yeah that's if we have that in common i imagine a lot of people uh yeah who listen to i imagine a lot of listeners to the podcast so i was like yeah yeah i emailed

chris too yeah well i emailed them and then they flew me out to interview oh wow okay great and then turned me down um you got farther than i did i got a i think less than a sentence of like like sorry i'm not interested we're like sorry no yeah um but talking with them was really cool and gave me a clearer idea of what they were trying to do. And part of the core technology we were building on was this Datalog-like stuff. Yep. Oh, that's where you first heard about, you first got into it? That's really where I first got interested in Datalog in relation to the program. No way.

That's fascinating. I guess I probably have already said this in the intro to the podcast, but you're really into datalog, it seems. That's what your research is about. That's a fascinating little historical tidbit that you got it from. My research direction has been determined by getting turned down from my dream job. Well, it's just so funny to think that Eve was, which just, like, feels so outside of academia. Like, they took things from academia. But, like, the fact that they were then able to, like, influence academia, I just find that somehow fascinating and wonderful.

Yeah, I mean, I think academics are more open-minded than a lot of people might think. Yeah, of course, and their reputation. Yeah, academics are just people, and like, you know. Especially grad students. Especially grad students. You get less than this a person if you get tenure. I see. I see.

I regret saying that at some point in my life. Well, I guess there's like a period in time at which you can like choose which very sliver of knowledge you're going to be an expert on and once you've like established that it's not i guess it's not you can still change but like once you've like established but it's hard right it's i guess it's kind of a sunk cost thing but it's also like or it's you're already there like you might as well just keep going yeah not totally yeah you can think of it as sunk cost or you can think of it as like you have built up an expertise in a very specific area

and it's sort of a matter of your relative advantages right you have a lot of knowledge of this area so you have a real advantage in working at starting in a new area is like starting all over yeah exactly so when when you're like a grad student it's very easy to be influenced by things but then like 10 years from now you're not going to want to like if some if the next chris granger comes up with a new company 10 years with a new direction you're like not going to switch to that thing you know it's it's like a one-time thing maybe yeah or it gets harder it gets harder yeah or less common yeah cool i've lost track of where we are um i'm curious how you it how you originally got an frp why right frp and how do you find that um i'm not i'm still obsessed with it i've been obsessed with it for years like since like since i saw react js i was obsessed with it like i was into all the front end frameworks and finally i

found connell elliott's work and then i was like ah now i'm really into it and now i'm like um like annoying because i'm like so into it and i have like nobody to talk to because i almost feel like like it was like in a like nobody or anyways the people i talk to aren't really interested in it uh the way that i am so yeah i mean i think it's sort of gained a brief moment of um uh being slightly more mainstream especially with elm right and then elm actually kind of abandoned the approach and there haven't been a lot of attempts to really push it forward since then. I mean, there's been academic work on it, but it's not in the spotlight anymore. And it was never hugely in the spotlight.

So I got interested in it more or less because I think Elm might have been part of it, exposing me to it, and it seemed like a nicer way to write user-facing programs. It still seems like it might be a nicer way to write user-facing programs, although I think my attention has turned more generally to the problem of incremental computation, which FRP, I think, is... Or dealing with change is how i would summarize the the problem is i see it of front end of front end programming right um yeah and if well i guess because like events like you know yeah you have some ui and it like mostly stays the same but as you interact with it the ui slowly changes yeah

but also the external world is changing, right? You know, you're running a website where someone has a shopping basket, right? And maybe you're trying to do it in a distributed setting. Now things can change. They can change at different places at different points in time, and you have to integrate all of that somehow. Or... That's interesting i guess because i don't i i usually make the distinction in my head between

batch programs and then reactive programs reactive programs like respond to the environment and batch programs you do some just processing once um but i guess what a reactive program is, is something that changes over time. Yeah. But it, like, it has inertia. It doesn't, like, it's not a step-functioning thing. It's like a smooth, it's usually a smooth kind of changing thing. Smooth-ish. Occasionally you'll press a button and the entire page will change.

Yeah. But usually it's like... Most changes are small. Most changes are small. Most changes are small. Maybe that doesn't make any sense. No, I mean, it makes sense. Continuity is sort of a huge theme that connects to everything

if you look into it deep enough and I don't fully understand it. Almost like differential build to be... Yeah. In a certain sense, only continuous functions are computable. There's this connection between topology and computation that I do not fully understand. I see. That's interesting.

Anyway, yeah, so I got into FRP because I was interested in it as a better or nicer model of writing UI programs. And why did I end up not so interested in it? I guess I basically got sidelined in my mind by the Datalog and Datafund and relational programming ideas. So it feels like you first got into logic programming and then got into relational programming ideas. So that's, well, so it feels like you first got into logic programming and then got into relational programming or it kind of happened at the same time? It happened at the same time. I treat them

as kind of the same. Oh, relational programming and logic programming. Yeah. Oh, they're kind of synonyms. Because to me, one feels like relational, I think, SQL databases and logic, I think, prologue. But I guess part of your thing is you want to unify them.

Well, I don't know about whether unifying them fully, but I do think of them as strongly related, right? Do most logic programmers think of them that way? I don't know. Okay. know okay um certainly will bird and uh his collaborators uh frequently refer to their work as relational programming who's will bird uh will bird is a how do i explain little bird he's an academic he's uh i think probably mostly known for minicanon, which is a relational slash logic programming language that is distinctly not Prolog. It's built in Scheme, and it's sort of notable feature. Well, there's two things I would mention. First off, there's a mini version of it called MicroKanren, which is notable for having an implementation that is like 50 lines long,

and that has been ported to every language under the sun because it has an implementation that is about 50 lines long, but it captures the essence of MiniKanren. So it's a really fun thing to play around with if you're interested in relational programming. And the interesting thing about Minicam and beyond that is that unlike Prolog, its search strategy is complete. So Prolog, if you write a particular thing, if you read it logically, specifies something. Like, let's say you write transitive closure. So you have edges in a graph, you have relation predicate edge that tells a set of two arguments that says an edge from this node to that node, and you want to find a, you want to define a predicate that gives you

reachability, that tells you there's a path from this node to that node. If you do this in the obvious way, which is just there's a path from x to y if there's an edge from x to y, and there's a path from x to z if there's a path from x to y and a path from y to z, right? It's just? It's edges but transitive. If you do this and you feed it to Prolog, it will infinite loop and generate nothing of interest. Because it'll just keep generating extra facts that you already know? Yeah, so it'll take the second clause, which is a path can be built from a concatenation of two paths, and if you ask it, hey, what are the paths, it will keep applying that second rule indefinitely.

I see. Right? Because it does a sort of depth-first search, and the tree, the search tree you've given it, it has infinite branches. I see. And, um, so this is really annoying. From a pure logic point of view, I've given you the logical definition of this, why aren't you computing it? This is the promise of logic programming discarded for the sake of a simple implementation. Okay.

And many counter is like, no, we will not discard that promise. We give a complete search strategy. If you give us some rules, we will give you eventually all of their consequences. No matter how you order the rules, no matter what you do, we will eventually find all the consequences of these rules. And they're able to do this because... They changed the search strategy. Oh, so just an implementation detail.

Well... Like they didn't restrict the way you could... There are a couple of features in Prologue that are specifically about the search strategy and are about sort of extra logical things. So, for example, there is the cut operator, the bang operator that prevents backtracking. That's about the search strategy. It prevents backtracking. Wait, this is in mini Cameron. No, cut is in prologue.

I see. It is not in mini Cameron. So mini Cameron is almost like higher level. It wouldn't let you. Yeah, it would not let you do this. Explain the search, like direct the search strategy. That's not entirely true. The order in which you put things will affect the order in which the tree gets searched, but it will eventually find... search the whole tree. How will it know when to stop?

In a way that Prologue doesn't know when to stop. So if you give it an infinite search tree, it will never stop. Oh. But if you give Prologue an infinite search tree, it will never stop. Oh, mini-cadron. But if you give Prolog an infinite search tree, it might never stop and also not explore the whole tree. Oh. Right? So it might just get stuck going down one particular branch of the tree and never come back up.

Whereas mini-cadron is more like doing, it's not doing a breadth first search, but it's doing something more similar to a breadth first search where eventually it will reach any node in the tree. Oh, but it might keep going forever. But it might keep going forever if the tree is infinite. Yeah, that's your problem. I see. Datalog, on the other hand, simply does not allow infinite searches.

Okay. That's the area I've focused on. I've focused on very decidable logic programming. Okay, well, let's rewind and unpack some of these terms because i want to give i want to use this opportunity to give a good foundation for these topics because i think a lot most of us i think have heard of these things prologue and logic programming and relational things but um anyways i just want to you know start on firm foundations. So when I hear relational, I think of COD and databases. So maybe give like a brief history. Is that kind of where relational came from?

Yeah. Yeah. It's a perfectly reasonable thing to think of when you hear relational, right? Like you created relational algebra, relational calculus. I still don't know what the difference between those two is, by the way. And, you know, from that came SQL and most of our modern database work. And so when I think of that, I think of path independence and normalization. Like that's where my ring goes, but is that, that's not. What is path independence? The opposite of path independence is when I have, like, a nested JSON data structure, and I realize, like, oh, crap, like, I actually want, like, you know, if I have a list of people, and each people have some, like, each person has a list of favorite things.

I'm like, oh, crap, actually, like, I want to know how list of favorite things i'm like oh crap actually like i want to know how many distinct favorite things there are and i have to like you know i have to go out of one you know basically right okay i know i can get in trouble if i if i just like nest the data structure in the way that i think i'm going to want the data and then i'm like oh crap i actually wanted that i actually want the data in a different way. And usually what happens to me is I end up taking a nested data structure and then unfurling it into orthogonal lists that point to each other. Yeah, which is very much the sort of relational approach, right? Just have a bunch of relations saying how your data relates.

Don't think too hard about nesting everything so that it's efficient. Leave that up to the query optimizer and hope you have a good query optimizer. So relational algebra, what is the relation? Because I think most of us have used SQL. What is the relationship between relational algebra and SQL? So relational algebra is this formalism that Kot came up with in the 70s? Could be the 60s. I could be wrong. But anyway. Is it like lambda calculuses to functional programming? Kind of, yeah. Right?

So SQL can be thought of as an implementation of relational algebra plus some other stuff, except not quite. So it's relational algebra plus some stuff, but it gives up on some of the simplicity of relational algebra. For example, it has bagged semantics, not set semantics. So there's a difference between having multiple of the same thing, right? And it also adds some stuff to relational algebra that's really important, like aggregations. So anyway, before talking about what it adds, what is relational algebra? Relational algebra is you have a bunch of relations, right? A relation is basically just a set of tuples, right? So it's a set of rows. Okay. And a tuple is just like a dictionary or a object, like it's a key, key values.

You can think of it as key values if you like, right? But you think of a relation has a bunch of columns, right? Like there might be first name, last name, user ID, right? Every, the element of elements of a relation are, you relation are individual rows, which have a value first name and a value last name and a user ID. And that's what a relation is. It's just a collection of rows. And all the rows have the same shape. They have values for each column. And then you said it's a set of tuples. So it's not a list, it's... Yeah, it's not ordered. it does not care about duplicates.

Okay. Right. And IDs, we talked about that, or not yet? No, no, that's not particularly important. Okay. I don't even know whether the concept of a primary key is in the relational algebra. It's certainly not... Foreign keys?

That's, again, that's sort of, in my mind, I can't, I haven't read any of the original stuff on relational algebra, only like sort of read second sources or read Wikipedia. But in my mind that's sort of just a concept layered on top of it that formalizes a pattern of using relational algebra. Okay. Right. So you have relations, now how do you use relations? And the answer is you have various operators that combine them.

Some of them are simple. Filtering. You can say, you know, throw out the things in this relation that don't satisfy such and such a condition. Right? Union. If two relations have the same column names, right, or contain the same, you know, shape of stuff, you can take their union.

And then the most interesting one, of course, is relational joins. And what a join is, is... Actually, perhaps before we even talk about joins, we can talk about cross-product. Unions... I thought that was what joins were. No. So union is just like, give me anything that is in either of these sets. Oh, yeah, yeah, oh yeah yeah right so it's literal set theory union so a relation like i usually think of a um a it's not quite because uh in a database you have like a customer's table it has all the customers yeah but a relation

wouldn't be like i could have a relation of two different subsets of customers and take a union. Yeah, you could if you wanted to. And you can do that in SQL too. SQL has unions. I see. It's just they're not all that commonly used, but they are there. I see. Okay.

So joins are more interesting. Joins are like the thing. Right. All of this other stuff is useful and sometimes necessary, but joins are the single most common operation. And what they are, the way I like to think of them, although this may not be immediately obvious, is they're a cross product followed by a filter followed by a projection. So hold on, what are each of those things? A cross product is just, I have two relations, give, all possible pairings of things from those relations. Okay.

Right? So, you know, if I have a table of customers and I have a table of ice cream flavors, you know, let's say I have Charlie Coder user ID 0 and Hillary Hacker user ID 1, and I have chocolate and strawberry, the cross product will be charlie coder user id 0 strawberry, charlie coder user id 0 chocolate, hillary hacker user id 1 strawberry, hillary hacker user id 1 chocolate, right? All possible combinations. This can get very big. So, okay, why would you want to do that? Well, you can then filter this by some predicate. And I've chosen a bad example because there's no obvious way those things are connected. Maybe we can say that the parity of somebody's user ID determines whether they like chocolate

or strawberry ice cream. Well, maybe you could... well, yeah. Or another way to do it would be you have... a more realistic way is you have a table of users and then a table of orders where there's the user ID and then the order ID. So the table relating user IDs to order IDs and a table relating user IDs to their names and you want to have the order IDs and the names paired together. So you can take your cross product which just gives you, you know, every possible user paired with every possible order and then you filter it down by requiring that the user IDs match. Right? So that's called

an equi-join because you're requiring the two things be equal. Right? And then you, yeah, you throw out the junk, you project. That's not particularly important, right? Because you have two copies of the user ID column and you're required them to be equal, and that's silly, just throw out one. Okay, so the select is kind of the project, the join is the cross product, and then the predicate is the join on. Yeah, right. And then you say the predicate. Okay. So yeah, this is when you have two relations and you want to correlate them somehow. You want to say, give me all combinations of things from this relation and that relation that satisfy some

predicate, right, where these things match. And that to me, that's the relational algebra, right? You have relations, you have joins, you have a few other things like unions and filters, and you're done. And you can do a whole lot of stuff with this, but not everything. For example, if you want to have the sum of something, the relational algebra does not do that. It manipulates relations. A sum is a number, not a relation. Right? It just does not have aggregations. Oh, okay. Interesting. Which, I mean, obviously this is a limitation. It's not as if anybody has ever thought, oh, that's enough. Right, elation algebra is enough.

Right. But... I guess, well, because, and it seems like something, like, why would you leave that out? But I guess when you have an algebra, you have types and you have operations on those types. So, like, if you had, like, we have algebra algebra for numbers and we can add 1 and 2 And it'll get you the number 3, but let's say I want the word 3 like it won't... We need the word 3, but it would never give you the word 3, it'll just give you the number 3. Right, it's useful to formalize numbers even without formalizing how to, you know, print them as strings

Because well, you can add that part if you like, but here's how we do numbers. Relational algebra is here is how we do relations. I see. And then you can add extra stuff on top of that, and SQL does, and it's useful. I never use aggregations. Well, it's interesting because Datalog goes in a totally different direction. Datalog adds some... So Datalog maybe gives the logic programming background? Yeah, so, well, one way of explaining Datalog adds some... So Datalog maybe gives the logic programming background? Yeah, so, well, one way of explaining Datalog.

So Datalog can be thought of as a logic programming language. It can be thought of as a database language. It's sort of somewhere between the two. Okay, so, okay, sorry for interrupting. Keep going with what you were saying. Yeah, and the way, one way of thinking about it is it takes relational algebra and it adds something to it, just like SQL, but it adds a completely different thing. It adds the ability to define relations, to construct

relations recursively. And so the classic example of this is what I already gave, transitive closure in a graph, right? You have the edges, and you want to find all the pairs of nodes which are reachable from one another, right? So an edge relation would have a source and a dest column. And in relation to algebra, pick any number n, and I can find you the n distance paths. I see, I see. I can't find you all the paths. I see, I see. Because if you do the cross product once, that you one and then you filter that gets you one

uh path yeah and then you do the cross product again but you can't do the cross product infinitely yeah or like until it doesn't change or something like that i see okay so yeah i want to spend a lot of time talking about computability with you because i feel like you're you're i because i think that's that's something that comes up a lot when people discount logic programming. It's too slow or it'll infinite loop forever or, you know, like basically it's like too abstract. Like, you know, let's stick closer to the bits because we know that, you know, if we're controlling all the bits, we know the program will end because, you know, we have a tight rein on it. So, yeah. So I guess maybe let's start theoretical.

What is computability? Well, whether something can be computed or not by, usually we think of a Turing machine or whatever, it hardly matters. Is it related to decidability? Yeah, decidability is the same thing, basically. Decidability, strictly speaking, is pose a question with a definite yes-no answer. Or think of a question, a class of questions, parameterized by something, with definite yes-no answers. So an example would be, are these two numbers equal? So that's a class of questions, not a specific question. It would be like, does two equal four?

And of course that can be answered by a machine. Just build a machine that returns no. But it only gets interesting once it's a class of questions. So here is, you know, whether two numbers are equal. So it has two placeholders, two variables in it, x and y, you can call them or whatever. That question is decidable if your numbers are natural numbers. It is not decidable if your numbers are real numbers. Um. numbers. It is not decidable if your numbers are real numbers. Tell me. Oh, I see, because real numbers could be infinite?

Yeah, real numbers have infinite precision, and you cannot tell in advance how many digits you'll have to look at. You might have a number that you, you know, basically if you have, let's say you have the number 1, 2, 1, 3, 4, 5, 6, know basically if you have let's say you have you know the number one two one three four five six seven and you have another number one two one three four five six seven and they keep going and they keep going forever how do you know when you're done how do you know that they really are equal maybe there's a digit that's not equal just beyond where you looked so decidability to me if it has and computability has a lot to do with looping for forever? Yeah, right. I mean, when we say decidable, we ask, like, is there a... To say that a question is decidable is to say there is a machine or a computer program

that will answer every single question of that form, and for each one it will answer it in finite time, right, with yes or no. Okay. So that it never infinite loops on any particular instance of that problem. If it infinite loops on some instance, then it's not a decision procedure. It does not, so the problem is not decided by that program. Okay. Right. So, right, the real number equality is an interesting case, because it has the property that if two numbers are not equal, then the sort of obvious program, just compare the digits one by one, will eventually say these aren't equal. If two numbers aren't equal, eventually you'll get to a digit where they differ and you'll be like they're not

equal. It's only when... It's only when they are equal that you fail to terminate. Oh, I see. I see. That is interesting. Yeah. So that's called either semi-decidability or co-semi-decidability. I never remember which is which.

Oh, I see. Semi-decidability is when it's decidable in specific cases. Semi-decidable is when you have a program that if the answer is no, it will eventually answer no. But if the answer is yes, it might infinite loop. Okay. And so I forget how we got in this tangent. It's related to data log? You're sort of thinking about decidability and computability and logic programming.

Okay. Well, I think let's just unroll the stack. And before we continue down this thread, I want to ask you about, you were laying out three things. Right. Relations. Tables, relations, and predicates. Okay. And do you remember why?

Oh, because you said you were explaining how you can get to data logs from the relational path. Right, yeah. Or you can get to it from the logic path. Yeah. Do you know the history of Prologue, which way it came from, or was it influenced by both?

So I think what sort of... I'm not sure. Datalog sort of arose, it arose after the relational algebra. I think it arose mostly in the 80s by people sort of noticing... I don't know whether they noticed that the syntax looks like prologue so based on that I imagine they noticed hey if we limit

prologue in such-and-such a way then suddenly it is decidable right which is to say in prologue you can ask queries where it will infinite loop in datalog you cannot every program in datalog terminates, every query in Datalog terminates, it will always answer any question you pose of it. What do they remove? They removed basically every predicate or relation or table in a Datalog program has to be finite. So in Prolog, for example, you can find a predicate that says, you know, takes three lists and says, you know, column X, Y, and Z, and it whole, it is true if X appended to Y is Z. Okay. And you can run this, one of the wonders of

logic programming, you can run this relation in any direction. So you can give it two lists, X and Y, and it will give you, spit back at you, the append of these two lists. But you can also give it one list for z, and it will spit back all the lists which, when appended, make that list. In other words, it will find all the ways to split a list into two smaller lists. And these are both the same relation. You write it once and you get both ways of doing it. I may have missed it. So the same relation goes in both. So maybe give me an example. Maybe give me concrete lists. Sure. So if I say, you know, append, you know, list containing one, list containing two, z, right? What's z? Where z is a variable. It's an unknown. And I'm asking it, when you do this, this is

called a query. And it's saying, give me all the values of z such that this is true. Such that the append of one and two is z. In a normal programming language you say z equals append 1, 2. Yeah, right. Yeah. Okay, but in prologue you use z. You just give the logical expression that you want to be true, and it finds the solutions. Okay. Right, and in this case the solution is z equals 1 comma 2. Okay. But you can also put variables for the other parts of it. You can say give me x and y such that append x y is 1 comma 2. I see, okay. Right? So this is like saying, you know, 1 comma 2 equals x plus y, right? Which in a

normal programming language would be a syntax error probably. I see, I see, okay. But in Prolog it will give you back multiple answers. It will say, okay, one solution is x is the list and y is the empty list. Another one is x is the list and y is the list, and the final one is x is the empty list and y is the list. And the same code, and I can write down the code, I mean this is a podcast so that's probably not helpful, but I can write down the code for this. It's not very complicated. And it computes in both

directions. Yeah, just write down the code and show it to the microphone. Okay, and so this is almost like this can lead us to bad things in Prologue. This can lead to undecisability. Yeah, I mean, at the one time, this is part of why Prologue is awesome. And it's also dangerous because it makes your language more powerful and it can lead to, you know, programs in an infinite loop. Admittedly, this is not particularly any more dangerous than any other term, complete programming language, right? Every programming language that we know can write

infinite loops, except for ones that are very, very carefully limited, like Datalog. Okay. Datalog cannot infinite loop. Cannot infinite loop. Like, most programming languages, you could just write, like, while true. Yeah. The Datalog does not have while true. Right.

The equivalent of while true terminates with false. That's a little bit of unfair comparison. But there's a concrete example of this, which is in Prologue, you can feed it not the liar's paradox. So it's a logic programming language, so you can actually translate paradoxes into it. But the liar's paradox is this sentence is false. And this is problematic because if it's false, it's true, and if it's true, it's false. But there's another not exactly paradox, the truth teller's paradox. I'm not sure if that's the standard name, but it's this sentence is true. And this isn't really a paradox because, like, you can say it's false and then it's false, right?

Because it says it's true and it's not true, so it's false. Okay. But you can also say it's true because it says it's true and it's true also say it's true. Because it says it's true, and it's true, so it's true. So it's unclear what truth value it should have, but it is not paradoxical to assign a particular truth value. Now if you feed the equivalent of this to prologue, you say basically, you know, foo holds of a variable x if foo holds of a variable x. Okay. Yeah, foo of x if foo of x. And then if you ask prologue, does foo hold of 2? It will infinite loop.

Okay. Now, in datalog, if you do the equivalent thing, it will simply say no. No, it's false. So Datalog has an answer to the question, what is the value of the sentence? This sentence is true, and its answer is it's false. Okay. And the reason for this is basically Datalog has a sort of minimum, least fixed point semantics, or sometimes called a minimum model semantics. But what it basically means is if you don't say something is true it assumes it is false. For example, if you say there is an edge from two to three and then you end your program, right, you say that's all there is in the program if there is an edge from a two to three,

and then you ask it is there an edge from three to seven? No. You didn't write that, so it's not true. So it infers only the minimum set of things consistent with the program that you've written. It will not infer anything that you didn't write. And so if you say foo of x if foo of x, it will not infer that foo of 2 is true because there's no way to get to that. Right? not infer that foo of two is true because there's no way to get to that right it's consistent that it'd be true just like it's consistent with what you wrote down that there'd be an edge from from four to seven right you didn't explicitly say that it was false but sort of normally we only write down the things that are true right sort of intuitively if we're describing something we say

all the things that are true of the situation, not all the things that were false, because there are too goddamn many. And so based on that, based on that idea, only assume things are true if there's a clear way to prove them, Datalog will give you sort of the minimum rule. It will not... yeah. I feel like there's a... there's probably... there's a phrase in mathematics that does this, that only proves things. I think that's sort of what minimal model or least fixed point is. So we talked about the basis for relational stuff was relational algebra. The basis for logic programming is logic. First order logic, yeah.

And first order refers to? First order means you can quantify over objects, but not over sets of objects. So first order logic is the kind of logic that we're sort of most familiar with. We can say things like, for any number x, x plus 1 is greater than x. And calling it first order means that you can write that for any number x. So there's also something less powerful than that, which is propositional logic, where you cannot write for all. You can only, you can take primitive propositions and you can conjunct them, you can say x and

y. You can disjunct them x or y and so on. But you can't quantify over all variables. And then there's higher-order logics, which let you quantify not just, effectively, not just quantify over individual things like numbers, but let you quantify over properties of numbers. For any property p of numbers,

there exists a number x which p satisfies. I mean, this isn't true. That's a false proposition because consider the property that doesn't hold of any number. But it allows you to quantify over even larger stuff. I see. And now I see how it's higher order. I see how the phrase makes sense. sense you have you can you can have specific propositions about specific numbers you can you can have propositions for a bunch of numbers and

then you can have propositions about propositions yeah i see yeah um yeah and the weird thing, this is a total tangent, but sort of the weird thing about this is, so people, logicians, right, more or less figured out propositional logic, then first order logic, then higher order logics, right? There's obviously still work on each of these things, but sort of that's the order in which they started considering things. Type theorists and programming language theorists figured out the equivalent of propositional logic, very simple type systems, and then they figured out precisely second order type systems. Right? Type systems that you quantify over types,

but not over values, over types. And then we're beginning to figure out, we are figuring out dependent types, which are kind of first order as well as higher order. Oh, that's interesting. Right? So it's like we sort of skipped over the just first order phase. There are type systems that are kind of directly corresponding to first order logics, but they're kind of weird.

The first thing we figured out was so-called parametric polymorphism, which is where you're allowed to quantify over types. You're allowed to say, this function has type. For any type alpha, it takes alpha to alpha. So in my head, i have in like in haskell i'm thinking int arrow int is like first is first or it's like it's like the base that's about there's many different kinds of higher orderness in programming languages um and so

one of them is like are your functions higher order? Which I think is what you were thinking of. Well, I'm just saying we can have tight... I guess ignore the fact that it was... Yeah, you're right. I don't even have to talk about functions. Oh, maybe I was missing it. No, no. I just was overcomplicating my example.

We have ints. Yeah. And then we have lists of ints, which is... And like a list of an int is... is that polymorphic at all or higher order that's still first the first order can be parameterized that's like even a different direction that's talking about types parameterized by other types is that right well it's not exactly the same thing. So, quantification in a type system is, for example, having a function, the identity function, for example, that works at any type. Or the map function that maps a function, well that complicates things because it also

involves lists. So if you can describe types, if you have a type that admits other type, like subtyping, like num is... It's not about subtyping, not really. It's about what is the type of the identity function. Well, you could, what is the type of the identity function? Well, you could say it has the type int arrow int, because it takes instins. You could say it has the type boolean arrow boolean. But neither of these is really the most general type to give it. The most general type to give it is to say, for any type a, it has type a arrow a. That for any I put there, that's the equivalent of a for all in logic

but what is it quantifying over right it's not quantifying over values it's not for any value x it's quantifying over types it's for any type x i see and that's what makes it a second-order quantification. Is it only useful for the ID function? No, it's useful for a lot of other functions. They usually have to involve some sort of data structure. So an example would be the map function that takes a function and a list and applies the function to every part of that list. It doesn't care whether it's a list of integers or a list of booleans. So it has the type for any type a and any type b. Give me a function from a to b and give me a list of a and I'll give you a list of b. I guess I normally think about, yeah, it doesn't occur to me that there's an implicit

for any a and for any b. The only time I think of the implicit for any is if it's like show A fat arrow equal, you know. Because then it's like, oh, okay, this is for any show. Yeah, yeah, yeah. Because then it's explicit in the syntax. Yes, exactly. Yeah, but to a type theorist, we think of there being an implicit for any A. For any A. I see.

I see. Okay. Okay. Okay, so it's interesting that we skipped. So the middle level that we skipped would be... First order. First order. It cools into first order logic. So what would be a type in first order? Well, the reason why we skipped it is it's very not obvious what it would be.

Oh, okay. Right? Because... It's just less useful. Well, I don't know about less useful. I mean, the obvious example that I can give is dependent types. But dependent types don't really correspond to first order logic. They correspond to very higher order logic. Like all the bloody layers. There's not a clear correspondence anymore. Oh, okay. Interesting. But the thing that dependent types allow you to do that is like first order logic is they allow you to quantify over all values of a given type. So I can say for any natural number n,

this will take a list of length n and of, you know, I don't know, integers, and return a list of length n integers, right? So I'm not quantifying over a type there, I'm quantifying over a natural number, right, for the length of the list, right? That's like what first-order logic lets you do, right? Okay, interesting. Okay, so that was a kind of huge tangent yeah well i feel like this has been great i feel like we've been talking about interesting things but we should probably get to your main project okay i think we spent enough time laying foundations and talking around So yeah, maybe give the quick summary. The Spiel für Datafan. So we have Datalog, which is this language that can be thought of as logic programming, but limited.

Limited so that it's no longer true and complete. It always terminates. But because of those limitations we have, for example, much more efficient implementation strategies for it. And, yeah, I mean, that's basically the idea. It makes the implementation strategies more efficient and do interesting things. Or you can think of it as relational algebra plus fixed points. So it's like SQL with extra stuff, except aggregations are a pain. So I'll talk more about that later. But anyway, it's between these two cool areas, logic programming and relational programming.

This is Datalog? Datalog. Okay. That's what Datalog is. But what Datalog doesn't let you do is it doesn't let you notice that there's a repeated pattern in your code and break it out into a function. This is an ability that logic programming has because logic programming doesn't have the limitations of data log. But once you impose the limitations of data log, which are nice, you lose that ability.

But it's also something that functional programming has, because we have functions. See a repeated pattern? Just write the function that encapsulates that repeated pattern, right? That, you know, take the parts that are varying and make them arguments to the function, take the parts that are constant and make them the code of the function. And it seems like this would be a useful ability to have in datalog. For example, transitive closure. The standard datalog example. You have a lot of graphs you're having to do worse in your life. You can write transitive closure in Datalog, but you cannot write a function that, taken a graph, takes its transitive closure.

It only works for specific graphs. Right. You have to hard code. You have to pick a relation that represents the graph that you want to take the transitive closure of and write the thing that takes its transitive closure. And it's hard coded to that graph. You cannot plug in a different graph. You just gotta write a macro to plug in a different graph. Or, you know, add the ability to write functions.

Or add the ability to write goddamn functions. So that's kind of what Datafund is. It's an attempt to allow you to write what is effectively data log code, but in a functional language, so that if you see repeated patterns in your code, you can just abstract out over them. And along the way, we sort of end up adding a bunch of interesting things because it's easy and natural to add them in the context of a functional language. So, for example, we can add types, right? Datalog is

traditionally kind of untyped. There's no particular problem with adding types directly to Datalog, but as long as we're going to a functional language and we know how to use types for that, we add those, right? So you can have some types now if you want some types. Also lattices. So datalog... how do I explain the use of lattices in logic programming and in datalog and in datafun? I always forget what a lattice is. So in this case what I'm actually concerned with are join semi lattices. People often call them lattices because saying join semi lattices. People often call them lattices because saying join semi lattice every time gets it to be a mouthful. But what that means is you have there's two ways of thinking about it. One way of thinking about it is you have

a binary operator that is associative, commutative, and idempotent. So associative, the parens don't matter. Commutative, the order doesn't matter. Swap things around as much as you'd like. Idympotent, doing things twice doesn't matter. X join, the operator is usually called join, which is confusing because it's not database join. It's a different operator. So X join, X is X.

That's what idympotence means. And it has an identity element, a thing that does nothing. So the classic example of a joint semi-lattice is sets under union. Union is associative. The parens don't matter. It's commutative. X union, Y equals Y union, X. Or it doesn't matter.

It's idempotent. A thing union itself is that thing, you know? You're adding the set to itself. It has the same elements. I see, I see. Right? And the identity element, the thing that is nothing, is the empty set. Right.

Addition and multiplication are? Addition and multiplication are not semi-lattices because they're not idempotent. Oh, if you add a number to it. 2 plus 2 is 4. I see, I see. But maximum is a semi-lattice on the natural numbers. Or minimum, I guess. Minimum on the negative numbers would be.

Why you need an identity element. So let's go through each of the properties. Oh, I see. Maximum is associative. Yes. It's commutative. X max Y is Y max X. It's idempotent, a thing maxes itself is itself. But you need an identity element, a thing such that the maximum of X and this identity element is always x.

And so zero. Right. And so zero, the maximum of something in zero is always that thing, as long as it's non-negative. Right. So max, different people differ on whether a joint semi-lattice needs a zero, as it were, but for me, I always insist that it have that there be an identity element and so in haskell we have like types like monads and monoids and traversable and like we have like a uh type classopedia yeah semi-lattice would be a type

class okay great that was my question and what it, where would it fit in the tree? And like, why don't we have it in the tree? Because there's too many goddamn mathematical concepts. You can't, you know, having all of them in your standard library would be a bit much. I mean, you can add it, right? I think more practically, the reason why you don't have it yet is nobody has made a strong enough case for it to be in the standard library. Okay. is nobody has made a strong enough case for it to be in the standard library. It's not hard to add as your own library. Type classes aren't something limited to the core libraries.

You can make your own. And that's exactly what I do when I need to use semi-lattices. But yeah, what it would have... Well, okay, so first let me talk about the other way to think about lattices. I'll talk about them as an operator, but there's an equally important way to view them, which is as a partial order. Yeah, that's another phrase that... So a partial order is just something that acts sort of like less than or equal to,

except it doesn't have comparison. There can be two things, neither of which is less than or equal to the other. So the classic example here will be sets under subsetting. So you say that set x is less than or equal to the set y if x is a subset of y, not necessarily proper subset. So x is less than or equal to itself. It's a subset of itself, right, as far as I'm concerned. And so this forms an order in a sense in that it's transitive. If x is a subset of y and y is a subset of z, then x is a subset of z, right? Or a subset you might say included in, right? If x is included in y and y is included in z, right? It's reflexive. A thing is included in itself. A set is included in itself. And

it's anti-symmetric, which is if X is a subset of Y and Y is a subset of X, they're the same set. That's what we mean by a partial order. Those three things. And it's equivalent to a lattice? No. No. Okay. Every lattice is a partial order. not every partial order is a lattice. I'll get to that bit in a bit. Okay.

But yeah, it needs to be a thing like less than or equal to that has to be reflexive, transitive, and anti-symmetric. Okay. But it doesn't have to be total. There can be things that are just incomparable. Like the set containing just one, and the set containing just two. Neither of them is a subset of the other. Okay, so when is a partial order is a lattice

if it has a least element, a thing that is smaller than everything, and any two elements have a least upper bound. So a thing that is bigger than both of them, but smaller than any other thing that is bigger than both of them, but smaller than any other thing that's bigger than both of them. So the example here would be the union of two sets, right? And the least element obviously is the empty set, right?

It's smaller than any other set. The union of two sets is bigger than both of them. It's a superset of both of them. And anything else that is a superset of both of them contains everything in the union. Right? So that's what a least upper bound is. Okay. And that's what a semi-lattice is as a partial order. It's a partial order that has least upper bounds. Okay. And the least element. And you can prove these two things, these two views of them, the partial order view and the operation which is associated commutative and impotent, are equivalent. Because you can prove that the least upper

bound operator is associated commutative and impotent, and that the least element forms its identity. I'm just curious from a historical perspective, was there a person or an event that joined these things? God, I have no idea okay this is all like really old math yeah like this is uh yeah yeah like was it like hilbert or someone before like euler like i like i don't know it wasn't aristotle you know like um yeah and there's like umpteen zillion variations on this. So there's semi-lattices.

Some people take that to mean not necessarily having a least element. And then you can talk about semi-lattices with least elements. And then you can have meet semi-lattices instead of joint semi-lattices, which is the same thing. Instead of having a least element and a least upper bound, you have a greatest element and a greatest lower bound, which is... Right. And then you can consider having both of these,

and that's what we usually call a lattice. Is if you have a least element, a top element, least upper bound, and greatest lower bounds. Okay. And sets are... subsets of a given set form a lattice in that sense. The least element is the empty set. The greatest element is the whole set everything. Least upper bound is union and greatest lower bound is intersection. And these structures are very well behaved. They have all sorts of operators and they all interact nicely and you can... anyway. So anyway, yeah, you can view them as having to do with partial orders, or you can view

them as just being this algebraic structure. They have an operator and it abates certain laws. So why are semi-lattices interesting? Oh, right. Because sets are a semi-lattice, right? And remember how I talked about, you know, we have relations and you have tables and you have predicates. Well, here's another thing to add to the list. Sets plus tuples. Okay. Because a relation or a table can be thought of as a set of tuples, right? A tuple representing a row in the table and the set representing the whole collection, right? And so this is what DataFun does. It takes a

functional language, it takes a basic simply type lambda calculus, which is sort of like your vanilla, you know, starter base for a functional language design. And it adds to it finite sets as a data type and, you know, tuples, which are easy and ordinary, right? And then with those, those, okay, so the next question is, okay, you have finite sets, but how do you make them and how do you use them? And the answer that I give is, well, making sets is easy, you just list the things you want to be in the set. But how do you manipulate sets? You use set comprehensions. Which is, you can basically say, for every element x in the set y, do something, right, and give me the union of all of those somethings. So you can say for every element x

in the set 1 comma 2 comma 3, union together the result of the set, you know, 2 times x comma x plus 2. So the body of the comprehension is itself a set. It's not just one element. Yes, right. It's not just one element. It can be a second-handing one element or a second-handing the opposite. Yeah, second-handing two elements. But it turns out to be equivalent. You can do both ways, and they're equivalent.

The reason being, if you just want to give one element, if you want to restrict it to... I mean, this is impossible to describe without pen and paper. So I'm just not going to try it. But basically, basically this lets you write down what you would normally think of, or what a mathematician would normally think of as a set comprehension within certain limits, right? So you can't do infinite sets this way, but you can filter existing sets, you can take the cross product of sets because you can just comprehend over two sets, you know, for every x in the set A, for every y in the set B, give me x comma y. Sure. Right? And if you can filter and you can do cross products, then you can do relational joins. And so you started from the lambda calculus and added

set comprehensions, which you didn't like add relational algebra. Not explicitly. But you can maybe prove that it's like equivalent or? It can express everything add relational algebra. Not explicitly. But you can maybe prove that it's equivalent? It can express everything in relational algebra. And some other stuff that's not in relational algebra. Functions from the lambda type, for example. But I guess you could think of it as you took two algebras, like lambda calculus or two calculi and relational calculus, and you did the union.

Yeah, I sort of glommed them into one language that's one way of thinking about it uh but but technically you you just lambda calculus then and you added some things lambda calculus add set comprehensions and with a few other things like if you want to do an equi join you need to be able to test equality so add equality test and booleans okay not a big deal so in in in functional languages before you came along, I was already able to filter. Yeah. And I guess a set comprehension,

what's the equivalent in a functional language that we already have? You just do a list comprehension, right? Yeah, set comprehensions are like list comprehensions except for sets. And a list comprehension is a weird word. I don't know why that word got there, but that's the word we use. I used list comprehensions in Python, but I think in languages I just use, it's just map. Yeah, list comprehensions can all be done in terms of map and filter. Map and filter. Oh, okay, map and filter. But then I've never mapped over to... That's not true. You also need monadic join.

Another join that's different from all the previous joins we've discussed. So you also need basically concat map. Concat map, yeah. That makes sense. Concat map and from that you can get filter and yeah, that's it. Okay, so basically it's concat map. So well, we already had this in functional languages before this came along. Yes, absolutely. So you just invented a functional language that's just a regular functional language. Yeah. Uh, well, but it's not Turing complete. Oh, okay. So you took a functional language and you just subtracted things.

Yes. That's another way of looking at it. It is less powerful than almost every other functional language. Okay. Deliberately less powerful in the hopes that we can apply a bunch of prior work that's been done in the datalog community and the SQL community on optimizing expressions of this form, on optimizing datalog log evaluation and optimizing SQL evaluation. Because if you take that work and you try to apply it in the context of a full-blown higher order Turing complete functional language, it is a nightmare. But if we limit our language enough, we're hoping and we have some reason to believe that we might have some success in generalizing the

existing optimization literature so that you can write the stupid, dumb, obvious way of computing a join and your compiler or your implementation will figure out how to do it efficiently using an index. Which is not something that existing functional languages do. The best you've got is sort of list fusion, which is an impressive optimization, but it's sort of like combining multiple passes over a list into one pass. Like map, map, filter, map, filter gets commanded to one single pass over the list. I didn't know that that's what happens sometimes.

Yeah, this is an optimization that a bunch of people have worked on and they've gotten it to be pretty good and that's like, that is table stakes for database query engines. That is just like, nobody talks about that because it's freaking obvious, right? And this is what happens when you make your language more powerful. Everything gets harder, right? And so we're trying to find a sweet spot of something that is more powerful than Datalog, but still constrained enough that we can apply existing optimizations to it and imitate what has been done in the database community and the Datalog community.

Yeah, well said. I personally am someone who's really excited about the idea of less powerful languages. I think, I don't know if you feel this way, but I feel that, like, our, like, patron saint, or, like, the article, patron, the patron saint article is go to considered harmful, and in that, like, it was, like, very explicitly calling out, like, our languages are too powerful in this one explicit way, and if we get rid of this, it will actually be an upgrade, and so I, so I guess it spawned a whole class of articles like X and Y and Z is considered harmful. But particularly in making languages less powerful, so almost like we make them more well-behaved.

So we get more mathematical properties out of them so we can optimize them easier and other things like that. I'm a big fan of this theme. Yeah, I mean, I think I'm also kind of a fan of this. I don't know that it's the... I'm kind of a pluralist, right? I believe in taking every approach under the sun and seeing how it works out. But I think that trying to make less powerful languages so that you can do more to the languages is an underexplored area. What's the opposite of a pluralist? Because I feel like I'm someone who's like ideologic or like...

A Unitarian? I don't know. I find that I kind of like to do the opposite. I don't want to just try things until one works. I want to, from first principles, have a... Well, so when I say I'm a pluralist, I sort of say that as a belief about how a research community should function, not a belief about how any individual should do research. I think it totally makes sense to focus on one particular idea or one particular principle. I just don't think that any one principle is the only one we should be considering as a community. Yeah, sure. Of course. Okay. Right. But like this is in contrast to

people who want to build one language to rule them all, for example. I think that's sort of doomed to failure because I think that humans have many purposes, and programming languages are going to need to be built for many purposes too. I also sort of... I think some of the most interesting ideas in programming languages have come from programming languages which tried to do tried to say everything is a something right everything is an object everything is a function everything is a process there's a list of these yeah like there's a list of uh of for for each language x everything is a y there's a there's a like I'm just trying to do a verbal set comprehension. I think it's like on a TiddlyWiki. There's like a list given the language at all.

Right. And on the one hand, I think that some extremely interesting research has come out of this. Like functional programming came out of a lambda calculus where everything is a function. Object-oriented programming came out of thinking about trying to make everything an object. Logic programming. There are process calculi, which come out of everything is a process communicating with everything else. Logic programming comes out of everything is first-order logic, right? But at the end of the day, I don't believe any of it. Like, no, everything is not an object. Everything is not a function. Not everything is a process. Not everything is amenable to being described in terms of first-order logic, right? At the end of the day, the world is complicated,

and we need many tools, many approaches to try and understand it. But the kind of single-minded focus on a single thing is how you find out what the limits of that idea is. Until you commit yourself to fully exploring a particular idea, you probably won't realize just how useful it is. So this is sort of the sense in which I'm a pluralist. I do not believe that any one of these single-minded ideas will rule the world, but I think the world is better for having had lots of people who have tried to push these ideas as far as possible i i i think if i had to bet that's probably the world the view that would win but like in and so it's like i feel like it's irrational but i am one of the one one thing to rule them all kind of people uh i you know maybe i should work on changing that about myself because i'm like i

explicitly notice that it's like a weird thing or maybe just like a hope like i i like the idea of it's almost like physics envy you know like like a bunch of it's like you've heard the term physics envy it's like a derogatory term for fields that aren't physics that try to pretend like physics like mathematize things or reductionize things which is kind of what you're getting at everything is just this one we're going to reduce everything in the complex world

to this one simple thing because it's just more elegant to look at the world that way I hold out hope that we'll figure it out. Yeah, and you're someone who built on the lambda calculus. Is there a chance that everything is a function is the one that wins? Well, but here's the thing.

Almost every language that builds on the lambda calculus drops everything as a function. Right? Like when you represent natural numbers in functional languages, are they represented as church-oded natural numbers no they're represented as a bunch of bits representing a natural number in two's complement well i think there's um we could talk that's kind of like an implementation detail like the semantics of a language but it's not an implementation detail right it's there in the semantics too i cannot apply a number to a function and get that function applied that many times right that's what a church encoded natural number is yeah yeah yeah right well the only there

is one language i know of which sort of tries to take this idea to its logical extreme and like more or less encode everything and that is i hesitate to even mention it because i erbit tries to sort of do this it builds this extraordinarily simple um uh virtual machine which is almost a combinator calculus right and then tries to build everything up on top of that and if you can't do something efficiently then rather than introducing a new primitive this they have this concept, I think they might have called it JETS, of writing the code that does it inefficiently and having the compiler recognize that specific code and turn it into something that does it efficiently. Okay. Which is a cool idea, but I'm hesitant to mention the project because it's tangled up

with a whole bunch of ideological ideas about how programming should be organized and how distributed systems should be organized. And it's also just filled with obscurantist jargon, and it's really hard to decode what they're actually doing. It's funny you say this in this way because I think it was last night someone... You may have seen this. Someone I don't know on Twitter reached out, like, what do you think of Urban?

I clicked on their new primer. I was like, wow, what do you think of Urban? I clicked on the new primer. I was like, wow, like this is like so much better design than I've seen in the past. And so I posted it on Slack because of the graphic design of it. Maybe you haven't seen the new. No, I haven't. I don't know when it came out.

And like the first response was basically what you said. Like there's some useful things here, but like there's just like so much noise and like ideological stuff and like uh that like you know it's just like hard to focus on it um but it it i think other projects like it um there are a lot of projects that are just super wacky and but you kind of have to focus on the parts that are worth noticing and then just talk about those parts you shouldn't throw the

baby out with the bathwater I guess yeah I mean this idea about writing it the inefficient way and having the compiler recognize it is not unique to Ergrid I think somebody working on another wacky project called Avalon Blue who calls it it, I wish I could remember

their name, they call it Accelerators. So it's an idea that's going around in the fringes of programming language design community. It's very cool. So like at the, if you wanted to, you could like fully expand everything and see the inefficient but recognizable code, but then under the hood, the optimizations happen. Yeah, I'm just skeptical that it will overall reduce the complexity of your system because you still have to have that complexity, that inefficient implementation somewhere. It's just now that it's hidden beneath, it's hidden in your compiler implementation.

The, out of the tar pit paper, I think did a good job of arguing for something along these lines of like shoving your optimizations away from your more declarative code. Yeah, but I think there's a difference. So like the approach that I'm taking is again, trying to write declarative code, right?

Write the obvious, you know, join algorithm, which is just loop over set A, loop over set B. If some condition is true, yield, you know, two, whatever. Which, if you implement it naively, is at least quadratic in complexity, right? And then having your compiler recognize this. But it's like the accelerator approach is you don't just do that. You write the code that implements the naive version of a join and then you have your compiler

recognize when it is compiling that specific chunk of code, right, as if it's a reflection on trusting trust attack only being used to to make your code go faster um and then compile it to something more efficient right which strikes me as trading you know you're gaining one sort of elegance and that you just have one turn complete language as your source but you're losing the simplicity of your compiler. You're not cashing in on the ability to make real abstractions. That makes sense. It feels ad hoc. Yeah, I don't know. So back to DataFun. Yeah.

One way to look at it is it's a functional language, but we remove some things. I want to get into what those things are to make it, I guess, in the hope is as performant as a database. Or it could be used as a query language. Yeah.

So You could have really long, really big sets. Huge sets. Because in a programming language you would never If you were going to use sets that big, you would probably use a database. Exactly.

Right. That's a good way to put it. So Data Fund is like... It's a programming language that can work with sets so big that you normally would have used a database for them. Well, yeah, that's what we hope it can become. The implementation right now is not like that, right? You would not use it for anything other than toy examples.

Sure. And part of this is that, you know, building a really performant database engine is a lot of work and I don't... I'm one person with an advisor and that's not enough people to build a performant database engine. So the things we can work on are sort of the theory, right? Showing that all these optimizations that people use in real database engines and real data log implementations can be ported to a functional language like data log. Cool. And so I haven't actually finished describing data log, right? So we add sets and set comprehensions, but that only gets you to relational algebra.

That only gets you to sort of SQL-like levels of capability. To do what datalog can do, you also need a certain sort of recursion. The ability to find sets recursively. Mm-hmm. Yeah, the join thing we talked about. Yeah. For example, transitive closure. Mm-hmm.

Yeah, yeah. Transitive closure is defined in terms of itself. The fixed point join. Yeah, fixed point. Yeah, so we add a certain sort of fixed point to Datafund that allows you to find sets recursively, right, and that is what allows you to do the things Datalog can do. And one of the interesting things about this from sort of an academic point of view that maybe is less interesting to other people is... Well, actually, let's go back to logic. Paradoxes. Datalog allows you to define things recursively. Now, if you think about logical paradoxes, a lot of them involve self-reference. Like the liar's paradox, the sentence is false. Or the set of all sets that don't contain themselves, Russell's paradox.

So you might start to worry if you hear the logic programming language includes recursion. You might start to worry about logical paradoxes. And Datalog does something that prevents you from getting into trouble with logical paradoxes, even though you're allowed to define things recursively. And that thing is called stratification. What it means is you can write things that refer to themselves, but not in a negated way. You can refer to yourself, but you cannot refer to the negation of yourself. Okay. And if you look at all logical paradoxes, they all involve not just self-reference,

but negation. The set of soul sets that don't contain themselves. This sentence is not true. So that is what avoids datalog getting into hot water. It'll avoid having things that have no clear meaning. The equivalent of that, when you move to a functional language and you start allowing yourself to define things recursively as a fixed point, is that the function you're taking a fixed point of has to be monotone. An increasing input must yield an increasing, or at least non-decreasing, output, right? And this is sort of because negation is sort of the fundamental non-monotone logical operator. Increases input from false to true and its output decreases from true to false.

Every other logical operator increases inputs and its outputs increase. And make some of its inputs true, the output can only become true. Right? Or same thing. Right? So not is the fundamental non-monotone logical operator. I see. So there's this connection between monotonicity and defining things recursively without screwing yourself over, without being inconsistent or in sort of computational terms being Turing complete. And so we need a type system that guarantees that functions are monotone. And so that is part of sort of the more academic side of the data fund work, is a type system for

guaranteeing that functions are monotone. And this is the modal type stuff? The modal type stuff is like version two of that. So I'm skipping ahead. Yeah, so the original paper gives a type system that is able to guarantee that certain functions are monotone, and it's somewhat inflexible in certain ways, and so I've been working on a more flexible version that involves modal types. Got it. But it's for the same purpose, effectively.

It's for guaranteeing things are monotone. Got it, got it. So it, like, when you do certain operations and functions it it tracks the effect they have on the order for example if you have you know expression one set minus expression two right find the difference between these sets well that is monotone in the left hand side in the set that you're subtracting from but it's anti-tone in the right-hand side, the set that you were... I see, I see. Right? And if we do... But then if, like, another operation, like, does the opposite...

Right, yes. Subtracts again... Right. Then it flips. Then it all flips. And it tracks the flipping. Yeah, well, the original one only tracks monotonicity and non-monotonicity. Right?

The modal type stuff will track monotonicity, non-monotonicity, anti-tonicity. And I don't care tonicity, which I...icity, which I would call it bivariance. So it tracks like four different ways an operation can care about the order of its arguments. It can have, say, increasing inputs yield increasing outputs. That's monotone. It can say, I give you nothing. I give you no guarantees. That's non-monotonicity, right? No guarantees.

It can say, increasing inputs yield decreasing outputs. That's anti-tonicity or anti-monotonicity. And it can say, you can change that input however you like. My output will increase. That's not quite right. How could that be? So the obvious answer is a constant function. Change the input however you like. The output stays the same, which as far as I'm concerned is increasing. So when I say increasing, I mean weekly increasing.

Staying the same or growing. Oh, okay, sure. I'm like, how am I staying the same increasing? Weekly increasing. Or you can have a multi-argument function, which is constant in one of its arguments, but not in two arguments. But actually, it's a little more subtle. What it actually is is as long as the input changes to something that it is related to either by increasing or by decreasing then the output will stay the same or decrease. So an example of this might be, let's say you have a type which has two copies of the natural numbers in it. So it has, say, left

0, left 1, left 2, left 3, blah blah blah. And it has right 0, right 1, right 2, right 3, blah blah blah. OK. And the way they're ordered is left 0 is below left 1 is below left 2 is below left 3, and right 0 is below right 1 is below right 2 is below left 3 and right 0 is below right 1 is below right 2 is below right 3 blah blah blah. But lefts and rights are never comparable. Okay. They're incomparable. So what this, what the kind of function I'm talking about is called a bivariant function. What it says basically is if you change from left to right or right to left, I give you no guarantees.

But as long as you stay within left, my output will stay the same or increase. Which basically means it will stay the same. Or if you stay within right, then it will stay the same or increase. And this comes up basically nowhere in practice, but it makes certain internals of the system works out. It is in a certain sense dual to the I give you no guarantees notion. So anyway, I don't know why I got started talking about this. The notion of keeping a typism that keeps track in this way it's cool i it reminds me of this connell elliott quote where he he says like part of what makes algebra so great is that it doesn't keep track like four plus three is just it just is seven

and it's like it doesn't matter like seven is is isn't four plus three or five plus two it's just seven is just seven it doesn't um and so this like and he says if if seven wasn't like equivalent to three plus four or five plus two if you had to keep track of five plus two you would have a tree sorts of thing uh algebra would be like a tree thing and be less elegant so is your thing somehow less elegant or or you don't have to actually keep track of that far in the past because each thing is at any point in time either monotone or anti-tone and so you don't have to remember the past too much it's not a tree so there is no explicit past here right what this is really tracking is properties of functions. Right? A function is monotone, or it's non-monotone, or it's antitone, or whatever. Right? And the type system can tell you whether it's monotone or antitone or monotone.

I see. Right? And so plus and minus are functions. Plus and minus are functions. Plus would be monotone. Minus would be monotone in one argument, antitone in the other. And so once you apply plus to... So once you have a function that uses plus, that function itself just has a tone as well. Yeah, that function has a tonality. Okay, so there's no tracking really, it's just, you're just encoding the types in the same way. Yeah,

it goes into the types, right, so the type system, you know, tracks this and then it analyzes your code according to a certain set of rules. Well. I guess it tracks in the same way that the plus function tracks that its inputs were ints and now the output's an int. Yeah, exactly. I see. Okay, cool. That's very cool. It seems obvious now that you say it.

It seems like an easy thing to do now that you say it. But I would have never thought to add monotonicity into a type system yeah i mean it we added it because we needed it to capture datalog i wouldn't have thought of it otherwise but it turns out monotonicity has all sorts of strange applications um so uh so as i said monotonicity helps you avoid logical paradox, which is sort of why it's helpful here. It allows us to define things recursively while still having a well-defined best answer. Monotonicity also shows up in distributed and concurrent systems a bunch, though. So there's this work out from the West Coast in Berkeley and other places.

The boom? Yeah, the boom stuff, or specifically the consistency as logical monotonicity work. So I think there's a paper called Consistency as Logical Monotonicity or something like that. Sounds like a cool paper. And it says basically that the things that you can implement in a distributed system without any coordination without having to get the nodes to explicitly coordinate are exactly those things which are monotone in a certain sense like um a number that can only go like yeah a counter that can only go up a counter that can only go up or what's like the other yeah that's like i guess a canonical example. Or a pended-only set. Yeah, a pended-only list. A pended-only, but where ordering doesn't matter.

Yeah, I mean, yeah, a pen, yeah, that would work. I think you can also have a pended-only list. It's just a little more complicated. But yeah, and this is sort of connected in a way that I still don't fully understand to the CRDT work, right? Sounds like it. of connected in a way that I still don't fully understand to the CRDT work. Mm-hmm. Right? Sounds like it. And CRDTs are connected to semi-lattices. Because what are CRDTs? Okay, you keep track of a data structure that represents sort of your state of each node.

And there is a way to merge these states when you get one from another node. And this operation, it has to be associative. I see. It has to be commutative. I see. It has to be idempotent. And it may as well have a zero value or starting value. And that makes it a semi-line. So funny. I never thought of CRDTs because the merge function, I never thought of it as a function, but yeah. Right, because it's often not explicit, right, this merge function. That's not

usually the way you implement it, but it is there, right when you think about it it's there in your conception of the underlying structure i guess because it's the flipped perspective you think of a crdt as i have an object you have an object and we merge the objects but what's actually happening is the the thing i do to my object and the thing you do your object are then merged so it's like the edit actions that are that you apply the merge operation to it sort of depends CRDTs are there are like a lot of different ways of representing CRDTs okay so this the simplest way of representing CRDTs and the way that I'm sort of thinking of this is sort of state based right so you each node keeps a data structure representing its current state yeah so for a grow-only counter, this is simple. It's the counter, the value of the counter. Sure.

And then to synchronize with another node, you just send it your state. Oh, okay. You just send it your state. You don't send it the diff. You don't send it the diff. You just send it your state. Sending it diffs is sort of an optimization on top of this, or at least that's the way I think of it, right? But once you do that, the connection to semi-lattices becomes a lot more obscure. And so this is, you know, if I had the time, I would go and investigate this area from the viewpoint of, hey, semi-lattices are cool, can we make sense of all of this in terms of semi-lattices?

But I don't have enough time, I'm busy doing data fun. But yeah, I mentioned this idea to some people, in particular Martin Kleppmann, who has this idea of using Datalog to implement CRDTs, which I find super cool, right? So it seems to me that there is like some basic science waiting to be done in this area of CRDTs. But I really am not up to date on the area. I only have an outsider's perspective. I see. We've been doing a lot of talking about math in this conversation.

And I'm having a great time. I love math. But I think I've seen people criticize, people in our community, people trying to improve programming, criticize math. Or like using math too much. Not criticizing math for its own sake, but people say that we make our types too complicated. We're trying to incorporate math in ways that overcomplicate things. And that programming isn't math and we shouldn't make it math. We should make it its own thing. how would you respond to that criticism i have somewhat complicated thoughts

about this but so the first one i would think is it definitely can get in the way if you are trying to learn something quickly and you want to just start right so for people first learning to program i think that excessive abstraction including excessive use of type class abstractions something quickly and you want to just start right so for people first learning to program i think that excessive abstraction including excessive use of type class abstractions can definitely get in the way um i think for example probably we should teach people to program in dynamically typed languages because it is one fewer thing to worry about um i'm not like dogmatic about this i don't have a strong opinion on this but that would be my intuition but I think that these abstractions that we create type classes monads they come

about because they really are recurring patterns in programs. And it really does help, especially for programming at large, to have names for these patterns and ways to reuse them in your code. And how much it helps will depend on what kind of code you're writing and what kind of things you care about, right? If you really need absolute control of what's going on with all your bits, then abstractions can absolutely get in your way. But a lot of code doesn't need that. And a lot of code, it's more important that you be able to grasp at a high level what you are doing and to articulate that

at the level at which you are thinking it, for which it can be useful to have abstractions. So basically, I think abstraction, the level of abstraction at which you work is one part of the trade-off space that is programming. You always have to trade off things against other things. And abstraction pays dividends in the long run, but it requires some investment up front. I think that's a really great lens, that it's like a short-term, long-term thing. If you want to just get going, and I think a lot of people who want to improve programming, what they really care about is the onboarding. People should be able to learn to code as fast as possible.

Yeah, and I think that is important. And then there are other people who care about the, once you've learned, how easy it should be. And they're almost opposed. They're almost directly opposed. The easier it is once you know how to do it. Well, I think we perceive them as opposed. This is another one of my bugbears. I think we perceive them as opposed because they are simply different and right and both hard um there are clearly ways

to optimize one it that is at the expense of the other yes but there are also ways that optimize both of them and we don't talk about those because we just do them right if there's an easy way to improve of course of course then we we do it right i see yeah um so it's sort of there's three classes we only talk about the ones that yeah are at are out of pose. Yeah, of course. Yeah. Yeah, yeah, of course. Well said. I've forgotten what I'm trying to say.

Yeah, the thing that's good for both beginners and experts are just in all programming languages. Yeah, unless they're hard. Unless they're like, but then that program, it's like very clear that you should just change that language. No, unless it is hard to do them. Oh see i see yeah yeah yeah i thought you said unless it's a hard language yeah unless it's just a bad language yeah yeah so um you're you're a train of well so i was i interjected to like affirm that i really like the idea that math math so one way to think instead of using the word math which like has all sorts of weird connotations you could just use the word patterns and recognizing patterns

and when you're first introduced to a subject you don't see any patterns because everything's new and so like to just throw patterns on people right at the beginning is not a good idea but but like the more you do something the more you're gonna going to use patterns because like you don't want to be repetitive yeah um and so if you're interested in making programming easy for beginners then throw away the patterns because they don't they like they won't mean anything yeah or build them into speeches of your language so that they don't have to think about them right right so like don't force people to use gotos, just have them use structured for loops, right? That is in some sense a pattern. For loops are a pattern that you can express in terms of gotos, but you can turn that pattern

into a language feature so that you can just think at the higher level immediately. So there are some abstractions that paint evidence immediately even for beginners, like for loops, like for loops. Other ones take a little more effort to learn, and maybe it's not worth trying to introduce a beginner to them. So you said that you can sort of replace the idea of mathematizing programming with the idea of recognizing and impressing patterns. But it's also true that there are different sorts of patterns in programming languages, some of which we know how to quantify and exactly capture using math, some of which are a little fuzzier at the moment, right? And I think there's this more general divide in programming between techniques that are useful when you know exactly what the problem you're solving is, and techniques

that are useful when the problem that you're solving is sort of fuzzy and not very clearly defined but still important right sometimes you see this as a front-end back-end dichotomy that's how it manifests sometimes but i think it's more to do with how precisely you can define what it is you're trying to do how how like iterative your process is are you gonna Are you changing your... What this brings to mind is waterfall versus agile. Are you a startup who's iterating really quick, or are you some old company that's rewriting existing software to do the same exact thing?

Yeah, I think that's another way this same distinction can manifest. And I think, basically, mathematics is most useful for the stuff where you know exactly what it is you want. Mathematics is about formalism, about being able to precisely specify things. It is most useful when we know exactly what it is we want and what we're doing. It's less useful when you're doing things that are fuzzier. Not useful, right? And I think a lot of the history of progress in programming science

has been being able to more precisely specify what we want for larger and larger components. Right? And that's why I think you sort of see an increasing tide of mathematization in programming languages and programming work because we are building up from the bottom, as it were, building up from the smallest things towards larger and larger things that we know how to precisely specify what we want but we also work down from the top we work from we want to make a system that does this

thing involving humans right um you know we want to make a video game that is enjoyable we don't know how to specify that right um and so the tension between those two things i think produces a lot of this conflict between the people who are really gung-ho about formal methods and mathematization and so on and the people who are really not gung-ho about that and think that premature formalization uh can bog you down in details that you don't want to get bogged down in yeah i and part of me wonders if if you can have the best of both worlds where you can not get bogged down but also

um get the benefits of more formalized stuff and so like the way i think that like it occurs to me is part of what i like about types is they um are like automated reminders of like oh by the way you know like in certain cases that you didn't handle things aren't going to go so well like uh but i i don't want the types to like stop anything i just just want like, like on the side as an afterthought, just so you know, if you care to know like there's some things, there's some implications that you may not be realizing. That's, that's what I feel like that could, that could maybe unify into the best of both worlds where it doesn't prevent

you, it doesn't bog you down, but it, but also doesn't like leave you in the dark. Yeah, and I think that's sort of a compelling vision, which is sort of what the gradual typing work is investigating, and Cyrus's work is sort of investigating this as well, with the holes that allow you to have not fully foreign programs or not fully well-typed programs that can still execute. Yeah, I've really had bad experiences with like typescript you know like i don't like

it at all people love typescript yeah i know someone who really loves everybody loves typescript and it's my only experience with gradual typing it's just like so much worse than just programming javascript because when i get i guess to your point when i program in javascript i just want the code to run like i don't care about the cases that you're telling like i don't like stop stop forcing me to like fix these type things like i just want to like iterate and then like at the end i want to like hear what you have to say about why my types don't make sense but like you're like you're bugging me right now you know interesting i guess it is true the gradual typing work is not generally cyrus's work is about being able to run incomplete or ill-typed programs with these holes inserted

but most of the gradual typing work is not about that right you can you can have a part of your program that is not typed and you can still run that program but if you add the types they better type check otherwise no yeah yeah so anyways so how does Datafun compare and contrast with the Eve work that you were such a fan of? It's much less ambitious. I'm not trying to reinvent all the programming. I'm just trying to see whether we can combine functional programming and data log, right? Simple relational programming. So Eve was trying to be a system which enabled non-programmers or people without a lot

of programming experience to build complex distributed systems. I'm not trying to do that. I'm just trying to combine what I like best about Datalog, that it lets you do simple relational stuff without worrying too much about how their data is represented behind the scenes, and then, you know, run it fairly efficiently, with what I like about functional programming, which is that I can abstract out repeated patterns in my code. Okay. And in a dream case for you, is it data fun itself that goes on

to be something that people use or more people take the underlying research and embed it into another language um i'm like all for any of these options right so like i find i think definitely um the thing that i think is the most likely dream scenario, right, is that the ideas explored in Datafund help other people design languages and build systems, right? And I think Datalog has been influential in that way, in the same way Relational Algebra has been influential in that way, right? Oh, interesting. Dat log influenced... Data log... So there's sort of a community of various industrial people who use various data log dialects. So Semmel uses data log to do static analysis of large code bases. Logic Blocks, who recently got acquired and basically no longer exist in any way that matters, but while they were around, they used Datalog to do business analytics. Yeah, I've heard of Logic Blocks from Jamie Brandon,

who used to be at EVE. Yeah. EVE was influenced by Datalog, so if they got off the ground, that would be great. And just, I don't know. It might seem that way to me only because I'm doing work on it, but there are people with ideas built around datalog cropping up in the research community and I think also

bleeding into certain parts of the industry community as well. It's still sort of on the fringes. Oh, there's the work out in Berkeley, the boom work, right data list data log in space so um is there a world in which um data fund becomes like a competitor to sql or like or a day or like a data log are there is it kind of equivalent in that way because i don't like i don't enjoy sql uh for all the reasons people don't enjoy sql but it seems but it's like fast and i like relations so could i like swap out my my postgres database with like a data fund database or that's not quite in some hypothetical future yeah um there are all sorts of questions that would be have to be answered along the way but yeah in some hypothetical future data fund could be a query language for a database.

The questions that would have to be answered along the way are, well, obviously the ones we're still working on. Can we port the existing optimizations work from the database community to work on DataFun? And also, SQL isn't just a language that lets you do queries, it also lets you do updates and, you know, migrations and stuff. Oh, I see. Yeah, yeah, yeah, of course. Migrations, of course. And transactions. And transactions.

Does DataFind... Kind of critical. It operates only on, like, an existing database. You can't... There's no... It doesn't talk to an existing database at all. What I'm getting at is it's immutable. You can't, there's no... It doesn't talk to an existing database at all. What I'm getting at is it's immutable. You can't, like, mutate.

Yeah, it's just a, it's like the relational algebra, it's just a query language, right? It just lets you answer questions about some data that already exists. I see, I see. Or write expressions that compute data. I see, I see.

It feels like it, yeah. Now it's making me think of Datomic, the Rich Hickey's project. Yeah, although that also deals with change in some way that we don't, right? They have some story about it being sort of append-only or always keeping your old data around, but we don't have any notion of time at all in Dataflip.

It's just sets and computing with them. Yeah, what made me think about it is they have a query language that feels like Prolog. You can, like, you give it a... Well, query language that feels like Prolog. You can like, you give it a... Well, yeah, that's, it's Datalog. Okay. Effectively, right? They sell it as, it's a Datalog dialect, I think. It's proprietary,

so I haven't been able to actually look at it properly. I see. Okay, yeah, yeah, yeah. So that's another thing to add to the list of things inspired by Datalog. Yeah. Okay, so in theory, the data funnel work could be a competitor or it's an alternative, or it's like in the same space as Datomic. Yeah, in the same space as Datalogs or as SQL. But again, there are a bunch of questions, practical questions that would have to be answered first.

Yeah. So incremental computation is when you change the inputs to a function, you're like reusing some of the old... Sorry, let me ask again. So maybe give us a foundation of what incremental computation is. I mean incremental computation is just the idea basically you run a function once, you change the input, you want to know what the functions result on the changed input is, how can you compute that more efficiently than just recomputing the function functions result on the changed input is, how can you compute that more efficiently than just recomputing the function from scratch on the new input? That's one way of thinking about it.

And so from a programming experience perspective, what I'm curious about is a slightly different perspective on incremental computing. If I keep the inputs the same, I slightly change the function. What can I reuse from the past computation god um i mean that's in some sense the same question in that you have the function that takes the program and the input and gives you the result and you're changing one of the inputs to that function namely the program ah um well said uh but it's a much harder problem because programs are really complicated, structured things. And so you're kind of taking the derivative of the input. So we're taking a derivative of a program.

Yeah, so one perspective on incremental computation is that you're taking the quote-unquote derivative of the program or the function that you want to compute incrementally. Because you want to know howally, because you want to know how does this function change as its input changes. And that's actually related to the derivatives of fixed point is a fixed point of derivative, right? Basically, I found a rule for in a certain system of incremental computation, finding the derivative of fixed point, and it turned out to be involved taking the fixed point of the derivative of the function that you were originally taking the fixed point of. I see. And so what it was useful for is making data fun go faster. Because data fun allows you to compute fixed points, and fixed points can be computed naively

just by taking the function you want the fixed point of and repeatedly applying it, smacking it on the data until its output equals its input. This is kind of annoying because you have the same function and its input is changing, right? First its input is, you know, the empty set. Then you take its output and you use it as its input. So you have changed its input from the empty set to whatever its output was. And then you reapply it. I see. Right? And you keep on doing that.

Oh, I see. And really what you want to do is incrementally recompute the results of the function because its input has just changed. It happens to be that the thing you've changed it to was its old output, right? That's the weird part about fixed points. But it's really just incrementally recomputing the function. I see. And that's where incremental computation and fixed points and derivatives all intersect. I see. Cool. If you want to make fixed points more efficient, you're going to use incremental computation, and then it's really important to know that the fixed point of derivative is the

derivative of the fixed point. It's important if you nest fixed points. Okay. Because, for example, if I have a function that I want to take the fixed point out and the function is defined in terms of a fixed point, I need the derivative of the function to compute the outer fixed point incrementally, and the fixed point function itself involves a fixed point, so I need to know how that fixed point changes. Okay. I'm going to have to listen to this a couple times in post-production to get it.

But that sounds... Apologies to anybody listening at double speed. Just hit the rewind button a few times okay thank you so much for taking the time this was a lot of fun yeah this was fun