Type.Reflection
Copyright | (c) The University of Glasgow CWI 2001--2017 |
---|---|
License | BSD-style (see the file libraries/base/LICENSE) |
Maintainer | [email protected] |
Stability | experimental |
Portability | non-portable (requires GADTs and compiler support) |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
Description
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). ([PDF](https:/www.microsoft.comen-usresearchwp-contentuploads201608dynamic.pdf))
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
The Typeable class
class Typeable (a :: k) Source
The class Typeable
allows a concrete representation of a type to be calculated.
Minimal complete definition
typeRep#
typeRep :: Typeable a => TypeRep a Source
withTypeable :: forall k (a :: k) rep (r :: TYPE rep). TypeRep a -> (Typeable a => r) -> r Source
Use a TypeRep
as Typeable
evidence.
Propositional equality
data a :~: b 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) | Since: base-4.7.0.0 |
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
TestCoercion ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Coercion | |
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 Methodssucc :: (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 | |
Eq (a :~: b) | Since: base-4.7.0.0 |
(a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Data Methodsgfoldl :: (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 | |
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 :~~: b 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) | Since: base-4.10.0.0 |
TestEquality ((:~~:) a :: k -> Type) | Since: base-4.10.0.0 |
Defined in Data.Type.Equality | |
TestCoercion ((:~~:) a :: k -> Type) | Since: base-4.10.0.0 |
Defined in Data.Type.Coercion | |
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 Methodssucc :: (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 | |
Eq (a :~~: b) | Since: base-4.10.0.0 |
(Typeable i, Typeable j, Typeable a, Typeable b, a ~~ b) => Data (a :~~: b) | Since: base-4.10.0.0 |
Defined in Data.Data Methodsgfoldl :: (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 | |
Ord (a :~~: b) | Since: base-4.10.0.0 |
Defined in Data.Type.Equality Methodscompare :: (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 | |
a ~~ b => Read (a :~~: b) | Since: base-4.10.0.0 |
Show (a :~~: b) | Since: base-4.10.0.0 |
Type representations
Type-Indexed
A concrete representation of a (monomorphic) type. TypeRep
supports reasonably efficient equality.
Instances
TestEquality (TypeRep :: k -> Type) | |
Defined in Data.Typeable.Internal | |
Eq (TypeRep a) | Since: base-2.1 |
Ord (TypeRep a) | Since: base-4.4.0.0 |
Defined in Data.Typeable.Internal | |
Show (TypeRep a) | |
typeOf :: Typeable a => a -> TypeRep a Source
pattern App :: forall k2 (t :: k2). () => forall k1 (a :: k1 -> k2) (b :: k1). 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 :: forall k (a :: k). () => IsApplication a ~ "" => TyCon -> TypeRep a Source
Pattern match on a type constructor
pattern Con' :: forall k (a :: k). () => IsApplication 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 :: k). () => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (arg :: TYPE r1) (res :: TYPE r2). (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 :: TypeRep a -> TyCon Source
Observe the type constructor of a type representation
rnfTypeRep :: 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
typeRepKind :: TypeRep (a :: k) -> TypeRep k Source
Observe the kind of a type.
splitApps :: TypeRep a -> (TyCon, [SomeTypeRep]) Source
Quantified
data SomeTypeRep where Source
A non-indexed type representation.
Constructors
SomeTypeRep :: forall k (a :: k). !(TypeRep a) -> SomeTypeRep |
Instances
Eq SomeTypeRep | |
Defined in Data.Typeable.Internal Methods(==) :: SomeTypeRep -> SomeTypeRep -> Bool Source (/=) :: SomeTypeRep -> SomeTypeRep -> Bool Source | |
Ord SomeTypeRep | |
Defined in Data.Typeable.Internal Methodscompare :: 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 | |
Show SomeTypeRep | Since: base-4.10.0.0 |
Defined in Data.Typeable.Internal MethodsshowsPrec :: Int -> SomeTypeRep -> ShowS Source show :: SomeTypeRep -> String Source showList :: [SomeTypeRep] -> ShowS Source |
someTypeRep :: forall proxy a. 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
tyConName :: TyCon -> String Source
rnfTyCon :: TyCon -> () Source
Module names
Instances
moduleName :: Module -> String Source
modulePackage :: Module -> String Source
rnfModule :: Module -> () Source
Helper to fully evaluate TyCon
for use as NFData(rnf)
implementation
Since: base-4.8.0.0
© The University of Glasgow and others
Licensed under a BSD-style license (see top of the page).
https://downloads.haskell.org/~ghc/8.10.2/docs/html/libraries/base-4.14.1.0/Type-Reflection.html