| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Language.Symantic.Typing.Type
Contents
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 #
Constructors
| 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 Methods 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 #
Minimal complete definition
Nothing
Methods
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 #
Minimal complete definition
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.
Constructors
| 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 Consts 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 #
Constructors
| 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
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 Constraints.
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 Types 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 Types 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 Types.
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 Vars 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 EitherProxy
>>>Proxy :: Proxy FunctorProxy
>>>Proxy :: Proxy complicatedStructureProxy
Constructors
| Proxy |
Instances
| (ModuleFor src ss s, ModulesInjR src ss rs) => ModulesInjR src ss (Proxy s ': rs) Source # | |
Defined in Language.Symantic.Compiling.Module Methods 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 Methods 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 Methods 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 Methods 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 |
Defined in Data.Proxy | |
| 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 Methods 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.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 Methods 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