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

Safe HaskellTrustworthy

Type.Eq

Contents

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 extremely useful for working with values of type Maybe (a :~: b).

Constructors

Eq :: a ~ b => 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!

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

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

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

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!

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 TypeEq 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 (<~).

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