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.
discarded1023 · 42d ago
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.
cryptonector · 42d ago
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).
atombender · 42d ago
So how's the Verse language and ecosystem turning out?
There was a big splash about this when it came out in 2023, with big names like Simon Peyton-Jones, Lennart Augustsson, and Guy Steele involved. But since then I've heard nothing. Apparently still Fortnite-only, not built into the Unreal Engine. I'm not wired into the gamedev world, is anything happening here?
MattRix · 42d ago
It is still used exclusively in Fortnite map-making at this point, and Epic is using it internally themselves for implementing certain Fortnite features as well. The plan is that it will be one of the major features of Unreal Engine 6.
zaxioms · 42d ago
I'm fascinated that Epic Games are the authors. Does anyone know what their motivation for this research would be?
troupo · 42d ago
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
It looks like it's currently down (not sure if a glitch or what).
woolybully · 42d ago
Tim Sweeney & Epic are creating the language Verse whose logic functional underpinnings will make concurrency & correctness easier in Fortnite.
https://youtu.be/ub-dls31Pyw
cryptonector · 42d ago
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".
cryptonector · 41d ago
Reading the paper I see they even have a subsection (6.6) comparing the verse calculus to Icon. Nice!
A few nits on section 6.6:
- difference (2) is just a limitation of Icon that no collect() primitive is provided, but a) it could have been, and b) one can build one:
procedure collect(expr)
local results, value
results := []
every value := expr do
put(results, value)
return results
end
which is not unlike the situation in jq where there is a built-in array collector `[exp]` but one could build one with `reduce` like so:
# There is no need for this given that jq has [exp]
# as syntactic sugar for collecting expression
# outputs into arrays, but still, this does work:
#
def collect(e): reduce e as $i ([]; .[length] = $i);
Of course, the jq `[exp]` collector internally works a lot like the above `collect()`, which is what one might expect, and I would expect that the verse calculus `all` would also work this way (when "run in the forwards direction" anyways).
- difference (3) is not quite true in that there are reversible assignments in Icon where backtracking undoes the assignment, but TFA's point is probably really about the existence of non-reversible assignments _at all_. (jq only has reversible lexical assignments called bindings, and does not have non-reversible assignments.)
- I suppose there is a difference that is not listed: Icon lacks unification, so it cannot solve equations backwards like the verse calculus can. (This is also the case in jq.) This was very much worth mentioning!
Note that jq can be condensed into a much simpler prelude that begins to look like a calculus. Note also that jq does not have implicit cuts, which was probably a mistake.
cryptonector · 40d ago
More commentary.
VC is just a calculus, and as such there are no performance concerns. Still, I find it weird that `all` is essentially a collector operation, and that's the only way to "get all the outputs" of an [generator] expression. In jq, because the jq executable itself outputs all the values of the given jq expression [applied to every input to the jq executable, unless -n is given] there is no need to collect all outputs in order to do something with them. What this amounts to is that the jq programmer can trivially implement list fusion, for example, as jq expressions are by default online, and you only lose the online property if you resort to collecting values.
I've not yet looked at the Verse programming language, but I would hope that the language -unlike the calculus- does not force one to give up the online property all the time like VC does.
OTOH, the `one`<->`all` duality is quite elegant -- a tour de force, and a great insight.
This has me wondering how to add unification to jq, or even what a jq calculus might look like.
For example, we can cut the jq language way down, removing even `reduce`, array and object constructor syntax, array and object index syntax, and even `if`, and have just values, expressions, very few built-ins (like `empty/0`, `first/1`, array and object constructor and indexer functions, and maybe a `cond/3`) and application, then we can construct reduction out of recursion, and then the rest of the jq prelude. jq is very close to a calculus as it is.
In particular how to add unification to jq... here's my thoughts:
- add a unification operator, like `?=`, so `lhs ?= rhs | e` would evaluate `e` with all the unified bindings in `lhs` and `rhs` when the equation is true -- the `lhs` and `rhs` would have to be destructuring binders, not regular expressions
- to evaluate the lhs and rhs evaluate all of the rhs for each value produced by the lhs, and then whenever their binders are equal execute the downstream expression `e`
This could be optimized so that as the VM evaluates the rhs it would prune the evaluation as soon as a binding does not match the binding established by the lhs. Right, the evaluation of the rhs can proceed as usual but it wouldn't establish new bindings but, rather, whenever it would have had it been the lhs just check that the binding to be established matches the one currently established, and if not then backtrack immediately.
A bit brute force, being O(N^2), but hey, first the jq programmer can arrange things so that the pruning behavior yields better performance than N^2, and second the compiler could learn to reason about the lhs and rhs and come up with better solutions, though at the cost of compile-time (which for an interpreted language is not unimportant).
swatson741 · 42d ago
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?
cryptonector · 41d ago
> My specific concern is that by having logical semantics in a language you can represent non-deterministic ambiguous computations
As I understand it the verse calculus can only represent non-deterministic unambiguous computations, and that follows from confluence. The point is that it's the non-determinism that's useful, not ambiguity. Am I understanding correctly?
swatson741 · 40d ago
The paper has this to say:
> Choice is a fundamental feature of all functional logic languages. In VC, choice is expressed in the syntax of the term (“laid out in space”) rather than, as is more typical, handled by non-deterministic rewrites and backtracking (“laid out in time”). This makes VC completely deterministic, unlike most functional logic languages which are non-deterministic by design (Section 6.1).
So, the language is deterministic which is a result of being confluent. And going to section 6.1 as suggested says this:
> In contrast, our rules never pick one side or the other of a choice. And yet, (3 +(20 | 30)) can still make progress by floating out the choice (rule choose in Fig. 3), thus (3 +20) | (3 +30). In effect, choices are laid out in space (in the syntax of the term), rather than being explored by non-deterministic selection. Rule choose is not a new idea.
So the syntax is "ambiguous" and given context with "choose" to make it unambiguous.
To answer your question more plainly it's the ambiguity that's important. Non-determinism usually follows as a natural consequent.
However, it may be a hinderance or it may be desired. Usually we're only interested in one single useful result. But, if I do a search in a data structure for all occurrences of X, and there are 5 of them then I may want a result of all 5 occurrences of X.
cryptonector · 40d ago
> So, the language is deterministic which is a result of being confluent. And going to section 6.1 as suggested says this:
Non-determinism in programming language theory does not mean _physical_ non-determinism.
> To answer your question more plainly it's the ambiguity that's important. Non-determinism usually follows as a natural consequent.
Non-determinism in programming language theory does not require ambiguity. Non-determinism here means something more like that the program's execution will search for matching solutions as if it knew them non-deterministically, but the search process will be deterministic (and it's almost invariably a depth-first search).
discarded1023 · 42d ago
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`.
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
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.
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.
I notice that they reference Icon. They don't reference jq (well, there's no publications on jq to reference).
There was a big splash about this when it came out in 2023, with big names like Simon Peyton-Jones, Lennart Augustsson, and Guy Steele involved. But since then I've heard nothing. Apparently still Fortnite-only, not built into the Unreal Engine. I'm not wired into the gamedev world, is anything happening here?
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
After Epic's wild success hes now got a bit of cash to splash on making his dream a reality :-)
It looks like it's currently down (not sure if a glitch or what).
A few nits on section 6.6:
- difference (2) is just a limitation of Icon that no collect() primitive is provided, but a) it could have been, and b) one can build one:
which is not unlike the situation in jq where there is a built-in array collector `[exp]` but one could build one with `reduce` like so: Of course, the jq `[exp]` collector internally works a lot like the above `collect()`, which is what one might expect, and I would expect that the verse calculus `all` would also work this way (when "run in the forwards direction" anyways).- difference (3) is not quite true in that there are reversible assignments in Icon where backtracking undoes the assignment, but TFA's point is probably really about the existence of non-reversible assignments _at all_. (jq only has reversible lexical assignments called bindings, and does not have non-reversible assignments.)
- I suppose there is a difference that is not listed: Icon lacks unification, so it cannot solve equations backwards like the verse calculus can. (This is also the case in jq.) This was very much worth mentioning!
Note that jq can be condensed into a much simpler prelude that begins to look like a calculus. Note also that jq does not have implicit cuts, which was probably a mistake.
VC is just a calculus, and as such there are no performance concerns. Still, I find it weird that `all` is essentially a collector operation, and that's the only way to "get all the outputs" of an [generator] expression. In jq, because the jq executable itself outputs all the values of the given jq expression [applied to every input to the jq executable, unless -n is given] there is no need to collect all outputs in order to do something with them. What this amounts to is that the jq programmer can trivially implement list fusion, for example, as jq expressions are by default online, and you only lose the online property if you resort to collecting values.
I've not yet looked at the Verse programming language, but I would hope that the language -unlike the calculus- does not force one to give up the online property all the time like VC does.
OTOH, the `one`<->`all` duality is quite elegant -- a tour de force, and a great insight.
This has me wondering how to add unification to jq, or even what a jq calculus might look like.
For example, we can cut the jq language way down, removing even `reduce`, array and object constructor syntax, array and object index syntax, and even `if`, and have just values, expressions, very few built-ins (like `empty/0`, `first/1`, array and object constructor and indexer functions, and maybe a `cond/3`) and application, then we can construct reduction out of recursion, and then the rest of the jq prelude. jq is very close to a calculus as it is.
In particular how to add unification to jq... here's my thoughts:
- add a unification operator, like `?=`, so `lhs ?= rhs | e` would evaluate `e` with all the unified bindings in `lhs` and `rhs` when the equation is true -- the `lhs` and `rhs` would have to be destructuring binders, not regular expressions
- to evaluate the lhs and rhs evaluate all of the rhs for each value produced by the lhs, and then whenever their binders are equal execute the downstream expression `e`
This could be optimized so that as the VM evaluates the rhs it would prune the evaluation as soon as a binding does not match the binding established by the lhs. Right, the evaluation of the rhs can proceed as usual but it wouldn't establish new bindings but, rather, whenever it would have had it been the lhs just check that the binding to be established matches the one currently established, and if not then backtrack immediately.
A bit brute force, being O(N^2), but hey, first the jq programmer can arrange things so that the pruning behavior yields better performance than N^2, and second the compiler could learn to reason about the lhs and rhs and come up with better solutions, though at the cost of compile-time (which for an interpreted language is not unimportant).
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?
As I understand it the verse calculus can only represent non-deterministic unambiguous computations, and that follows from confluence. The point is that it's the non-determinism that's useful, not ambiguity. Am I understanding correctly?
> Choice is a fundamental feature of all functional logic languages. In VC, choice is expressed in the syntax of the term (“laid out in space”) rather than, as is more typical, handled by non-deterministic rewrites and backtracking (“laid out in time”). This makes VC completely deterministic, unlike most functional logic languages which are non-deterministic by design (Section 6.1).
So, the language is deterministic which is a result of being confluent. And going to section 6.1 as suggested says this:
> In contrast, our rules never pick one side or the other of a choice. And yet, (3 +(20 | 30)) can still make progress by floating out the choice (rule choose in Fig. 3), thus (3 +20) | (3 +30). In effect, choices are laid out in space (in the syntax of the term), rather than being explored by non-deterministic selection. Rule choose is not a new idea.
So the syntax is "ambiguous" and given context with "choose" to make it unambiguous.
To answer your question more plainly it's the ambiguity that's important. Non-determinism usually follows as a natural consequent.
However, it may be a hinderance or it may be desired. Usually we're only interested in one single useful result. But, if I do a search in a data structure for all occurrences of X, and there are 5 of them then I may want a result of all 5 occurrences of X.
Non-determinism in programming language theory does not mean _physical_ non-determinism.
> To answer your question more plainly it's the ambiguity that's important. Non-determinism usually follows as a natural consequent.
Non-determinism in programming language theory does not require ambiguity. Non-determinism here means something more like that the program's execution will search for matching solutions as if it knew them non-deterministically, but the search process will be deterministic (and it's almost invariably a depth-first search).