ddc-core-0.2.0.2: Disciple Core language and type checker.

Safe HaskellSafe-Infered

DDC.Type.Exp

Contents

Synopsis

Types, Kinds, and Sorts

data Binder n Source

A variable binder.

Constructors

RNone 
RAnon 
RName n 

Instances

Show n => Show (Binder n) 
Pretty n => Pretty (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.

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 (Type n)

Nameless variable that should be on the deBruijn stack.

UName n (Type n)

Named variable that should be in the environment.

UPrim n (Type n)

Named primitive that is not bound in the environment. Prims aren't every counted as being free.

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

SpreadT Type 
LowerT Type 
LiftT Type 
BindStruct Type 
Rewrite Type 
SubstituteT Type 
SubstituteTX Type 
Eq n => Eq (Type n) 
Show n => Show (Type n) 
(Pretty n, Eq n) => Pretty (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

TypeSum 

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

data TyConHash Source

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

Constructors

TyConHash !Int 

data TypeSumVarCon n Source

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

Constructors

TypeSumVar (Bound n) 
TypeSumCon (Bound n) 

Instances

Eq n => Eq (TypeSumVarCon n) 
Ord n => Ord (TypeSumVarCon n) 
Show n => Show (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)

User defined and primitive constructors.

Instances

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

data SoCon Source

Sort constructor.

Constructors

SoConProp

Sort of witness kinds.

SoConComp

Sort of computation kinds.

Instances

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

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.

TwConLazy

Laziness of some region.

TwConHeadLazy

Laziness of the primary region in some type.

TwConManifest

Manifestness of some region (not lazy).

Instances

data TcCon Source

Other constructors at the spec level.

Constructors

TcConFun

The function type constructor is baked in so we represent it separately.

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