The Verse Calculus: A Core Calculus for Functional Logic Programming [pdf]

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.

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 :-)

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.

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.

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).