Safe Haskell | Safe |
---|---|
Language | Haskell98 |
- takeNameOfBind :: Bind n -> Maybe n
- typeOfBind :: Bind n -> Type n
- replaceTypeOfBind :: Type n -> Bind n -> Bind n
- binderOfBind :: Bind n -> Binder n
- makeBindFromBinder :: Binder n -> Type n -> Bind n
- partitionBindsByType :: Eq n => [Bind n] -> [([Binder n], Type n)]
- takeNameOfBound :: Bound n -> Maybe n
- takeTypeOfBound :: Bound n -> Maybe (Type n)
- boundMatchesBind :: Eq n => Bound n -> Bind n -> Bool
- namedBoundMatchesBind :: Eq n => Bound n -> Bind n -> Bool
- takeSubstBoundOfBind :: Bind n -> Maybe (Bound n)
- takeSubstBoundsOfBinds :: [Bind n] -> [Bound n]
- replaceTypeOfBound :: Type n -> Bound n -> Bound n
- kFun :: Kind n -> Kind n -> Kind n
- kFuns :: [Kind n] -> Kind n -> Kind n
- takeKFun :: Kind n -> Maybe (Kind n, Kind n)
- takeKFuns :: Kind n -> ([Kind n], Kind n)
- takeKFuns' :: Kind n -> [Kind n]
- takeResultKind :: Kind n -> Kind n
- tForall :: Kind n -> (Type n -> Type n) -> Type n
- tForall' :: Int -> Kind n -> (Type n -> Type n) -> Type n
- tForalls :: [Kind n] -> ([Type n] -> Type n) -> Type n
- tForalls' :: Int -> [Kind n] -> ([Type n] -> Type n) -> Type n
- takeTForalls :: Type n -> Maybe ([Bind n], Type n)
- eraseTForalls :: Ord n => Type n -> Type n
- tBot :: Kind n -> Type n
- tSum :: Ord n => Kind n -> [Type n] -> Type n
- tApp :: Type n -> Type n -> Type n
- ($:) :: Type n -> Type n -> Type n
- tApps :: Type n -> [Type n] -> Type n
- takeTApps :: Type n -> [Type n]
- takeTyConApps :: Type n -> Maybe (TyCon n, [Type n])
- takePrimTyConApps :: Type n -> Maybe (n, [Type n])
- takeDataTyConApps :: Type n -> Maybe (TyCon n, [Type n])
- takePrimeRegion :: Type n -> Maybe (Type n)
- tFun :: Type n -> Type n -> Type n
- tFunOfList :: [Type n] -> Maybe (Type n)
- tFunOfParamResult :: [Type n] -> Type n -> Type n
- takeTFun :: Type n -> Maybe (Type n, Type n)
- takeTFunArgResult :: Type n -> ([Type n], Type n)
- takeTFunWitArgResult :: Type n -> ([Type n], [Type n], Type n)
- takeTFunAllArgResult :: Type n -> ([Type n], Type n)
- arityOfType :: Type n -> Int
- dataArityOfType :: Type n -> Int
- tSusp :: Effect n -> Type n -> Type n
- takeTSusp :: Type n -> Maybe (Effect n, Type n)
- takeTSusps :: Type n -> ([Effect n], Type n)
- tImpl :: Type n -> Type n -> Type n
- tUnit :: Type n
- tIx :: Kind n -> Int -> Type n
- takeTExists :: Type n -> Maybe Int
- sComp :: Type n
- sProp :: Type n
- kData :: Type n
- kRegion :: Type n
- kEffect :: Type n
- kClosure :: Type n
- kWitness :: Type n
- 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
- tPure :: 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
- tConData0 :: n -> Kind n -> Type n
- tConData1 :: n -> Kind n -> Type n -> Type n
Binds
takeNameOfBind :: Bind n -> Maybe n Source #
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 Source #
Take the type of a bind.
Binders
binderOfBind :: Bind n -> Binder n Source #
Take the binder of a bind.
partitionBindsByType :: Eq n => [Bind n] -> [([Binder n], Type n)] Source #
Make lists of binds that have the same type.
Bounds
takeNameOfBound :: Bound n -> Maybe n Source #
Take the name of bound variable. If this is a deBruijn index then there won't be a name.
namedBoundMatchesBind :: Eq n => Bound n -> Bind n -> Bool Source #
Check whether a named bound matches a named bind.
Yields False
if they are not named or have different names.
Kinds
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 n Source #
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 Source #
Build an anonymous type abstraction, with a single parameter.
tForall' :: Int -> Kind n -> (Type n -> Type n) -> Type n Source #
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 Source #
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 Source #
Build an anonymous type abstraction, with several parameters. Starting the next index from the given value.
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.
Sums
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.
takePrimTyConApps :: Type n -> Maybe (n, [Type n]) Source #
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]) Source #
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) Source #
Take the prime region variable of a data type. This corresponds to the region the outermost constructor is allocated into.
Functions
tFunOfList :: [Type n] -> Maybe (Type n) Source #
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 Source #
Construct a function type from a list of parameter types and the return type.
takeTFun :: Type n -> Maybe (Type n, Type n) Source #
Yield the argument and result type of a function type.
takeTFunArgResult :: Type n -> ([Type n], Type n) Source #
Destruct the type of a function, returning just the argument and result types.
takeTFunWitArgResult :: Type n -> ([Type n], [Type n], Type n) Source #
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) Source #
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 Source #
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 Source #
The data arity of a type is the number of data values it takes.
Unlike arityOfType
we ignore type and witness parameters.
Suspensions
takeTSusp :: Type n -> Maybe (Effect n, Type n) Source #
Take the effect and result type of a suspension type.
Implications
Units
Variables
Sort construction
Kind construction
Effect type constructors
tDeepWrite :: Type n -> Type n Source #
Deep Write effect type constructor.
tDeepAlloc :: Type n -> Type n Source #
Deep Alloc effect type constructor.
Witness type constructors
tDeepConst :: Type n -> Type n Source #
Deep Const witness type constructor.
tDeepMutable :: Type n -> Type n Source #
Deep Mutable witness type constructor.