- data Type n
- type Kind n = Type n
- type Sort n = Type n
- type Region n = Type n
- type Effect n = Type n
- type Closure n = Type n
- data TypeSum n
- data TyConHash = TyConHash !Int
- data TypeSumVarCon n
- data TyCon n
- data SoCon
- data KiCon
- data TwCon
- data TcCon
- data Binder n
- data Bind n
- data Bound n
Types, Kinds, and Sorts
A value type, kind, or sort.
We use the same data type to represent all three universes, as they have a similar algebraic structure.
|TVar !(Bound n)|
|TCon !(TyCon n)|
|TForall !(Bind n) !(Type n)|
|TApp !(Type n) !(Type n)|
|TSum !(TypeSum n)|
Least upper bound.
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.
Wraps a variable or constructor that can be added the
Kind, type and witness constructors.
These are grouped to make it easy to determine the universe that they belong to.
(level 3) Builtin Sort constructors.
(level 2) Builtin Kind constructors.
(level 1) Builtin Spec constructors for the types of witnesses.
(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.
Function kind constructor. This is only well formed when it is fully applied.
Kind of witnesses.
Kind of data values.
Kind of regions.
Kind of effects.
Kind of closures.
Witness type constructors.
Purity of some effect.
Emptiness of some closure.
Globalness of some region.
Globalness of material regions in some type.
Constancy of some region.
Constancy of material regions in some type
Mutability of some region.
Mutability of material regions in some type.
Distinctness of some n regions
Laziness of some region.
Laziness of the primary region in some type.
Manifestness of some region (not lazy).
Non-interfering effects are disjoint. Used for rewrite rules.
Other constructors at the spec level.
The unit data type constructor is baked in.
Function with a latent effect and closure.
A suspended computation.
Read of some region.
Read the head region in a data type.
Read of all material regions in a data type.
Write of some region.
Write to all material regions in some data type.
Allocation into some region.
Allocation into all material regions in some data type.
Region is captured in a closure.
All material regions in a data type are captured in a closure.
A variable binder.
A variable binder with its type.
|BNone !(Type n)|
A variable with no uses in the body doesn't need a name.
|BAnon !(Type n)|
Nameless variable on the deBruijn stack.
|BName n !(Type n)|
Named variable in the environment.
A bound occurrence of a variable, with its type.
If variable hasn't been annotated with its real type then this
tBot (an empty sum).
Nameless variable that should be on the deBruijn stack.
Named variable that should be in the environment.
|UPrim !n !(Type n)|
Named primitive that has its type attached to it. The types of primitives must be closed.