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

typeOfBound :: Bound n -> Type n

Take the type of a bound variable.

takeNameOfBound :: Bound n -> Maybe n

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

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

Replace the type of a bound with a new one.

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 Bound to a Bind, ready for substitution.

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

Type structure

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

Construct a deBruijn index.

tApp, ($:) :: 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.

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.

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

Build an anonymous type abstraction, with a single parameter.

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

Build an anonymous type abstraction, with several parameters.

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.

tBot :: Kind n -> Type n

Construct an empty type sum.

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

Function type construction

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.

tFun :: 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, Effect n, Closure n, Type n)

Destruct the type of a value function.

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

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

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

Construct a pure and empty value type function.

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

Construct a witness implication 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

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.