# Par is a concurrent language where linear types are the only safety net

> Par is an experimental Rust implementation of a concurrent programming language built on linear logic, where every value must be used exactly once and concurrency is automatic rather than declared. It has no runtime exceptions, no deadlocks and almost no infinite loops, and the escape hatch for the last of those is a keyword called unfounded.

**par-team/par-lang** — Par (⅋) is an experimental concurrent programming language. It's an attempt to bring the expressive power of linear logic into practice.

- Repository: https://github.com/par-team/par-lang
- Website: https://par.run
- Stars: 813 · Forks: 42
- Language: Rust
- License: MIT
- Published: 2026-10-20 · Updated: 2026-10-20 · Language: en
- Canonical page: https://hysenlabs.com/projects/par-team-par-lang

## Every value has to be used exactly once

Par takes its name from the symbol for parallel composition and describes itself as an expressive, concurrent, total language. The README puts the type system first, and it is worth being precise about what that means, because it is not a type system you can bolt onto an existing language.

Par is fully based on linear logic, and the stated aim is to bring the expressive power of linear logic into practice by interpreting linear logic as session types. The language itself descends from a small process language called CP, from the paper Propositions as Sessions by Phil Wadler. The README makes a strong claim about the correspondence: programs in Par correspond one-to-one with linear logic proofs.

The practical consequence of linear typing is that a resource cannot be silently dropped or duplicated. Duality gives two sides to every concept, which the README describes as the source of composability, since whichever angle you take on a problem there will likely be ways to express it.

This is the reason the project exists rather than a feature bolted on. If you have read about linear logic and wanted to see it in practice rather than in proofs, Par is the experiment that does that, and the book at par.run is the entry point.

The repository is Rust, MIT licensed, with the last push on 2026-10-19 and the homepage at par.run.

## Concurrency is automatic because data dependencies decide what runs in parallel

The concurrency story is unusual enough to be the main draw. The README states that everything that can run concurrently does, and that sequential execution is only enforced by data dependencies. The comparison the project uses is that it is as if everything were `async` but nothing needed `await`.

Underneath, Par compiles to interaction combinators, which the README identifies as the basis for HVM and the Bend programming language. So the runtime model is not a promise about scheduling but a translation into a representation that is known to handle concurrency this way.

On top of that sits structured concurrency with session types. Session types describe concurrent protocols, almost like finite state machines, and Par checks that they are upheld in the code. The README makes a point that generalises well beyond Par: linear types are session types, at least in their full version which embraces duality. No special library is needed for this in Par.

Two consequences follow for a reader. Deadlocks are impossible, because structured concurrency rules them out. And you do not choose between sequential and concurrent code paths, since the shape of the data decides. That is a different design contract from the async/await model most languages now use.

## Total means no crashes, no deadlocks and a checked recursion budget

The totality claims are the part most likely to surprise a working programmer, because each one removes a category of runtime failure.

Runtime exceptions are not supported, except for running out of memory. Deadlocks are impossible, as a consequence of the structured concurrency described above. And infinite loops are mostly prevented: by default, recursion using `begin` and `loop` is checked for well-foundedness.

That last point is the subtle one. Well-foundedness checking is a static guarantee that the recursion terminates, and it is what lets the language promise no infinite loops without a timeout or a fuel counter.

The README is honest about where this breaks down. Some algorithms, especially divide-and-conquer, are difficult or impossible to implement using easy-to-check well-founded strategies. For those, `unfounded` turns the check off. The vast majority of code does not need to opt out, because it naturally fits the requirements, and the parts that do are clearly marked with `unfounded`. Those marked parts are the only places that can potentially cause an infinite loop.

So the guarantee is not absolute, it is a static default with an explicit, greppable escape hatch. That is a workable design, and the escape hatch being named and visible is what makes it tolerable.

## Recursive and iterative types are separate, and the type list is unusually wide

Par distinguishes iterative, co-recursive and potentially infinite types from recursive ones, which the README says are finite. The point of the separation is that iterative types let you construct potentially unbounded objects, such as infinite sequences, with no danger of an infinite loop and no need to opt out of totality checking. A recursive type that happens to be infinite and an iterative type that is allowed to be infinite are different things, and the language keeps them apart.

The list of first-class structural types is broader than most languages manage. Pairs, which the README says are easily extensible to tuples, sit next to functions, which are naturally curried. Eithers, the sum types, sit next to choices, which the README describes as unusual but powerful dispatchers. Recursive types sit next to iterative ones with totality checking. Universally and existentially quantified generic functions and values are both present. Unit and continuation close the list.

The README's term for this is orthogonal concepts, and it claims that they combine to give a rich world of types and semantics.

Choices are worth a second look, since they are the least standard entry. A choice provides multiple ways to take apart a value, where an either gives exactly two alternatives. Whatever the exact operational meaning, the design goal is stated plainly: whichever angle you approach a problem from, you should find a way to express it.

## Building Par from the workspace, with a playground feature behind a flag

The repository is a Cargo workspace, and the workspace definition is minimal:

```toml
[workspace]
members = ["crates/par-core", "crates/par-builtin", "crates/par-doc"]
```

The root package is the compiler binary itself:

```toml
[[bin]]
name = "par"
path = "src/main.rs"
```

Note that the workspace lists three members while the root package depends on four local crates, including par-runtime, so the runtime lives outside the explicit workspace member list. The dependency list in the root manifest shows the shape of the tool: a web stack built on hyper, hyper-util, reqwest and tokio-util, a parser generator in winnow, diagnostics from miette, an LSP server and types for editor support, serde and serde_json plus bincode for data handling, clap for the command line, and tracing for diagnostics.

The playground is a feature, and it is on by default:

```toml
[features]
default = ["playground"]
playground = ["eframe", "egui_code_editor", "rfd", "par-core/playground", "par-runtime/playground"]
```

The playground pulls in eframe and egui_code_editor, which are desktop GUI and editor crates, and rfd for file dialogs. That combination explains the presence of index.html, Trunk.toml and playground-examples/ in the tree, since a browser playground and a native one are built from the same language.

The README does not give a build or install command, so the documented route in is the book at par.run, and there is a VS Code extension published in the marketplace for editor support.

## The examples are where the language actually gets evaluated

The repository carries example programs rather than a standard library tour, and they are the closest thing to a use case guide.

There is a chat room in the browser under examples/big/chat/, a downloader under examples/big/downloader/ that downloads files with live progress and supports cancelling on a web page, and a task list under examples/big/tasks/ that runs in the browser and stores its state in SQLite. The smaller examples live under examples/small/src/ and cover individual features, including a Sokoban game in the terminal.

The two larger ones are the interesting demonstrations. A downloader with progress and cancellation is a concurrency program with real backpressure, which is the kind of thing the automatic concurrency model either handles well or does badly, and a browser-based chat room exercises the session type side, since a chat protocol between two parties is close to what session types describe.

There are also two videos linked from the README. One codes a Mini Grep in Par, and the other asks what it would mean if everything were async but nothing needed await, which is the project's own framing of the concurrency model. The README points to the book, the VS Code extension, and the examples directory, and invites questions on Discord or through the GitHub Discussions forum.

One funding note is worth carrying into any evaluation. The README states that Par is currently funded by motivation alone and asks for sponsorship to make it viable long term.

## Conclusion

Adopt Par if you are studying linear logic in practice, teaching concurrent programming, or prototyping where the discipline of using every value once removes whole classes of bug, and you are willing to accept a language whose package version is still 0.1.0 with no GitHub releases. Skip it if you need production tooling, a stable package set, or a language that lets an unused value slide by, because Par's central rule is that it cannot. Verify first that your algorithm can be expressed with well-founded recursion, since divide-and-conquer patterns are the documented cases where you must reach for unfounded.

## FAQ

### What makes Par different from other concurrent languages?

The README says everything that can run concurrently does, and sequential execution is only enforced by data dependencies, as if everything were async but nothing needed await. Par compiles to interaction combinators, the basis for HVM and Bend.

### Can Par programs crash or deadlock at runtime?

Runtime exceptions are not supported, except for running out of memory, and the README states that the structured concurrency of Par makes deadlocks impossible. Infinite loops are prevented by default through well-foundedness checking on recursion.

### When do I need the unfounded keyword in Par?

The README says some algorithms, especially divide-and-conquer, are difficult or impossible to implement with easy-to-check well-founded strategies, and unfounded turns the totality check off for those. The vast majority of code does not need it, and the parts that do are clearly marked.

## Sources

- [Issues](https://github.com/par-team/par-lang/issues)
- [License: MIT](https://github.com/par-team/par-lang/blob/main/LICENSE)
- [par-team/par-lang on GitHub](https://github.com/par-team/par-lang)
- [Project website](https://par.run)
- [README](https://github.com/par-team/par-lang/blob/main/README.md)

---

Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/par-team-par-lang