Terms

Duo is based on a term language for the sequent calculus. In distinction to lambda calculus, the term language of natural deduction, we have a first-class treatment of both producers and consumers of each type. In addition, there is a third syntactic category, commands. Commands are executable pieces of code. For example, it is possible to define producers, consumers and commands at the toplevel of the program:

def prd someProducer := ...;
def cns someConsumer := ...;
def cmd  someCommand := ...;

Toplevel declarations of consumers and producers can additionally be annotated with a type scheme.

def prd someProducer : ... := ...;
def cns someConsumer : ... := ...;

For example, the polymorphic identity function is defined like so:

def prd id : forall (a : CBV). a -> a :=
  \x => x;

If a function is used recursively in its own body, the rec keyword is necessary:

def rec prd add := \x y => case x of {
    Z => y,
    S(x) => S(add x y)
}

There are five categories of terms in Duo:

• Core constructs, which are independent of any concrete type.
• Producer introduction rules
• Consumer introduction rules
• Producer elimination rules
• Consumer elimination rules

Core constructs

Duo supports control operators in the form of the \(\mu\) and \(\tilde\mu\) constructs of the \(\lambda\mu\tilde\mu\) calculus. Both constructs use identical syntax.

def prd ex1 := mu x. #ExitSuccess;
def cns ex2 := mu k. #ExitSuccess;

Producer Introduction Rules

The rules for data and codata types are given separately

Data Types

Introduction rules for producers of codata types are just uses of the corresponding constructors:

data Nat : CBV { Z, S(Nat) };
def prd ex1 := S(Z);

Codata Types

Introduction rules for producers of codata types consists of copattern matching.

codata Pair : (+a : CBV, +b : CBV) -> CBV {
    PiLeft(return a),
    PiRight(return b)
};

def prd ex1 : Pair(Nat,Bool) := cocase
  { PiLeft(*) => 5,
    PiRight(*) => True
  };

def prd ex2 : Pair(Nat,Bool) := cocase
  { PiLeft(k) => 5 >> k,
    PiRight(k) => True >> k
  };

Consumer Introduction Rules

The rules for data and codata types are given separately

Data Types

A consumer of a data type is introduced using pattern matching

def cns ex1 := case {
    Z => #ExitSuccess,
    S(x) => #ExitSuccess
};

Codata Types

Introduction rules for consumers of codata types use one of the available destructors.

def cns ex1 : NatStream := Head(mu x. #ExitSuccess);

Producer Elimination Rules

The rules for data and codata types are given separately

Data Types

TODO

Codata Types

TODO

Consumer Elimination Rules

The rules for data and codata types are given separately

Data Types

TODO

Codata Types

TODO