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

[discarded1023]

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

[nextos]

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.

[atombender]

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]

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]

I'm fascinated that Epic Games are the authors. Does anyone know what their motivation for this research would be?

[troupo]

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

[woolybully]

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]

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]

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.

[swatson741]

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]

> 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?

[discarded1023]

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