Changes between Version 7 and Version 8 of Language/Core
 Timestamp:
 Dec 28, 2011, 5:30:35 AM (8 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

Language/Core
v7 v8 18 18 Constructors can be named or symbolic. A named constructor starts with an upper case letter, and can be followed by upper and lower case letters, digits, underscores and primes. Named constructors can also optionally end with a hash. 19 19 20 * Constructors that end with a hash are used for unboxed types. 21 * ddcicore also uses constructors with a hash to represent store locations ({{{L0#}}}) and region handles ({{{R0#}}}). 22 23 20 24 === Symbolic constructors === 21 =Name==Syntax==Universe= 22  Prop sort  {{{@@}}}  sort  23  Data sort  {{{**}}}  sort  24  Data kind  {{{*}}}  kind  25  Region kind  {{{%}}}  kind  26  Effect kind  {{{!}}}  kind  27  Closure kind  {{{$}}}  kind  28  Kind arrow  {{{(~>)}}}  kind  29  Implication arrow  {{{(=>)}}}  type  30  Function arrow  {{{(>)}}}  type  25 =Name==Syntax==Universe==Classification= 26  Prop sort  {{{@@}}}  sort   27  Data sort  {{{**}}}  sort   28  Data kind  {{{*}}}  kind  {{{* :: **}}}  29  Region kind  {{{%}}}  kind  {{{% :: **}}}  30  Effect kind  {{{!}}}  kind  {{{! :: **}}}  31  Closure kind  {{{$}}}  kind  {{{$ :: **}}}  32  Kind arrow  {{{(~>)}}}  kind  {{{ kind ~> kind}}}  33  Implication arrow  {{{(=>)}}}  type  {{{(=>) :: @@ > @@}}} or {{{(=>) :: @@ > **}}}  34  Function arrow  {{{(>)}}}  type  {{{(>) :: * > ! > $ > * > *}}}  35 36 * The kind arrow {{{(~>)}}} takes any kind to any kind, for example, both {{{* ~> *}}} and {{{% ~>!}}} are well typed. 37 * The implication arrow {{{(=>)}}} can have two possible kinds, shown above. 38 31 39 32 40 === Primitive named constructors === … … 34 42 The following constructors are baked into the language definition, have specific types, and cannot be redefined. 35 43 36 The following are witness kind constructors, and classify witnesses ofsome operational property of the system. If a witness with the specified type exists in the program, then the associated property is guaranteed to be true.44 The following witness kind constructors are baked into the language, have specific types, and cannot be redefined. A witness kind classifies some operational property of the system. If a witness with the specified type exists in the program, then the associated property is guaranteed to be true. 37 45 38 46 =Name==Type==Description= … … 50 58 {{{DistinctN}}} {{{% ~> % ~> ... ~> @}}}  (N >= 2). Regions are distinct, and nonoverlapping.  51 59 60 * An effect is {{{Pure}}} when it contains no {{{Write}}} components, and all its {{{Read}}} and {{{Alloc}}} components affect regions that are {{{Const}}}. 61 * A closure is {{{Empty}}} when all its {{{Use}}} components are on regions that are {{{Global}}} 62 * A region cannot be {{{Const}}} and {{{Mutable}}} at the same time. 63 * A region cannot be {{{Lazy}}} and {{{Direct}}} at the same time. 64 65 [[br]] 52 66 The following are computation type constructors, and classify the dynamic behaviour of the system. 53 67 =Name==Type==Description= … … 61 75 {{{Use}}}{{{% > $}}}Use of some region. 62 76 {{{DeepUse}}}{{{* > $}}}Use of all material regions in some type. 63 64 77 78 79 [[br]] 80 == Binders == 81 82 {{{ 83 BINDER 84 ::= NAMEDVAR  HAT  UNDERSCORE 85 }}} 86 87 These are used at binding positions in both types and expressions. The hat {{{(^)}}} adds deDebruijn index to the stack. The underscore (_) is a nonbinding binder, or alternatively, is sugar for a named variable that is not free in the body of the binding construct. 88 89 * During type checking, evaluation and optimisation, named variables are rewritten to deBruijn indices to avoid variable capture. 90 91 [[br]] 65 92 == Types == 66 93 … … 69 96 ::= VAR 70 97  CON 98  TYPE TYPE 71 99  [ BINDER+ : TYPE ] . TYPE 72  TYPE TYPE73 100  ( TYPE ) 74 101 … … 90 117 91 118 An arrow type can be the kind arrow, implication, the pure and empty function, the effectful and closureful function. 119 120 * We use the same {{{TYPE}}} syntax to represent the types of value expressions, the types of witnesses, the kinds of types, and the sorts of kinds. 121 * The components of a type sum must have effect or closure kind. 122 * The kind arrow and implication arrows must be fully applied. 92 123 93 124 The following are equivalent: … … 110 141 111 142 143 144 Examples: 145 {{{ 146 147 }}} 148 149 150 [[br]] 151 == Expressions == 152 153 {{{ 154 EXP 155 ::= VAR 156  CON 157  LITERAL 158 159 (applications) 160  EXP ARGS 161 162 (lambda abstractions) 163  \(BINDER+ : TYPE) . EXP 164 165 (nonrecursive and recursive let binding) 166  let LETBIND in EXP 167  letrec LETBINDTYPED+ in EXP 168 169 (region introduction and context) 170  letregion BINDER with { TYPESIG* } in EXP 171  letregion BINDER in EXP 172  withregion VAR in EXP 173 174 (case expression) 175  case EXP of { ALT+ } 176 177 (type casts) 178  purify < WITNESS > EXP 179  forget < WITNESS > EXP 180 181 182 ARGS 183 ::= EXP 184  { TYPE }  {: ARGTYPE+ :} 185  < WITNESS >  <: ARGWITNESS+ :> 186 187 ARGTYPE ::= VAR  CON  !0  $0  (TYPE) 188 ARGWITNESS ::= VAR  CON  (WITNESS) 189 190 191 LETBIND 192 ::= BINDER = EXP 193  BINDER : TYPE = EXP 194 195 LETBINDTYPED 196 ::= BINDER : TYPE = EXP 197 198 199 TYPESIG 200 ::= VAR : TYPE 201 202 203 ALT ::= PAT > EXP 204 PAT ::= UNDERSCORE  CON PATBIND+ 205 PATBIND ::= BINDER  BINDER : TYPE 206 }}} 207 208 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. 209