Changes between Version 7 and Version 8 of Language/Core


Ignore:
Timestamp:
Dec 28, 2011, 5:30:35 AM (8 years ago)
Author:
benl
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Language/Core

    v7 v8  
    1818Constructors 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.
    1919
     20 * Constructors that end with a hash are used for unboxed types.
     21 * ddci-core also uses constructors with a hash to represent store locations ({{{L0#}}}) and region handles ({{{R0#}}}).
     22
     23
    2024=== 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
    3139
    3240=== Primitive named constructors ===
     
    3442The following constructors are baked into the language definition, have specific types, and cannot be redefined.
    3543
    36 The following are witness kind constructors, and classify witnesses of 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.
     44The 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.
    3745
    3846||=Name=||=Type=||=Description=||
     
    5058||{{{DistinctN}}}|| {{{% ~> % ~> ... ~> @}}} || (N >= 2). Regions are distinct, and non-overlapping. ||
    5159
     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]]
    5266The following are computation type constructors, and classify the dynamic behaviour of the system.
    5367||=Name=||=Type=||=Description=||
     
    6175||{{{Use}}}||{{{% -> $}}}||Use of some region.||
    6276||{{{DeepUse}}}||{{{* -> $}}}||Use of all material regions in some type.||
    63 
    64 
     77 
     78
     79[[br]]
     80== Binders ==
     81
     82{{{
     83BINDER
     84   ::= NAMEDVAR | HAT | UNDERSCORE
     85}}}
     86
     87These 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.
     88
     89 * During type checking, evaluation and optimisation, named variables are rewritten to deBruijn indices to avoid variable capture.
     90
     91[[br]]
    6592== Types ==
    6693
     
    6996  ::= VAR
    7097   |  CON
     98   |  TYPE TYPE
    7199   |  [ BINDER+ : TYPE ] . TYPE
    72    |  TYPE TYPE
    73100   |  ( TYPE )
    74101
     
    90117
    91118An 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.
    92123
    93124The following are equivalent:
     
    110141
    111142
     143
     144Examples:
     145{{{
     146
     147}}}
     148
     149
     150[[br]]
     151== Expressions ==
     152
     153{{{
     154EXP
     155  ::= VAR
     156   |  CON
     157   |  LITERAL
     158
     159(applications)
     160   |  EXP ARGS
     161
     162(lambda abstractions)
     163   |  \(BINDER+ : TYPE) . EXP
     164
     165(non-recursive 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
     182ARGS
     183  ::= EXP
     184   |  { TYPE }     |  {: ARGTYPE+ :}
     185   |  < WITNESS >  |  <: ARGWITNESS+ :>
     186
     187ARGTYPE    ::= VAR | CON | !0 | $0 | (TYPE)
     188ARGWITNESS ::= VAR | CON | (WITNESS)
     189
     190
     191LETBIND 
     192  ::= BINDER        = EXP
     193  |   BINDER : TYPE = EXP
     194
     195LETBINDTYPED
     196  ::= BINDER : TYPE = EXP
     197
     198
     199TYPESIG
     200  ::= VAR : TYPE
     201
     202
     203ALT     ::= PAT -> EXP
     204PAT     ::= UNDERSCORE | CON PATBIND+
     205PATBIND ::= BINDER | BINDER : TYPE
     206}}}
     207
     208Applications 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