wiki:Language/Core/Universes

The Five Universes

Disciple Core uses a four level hierarchy, consisting of five distinct universes.

 Level        Universe        Example terms

   3:           Sort          Prop  Comp
                  |
   2:           Kind          Data  Region  Effect  Closure  (Data ~> Data)  (Region ~> Effect)
                  |
   1:           Spec          (Int r1)  ([a : Data]. a -> Char r1)
                /   \
   0:       Data    Witness   5#   (\(x : Unit). x)   {data}
                              (read [r1] w1)          {witness}
  • Level 0: Data values. These are physical data objects that take up space at runtime. This is like the Set universe in constructive logic, but the expressions may diverge or cause side effects.
  • Level 0: Witnesses. The existence of a witness in the program guarantees that some property about how it operates at runtime. For example, a witness of constancy of some region guarantees objects in that region will not be updated. This is like the Prop universe in constructive logic.
  • Level 1: Specifications. In Haskell these are called "types", but we avoid using that word here because it is overloaded 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.
  • Level 2: Kinds classify specifications.
  • Level 3: Sorts classify kinds.
  • 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.

History

  • 2011/12: Split the witness and spec universes. These used to be merged together, because we thought that level 0 things should exist at runtime, while level 1 and higher should be erased. The downside was that witnesses then needed to be classified by Kinds instead of Specs, and as witnesses referred to level 1 things like regions, the witness classifiers needed to be dependent kinds. Dependent kinds complicate other things in the implementation, so we moved witnesses down to level 0 to remove the reverse dependency. We followed GHC in this regard, which moved its type equality witnesses down to level 0 earlier in the same year.
Last modified 3 years ago Last modified on Mar 8, 2014, 4:20:49 AM