Changes between Version 18 and Version 19 of Language/Core


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

--

Legend:

Unmodified
Added
Removed
Modified
  • Language/Core

    v18 v19  
    11= DDC Core Language =
    22
    3 == The Five Universes ==
    4 
    5 DDC core uses a four level hierarchy, consisting of five distinct universes.
    6 
    7 {{{
    8  Level        Universe        Example terms
    9 
    10    3:           Sort          @@  **
    11                   |
    12    2:           Kind          *  %  !  $  (* ~> *)  (% ~> !)
    13                   |
    14    1:           Spec          (Int r1)  ([a : *]. a -> Char r1)
    15                 /   \
    16    0:       Comp    Witness   (5 {r1} ())  (\(x : Unit). x)   {comp}
    17                               (read {r1} <w1>)                {witness}
    18 }}}
    19 
    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.
    21  * 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.
    22  * 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.
    23  * Level 2: Kinds classify specifications.
    24  * Level 3: Sorts classify kinds.
    25 
    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.
     3 * [wiki:Language/Core/Universes Universes]
    274
    285[[br]]