Introduction

Par (⅋) is a concurrent programming language bringing the expressive power of linear logic into practice.

This reference contains not only the complete grammar and specification of Par but also an extensive collection of examples, explanations and best practices.

Overview

Par is a multi-layer language with an intermediate representation in itself.

A simple program like

type HW = either { .hello_world! }

def main: HW = .hello_world!

is compiled to a program fully written in process syntax:

type HW = either { .hello_world! }

def main: HW = chan user {
  user.hello_world
  user!
}

Par is centered around concurrency and session typing, all in the framework of linear logic. What does that mean?

• Types are linear, i.e. a value must be used exactly once. You might know the type system of Rust, where a value must be used at most once.
• Ultimately, everything in Par is a channel.
  • A list sends every item in order and then closes
  • A function receives its argument and becomes the result
  • An infinite stream can be signaled to either yield the next item or close
• Channels communicate with each other by
  • sending signals (the names with a dot in front)
  • sending values
  • closing each other
• Everything has a dual in Par: A value can be created by destroying its dual (see channel expressions)
• This can all be abstracted away in expressions and types or be exposed as statements in process syntax.

Putting all of this together, Par manages to be a functional language while also allowing imperative-style code and mutability.

For example, a mutable stack can be implemented like this (explanation):

type Bool = either { .true!, .false! }
type List<T> = recursive either { .empty!, .item(T) self }
type Option<T> = either { .none!, .some T }

type Stack<Unwrap, T> = iterative {
  .push(T) => self
  .pop => (Option<T>) self
  .unwrap => Unwrap
}

dec list_stack : [type T] [List<T>] Stack<List<T>, T>
def list_stack = [type T] [list] begin {
  .push(x) => let list: List<T> = .item(x) list in loop
  .pop => list {
    .empty! => (.none!) let list: List<T> = .empty! in loop,
    .item(head) tail => (.some head) let list = tail in loop
  }
  .unwrap => list
}

def main = do {
  let list: List<Bool> = .empty!
  let stack = list_stack(type Bool)(list)
  // stack currently represents an empty list

  // the following operations mutate stack
  stack.push(.true!)
  // stack now represents a singleton of .true!
  stack.push(.false!)
  // stack now represents a two-element list
} in stack

Running this in the playground you can push and pop elements, or inspect the underlying data using unwrap.

For a complete tutorial, see the Readme

Getting Started

To use Par, clone the repository

$ git clone https://github.com/faiface/par-lang.git

and run the app

$ cd par-lang
$ cargo run

Note: If you don’t have Rust and Cargo installed, do that first

This will launch the Par playground. Some example code is already written for you. Just press Compile and Run to run any definition from the program on the left.

Community

To ask questions or discuss ideas, join our Discord.

Lexical Structure

Comments

^Lexer
LINE_COMMENT :
      // (~\n)^*

BLOCK_COMMENT :
      /* (BLOCK_COMMENT | ~*/)^* */

Comments have no effect on the program.

// This is a line comment

/*
 * And this is a multiline (block) comment.
 * The stars on the left are purely for aesthetics
 */

Names

^Lexer
ID :
      (ID_START ID_CONT^*)_{Expect keywords}

ID_START :
      [a-z A-Z]

ID_CONT :
      [_ a-z A-Z 0-9]

^Syntax
ID_List :
      ID (, ID)^* ,^?

Some valid identifiers are:

• snake_case
• PascalCase
• letters123

Some invalid identifiers are:

• chan, a keyword
• 3D, starts with a number
• kebab-case, same as kebab - case

Keywords

Punctuation

Whitespace

Whitespace in Par serves merely the purpose of separating tokens. Whitespace characters are:

• The whitespace ' '
• Tabs '\t', '\v'
• Newline '\n'
• Carriage return '\r'

Source Files

^Syntax
ParFile :
      Item^*

This rule is the entry point for every file written in Par.

Currently, every Par program consists entierely of items:

• Type definitions

  type TypeName = SomeType
  

• Value definitions and declarations

  // type and value together
  def name: Type = value
  
  // separate type declaration
  dec name : Type
  def name = value
  

Items

^Syntax
Item :
      TypeDefinition
   | Declaration
   | Definition

Items are the primary building block of Par programs.

Definitions

^Syntax
Declaration :
      dec ID : Type

Definition :
      def ID Annotation^? = Expression

def defines a global definition usable throughout the file in which it was defined. It can be used as many times as one desires, instantiating itself every time it’s used.

// define a static value
dec unit : !
def unit = !
// or all-in-one
def unit: ! = !

// define a function
def negate: [Bool] Bool = [b] b {
  .true! => .false!
  .false! => .true!
}

// define a function receiving types
dec pop : [type T] [List<T>] (Option<T>) List<T>
def pop = [type T] [list] list {
  .empty! => (.none!) .empty!
  .item(head) tail => (.some head) tail
}

Type Definitions

^Syntax
TypeDefinition :
      type ID TypeParameters^? = Type

TypeParameters :
      < TypeParameter (, TypeParamter)^* ,^? >

TypeParameter :
      ID

A type definition defines a type alias, not a “new type”. All types in Par are structural.

// simple type alias
type Boolean = Bool

// the definition of Bool
type Bool = either {
  .true!
  .false!
}

// parameterized type alias
type Option<T> = either {
  .none!
  .some T
}

Types

At the heart of Par lies its type system, representing linear logic.

^Syntax
Type :
      NamedType
   | Unit
   | PairType
   | FunctionType
   | EitherType
   | ChoiceType
   | RecursiveType
   | IterativeType
   | ExistentialType
   | UniversalType
   | Bottom
   | ChannelType
   | Self

Self :
      self LoopLabel^?

TypeList :
      Type (, Type)^* ,^?

TypeArguments :
      < TypeList >

Annotation :
      : Type

Label :
      . ID

Named Types

^Syntax
NamedType : ID TypeArguments^?

Defined via type aliases, named types can always be replaced with their definition without changing meaning.

let x: Option<T> = .none!
// is equivalent to
let x: either { .none!, .some T } = .none!

The Unit Type

^Syntax
Unit : !

^{Dual | Constructing Expression | Pattern | Constructing Statement | Destructing Statement}

Unit is a type providing no information. In C(++) it’s called void, in Rust it’s () (and it can be thought of as an empty tuple in Par as well). There is exactly one value of type !, and it’s also !.

let unit: ! = !

Every value of a type A corresponds to a function [!] A:

def select: [type T] [T] [!] T = [type T] [x] [!] x
// uncurrying makes this clear
// [T] [!] T = [T, !] T ≅ [(T) !] T ≅ [T] T

def extract: [type T] [[!] T] T = [type T] [f] f(!)

For some types there is a function [A] !. Those can be destroyed without any transformation.

// Types constructed only from ! are droppable
def drop_bool: [Bool] ! = [b] b {
  .true! => !
  .false! => !
}

// Functions are not droppable in general
def drop_impossible: [[Bool] Bool] ! = todo

Mathematically, ! is \(\mathbf{1}\), the unit for \(\otimes\).

Pair Types

^Syntax
PairType : ( TypeList ) Type

^{Dual | Constructing Expression | Pattern | Constructing Statement | Destructing Statement}

Having multiple types between ( and ) is just syntax sugar:

type T = (A, B) R
// is equivalent to
type T = (A) (B) R

While (A, B)! and (A) B are both valid ways to define a pair of A and B, depending on the context, one might be more convenient than the other:

// convert (A, B)! into (A) B
def i : [(A, B)!] (A) B = [x]
  let (a, b)! = x in (a) b
// and back
def j : [(A) B] (A, B)! = [x]
  let (a) b = x in (a, b)!

// a good use case of (A) B
type List<T> = recursive either {
  .empty!
  .item(T) self
}
// can now be created like this:
let bool_list: List<Bool> =
  .item(.true!).item(.false!).empty!

// in most cases, (A, B)! is the safer bet
// as it uses more friendly syntax
type Pair<T, T> = (T, T)!

let bool_pair: Pair<Bool> =
  (.true!, .false!)!

Values are created using pair expressions:

let a: A = ...
let b: B = ...

let pair: (A) B = (a) b

and they can be destructed using pair patterns or receive commands:

let triple: (A, B, C)! = (a, b, c)!

// pattern matching
let (first) rest = triple
// first = a
// rest = (b, c)!

// commands
do {
  rest[second]
  // after this command:
  // rest = (c)! 
  // second = b
} in ...

Mathematically, (A) B is \(A \otimes B\). For session types, it means “send A and continue as B”.

Function Types

^Syntax
FunctionType : [ TypeList ] Type

^{Dual | Constructing Expression | Destructing Expression | Constructing Statement | Destructing Statement}

Having multiple types between [ and ] is just syntax sugar:

type T = [A, B] R
// is equivalent to
type T = [A] [B] R

Values are created using function expressions:

let add1: [Nat] Nat = [n] .succ n

and destructed by calling the function:

let one: Nat = .succ.zero!
let two = add1(one)

Mathematically, [A] B is a linear function \(A \multimap B\). For session types, it means “receive A and continue as B”.

Either Types

^Syntax
EitherType : either { (Label Type ,^?)^* }

^{Dual | Constructing Expression | Destructing Expression | Constructing Statement | Destructing Statement}

An either type is the usual sum type aka. a tagged union (in Rust, it’s an enum). Every value of such a type consists of a label, marking the variant, and a value of the type corresponding to the label (its “payload”).

// the most basic sum type
type Bool = either {
  .true!  // variant "true" with payload !
  .false! // variant "false", also with payload !
}

// a slightly more complex example
type TwoOrNone<T> = either {
  .none!      // variant "none" with "no" payload (using !)
  .two(T, T)! // variant "some" with "two" payloads
}

Values are created by attaching a label to its required payload. Note that the corresponding either type must always be known when labeling an expression. A type annotation can be used for that.

let no_bool: TwoOrNone<Bool> = .none!

let both_bools: TwoOrNone<Bool> = .two(.true!, .false!)!

Mathematically, either { .a A, .b B } is \(A \oplus B\). For session types, it means “select from A or B”. An empty either type either {} is therefore \(\mathbf{0}\), the empty type. In Haskell, it’s called void and in Rust it’s ! (not to be confused with the ! in Par). There is a function from it to every type:

def absurd: [type T] [either {}] T = [type T] [x] x {}

This function can never be called though.

Either types are often used as recursive types.

Choice Types

^Syntax
ChoiceType :
      { (Label (( ReceiveTypes ))^* => Type ,^?)^* }

ReceiveTypes :
      TypeList
   | type ID_List

^{Dual | Constructing Expression | Destructing Expression | Constructing Statement | Destructing Statement}

A choice type is dual to an either type. Constructing a value of an either type is “making a choice” and similarly, destructing such a value looks exactly like constructing a value of a choice type. It consists of several labels that can be used as signals to destruct the receiver.

// choice of two
type BoolChoice<A, B> = {
  .true => A
  .false => B
}

// destruct a Bool
def negate(b: Bool): Bool = b {
  .true! => .false!
  .false! => .true!
}

// construct a choice
def negate_choice: BoolChoice<Bool, Bool> = {
  .true => .false!
  .false => .true!
}

// define negate using the choice
// featuring selecting from the choice type value
def also_negate: [Bool] Bool = [b] b {
  .true! => negate_choice.true
  .false! => negate_choice.false
}

.cons => [A] B can also be written as .cons(A) => B

A choice type represents an interface for interacting with data. While an either type describes its underlying data, a choice type describes what can be done with it.

// creating an interface
type Stack<T, Unwrap> = iterative {
  .push(T) => self
  .pop => (Option<T>) self
  .unwrap => Unwrap
}

// implementing it
dec list_stack : [type T] [List<T>] Stack<T, List<T>>
def list_stack = [type T] [list] begin {
  .push(x) => let list: List<T> = .item(x) list in loop
  .pop => list {
    .empty! => (.none!) let list: List<T> = .empty! in loop,
    .item(head) tail => (.some head) let list = tail in loop
  }
  .unwrap => list
}

def main = do {
  let stack = list_stack(type Bool)(.empty!)
  stack.push(.true!)
  stack.push(.false!)
} in stack

For an explanation of iterative-self and begin-loop, see iterative types

Mathematically, { .a => A, .b => B } is \(A \mathbin{\&} B\). For session types, it means “offer a choice of A or B”. An empty choice {} is therefore \(\top\) and has exactly one value, {}. There is a function to it from every type:

def immortalize: [type T] [T] {} = [type T] [x] {}

The result of this function can never be used though.

Choice types are often used as iterative types.

Recursive Types

^Syntax
RecursiveType : recursive LoopLabel^? Type

^{Dual | Destructing Expression | Destructing Statement}

A recursive type can be used within itself via self.

If no loop label is present, self corresponds to the innermost recursive/iterative. Else to the one with the same loop label.

Recursive types are mostly used in conjunction with either types:

type List<T> = recursive either {
  .empty!
  .item(T) self
}

Values of recursive types always terminate. They have to be constructed finitely.

// a simple List
let l: List<Bool> = .item(.true!).item(.false!).empty!

Mathematically, a recursive either type represents an inductive type. Constructors without self are the base cases while those with self represent inductive steps.

A function from a recursive type is defined using induction:

// recursive (inductive) type representing
// the natural numbers
type Nat = recursive either { 
  .zero!, 
  .succ self
}

dec is_even : [Nat] Bool
// induction over n (marked by applying begin-loop)
def is_even = [n] n begin {
  // base case(s)
  .zero! => .true!
  // inductive step(s)
  // pred loop is analogous to an inductive hypothesis
  .succ pred => not(pred loop)
}

Iterative Types

^Syntax
IterativeType : iterative LoopLabel^? Type

^{Dual | Constructing Expression | Constructing Statement}

An iterative type can be used within itself via self.

If no loop label is present, self corresponds to the innermost recursive/iterative. Else to the one with the same loop label.

Iterative types are mostly used in conjunction with choice types, for example:

type Stream<T> = iterative {
  .close => !
  .next => (T) self
}

Values of iterative types may be infinite. In contrast to recursive types, such values can only be destructed in finitely many steps.

type Inf<T> = iterative (T) self

def infinite_bools: Inf<Bool> = begin (.true!) loop

This infinite value can be constructed but there is no way of fully destructing (so: using) it.

Mathematically, an iterative choice type represents a coinductive type. Destructors without loop break the iteration and return, while those containing loop yield and continue.

A function to an iterative type is defined using coinduction (iteration):

type Nat = recursive either { .zero!, .succ self }

// construct a stream of all natural numbers
// in form of the iterative Stream<Nat>
def nat_stream: Stream<Nat> = 
  let n: Nat = .zero! in 
  // coinduction (independent begin-loop)
  begin {
    // break, return !
    .close => drop(n),

    .next => do {
      let (next, n)! = copy(n)
      let n: Nat = .succ n
    } in
      // yield the next number 
      (n1)
      // continue (coinductive step)
      loop 
  }

// helpers

def drop: [Nat] ! = [n] n begin {
  .zero! => !
  .succ pred => pred loop
}

def copy: [Nat] (Nat, Nat)! = [n] n begin {
  .zero! => (.zero!, .zero!)!
  .succ pred => let (p1, p2)! = pred loop
    in (.succ p1, .succ p2)!
}

Existential Types

^Syntax
ExistentialType : ( type ID_List ) Type

^{Dual | Constructing Expression | Pattern | Constructing Statement | Destructing Statement}

Having multiple types between ( and ) is just syntax sugar:

type T = (type A, B) X
// is equivalent to
type T = (type A) (type B) X

Existential types mirror pair types but they’re qualified over types rather than values. They are used to encapsulate their underlying type.

type Bool  = either { .true!, .false! }
type Nat = recursive either { .zero!, .succ self }

type Any = (type T) T

def main = chan user {
// create values of the existential Any type
// note that both have exactly the same type!
let any1: Any = (type Bool) .true!
let any2: Any = (type Nat) .succ.zero!

user(any1)
user(any2)
user!
}

The qualifying types and values can both be extracted from a value of such a type:

let any: Any = ...
let (type X) x = any
let y: X = x

Mathematically, (type T) A is \(\exists\ T: A\).

Universal Types

^Syntax
UniversalType : [ type ID_List ] Type

^{Dual | Constructing Expression | Destructing Expression | Constructing Statement | Destructing Statement}

Having multiple types between [ and ] is just syntax sugar:

type T = [type A, B] X
// is equivalent to
type T = [type A] [type B] X

Values of universal types can be instantiated for any type. These types syntactically mirror function types but they’re qualified over types rather than values. They’re also similar to parameterized types.

// compare the three types of parameterizing types
type UnivEndo = [type T] [T] T
type ParamEndo<T> = [T] T
type ExistEndo = (type T) [T] T

// a value of an universal type must be defined
// for all types
let id: UnivEndo = [type T] [x] x

// a specialized version can be represented using
// a parameterized type
let id_bool: ParamEndo<Bool> = id(type Bool)

// this type encapsulates the Bool
let id_bool_2: ExistEndo = (type Bool) id_bool

A more interesting example is reversing a list of any type.

Mathematically, [type T] A is \(\forall\ T: A\).

The Bottom Type

^Syntax
Bottom : ?

^{Dual | Constructing Statement | Destructing Statement}

The bottom ? is dual to the unit !.

def main: Bool = chan user {
  user.true
  // user now has type ?
  user!
}

Mathematically, ? is \(\bot\), the unit for \(⅋\). So \(\bot \mathbin{⅋} A = \mathbf{1} \multimap A \cong A\) (as seen before for the unit type).

Channel Types

^Syntax
ChannelType : chan Type

^{Dual | Constructing Expression}

chan A represents a channel accepting an A:

def just_true: Bool = chan yield {
  let c: chan Bool = yield
  c.true!
}

chan is merely a type transformer, turning a type into its dual. For example, chan chan T is equal to T (not just isomorphic).

A more elaborate example can be seen here

A chan A can be linked with an A (using <>), annihilating both and ending the process.

def just_true: Bool = chan yield {
  let c: chan Bool = yield
  let b: Bool = .true!
  c <> b
}

Note that b <> c would have been equally valid.

Duality equations

Mathematically, chan A is \(A^\perp\), i.e. the dual type to A. Every type has a dual. These are defined according to this table:

Moreover, chan A ≅ [A]? is an isomorphism

dec i : [type A] [chan A] [A]?
def i = [type A] [ch] chan receive {
  // receive is of type (A)!
  receive[a]?
  ch <> a
}

dec j : [type A] [[A]?] chan A
def j = [type A] [annihilate] chan a {
  // a is of type A
  annihilate(a)!
}

So the dual of a type can be used to destruct a value.

Expressions

^Syntax
Expression :
      Construction
   | Application
   | LetExpression
   | DoExpression
   | ChanExpression

Every expression desugars to a channel expression. In the most simple way, that is

expr
// is equivalent to
chan dual {
  dual <> expr
}

This can now be further translated into process syntax by rewriting the link dual <> expr. Rules for that are provided in every expression rule.

Primary Expressions

^Syntax
PrimaryExpression :
      ID
   | GroupedExpression

GroupedExpression :
      { Expression }

Par uses { and } for grouping expressions together. Together with names like x they form the primary expressions, which can be destructed using expressions.

Primary expressions appear here in the grammar.

Examples:

dec apply_id : [type T] [T] T
def apply_id = [type T] [x] {[y] y}(x)

Primary expressions can be linked via:

dual <> id // can't be further simplified

dual <> {expr}
// is just
dual <> expr

Let Expressions

^Syntax
LetExpression : let Pattern = Expression in Expression

The second expression must use all bindings of the pattern (which must be irrefutable) due to linearity.

Let expressions make code easier to read by creating an expression in multiple steps. Compare:

let x = call_a_long_function(and_another_one(y))
in (.true!, x, .false!)!
// with
(.true!, call_a_long_function(and_another_one(y)), .false!)!

But arguably even morer useful are the destruction-by-pattern capabilities let expressions offer:

// this expression is not possible
// without let or do expressions
let (b1, b2)! = copy_bool(b)
in (b1, not(b2))!

Let statements are very similar, so when multiple let expressions in a row would be required, it’s often more convenient to switch to those and put them inside do expressions.

Let expressions can be linked via:

dual <> let p = x in y
// is equivalent to
let p = x
dual <> y

Do Expressions

^Syntax
DoExpression : do { Process } in Expression

Do expressions allow process syntax inside an expression context:

do { 
  commands... 
} in result
// is equivalent to
chan return {
  commands...
  return <> result
}

Linearity requires that all leftover bindings from the process must be used in the expression at the end.

Do expressions are useful for…

// ...binding multiple values with let
do {
  let v1 = e1
  ...
  let vn = en
} in result
// is preferred over
let v1 = e1 in
...
let vn = en in
result

// ...destructing values
do {
  drop(x1)?
  drop(x2)?
} in result

Expressions construct, commands destruct. Because of this, when a value is destructed, process syntax (for example via a do expression) is the way to go.

Do expressions can be linked via:

dual <> do { proc } in y
// is equivalent to
proc
dual <> y

Channel Expressions

^Syntax
ChanExpression : chan ID Annotation^? { Process }

The name declared after the channel may be used inside the process and must be fully destructed inside or moved out of there.

The expression chan a: A { ... } has type chan A. Conversely, if chan b { ... } has type B, b has type chan B.

Note, that chan A, the channel type, is not a separate type. It merely transforms the A to its dual, according to the duality equations.

These expressions are key to exploiting duality. The expression chan c { ... } spawns a process, and at the same time creates a channel, whose one end is accessible as c inside the process, and the other end is returned from the expression. The types of these are dual.

Channel expressions are the only expression which is not syntax sugar. Under the hood, all expressions are syntax sugar for channel expressions.

Par even has an intermediate representation in which all expressions are channel expressions.

A channel expression constructs a value by destructing a value of its dual. For example:

dec is_even : [Nat] Bool
def is_even = chan return: (Nat) chan Bool {
  // destruct return in this process

  return[n]
  // return is now of type chan Bool
  // and n is of type Nat

  // destruct n
  n begin {
    .zero! => {
      // fully destruct return
      return.true!
    }
    .succ => {
      // n is now its former predecessor
      n {
        .zero! => {
          // n was 1
          return.false!
        }
        .succ => {
          n loop
        }
      }
    }
  }
}

Learn more about destructing values using commands here.

A more elaborate example is reversing a list using the generator pattern:

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 {
    // The list is empty, give back the generator handle.
    .empty!       => yield,
    // The list starts with an item `x`.
    .item(x) rest => do {
      // Traverse into the rest of the list first.            
      let yield = rest loop
      // After that, produce `x` on the reversed list.          
      yield.item(x)                  
    } in yield // Finally, give back the generator handle.
  }
  // At the very end, signal the end of the list.
  yield.empty!                       
}

Construction Expressions

^Syntax
Construction :
      Unit
   | PairExpression
   | FunctionExpression
   | EitherSelection
   | ChoiceConstruction
   | IterativeConstruction
   | Loop
   | ExistentialConstruction
   | UniversalConstruction

The Unit Expression

^Syntax
Unit : !

^{Type | Pattern | Statement | Destructing Statement}

The unit expression ! is of the unit type !.

It’s the only value of its type:

def unit: ! = !

Unit expressions can be linked via:

dual <> !
// is equivalent to
dual!

Pair Expressions

^Syntax
PairExpression : ( ExpressionList ) Expression

^{Type | Pattern | Statement | Destructing Statement}

Having multiple expressions between ( and ) is just syntax sugar:

(a, b) c
// is equivalent to
(a) (b) c

If a is of type A and b is of type B, the pair expression (a) b is of the pair type (A) B.

let bool_pair: (Bool, Bool)! = (.true!, .false!)!

The difference between representing a pair of A and B as (A, B)! or (A) B is:

• (A1, ..., An)!. is the default for regular tuples.

  let zero_to_two: (Nat, Nat, Nat)! = (
    .zero!,
    .succ.zero!,
    .succ.succ.zero!,
  )!
  

• (A1, ..., An) B more specifically means “send A1, …, and An, then continue as B”. It’s used when all but the last member of a tuple should be received separately and the receiver should continue as the last one. For example:

  def length: [List] (Nat) List = [l] l begin {
    .empty! => (.zero!) .empty!,
    .item(head) tail => do {
      // tail loop is of type (Nat) List
      tail loop
      // receive len_pred 
      tail[len_pred]
      // tail is now as before
    } in (.succ len_pred) .item(head) tail
  }
  

Pair expressions can be linked via:

dual <> (a) b
// is equivalent to
dual(a)
dual <> b

Function Expressions

^Syntax
FunctionExpression : [ PatternList ] Expression

^{Type | Destructing Expression | Statement | Destructing Statement}

Having multiple patterns between [ and ] is just syntax sugar:

[p, q] x
// is equivalent to
[p] [q] x

If p is an irrefutable pattern for type A and b (wich must use the bindings of p) is of type B, the function expression [p] b is of the function type [A] B.

We’ve already seen a lot of functions, so here’s a simple one:

def add2: [Nat] Nat = [n] .succ.succ n

Note that function expressions are the primary way of defining functions in par. Defining a function looks the same as defining any other value.

Function expressions can be linked via:

dual <> [p] b
// is equivalent to
dual[p]
dual <> b

Either Selections

^Syntax
EitherSelection : Label Expression

^{Type | Destructing Expression | Statement | Destructing Statement}

The type of an either selection cannot be inferred from itself.
A selection of the either type either { .a A, .b B } is either .a a if a is of type A or .b b if b is of type B.

type Bool = either {
  .true!,
  .false!,
}

def true: Bool = .true!

Recursive types have no special construction syntax, instead they are finitely constructed as their underlying type. Most often they’re seen as recursive either types:

type Nat = recursive either {
  .zero!,
  .succ self,
}

// construct a value of the recursive
// Nat type like any other either type
def two = .succ.succ.zero!

Either selections can be linked via:

dual <> .a a
// is equivalent to
dual.a
dual <> a

Choice Constructions

^Syntax
ChoiceConstruction :
      { (Label (( ReceivePatterns ))^* => Expression ,^?)^* }

ReceivePatterns :
      PatternList
   | type ID_List

^{Type | Destructing Expression | Statement | Destructing Statement}

If a is of type A and b is of type B, the choice construction { .a => a, .b => b } is of the choice type { .a => A, .b => B }.

Some patterns can be used on the left side:

• { .a(p) => a } is equivalent to { .a => [p] a }
• { .a(type T) => a } is equivalent to { .a => [type T] a }

Choice constructions look very similar to match expressions (intentionally!).

type BoolChoice = {
  .true => Bool,
  .false => Bool,
}

def negate: BoolChoice = {
  .true => .false!,
  .false => .true!,
}

Choice constructions can be linked via:

dual <> { .a => a, .b => b }
// is equivalent to
dual { 
  .a => { dual <> a }
  .b => { dual <> b }
}

Iterative Constructions

^Syntax
IterativeConstruction :
      begin LoopLabel^? Expression

Loop :
      loop LoopLabel^?

^{Type | Statement}

If — given every loop in a is of type iterative A — a is of type A, the iterative construction begin a is of the iterative type iterative A.

A loop corresponds to the innermost begin with the same loop label. loop without a label can only correspond to begin without a label.

Iterative types are constructed with begin-loop and as such, their values are often infinite. This is not a problem, however, as they don’t have special syntax for destruction, i.e. they can only be finitely destructed.

type Omega = iterative {
  .close => !,
  .next => self,
}

// This value is infinite:
// .next can be called as often
// as one desires
// (but only finitely many times)
def omega: Omega = begin {
  .close => !,
  .next => loop,
}

Iterative constructions can be linked via:

dual <> begin a
// is equivalent to
dual begin
dual <> a // with loop in a replaced by begin a

Existential Constructions

^Syntax
ExistentialConstruction : ( type TypeList ) Expression

^{Type | Pattern | Statement | Destructing Statement}

Having multiple types between ( and ) is just syntax sugar:

(type A, B) c
// is equivalent to
(type A) (type B) c

If a is of type A, the existential construction (type T) a is of the existential type (type T) A.

type Any = (type T) T

let any_bool: Any = (type Bool) .true!
let any_unit: Any = (type !) !

Existential constructions can be linked via:

dual <> (type T) a
// is equivalent to
dual(type T)
dual <> a

Universal Constructions

^Syntax
UniversalConstruction : [ type ID_List ] Expression

^{Type | Destructing Expression | Statement | Destructing Statement}

Having multiple names between [ and ] is just syntax sugar:

[type T, U] x
// is equivalent to
[type T] [type U] x

If a is of type A, the universal construction [type T] a (where a can use the type T) is of the universal type [type T] A.

Universal constructions are moslty used to define “generic functions”:

def empty_list : [type T] List<T> = [type T] .empty!

// called via
let bools: List<Bool> = empty_list(type Bool)

Universal constructions can be linked via:

dual <> [type T] a
// is equivalent to
dual[type T]
dual <> a

Application Expressions

^Syntax
Application :
      Applicable
   | MatchExpression
   | LoopApplication

Applicable :
      PrimaryExpression
   | FunctionCall
   | ChoiceSelection
   | RecursiveDestruction
   | UniversalSpecialization

While constructions construct values, applications destruct them. Some types do not have an application expression for destruction – they use patterns instead.

An application is always of the form: Applicable Suffix. Every application corresponds to a command, which looks the same. In contrast to commmand receivers however, applicables don’t become the result of this expression.

All applications can be linked via:

dual <> app suffix
// is equivalent to
let a = app
a suffix
dual <> a

Note that if app is a local variable, the let is not needed.

Function Calls

^Syntax
FunctionCall : Applicable ( ExpressionList )

^{Destructs Type | Destructs Expression | Statement}

Having multiple expressions between ( and ) is just syntax sugar:

f(a, b)
// is equivalent to
f(a)(b)

If f is of type [A] B and a is of type A, the function call f(a) is of type B.

def function: [A] B

let a: A = ...
let b: B = function(a)

A function call is equivalent to a send command:

// in process syntax
let b = f(a)
// is equivalent to
let b = f
b(a)

Choice Selections

^Syntax
ChoiceSelection : Applicable Label

^{Destructs Type | Destructs Expression | Statement}

If x is of type { ..., .label => T, ... }, the choice selection x.label is of type T.

type BoolChoice = {
  .true => Bool,
  .false => Bool,
}

let bc: BoolChoice = ...
let choose_true = bc.true

Iterative types have no special destruction syntax, instead they are finitely destructed as their underlying type. Most often they’re seen as iterative choice types:

type Stream<T> = iterative {
  .close => !,
  .next => (T) self
}

let nats: Stream<Nat> = ...

// finitely destruct nats
do {
  let (first) rest = nats.next
  let (second) rest = nats.next
  let ! = rest.close
} in (first, second)!

A choice selection is equivalent to a signal command:

// in process syntax
let y = x.label
// is equivalent to
let y = x
y.label

Match Expressions

^Syntax
MatchExpression : Applicable { (Label (( ReceivePatterns ))^* (ID | !) => Expression ,^?)^* }

^{Destructs Type | Destructs Expression | Statement}

Match expressions are similar to match in Rust or case in Haskell. Their pattern matching abilities are currently limited but will expand in the future.

If x is of type either { .l1 T1, ..., .ln Tn } and

• p1 is a pattern for type T1, and so on, until pn is a pattern for type Tn
• y1, …, yn are all of type U

then x { .l1 p1 => y1, ..., .ln pn => yn } is of type U. It evaluates to the yi which label .li was matched.

type Option<T> = either {
  .none!,
  .some T
}

let o: Option<Nat> = ...

let o_add1: Option<Nat> = o {
  .none! => .none!,
  .some n => .some.succ n,
}

Recursive Destructions

^Syntax
RecursiveDestruction :
      Applicable unfounded^? begin LoopLabel^?

LoopApplication :
      Applicable loop LoopLabel^?

^{Destructs Type | Statement}

A loop corresponds to the innermost begin with the same loop label. loop without a label can only correspond to begin without a label.

If x is of type recursive T, then begin x is of type T, replacing each corresponding self of T with recursive T.

A loop corresponding to this begin can be used on values of type recursive T. Its behavior is equivalent to “pasting” the begin and every application that follows it.

Consider the recursive type

type List<T> = recursive either {
  .empty!,
  .item(T) self,
}

This is a total begin-loop

dec reverse : [type T] [List<T>] List<T>
def reverse = [type T] [list] do {
  let rev = .empty!
} in list begin {
  .empty! => rev,
  .item(head) tail => do {
    let rev = .item(head) rev
  } in tail loop
  // tail corresponds to the self in the
  // .item(T) self
  // branch
}

This is a total unfounded begin-loop, as the totality checker currently doesn’t recognize this loop as total.

dec reverse : [type T] [List<T>] List<T>
def reverse = [type T] [list] list unfounded begin {
  .empty! => .empty!,
  .item(head) tail => do {
    let (left, right)! = split(type T)(.item(head) tail)
  } in concat(type T)(
    left loop,
    right loop,
  )
}

/// splits the list into two lists
/// of equal length
/// (the left list may be one longer)
dec split : [type T] [List<T>] (List<T>, List<T>)!

/// concatenates two lists
dec concat : [type T] [List<T>, List<T>] List<T>

This is a nontotal unfounded begin-loop. Caution is required when using these to not lose totality.

def infinite_loop: ! = do {
  let list: List<!> = .item(!).empty!
} in list unfounded begin {
  .empty! => !, // this is total
  .item(head) tail => do {
    let list: List<!> = .item(head) tail
  } in list loop, // this is not total
}

Universal Specializations

^Syntax
UniversalSpecialization : Applicable ( type TypeList )

^{Destructs Type | Destructs Expression | Statement}

Having multiple types between ( and ) is just syntax sugar:

x(type T, U)
// is equivalent to
x(type T)(type U)

If x is of the universal type [type T] R, the specialization f(type X) is of type R.

These expressions often “instantiate generic functions”

def id = [type T] [x: T] x

def id_bool: [Bool] Bool = id(type Bool)
def id_unit: [!] ! = id(type !)

Patterns

^Syntax
Pattern :
      PatternNoAlt

PatternNoAlt :
      BindingPattern
   | Unit
   | PairPattern
   | ExistentialPattern

PatternList :
      PatternNoAlt (, PatternNoAlt)^* ,^?

There are two properties of a pattern: What names it binds and whether it’s refutable.

Patterns can appear in several places:

• in a let binding:

  // as an expression
  let p = x in y
  
  // or in process syntax
  let p = x
  rest...
  

  All bindings of p must be used in y or rest... respectively. Here, p must be irrefutable.

• between [ and ]

  // in a function expression
  [p] body
  
  // destructing a pair (process syntax)
  tail[p]
  rest...
  

  All bindings of p must be used in body or rest... respectively. Here, p must also be irrefutable.

• in pattern matching, i.e. either destruction/choice construction

  // either destruction
  x {
    .label (p) rest_payload => y
    ...
  }
  // in process syntax, the rest_payload isn't present
  // (instead, x becomes it)
  
  // choice construction
  {
    .label (p) => y
    ...
  }
  

  All bindings of p must be used in y. Here, p must also be irrefutable.

Binding Patterns

^Syntax
BindingPattern : ID Annotation^?

The pattern name or name: T is always irrefutable and binds name to x when matching x.

The pattern name can be used on a value which type is known. Otherwise, name: T must be used, which can only be used on a value of type T.

Binding patterns are the most used patterns.

// break up an expression
do {
  let v1 = e1
  let v2 = e2
} in // expression using v1 and v2

If the type of the value matched is already known, a type annotation would have to match it. Such an annotation can be useful for declaring functions, though:

// no extra type annotation/declaration needed
def negate = [b: Bool] let result: Bool = b {
  .true! => .false!
  .false! => .true!
} in result

The Unit Pattern

^Syntax
Unit : !

^{Type | Constructing Expression | Destructing Statement}

The unit pattern ! is always irrefutable and binds nothing. It can only be used on values of type !.

// if there is a value of a type T,
// there is a function [!] T
def returns_true: [!] Bool = [!] .true!

// ! can be used to destroy a unit
def drop_two_bools: [Bool, Bool] ! = 
  [b1, b2] let ! = drop(b1) in drop(b2)

// though process syntax is generally used for this
def drop_two_bools: [Bool, Bool] ! = [b1, b2] do {
  drop(b1)?
  drop(b2)?
} in !

dec drop_bool : [Bool] ! 
def drop_bool = [b] {
  .true! => !
  .false! => !
}

Pair Patterns

^Syntax
PairPattern : ( PatternList ) Pattern

^{Type | Constructing Expression | Destructing Statement}

• A pair pattern (p) q is irrefutable if and only if both p and q are irrefutable
• When p can be used on type A and q on type B, (p) q can be used on type (A) B
• (p) q matches (a) b if and only if p matches a and q matches b
• When matching (a) b, the bindings are those of p matching a, together with those of q matching b

Having multiple patterns between ( and ) is just syntax sugar:

// the pattern
(p, q) r
// is equivalent to
(p) (q) r

A pair pattern is used to destruct a value of a pair type:

dec uncurry : [type A, B, C] [[A, B] C] [(A, B)!] C
def uncurry = [type A, B, C] [f] [(a, b)!] f(a, b)

Existential Patterns

^Syntax
ExistentialPattern : ( type ID ) Pattern

^{Type | Constructing Expression | Destructing Statement}

• An existential pattern (type X) p can only be used on an existential type (type T) A and p must be able to be used on type A
• When it can match, it is irrefutable if and only if p is irrefutable
• (type X) p matches (type T) a if and only if p matches a
• When matching (type T) a, the bindings are those of p matching a, and X is bound to T

Having multiple types between ( and ) is just syntax sugar:

// the pattern
(type X, Y) p
// is equivalent to
(type X) (type Y) p

An existential pattern is used to destruct a value of an existential type

type Any = (type T) T

def any_test: Any = do {
  let x: Any = (type Bool) .true!
  let (type X) x_val = x
  // X = Bool
  // x_val = .true!
  let y: X = x_val
} (type X) y

Future

More extensive pattern matching, along with more types of patterns is planned in the future. See here for more.

Statements

Statements are used in process syntax to

• destruct values: Command
• bind values: LetStatement

Process syntax is a series of statements, where all are nonterminating. In a channel expression the last one will be terminating, making it an exception.

Process syntax is introduced by the Proces Rule:

^Syntax
Process : (Statement (;^? Statement) (;^? TerminatingStatement)^?)^?

Statement :
      Command
   | LetStatement

TerminatingStatement :
      TerminatingCommand

It is used in the following places:

• do expressions:

  let x = do { process } in value
  

  The process here may not use terminating statements.

• channel expressions:

  let x = chan dual { process }
  

  The process here must use a terminating statement. It constructs x by destructing its dual, dual.

Let Statements

^Syntax
LetStatement :
      let Pattern = Expression

Let statements are used to create values in processes. They are the only constructive statements, as commands always destruct.

In do expressions, they are used to bind the values used in the value after in:

let true_and_false = do {
  let x: Bool = .true!
  let y: Bool = .false!
} in (x, y)!

In chan expressions, they can be used to construct a value that is then linked with a value of dual type:

def just_true = chan return: chan Bool {
  // constructing the return value
  let b: Bool = .true!
  // linking it
  return <> b
}
// is equivalent to
def just_true = chan return: chan Bool {
  // destructing the result
  return.true!
}

Commands

^Syntax
Command :
      ContinueCommand
   | SendCommand
   | ReceiveCommand
   | SignalCommand
   | MatchCommand
   | BeginCommand
   | SendTypeCommand
   | ReceiveTypeCommand

TerminatingCommand :
      BreakCommand
   | LinkCommand
   | Loop

Receiver :
      ID
   | Command

Nonterminating commands can be chained.

rec cmd1 cmd2
// is just
rec cmd1
rec cmd2

Link Commands

^Syntax
LinkCommand : Receiver <> Expression

Link commands are symmetric, i.e. a <> b is the same as b <> a. On the right side, any expression can be used, however.

The types on both sides must be dual to each other. The link then annihilates both and ends the process.

def f: A = chan return: chan A {
  let a: A = ...
  return <> a
}

Rewrite rules for all expressions can be found at their respective rules (for applications they are grouped at the start).

The Break Command

^Syntax
BreakCommand : Receiver !

^{Dual | Destructs Type | Destructs Channel}

A break command destructs a ? and ends the process. It is used with chan, as destructing a ? is constructing its dual ! there.

def unit: ! = chan bottom: ? {
  bottom!
}

The Continue Command

^Syntax
ContinueCommand : Receiver ?

^{Dual | Destructs Type | Destructs Channel | Pattern | Constructing Expression}

A continue is used to destruct a !:

dec drop_bool : [Bool] !

let b1: Bool = ...
let b2: Bool = ...
// get rid of b1
do {
  // drop_bool(b1) returns !
  // this is destructed by ?
  drop_bool(b1)?
} in b2

Send Commands

^Syntax
SendCommand : Receiver ( ExpressionList )

^{Dual | Destructs Type | Destructs Channel | Expression | Constructing Expression}

Having multiple expressions between ( and ) is just syntax sugar:

// the command
r(x, y)
// is equivalent to
r(x)(y)

A send command can destruct (“call”) a function:

do {
  let b: Bool = .true!
  let negate: [Bool] Bool = ...

  // call negate
  negate(b)
  // negate is now the negation of b
} in negate
// evaluates to .false!

It can also be used with chan: Destructing [A] chan B to dually construct (A) B

def true_false: (Bool) Bool = chan return: [Bool] chan Bool {
  return(.true!)
  // return is now a chan Bool
  return <> .false!
}

Receive Commands

^Syntax
SendCommand : Receiver [ PatternList ]

^{Dual | Destructs Type | Destructs Channel | Pattern | Constructing Expression}

Having multiple patterns between [ and ] is just syntax sugar:

// the pattern
r[p, q]
// is equivalent to
r[p][q]

A receive command can destruct a pair:

dec reverse : [type A, B] [(A) B] (B) A
def reverse = [type A, B] [pair] do {
  // receive first value
  pair[first]
  // if pair was (a) b :
  // first is now a
  // pair is now b
} in (pair) first

It can also be used with chan: Destructing (A) chan B to dually construct [A] B

def negate: [Bool] Bool = chan return: (Bool) chan Bool {
  // receive the argument
  return[arg]
  // return is now a chan Bool
  return <> arg {
    .true! => .false!
    .false! => .true!
  }
}

Signal Commands

^Syntax
SignalCommand : Receiver Label

^{Dual | Destructs Type | Destructs Channel | Expression | Constructing Expression}

A signal command can destruct a choice:

type Stream<T> = iterative {
  .close => !
  .next => (T) self
}

dec first_two : [type T] [Stream<T>] (T, T)!
def first_two = [type T] [stream] do {
  // signal next
  stream.next
  // stream is now (T) Stream<T>
  stream[first]
  // stream is now again Stream<T>

  // combine both operations
  stream.next[second]

  // close the stream
  stream.close?
} in (first, second)!

It can also be used with chan: Destructing a choice type to dually construct an either type:

// chan Bool is equal to
type ChanBool = {
  .true => ?
  .false => ?
}

def just_true: Bool = chan return: ChanBool {
  // signal true
  return.true
  // return is now ?
  return!

  // return.true! would have been equally valid
}

Match Commands

^Syntax
MatchCommand : Receiver { (Label (( ReceivePatterns ))^* !^? => { Process })^* }

^{Dual | Destructs Type | Destructs Channel | Expression | Constructing Expression}

Patterns in (...) after the label are equivalent to a receive command in the body:

x {
  .label(a) => { rest... }
}
// is equivalent to
x {
  .label => {
    x[a]
    rest...
  }
}

(a, b) is also equivalent to (a)(b) here.

Similarly, a ! afterwards is equivalent to a continue in the body:

x {
  .label(...)! => { rest... }
}
// is equivalent to
x {
  .label(...) => {
    x?
    rest...
  }
}

A match command can destruct an either type:

def drop_bool: [Bool] ! = [b] do {
  // match on b
  b {
    .true => {
      // b is now !
      b?
    }
    // combine both 
    // (moving ? over => makes it !)
    .false! => {}
  }
} in !

It can also be used with chan: Destructing an either type to dually construct a choice type:

// choice of two
type BoolChoice<A, B> = {
  .true => A
  .false => B
}

// dual type
type ChanBoolChoice<A, B> = either {
  .true chan A
  .false chan B
}

dec negate_choice : BoolChoice<Bool, Bool>
def negate_choice = chan return: ChanBoolChoice<Bool, Bool> {
  return {
    .true => {
      // return is now of type chan Bool
      return.false!
    }
    .false => { return.true! }
  }
}

Recursive Commands

^Syntax
SendCommand :
      Receiver unfounded^? begin LoopLabel^?

LoopCommand :
      Receiver loop LoopLabel^?

LoopLabel :
      : ID

^{Destructs Type | Destructs Channel | Expression}

A loop corresponds to the innermost begin with the same loop label. loop without a label can only correspond to begin without a label.

A recursive command can destruct a recursive type:

def list_and: [List<Bool>] Bool = [list] do {
  let result: Bool = .true!

  // destruct list recursively
  list begin {
    // after begin, list is of type
    // either { .empty!, .item(Bool) List<Bool> }
    // notice the absence of recursive
    .item => {
      // list is now of type (Bool) List<Bool>
      list[b]
      b {
        .true! => {}
        .false! => {
          drop_bool(result)?
          // reassign result here
          let result: Bool = .false!
        }
      }
      // list is now of type List<Bool>
      // go to begin
      list loop
    }
    .empty! => {}
  }
} in result

Note that

.item => {
  list[b]
  ...
}

could have been replaced with

.item(b) => {
  ...
}

A very important concept is that all values which were consumed between begin and loop must be reassigned (like result in the example). This even allows variables to change in between the iterations:

def first_nats: [Nat] List<Nat> = [n] do {
  // initialize "mutable" value
  let list: List<Nat> = .empty!
  n begin {
    .zero! => {
      // also reassign, but for after `in`
      let list = .item(.zero!) list
    }
    .succ pred => {
      // here pred gets reassigned
      let (pred, p)! = copy_nat(pred)
      // and list gets reassigned as well
      let list = .item(.succ p) list
      pred loop
    }
  } 
} in list

A recursive command can also be used with chan: Destructing a recursive (here: either) type to dually construct an iterative (here: choice) type:

// chan Stream<Bool> is
type ChanStreamBool = recursive either {
  .close?
  .next[T] self
}

def alt_true_false: Stream<Bool> = chan return: ChanStreamBool {
  let next: Bool = .true!
  // begin recursive destruction
  return begin {
    // return is now of type 
    // either { .close?, .next[T] ChanStreamBool }
    // again, notice the absence of recursive
    .close => {
      // return is now ?
      // handle next first
      drop_bool(next)?
      return!
    }
    .next => {
      // return is now of type [T] ChanStreamBool
      // handle next first
      next {
        .true! => {
          let yield = .true!
          let next = .false!
        }
        .false! => {
          let yield = .false!
          let next = .true!
        }
      }
      return(yield)
      // return is now of type ChanStreamBool
      return loop

      // return(yield) loop would have been equally valid
    }
  }
}

// in expression syntax:
def alt_true_false: Stream<Bool> = do {
  let next: Bool = .true!
} in begin {
  .close => drop_bool(next),
  .next => let (yield: Bool, next: Bool)! = next {
    .true! => (.true!, .false!)!
    .false! => (.false!, .true!)!
  } in (yield) loop
}

Send Type Commands

^Syntax
SendTypeCommand : Receiver ( type ID_List )

^{Dual | Destructs Type | Destructs Channel | Expression | Constructing Expression}

Having multiple types between ( and ) is just syntax sugar:

// the command
r(type T, U)
// is equivalent to
r(type T)(type U)

A send command can destruct (“specialize”) a universal type:

def id: [type T] [T] T = [type T] [x] x

def just_true = do {
  let b: Bool = .true!
  
  let f = id
  // specialize f
  f(type Bool)
  // f is now of type [Bool] Bool
  f(b)
  // f is now .true!
} in f

It can also be used with chan: Destructing [type X] chan T to dually construct (type X) T

type Any = (type T) T

def true_as_any: Any = chan return: [type T] chan T {
  return(type Bool)
  // return is now type chan Bool
  return.true!

  // could have been combined to
  // return (type Bool) .true!
}

Receive Type Commands

^Syntax
SendTypeCommand : Receiver [ type ID_List ]

^{Dual | Destructs Type | Destructs Channel | Pattern | Constructing Expression}

Having multiple names between [ and ] is just syntax sugar:

// the pattern
r[type X, Y]
// is equivalent to
r[type X][type Y]

A receive command can destruct an existential type:

def complicated_any_id: (Any) Any = [x] do {
  // receive the type
  x[type X]
  // x is now of type X
  let y: X = x
} in (type X) y

It can also be used with chan: Destructing (type T) chan R to dually construct [T] R

def id: [type T] [T] T = chan return: (type T) (T) chan T {
  return[type T]
  // return is now of type (T) chan T
  return[x]
  // return is now of type chan T
  return <> x
}

Future

Here the planned features are listed. You can read more and even actively help the language grow on the Par Discord

Primitives

^{Priority: Essential}

Replicables

^{Priority: Essential}

Extensible I/O via Rust-controlled objects

^{Priority: Essential}

Non-determinism

^{Priority: Essential}

Tagged types

^{Priority: High}

Traits

^{Priority: High}

Powerful pattern matching

^{Priority: Medium}

Records

^{Priority: Medium}

Reactive values

^{Priority: Low}

Appendix

Thank you for reading the Par documentation!

Read about more technical topics in the next chapters.

Contributors

TODO

Influences

TODO

Notation

Grammar

The grammar of Par is declared in Lexer and Syntax blocks. It uses the following notation:

• Sequences of capital letters like DIGIT represent lexer tokens

• Italic names in CamelCase like Item represent parser nonterminals

• Character sequences in monospace like type represent literals

• Characters may be represented using escape sequences, like \n

• • x^? means x, zero or once
  • x^* means x, zero or more
  • x⁺ means x, once or more
  • x^a..b means at least a and at most b of x

• x | y means either x or y

• [ and ] group characters together, like [x X] or [a-z]

• character sequences (and groups of them) can be negated by ~, like ~\n

• ( and ) group arbitrary rules for precedence

Glossary