Define typeRep in terms of new Proxy#
[packages/base.git] / Data / Typeable.hs
1 {-# LANGUAGE Trustworthy #-}
2 {-# LANGUAGE NoImplicitPrelude
3 , OverlappingInstances
4 , ScopedTypeVariables
5 , ForeignFunctionInterface
6 , FlexibleInstances
7 , TypeOperators
8 , PolyKinds
9 , GADTs
10 , MagicHash
11 #-}
12 {-# OPTIONS_GHC -funbox-strict-fields #-}
13
14 -- The -XOverlappingInstances flag allows the user to over-ride
15 -- the instances for Typeable given here. In particular, we provide an instance
16 -- instance ... => Typeable (s a)
17 -- But a user might want to say
18 -- instance ... => Typeable (MyType a b)
19
20 -----------------------------------------------------------------------------
21 -- |
22 -- Module : Data.Typeable
23 -- Copyright : (c) The University of Glasgow, CWI 2001--2004
24 -- License : BSD-style (see the file libraries/base/LICENSE)
25 --
26 -- Maintainer : libraries@haskell.org
27 -- Stability : experimental
28 -- Portability : portable
29 --
30 -- The 'Typeable' class reifies types to some extent by associating type
31 -- representations to types. These type representations can be compared,
32 -- and one can in turn define a type-safe cast operation. To this end,
33 -- an unsafe cast is guarded by a test for type (representation)
34 -- equivalence. The module "Data.Dynamic" uses Typeable for an
35 -- implementation of dynamics. The module "Data.Data" uses Typeable
36 -- and type-safe cast (but not dynamics) to support the \"Scrap your
37 -- boilerplate\" style of generic programming.
38 --
39 -----------------------------------------------------------------------------
40
41 module Data.Typeable
42 (
43 -- * A proxy type
44 Proxy (..),
45
46 -- * The Typeable class
47 Typeable,
48 typeRep,
49
50 -- * Propositional equality
51 (:=:)(Refl),
52
53 -- * For backwards compatibility
54 typeOf, typeOf1, typeOf2, typeOf3, typeOf4, typeOf5, typeOf6, typeOf7,
55
56 -- * Type-safe cast
57 cast,
58 gcast, -- a generalisation of cast
59
60 -- * Generalized casts for higher-order kinds
61 gcast1, -- :: ... => c (t a) -> Maybe (c (t' a))
62 gcast2, -- :: ... => c (t a b) -> Maybe (c (t' a b))
63
64 -- * Type representations
65 TypeRep, -- abstract, instance of: Eq, Show, Typeable
66 showsTypeRep,
67
68 TyCon, -- abstract, instance of: Eq, Show, Typeable
69 tyConString,
70 tyConPackage,
71 tyConModule,
72 tyConName,
73
74 -- * Construction of type representations
75 -- mkTyCon, -- :: String -> TyCon
76 mkTyCon3, -- :: String -> String -> String -> TyCon
77 mkTyConApp, -- :: TyCon -> [TypeRep] -> TypeRep
78 mkAppTy, -- :: TypeRep -> TypeRep -> TypeRep
79 mkFunTy, -- :: TypeRep -> TypeRep -> TypeRep
80
81 -- * Observation of type representations
82 splitTyConApp, -- :: TypeRep -> (TyCon, [TypeRep])
83 funResultTy, -- :: TypeRep -> TypeRep -> Maybe TypeRep
84 typeRepTyCon, -- :: TypeRep -> TyCon
85 typeRepArgs, -- :: TypeRep -> [TypeRep]
86
87 -- * Type-level reasoning with Typeable
88 -- eqTypeable, decideEqTypeable
89 ) where
90
91 import Data.Typeable.Internal hiding (mkTyCon)
92 import Data.Type.Equality
93
94 import Unsafe.Coerce
95 import Data.Maybe
96 import GHC.Base
97
98 -------------------------------------------------------------
99 --
100 -- Type-safe cast
101 --
102 -------------------------------------------------------------
103
104 -- | The type-safe cast operation
105 cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b
106 cast x = if typeRep (Proxy :: Proxy a) == typeRep (Proxy :: Proxy b)
107 then Just $ unsafeCoerce x
108 else Nothing
109
110 -- | Extract a witness of equality of two types
111 eqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :=: b)
112 eqT = if typeRep (Proxy :: Proxy a) == typeRep (Proxy :: Proxy b)
113 then Just $ unsafeCoerce Refl
114 else Nothing
115
116 -- | A flexible variation parameterised in a type constructor
117 gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b)
118 gcast x = fmap (\Refl -> x) (eqT :: Maybe (a :=: b))
119
120 -- | Cast over @k1 -> k2@
121 gcast1 :: forall c t t' a. (Typeable t, Typeable t')
122 => c (t a) -> Maybe (c (t' a))
123 gcast1 x = fmap (\Refl -> x) (eqT :: Maybe (t :=: t'))
124
125 -- | Cast over @k1 -> k2 -> k3@
126 gcast2 :: forall c t t' a b. (Typeable t, Typeable t')
127 => c (t a b) -> Maybe (c (t' a b))
128 gcast2 x = fmap (\Refl -> x) (eqT :: Maybe (t :=: t'))
129