License | BSD-style (see the LICENSE file in the distribution) |
---|---|
Maintainer | libraries@haskell.org |
Stability | stable |
Portability | not portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Definition of representational equality (Coercion
).
Since: base-4.7.0.0
Synopsis
- data Coercion a b where
- coerceWith :: Coercion a b -> a -> b
- gcoerceWith :: Coercion a b -> (Coercible a b => r) -> r
- sym :: Coercion a b -> Coercion b a
- trans :: Coercion a b -> Coercion b c -> Coercion a c
- repr :: (a :~: b) -> Coercion a b
- class TestCoercion f where
- testCoercion :: f a -> f b -> Maybe (Coercion a b)
Documentation
data Coercion a b where Source #
Representational equality. If Coercion a b
is inhabited by some terminating
value, then the type a
has the same underlying representation as the type b
.
To use this equality in practice, pattern-match on the Coercion a b
to get out
the Coercible a b
instance, and then use coerce
to apply it.
Since: base-4.7.0.0
Instances
Category (Coercion :: k -> k -> Type) Source # | Since: base-4.7.0.0 |
TestCoercion (Coercion a :: k -> Type) Source # | Since: base-4.7.0.0 |
Defined in Data.Type.Coercion | |
(Coercible a b, Data a, Data b) => Data (Coercion a b) Source # | Since: base-4.7.0.0 |
Defined in Data.Data gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Coercion a b -> c (Coercion a b) Source # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Coercion a b) Source # toConstr :: Coercion a b -> Constr Source # dataTypeOf :: Coercion a b -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Coercion a b)) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Coercion a b)) Source # gmapT :: (forall b0. Data b0 => b0 -> b0) -> Coercion a b -> Coercion a b Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Coercion a b -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Coercion a b -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Coercion a b -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Coercion a b -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Coercion a b -> m (Coercion a b) Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion a b -> m (Coercion a b) Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion a b -> m (Coercion a b) Source # | |
Coercible a b => Bounded (Coercion a b) Source # | Since: base-4.7.0.0 |
Coercible a b => Enum (Coercion a b) Source # | Since: base-4.7.0.0 |
Defined in Data.Type.Coercion succ :: Coercion a b -> Coercion a b Source # pred :: Coercion a b -> Coercion a b Source # toEnum :: Int -> Coercion a b Source # fromEnum :: Coercion a b -> Int Source # enumFrom :: Coercion a b -> [Coercion a b] Source # enumFromThen :: Coercion a b -> Coercion a b -> [Coercion a b] Source # enumFromTo :: Coercion a b -> Coercion a b -> [Coercion a b] Source # enumFromThenTo :: Coercion a b -> Coercion a b -> Coercion a b -> [Coercion a b] Source # | |
Coercible a b => Read (Coercion a b) Source # | Since: base-4.7.0.0 |
Show (Coercion a b) Source # | Since: base-4.7.0.0 |
Eq (Coercion a b) Source # | Since: base-4.7.0.0 |
Ord (Coercion a b) Source # | Since: base-4.7.0.0 |
Defined in Data.Type.Coercion compare :: Coercion a b -> Coercion a b -> Ordering Source # (<) :: Coercion a b -> Coercion a b -> Bool Source # (<=) :: Coercion a b -> Coercion a b -> Bool Source # (>) :: Coercion a b -> Coercion a b -> Bool Source # (>=) :: Coercion a b -> Coercion a b -> Bool Source # max :: Coercion a b -> Coercion a b -> Coercion a b Source # min :: Coercion a b -> Coercion a b -> Coercion a b Source # |
coerceWith :: Coercion a b -> a -> b Source #
Type-safe cast, using representational equality
gcoerceWith :: Coercion a b -> (Coercible a b => r) -> r Source #
Generalized form of type-safe cast using representational equality
Since: base-4.10.0.0
trans :: Coercion a b -> Coercion b c -> Coercion a c Source #
Transitivity of representational equality
repr :: (a :~: b) -> Coercion a b Source #
Convert propositional (nominal) equality to representational equality
class TestCoercion f where Source #
This class contains types where you can learn the equality of two types from information contained in terms. Typically, only singleton types should inhabit this class.
testCoercion :: f a -> f b -> Maybe (Coercion a b) Source #
Conditionally prove the representational equality of a
and b
.
Instances
TestCoercion (Coercion a :: k -> Type) Source # | Since: base-4.7.0.0 |
Defined in Data.Type.Coercion | |
TestCoercion ((:~:) a :: k -> Type) Source # | Since: base-4.7.0.0 |
Defined in Data.Type.Coercion | |
TestCoercion ((:~~:) a :: k -> Type) Source # | Since: base-4.10.0.0 |
Defined in Data.Type.Coercion |