Safe Haskell | Trustworthy |
---|---|

Language | Haskell98 |

Types and functions for storing and manipulating type equality evidence.

This module is kind-polymorphic if `PolyKinds`

are available (GHC 7.6+).

Notable functions 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
- (|>) :: 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 TypeCompare t where

# Full equality

Evidence that `a`

is the same type as `b`

.

The

, `Functor`

, and `Applicative`

instances of `Monad`

`Maybe`

are very useful for working with values of type `Maybe (a :~: b)`

.

withEq :: ((a ~ b) => r) -> (a :~: b) -> r Source

Unpack equality evidence and use it.

This function compiles with GHC 6.10, but doesn't work.

argumentEq :: (f a :~: g b) -> a :~: b Source

Type constructors are injective

# Partial equality

Evidence that `f`

is the outermost type constructor of `a`

TypeCompare k (OuterEq k k f) | |

Typeable ((k -> k) -> k -> *) (OuterEq k k) |

Evidence that `i`

is the argument type of the outermost type constructor of `a`

TypeCompare k (InnerEq k k i) | |

Typeable (k -> k -> *) (InnerEq k k) |

withOuterEq :: (forall i. (f i ~ a) => r) -> OuterEq f a -> r Source

Unpack partial equality evidence and use it.

This function compiles with GHC 6.10, but doesn't work.

withInnerEq :: (forall f. (f i ~ a) => r) -> InnerEq i a -> r Source

Unpack partial equality evidence and use it.

This function compiles with GHC 6.10, but doesn't work.

assembleEq :: OuterEq f a -> InnerEq i a -> f i :~: a Source

sameInnerEq :: InnerEq i a -> InnerEq j a -> i :~: j Source

# Testing for equality

class TypeCompare t where Source

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`

and`maybeInnerEq`

. or `(<~>)`

, or- both
`(~>)`

and`(<~)`

.

Due to http://hackage.haskell.org/trac/ghc/ticket/5591 you may have to use `unsafeOuterEq`

and/or `unsafeInnerEq`

to define some of these.

Nothing

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

TypeCompare k ((:~:) k a) | |

TypeCompare k (OuterEq k k f) | |

TypeCompare k (InnerEq k k i) | |

Typeable ((k -> *) -> Constraint) (TypeCompare k) |