type-eq-0.2: Type equality evidence you can carry around

Type.Eq

Description

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`.

Synopsis

# Full equality

data a :~: b whereSource

Evidence that type `a` is the same as type `b`.

The `Functor`, `Applicative`, and `Monad` instances of `Maybe` are very useful for working with values of type `Maybe (a :~: b)`.

Constructors

 Eq :: a ~ b => a :~: b

Instances

 TypeCompare k (:~: k a) Typeable2 (:~: *) Category (:~: *) Groupoid (:~: *) Semigroupoid (:~: *)

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

Unpack equality evidence and use it.

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

idEq :: a :~: aSource

Reflexivity

composeEq :: (b :~: c) -> (a :~: b) -> a :~: cSource

Transitivity

flipEq :: (a :~: b) -> b :~: aSource

Symmetry

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

Type constructors are injective

cast :: a -> (a :~: b) -> bSource

Use equality evidence to cast between types

(|>) :: a -> (a :~: b) -> bSource

Use equality evidence to cast between types

# Partial equality

data OuterEq f a whereSource

Evidence that `f` is the outermost type constructor of `a`

Constructors

 OuterEq :: f i ~ a => OuterEq f a

Instances

 TypeCompare k (OuterEq k k1 f)

data InnerEq i a whereSource

Evidence that `i` is the argument type of the outermost type constructor of `a`

Constructors

 InnerEq :: f i ~ a => InnerEq i a

Instances

 TypeCompare k (InnerEq k1 k i)

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.

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.

outerEq :: (f i :~: a) -> OuterEq f aSource

innerEq :: (f i :~: a) -> InnerEq i aSource

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`

class TypeCompare t whereSource

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.

Methods

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
```

Instances

 TypeCompare k (:~: k a) TypeCompare k (OuterEq k k1 f) TypeCompare k (InnerEq k1 k i)