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

Safe HaskellTrustworthy

Type.Eq.Higher

Contents

Description

Types and functions for storing and manipulating evidence of equality between types of higher kind.

Available up to * -> * -> *. Yell if you need more.

Synopsis

Documentation

module Type.Eq

Additional functions, kind *

constructorEq :: (f a :~: g b) -> f ::~:: gSource

Type constructors are generative

sameOuterEq :: OuterEq f a -> OuterEq g a -> f ::~:: gSource

Full equality, kind * -> *

data f ::~:: g whereSource

Constructors

Eq1 :: f ~ g => f ::~:: g 

withEq1 :: (f ~ g => r) -> (f ::~:: g) -> rSource

idEq1 :: f ::~:: fSource

Reflexivity

composeEq1 :: (g ::~:: h) -> (f ::~:: g) -> f ::~:: hSource

Transitivity

(|.|) :: (g ::~:: h) -> (f ::~:: g) -> f ::~:: hSource

Transitivity

flipEq1 :: (f ::~:: g) -> g ::~:: fSource

Symmetry

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

Congruence?

(|$|) :: (f ::~:: g) -> (a :~: b) -> f a :~: g bSource

Congruence?

constructorEq1 :: (m a ::~:: n b) -> m :::~::: nSource

Type constructors are generative

argumentEq1 :: (m a ::~:: n b) -> a :~: bSource

Type constructors are injective

dynamicEq1 :: (Typeable1 f, Typeable1 g) => Maybe (f ::~:: g)Source

Runtime type equality evidence from Typeable1

Partial equality, kind * -> *

data OuterEq1 m f whereSource

Constructors

OuterEq1 :: m a ~ f => OuterEq1 m f 

data InnerEq1 a f whereSource

Constructors

InnerEq1 :: m a ~ f => InnerEq1 a f 

withOuterEq1 :: (forall a. m a ~ f => r) -> OuterEq1 m f -> rSource

withInnerEq1 :: (forall m. m a ~ f => r) -> InnerEq1 a f -> rSource

outerEq1 :: (m a ::~:: f) -> OuterEq1 m fSource

innerEq1 :: (m a ::~:: f) -> InnerEq1 a fSource

assembleEq1 :: OuterEq1 m f -> InnerEq1 a f -> m a ::~:: fSource

Full equality, kind * -> * -> *

data m :::~::: n whereSource

Constructors

Eq2 :: m ~ n => m :::~::: n 

withEq2 :: (m ~ n => r) -> (m :::~::: n) -> rSource

idEq2 :: m :::~::: mSource

Reflexivity

composeEq2 :: (n :::~::: o) -> (m :::~::: n) -> m :::~::: oSource

Transitivity

(||.||) :: (n :::~::: o) -> (m :::~::: n) -> m :::~::: oSource

Transitivity

flipEq2 :: (m :::~::: n) -> n :::~::: mSource

Symmetry

applyEq2 :: (m :::~::: n) -> (a :~: b) -> m a ::~:: n bSource

Congruence?

(||$||) :: (m :::~::: n) -> (a :~: b) -> m a ::~:: n bSource

Congruence?

dynamicEq2 :: (Typeable2 n, Typeable2 m) => Maybe (n :::~::: m)Source

Runtime type equality evidence from Typeable2