Safe Haskell	Safe
Language	Haskell98

DDC.Type.Exp.Simple.Exp

Synopsis

Documentation

data Binder n Source #

Constructors

RNone
RAnon
RName !n

Instances

Show n => Show (Binder n) Source #
Methods showsPrec :: Int -> Binder n -> ShowS # show :: Binder n -> String # showList :: [Binder n] -> ShowS #

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

SpreadT Bind Source #
Methods spreadT :: Ord n => TypeEnv n -> Bind n -> Bind n Source #
Rename Bind Source #
Methods renameWith :: Ord n => Sub n -> Bind n -> Bind n Source #
SpreadX Bind Source #
Methods spreadX :: Ord n => Env n -> Env n -> Bind n -> Bind n Source #
SupportX Bind Source #
Methods support :: Ord n => KindEnv n -> TypeEnv n -> Bind n -> Support n Source #
SubstituteT Bind Source #
Methods substituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> Bind n -> Bind n Source #
SubstituteTX Bind Source #
Methods substituteWithTX :: Ord n => Type n -> Sub n -> Bind n -> Bind n Source #
Ord n => MapBoundT Bind n Source #
Methods mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Bind n -> Bind n Source #
Show n => Show (Bind n) Source #
Methods showsPrec :: Int -> Bind n -> ShowS # show :: Bind n -> String # showList :: [Bind n] -> ShowS #

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 Source #
Methods spreadT :: Ord n => TypeEnv n -> Bound n -> Bound n Source #
SpreadX Bound Source #
Methods spreadX :: Ord n => Env n -> Env n -> Bound n -> Bound n Source #
MapBoundT Bound n Source #
Methods mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Bound n -> Bound n Source #
MapBoundX Bound n Source #
Methods mapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Bound n -> Bound n Source #
Show n => Show (Bound n) Source #
Methods showsPrec :: Int -> Bound n -> ShowS # show :: Bound n -> String # showList :: [Bound n] -> ShowS #

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

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

Instances

SpreadT Type Source #
Methods spreadT :: Ord n => TypeEnv n -> Type n -> Type n Source #
Rename Type Source #
Methods renameWith :: Ord n => Sub n -> Type n -> Type n Source #
FreeVarConT Type Source #
Methods freeVarConT :: Ord n => KindEnv n -> Type n -> (Set (Bound n), Set (Bound n)) Source #
SupportX Type Source #
Methods support :: Ord n => KindEnv n -> TypeEnv n -> Type n -> Support n Source #
SubstituteT Type Source #
Methods substituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> Type n -> Type n Source #
SubstituteTX Type Source #
Methods substituteWithTX :: Ord n => Type n -> Sub n -> Type n -> Type n Source #
Ord n => MapBoundT Type n Source #
Methods mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Type n -> Type n Source #
Show n => Show (Type n) Source #
Methods showsPrec :: Int -> Type n -> ShowS # show :: Type n -> String # showList :: [Type n] -> ShowS #

type Sort n = Type n Source #

Sorts are types at level 3.

type Kind n = Type n Source #

Kinds are types at level 2

type Region n = Type n Source #

Alias for region types.

type Effect n = Type n Source #

Alias for effect types.

type Closure n = Type n Source #

Alias for closure types.

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

SpreadT TypeSum Source #
Methods spreadT :: Ord n => TypeEnv n -> TypeSum n -> TypeSum n Source #
Rename TypeSum Source #
Methods renameWith :: Ord n => Sub n -> TypeSum n -> TypeSum n Source #
SubstituteT TypeSum Source #
Methods substituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> TypeSum n -> TypeSum n Source #
Ord n => MapBoundT TypeSum n Source #
Methods mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> TypeSum n -> TypeSum n Source #
Show n => Show (TypeSum n) Source #
Methods showsPrec :: Int -> TypeSum n -> ShowS # show :: TypeSum n -> String # showList :: [TypeSum n] -> ShowS #

data TyConHash Source #

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

Constructors

TyConHash !Int

Instances

Eq TyConHash Source #
Methods (==) :: TyConHash -> TyConHash -> Bool # (/=) :: TyConHash -> TyConHash -> Bool #
Ord TyConHash Source #
Methods compare :: TyConHash -> TyConHash -> Ordering # (<) :: TyConHash -> TyConHash -> Bool # (<=) :: TyConHash -> TyConHash -> Bool # (>) :: TyConHash -> TyConHash -> Bool # (>=) :: TyConHash -> TyConHash -> Bool # max :: TyConHash -> TyConHash -> TyConHash # min :: TyConHash -> TyConHash -> TyConHash #
Show TyConHash Source #
Methods showsPrec :: Int -> TyConHash -> ShowS # show :: TyConHash -> String # showList :: [TyConHash] -> ShowS #
Ix TyConHash Source #
Methods range :: (TyConHash, TyConHash) -> [TyConHash] # index :: (TyConHash, TyConHash) -> TyConHash -> Int # unsafeIndex :: (TyConHash, TyConHash) -> TyConHash -> Int inRange :: (TyConHash, TyConHash) -> TyConHash -> Bool # rangeSize :: (TyConHash, TyConHash) -> Int # unsafeRangeSize :: (TyConHash, 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) !(Kind n)

Instances

Show n => Show (TypeSumVarCon n) Source #
Methods showsPrec :: Int -> TypeSumVarCon n -> ShowS # show :: TypeSumVarCon n -> String # showList :: [TypeSumVarCon n] -> ShowS #

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 Source #
Methods spreadT :: Ord n => TypeEnv n -> TyCon n -> TyCon n Source #
Show n => Show (TyCon n) Source #
Methods showsPrec :: Int -> TyCon n -> ShowS # show :: TyCon n -> String # showList :: [TyCon n] -> ShowS #

data SoCon Source #

Sort constructor.

Constructors

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

Instances

Eq SoCon Source #
Methods (==) :: SoCon -> SoCon -> Bool # (/=) :: SoCon -> SoCon -> Bool #
Ord SoCon Source #
Methods compare :: SoCon -> SoCon -> Ordering # (<) :: SoCon -> SoCon -> Bool # (<=) :: SoCon -> SoCon -> Bool # (>) :: SoCon -> SoCon -> Bool # (>=) :: SoCon -> SoCon -> Bool # max :: SoCon -> SoCon -> SoCon # min :: SoCon -> SoCon -> SoCon #
Show SoCon Source #
Methods showsPrec :: Int -> SoCon -> ShowS # show :: SoCon -> String # showList :: [SoCon] -> ShowS #

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 Source #
Methods (==) :: KiCon -> KiCon -> Bool # (/=) :: KiCon -> KiCon -> Bool #
Ord KiCon Source #
Methods compare :: KiCon -> KiCon -> Ordering # (<) :: KiCon -> KiCon -> Bool # (<=) :: KiCon -> KiCon -> Bool # (>) :: KiCon -> KiCon -> Bool # (>=) :: KiCon -> KiCon -> Bool # max :: KiCon -> KiCon -> KiCon # min :: KiCon -> KiCon -> KiCon #
Show KiCon Source #
Methods showsPrec :: Int -> KiCon -> ShowS # show :: KiCon -> String # showList :: [KiCon] -> ShowS #

data TwCon Source #

Witness type constructors.

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.

Instances

Eq TwCon Source #
Methods (==) :: TwCon -> TwCon -> Bool # (/=) :: TwCon -> TwCon -> Bool #
Ord TwCon Source #
Methods compare :: TwCon -> TwCon -> Ordering # (<) :: TwCon -> TwCon -> Bool # (<=) :: TwCon -> TwCon -> Bool # (>) :: TwCon -> TwCon -> Bool # (>=) :: TwCon -> TwCon -> Bool # max :: TwCon -> TwCon -> TwCon # min :: TwCon -> TwCon -> TwCon #
Show TwCon Source #
Methods showsPrec :: Int -> TwCon -> ShowS # show :: TwCon -> String # showList :: [TwCon] -> ShowS #

data TcCon Source #

Other constructors at the spec level.

Constructors

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.

Instances

Eq TcCon Source #
Methods (==) :: TcCon -> TcCon -> Bool # (/=) :: TcCon -> TcCon -> Bool #
Ord TcCon Source #
Methods compare :: TcCon -> TcCon -> Ordering # (<) :: TcCon -> TcCon -> Bool # (<=) :: TcCon -> TcCon -> Bool # (>) :: TcCon -> TcCon -> Bool # (>=) :: TcCon -> TcCon -> Bool # max :: TcCon -> TcCon -> TcCon # min :: TcCon -> TcCon -> TcCon #
Show TcCon Source #
Methods showsPrec :: Int -> TcCon -> ShowS # show :: TcCon -> String # showList :: [TcCon] -> ShowS #