Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- class TypeOf a where
- data Types src vs (ts :: [Type]) where
- class ExpandFam a where
- class TypeInstancesFor (c :: kc) where
- type family Fam (fam :: k) (hs :: [Type]) :: k
- class ClassInstancesFor c where
- proveConstraintFor :: Source src => proxy c -> Type src vs q -> Maybe (Qual q)
- data Qual q where
- class x ~ y => x #~ y
- class (x, y) => x # y
- newtype (q :: Constraint) #> (a :: Type) = Qual (q => a)
- type family FunRes (fun :: Type) :: Type where ...
- type family FunArg (fun :: Type) :: Type where ...
- data ConstC src = ConstC (Const src c)
- class ConstsOf a where
- class (Typeable c, FixityOf c, NameTyOf c, ClassInstancesFor c, TypeInstancesFor c) => Constable c
- data Const src (c :: kc) where
- data TypeVT src = TypeVT (Type src vs t)
- data TypeT src vs = TypeT (Type src vs t)
- data TypeK src vs kt = TypeK (Type src vs t)
- data Type (src :: Type) (vs :: [Type]) (t :: kt) where
- pattern (:@) :: forall kt src (vs :: [Type]) (t :: kt). () => forall k (f :: k -> kt) (a :: k). t ~# f a => Type src vs f -> Type src vs a -> Type src vs t
- pattern (:$) :: forall kt src (vs :: [Type]) (t :: kt). () => forall k (f :: k -> kt) (a :: k). t ~# f a => Type src vs f -> Type src vs a -> Type 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)
- kindOfConst :: Const src (t :: kt) -> Kind src kt
- (~>) :: Source src => Constable (->) => Type src vs a -> Type src vs b -> Type src vs (a -> b)
- 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 src => Type src vs q -> Type src vs t -> Type src vs (q #> t)
- (#) :: 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)
- (#~) :: 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
- 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
- kindOfType :: Type src vs (t :: kt) -> Kind src kt
- normalizeVarsTy :: Type src vs (t :: kt) -> (forall vs'. Type src vs' (t :: kt) -> ret) -> ret
- 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
- data Proxy (t :: k) :: forall k. k -> Type = Proxy
- data (a :: k) :~: (b :: k) :: forall k. k -> k -> Type where
- data (a :: k1) :~~: (b :: k2) :: forall k1 k2. k1 -> k2 -> Type where
- data Constraint
Documentation
data Types src vs (ts :: [Type]) where Source #
TypesZ :: Types src vs '[] | |
TypesS :: Type src vs t -> Types src vs ts -> Types src vs (Proxy t ': ts) infixr 5 |
Instances
Source src => Show (Types src vs ts) Source # | |
UsedVarsOf (Types src vs ts) Source # | |
VarOccursIn (Types src vs ts) Source # | |
Defined in Language.Symantic.Typing.Type | |
ConstsOf (Types src vs ts) Source # | |
Substable (Types src vs ts) Source # | |
Defined in Language.Symantic.Typing.Unify substVarUnsafe :: (src0 ~ SourceOf (Types src vs ts), vs0 ~ VarsOf (Types src vs ts)) => Var src0 vs0 v -> Type src0 vs0 v -> Types src vs ts -> Types src vs ts Source # subst :: (src0 ~ SourceOf (Types src vs ts), vs0 ~ VarsOf (Types src vs ts)) => Subst src0 vs0 -> Types src vs ts -> Types src vs ts Source # | |
type SourceOf (Types src vs ts) Source # | |
Defined in Language.Symantic.Typing.Type | |
type VarsOf (Types src vs ts) Source # | |
Defined in Language.Symantic.Typing.Type |
class TypeInstancesFor (c :: kc) where Source #
Nothing
expandFamFor :: Source src => proxy c -> Len vs -> Const src fam -> Types src vs ts -> Maybe (Type src vs (Fam fam ts)) Source #
Instances
TypeInstancesFor () Source # | |
TypeInstancesFor (#>) Source # | |
TypeInstancesFor (#) Source # | |
TypeInstancesFor ((#~) :: k -> k -> Constraint) Source # | |
class ClassInstancesFor c where Source #
Nothing
Instances
ClassInstancesFor () Source # | |
Defined in Language.Symantic.Typing.Type | |
ClassInstancesFor (#>) Source # | |
Defined in Language.Symantic.Typing.Type | |
ClassInstancesFor (#) Source # | |
Defined in Language.Symantic.Typing.Type | |
(KindInj k, Typeable k) => ClassInstancesFor ((#~) :: k -> k -> Constraint) Source # | |
Defined in Language.Symantic.Typing.Type |
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 x ~ y => x #~ y infixr 2 Source #
Type equality Constraint
.
Instances
x ~ y => (x :: k) #~ (y :: k) Source # | |
Defined in Language.Symantic.Typing.Type | |
FixityOf ((#~) :: k -> k -> Constraint) Source # | |
NameTyOf ((#~) :: k -> k -> Constraint) Source # | |
TypeInstancesFor ((#~) :: k -> k -> Constraint) Source # | |
(KindInj k, Typeable k) => ClassInstancesFor ((#~) :: k -> k -> Constraint) Source # | |
Defined in Language.Symantic.Typing.Type |
class (x, y) => x # y infixr 2 Source #
Constraint
union.
newtype (q :: Constraint) #> (a :: Type) infixr 0 Source #
Type constant to qualify a Type
.
Qual (q => a) |
Instances
Eq (ConstC src) Source # | |
Ord (ConstC src) Source # | |
Defined in Language.Symantic.Typing.Type |
class ConstsOf a where Source #
Return the Const
s used by something.
class (Typeable c, FixityOf c, NameTyOf c, ClassInstancesFor c, TypeInstancesFor c) => Constable c Source #
Instances
(Typeable c, FixityOf c, NameTyOf c, ClassInstancesFor c, TypeInstancesFor c) => Constable (c :: kc) Source # | |
Defined in Language.Symantic.Typing.Type |
data Const src (c :: kc) where Source #
Type constant.
Instances
SourceInj (ConstC src) src => KindOf (Const src :: kt -> Type) Source # | |
Eq (Const src c) Source # | |
Ord (Const src c) Source # | |
Defined in Language.Symantic.Typing.Type | |
NameTyOf c => Show (Const src c) Source # | |
ConstsOf (Const src c) Source # | |
type SourceOf (Const src c) Source # | |
Defined in Language.Symantic.Typing.Type |
Existential polymorphic Type
.
Existential for 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) |
Instances
AllocVars (Type src :: [Type] -> k -> Type) Source # | |
Defined in Language.Symantic.Typing.Type | |
SourceInj (TypeVT src) src => TestEquality (Type src vs :: k -> Type) Source # | |
Defined in Language.Symantic.Typing.Type | |
SourceInj (TypeVT src) src => KindOf (Type src vs :: kt -> Type) Source # | |
Source src => Eq (Type src vs t) Source # | |
Source src => Show (Type src vs t) Source # | |
Source src => Sourceable (Type src vs t) Source # | |
UsedVarsOf (Type src vs t) Source # | |
VarOccursIn (Type src vs t) Source # | |
Defined in Language.Symantic.Typing.Type | |
LenVars (Type src vs t) Source # | |
ExpandFam (Type src vs t) Source # | |
ConstsOf (Type src vs t) Source # | |
Substable (Type src vs t) Source # | |
Defined in Language.Symantic.Typing.Unify | |
type SourceOf (Type src vs t) Source # | |
Defined in Language.Symantic.Typing.Type | |
type VarsOf (Type src vs t) Source # | |
Defined in Language.Symantic.Typing.Type |
pattern (:@) :: forall kt src (vs :: [Type]) (t :: kt). () => forall k (f :: k -> kt) (a :: k). t ~# f a => Type src vs f -> Type src vs a -> Type src vs t infixl 9 Source #
pattern (:$) :: forall kt src (vs :: [Type]) (t :: kt). () => forall k (f :: k -> kt) (a :: k). t ~# f a => Type src vs f -> Type src vs a -> Type src vs t infixr 0 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
.
kindOfConst :: Const src (t :: kt) -> Kind src kt Source #
(~>) :: 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.
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.
(#>) :: Source src => Type src vs q -> Type src vs t -> Type src vs (q #> t) infixr 0 Source #
Qualify a Type
.
(#) :: Source src => Type src vs qx -> Type src vs qy -> Type src vs (qx # qy) infixr 2 Source #
Unify two Constraint
s.
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
.
(#~) :: 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.
ordType :: Source src => Type src tys (x :: kx) -> Type src tys (y :: ky) -> Ordering Source #
Compare two Type
s.
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 #
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 #
normalizeVarsTy :: Type src vs (t :: kt) -> (forall vs'. Type src vs' (t :: kt) -> ret) -> ret Source #
Remove unused Var
s from the context.
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 #
data Proxy (t :: k) :: forall k. k -> Type #
Proxy
is a type that holds no data, but has a phantom parameter of
arbitrary type (or even kind). Its use is to provide type information, even
though there is no value available of that type (or it may be too costly to
create one).
Historically,
is a safer alternative to the
Proxy
:: Proxy
a'undefined :: a'
idiom.
>>>
Proxy :: Proxy (Void, Int -> Int)
Proxy
Proxy can even hold types of higher kinds,
>>>
Proxy :: Proxy Either
Proxy
>>>
Proxy :: Proxy Functor
Proxy
>>>
Proxy :: Proxy complicatedStructure
Proxy
Instances
(ModuleFor src ss s, ModulesInjR src ss rs) => ModulesInjR src ss (Proxy s ': rs) Source # | |
Defined in Language.Symantic.Compiling.Module modulesInjR :: Either Error_Module (Modules src ss) Source # | |
(Gram_Term_AtomsFor src ss g t, Gram_Term_AtomsR src ss rs g) => Gram_Term_AtomsR src ss (Proxy t ': rs) g Source # | |
Defined in Language.Symantic.Compiling.Grammar g_term_atomsR :: [CF g (AST_Term src ss)] Source # | |
Generic1 (Proxy :: k -> Type) | |
Monad (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Functor (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Applicative (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Foldable (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Defined in Data.Foldable fold :: Monoid m => Proxy m -> m # foldMap :: Monoid m => (a -> m) -> Proxy a -> m # foldr :: (a -> b -> b) -> b -> Proxy a -> b # foldr' :: (a -> b -> b) -> b -> Proxy a -> b # foldl :: (b -> a -> b) -> b -> Proxy a -> b # foldl' :: (b -> a -> b) -> b -> Proxy a -> b # foldr1 :: (a -> a -> a) -> Proxy a -> a # foldl1 :: (a -> a -> a) -> Proxy a -> a # elem :: Eq a => a -> Proxy a -> Bool # maximum :: Ord a => Proxy a -> a # minimum :: Ord a => Proxy a -> a # | |
Traversable (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Eq1 (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Ord1 (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Defined in Data.Functor.Classes | |
Read1 (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Defined in Data.Functor.Classes | |
Show1 (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Alternative (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
MonadPlus (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
SymInjP Zero (Proxy s ': ss) (s :: k) Source # | |
SymInjP p ss s => SymInjP (Succ p :: Type) (Proxy not_s ': ss) (s :: k2) Source # | |
(NameTyOf t, FixityOf t, ImportTypes ts) => ImportTypes (Proxy t ': ts :: [Type]) Source # | |
Defined in Language.Symantic.Typing.Module | |
(KindInjP (Ty_of_Type (K c)), K c ~ Type_of_Ty (Ty_of_Type (K c)), Constable c, ModulesTyInj ts) => ModulesTyInj (Proxy c ': ts :: [Type]) Source # | |
Defined in Language.Symantic.Typing.Grammar modulesTyInj :: Source src => ModulesTy src Source # | |
Bounded (Proxy t) | Since: base-4.7.0.0 |
Enum (Proxy s) | Since: base-4.7.0.0 |
Eq (Proxy s) | Since: base-4.7.0.0 |
Ord (Proxy s) | Since: base-4.7.0.0 |
Read (Proxy t) | Since: base-4.7.0.0 |
Show (Proxy s) | Since: base-4.7.0.0 |
Ix (Proxy s) | Since: base-4.7.0.0 |
Generic (Proxy t) | |
Semigroup (Proxy s) | Since: base-4.9.0.0 |
Monoid (Proxy s) | Since: base-4.7.0.0 |
type Rep1 (Proxy :: k -> Type) | Since: base-4.6.0.0 |
type Rep (Proxy t) | Since: base-4.6.0.0 |
data (a :: k) :~: (b :: k) :: forall k. k -> k -> Type 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: base-4.7.0.0
Instances
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0 |
a ~ b => Enum (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
Eq (a :~: b) | Since: base-4.7.0.0 |
Ord (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
a ~ b => Read (a :~: b) | Since: base-4.7.0.0 |
Show (a :~: b) | Since: base-4.7.0.0 |
data (a :: k1) :~~: (b :: k2) :: forall k1 k2. k1 -> k2 -> Type 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: base-4.10.0.0
Instances
TestEquality ((:~~:) a :: k -> Type) | Since: base-4.10.0.0 |
Defined in Data.Type.Equality | |
a ~~ b => Bounded (a :~~: b) | Since: base-4.10.0.0 |
a ~~ b => Enum (a :~~: b) | Since: base-4.10.0.0 |
Defined in Data.Type.Equality succ :: (a :~~: b) -> a :~~: b # pred :: (a :~~: b) -> a :~~: b # fromEnum :: (a :~~: b) -> Int # enumFrom :: (a :~~: b) -> [a :~~: b] # enumFromThen :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] # enumFromTo :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] # enumFromThenTo :: (a :~~: b) -> (a :~~: b) -> (a :~~: b) -> [a :~~: b] # | |
Eq (a :~~: b) | Since: base-4.10.0.0 |
Ord (a :~~: b) | Since: base-4.10.0.0 |
a ~~ b => Read (a :~~: b) | Since: base-4.10.0.0 |
Show (a :~~: b) | Since: base-4.10.0.0 |
data Constraint #
The kind of constraints, like Show a