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

# DDC Core Language

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