| 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] |
