Safe Haskell | Safe-Infered |
---|
Universes of the Disciple Core language.
- data Universe
- universeFromType3 :: Type n -> Maybe Universe
- universeFromType2 :: Type n -> Maybe Universe
- universeFromType1 :: Type n -> Maybe Universe
- universeOfType :: Type n -> Maybe Universe
Documentation
Universes of the Disciple Core language.
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 UniverseSource
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 UniverseSource
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.
universeFromType1 :: Type n -> Maybe UniverseSource
Given the type of some thing (up one level),
yield the universe of the original thing, or Nothing
if it was badly formed.
universeOfType :: Type n -> Maybe UniverseSource
Yield the universe of some type.
universeOfType (tBot kEffect) = UniverseSpec universeOfType kRegion = UniverseKind