As someone whose day job involves a lot of graph analysis and logic programming[0], I'm always excited to see new applied research in this area. More energy is needed here.
Logic systems will be a key part of solving problems of hybrid data analysis (e.g. involving both social graphs, embedding spaces, and traditional relational data) - Cozo[1] sticks out as a great example.
[0] https://codeql.github.com/docs/ql-language-reference/about-t...
Oh, hello hacker news!
Also potentially interesting to this crowd are the underlying editor, which I split out from the online Dusa editor and called "sketchzone" (https://github.com/robsimmons/sketchzone). Some of my motivations and hopes for sketchzone are blogged here: https://typesafety.net/rob/blog/endless-sketchzone
Also, I more-or-less did Advent of Code 2024 in Dusa: journal entries and links to solutions are at https://typesafety.net/rob/blog/advent-of-dusa-2024
Additional shout out to the Recurse Center (https://www.recurse.com/) which was instrumental in giving me the space and environment to start working on Dusa. I did a partially-remote, partially-in-person batch at Recurse in late 2023.
Is there an implicit algorithm for how this language is evaluated? It seems hard to use without having an understanding of the likely performance of your code.
There is an implicit algorithm, and I'm so happy about this question. The inability to reason about likely performance of one's code is, to me, one of the things that bothers me most about Answer Set Programming, the programming paradigm that's probably the most like Finite-Choice Logic Programming.
The Dusa implementation has a couple of ways to reason at a high level about the performance of programs. The academic paper that febin linked to elsethread spends a fair amount of time talking about this, and if you really want to dig in, I recommend searching the paper for the phrases "deduce, then choose" and "cost semantics".
There's work to do in helping non-academics who just want to use Dusa reason about program performance, so I appreciate your comment as encouragement to prioritize that work when I have the chance.
Is it different from SQL though?
> Note that this if-then statement is written backwards from how it’s written in English: the “then” part, the conclusion is written first, followed by the :- symbol. After the :- symbol come the premises
Why not write it like it’s written in English? It could be one less thing to learn for people trying to adopt the language.
The two answers by jonjojojo and khaledh are great, because they are both the correct answers.
From a principled point of view, the rule "a :- b, c" helps define what "a" means, and it seems, in practice, most helpful to be able to quickly visually identify the rules that define a certain relation. The list of premises tends to be of secondary importance (in addition to often being longer and more complicated).
From a practical point of view, we wrote Dusa as people familiar with existing Datalog and Answer Set Programming languages, which use the backwards ordering and ":-" notation, and some of the core target audience we hope to get interested in this project is people familiar with those languages, so we made some syntax choices to make things familiar to a specific target audience. (Same reason Java uses C-like syntax.)
The :- is supposed to sort of look like a left facing arrow for an implication. I think this notation started with prolog, so that is my guess why they chose to make it like this.
I think the reason is that the right hand side can be a long and complex set of premises. It is supposed to be read as: The lhs is true iff everything on the rhs is true.
You can also think the same way about functions in typical languages: we don't write the body of the function first and then assign it to an identifier.
Yes, but not `iff`.
f(X) :- g(X), h(X).
f(a).
With those two statements, `f(a)` is true, but it does not mean that `g(a)` and `h(a)` are also true. Instead, it means that we happen to know some fact, `f(a)`, and some rule for cases beyond that fact. If it also happened that `g(a)` and `h(a)` are true then we'd have two ways of arriving at the fact of `f(a)` being true.It's a reverse of the implication arrow and is meant to be read that way:
f(X) :- g(X), h(X).
Is read as "f(X) if g(X) and h(X)", versus "if g(X) and h(X) then f(X)".Thanks for the correction :)
It's not really written backwards; it's just equivalent to a different if statement. Something like this:
if (want: edge Y X) { search for: edge X Y }
This is searching in reverse compared to a different if statement:
if (have: edge X Y) { assert: edge Y X }
So happy to see Dusa on HN. Was a joy to see you work on it while in batch at RC. Congrats!
Research Paper https://arxiv.org/pdf/2405.19040
...and if you're in the vanishingly small overlap of folks reading this comment and people interesting in attending an academic talk in Denver next Wednesday, the official conference page for the paper is https://popl25.sigplan.org/details/POPL-2025-popl-research-p...
(The ArXiV preprint has the exact same content)
Oh, I'll be on the live streams!
https://popl25.sigplan.org/attending/live-streams
I want to say that the cultural changes inside of the ACM to make historical research open access and to have excellent live streams of the conferences is just so damn wholesome and wonderful. Thank you ACM and the people inside the ACM that made this happen.
And in case someone from the ACM is reading this, the live streams are very useful for physical attendees. I was attending Splash! and there were a ton of talks where I would have needed to change rooms, wanted lots of desk space for notes and research. It was somewhat ironic attending half a day from a vacation rental. :)
Any real life tasks examples?
not only do I think that choice is a really important tool for writing pragmatic logic programs, this is a key piece to a really interesting goal - unifying logical and procedural programming (see verse)