Safe Haskell | None |
---|---|
Language | Haskell2010 |
Language.Symantic.Typing.Kind
Contents
- data Kind src k where
- KiType :: src -> Kind src Type
- KiConstraint :: src -> Kind src Constraint
- KiFun :: src -> Kind src ka -> Kind src kb -> Kind src (ka -> kb)
- eqKind :: Kind xs x -> Kind ys y -> Maybe (x :~: y)
- type K (t :: kt) = kt
- class KindOf (a :: kt -> Type) where
- class (KindInjP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => KindInj k
- kindInj :: forall k src. Source src => KindInj k => Kind src k
- class KindInjP k where
- data Ty
- type family Ty_of_Type (t :: Type) :: Type
- type family Type_of_Ty (t :: Type) :: Type
- data KindK src = KindK (Kind src k)
- data Con_Kind src
- = Con_Kind_Eq (KindK src) (KindK src)
- | Con_Kind_Arrow (KindK src)
- when_EqKind :: ErrorInj (Con_Kind src) err => Kind src x -> Kind src y -> ((x :~: y) -> Either err ret) -> Either err ret
- when_KiFun :: ErrorInj (Con_Kind src) err => SourceInj (KindK src) src => Kind src x -> (forall a b. (x :~: (a -> b)) -> Kind src a -> Kind src b -> Either err ret) -> Either err ret
Type Kind
data Kind src k where Source #
Singleton for kind types.
Constructors
KiType :: src -> Kind src Type | |
KiConstraint :: src -> Kind src Constraint | |
KiFun :: src -> Kind src ka -> Kind src kb -> Kind src (ka -> kb) infixr 5 |
Type K
Class KindOf
class KindOf (a :: kt -> Type) where Source #
Return the Kind
of something.
Minimal complete definition
Type KindInj
class (KindInjP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => KindInj k Source #
Implicit Kind
.
NOTE: GHC-8.0.1's bug #12933
makes it fail to properly build an implicit Kind
,
this can however be worked around by having the class instances
work on a data type Ty
instead of Type
,
hence the introduction of Ty
, Ty_of_Type
, Type_of_Ty
and KindP
.Inj
Instances
(KindInjP (Ty_of_Type k), (~) Type (Type_of_Ty (Ty_of_Type k)) k) => KindInj k Source # | |
Type KindInjP
class KindInjP k where Source #
Minimal complete definition
Methods
kindInjP :: src -> Kind src (Type_of_Ty k) Source #
Type Ty
FIXME: workaround to be removed when #12933 will be fixed.
Type family Ty_of_Type
type family Ty_of_Type (t :: Type) :: Type Source #
NOTE: As of GHC-8.0.2, using a closed type family does not work here,
this notably disables the expansion of Ty_of_Type
Any
.
Instances
type Ty_of_Type Type Source # | |
type Ty_of_Type Constraint Source # | |
type Ty_of_Type (a -> b) Source # | |
Type family Type_of_Ty
type family Type_of_Ty (t :: Type) :: Type Source #
NOTE: As of GHC-8.0.2, using a closed type family does not work here,
this notably disables the expansion of Type_of_Ty
Any
.
Instances
type Type_of_Ty Constraint Source # | |
type Type_of_Ty Ty Source # | |
type Type_of_Ty (a -> b) Source # | |
Type KindK
Existential for Kind
.
Type Con_Kind
Constructors
Con_Kind_Eq (KindK src) (KindK src) | |
Con_Kind_Arrow (KindK src) |