-
💬 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.
-
🦀 If you like this concurrent paradigm, and want to use it in a real programming language, check out my Rust crate with the same name: Par. It's a full implementation of session types, including non-deterministic handling of many clients.
🚀 Get started with the Language Reference
It contains a full guide of the language and its type system.
A live-stream tutorial on a slightly out-dated version of Par is also up on YouTube.
To run the playground:
- Install Rust and Cargo.
git clone https://github.com/faiface/par-lang.gitcd par-langcargo run
💡 Examples
Open an example in the interactive playground, and play with any function.
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.
Some features that require special syntax in other languages fall naturally out of the basic building
blocks above. For example, constructing a list using the generator syntax, like yield in Python,
is possible by operating on the dual of a list:
dec reverse : [type T] [List<T>] List<T>
// We construct the reversed list by destructing its dual: `chan List<T>`.
def reverse = [type T] [list] chan yield {
let yield: chan List<T> = list begin {
.empty! => yield, // The list is empty, give back the generator handle.
.item(x) rest => do { // The list starts with an item `x`.
let yield = rest loop // Traverse into the rest of the list first.
yield.item(x) // After that, produce `x` on the reversed list.
} in yield // Finally, give back the generator handle.
}
yield.empty! // At the very end, signal the end of the list.
}
Automatically parallel execution. Everything that can run in parallel, runs in parallel. Thanks to its semantics based on linear logic, Par programs are easily executed in parallel. Sequential execution is only enforced by data dependencies.
Par even 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.
This (session) type fully describes the behavior of a player of rock-paper-scissors:
type Player = iterative :game {
.stop => ! // Games are over.
.play_round => iterative :round { // Start a new round.
.stop_round => self :game, // End current round prematurely.
.play_move => (Move) { // Pick your next move.
.win => self :game, // You won! The round is over.
.lose => self :game, // You lost! The round is over.
.draw => self :round, // It's a draw. The round goes on.
}
}
}
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.
// An iterative type. Constructed by `begin`/`loop`, and destructed step-by-step.
type Stream<T> = iterative {
.close => ! // Close this stream, and destroy its internal resources.
.next => (T) self // Produce an item, then ask me what I want next.
}
// An infinite sequence of `.true!` values.
def forever_true: Stream<either { .true!, .false! }> = begin {
.close => ! // No resources to destroy, we just end.
.next => (.true!) loop // We produce a `.true!`, and repeat the protocol.
}
*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 begin turns this check
off. Vast majority of code doesn't need to opt-out of totality checking, it naturaly 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.
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.
Par is a fresh project in early stages of development. While the foundations, including some apparently advanced features, are designed and implemented, some basic features are still missing.
Basic missing features:
- Strings and numbers
- Replicable data types (automatically copied and dropped)
- External I/O implementation
There are also some advanced missing features:
- Non-determinism
- Traits / type classes
There's still so much to be done! If this project speaks to you, join us on Discord.