On the relationship to my work

[FranchuFranchu]

This is going to be a very messy post, sorry. There's a lot of topics I'd like to cover.

I've been working with interaction nets for a long time. Interaction nets are a computational model based on graph rewriting, where there nodes interact through their principal ports. There's a problem which I'd like to fix, which is how to add static typing to a language based on interaction nets.

Historically, interaction nets are a generalization of proof nets, which are used to encode linear logic proofs. Thus, it makes sense to attempt to use linear logic to type interaction nets.

This led me to work in linear-nets, a project to design a programming language based on linear logic. The user constructs proof nets, which are then typed using a type inference algorithm. Then, we can compile the proof nets to interaction combinators and use them as a program. My plan is to have a nice user-facing syntax which is then used to build the proof nets. The user-syntax should be as close to the proof net as possible.

Due to the construction properties of proof nets, this ensures that vicious circles never happen (vicious circles are analogous to deadlocks), which is very good.

Now that I've given the context of my post, I'll start commenting on par-lang.

Congratulations on the language! It's very nice and polished.

One of the things that this language does very well is explain the connectedness condition of proof nets (by the fact that two processes are connected by a single channel). With my approach, I'm not sure how I'd explain to the users that the constructed program is not a valid proof net (wrt. error messages and such).

Another thing this does very well is pattern-matching. There is no need to manually write the with terms which are necessary in my approach.

That said, I'm curious about what the plans for a runtime for this language are. I don't know how familiar you are with interaction combinators, but do you think trying to write a par-lang -> interaction combinators compiler is worth it? For example, I don't know how signals are implemented in terms of linear logic, but those could be quite challenging (I haven't read the paper this is based on yet).

I'd like to help and learn more about this project. It's really impressive.

[faiface]

@FranchuFranchu

Thanks a lot for this! Your project sounds fascinating, I'm going to take a closer look tomorrow. Meanwhile, I can answer some things you ask about Par.

I don't know how familiar you are with interaction combinators, but do you think trying to write a par-lang -> interaction combinators compiler is worth it?

I'm actually not familiar with interaction combinators at all, but if they can implement a parallel runtime for linear logic semantics, that sounds extremely promising for a runtime for Par too! A question that immediately pops up is if compiling to interaction nets would not cause problems when trying to do interop, say with Rust, to implement some I/O functionality.

But Par definitely needs a better runtime/compilation. I haven't done benchmarks, but I'm sure it's quite slow. It uses one-shot channels for everything, so you can imagine a lot of channels are created and used all the time. Also, it starts an async coroutine for every process, which, while correct, can also pose an overhead.

For example, I don't know how signals are implemented in terms of linear logic

Signals are my own terminology here, and they correspond to additives in linear logic. In usual linear logic, additives are binary, but here I use the extended version of just naming each variant, and those names are signals. So channel.signal, when used as a command is constructing a "plus" (and .signal expression is doing the same), and matching with channel { signal => { ... } ... } is constructing a "with".

[4ad]

It would be amazing if there was a guide of the translation between linear logic and Par (or the other way around), however informal!

[faiface]

@4ad I can put one together

[FranchuFranchu]

@faiface

compiling to interaction nets would not cause problems when trying to do interop, say with Rust, to implement some I/O functionality.

That would have to be implemented, but it's not a serious problem. It is possible to extend interaction combinators with special side-effectful IO nodes to allow for IO. To be fair, it would definitely be harder to add easy-to-use / transparent FFI, but as long as the language has enough IO capabilities, I don't think it should be a problem.

For example, I don't know how signals are implemented in terms of linear logic

the main problem for compilation to interaction combinators is that the compiler would have to statically know which are the signals that each channel can receive, and from which set of signals each send operation is sending from. I assume this would be fixed by a type system, although perhaps par-lang in its current state already has this capability.

I recommend reading the interaction net and interaction combinator papers I linked in my introduction on the welcome thread. They are very easy to understand, and light on notation.

I'll dive into Par's internals and see how compilation to interaction combinators could be implemented, and where it could be inserte

[faiface]

@FranchuFranchu

To be fair, it would definitely be harder to add easy-to-use / transparent FFI, but as long as the language has enough IO capabilities, I don't think it should be a problem.

I see, and I agree. An FFI is not a goal, but a way to add Rust-controlled objects to be used from Par is a goal. And I see that's probably not going to be a problem.

the compiler would have to statically know which are the signals that each channel can receive, and from which set of signals each send operation is sending from. I assume this would be fixed by a type system, although perhaps par-lang in its current state already has this capability.

This will absolutely be fixed with a type system, but I'm not sure is already doable. A channel only gets to know the full set of signals at the point of receiving a signal (channel { signal1 => ... }). On sending a signal, only the sent signal is known. So, at some point the set of signals is clear, but not before any interaction begins. But I wonder if this would necessarily pose a problem. Perhaps an additional specialized node with a signal name could be created in interaction nets to fascilitate the matching?

On interaction nets: I'm still reading the papers, but it's already absolutely clear to me this is the way to go! Especially since there already is a performant runtime for them, this would provide great performance for the language. So far, my impression is this is the way to go!

The compilation would go like this. The high-level Par is first compiled to a low-level process language (defined in process.rs), which is more-or-less a subset of the high-level Par. This language only has a single expression (aside from direct name references): chan <channel> { <process> }. Everything else in it is process syntax. The compilation to interaction nets would thus go from this low-level process language.

[4ad]

General information about proof nets vs. interaction nets: Yves Lafont (1995), From proof-nets to interaction nets. Proceedings of the workshop on Advances in linear logic (225-247).

A more modern translation of linear logic into interaction nets: Ian Mackie (2000), Interaction nets for linear logic. Theoretical Computer Science, Volume 247, Issues 1–2, 2000, (83-140).

I don't know if this was mentioned already, but this book is a very good and complete introduction to interaction nets, somewhat focused on λ-calculus:

Asperti, Andrea & Guerrini, Stefano. (1998). The optimal implementation of functional programming languages. ISBN-13: 978-0-521-62112-0.

[faiface]

@4ad Thanks for the links!

[FranchuFranchu]

So, at some point the set of signals is clear, but not before any interaction begins. But I wonder if this would necessarily pose a problem. Perhaps an additional specialized node with a signal name could be created in interaction nets to fascilitate the matching?

@faiface Yes, it's a problem. To implement it in pure interaction combinators, we could store the signal name encoded as a tree of interaction combinators in each Choose command. However, this would have a very large overhead when compared to a type-aware solution.

An alternative, as you said, is extending interaction combinators with a special family of nodes which store the signal name internally. The comparison and branching would be done natively which would be better than a solution implemented in interaction combinators. I think this is the best approach if we don't want to implement a type system yet.

[faiface]

@FranchuFranchu A question, is there an advantage in using interaction combinators as opposed to just creating custom interaction nets? By custom I mean a custom set of node names and rules.

[faiface]

@4ad @FranchuFranchu I put together a sketch of a correspondence between linear logic and Par here: #4