DDC.Type.Exp.Simple

Abstract Syntax

Types

data Type n

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

Methods

spreadT :: Ord n => TypeEnv n -> Type n -> Type n

Rename Type

Methods

renameWith :: Ord n => Sub n -> Type n -> Type n

FreeVarConT Type

Methods

freeVarConT :: Ord n => KindEnv n -> Type n -> (Set (Bound n), Set (Bound n))

SupportX Type

Methods

support :: Ord n => KindEnv n -> TypeEnv n -> Type n -> Support n

SubstituteT Type

Methods

substituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> Type n -> Type n

SubstituteTX Type

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Type n -> Type n

Ord n => MapBoundT Type n

Methods

mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Type n -> Type n

Show n => Show (Type n)

Methods

showsPrec :: Int -> Type n -> ShowS

show :: Type n -> String

showList :: [Type n] -> ShowS

data TypeSum n

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

SpreadT TypeSum

Methods

spreadT :: Ord n => TypeEnv n -> TypeSum n -> TypeSum n

Rename TypeSum

Methods

renameWith :: Ord n => Sub n -> TypeSum n -> TypeSum n

SubstituteT TypeSum

Methods

substituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> TypeSum n -> TypeSum n

Ord n => MapBoundT TypeSum n

Methods

mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> TypeSum n -> TypeSum n

Show n => Show (TypeSum n)

Methods

showsPrec :: Int -> TypeSum n -> ShowS

show :: TypeSum n -> String

showList :: [TypeSum n] -> ShowS

data TyConHash

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

Constructors

TyConHash !Int

Instances

Eq TyConHash

Methods

(==) :: TyConHash -> TyConHash -> Bool

(/=) :: TyConHash -> TyConHash -> Bool

Ord TyConHash

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

Methods

showsPrec :: Int -> TyConHash -> ShowS

show :: TyConHash -> String

showList :: [TyConHash] -> ShowS

Ix TyConHash

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

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)

Methods

showsPrec :: Int -> TypeSumVarCon n -> ShowS

show :: TypeSumVarCon n -> String

showList :: [TypeSumVarCon n] -> ShowS

Binding

data Binder n

Constructors

RNone

RAnon

RName !n

Instances

Show n => Show (Binder n)

Methods

showsPrec :: Int -> Binder n -> ShowS

show :: Binder n -> String

showList :: [Binder n] -> ShowS

data Bind n

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

Methods

spreadT :: Ord n => TypeEnv n -> Bind n -> Bind n

Rename Bind

Methods

renameWith :: Ord n => Sub n -> Bind n -> Bind n

SpreadX Bind

Methods

spreadX :: Ord n => Env n -> Env n -> Bind n -> Bind n

SupportX Bind

Methods

support :: Ord n => KindEnv n -> TypeEnv n -> Bind n -> Support n

SubstituteT Bind

Methods

substituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> Bind n -> Bind n

SubstituteTX Bind

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Bind n -> Bind n

Ord n => MapBoundT Bind n

Methods

mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Bind n -> Bind n

Show n => Show (Bind n)

Methods

showsPrec :: Int -> Bind n -> ShowS

show :: Bind n -> String

showList :: [Bind n] -> ShowS

data Bound n

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

Methods

spreadT :: Ord n => TypeEnv n -> Bound n -> Bound n

SpreadX Bound

Methods

spreadX :: Ord n => Env n -> Env n -> Bound n -> Bound n

MapBoundT Bound n

Methods

mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Bound n -> Bound n

MapBoundX Bound n

Methods

mapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Bound n -> Bound n

Show n => Show (Bound n)

Methods

showsPrec :: Int -> Bound n -> ShowS

show :: Bound n -> String

showList :: [Bound n] -> ShowS

Constructors

data TyCon n

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

Methods

spreadT :: Ord n => TypeEnv n -> TyCon n -> TyCon n

Show n => Show (TyCon n)

Methods

showsPrec :: Int -> TyCon n -> ShowS

show :: TyCon n -> String

showList :: [TyCon n] -> ShowS

data SoCon

Sort constructor.

Constructors

SoConProp

Sort of witness kinds.

SoConComp

Sort of computation kinds.

Instances

Eq SoCon

Methods

(==) :: SoCon -> SoCon -> Bool

(/=) :: SoCon -> SoCon -> Bool

Ord SoCon

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

Methods

showsPrec :: Int -> SoCon -> ShowS

show :: SoCon -> String

showList :: [SoCon] -> ShowS

data KiCon

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

Methods

(==) :: KiCon -> KiCon -> Bool

(/=) :: KiCon -> KiCon -> Bool

Ord KiCon

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

Methods

showsPrec :: Int -> KiCon -> ShowS

show :: KiCon -> String

showList :: [KiCon] -> ShowS

data TwCon

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

Methods

(==) :: TwCon -> TwCon -> Bool

(/=) :: TwCon -> TwCon -> Bool

Ord TwCon

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

Methods

showsPrec :: Int -> TwCon -> ShowS

show :: TwCon -> String

showList :: [TwCon] -> ShowS

data TcCon

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

Methods

(==) :: TcCon -> TcCon -> Bool

(/=) :: TcCon -> TcCon -> Bool

Ord TcCon

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

Methods

showsPrec :: Int -> TcCon -> ShowS

show :: TcCon -> String

showList :: [TcCon] -> ShowS

Aliases

type Sort n = Type n

Sorts are types at level 3.

type Kind n = Type n

Kinds are types at level 2

type Region n = Type n

Alias for region types.

type Effect n = Type n

Alias for effect types.

type Closure n = Type n

Alias for closure types.

Predicates

Binders

isBNone :: Bind n -> Bool

isBAnon :: Bind n -> Bool

isBName :: Bind n -> Bool

Atoms

isTVar :: Type n -> Bool

Check whether a type is a TVar

isBot :: Type n -> Bool

Test if some type is an empty TSum

isAtomT :: Type n -> Bool

Check whether a type is a TVar, TCon or is Bottom.

isTExists :: Type n -> Bool

Check whether this type is an existential variable.

Kinds

isDataKind :: Kind n -> Bool

Check if some kind is the data kind.

isRegionKind :: Region n -> Bool

Check if some kind is the region kind.

isEffectKind :: Kind n -> Bool

Check if some kind is the effect kind.

isClosureKind :: Kind n -> Bool

Check if some kind is the closure kind.

isWitnessKind :: Kind n -> Bool

Check if some kind is the witness kind.

Data Types

isAlgDataType :: Eq n => Type n -> Bool

Check whether this type is that of algebraic data.

It needs to have an explicit data constructor out the front, and not a type variable. The constructor must not be the function constructor, and must return a value of kind *.

isWitnessType :: Eq n => Type n -> Bool

Check whether type is a witness constructor

isConstWitType :: Eq n => Type n -> Bool

Check whether this is the type of a Const witness.

isMutableWitType :: Eq n => Type n -> Bool

Check whether this is the type of a Mutable witness.

isDistinctWitType :: Eq n => Type n -> Bool

Check whether this is the type of a Distinct witness.

Effect Types

isReadEffect :: Effect n -> Bool

Check whether this is an atomic read effect.

isWriteEffect :: Effect n -> Bool

Check whether this is an atomic write effect.

isAllocEffect :: Effect n -> Bool

Check whether this is an atomic alloc effect.

isSomeReadEffect :: Effect n -> Bool

Check whether an effect is some sort of read effect. Matches Read HeadRead and DeepRead.

isSomeWriteEffect :: Effect n -> Bool

Check whether an effect is some sort of allocation effect. Matches Alloc and DeepAlloc

isSomeAllocEffect :: Effect n -> Bool

Check whether an effect is some sort of allocation effect. Matches Alloc and DeepAlloc

Relations

Equivalence

equivT :: Ord n => EnvT n -> Type n -> Type n -> Bool

Check equivalence of types.

Checks equivalence up to alpha-renaming, as well as crushing of effects and trimming of closures.

• Return False if we find any free variables.
• We assume the types are well-kinded, so that the type annotations on bound variables match the binders. If this is not the case then you get an indeterminate result.

equivWithBindsT

Arguments

:: Ord n

=> EnvT n

Environment of types.

-> [Bind n]

Stack of binders for first type.

-> [Bind n]

Stack of binders for second type.

-> Type n

First type to compare.

-> Type n

Second type to compare.

-> Bool

Like equivT but take the initial stacks of type binders.

equivTyCon :: Eq n => TyCon n -> TyCon n -> Bool

Check if two TyCons are equivalent. We need to handle TyConBound specially incase it's kind isn't attached,

Subsumption

subsumesT :: Ord n => EnvT n -> Kind n -> Type n -> Type n -> Bool

Check whether the first type subsumes the second.

Both arguments are converted to sums, and we check that every element of the second sum is equivalent to an element in the first.

This only works for well formed types of effect and closure kind. Other types will yield False.

Transforms

Crushing

crushSomeT :: Ord n => EnvT n -> Type n -> Type n

Crush compound effects and closure terms. We check for a crushable term before calling crushT because that function will recursively crush the components. As equivT is already recursive, we don't want a doubly-recursive function that tries to re-crush the same non-crushable type over and over.

crushEffect :: Ord n => EnvT n -> Effect n -> Effect n

Crush compound effect terms into their components.

For example, crushing DeepRead (List r1 (Int r2)) yields (Read r1 + Read r2).

Compounds

Binds

takeNameOfBind :: Bind n -> Maybe n

Take the variable name of a bind. If this is an anonymous binder then there won't be a name.

typeOfBind :: Bind n -> Type n

Take the type of a bind.

replaceTypeOfBind :: Type n -> Bind n -> Bind n

Replace the type of a bind with a new one.

Binders

binderOfBind :: Bind n -> Binder n

Take the binder of a bind.

makeBindFromBinder :: Binder n -> Type n -> Bind n

Make a bind from a binder and its type.

partitionBindsByType :: Eq n => [Bind n] -> [([Binder n], Type n)]

Make lists of binds that have the same type.

Bounds

takeNameOfBound :: Bound n -> Maybe n

Take the name of bound variable. If this is a deBruijn index then there won't be a name.

takeTypeOfBound :: Bound n -> Maybe (Type n)

Get the attached type of a Bound, if any.

boundMatchesBind :: Eq n => Bound n -> Bind n -> Bool

Check whether a bound maches a bind. UName and BName match if they have the same name. UIx 0 _ and BAnon _ always match. Yields False for other combinations of bounds and binds.

namedBoundMatchesBind :: Eq n => Bound n -> Bind n -> Bool

Check whether a named bound matches a named bind. Yields False if they are not named or have different names.

takeSubstBoundOfBind :: Bind n -> Maybe (Bound n)

Convert a Bind to a Bound, ready for substitution.

Returns UName for BName, UIx 0 for BAnon and Nothing for BNone, because there's nothing to substitute.

takeSubstBoundsOfBinds :: [Bind n] -> [Bound n]

Convert some Binds to Bounds

replaceTypeOfBound :: Type n -> Bound n -> Bound n

If this Bound is a UPrim then replace it's embedded type with a new one, otherwise return it unharmed.

Sorts

sComp :: Type n

Sort of kinds of computational types.

sProp :: Type n

Sort of kinds of propositional types.

Kinds

kData :: Type n

Kind of data types.

kRegion :: Type n

Kind of region types.

kEffect :: Type n

Kind of effect types.

kClosure :: Type n

Kind of closure types.

kWitness :: Type n

Kind of witness types.

kFun :: Kind n -> Kind n -> Kind n infixr 9

Construct a kind function.

kFuns :: [Kind n] -> Kind n -> Kind n

Construct some kind functions.

takeKFun :: Kind n -> Maybe (Kind n, Kind n)

Destruct a kind function

takeKFuns :: Kind n -> ([Kind n], Kind n)

Destruct a chain of kind functions into the arguments

takeKFuns' :: Kind n -> [Kind n]

Like takeKFuns, but return argument and return kinds in the same list.

takeResultKind :: Kind n -> Kind n

Take the result kind of a kind function, or return the same kind unharmed if it's not a kind function.

Quantifiers

tForall :: Kind n -> (Type n -> Type n) -> Type n

Build an anonymous type abstraction, with a single parameter.

tForall' :: Int -> Kind n -> (Type n -> Type n) -> Type n

Build an anonymous type abstraction, with a single parameter. Starting the next index from the given value.

tForalls :: [Kind n] -> ([Type n] -> Type n) -> Type n

Build an anonymous type abstraction, with several parameters. Starting the next index from the given value.

tForalls' :: Int -> [Kind n] -> ([Type n] -> Type n) -> Type n

Build an anonymous type abstraction, with several parameters. Starting the next index from the given value.

takeTForalls :: Type n -> Maybe ([Bind n], Type n)

Split nested foralls from the front of a type, or Nothing if there was no outer forall.

eraseTForalls :: Ord n => Type n -> Type n

Erase all TForall quantifiers from a type.

Sums

tBot :: Kind n -> Type n

Construct an empty type sum.

tSum :: Ord n => Kind n -> [Type n] -> Type n

Applications

tApp :: Type n -> Type n -> Type n

Construct a type application.

($:) :: Type n -> Type n -> Type n

Construct a type application.

tApps :: Type n -> [Type n] -> Type n

Construct a sequence of type applications.

takeTApps :: Type n -> [Type n]

Flatten a sequence ot type applications into the function part and arguments, if any.

takeTyConApps :: Type n -> Maybe (TyCon n, [Type n])

Flatten a sequence of type applications, returning the type constructor and arguments, if there is one.

takePrimTyConApps :: Type n -> Maybe (n, [Type n])

Flatten a sequence of type applications, returning the type constructor and arguments, if there is one. Only accept primitive type constructors.

takeDataTyConApps :: Type n -> Maybe (TyCon n, [Type n])

Flatten a sequence of type applications, returning the type constructor and arguments, if there is one. Only accept data type constructors.

takePrimeRegion :: Type n -> Maybe (Type n)

Take the prime region variable of a data type. This corresponds to the region the outermost constructor is allocated into.

Functions

tFun :: Type n -> Type n -> Type n infixr 9

Construct a pure function type.

tFunOfList :: [Type n] -> Maybe (Type n)

Construct a function type from a list containing the parameter and return types. Yields Nothing if the list is empty.

tFunOfParamResult :: [Type n] -> Type n -> Type n

Construct a function type from a list of parameter types and the return type.

takeTFun :: Type n -> Maybe (Type n, Type n)

Yield the argument and result type of a function type.

takeTFunArgResult :: Type n -> ([Type n], Type n)

Destruct the type of a function, returning just the argument and result types.

takeTFunWitArgResult :: Type n -> ([Type n], [Type n], Type n)

Destruct the type of a function, returning the witness argument, value argument and result types. The function type must have the witness implications before the value arguments, eg T1 => T2 -> T3 -> T4 -> T5.

takeTFunAllArgResult :: Type n -> ([Type n], Type n)

Destruct the type of a possibly polymorphic function returning all kinds of quantifiers, witness arguments, and value arguments in the order they appear, along with the type of the result.

arityOfType :: Type n -> Int

Determine the arity of an expression by looking at its type. Count all the function arrows, and foralls.

This assumes the type is in prenex form, meaning that all the quantifiers are at the front.

dataArityOfType :: Type n -> Int

The data arity of a type is the number of data values it takes. Unlike arityOfType we ignore type and witness parameters.

Suspensions

tSusp :: Effect n -> Type n -> Type n

Construct a suspension type.

takeTSusp :: Type n -> Maybe (Effect n, Type n)

Take the effect and result type of a suspension type.

takeTSusps :: Type n -> ([Effect n], Type n)

Split off enclosing suspension types.

Implications

tImpl :: Type n -> Type n -> Type n infixr 9

Construct a witness implication type.

Units

tUnit :: Type n

The unit type.

Variables

tIx :: Kind n -> Int -> Type n

Construct a deBruijn index.

takeTExists :: Type n -> Maybe Int

Take an existential variable from a type.

Effect types

tRead :: Type n -> Type n

Read effect type constructor.

tDeepRead :: Type n -> Type n

Deep Read effect type constructor.

tHeadRead :: Type n -> Type n

Head Read effect type constructor.

tWrite :: Type n -> Type n

Write effect type constructor.

tDeepWrite :: Type n -> Type n

Deep Write effect type constructor.

tAlloc :: Type n -> Type n

Alloc effect type constructor.

tDeepAlloc :: Type n -> Type n

Deep Alloc effect type constructor.

Witness types

tPure :: Type n -> Type n

Pure witness type constructor.

tConst :: Type n -> Type n

Const witness type constructor.

tDeepConst :: Type n -> Type n

Deep Const witness type constructor.

tMutable :: Type n -> Type n

Mutable witness type constructor.

tDeepMutable :: Type n -> Type n

Deep Mutable witness type constructor.

tDistinct :: Int -> [Type n] -> Type n

Distinct witness type constructor.

tConData0 :: n -> Kind n -> Type n

Build a nullary type constructor of the given kind.

tConData1 :: n -> Kind n -> Type n -> Type n

Build a type constructor application of one argumnet.