License | BSD-style (see the LICENSE file in the distribution) |
---|---|
Maintainer | [email protected] |
Stability | experimental |
Portability | not portable |
Safe Haskell | None |
Language | Haskell2010 |
Definition of representational equality (Coercion
).
Since: 4.7.0.0
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: 4.7.0.0
Category k (Coercion k) # | |
TestCoercion k (Coercion k a) # | |
Coercible k a b => Bounded (Coercion k a b) # | |
Coercible k a b => Enum (Coercion k a b) # | |
Eq (Coercion k a b) # | |
(Coercible * a b, Data a, Data b) => Data (Coercion * a b) # | |
Ord (Coercion k a b) # | |
Coercible k a b => Read (Coercion k a b) # | |
Show (Coercion k a b) # | |
coerceWith :: Coercion a b -> a -> b Source #
Type-safe cast, using representational equality
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
.
TestCoercion k (Coercion k a) # | |
TestCoercion k ((:~:) k a) # | |