Safe Haskell | Trustworthy |
---|
Types and combinators for storing and manipulating type equality evidence.
This module is kind-polymorphic if PolyKinds
are available (GHC 7.6+).
Notable combinators missing from this module include applyEq
, constructorEq
, and sameOuterEq
.
See also Type.Eq.Higher
and Type.Eq.Poly
.
- data a :~: b where
- withEq :: (a ~ b => r) -> (a :~: b) -> r
- idEq :: a :~: a
- composeEq :: (b :~: c) -> (a :~: b) -> a :~: c
- flipEq :: (a :~: b) -> b :~: a
- argumentEq :: (f a :~: g b) -> a :~: b
- cast, (|>) :: a -> (a :~: b) -> b
- data OuterEq f a where
- data InnerEq i a where
- withOuterEq :: (forall i. f i ~ a => r) -> OuterEq f a -> r
- withInnerEq :: (forall f. f i ~ a => r) -> InnerEq i a -> r
- outerEq :: (f i :~: a) -> OuterEq f a
- innerEq :: (f i :~: a) -> InnerEq i a
- assembleEq :: OuterEq f a -> InnerEq i a -> f i :~: a
- sameInnerEq :: InnerEq i a -> InnerEq j a -> i :~: j
- dynamicEq :: (Typeable a, Typeable b) => Maybe (a :~: b)
- class TypeEq t where
Full equality
Evidence that type a
is the same as type b
.
The
, Functor
, and Applicative
instances of Monad
Maybe
are extremely useful for working with values of type Maybe (a :~: b)
.
withEq :: (a ~ b => r) -> (a :~: b) -> rSource
Unpack equality evidence and use it.
This function compiles with GHC 6.10, but doesn't work. Beware!
argumentEq :: (f a :~: g b) -> a :~: bSource
Type constructors are injective
Partial equality
Evidence that f
is the outermost type constructor of a
Evidence that i
is the argument type of the outermost type constructor of a
withOuterEq :: (forall i. f i ~ a => r) -> OuterEq f a -> rSource
Unpack partial equality evidence and use it.
This function compiles with GHC 6.10, but doesn't work. Beware!
withInnerEq :: (forall f. f i ~ a => r) -> InnerEq i a -> rSource
Unpack partial equality evidence and use it.
This function compiles with GHC 6.10, but doesn't work. Beware!
assembleEq :: OuterEq f a -> InnerEq i a -> f i :~: aSource
sameInnerEq :: InnerEq i a -> InnerEq j a -> i :~: jSource
Testing for equality
dynamicEq :: (Typeable a, Typeable b) => Maybe (a :~: b)Source
Runtime type equality evidence from Typeable
Can be implemented by types storing evidence of type equalities, i.e. GADTs.
A return value of Nothing
can mean any of definite inequality, impossible arguments, or insufficient information.
Minimal complete definition: maybeEq
or (~~)
, plus either:
-
piecewiseMaybeEq
, or - both
maybeOuterEq
andmaybeInnerEq
. or -
(<~>)
, or - both
(~>)
and(<~)
.
maybeEq, (~~) :: t a -> t b -> Maybe (a :~: b)Source
maybeOuterEq, (~>) :: t (f i) -> t a -> Maybe (OuterEq f a)Source
maybeInnerEq, (<~) :: t (f i) -> t a -> Maybe (InnerEq i a)Source
piecewiseMaybeEq, (<~>) :: t (f i) -> t a -> (Maybe (OuterEq f a), Maybe (InnerEq i a))Source
uncurry (liftA2 assembleEq) (a <~> b) = a ~~ b