DDC.Type.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.

Kinds

kFun :: Kind n -> Kind n -> Kind n

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

Construct a pure function type.

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

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

tFunPE :: Type n -> Type n -> Type n

Construct a pure and empty value type function.

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

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

tFunEC :: Type n -> Effect n -> Closure n -> Type n -> Type n

Construct a value type function, with the provided effect and closure.

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

Yield the argument and result type of a function type.

Works for both TcConFun and TcConFunEC.

takeTFunEC :: Type n -> Maybe (Type n, Effect n, Closure 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.

Works for both TcConFun and TcConFunEC.

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.

Works for both TcConFun and TcConFunEC.

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.

Suspensions

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

Implications

tImpl :: Type n -> Type n -> Type n

Construct a witness implication type.

Units

tUnit :: Type n

Variables

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

Construct a deBruijn index.

takeTExists :: Type n -> Maybe Int

Take an existential variable from a type.

Sort construction

sComp :: Type n

sProp :: Type n

Kind construction

kData :: Type n

kRegion :: Type n

kEffect :: Type n

kClosure :: Type n

kWitness :: Type n

Effect type constructors

tRead :: Type n -> Type n

tDeepRead :: Type n -> Type n

tHeadRead :: Type n -> Type n

tWrite :: Type n -> Type n

tDeepWrite :: Type n -> Type n

tAlloc :: Type n -> Type n

tDeepAlloc :: Type n -> Type n

Closure type constructors

tUse :: Type n -> Type n

tDeepUse :: Type n -> Type n

Witness type constructors

tPure :: Type n -> Type n

tEmpty :: Type n -> Type n

tGlobal :: Type n -> Type n

tDeepGlobal :: Type n -> Type n

tConst :: Type n -> Type n

tDeepConst :: Type n -> Type n

tMutable :: Type n -> Type n

tDeepMutable :: Type n -> Type n

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

tLazy :: Type n -> Type n

tHeadLazy :: Type n -> Type n

tManifest :: Type n -> Type n

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.