It's a nice write up but I'm not sure what the contribution is. I would have expected more engagement with Peter Van Roy's work, in particular his and Seif Haridi's epic book CTM [1] where the logic variable got properly unpacked more than 15 years previously. Or at least a citation.
Has anyone looked into how to decouple logic variables from backtracking? i.e., is there a good reason to unbind a variable apart from the Prolog discipline? (Without unbinding we get single-assignment variables where initialisation is decoupled from declaration, which I feel can often be simulated with laziness ala Haskell, but see CTM.)
They cite one of the works of Gert Smolka (Smolka and Panangaden, 1985), who was the original creator of Oz. But I agree that Van Roy and Haridi did a lot of research on functional logic programming back in the 1990s that seems to be ignored here.
When I worked on program semantics, I had the impression that PLT communities in the US and EU tend to ignore each other. This also translates to education. CTM is an epic book, and very readable, but I don't think it's well known or used much on the other side of the pond.
Yes, I was unaware of Smolka's early work and it does look very nice. (Much of Smolka's work seems underappreciated.) The evaluation in the paper under discussion of this work seems weak given that Smolka's early effort has a very similar set of features to what they want.
I concur about the research silo-ing. However in this case we have Europeans ignoring Europeans, and on that CTM page you will find a grab from a review in the Journal of Functional Programming. Several authors of this paper have published in the JFP, leading me to conclude that the JFP is a write-only journal, like much of CS literature.
The Verse programming language, at least a while back, reminds me a great deal of the Icon programming language, as well as jq, with pervasive backtracking and generators. Icon's authors referred to it as "a goal-oriented programming language".
Tim Sweeney & Epic are creating the language Verse whose logic functional underpinnings will make concurrency & correctness easier in Fortnite.
https://youtu.be/ub-dls31Pyw
The original claim was to create a new programming language for developing games.
Everything that has come out of Verse so far has been "oh look, I designed this language I wanted to design and the only relation it has to gaming is the title of the paper"
We don't even know if it's a good programming language for anything, as it doesn't exist outside Unreal for Fortnite
Maybe I'm not understanding the insight here, but it sort of seams like having confluence defeats the purpose of logical semantics.
My specific concern is that by having logical semantics in a language you can represent non-deterministic ambiguous computations, but for this you need divergent paths which, if I understand correctly, the authors have removed from their language. So what's the point of doing this?
I can't speak to the point of doing this, but (IIRC/IIUC) you're talking paths and they're talking the entire computation tree, i.e., a term in their calculus represents all solutions, and computing normal forms makes them easy to read off (?). Perhaps there's some meat in how they handle the equivalent of `bagof/3`/`setof/3`.
It's a nice write up but I'm not sure what the contribution is. I would have expected more engagement with Peter Van Roy's work, in particular his and Seif Haridi's epic book CTM [1] where the logic variable got properly unpacked more than 15 years previously. Or at least a citation.
Has anyone looked into how to decouple logic variables from backtracking? i.e., is there a good reason to unbind a variable apart from the Prolog discipline? (Without unbinding we get single-assignment variables where initialisation is decoupled from declaration, which I feel can often be simulated with laziness ala Haskell, but see CTM.)
[1] https://webperso.info.ucl.ac.be/~pvr/book.html
They cite one of the works of Gert Smolka (Smolka and Panangaden, 1985), who was the original creator of Oz. But I agree that Van Roy and Haridi did a lot of research on functional logic programming back in the 1990s that seems to be ignored here.
When I worked on program semantics, I had the impression that PLT communities in the US and EU tend to ignore each other. This also translates to education. CTM is an epic book, and very readable, but I don't think it's well known or used much on the other side of the pond.
Yes, I was unaware of Smolka's early work and it does look very nice. (Much of Smolka's work seems underappreciated.) The evaluation in the paper under discussion of this work seems weak given that Smolka's early effort has a very similar set of features to what they want.
I concur about the research silo-ing. However in this case we have Europeans ignoring Europeans, and on that CTM page you will find a grab from a review in the Journal of Functional Programming. Several authors of this paper have published in the JFP, leading me to conclude that the JFP is a write-only journal, like much of CS literature.
Could it be that they're not aware of that which they are not referencing?
I notice that they reference Icon. They don't reference jq (well, there's no publications on jq to reference).
The Verse programming language, at least a while back, reminds me a great deal of the Icon programming language, as well as jq, with pervasive backtracking and generators. Icon's authors referred to it as "a goal-oriented programming language".
I'm fascinated that Epic Games are the authors. Does anyone know what their motivation for this research would be?
Tim Sweeney & Epic are creating the language Verse whose logic functional underpinnings will make concurrency & correctness easier in Fortnite. https://youtu.be/ub-dls31Pyw
The original claim was to create a new programming language for developing games.
Everything that has come out of Verse so far has been "oh look, I designed this language I wanted to design and the only relation it has to gaming is the title of the paper"
We don't even know if it's a good programming language for anything, as it doesn't exist outside Unreal for Fortnite
Reinventing the programming paradigm has been Tim Sweeney's hobby horse since before 2006: https://groups.csail.mit.edu/cag/crg/papers/sweeney06games.p...
After Epic's wild success hes now got a bit of cash to splash on making his dream a reality :-)
Maybe I'm not understanding the insight here, but it sort of seams like having confluence defeats the purpose of logical semantics.
My specific concern is that by having logical semantics in a language you can represent non-deterministic ambiguous computations, but for this you need divergent paths which, if I understand correctly, the authors have removed from their language. So what's the point of doing this?
I can't speak to the point of doing this, but (IIRC/IIUC) you're talking paths and they're talking the entire computation tree, i.e., a term in their calculus represents all solutions, and computing normal forms makes them easy to read off (?). Perhaps there's some meat in how they handle the equivalent of `bagof/3`/`setof/3`.