Copyright | (c) The University of Glasgow CWI 2001--2017 |
---|---|
License | BSD-style (see the file libraries/base/LICENSE) |
Maintainer | libraries@haskell.org |
Stability | stable |
Portability | non-portable (requires GADTs and compiler support) |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
This provides a type-indexed type representation mechanism, similar to that described by,
- Simon Peyton-Jones, Stephanie Weirich, Richard Eisenberg, Dimitrios Vytiniotis. "A reflection on types". Proc. Philip Wadler's 60th birthday Festschrift, Edinburgh (April 2016).
The interface provides TypeRep
, a type representation which can
be safely decomposed and composed. See Data.Dynamic for an example of this.
@since base-4.10.0.0
Synopsis
- class Typeable (a :: k)
- typeRep :: forall {k} (a :: k). Typeable a => TypeRep a
- withTypeable :: forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
- data (a :: k) :~: (b :: k) where
- data (a :: k1) :~~: (b :: k2) where
- data TypeRep (a :: k)
- pattern TypeRep :: () => Typeable a => TypeRep a
- typeOf :: Typeable a => a -> TypeRep a
- pattern App :: forall k2 t k1 a b. () => t ~ a b => TypeRep a -> TypeRep b -> TypeRep t
- pattern Con :: () => NotApplication a => TyCon -> TypeRep a
- pattern Con' :: () => NotApplication a => TyCon -> [SomeTypeRep] -> TypeRep a
- pattern Fun :: forall k fun (r1 :: RuntimeRep) (r2 :: RuntimeRep) arg res. () => (k ~ Type, fun ~~ (arg -> res)) => TypeRep arg -> TypeRep res -> TypeRep fun
- typeRepTyCon :: forall {k} (a :: k). TypeRep a -> TyCon
- rnfTypeRep :: forall {k} (a :: k). TypeRep a -> ()
- eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b)
- decTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Either ((a :~~: b) -> Void) (a :~~: b)
- typeRepKind :: forall k (a :: k). TypeRep a -> TypeRep k
- splitApps :: forall {k} (a :: k). TypeRep a -> (TyCon, [SomeTypeRep])
- data SomeTypeRep where
- SomeTypeRep :: forall k (a :: k). !(TypeRep a) -> SomeTypeRep
- someTypeRep :: forall {k} proxy (a :: k). Typeable a => proxy a -> SomeTypeRep
- someTypeRepTyCon :: SomeTypeRep -> TyCon
- rnfSomeTypeRep :: SomeTypeRep -> ()
- data TyCon
- tyConPackage :: TyCon -> String
- tyConModule :: TyCon -> String
- tyConName :: TyCon -> String
- rnfTyCon :: TyCon -> ()
- data Module
- moduleName :: Module -> String
- modulePackage :: Module -> String
- rnfModule :: Module -> ()
The Typeable class
class Typeable (a :: k) Source #
The class Typeable
allows a concrete representation of a type to
be calculated.
typeRep#
withTypeable :: forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r Source #
Use a TypeRep
as Typeable
evidence.
The TypeRep
pattern synonym brings a Typeable
constraint into
scope and can be used in place of withTypeable
.
f :: TypeRep a -> .. f rep = withTypeable {- Typeable a in scope -} f :: TypeRep a -> .. f TypeRep = {- Typeable a in scope -}
Propositional equality
data (a :: k) :~: (b :: k) where infix 4 Source #
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
Category ((:~:) :: k -> k -> Type) Source # | @since base-4.7.0.0 |
TestCoercion ((:~:) a :: k -> Type) Source # | @since base-4.7.0.0 |
Defined in GHC.Internal.Data.Type.Coercion | |
TestEquality ((:~:) a :: k -> Type) Source # | @since base-4.7.0.0 |
Defined in GHC.Internal.Data.Type.Equality | |
(a ~ b, Data a) => Data (a :~: b) Source # | @since base-4.7.0.0 |
Defined in GHC.Internal.Data.Data gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) Source # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) Source # toConstr :: (a :~: b) -> Constr Source # dataTypeOf :: (a :~: b) -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) Source # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source # gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source # | |
a ~ b => Bounded (a :~: b) Source # | @since base-4.7.0.0 |
a ~ b => Enum (a :~: b) Source # | @since base-4.7.0.0 |
Defined in GHC.Internal.Data.Type.Equality succ :: (a :~: b) -> a :~: b Source # pred :: (a :~: b) -> a :~: b Source # toEnum :: Int -> a :~: b Source # fromEnum :: (a :~: b) -> Int Source # enumFrom :: (a :~: b) -> [a :~: b] Source # enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] Source # enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] Source # enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] Source # | |
a ~ b => Read (a :~: b) Source # | @since base-4.7.0.0 |
Show (a :~: b) Source # | @since base-4.7.0.0 |
Eq (a :~: b) Source # | @since base-4.7.0.0 |
Ord (a :~: b) Source # | @since base-4.7.0.0 |
Defined in GHC.Internal.Data.Type.Equality |
data (a :: k1) :~~: (b :: k2) where infix 4 Source #
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
Category ((:~~:) :: k -> k -> Type) Source # | @since base-4.10.0.0 |
TestCoercion ((:~~:) a :: k -> Type) Source # | @since base-4.10.0.0 |
Defined in GHC.Internal.Data.Type.Coercion | |
TestEquality ((:~~:) a :: k -> Type) Source # | @since base-4.10.0.0 |
Defined in GHC.Internal.Data.Type.Equality | |
(Typeable i, Typeable j, Typeable a, Typeable b, a ~~ b) => Data (a :~~: b) Source # | @since base-4.10.0.0 |
Defined in GHC.Internal.Data.Data gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~~: b) -> c (a :~~: b) Source # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~~: b) Source # toConstr :: (a :~~: b) -> Constr Source # dataTypeOf :: (a :~~: b) -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~~: b)) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~~: b)) Source # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~~: b) -> a :~~: b Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r Source # gmapQ :: (forall d. Data d => d -> u) -> (a :~~: b) -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~~: b) -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) Source # | |
a ~~ b => Bounded (a :~~: b) Source # | @since base-4.10.0.0 |
a ~~ b => Enum (a :~~: b) Source # | @since base-4.10.0.0 |
Defined in GHC.Internal.Data.Type.Equality succ :: (a :~~: b) -> a :~~: b Source # pred :: (a :~~: b) -> a :~~: b Source # toEnum :: Int -> a :~~: b Source # fromEnum :: (a :~~: b) -> Int Source # enumFrom :: (a :~~: b) -> [a :~~: b] Source # enumFromThen :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] Source # enumFromTo :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] Source # enumFromThenTo :: (a :~~: b) -> (a :~~: b) -> (a :~~: b) -> [a :~~: b] Source # | |
a ~~ b => Read (a :~~: b) Source # | @since base-4.10.0.0 |
Show (a :~~: b) Source # | @since base-4.10.0.0 |
Eq (a :~~: b) Source # | @since base-4.10.0.0 |
Ord (a :~~: b) Source # | @since base-4.10.0.0 |
Defined in GHC.Internal.Data.Type.Equality compare :: (a :~~: b) -> (a :~~: b) -> Ordering Source # (<) :: (a :~~: b) -> (a :~~: b) -> Bool Source # (<=) :: (a :~~: b) -> (a :~~: b) -> Bool Source # (>) :: (a :~~: b) -> (a :~~: b) -> Bool Source # (>=) :: (a :~~: b) -> (a :~~: b) -> Bool Source # |
Type representations
Type-Indexed
data TypeRep (a :: k) Source #
TypeRep is a concrete representation of a (monomorphic) type.
TypeRep
supports reasonably efficient equality.
See Note [Grand plan for Typeable] in GHC.Tc.Instance.Typeable
Instances
TestEquality (TypeRep :: k -> Type) Source # | |
Defined in GHC.Internal.Data.Typeable.Internal | |
Show (TypeRep a) Source # | |
Eq (TypeRep a) Source # | @since base-2.01 |
Ord (TypeRep a) Source # | @since base-4.4.0.0 |
Defined in GHC.Internal.Data.Typeable.Internal |
pattern TypeRep :: () => Typeable a => TypeRep a Source #
A explicitly bidirectional pattern synonym to construct a concrete representation of a type.
As an expression: Constructs a singleton TypeRep a
given a
implicit 'Typeable a' constraint:
TypeRep @a :: Typeable a => TypeRep a
As a pattern: Matches on an explicit TypeRep a
witness bringing
an implicit Typeable a
constraint into scope.
f :: TypeRep a -> .. f TypeRep = {- Typeable a in scope -}
@since base-4.17.0.0
pattern App :: forall k2 t k1 a b. () => t ~ a b => TypeRep a -> TypeRep b -> TypeRep t Source #
A type application.
For instance,
typeRep @(Maybe Int) === App (typeRep @Maybe) (typeRep @Int)
Note that this will also match a function type,
typeRep @(Int# -> Char) === App (App arrow (typeRep @Int#)) (typeRep @Char)
where arrow :: TypeRep ((->) :: TYPE IntRep -> Type -> Type)
.
pattern Con :: () => NotApplication a => TyCon -> TypeRep a Source #
Pattern match on a type constructor
pattern Con' :: () => NotApplication a => TyCon -> [SomeTypeRep] -> TypeRep a Source #
Pattern match on a type constructor including its instantiated kind variables.
For instance,
App (Con' proxyTyCon ks) intRep = typeRep @(Proxy @Int)
will bring into scope,
proxyTyCon :: TyCon
ks == [someTypeRep Type] :: [SomeTypeRep]
intRep == typeRep
Int
pattern Fun :: forall k fun (r1 :: RuntimeRep) (r2 :: RuntimeRep) arg res. () => (k ~ Type, fun ~~ (arg -> res)) => TypeRep arg -> TypeRep res -> TypeRep fun Source #
The function type constructor.
For instance,
typeRep @(Int -> Char) === Fun (typeRep @Int) (typeRep @Char)
typeRepTyCon :: forall {k} (a :: k). TypeRep a -> TyCon Source #
Observe the type constructor of a type representation
rnfTypeRep :: forall {k} (a :: k). TypeRep a -> () Source #
Helper to fully evaluate TypeRep
for use as NFData(rnf)
implementation
@since base-4.8.0.0
eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b) Source #
Type equality
@since base-4.10
decTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Either ((a :~~: b) -> Void) (a :~~: b) Source #
Type equality decision
@since base-4.19.0.0
typeRepKind :: forall k (a :: k). TypeRep a -> TypeRep k Source #
Observe the kind of a type.
Quantified
data SomeTypeRep where Source #
A non-indexed type representation.
SomeTypeRep :: forall k (a :: k). !(TypeRep a) -> SomeTypeRep |
Instances
Show SomeTypeRep Source # | @since base-4.10.0.0 |
Defined in GHC.Internal.Data.Typeable.Internal | |
Eq SomeTypeRep Source # | |
Defined in GHC.Internal.Data.Typeable.Internal (==) :: SomeTypeRep -> SomeTypeRep -> Bool Source # (/=) :: SomeTypeRep -> SomeTypeRep -> Bool Source # | |
Ord SomeTypeRep Source # | |
Defined in GHC.Internal.Data.Typeable.Internal compare :: SomeTypeRep -> SomeTypeRep -> Ordering Source # (<) :: SomeTypeRep -> SomeTypeRep -> Bool Source # (<=) :: SomeTypeRep -> SomeTypeRep -> Bool Source # (>) :: SomeTypeRep -> SomeTypeRep -> Bool Source # (>=) :: SomeTypeRep -> SomeTypeRep -> Bool Source # max :: SomeTypeRep -> SomeTypeRep -> SomeTypeRep Source # min :: SomeTypeRep -> SomeTypeRep -> SomeTypeRep Source # |
someTypeRep :: forall {k} proxy (a :: k). Typeable a => proxy a -> SomeTypeRep Source #
Takes a value of type a
and returns a concrete representation
of that type.
@since base-4.7.0.0
someTypeRepTyCon :: SomeTypeRep -> TyCon Source #
Observe the type constructor of a quantified type representation.
rnfSomeTypeRep :: SomeTypeRep -> () Source #
Helper to fully evaluate SomeTypeRep
for use as NFData(rnf)
implementation
@since base-4.10.0.0
Type constructors
tyConPackage :: TyCon -> String Source #
tyConModule :: TyCon -> String Source #
Module names
Instances
moduleName :: Module -> String Source #
modulePackage :: Module -> String Source #