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.
replaceTypeOfBind :: Type n -> Bind n -> Bind n Source
Replace the type of a bind with a new one.
Binders
binderOfBind :: Bind n -> Binder n Source
Take the binder of a bind.
makeBindFromBinder :: Binder n -> Type n -> Bind n Source
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
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.
takeSubstBoundOfBind :: Bind n -> Maybe (Bound n) Source
takeSubstBoundsOfBinds :: [Bind n] -> [Bound n] Source
Convert some Bind
s to Bounds
replaceTypeOfBound :: Type n -> Bound n -> Bound n Source
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.
takeTSusps :: Type n -> ([Effect n], Type n) Source
Split off enclosing suspension types.
Implications
Units
Variables
takeTExists :: Type n -> Maybe Int Source
Take an existential variable from a type.
Sort construction
Kind construction
Effect type constructors
tDeepWrite :: Type n -> Type n Source
tDeepAlloc :: Type n -> Type n Source
Witness type constructors
tDeepConst :: Type n -> Type n Source
tDeepMutable :: Type n -> Type n Source