Changes between Version 10 and Version 11 of Language/Core


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

--

Legend:

Unmodified
Added
Removed
Modified
  • Language/Core

    v10 v11  
    5656|| Effect kind || {{{!}}} || kind || {{{! :: **}}} ||
    5757|| Closure kind || {{{$}}} || kind || {{{$ :: **}}} ||
     58|| Witness kind || {{{@}}} || kind || {{{@ :: @@}}} ||
    5859|| Kind arrow || {{{(~>)}}} || kind || {{{ kind ~> kind}}}  ||
    5960|| Implication arrow || {{{(=>)}}} || type || {{{(=>) :: @@ -> @@}}} or {{{(=>) ::  @@ -> **}}} ||
     
    116117[[br]]
    117118== Types ==
     119We use the same syntax of "types" for terms of the Spec, Kind and Sort universes.
    118120
    119121{{{
     
    143145An arrow type can be the kind arrow, implication, the pure and empty function, the effectful and closureful function.
    144146
    145  * 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.
    146147 * The components of a type sum must have effect or closure kind.
    147148 * The kind arrow and implication arrows must be fully applied.
    148 
    149 The following are equivalent:
     149 * With the function arrow, the first and last type arguments are the parameter and return types. The second and third type arguments are the effect and closure of the function.
     150
     151The following type expressions are equivalent:
    150152|| {{{[BIND1 BIND2 : TYPE1] . TYPE2}}}    || = || {{{[BIND1 : TYPE1] . [BIND2 : TYPE1] . TYPE2}}} ||
    151153|| {{{[BIND1 : TYPE1]. TYPE2 TYPE3}}} || = || {{{[BIND1 : TYPE1]. (TYPE2 TYPE3)}}} ||
     
    187189== Witnesses ==
    188190
     191{{{
     192WITNESS
     193   ::= VAR
     194    |  WCON
     195    |  WITNESS WARGS
     196    |  WITNESS & WITNESS
     197
     198WARGS    ::= ARGTYPES | ARGWITS
     199
     200ARGTYPES ::= { TYPE }    | {: ARGTYPE+ :}
     201ARGWITS  ::= < WITNESS > | <: ARGWIT+  :>
     202
     203ARGTYPE  ::= VAR | CON | !0 | $0 | (TYPE)
     204ARGWIT   ::= VAR | CON | (WITNESS)
     205}}}
     206
     207
     208A witness can be a variable, witness constructor, witness application or witness join. All the witness constructors are baked in, and are listed below.
     209
     210Witness 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)}}}||
     223
     224 * 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.
     225 * User witness constructors are marked with (U), and can be used in the source program. The user witness constructors are either always true, as with the axioms {{{pure}}} and {{{empty}}}, or combine existing witnesses, as with {{{use}}}, {{{read}}} and {{{alloc}}}.
     226
     227 * Only witnesses of types {{{Pure t}}} or {{{Empty t}}} can be joined, for some type {{{t}}}.
     228
     229Example witnesses:
     230
     231{{{
     232 1) pure  :: Pure !0
     233
     234 2) const r1 :: Const r1
     235
     236 3) given  w1 :: Const r1
     237
     238     read {r1} <w1> :: Pure (Read r1)
     239     
     240 4) given w1 :: Const r1  and  w2 :: Const r2
     241
     242     read {r1} <w1> & alloc {r2} <w2> :: Pure (Read r1 + Alloc r1)
     243}}}
     244
    189245
    190246[[br]]
     
    198254
    199255(applications)
    200    |  EXP ARGS
     256   |  EXP XARGS
    201257
    202258(lambda abstractions)
     
    222278
    223279
    224 ARGS
     280XARGS
    225281  ::= EXP
    226282   |  { TYPE }     |  {: ARGTYPE+ :}
    227283   |  < WITNESS >  |  <: ARGWITNESS+ :>
    228284
    229 ARGTYPE    ::= VAR | CON | !0 | $0 | (TYPE)
    230 ARGWITNESS ::= VAR | CON | (WITNESS)
    231 
    232285
    233286LETBIND