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

Type.Eq.Higher

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

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`