ddc-core-0.2.1.2: Disciple Core language and type checker.

Safe HaskellSafe-Inferred

DDC.Type.Compounds

Contents

Synopsis

Binds

takeNameOfBind :: Bind n -> Maybe nSource

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

typeOfBind :: Bind n -> Type nSource

Take the type of a bind.

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

Replace the type of a bind with a new one.

Binders

binderOfBind :: Bind n -> Binder nSource

Take the binder of a bind.

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

Make a bind from a binder and its type.

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

Make lists of binds that have the same type.

Bounds

typeOfBound :: Bound n -> Type nSource

Take the type of a bound variable.

takeNameOfBound :: Bound n -> Maybe nSource

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 nSource

Replace the type of a bound with a new one.

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

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 -> BoolSource

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)Source

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 nSource

Construct a deBruijn index.

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

Construct a type application.

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

Construct a type application.

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

Construct a sequence of type applications.

takeTApps :: Type n -> [Type n]Source

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

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

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

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

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 nSource

Build an anonymous type abstraction, with a single parameter.

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

Build an anonymous type abstraction, with several parameters.

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

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

tBot :: Kind n -> Type nSource

Construct an empty type sum.

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

Function type construction

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

Construct a kind function.

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

Construct some kind functions.

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

Destruct a kind function

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

Destruct a chain of kind functions into the arguments

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

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

takeResultKind :: Kind n -> Kind nSource

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 nSource

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

takeTFun :: Type n -> Maybe (Type n, Effect n, Closure n, Type n)Source

Destruct the type of a value function.

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

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

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

Construct a pure and empty value type function.

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

Construct a witness implication type.

Sort construction

Kind construction

Effect type constructors

Closure type constructors.

tUse :: Type n -> Type nSource

Witness type constructors.

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

Build a nullary type constructor of the given kind.

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

Build a type constructor application of one argumnet.