Changes between Version 20 and Version 21 of Language/Core


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

--

Legend:

Unmodified
Added
Removed
Modified
  • Language/Core

    v20 v21  
    33 * [wiki:Language/Core/Universes Universes]
    44 * [wiki:Language/Core/Variables Variables and Constructors]
    5  
    6 
    7 [[br]]
    8 == Binders ==
    9 
    10 {{{
    11 BINDER
    12    ::= NAMEDVAR | HAT | UNDERSCORE
    13 }}}
    14 
    15 These are used at binding positions in both types and expressions. The hat {{{(^)}}} binder adds a debruijn 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.
    16 
    17  * During type checking, evaluation and optimisation, named variables can be rewritten to debruijn indices to avoid name capture.
    18 
    19 [[br]]
    20 == Types ==
    21 We use the same syntax of "types" for terms of the Spec, Kind and Sort universes.
    22 
    23 {{{
    24 TYPE
    25   ::= VAR
    26    |  CON
    27    |  TYPE TYPE
    28    |  [ BINDER+ : TYPE ] . TYPE
    29    |  ( TYPE )
    30 
    31 (type sums)
    32    |  TYPE + TYPE
    33    |  !0
    34    |  $0
    35 
    36 (arrow types)
    37    |  TYPE ~> TYPE
    38    |  TYPE => TYPE
    39    |  TYPE -> TYPE
    40    |  TYPE -(TYPE | TYPE)> TYPE
    41 }}}
    42 
    43 A type can be a variable, constructor, universally quantified type, type application, parenthesised type, type sum or arrow type.
    44 
    45 A type sum can be the least-upper-bound of two types, the least effect, or the least closure.
    46 
    47 An arrow type can be the kind arrow, implication, the pure and empty function, or the effectful and closureful function.
    48 
    49  * The components of a type sum must have effect or closure kind.
    50  * The kind arrow and implication arrows must be fully applied.
    51  * With the function arrow, the first and last arguments are the parameter and return types. The second and third arguments are the effect and closure of the function.
    52 
    53 The following type expressions are equivalent:
    54  || {{{[BIND1 BIND2 : TYPE1] . TYPE2}}}    || = || {{{[BIND1 : TYPE1] . [BIND2 : TYPE1] . TYPE2}}} ||
    55  || {{{[BIND1 : TYPE1]. TYPE2 TYPE3}}} || = || {{{[BIND1 : TYPE1]. (TYPE2 TYPE3)}}} ||
    56  || {{{(TYPE)}}} || = || {{{TYPE}}} ||
    57  || {{{TYPE1 TYPE2 TYPE3}}} || = || {{{(TYPE1 TYPE2) TYPE3}}} ||
    58  || {{{TYPE1 + TYPE2}}} || = ||{{{TYPE2 + TYPE1}}} ||
    59  || {{{(TYPE1 + TYPE2) + TYPE3 }}} || = || {{{TYPE1 + (TYPE2 + TYPE3)}}} ||
    60  || {{{TYPE + !0}}} || = || {{{TYPE}}} ||
    61  || {{{TYPE + $0}}} || = || {{{TYPE}}} ||
    62  || {{{TYPE1 ~> TYPE2}}} || = || {{{(~>) TYPE1 TYPE2}}} ||
    63  || {{{TYPE1 => TYPE2}}} || = || {{{(=>) TYPE1 TYPE2}}} ||
    64  || {{{TYPE1 -(TYPE2 | TYPE3)> TYPE4}}} || = || {{{(->) TYPE1 TYPE2 TYPE3 TYPE4}}} ||
    65  || {{{TYPE1 -> TYPE2}}} || = || {{{(->) TYPE1 !0 $0 TYPE2}}} ||
    66  || {{{TYPE1 ~> TYPE2 ~> TYPE3}}} || = || {{{TYPE1 ~> (TYPE2 ~> TYPE3)}}} ||
    67  || {{{TYPE1 => TYPE2 => TYPE3}}} || = || {{{TYPE1 => (TYPE2 => TYPE3)}}} ||
    68  || {{{TYPE1 -> TYPE2 -> TYPE3}}} || = || {{{TYPE1 -> (TYPE2 -> TYPE3)}}} ||
    69  || {{{TYPE1 -> TYPE2 + TYPE3}}} || = || {{{(TYPE1 -> TYPE2) + TYPE3}}} ||
    70 
    71 
    72 
    73 Example types:
    74 {{{
    75 1)  Int r1
    76 
    77 2)  e + Read r1 + Write r2
    78 
    79 3)  [r:%]. Int r
    80 
    81 4)  [a: *]. a -> a
    82 
    83 5)  [r:%]. [e:!]. [c:$]. [a b:*].
    84       (a -(e | c)> b) -> List r a -(Read r + e | c)> List r b
    85 
    86 6)  [^^^:%].Int ^2 -> Int ^1 -(Read ^2 + Read ^1 + Alloc ^0 | Use ^2)> Int ^0
    87 }}}
    88 
     5 * [wiki:Language/Core/Types Types]
    896
    907[[br]]