Version 17 (modified by benl, 8 years ago) (diff) |
---|

# DDC Core Language

## The Five Universes

DDC core uses a four level hierarchy, consisting of five distinct universes.

Level Universe Example terms 3: Sort @@ ** | 2: Kind * % ! $ (* ~> *) (% ~> !) | 1: Spec (Int r1) ([a : *]. a -> Char r1) / \ 0: Comp Witness (5 {r1} ()) (\(x : Unit). x) {comp} (read {r1} <w1>) {witness}

- Level 0: Computations. Expressions in this universe are manipulated at runtime to make the program work. Values, regions, effects, closures and non-termination all live here.
- Level 0: Witnesses, also known as "capabilities", or "proof terms". When a witness exists in the program, a certain property of the system is guaranteed to be true.
- Level 1: Specifications. In Haskell these are called "types", but we avoid using that word here because we overload it to mean "kinds" and "sorts" as well. Specs classify both computation and witness expressions. A specification of a computation gives an upper bound on what might happen at runtime. A specification of a witness describes what property is true when the witness exists in the program.
- Level 2: Kinds. Kinds classify specifications.
- Level 3: Sort. Sorts classify kinds.

- In contrast to a language such as Gallina(Coq) or Agda, we only have a finite number of universe levels, and the structure of the higher levels is simpler than the lower ones.

## Variables and Constructors

VAR ::= NAMEDVAR | INDEXVAR NAMEDVAR ::= LOWER VARCHAR* INDEXVAR ::= HAT DIGIT+ CON ::= NAMEDCON | SYMBOLCON NAMEDCON ::= UPPER VARCHAR* HASH? SYMBOLCON ::= @@ | ** | * | % | ! | $ | @ | (~>) | (=>) | (->) VARCHAR ::= LOWER | UPPER | DIGIT | UNDERSCORE | PRIME

Variables can be named or be defined via a deBruijn index. Named variables start with a lower case letter, and can be followed by upper and lower case letters, digits, underscores and primes. Index variables start with a hat and are followed by some digits.

Constructors can have textual or symbolic names. A textual constructor starts with an upper case letter, and can be followed by upper and lower case letters, digits, underscores and primes. Named constructors can optionally end with a hash.

- Constructors that end with a hash are used for unboxed types.
- ddci-core also uses constructors with a hash to represent store locations (
`L0#`) and region handles (`R0#`).

### Symbolic constructors

Name Syntax Universe Classification Prop sort @@sort Data sort **sort Data kind *kind * :: **Region kind %kind % :: **Effect kind !kind ! :: **Closure kind $kind $ :: **Witness kind @kind @ :: @@Kind arrow (~>)kind kind ~> kindImplication arrow (=>)type (=>) :: @@ -> @@or(=>) :: @@ -> **Function arrow (->)type (->) :: * -> ! -> $ -> * -> *

- The kind arrow
`(~>)`takes any kind to any kind, for example, both`* ~> *`and`% ~>!`are well typed. - The implication arrow
`(=>)`can have two possible kinds, shown above. - The function arrow classifies a computation abstraction, which might diverge or perform some other effect when it is applied.
- The implication arrow classifies a witness abstraction, which is always pure and total. The application of a witness to a witness abstraction does not perform an effect, and corresponds to logical implication elimination (modus ponens).

### Primitive named constructors

The following witness kind constructors are baked into the language, have specific types, and cannot be redefined.

Name Type Description Pure! ~> @Purity of an effect. Empty$ ~> @Emptiness of a closure. Global% ~> @Region is allocated in the global pool. DeepGlobal* ~> @All material regions in some type are allocated in the global pool. Const% ~> @Region is constant. DeepConst* ~> @All material regions in some type are constant. Mutable% ~> @Region is mutable. DeepMutable* ~> @All material regions in some type are mutable. Lazy% ~> @Region may contain thunks. HeadLazy* ~> @Head region in some type may contain thunks. Direct% ~> @Region does not contain thunks. DistinctN% ~> % ~> ... ~> @(N >= 2). Regions are distinct, and non-overlapping.

- An effect is
`Pure`when it contains no`Write`components, and all its`Read`and`Alloc`components affect regions that are`Const`. - A closure is
`Empty`when all its`Use`components are on regions that are`Global` - A region cannot be
`Const`and`Mutable`at the same time. - A region cannot be
`Lazy`and`Direct`at the same time.

The following are computation type constructors, and classify the dynamic behaviour of the system.

Name Type Description Read% -> !Read effect on some region HeadRead* -> !Read effect on the head region of some type. DeepRead* -> !Read effect on all material regions in some type. Write% -> !Write effect on some region DeepWrite* -> !Write effect on all material regions in some type. Alloc% -> !Allocation effect on some region. DeepAlloc* -> !Allocation effect on all material regions in some type. Use% -> $Use of some region. DeepUse* -> $Use of all material regions in some type.

## Binders

BINDER ::= NAMEDVAR | HAT | UNDERSCORE

These are used at binding positions in both types and expressions. The hat `(^)` adds deDebruijn index to the stack. The underscore (_) is a non-binding binder, or alternatively, is sugar for a named variable that is not free in the body of the binding construct.

- During type checking, evaluation and optimisation, named variables are rewritten to deBruijn indices to avoid variable capture.

## Types

We use the same syntax of "types" for terms of the Spec, Kind and Sort universes.

TYPE ::= VAR | CON | TYPE TYPE | [ BINDER+ : TYPE ] . TYPE | ( TYPE ) (type sums) | TYPE + TYPE | !0 | $0 (arrow types) | TYPE ~> TYPE | TYPE => TYPE | TYPE -> TYPE | TYPE -(TYPE | TYPE)> TYPE

A type can be a variable, constructor, universally quantified type, type application, parenthesised type, type sum or arrow type.

A type sum can also be the least-upper-bound of two types, the least effect, or the least closure.

An arrow type can be the kind arrow, implication, the pure and empty function, the effectful and closureful function.

- The components of a type sum must have effect or closure kind.
- The kind arrow and implication arrows must be fully applied.
- With the function arrow, the first and last type arguments are the parameter and return types. The second and third type arguments are the effect and closure of the function.

The following type expressions are equivalent:

[BIND1 BIND2 : TYPE1] . TYPE2= [BIND1 : TYPE1] . [BIND2 : TYPE1] . TYPE2[BIND1 : TYPE1]. TYPE2 TYPE3= [BIND1 : TYPE1]. (TYPE2 TYPE3)(TYPE)= TYPETYPE1 TYPE2 TYPE3= (TYPE1 TYPE2) TYPE3TYPE1 + TYPE2= TYPE2 + TYPE1(TYPE1 + TYPE2) + TYPE3= TYPE1 + (TYPE2 + TYPE3)TYPE + !0= TYPETYPE + $0= TYPETYPE1 ~> TYPE2= (~>) TYPE1 TYPE2TYPE1 => TYPE2= (=>) TYPE1 TYPE2TYPE1 -(TYPE2 | TYPE3)> TYPE4= (->) TYPE1 TYPE2 TYPE3 TYPE4TYPE1 -> TYPE2= (->) TYPE1 !0 $0 TYPE2TYPE1 ~> TYPE2 ~> TYPE3= TYPE1 ~> (TYPE2 ~> TYPE3)TYPE1 => TYPE2 => TYPE3= TYPE1 => (TYPE2 => TYPE3)TYPE1 -> TYPE2 -> TYPE3= TYPE1 -> (TYPE2 -> TYPE3)TYPE1 -> TYPE2 + TYPE3= (TYPE1 -> TYPE2) + TYPE3

Example types:

1) Int r1 2) e + Read r1 + Write r2 3) [r:%]. Int r 4) [a: *]. a -> a 5) [r:%]. [e:!]. [c:$]. [a b:*]. (a -(e | c)> b) -> List r a -(Read r + e | c)> List r b 6) [^^^:%].Int ^2 -> Int ^1 -(Read ^2 + Read ^1 + Alloc ^0 | Use ^2)> Int ^0

## Witnesses

WIT ::= VAR | WCON | WIT WARGS | WIT & WIT | ( WIT ) WARGS ::= ARGTYPES | ARGWITS ARGTYPES ::= { TYPE } | {: ARGTYPE+ :} ARGWITS ::= < WIT > | <: ARGWIT+ :> ARGTYPE ::= VAR | CON | !0 | $0 | (TYPE) ARGWIT ::= VAR | CON | (WITNESS)

A witness can be a variable, witness constructor, witness application or witness join. All the witness constructors are baked in, and are listed below.

Witness constructors:

Name Type U purePure !0U emptyEmpty !0R global[r:%].Global rR const[r:%].Const rR mutable[r:%].Mutable rR lazy[r:%].Lazy rR direct[r:%].Direct rR distinctN[r1 .. rN:%].DistinctN r1 .. rNU use[r:%].Global r => Const r => Empty (Use r)U read[r:%].Const r => Pure (Read r)U alloc[r:%].Const r => Pure (Alloc r)

- Runtime witness constructors are marked with (R), and are introduced into the program at runtime. They cannot appear in the source code. They are introduced by the system only when the associated property is true, and the type system ensures that they are eliminated from the program when this is no longer the case.
- User witness constructors are marked with (U), and can be used in the source program. The user witness constructors are either always true, as with the axioms
`pure`and`empty`, or combine existing witnesses, as with`use`,`read`and`alloc`.

- Only witnesses of types
`Pure t`or`Empty t`can be joined, for some type`t`.

The following witness expressions are equivalent:

WIT1 WIT2 WIT3= (WIT1 WIT2) WIT3distinct3 {r1} {r2} {r3}= distinct3 {:r1 r2 r3:}WIT1 & WIT2= WIT2 & WIT1(WIT1 & WIT2) & WIT3= WIT1 & (WIT2 & WIT3)

Example witnesses:

1) pure :: Pure !0 2) const {r1} :: Const r1 3) read {r1} <w1> :: Pure (Read r1) ... where w1 :: Const r1 4) read {r1} <w1> & alloc {r2} <w2> :: Pure (Read r1 + Alloc r1) ... where w1 :: Const r1 and w2 :: Const r2

## Expressions

EXP ::= VAR | CON | LITERAL (applications) | EXP XARGS (lambda abstractions) | \(BINDER+ : TYPE) . EXP (non-recursive and recursive let binding) | let LETBIND in EXP | letrec LETBINDTYPED+ in EXP (region introduction and context) | letregion BINDER with { TYPESIG* } in EXP | letregion BINDER in EXP | withregion VAR in EXP (case expression) | case EXP of { ALT+ } (type casts) | weakeff ARGTYPE EXP | weakclo ARGTYPE EXP | purify < WITNESS > EXP | forget < WITNESS > EXP XARGS ::= EXP | { TYPE } | {: ARGTYPE+ :} | < WITNESS > | <: ARGWITNESS+ :> LETBIND ::= BINDER = EXP | BINDER : TYPE = EXP LETBINDTYPED ::= BINDER : TYPE = EXP TYPESIG ::= VAR : TYPE ALT ::= PAT -> EXP PAT ::= UNDERSCORE | CON PATBIND+ PATBIND ::= BINDER | BINDER : TYPE

Applications are between an expression and an argument. The argument may be another expression, a type or a witness. Types used as arguments are wrapped in braces, while witnesses used as arguments are wrapped in angle brackets.