Changes between Version 19 and Version 20 of Language/Core


Ignore:
Timestamp:
Dec 28, 2011, 9:41:32 AM (8 years ago)
Author:
benl
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Language/Core

    v19 v20  
    22
    33 * [wiki:Language/Core/Universes Universes]
    4 
    5 [[br]]
    6 == Variables and Constructors ==
    7 {{{
    8 VAR        ::= NAMEDVAR | INDEXVAR
    9 NAMEDVAR   ::= LOWER VARCHAR*
    10 INDEXVAR   ::= HAT DIGIT+
    11 
    12 CON        ::= NAMEDCON | SYMBOLCON
    13 NAMEDCON   ::= UPPER VARCHAR* HASH?
    14 SYMBOLCON  ::= @@ | ** |  * | % | ! | $ | @ | (~>) | (=>) | (->)
    15 
    16 VARCHAR    ::= LOWER | UPPER | DIGIT | UNDERSCORE | PRIME
    17 }}}
    18 
    19 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.
    20 
    21 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.
    22 
    23  * The {{{CON}}} grammar is used for both type and data constructors. Witness constructors have their own grammar.
    24  * Constructors that end with a hash are used for unboxed types.
    25  * ddci-core also uses constructors with a hash to represent store locations ({{{L0#}}}) and region handles ({{{R0#}}}).
    26 
    27 
    28 === Symbolic constructors ===
    29  ||=Name=||=Syntax=||=Universe=||=Classification=||
    30  || Prop sort || {{{@@}}} || sort || ||
    31  || Data sort || {{{**}}} || sort || ||
    32  || Data kind || {{{*}}} || kind || {{{* :: **}}} ||
    33  || Region kind || {{{%}}} || kind || {{{% :: **}}} ||
    34  || Effect kind || {{{!}}} || kind || {{{! :: **}}} ||
    35  || Closure kind || {{{$}}} || kind || {{{$ :: **}}} ||
    36  || Witness kind || {{{@}}} || kind || {{{@ :: @@}}} ||
    37  || Kind arrow || {{{(~>)}}} || kind || {{{ kind ~> kind}}}  ||
    38  || Implication arrow || {{{(=>)}}} || type || {{{(=>) :: @@ -> @@}}} or {{{(=>) ::  @@ -> **}}} ||
    39  || Function arrow || {{{(->)}}} || type || {{{(->) :: * -> ! -> $ -> * -> *}}} ||
    40 
    41  * The kind arrow {{{(~>)}}} takes any kind to any kind, for example, both {{{* ~> *}}} and {{{% ~>!}}} are well typed.
    42  * The implication arrow {{{(=>)}}} can have two possible kinds, shown above.
    43  * 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).
    44  * The function arrow classifies a computation abstraction, which might diverge or perform some other effect when it is applied.
    45 
    46 === Primitive named constructors ===
    47 
    48 The following witness type constructors are baked into the language, have specific types, and cannot be redefined.
    49 
    50  ||=Name=||=Type=||=Description=||
    51  ||{{{Pure}}}|| {{{! ~> @}}} || Purity of an effect. ||
    52  ||{{{Empty}}}|| {{{$ ~> @}}} || Emptiness of a closure. ||
    53  ||{{{Global}}}|| {{{% ~> @}}} || Objects in global regions are allocated in the heap, instead of on local stacks. ||
    54  ||{{{DeepGlobal}}}|| {{{* ~> @}}} || All material regions in some type are global. ||
    55  ||{{{Const}}}|| {{{% ~> @}}} || Objects in constant regions cannot be destructively updated. ||
    56  ||{{{DeepConst}}}|| {{{* ~> @}}} || All material regions in some type are constant. ||
    57  ||{{{Mutable}}}|| {{{% ~> @}}} || Objects in mutable regions may be destructively updated. ||
    58  ||{{{DeepMutable}}}|| {{{* ~> @}}} || All material regions in some type are mutable. ||
    59  ||{{{Lazy}}}|| {{{% ~> @}}} || Lazy regions may contain thunks instead of manifest objects. ||
    60  ||{{{HeadLazy}}}|| {{{* ~> @}}} || Head region in some type may contain thunks. ||
    61  ||{{{Manifest}}}|| {{{% ~> @}}} || Manifest regions do not contain thunks. ||
    62  ||{{{DistinctN}}}|| {{{% ~> % ~> ... ~> @}}} || (N >= 2). Regions are distinct, and non-overlapping. ||
    63 
    64  * An effect is {{{Pure}}} when it contains no {{{Write}}} components, and all its {{{Read}}} and {{{Alloc}}} components affect regions that are {{{Const}}}.
    65  * A closure is {{{Empty}}} when all its {{{Use}}} components are on regions that are {{{Global}}}
    66  * A region cannot be {{{Const}}} and {{{Mutable}}} at the same time.
    67  * A region cannot be {{{Lazy}}} and {{{Manifest}}} at the same time.
    68 
    69 [[br]]
    70 The following are computation type constructors.
    71  ||=Name=||=Type=||=Description=||
    72  ||{{{Read}}}||{{{% -> !}}}||Read effect on some region||
    73  ||{{{HeadRead}}}||{{{* -> !}}}||Read effect on the head region of some type.||
    74  ||{{{DeepRead}}}||{{{* -> !}}}||Read effect on all material regions in some type.||
    75  ||{{{Write}}}||{{{% -> !}}}||Write effect on some region||
    76  ||{{{DeepWrite}}}||{{{* -> !}}}||Write effect on all material regions in some type.||
    77  ||{{{Alloc}}}||{{{% -> !}}}||Allocation effect on some region.||
    78  ||{{{DeepAlloc}}}||{{{* -> !}}}||Allocation effect on all material regions in some type.||
    79  ||{{{Use}}}||{{{% -> $}}}||Use of some region.||
    80  ||{{{DeepUse}}}||{{{* -> $}}}||Use of all material regions in some type.||
     4 * [wiki:Language/Core/Variables Variables and Constructors]
    815 
    826