Type.Eq

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.

Full equality

data a :~: b where

Evidence that a is the same type as 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

Category k ((:~:) k)

TypeCompare k ((:~:) k a)

Typeable (k -> k -> *) ((:~:) k)

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

Unpack equality evidence and use it.

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

idEq :: a :~: a

Reflexivity

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

Transitivity

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

Symmetry

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

Type constructors are injective

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

Use equality evidence to cast between types

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

Use equality evidence to cast between types

Partial equality

data OuterEq f a where

Evidence that f is the outermost type constructor of a

Constructors

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

Instances

TypeCompare k (OuterEq k k f)

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

data InnerEq i a where

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 k k i)

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

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

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

Unpack partial equality evidence and use it.

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

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

Testing for equality

dynamicEq :: (Typeable a, Typeable b) => Maybe (a :~: b)

class TypeCompare t where

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.

Minimal complete definition

Nothing

Methods

maybeEq, (~~) :: t a -> t b -> Maybe (a :~: b)

maybeOuterEq, (~>) :: t (f i) -> t a -> Maybe (OuterEq f a)

maybeInnerEq, (<~) :: t (f i) -> t a -> Maybe (InnerEq i a)

piecewiseMaybeEq, (<~>) :: t (f i) -> t a -> (Maybe (OuterEq f a), Maybe (InnerEq i a))

uncurry (liftA2 assembleEq) (a <~> b) = a ~~ b

Instances

TypeCompare k ((:~:) k a)

TypeCompare k (OuterEq k k f)

TypeCompare k (InnerEq k k i)

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