License | BSD-style (see the LICENSE file in the distribution) |
---|---|
Maintainer | libraries@haskell.org |
Stability | experimental |
Portability | not portable |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
Definition of propositional equality (:~:)
. Pattern-matching on a variable
of type (a :~: b)
produces a proof that a ~ b
.
Since: 4.7.0.0
Synopsis
- data a :~: b where
- class a ~# b => (a :: k0) ~~ (b :: k1)
- data (a :: k1) :~~: (b :: k2) where
- sym :: (a :~: b) -> b :~: a
- trans :: (a :~: b) -> (b :~: c) -> a :~: c
- castWith :: (a :~: b) -> a -> b
- gcastWith :: (a :~: b) -> (a ~ b => r) -> r
- apply :: (f :~: g) -> (a :~: b) -> f a :~: g b
- inner :: (f a :~: g b) -> a :~: b
- outer :: (f a :~: g b) -> f :~: g
- class TestEquality f where
- testEquality :: f a -> f b -> Maybe (a :~: b)
- type family (a :: k) == (b :: k) :: Bool where ...
The equality types
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: 4.7.0.0
Instances
Category ((:~:) :: k -> k -> Type) Source # | Since: 4.7.0.0 |
TestEquality ((:~:) a :: k -> Type) Source # | Since: 4.7.0.0 |
Defined in Data.Type.Equality | |
TestCoercion ((:~:) a :: k -> Type) Source # | Since: 4.7.0.0 |
Defined in Data.Type.Coercion | |
a ~ b => Bounded (a :~: b) Source # | Since: 4.7.0.0 |
a ~ b => Enum (a :~: b) Source # | Since: 4.7.0.0 |
Defined in Data.Type.Equality succ :: (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) Source # | Since: 4.7.0.0 |
(a ~ b, Data a) => Data (a :~: b) Source # | Since: 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) -> (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 :: (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) Source # | Since: 4.7.0.0 |
Defined in Data.Type.Equality | |
a ~ b => Read (a :~: b) Source # | Since: 4.7.0.0 |
Show (a :~: b) Source # | Since: 4.7.0.0 |
class a ~# b => (a :: k0) ~~ (b :: k1) Source #
Lifted, heterogeneous equality. By lifted, we mean that it
can be bogus (deferred type error). By heterogeneous, the two
types a
and b
might have different kinds. Because ~~
can
appear unexpectedly in error messages to users who do not care
about the difference between heterogeneous equality ~~
and
homogeneous equality ~
, this is printed as ~
unless
-fprint-equality-relations
is set.
data (a :: k1) :~~: (b :: k2) 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: 4.10.0.0
Instances
Category ((:~~:) :: k -> k -> Type) Source # | Since: 4.10.0.0 |
TestEquality ((:~~:) a :: k -> Type) Source # | Since: 4.10.0.0 |
Defined in Data.Type.Equality | |
TestCoercion ((:~~:) a :: k -> Type) Source # | Since: 4.10.0.0 |
Defined in Data.Type.Coercion | |
a ~~ b => Bounded (a :~~: b) Source # | Since: 4.10.0.0 |
a ~~ b => Enum (a :~~: b) Source # | Since: 4.10.0.0 |
Defined in Data.Type.Equality succ :: (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) Source # | Since: 4.10.0.0 |
(Typeable i, Typeable j, Typeable a, Typeable b, a ~~ b) => Data (a :~~: b) Source # | Since: 4.10.0.0 |
Defined in Data.Data gfoldl :: (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 :: (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) Source # | Since: 4.10.0.0 |
Defined in Data.Type.Equality compare :: (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) Source # | Since: 4.10.0.0 |
Show (a :~~: b) Source # | Since: 4.10.0.0 |
Working with equality
gcastWith :: (a :~: b) -> (a ~ b => r) -> r Source #
Generalized form of type-safe cast using propositional equality
inner :: (f a :~: g b) -> a :~: b Source #
Extract equality of the arguments from an equality of applied types
outer :: (f a :~: g b) -> f :~: g Source #
Extract equality of type constructors from an equality of applied types
Inferring equality from other types
class TestEquality 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.
testEquality :: f a -> f b -> Maybe (a :~: b) Source #
Conditionally prove the equality of a
and b
.
Instances
TestEquality (TypeRep :: k -> Type) Source # | |
Defined in Data.Typeable.Internal | |
TestEquality ((:~:) a :: k -> Type) Source # | Since: 4.7.0.0 |
Defined in Data.Type.Equality | |
TestEquality ((:~~:) a :: k -> Type) Source # | Since: 4.10.0.0 |
Defined in Data.Type.Equality |