Changes between Version 9 and Version 10 of Language/Core


Ignore:
Timestamp:
Dec 28, 2011, 6:20:19 AM (8 years ago)
Author:
benl
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Language/Core

    v9 v10  
    1818}}}
    1919
    20  * Level 0: Computations. At runtime, expressions in this universe are manipulated at runtime to make the program work. Values, regions, effects, closures and non-termination all live here.
     20 * Level 0: Computations. Expressions in this universe are manipulated at runtime to make the program work. Values, regions, effects, closures and non-termination all live here.
    2121 * Level 0: Witnesses, also known as "capabilities", or "proof terms". When a witness exists in the program, a certain property of the system is guaranteed to be true.
    2222 * Level 1: Specifications. In Haskell these are called "types", but we avoid using that word here because we overload it to mean "kinds" and "sorts" as well. Specs classify both computation and witness expressions. A specification of a computation gives an upper bound on what might happen at runtime. A specification of a witness describes what property is true when the witness exists in the program.
     
    2424 * Level 3: Sort. Sorts classify kinds.
    2525
    26  * In contrast to a language such as Gallina(Coq) or Agda, we only have a finite number of universe levels, the structure of the higher levels is simpler than the lower ones.
     26 * In contrast to a language such as Gallina(Coq) or Agda, we only have a finite number of universe levels, and the structure of the higher levels is simpler than the lower ones.
    2727
    2828
     
    6262 * The kind arrow {{{(~>)}}} takes any kind to any kind, for example, both {{{* ~> *}}} and {{{% ~>!}}} are well typed.
    6363 * The implication arrow {{{(=>)}}} can have two possible kinds, shown above.
    64 
     64 * The function arrow classifies a computation abstraction, which might diverge or perform some other effect when it is applied.
     65 * 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).
    6566
    6667=== Primitive named constructors ===
    6768
    68 The following constructors are baked into the language definition, have specific types, and cannot be redefined.
    69 
    70 The 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.
     69The following witness kind constructors are baked into the language, have specific types, and cannot be redefined.
    7170
    7271||=Name=||=Type=||=Description=||
     
    168167
    169168
    170 Examples:
    171 {{{
    172 
     169Example types:
     170{{{
     1711)  Int r1
     172
     1732)  e + Read r1 + Write r2
     174
     1753)  [r:%]. Int r
     176
     1774)  [a: *]. a -> a
     178
     1795)  [r:%]. [e:!]. [c:$]. [a b:*].
     180      (a -(e | c)> b) -> List r a -(Read r + e | c)> List r b
     181
     1826)  [^^^:%].Int ^2 -> Int ^1 -(Read ^2 + Read ^1 + Alloc ^0 | Use ^2)> Int ^0
    173183}}}
    174184