Version 18 (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}
```
• 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 classify specifications.
• Level 3: 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.

• The CON grammar is used for both type and data constructors. Witness constructors have their own grammar.
• 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

NameSyntaxUniverseClassification
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 ~> kind
Implication 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 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).
• The function arrow classifies a computation abstraction, which might diverge or perform some other effect when it is applied.

### Primitive named constructors

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

NameTypeDescription
Pure ! ~> @ Purity of an effect.
Empty \$ ~> @ Emptiness of a closure.
Global % ~> @ Objects in global regions are allocated in the heap, instead of on local stacks.
DeepGlobal * ~> @ All material regions in some type are global.
Const % ~> @ Objects in constant regions cannot be destructively updated.
DeepConst * ~> @ All material regions in some type are constant.
Mutable % ~> @ Objects in mutable regions may be destructively updated.
DeepMutable * ~> @ All material regions in some type are mutable.
Lazy % ~> @ Lazy regions may contain thunks instead of manifest objects.
HeadLazy * ~> @ Head region in some type may contain thunks.
Manifest % ~> @ Manifest regions do 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 Manifest at the same time.

The following are computation type constructors.

NameTypeDescription
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 (^) binder adds a debruijn 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 can be rewritten to debruijn indices to avoid name 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 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, or 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 arguments are the parameter and return types. The second and third 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) = TYPE TYPE1 TYPE2 TYPE3 = (TYPE1 TYPE2) TYPE3 TYPE1 + TYPE2 = TYPE2 + TYPE1 (TYPE1 + TYPE2) + TYPE3 = TYPE1 + (TYPE2 + TYPE3) TYPE + !0 = TYPE TYPE + \$0 = TYPE TYPE1 ~> TYPE2 = (~>) TYPE1 TYPE2 TYPE1 => TYPE2 = (=>) TYPE1 TYPE2 TYPE1 -(TYPE2 | TYPE3)> TYPE4 = (->) TYPE1 TYPE2 TYPE3 TYPE4 TYPE1 -> TYPE2 = (->) TYPE1 !0 \$0 TYPE2 TYPE1 ~> 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:

NameType
UpurePure !0
UemptyEmpty !0
Rglobal[r:%].Global r
Rconst[r:%].Const r
Rmutable[r:%].Mutable r
Rlazy[r:%].Lazy r
Rdirect[r:%].Direct r
RdistinctN[r1 .. rN:%].DistinctN r1 .. rN
Uuse[r:%].Global r => Const r => Empty (Use r)
Ualloc[r:%].Const r => Pure (Alloc r)
• Runtime witness constructors are marked with (R). These are introduced into the program at runtime and 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). These can be used in the source code. The user witness constructors are either always true, as with the axioms pure and empty, or combine existing witnesses in a sound way, 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) WIT3 distinct3 {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

... 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.