Safe Haskell | Trustworthy |
---|
Types and functions for storing and manipulating evidence of equality between types of higher kind.
Available up to * -> * -> *
. Yell if you need more.
In GHC 7.8, this module uses Data.OldTypeable
. Future uncertain.
- module Type.Eq
- constructorEq :: (f a :~: g b) -> f ::~:: g
- sameOuterEq :: OuterEq f a -> OuterEq g a -> f ::~:: g
- data f ::~:: g where
- withEq1 :: (f ~ g => r) -> (f ::~:: g) -> r
- idEq1 :: f ::~:: f
- composeEq1 :: (g ::~:: h) -> (f ::~:: g) -> f ::~:: h
- (|.|) :: (g ::~:: h) -> (f ::~:: g) -> f ::~:: h
- flipEq1 :: (f ::~:: g) -> g ::~:: f
- applyEq1 :: (f ::~:: g) -> (a :~: b) -> f a :~: g b
- (|$|) :: (f ::~:: g) -> (a :~: b) -> f a :~: g b
- constructorEq1 :: (m a ::~:: n b) -> m :::~::: n
- argumentEq1 :: (m a ::~:: n b) -> a :~: b
- dynamicEq1 :: (Typeable1 f, Typeable1 g) => Maybe (f ::~:: g)
- data OuterEq1 m f where
- data InnerEq1 a f where
- withOuterEq1 :: (forall a. m a ~ f => r) -> OuterEq1 m f -> r
- withInnerEq1 :: (forall m. m a ~ f => r) -> InnerEq1 a f -> r
- outerEq1 :: (m a ::~:: f) -> OuterEq1 m f
- innerEq1 :: (m a ::~:: f) -> InnerEq1 a f
- assembleEq1 :: OuterEq1 m f -> InnerEq1 a f -> m a ::~:: f
- sameOuterEq1 :: OuterEq1 m f -> OuterEq1 n f -> m :::~::: n
- sameInnerEq1 :: InnerEq1 a f -> InnerEq1 b f -> a :~: b
- data m :::~::: n where
- withEq2 :: (m ~ n => r) -> (m :::~::: n) -> r
- idEq2 :: m :::~::: m
- composeEq2 :: (n :::~::: o) -> (m :::~::: n) -> m :::~::: o
- (||.||) :: (n :::~::: o) -> (m :::~::: n) -> m :::~::: o
- flipEq2 :: (m :::~::: n) -> n :::~::: m
- applyEq2 :: (m :::~::: n) -> (a :~: b) -> m a ::~:: n b
- (||$||) :: (m :::~::: n) -> (a :~: b) -> m a ::~:: n b
- dynamicEq2 :: (Typeable2 n, Typeable2 m) => Maybe (n :::~::: m)
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 * -> *
composeEq1 :: (g ::~:: h) -> (f ::~:: g) -> f ::~:: hSource
Transitivity
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 * -> *
withOuterEq1 :: (forall a. m a ~ f => r) -> OuterEq1 m f -> rSource
withInnerEq1 :: (forall m. m a ~ f => r) -> InnerEq1 a f -> rSource
assembleEq1 :: OuterEq1 m f -> InnerEq1 a f -> m a ::~:: fSource
sameOuterEq1 :: OuterEq1 m f -> OuterEq1 n f -> m :::~::: nSource
sameInnerEq1 :: InnerEq1 a f -> InnerEq1 b f -> a :~: bSource
Full equality, kind * -> * -> *
composeEq2 :: (n :::~::: o) -> (m :::~::: n) -> m :::~::: oSource
Transitivity