Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data Type (src :: Type) (vs :: [Type]) (t :: kt) where
- pattern (:$) :: forall kt src (vs :: [Type]) (t :: kt). () => forall k (f :: k -> kt) (a :: k). (~#) kt kt t (f a) => Type (k -> kt) src vs f -> Type k src vs a -> Type kt src vs t
- pattern (:@) :: forall kt src (vs :: [Type]) (t :: kt). () => forall k (f :: k -> kt) (a :: k). (~#) kt kt t (f a) => Type (k -> kt) src vs f -> Type k src vs a -> Type kt src vs t
- tyConst :: forall kc (c :: kc) src vs. Source src => LenInj vs => Constable c => KindInjP (Ty_of_Type kc) => Type_of_Ty (Ty_of_Type kc) ~ kc => Type src vs c
- tyConstLen :: forall kc (c :: kc) src vs. Source src => Constable c => KindInjP (Ty_of_Type kc) => Type_of_Ty (Ty_of_Type kc) ~ kc => Len vs -> Type src vs c
- tyApp :: Source src => Type src vs f -> Type src vs a -> Type src vs (f a)
- tyVar :: Source src => NameVar -> Var src vs v -> Type src vs v
- tyFam :: forall kc (c :: kc) as vs src. Source src => LenInj vs => Constable c => KindInjP (Ty_of_Type kc) => Type_of_Ty (Ty_of_Type kc) ~ kc => Types src vs as -> Type src vs (Fam c as)
- tyQual :: Source src => Type src vs q -> Type src vs t -> (Qual q -> Type src vs t -> Type src vs (q #> t)) -> Type src vs (q #> t)
- data TypeK src vs kt = TypeK (Type src vs t)
- data TypeT src vs = TypeT (Type src vs t)
- data TypeVT src = TypeVT (Type src vs t)
- data Const src (c :: kc) where
- kindOfConst :: Const src (t :: kt) -> Kind src kt
- class (Typeable c, FixityOf c, NameTyOf c, ClassInstancesFor c, TypeInstancesFor c) => Constable c
- class ConstsOf a where
- data ConstC src = ConstC (Const src c)
- (~>) :: Source src => Constable (->) => Type src vs a -> Type src vs b -> Type src vs (a -> b)
- type family FunArg (fun :: Type) :: Type where ...
- type family FunRes (fun :: Type) :: Type where ...
- unTyFun :: forall t src tys. SourceInj (TypeVT src) src => Constable (->) => Type src tys t -> Maybe (Type src tys (FunArg t), Type src tys (FunRes t))
- newtype (q :: Constraint) #> (a :: Type) = Qual (q => a)
- (#>) :: Source src => Type src vs q -> Type src vs t -> Type src vs (q #> t)
- class (x, y) => x # y
- (#) :: Source src => Type src vs qx -> Type src vs qy -> Type src vs (qx # qy)
- noConstraint :: Source src => LenInj vs => Type src vs (() :: Constraint)
- noConstraintLen :: Source src => Len vs -> Type src vs (() :: Constraint)
- class x ~ y => x #~ y
- (#~) :: forall k a b src vs. Source src => Typeable k => KindInj k => Type src vs (a :: k) -> Type src vs (b :: k) -> Type src vs (a #~ b)
- eqType :: Source src => Type src tys (x :: k) -> Type src tys (y :: k) -> Maybe (x :~: y)
- eqTypeKi :: Source src => Type src tys (x :: kx) -> Type src tys (y :: ky) -> Maybe (x :~~: y)
- eqTypes :: Source src => Types src tys x -> Types src tys y -> Maybe (x :~~: y)
- ordType :: Source src => Type src tys (x :: kx) -> Type src tys (y :: ky) -> Ordering
- ordTypes :: Source src => Types src tys x -> Types src tys y -> Ordering
- data Qual q where
- class ClassInstancesFor c where
- proveConstraint :: Source src => Type src vs q -> Maybe (Qual q)
- constInj :: forall c src. Source src => Constable c => KindInjP (Ty_of_Type (K c)) => Type_of_Ty (Ty_of_Type (K c)) ~ K c => Const src c
- constKiInj :: forall kc c src. Source src => Constable c => Kind src kc -> Const src (c :: kc)
- proj_Const :: forall c u src. Typeable c => Const src u -> Maybe (c :~: u)
- proj_ConstTy :: forall c u src vs. Typeable c => Type src vs u -> Maybe (c :~: u)
- proj_ConstKi :: forall kc (c :: kc) u src. Typeable c => kc ~ Type_of_Ty (Ty_of_Type kc) => KindInjP (Ty_of_Type kc) => Const src u -> Maybe (c :~~: u)
- proj_ConstKiTy :: forall kc (c :: kc) u src vs. Typeable c => kc ~ Type_of_Ty (Ty_of_Type kc) => KindInjP (Ty_of_Type kc) => Type src vs u -> Maybe (c :~~: u)
- eqConst :: Const src_x (x :: k) -> Const src_y (y :: k) -> Maybe (x :~: y)
- eqConstKi :: forall src_x src_y kx ky x y. Const src_x (x :: kx) -> Const src_y (y :: ky) -> Maybe (x :~~: y)
- ordConst :: forall src_x src_y kx ky x y. Const src_x (x :: kx) -> Const src_y (y :: ky) -> Ordering
- normalizeQualsTy :: Source src => Type src tys (t :: kt) -> TypeK src tys kt
- type family Fam (fam :: k) (hs :: [Type]) :: k
- class TypeInstancesFor (c :: kc) where
- class ExpandFam a where
- kindOfType :: Type src vs (t :: kt) -> Kind src kt
- normalizeVarsTy :: Type src vs (t :: kt) -> (forall vs'. Type src vs' (t :: kt) -> ret) -> ret
- data Types src vs (ts :: [Type]) where
- mapTys :: (forall kt (t :: kt). Type src vs t -> Type src vs' t) -> Types src vs ts -> Types src vs' ts
- foldlTys :: (forall k (t :: k). Type src vs t -> acc -> acc) -> Types src vs ts -> acc -> acc
- class TypeOf a where
- data Proxy k (t :: k) :: forall k. k -> * = Proxy
- data (k :~: (a :: k)) (b :: k) :: forall k. k -> k -> * where
- data (k1 :~~: k2) (a :: k1) (b :: k2) :: forall k1 k2. k1 -> k2 -> * where
- data Constraint :: *
Type Type
data Type (src :: Type) (vs :: [Type]) (t :: kt) where Source #
TyConst :: src -> Len vs -> Const src c -> Type src vs c | |
TyApp :: src -> Type src vs f -> Type src vs a -> Type src vs (f a) | |
TyVar :: src -> NameVar -> Var src vs v -> Type src vs v | |
TyFam :: src -> Len vs -> Const src fam -> Types src vs hs -> Type src vs (Fam fam hs) |
AllocVars k (Type k src) Source # | |
SourceInj (TypeVT src) src => TestEquality k (Type k src vs) Source # | |
SourceInj (TypeVT src) src => KindOf kt (Type kt src vs) Source # | |
Source src => Eq (Type kt src vs t) Source # | |
Source src => Sourced (Type kt src vs t) Source # | |
UsedVarsOf (Type kt src vs t) Source # | |
VarOccursIn (Type kt src vs t) Source # | |
LenVars (Type kt src vs t) Source # | |
ExpandFam (Type kt src vs t) Source # | |
ConstsOf (Type kt src vs t) Source # | |
Substable (Type kt src vs t) Source # | |
type SourceOf (Type kt src vs t) Source # | |
type VarsOf (Type kt src vs t) Source # | |
pattern (:$) :: forall kt src (vs :: [Type]) (t :: kt). () => forall k (f :: k -> kt) (a :: k). (~#) kt kt t (f a) => Type (k -> kt) src vs f -> Type k src vs a -> Type kt src vs t infixr 0 Source #
pattern (:@) :: forall kt src (vs :: [Type]) (t :: kt). () => forall k (f :: k -> kt) (a :: k). (~#) kt kt t (f a) => Type (k -> kt) src vs f -> Type k src vs a -> Type kt src vs t infixl 9 Source #
tyConst :: forall kc (c :: kc) src vs. Source src => LenInj vs => Constable c => KindInjP (Ty_of_Type kc) => Type_of_Ty (Ty_of_Type kc) ~ kc => Type src vs c Source #
tyConstLen :: forall kc (c :: kc) src vs. Source src => Constable c => KindInjP (Ty_of_Type kc) => Type_of_Ty (Ty_of_Type kc) ~ kc => Len vs -> Type src vs c Source #
tyFam :: forall kc (c :: kc) as vs src. Source src => LenInj vs => Constable c => KindInjP (Ty_of_Type kc) => Type_of_Ty (Ty_of_Type kc) ~ kc => Types src vs as -> Type src vs (Fam c as) Source #
tyQual :: Source src => Type src vs q -> Type src vs t -> (Qual q -> Type src vs t -> Type src vs (q #> t)) -> Type src vs (q #> t) infix 1 Source #
Qualify a Type
.
Type TypeK
Type TypeT
Existential for Type
.
Type TypeVT
Existential polymorphic Type
.
Type Const
kindOfConst :: Const src (t :: kt) -> Kind src kt Source #
Class Constable
class (Typeable c, FixityOf c, NameTyOf c, ClassInstancesFor c, TypeInstancesFor c) => Constable c Source #
(Typeable kc c, FixityOf kc c, NameTyOf kc c, ClassInstancesFor kc c, TypeInstancesFor kc c) => Constable kc c Source # | |
Class ConstsOf
Type ConstC
Type '(->)'
(~>) :: Source src => Constable (->) => Type src vs a -> Type src vs b -> Type src vs (a -> b) infixr 0 Source #
The function Type
(->)
,
with an infix notation more readable.
Type family FunArg
Type family FunRes
unTyFun :: forall t src tys. SourceInj (TypeVT src) src => Constable (->) => Type src tys t -> Maybe (Type src tys (FunArg t), Type src tys (FunRes t)) Source #
Return, when the given Type
is a function,
the argument of that function.
Type (#>)
newtype (q :: Constraint) #> (a :: Type) infixr 0 Source #
Type constant to qualify a Type
.
Qual (q => a) |
FixityOf (Constraint -> Type -> *) (#>) Source # | |
NameTyOf (Constraint -> Type -> *) (#>) Source # | |
TypeInstancesFor (Constraint -> Type -> *) (#>) Source # | |
ClassInstancesFor (Constraint -> Type -> *) (#>) Source # | |
(#>) :: Source src => Type src vs q -> Type src vs t -> Type src vs (q #> t) infixr 0 Source #
Qualify a Type
.
Class (#)
class (x, y) => x # y infixr 2 Source #
Constraint
union.
(x, y) => x # y Source # | |
FixityOf (Constraint -> Constraint -> Constraint) (#) Source # | |
NameTyOf (Constraint -> Constraint -> Constraint) (#) Source # | |
TypeInstancesFor (Constraint -> Constraint -> Constraint) (#) Source # | |
ClassInstancesFor (Constraint -> Constraint -> Constraint) (#) Source # | |
(#) :: Source src => Type src vs qx -> Type src vs qy -> Type src vs (qx # qy) infixr 2 Source #
Unify two Constraint
s.
Type (() ::
Constraint
)
noConstraint :: Source src => LenInj vs => Type src vs (() :: Constraint) Source #
Like noConstraintLen
, but using lenInj
.
noConstraintLen :: Source src => Len vs -> Type src vs (() :: Constraint) Source #
Empty Constraint
.
Class (#~)
class x ~ y => x #~ y infixr 2 Source #
Type equality Constraint
.
(~) k x y => (#~) k x y Source # | |
FixityOf (k -> k -> Constraint) ((#~) k) Source # | |
NameTyOf (k -> k -> Constraint) ((#~) k) Source # | |
TypeInstancesFor (k -> k -> Constraint) ((#~) k) Source # | |
(KindInj k3, Typeable Type k3) => ClassInstancesFor (k3 -> k3 -> Constraint) ((#~) k3) Source # | |
(#~) :: forall k a b src vs. Source src => Typeable k => KindInj k => Type src vs (a :: k) -> Type src vs (b :: k) -> Type src vs (a #~ b) infixr 2 Source #
Constraint two Type
s to be equal.
eqType :: Source src => Type src tys (x :: k) -> Type src tys (y :: k) -> Maybe (x :~: y) Source #
Type equality.
eqTypeKi :: Source src => Type src tys (x :: kx) -> Type src tys (y :: ky) -> Maybe (x :~~: y) Source #
Heterogeneous type equality:
return two proofs when two Type
s are equals:
one for the type and one for the kind.
Comparison
ordType :: Source src => Type src tys (x :: kx) -> Type src tys (y :: ky) -> Ordering Source #
Compare two Type
s.
Type Qual
Captures the proof of a Constraint
(and its dictionaries when it contains type classes):
pattern matching on the Dict
constructor
brings the Constraint
into scope.
Class ClassInstancesFor
class ClassInstancesFor c where Source #
ClassInstancesFor Constraint () Source # | |
ClassInstancesFor (Constraint -> Type -> *) (#>) Source # | |
ClassInstancesFor (Constraint -> Constraint -> Constraint) (#) Source # | |
(KindInj k3, Typeable Type k3) => ClassInstancesFor (k3 -> k3 -> Constraint) ((#~) k3) Source # | |
Injection
constInj :: forall c src. Source src => Constable c => KindInjP (Ty_of_Type (K c)) => Type_of_Ty (Ty_of_Type (K c)) ~ K c => Const src c Source #
constKiInj :: forall kc c src. Source src => Constable c => Kind src kc -> Const src (c :: kc) Source #
Projection
proj_Const :: forall c u src. Typeable c => Const src u -> Maybe (c :~: u) Source #
Like proj_ConstKi
, but with kind equality already known.
proj_ConstTy :: forall c u src vs. Typeable c => Type src vs u -> Maybe (c :~: u) Source #
Like proj_Const
, but on a Type
.
proj_ConstKi :: forall kc (c :: kc) u src. Typeable c => kc ~ Type_of_Ty (Ty_of_Type kc) => KindInjP (Ty_of_Type kc) => Const src u -> Maybe (c :~~: u) Source #
XXX: proj_ConstKi
must be given the kc
kind explicitely,
when used multiple times in the same pattern match,
because of GHC's #12933.
proj_ConstKiTy :: forall kc (c :: kc) u src vs. Typeable c => kc ~ Type_of_Ty (Ty_of_Type kc) => KindInjP (Ty_of_Type kc) => Type src vs u -> Maybe (c :~~: u) Source #
Like proj_ConstKi
, but on a Type
.
eqConstKi :: forall src_x src_y kx ky x y. Const src_x (x :: kx) -> Const src_y (y :: ky) -> Maybe (x :~~: y) Source #
ordConst :: forall src_x src_y kx ky x y. Const src_x (x :: kx) -> Const src_y (y :: ky) -> Ordering Source #
Type family Fam
Class TypeInstancesFor
class TypeInstancesFor (c :: kc) where Source #
expandFamFor :: Source src => proxy c -> Len vs -> Const src fam -> Types src vs ts -> Maybe (Type src vs (Fam fam ts)) Source #
TypeInstancesFor Constraint () Source # | |
TypeInstancesFor (Constraint -> Type -> *) (#>) Source # | |
TypeInstancesFor (Constraint -> Constraint -> Constraint) (#) Source # | |
TypeInstancesFor (k -> k -> Constraint) ((#~) k) Source # | |
Class ExpandFam
normalizeVarsTy :: Type src vs (t :: kt) -> (forall vs'. Type src vs' (t :: kt) -> ret) -> ret Source #
Remove unused Var
s from the context.
Type Types
mapTys :: (forall kt (t :: kt). Type src vs t -> Type src vs' t) -> Types src vs ts -> Types src vs' ts Source #
foldlTys :: (forall k (t :: k). Type src vs t -> acc -> acc) -> Types src vs ts -> acc -> acc Source #
Class TypeOf
data Proxy k (t :: k) :: forall k. k -> * #
A concrete, poly-kinded proxy type
(ModuleFor k src ss s, ModulesInjR src ss rs) => ModulesInjR src ss ((:) * (Proxy k s) rs) Source # | |
(Gram_Term_AtomsFor k src ss g t, Gram_Term_AtomsR src ss rs g) => Gram_Term_AtomsR src ss ((:) * (Proxy k t) rs) g Source # | |
Generic1 k (Proxy k) | |
Monad (Proxy *) | Since: 4.7.0.0 |
Functor (Proxy *) | Since: 4.7.0.0 |
Applicative (Proxy *) | Since: 4.7.0.0 |
Foldable (Proxy *) | Since: 4.7.0.0 |
Traversable (Proxy *) | Since: 4.7.0.0 |
Eq1 (Proxy *) | Since: 4.9.0.0 |
Ord1 (Proxy *) | Since: 4.9.0.0 |
Read1 (Proxy *) | Since: 4.9.0.0 |
Show1 (Proxy *) | Since: 4.9.0.0 |
Alternative (Proxy *) | Since: 4.9.0.0 |
MonadPlus (Proxy *) | Since: 4.9.0.0 |
SymInjP * k Zero ((:) * (Proxy k s) ss) s Source # | |
SymInjP * k2 p ss s => SymInjP * k2 (Succ p) ((:) * (Proxy k1 not_s) ss) s Source # | |
(NameTyOf k t, FixityOf k t, ImportTypes [*] ts) => ImportTypes [*] ((:) * (Proxy k t) ts) Source # | |
(KindInjP (Ty_of_Type (K k c)), (~) * (K k c) (Type_of_Ty (Ty_of_Type (K k c))), Constable k c, ModulesTyInj [*] ts) => ModulesTyInj [*] ((:) * (Proxy k c) ts) Source # | |
Bounded (Proxy k t) | |
Enum (Proxy k s) | Since: 4.7.0.0 |
Eq (Proxy k s) | Since: 4.7.0.0 |
Ord (Proxy k s) | Since: 4.7.0.0 |
Read (Proxy k s) | Since: 4.7.0.0 |
Show (Proxy k s) | Since: 4.7.0.0 |
Ix (Proxy k s) | Since: 4.7.0.0 |
Generic (Proxy k t) | |
Semigroup (Proxy k s) | Since: 4.9.0.0 |
Monoid (Proxy k s) | Since: 4.7.0.0 |
type Rep1 k (Proxy k) | |
type Rep (Proxy k t) | |
data (k :~: (a :: k)) (b :: k) :: forall k. k -> k -> * where infix 4 #
Propositional equality. If a :~: b
is inhabited by some terminating
value, then the type a
is the same as the type b
. To use this equality
in practice, pattern-match on the a :~: b
to get out the Refl
constructor;
in the body of the pattern-match, the compiler knows that a ~ b
.
Since: 4.7.0.0
data (k1 :~~: k2) (a :: k1) (b :: k2) :: forall k1 k2. k1 -> k2 -> * where infix 4 #
Kind heterogeneous propositional equality. Like '(:~:)', a :~~: b
is
inhabited by a terminating value if and only if a
is the same type as b
.
Since: 4.10.0.0
TestEquality k ((:~~:) k1 k a) | Since: 4.10.0.0 |
(~~) k1 k2 a b => Bounded ((:~~:) k1 k2 a b) | Since: 4.10.0.0 |
(~~) k1 k2 a b => Enum ((:~~:) k1 k2 a b) | Since: 4.10.0.0 |
Eq ((:~~:) k1 k2 a b) | Since: 4.10.0.0 |
Ord ((:~~:) k1 k2 a b) | Since: 4.10.0.0 |
(~~) k1 k2 a b => Read ((:~~:) k1 k2 a b) | Since: 4.10.0.0 |
Show ((:~~:) k1 k2 a b) | Since: 4.10.0.0 |
data Constraint :: * #
The kind of constraints, like Show a