DDC.Type.Universe

Universes of the Disciple Core language.

Documentation

data Universe

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 Prop universe in constructive logic.

UniverseData

(level 0). The universe of 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.

Instances

Eq Universe

Show Universe

universeFromType3 :: Type n -> Maybe Universe

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

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 Universe

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 Universe

Yield the universe of some type.

  universeOfType (tBot kEffect) = UniverseSpec
  universeOfType kRegion        = UniverseKind