Safe Haskell	Safe-Inferred

DDC.Type.Exp

Contents

Types, Kinds, and Sorts

Synopsis

Types, Kinds, and Sorts

data Type n Source

A value type, kind, or sort.

We use the same data type to represent all three universes, as they have a similar algebraic structure.

Constructors

TVar !(Bound n)	Variable.
TCon !(TyCon n)	Constructor.
TForall !(Bind n) !(Type n)	Abstraction.
TApp !(Type n) !(Type n)	Application.
TSum !(TypeSum n)	Least upper bound.

Instances

Rename Type
SpreadT Type
FreeVarConT Type
BindStruct Type
SubstituteT Type
SupportX Type
SubstituteTX Type
Ord n => MapBoundT Type n
Eq n => Eq (Type n)
Show n => Show (Type n)
(Pretty n, Eq n) => Pretty (Type n)
NFData n => NFData (Type n)

type Kind n = Type nSource

type Sort n = Type nSource

type Region n = Type nSource

type Effect n = Type nSource

type Closure n = Type nSource

data TypeSum n Source

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.

Constructors

TypeSumBot
Fields typeSumKind :: !(Kind n) The kind of the elements in this sum.
TypeSumSet
Fields typeSumKind :: !(Kind n) The kind of the elements in this sum. typeSumElems :: !(Array TyConHash (Set (TypeSumVarCon n))) Where we can see the outer constructor of a type, its argument is inserted into this array. This handles common cases like Read, Write, Alloc effects. typeSumBoundNamed :: !(Map n (Kind n)) A map for named type variables. typeSumBoundAnon :: !(Map Int (Kind n)) A map for anonymous type variables. typeSumSpill :: ![Type n] Types that can't be placed in the other fields go here. INVARIANT: this list doesn't contain more `TSum`s.

Instances

Rename TypeSum
SpreadT TypeSum
SubstituteT TypeSum
Ord n => MapBoundT TypeSum n
Eq n => Eq (TypeSum n)
Show n => Show (TypeSum n)
(Pretty n, Eq n) => Pretty (TypeSum n)
NFData n => NFData (TypeSum n)

data TyConHash Source

Hash value used to insert types into the typeSumElems array of a TypeSum.

Constructors

TyConHash !Int

Instances

Eq TyConHash
Ord TyConHash
Show TyConHash
Ix TyConHash
NFData TyConHash

data TypeSumVarCon n Source

Wraps a variable or constructor that can be added the typeSumElems array.

Constructors

TypeSumVar !(Bound n)
TypeSumCon !(Bound n) !(Kind n)

Instances

Eq n => Eq (TypeSumVarCon n)
Ord n => Ord (TypeSumVarCon n)
Show n => Show (TypeSumVarCon n)
NFData n => NFData (TypeSumVarCon n)

data TyCon n Source

Kind, type and witness constructors.

These are grouped to make it easy to determine the universe that they belong to.

Constructors

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.

Instances

SpreadT TyCon
BindStruct TyCon
Eq n => Eq (TyCon n)
Show n => Show (TyCon n)
(Eq n, Pretty n) => Pretty (TyCon n)
NFData n => NFData (TyCon n)

data SoCon Source

Sort constructor.

Constructors

SoConProp	Sort of witness kinds.
SoConComp	Sort of computation kinds.

Instances

Eq SoCon
Show SoCon
Pretty SoCon
NFData SoCon

data KiCon Source

Kind constructor.

Constructors

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.

Instances

Eq KiCon
Show KiCon
Pretty KiCon
NFData KiCon

data TwCon Source

Witness type constructors.

Constructors

TwConImpl
TwConPure	Purity of some effect.
TwConEmpty	Emptiness of some closure.
TwConGlobal	Globalness of some region.
TwConDeepGlobal	Globalness of material regions in some type.
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
TwConLazy	Laziness of some region.
TwConHeadLazy	Laziness of the primary region in some type.
TwConManifest	Manifestness of some region (not lazy).
TwConDisjoint	Non-interfering effects are disjoint. Used for rewrite rules.

Instances

Eq TwCon
Show TwCon
Pretty TwCon
NFData TwCon

data TcCon Source

Other constructors at the spec level.

Constructors

TcConUnit	The unit data type constructor is baked in.
TcConFun	Pure function.
TcConFunEC	Function with a latent effect and closure.
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.
TcConUse	Region is captured in a closure.
TcConDeepUse	All material regions in a data type are captured in a closure.

Instances

Eq TcCon
Show TcCon
Pretty TcCon
NFData TcCon

data Binder n Source

A variable binder.

Constructors

RNone
RAnon
RName !n

Instances

Show n => Show (Binder n)
Pretty n => Pretty (Binder n)
NFData n => NFData (Binder n)

data Bind n Source

A variable binder with its type.

Constructors

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.

Instances

Rename Bind
SpreadT Bind
SpreadX Bind
SubstituteT Bind
SupportX Bind
SubstituteTX Bind
Ord n => MapBoundT Bind n
Eq n => Eq (Bind n)
Show n => Show (Bind n)
(Pretty n, Eq n) => Pretty (Bind n)
NFData n => NFData (Bind n)

data Bound n Source

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).

Constructors

UIx !Int	Nameless variable that should be on the deBruijn stack.
UName !n	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.

Instances

SpreadT Bound
SpreadX Bound
MapBoundX Bound n
MapBoundT Bound n
Eq n => Eq (Bound n)
Ord n => Ord (Bound n)
Show n => Show (Bound n)
(Pretty n, Eq n) => Pretty (Bound n)
NFData n => NFData (Bound n)