| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
DDC.Type.Universe
Documentation
Universes of the Disciple Core language.
Constructors
| UniverseSort | (level 3). The universe of sorts. Sorts classify kinds. |
| UniverseKind | (level 2). The universe of kinds. Kinds classify specifications. |
| UniverseSpec | (level 1). The universe of specifications. Specifications classify both witnesses and data values. In the vanilla Haskell world "specifications" are known as "types", but here we use the former term because we overload the word "type" to refer to kinds and sorts as well. |
| UniverseWitness | (level 0). The universe of 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 |
| UniverseData | (level 0). The universe of data values.
These are physical data objects that take up space at runtime.
This is like the |
universeFromType3 :: Type n -> Maybe Universe Source
Given the type of the type of the type of some thing (up three levels),
yield the universe of the original thing, or Nothing it was badly formed.
universeFromType2 :: Type n -> Maybe Universe Source
Given the type of the type of some thing (up two levels),
yield the universe of the original thing, or Nothing if it was badly formed.