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

Sort construction

sComp :: Type n

Sort of kinds of computational types.

sProp :: Type n

Sort of kinds of propositional types.

Kind construction

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.

Effect type constructors

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 type constructors

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.

Type constructor wrappers.

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.