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

Par Documentation