wiki:Language/Core

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:

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)
Uread[r:%].Const r => Pure (Read 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

 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.