ddc-core-0.4.1.1: Disciplined Disciple Compiler core language and type checker.

Safe HaskellSafe-Inferred

DDC.Type.Exp

Contents

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

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

Instances

data TyConHash Source

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

Constructors

TyConHash !Int 

Instances

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

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

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.

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

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

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

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)