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

Safe HaskellTrustworthy

Type.Eq

Contents

Description

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.

Synopsis

Full equality

data a :~: b whereSource

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

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

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

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)