Of course, the intrinsic parallelism is useful there (especially since it is emergent from the structure of the program, rather than needing to be explicitly written). In terms of other interesting properties: interaction nets don't rely on linear memory, instead being based on a graph, which can naturally be chunked and distributed across machines, with synchronization only being necessary when wires span different chunks.

> And synchronization primitives?

The initial answer to this question is: interaction nets don't need synchronization primitives, as all parallelism is emergent from the net structure.

Now, in practice, one may want some additional synchronization-esque primitives. For example, a parallel shortcircuiting or is not expressible in vanilla interaction nets (as all computation is deterministic, and such an operation isn't deterministic). There are extensions to interaction nets for non-determinism, that allow some of these use-cases, which start to look more like synchronization primitives. Vine doesn't support any of these at the moment, but it may in the future.

> I wanted to also say I loved reading the documentation. Your idea of places, spaces and values feels like a waaay more intuitive naming scheme for than what's common in CS.

I'm glad to hear it! I spend a lot of time trying to come up with good names for things, so it's nice to know that that pays off. Though I suppose it's not too hard to improve on the status quo, when it's 'lvalue'/'rvalue', lol. (I did, however, steal 'place' and 'value' from Rust.)

> The time-travel example also felt oddly intuitive to me. I don't really care that it uses black magic underneath, it's quite elegant!

Yeah, the 'time-travel' stuff sounds wacky, but I do think it can be really intuitive if one is willing to accept it. I wrote a really cool algorithm a little while ago that really uses this 'time-travel' idea; I [wrote about it](https://discord.com/channels/1246152587883970662/12461564508...) on Discord. (I should really type that up into a blog post of sorts.

The key reason one may consider interaction nets to be more parallelisable than lambda calculus is that the key evaluation operation is global in lambda calculus, but local in interaction nets. The key evaluation operation in labmda calculus is (beta) reduction. For instance, if one evaluates a lambda term `(\n -> f n n) x`, reduction takes this to the term `f x x`. To do so, one must duplicate the entire term `x` from the argument to perform the computation, by either 1) physical duplication, or 2) keeping track of references. Both are unsatisfactory solutions with many properties hindering parallelism. As I shall explain, the term `x` may be of unbounded size or be intertwined non-locally with a large part of the control graphs of other terms.

If `x` is simply a ground term (i.e. a piece of data), then it seems like either duplication or keeping track of the references would be an inevitable and reasonable cost, with the usual managed-language issues of garbage collection. If one decides to solve the problem by attempting to force the argument to be a ground term, one would find the only method to be to impose eager evaluation, evaluating terms by always first evaluating the leaf of the expression, before evaluating internal nodes in the expression. Eager evaluation can easily become unboundedly wasteful when one strives to reuse a general computation for some more specific use cases, so one may not prefer an eager evaluation doctrine.

However, once one evaluates in an order that is not strictly eager (e.g. lazy evaluation), the terms that one is duplicating or referencing are no longer simple pieces of data, but pieces of a (not necessarily acyclic) control graph, and any referencing logic quickly becomes very complicated. Moreover, the argument `x` could also be a function, and keeping track of references would involve keeping track of closures over different variables and scopes, which complicates the problem of sharing even further.

Thus, either one follows an eager evaluation order, in which most of the nodes in a term's expression tree are not available for evaluation yet, and available pieces of work for evaluation are only generated as evaluation happens, which imposes a global and somewhat strict serialised order of execution, or one deals with a big complicated shared graph, which is also inconvenient to be distributed across computational resources.

In contrast with lambda calculus, the key evaluation operation in interaction nets is local. Interaction nets can be seen as more low-level than lambda calculus, and both code and data are represented as graphs of nodes to be evaluated. Thus, a large term is represented as a large net, and regardless of the unbounded size of a term, in one unit of evaluation, only one node from the term's graph is involved.

Given a graph of some 'net' to be evaluated, one can choose any "active" node and begin evaluating right there, and the result of computation in that unit of evaluation will be guaranteed to affect only the nodes originally connected to the evaluated node, no referencing involved. Thus, the problem of computation becomes almost embarrassingly parallel, where workers simply pick any piece of a graph and locally add or remove from that piece of the graph.

This is what is meant when one refers to interaction nets being more parallelisable than lambda calculus.

Yes; you can take the producer side of an `N32` wire `x` and link it to the consumer side of an `N32` wire `y`; that just means that the value that is sent across `y` will be sent across `x`.

> Should ~ be considered part of the type signature? Does `let ~x = y` work as destructuring?

In `let ~x = y`, the `~` is part of the pattern, and is destructuring, yes. So assuming `y` is some `~N32`, that statement declares a new variable `x`, with no initial value, and whatever the final value of `x` is, that's what passed along the wire. So re: what happens when a variable is assigned more than once, the last assignment wins.

IVM is architecturally similar to HVM-64 (which I was the lead developer of). The most major difference is how they handle IO. IVM uses its extrinsic system, where all side effects are mediated through an IO handle, which provides a number of useful properties, and is greatly simpler to implement / use. Interactions with side effects are small and low-cost, and can happen in parallel with the rest of the program.

HVM-64 had built-in net definitions that had side-effects when expanded, which was very messy to use in practice. HVM2 has a monadic IO interface, which requires stopping the whole program on every single IO call. (And also requires writing things monadically.)

Using extrinsics for IO handles in IVM creates a very nice API for IO in Vine; side-effect-ful functions simply take a mutable reference to the IO handle. It's also very easy to support multiple 'threads' of parallel IO effects – simply duplicate the IO handles.