Safe Haskell | Safe |
---|---|
Language | Haskell98 |
- data Binder n
- data Bind n
- data Bound n
- data Type n
- type Sort n = Type n
- type Kind n = Type n
- type Region n = Type n
- type Effect n = Type n
- type Closure n = Type n
- data TypeSum n
- = TypeSumBot {
- typeSumKind :: !(Kind n)
- | TypeSumSet {
- typeSumKind :: !(Kind n)
- typeSumElems :: !(Array TyConHash (Set (TypeSumVarCon n)))
- typeSumBoundNamed :: !(Map n (Kind n))
- typeSumBoundAnon :: !(Map Int (Kind n))
- typeSumSpill :: ![Type n]
- = TypeSumBot {
- data TyConHash = TyConHash !Int
- data TypeSumVarCon n
- = TypeSumVar !(Bound n)
- | TypeSumCon !(Bound n) !(Kind n)
- data TyCon n
- = TyConSort !SoCon
- | TyConKind !KiCon
- | TyConWitness !TwCon
- | TyConSpec !TcCon
- | TyConBound !(Bound n) !(Kind n)
- | TyConExists !Int !(Kind n)
- data SoCon
- data KiCon
- data TwCon
- data TcCon
Documentation
A variable binder with its type.
A bound occurrence of a variable, with its type.
If variable hasn't been annotated with its real type then this
can be tBot
(an empty sum).
A value type, kind, or sort.
We use the same data type to represent all three universes, as they have a similar algebraic structure.
A least upper bound of several types.
We keep type sums in this normalised format instead of joining them
together with a binary operator (like (+)
). This makes sums easier to work
with, as a given sum type often only has a single physical representation.
TypeSumBot | |
| |
TypeSumSet | |
|
Hash value used to insert types into the typeSumElems
array of a TypeSum
.
data TypeSumVarCon n Source #
Wraps a variable or constructor that can be added the typeSumElems
array.
TypeSumVar !(Bound n) | |
TypeSumCon !(Bound n) !(Kind n) |
Show n => Show (TypeSumVarCon n) Source # | |
Kind, type and witness constructors.
These are grouped to make it easy to determine the universe that they belong to.
TyConSort !SoCon | (level 3) Builtin Sort constructors. |
TyConKind !KiCon | (level 2) Builtin Kind constructors. |
TyConWitness !TwCon | (level 1) Builtin Spec constructors for the types of witnesses. |
TyConSpec !TcCon | (level 1) Builtin Spec constructors for types of other kinds. |
TyConBound !(Bound n) !(Kind n) | User defined type constructor. |
TyConExists !Int !(Kind n) | An existentially quantified name, with its kind. Used during type checking, but not accepted in source programs. |
Sort constructor.
Kind constructor.
KiConFun | Function kind constructor. This is only well formed when it is fully applied. |
KiConWitness | Kind of witnesses. |
KiConData | Kind of data values. |
KiConRegion | Kind of regions. |
KiConEffect | Kind of effects. |
KiConClosure | Kind of closures. |
Witness type constructors.
TwConImpl | |
TwConPure | Purity of some effect. |
TwConConst | Constancy of some region. |
TwConDeepConst | Constancy of material regions in some type |
TwConMutable | Mutability of some region. |
TwConDeepMutable | Mutability of material regions in some type. |
TwConDistinct Int | Distinctness of some n regions |
TwConDisjoint | Non-interfering effects are disjoint. Used for rewrite rules. |
Other constructors at the spec level.
TcConUnit | The unit data type constructor is baked in. |
TcConFun | Pure function. |
TcConSusp | A suspended computation. |
TcConRead | Read of some region. |
TcConHeadRead | Read the head region in a data type. |
TcConDeepRead | Read of all material regions in a data type. |
TcConWrite | Write of some region. |
TcConDeepWrite | Write to all material regions in some data type. |
TcConAlloc | Allocation into some region. |
TcConDeepAlloc | Allocation into all material regions in some data type. |