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 !)