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

Safe HaskellTrustworthy
LanguageHaskell98

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 ::~:: g Source

Type constructors are generative

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

Full equality, kind * -> *

data f ::~:: g where Source

Constructors

Eq1 :: (f ~ g) => f ::~:: g 

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

idEq1 :: f ::~:: f Source

Reflexivity

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

Transitivity

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

Transitivity

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

Symmetry

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

Congruence?

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

Congruence?

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

Type constructors are generative

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

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 where Source

Constructors

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

data InnerEq1 a f where Source

Constructors

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

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

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

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

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

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

sameInnerEq1 :: InnerEq1 a f -> InnerEq1 b f -> a :~: b Source

Full equality, kind * -> * -> *

data m :::~::: n where Source

Constructors

Eq2 :: (m ~ n) => m :::~::: n 

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

idEq2 :: m :::~::: m Source

Reflexivity

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

Transitivity

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

Transitivity

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

Symmetry

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

Congruence?

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

Congruence?

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

Runtime type equality evidence from Typeable2