Lambda the Ultimate

Logic variables behave like disjoint sets (union/find algorithm). This may reduce to "can you write an efficient union find in a pure functional way". You can have immutable logic variables with atoms as you only change the disjoint set links. Logic variables could be represented as an edge list. With committed choice you only add edges to the list, if you push new edges onto the head of the list, backtracking is just returning some tail of the list. I don't know if this answers the question, but it seems significant to me that there is a functional representation of logic variables.

A purely functional language with an affine vector type can implement efficient union-find, e.g. using the normal single-threaded imperative algorithms.

I plan to support this in my own language. Under the hood, updating a vector will simply peek at a reference count to decide whether it's uniquely owned, and copy if not. An affine type isn't required, but would help a developer enforce this discipline (preventing accidental copies). As I understand it, support for efficiently updating a vector is, by itself, sufficient for efficient union-find.

I also plan to support efficient splits and unsplits on affine (single refct) vectors. Split is obvious. For unsplits: when you append two affine vectors that were originally split from same affine vector, and those vectors have adjacent storage, they can rejoin seamlessly. Splits and unsplits should greatly help with parallel computations, in-memory sorts, etc..

A few little tricks like this can give FP performance on par with machine-level imperative programming, while preserving simple semantics.

"FP performance … while preserving simple semantics"

That's only simple if your semantics don't describe performance, not even at an abstract big-Oh level. I've spent a lot of time in systems with a lot of dynamic dispatch, and I'm comfortable with a fair amount of ad hoc polymorphism, but constant-time versus linear-time split/join seems like something for which I'd want a static guarantee.

Random hiccups deep in the call graph because some random piece of data is shared 1% of the time makes for really hard to debug performance issues. That's definitely true if coders can't ask for a static guarantee on linear-ness, but also true when coders can ask for such a guarantee but don't. We tend to fix problem we know exist (by testing) rather than proving the absence of certain issues, and implicit optimistic constant time joins can cause variable performance characteristics.

I agree that performance should be predictable, comprehensible, easy to debug. OTOH, I don't want a bunch of semantic clutter, tons of built-in types, floating point you can call it 'semantics' if you are generous, etc..

If I want a static guarantee that a program introduces no sharing, a nice constructive option is to write a DSL to write my program. OTOH, if I just want to debug a problem, I might write a function "unsharedAppend" and inject a runtime assertion that the two lists are unshared and adjacent, then disable the assertions when I'm confident my program is correct.

While my language has substructural types, those are currently enforced dynamically. I plan to eventually work on a good static typechecker or linter or something like SHErrLoc. But it isn't a high priority for me.

Testing can be vastly more effective than it is today. The common edit-compile-test cycle has a huge lag between tweak and observation. It's difficult to model user interactions in a first-class way in. Testing doesn't preserve information from previous application sessions. It's difficult to freeze and fork an application and try multiple progressions. And it's difficult to 'visualize' evaluation state or context in most languages. Many problems are subtle that could, in a better testing environment, be obvious.

In your example: if we just colored vectors based on sharing, we'd immediately see the problem. If we further animated the evaluation, we'd quickly discover where the sharing was introduced.

I don't see any need to give up on testing and optimistic simplicity. Proof is great, too, of course. Let's do more of that. I'd love to use EDSLs that construct code together with a proof of correctness. But we can also do a lot more with testing, especially with a simple language that is consequently easier to tool.

I want the folks who are obsessed about static typing to get that working ever better. I want the people who prefer dynamic/testing approaches to get that working even better.

But then I want both those things to be able to cohabitate in a programmning environment. I want to be able to bring *all* and *any* powers to bear whenever and wherever I decide to.

So my main beef is that we don't seem to have a Really Good skeleton for all these things to happen on, so they can work together on *my* machine. Things like Typed Racket seemed nice, but I've heard now and then that it isn't all as smooth perfect great idealistic sailing as one would really want for a day job.

I didn't really follow your first comment: I dug out an old paper on Alms to see how they had used affine vectors to handle vector updates - they have a scheme that allows multiple readers along with a single exclusive writer. I couldn't see what you meant about how this could could allow an efficient union-find algorithm.

Are you assuming union-find calls in a single thread? The main source of inefficiency would be taking O(n) time to update the tree roots, rather than the O(1) in an imperative setting where one cell in the array is overwritten. Which scope owns the unique copy of the vector to allow this to occur?

I'm also slightly confused by the unsplit operation that you refer to - does this assume that there are no collisions among the updates? So that if I hand a unique copy to two writers I need some kind of proof that they will only make disjoint accesses into the array. If they both alias the same cells then it is not obvious how to do the merge.

A few little tricks like this ...

All tricks are little once you know how they work, but quite intriguing until that point. It would be interesting if you could unpack it a little for someone who has not come across it before.

An affine vector has a single owner, e.g. just one thread. But we can divide an affine vector into two smaller affine vectors, and give each a distinct owner (via pure par-seq parallelism). Later, we can append the affine vectors back into one larger affine vector without copying. The latter requires a representation trick: our runtime peeks at the underlying buffer, recognizes the adjacent addresses. We could guard this otherwise ad-hoc trick via types, annotations, or assertions.

By splitting, updating, and appending affine vectors, we get easy access to imperative algorithms that use divide and conquer techniques. For example, in-place parallel quick sort is entirely feasible in a hopefully obvious way.

Parallelizing union-find is trickier.

The goal is to parallelize processing on a set of union inputs while performing as much path compression as feasible. Trivially, if we have a conveniently indexed set of unions, we can parallelize processing on fragments of the array. But unless we have a lot of locality of union relationships, we won't have much work to do within the segments.

Fortunately, we can usually develop a good set of probabilistic assumptions about locality. Many structures are aligned with physical surfaces or volumes (image data, geographic, etc.). In the OP case, we have a lot of alignment with modules and processes. We can align our elements in the array based on locality. A Z-order curve trivially handles spatial locality, for example. When processing the union data, then, we can systematically parallelize work on each segment and separately apply a (probably much smaller) subset of 'long-range' relationships between segments.

Of course, all this assumes our set of unions is conveniently indexed. If it's an unordered stream mixed in an ad-hoc way with finds, we'll be stuck with single-threaded processing. We still benefit, though: we're doing just as well as would the best imperative code, instead of using IntMaps or some other conventional FP solution that burns GC and breaks memory locality.

Aside:

Where imperative algorithms still benefit is the potential for ad-hoc communication between workers. Interestingly, we can also model this in a pure FP solution, e.g. break the same affine vector down but also model message passing between workers on separate segments. But in a strict FP language, a parallel computation must return a request for desired communications to its parent, which may shuffle data around then start a new set of parallel computations. So the amount of parallelism is reduced.

Affine vectors don't help in this case, but it is feasible to improve communication between parallel computations in a purely functional system. For example, we can a model lazily computed lists where one worker is computing the end of the list while another is processing the head. This list allows the runtime to pipeline communications between parallel computations instead of returning to a 'parent' computation that can perform the communication on behalf of the worker.

There was a cool paper with something like "Escape from the Zorg" in the title, about people switching their logic-programming course from Prolog to Haskell, reporting that they found the explicite-ness of having to use a search monad made it easier for students to understand what was going on -- that the sheer "magic" of Prolog's search semantics. I looked for it to post in this conversation, but wasn't able to find it again. That's one problem with cool titles referencing something that exists, you become harder to search for.

Found it here. Along the way I came across this, which contains a simple prolog interpreter written in Haskell.