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
}