Changes between Version 12 and Version 13 of Language/Core


Ignore:
Timestamp:
Dec 28, 2011, 7:12:49 AM (8 years ago)
Author:
benl
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Language/Core

    v12 v13  
    4949
    5050=== Symbolic constructors ===
    51 ||=Name=||=Syntax=||=Universe=||=Classification=||
    52 || Prop sort || {{{@@}}} || sort || ||
    53 || Data sort || {{{**}}} || sort || ||
    54 || Data kind || {{{*}}} || kind || {{{* :: **}}} ||
    55 || Region kind || {{{%}}} || kind || {{{% :: **}}} ||
    56 || Effect kind || {{{!}}} || kind || {{{! :: **}}} ||
    57 || Closure kind || {{{$}}} || kind || {{{$ :: **}}} ||
    58 || Witness kind || {{{@}}} || kind || {{{@ :: @@}}} ||
    59 || Kind arrow || {{{(~>)}}} || kind || {{{ kind ~> kind}}}  ||
    60 || Implication arrow || {{{(=>)}}} || type || {{{(=>) :: @@ -> @@}}} or {{{(=>) ::  @@ -> **}}} ||
    61 || Function arrow || {{{(->)}}} || type || {{{(->) :: * -> ! -> $ -> * -> *}}} ||
     51 ||=Name=||=Syntax=||=Universe=||=Classification=||
     52 || Prop sort || {{{@@}}} || sort || ||
     53 || Data sort || {{{**}}} || sort || ||
     54 || Data kind || {{{*}}} || kind || {{{* :: **}}} ||
     55 || Region kind || {{{%}}} || kind || {{{% :: **}}} ||
     56 || Effect kind || {{{!}}} || kind || {{{! :: **}}} ||
     57 || Closure kind || {{{$}}} || kind || {{{$ :: **}}} ||
     58 || Witness kind || {{{@}}} || kind || {{{@ :: @@}}} ||
     59 || Kind arrow || {{{(~>)}}} || kind || {{{ kind ~> kind}}}  ||
     60 || Implication arrow || {{{(=>)}}} || type || {{{(=>) :: @@ -> @@}}} or {{{(=>) ::  @@ -> **}}} ||
     61 || Function arrow || {{{(->)}}} || type || {{{(->) :: * -> ! -> $ -> * -> *}}} ||
    6262
    6363 * The kind arrow {{{(~>)}}} takes any kind to any kind, for example, both {{{* ~> *}}} and {{{% ~>!}}} are well typed.
     
    7070The following witness kind constructors are baked into the language, have specific types, and cannot be redefined.
    7171
    72 ||=Name=||=Type=||=Description=||
    73 ||{{{Pure}}}|| {{{! ~> @}}} || Purity of an effect. ||
    74 ||{{{Empty}}}|| {{{$ ~> @}}} || Emptiness of a closure. ||
    75 ||{{{Global}}}|| {{{% ~> @}}} || Region is allocated in the global pool. ||
    76 ||{{{DeepGlobal}}}|| {{{* ~> @}}} || All material regions in some type are allocated in the global pool. ||
    77 ||{{{Const}}}|| {{{% ~> @}}} || Region is constant. ||
    78 ||{{{DeepConst}}}|| {{{* ~> @}}} || All material regions in some type are constant. ||
    79 ||{{{Mutable}}}|| {{{% ~> @}}} || Region is mutable. ||
    80 ||{{{DeepMutable}}}|| {{{* ~> @}}} || All material regions in some type are mutable. ||
    81 ||{{{Lazy}}}|| {{{% ~> @}}} || Region may contain thunks. ||
    82 ||{{{HeadLazy}}}|| {{{* ~> @}}} || Head region in some type may contain thunks. ||
    83 ||{{{Direct}}}|| {{{% ~> @}}} || Region does not contain thunks. ||
    84 ||{{{DistinctN}}}|| {{{% ~> % ~> ... ~> @}}} || (N >= 2). Regions are distinct, and non-overlapping. ||
     72 ||=Name=||=Type=||=Description=||
     73 ||{{{Pure}}}|| {{{! ~> @}}} || Purity of an effect. ||
     74 ||{{{Empty}}}|| {{{$ ~> @}}} || Emptiness of a closure. ||
     75 ||{{{Global}}}|| {{{% ~> @}}} || Region is allocated in the global pool. ||
     76 ||{{{DeepGlobal}}}|| {{{* ~> @}}} || All material regions in some type are allocated in the global pool. ||
     77 ||{{{Const}}}|| {{{% ~> @}}} || Region is constant. ||
     78 ||{{{DeepConst}}}|| {{{* ~> @}}} || All material regions in some type are constant. ||
     79 ||{{{Mutable}}}|| {{{% ~> @}}} || Region is mutable. ||
     80 ||{{{DeepMutable}}}|| {{{* ~> @}}} || All material regions in some type are mutable. ||
     81 ||{{{Lazy}}}|| {{{% ~> @}}} || Region may contain thunks. ||
     82 ||{{{HeadLazy}}}|| {{{* ~> @}}} || Head region in some type may contain thunks. ||
     83 ||{{{Direct}}}|| {{{% ~> @}}} || Region does not contain thunks. ||
     84 ||{{{DistinctN}}}|| {{{% ~> % ~> ... ~> @}}} || (N >= 2). Regions are distinct, and non-overlapping. ||
    8585
    8686 * An effect is {{{Pure}}} when it contains no {{{Write}}} components, and all its {{{Read}}} and {{{Alloc}}} components affect regions that are {{{Const}}}.
     
    9191[[br]]
    9292The following are computation type constructors, and classify the dynamic behaviour of the system.
    93 ||=Name=||=Type=||=Description=||
    94 ||{{{Read}}}||{{{% -> !}}}||Read effect on some region||
    95 ||{{{HeadRead}}}||{{{* -> !}}}||Read effect on the head region of some type.||
    96 ||{{{DeepRead}}}||{{{* -> !}}}||Read effect on all material regions in some type.||
    97 ||{{{Write}}}||{{{% -> !}}}||Write effect on some region||
    98 ||{{{DeepWrite}}}||{{{* -> !}}}||Write effect on all material regions in some type.||
    99 ||{{{Alloc}}}||{{{% -> !}}}||Allocation effect on some region.||
    100 ||{{{DeepAlloc}}}||{{{* -> !}}}||Allocation effect on all material regions in some type.||
    101 ||{{{Use}}}||{{{% -> $}}}||Use of some region.||
    102 ||{{{DeepUse}}}||{{{* -> $}}}||Use of all material regions in some type.||
     93 ||=Name=||=Type=||=Description=||
     94 ||{{{Read}}}||{{{% -> !}}}||Read effect on some region||
     95 ||{{{HeadRead}}}||{{{* -> !}}}||Read effect on the head region of some type.||
     96 ||{{{DeepRead}}}||{{{* -> !}}}||Read effect on all material regions in some type.||
     97 ||{{{Write}}}||{{{% -> !}}}||Write effect on some region||
     98 ||{{{DeepWrite}}}||{{{* -> !}}}||Write effect on all material regions in some type.||
     99 ||{{{Alloc}}}||{{{% -> !}}}||Allocation effect on some region.||
     100 ||{{{DeepAlloc}}}||{{{* -> !}}}||Allocation effect on all material regions in some type.||
     101 ||{{{Use}}}||{{{% -> $}}}||Use of some region.||
     102 ||{{{DeepUse}}}||{{{* -> $}}}||Use of all material regions in some type.||
    103103 
    104104
     
    150150
    151151The following type expressions are equivalent:
    152 || {{{[BIND1 BIND2 : TYPE1] . TYPE2}}}    || = || {{{[BIND1 : TYPE1] . [BIND2 : TYPE1] . TYPE2}}} ||
    153 || {{{[BIND1 : TYPE1]. TYPE2 TYPE3}}} || = || {{{[BIND1 : TYPE1]. (TYPE2 TYPE3)}}} ||
    154 || {{{(TYPE)}}} || = || {{{TYPE}}} ||
    155 || {{{TYPE1 TYPE2 TYPE3}}} || = || {{{(TYPE1 TYPE2) TYPE3}}} ||
    156 || {{{TYPE1 + TYPE2}}} || = ||{{{TYPE2 + TYPE1}}} ||
    157 || {{{(TYPE1 + TYPE2) + TYPE3 }}} || = || {{{TYPE1 + (TYPE2 + TYPE3)}}} ||
    158 || {{{TYPE + !0}}} || = || {{{TYPE}}} ||
    159 || {{{TYPE + $0}}} || = || {{{TYPE}}} ||
    160 || {{{TYPE1 ~> TYPE2}}} || = || {{{(~>) TYPE1 TYPE2}}} ||
    161 || {{{TYPE1 => TYPE2}}} || = || {{{(=>) TYPE1 TYPE2}}} ||
    162 || {{{TYPE1 -(TYPE2 | TYPE3)> TYPE4}}} || = || {{{(->) TYPE1 TYPE2 TYPE3 TYPE4}}} ||
    163 || {{{TYPE1 -> TYPE2}}} || = || {{{(->) TYPE1 !0 $0 TYPE2}}} ||
    164 || {{{TYPE1 ~> TYPE2 ~> TYPE3}}} || = || {{{TYPE1 ~> (TYPE2 ~> TYPE3)}}} ||
    165 || {{{TYPE1 => TYPE2 => TYPE3}}} || = || {{{TYPE1 => (TYPE2 => TYPE3)}}} ||
    166 || {{{TYPE1 -> TYPE2 -> TYPE3}}} || = || {{{TYPE1 -> (TYPE2 -> TYPE3)}}} ||
    167 || {{{TYPE1 -> TYPE2 + TYPE3}}} || = || {{{(TYPE1 -> TYPE2) + TYPE3}}} ||
     152 || {{{[BIND1 BIND2 : TYPE1] . TYPE2}}}    || = || {{{[BIND1 : TYPE1] . [BIND2 : TYPE1] . TYPE2}}} ||
     153 || {{{[BIND1 : TYPE1]. TYPE2 TYPE3}}} || = || {{{[BIND1 : TYPE1]. (TYPE2 TYPE3)}}} ||
     154 || {{{(TYPE)}}} || = || {{{TYPE}}} ||
     155 || {{{TYPE1 TYPE2 TYPE3}}} || = || {{{(TYPE1 TYPE2) TYPE3}}} ||
     156 || {{{TYPE1 + TYPE2}}} || = ||{{{TYPE2 + TYPE1}}} ||
     157 || {{{(TYPE1 + TYPE2) + TYPE3 }}} || = || {{{TYPE1 + (TYPE2 + TYPE3)}}} ||
     158 || {{{TYPE + !0}}} || = || {{{TYPE}}} ||
     159 || {{{TYPE + $0}}} || = || {{{TYPE}}} ||
     160 || {{{TYPE1 ~> TYPE2}}} || = || {{{(~>) TYPE1 TYPE2}}} ||
     161 || {{{TYPE1 => TYPE2}}} || = || {{{(=>) TYPE1 TYPE2}}} ||
     162 || {{{TYPE1 -(TYPE2 | TYPE3)> TYPE4}}} || = || {{{(->) TYPE1 TYPE2 TYPE3 TYPE4}}} ||
     163 || {{{TYPE1 -> TYPE2}}} || = || {{{(->) TYPE1 !0 $0 TYPE2}}} ||
     164 || {{{TYPE1 ~> TYPE2 ~> TYPE3}}} || = || {{{TYPE1 ~> (TYPE2 ~> TYPE3)}}} ||
     165 || {{{TYPE1 => TYPE2 => TYPE3}}} || = || {{{TYPE1 => (TYPE2 => TYPE3)}}} ||
     166 || {{{TYPE1 -> TYPE2 -> TYPE3}}} || = || {{{TYPE1 -> (TYPE2 -> TYPE3)}}} ||
     167 || {{{TYPE1 -> TYPE2 + TYPE3}}} || = || {{{(TYPE1 -> TYPE2) + TYPE3}}} ||
    168168
    169169
     
    209209
    210210Witness constructors:
    211 ||||=Name=||=Type=||
    212 ||U||{{{pure}}}||{{{Pure !0}}}||
    213 ||U||{{{empty}}}||{{{Empty !0}}}||
    214 ||R||{{{global}}}||{{{[r:%].Global r}}}||
    215 ||R||{{{const}}}||{{{[r:%].Const r}}}||
    216 ||R||{{{mutable}}}||{{{[r:%].Mutable r}}}||
    217 ||R||{{{lazy}}}||{{{[r:%].Lazy r}}}||
    218 ||R||{{{direct}}}||{{{[r:%].Direct r}}}||
    219 ||R||{{{distinctN}}}||{{{[r1 .. rN:%].DistinctN r1 .. rN}}}||
    220 ||U||{{{use}}}||{{{[r:%].Global r => Const r => Empty (Use r)}}}||
    221 ||U||{{{read}}}||{{{[r:%].Const r => Pure (Read r)}}}||
    222 ||U||{{{alloc}}}||{{{[r:%].Const r => Pure (Alloc r)}}}||
     211 ||||=Name=||=Type=||
     212 ||U||{{{pure}}}||{{{Pure !0}}}||
     213 ||U||{{{empty}}}||{{{Empty !0}}}||
     214 ||R||{{{global}}}||{{{[r:%].Global r}}}||
     215 ||R||{{{const}}}||{{{[r:%].Const r}}}||
     216 ||R||{{{mutable}}}||{{{[r:%].Mutable r}}}||
     217 ||R||{{{lazy}}}||{{{[r:%].Lazy r}}}||
     218 ||R||{{{direct}}}||{{{[r:%].Direct r}}}||
     219 ||R||{{{distinctN}}}||{{{[r1 .. rN:%].DistinctN r1 .. rN}}}||
     220 ||U||{{{use}}}||{{{[r:%].Global r => Const r => Empty (Use r)}}}||
     221 ||U||{{{read}}}||{{{[r:%].Const r => Pure (Read r)}}}||
     222 ||U||{{{alloc}}}||{{{[r:%].Const r => Pure (Alloc r)}}}||
    223223
    224224 * Runtime witness constructors are marked with (R), and are introduced into the program at runtime. They 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.