par-lang

Par is an expressive, concurrent, total* language

...with linear types and duality

• Join our Discord, or use the Discussions as a forum to ask questions and share ideas!

• If you'd like to support my effort to bring the power of linear logic into practical programming, you can do it via GitHub Sponsors.

Get started with the Book

️ VSCode extension

Videos

• What’s a linear programming language like? — Coding a “Mini Grep” in Par
• What if everything was "Async", but nothing needed "Await"? | The Par Programming Language

Check out the examples

✨ Features

Expressive

Duality gives two sides to every concept, leading to rich composability. Whichever angle you take to tackle a problem, there will likely be ways to express it. Par comes with these first-class, structural types:

(Dual types are on the same line.)

• Pairs (easily extensible to tuples), and functions (naturally curried).
• Eithers (sum types), and choices (unusual, but powerful dispatchers).
• Recursive (finite), and iterative (co-recursive, potentially infinite) types, with totality checking.
• Universally, and existentially quantified generic functions and values.
• Unit, and continuation.

These orthogonal concepts combine to give rise to a rich world of types and semantics.

Concurrent

Automatically concurrent execution. Everything that can run concurrently, does! Sequential execution is only enforced by data dependencies. It's as if everything was async, but nothing needs await.

Par compiles to interaction combinators, which is the basis for the famous HVM, and the Bend programming language.

Structured concurrency with session types. Session types describe concurrent protocols, almost like finite-state machines, and make sure these are upheld in code. Par needs no special library for these. Linear types are session types, at least in their full version, which embraces duality.

️ Total*

No crashes. Runtime exceptions are not supported, except for running out of memory.

No deadlocks. Structured concurrency of Par makes deadlocks impossible.

(Almost) no infinite loops.* By default, recursion using begin/loop is checked for well-foundedness.

Iterative (corecursive) types are distinguished from recursive types, and enable constructing potentially unbounded objects, such as infinite sequences, with no danger of infinite loops, or a need to opt-out of totality.

*There is an escape hatch. Some algorithms, especially divide-and-conquer, are difficult or impossible to implement using easy-to-check well-founded strategies. For those, unfounded turns this check off. Vast majority of code doesn't need to opt-out of totality checking, it naturally fits its requirements. Those few parts that need to opt-out are clearly marked with unfounded. They are the only places that can potentially cause infinite loops.

Theoretical background

Par is fully based on linear logic. It's an attempt to bring its expressive power into practice, by interpreting linear logic as session types.

In fact, the language itself is based on a little process language, called CP, from a paper called "Propositions as Sessions" by the famous Phil Wadler.

While programming in Par feels just like a programming language, even if an unusual one, its programs still correspond one-to-one with linear logic proofs.

Come help us!

There's still so much to be done! If this project speaks to you, join us on Discord.

Support the project!

Par is currently funded by motivation alone. Only your support can make it viable long-term. Consider sponsoring.