Data.Type.Coercion

base-4.11.1.0: Basic libraries

License | BSD-style (see the LICENSE file in the distribution)
Maintainer | libraries@haskell.org
Stability | experimental
Portability | not portable
Safe Haskell | None
Language | Haskell2010

Data.Type.Coercion

Description

Definition of representational equality (`Coercion`).

Since: base-4.7.0.0

Synopsis

- data Coercion a b where
  - Coercion :: Coercible a b => Coercion a b
- 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

# Documentation

data Coercion a b where #

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

Constructors

Coercion :: Coercible a b => Coercion a b |

Instances

Category (Coercion :: k -> k -> *) # | Since: base-4.7.0.0
Instance details Defined in Control.Category Methods id :: Coercion a a # (.) :: Coercion b c -> Coercion a b -> Coercion a c #
TestCoercion (Coercion a :: k -> *) # | Since: base-4.7.0.0
Instance details Defined in Data.Type.Coercion Methods testCoercion :: Coercion a a0 -> Coercion a b -> Maybe (Coercion a0 b) #
Coercible a b => Bounded (Coercion a b) # | Since: base-4.7.0.0
Instance details Defined in Data.Type.Coercion Methods minBound :: Coercion a b # maxBound :: Coercion a b #
Coercible a b => Enum (Coercion a b) # | Since: base-4.7.0.0
Instance details Defined in Data.Type.Coercion Methods succ :: Coercion a b -> Coercion a b # pred :: Coercion a b -> Coercion a b # toEnum :: Int -> Coercion a b # fromEnum :: Coercion a b -> Int # enumFrom :: Coercion a b -> [Coercion a b] # enumFromThen :: Coercion a b -> Coercion a b -> [Coercion a b] # enumFromTo :: Coercion a b -> Coercion a b -> [Coercion a b] # enumFromThenTo :: Coercion a b -> Coercion a b -> Coercion a b -> [Coercion a b] #
Eq (Coercion a b) # |
Instance details Defined in Data.Type.Coercion Methods (==) :: Coercion a b -> Coercion a b -> Bool Source # (/=) :: Coercion a b -> Coercion a b -> Bool Source #
(Coercible a b, Data a, Data b) => Data (Coercion a b) # | Since: base-4.7.0.0
Instance details Defined in Data.Data Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Coercion a b -> c (Coercion a b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Coercion a b) # toConstr :: Coercion a b -> Constr # dataTypeOf :: Coercion a b -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Coercion a b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Coercion a b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> Coercion a b -> Coercion a b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Coercion a b -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Coercion a b -> r # gmapQ :: (forall d. Data d => d -> u) -> Coercion a b -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Coercion a b -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Coercion a b -> m (Coercion a b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion a b -> m (Coercion a b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion a b -> m (Coercion a b) #
Ord (Coercion a b) # |
Instance details Defined in Data.Type.Coercion Methods 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 #
Coercible a b => Read (Coercion a b) # | Since: base-4.7.0.0
Instance details Defined in Data.Type.Coercion Methods readsPrec :: Int -> ReadS (Coercion a b) # readList :: ReadS [Coercion a b] # readPrec :: ReadPrec (Coercion a b) # readListPrec :: ReadPrec [Coercion a b] #
Show (Coercion a b) # |
Instance details Defined in Data.Type.Coercion Methods showsPrec :: Int -> Coercion a b -> ShowS # show :: Coercion a b -> String # showList :: [Coercion a b] -> ShowS #

coerceWith :: Coercion a b -> a -> b #

Type-safe cast, using representational equality

gcoerceWith :: Coercion a b -> (Coercible a b => r) -> r #

Generalized form of type-safe cast using representational equality

Since: base-4.10.0.0

sym :: Coercion a b -> Coercion b a #

Symmetry of representational equality

trans :: Coercion a b -> Coercion b c -> Coercion a c #

Transitivity of representational equality

repr :: (a :~: b) -> Coercion a b #

Convert propositional (nominal) equality to representational equality

class TestCoercion f where #

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.

Minimal complete definition

testCoercion

Methods

testCoercion :: f a -> f b -> Maybe (Coercion a b) #

Conditionally prove the representational equality of `a` and `b`.

Instances

TestCoercion (Coercion a :: k -> *) # | Since: base-4.7.0.0
Instance details Defined in Data.Type.Coercion Methods testCoercion :: Coercion a a0 -> Coercion a b -> Maybe (Coercion a0 b) #
TestCoercion ((:~:) a :: k -> *) # | Since: base-4.7.0.0
Instance details Defined in Data.Type.Coercion Methods testCoercion :: (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) #
TestCoercion ((:~~:) a :: k -> *) # | Since: base-4.10.0.0
Instance details Defined in Data.Type.Coercion Methods testCoercion :: (a :~~: a0) -> (a :~~: b) -> Maybe (Coercion a0 b) #