-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Type equality evidence you can carry around -- -- This package provides types and combinators to store and manipulate -- evidence of equality between types. -- -- To take advantage of kind polymorphism when it is available but not -- require it, it is split into the following primary modules: -- -- -- -- Major required extensions: GADTs, TypeFamilies (for -- ~), Rank2Types, TypeOperators -- -- Optional extensions: PolyKinds (GHC 7.6+) -- -- Minimum GHC: 6.10 -- -- Related packages: -- -- @package type-eq @version 0.2 -- | This module is kind-polymorphic if PolyKinds are available -- (GHC 7.6+). module Type.Eq.Unsafe -- | Very unsafe! The same rules apply as for unsafeCoerce. unsafeCoercion :: a :~: b -- | Very unsafe! unsafeOuterEq :: OuterEq f a -- | Very unsafe! unsafeInnerEq :: InnerEq i a module Type.Eq.Higher.Unsafe -- | Very unsafe! The same rules apply as for unsafeCoerce. unsafeCoercion1 :: f ::~:: g -- | Very unsafe! The same rules apply as for unsafeCoerce. unsafeCoercion2 :: m :::~::: n -- | Very unsafe! unsafeOuterEq1 :: OuterEq1 m f -- | Very unsafe! unsafeInnerEq1 :: InnerEq1 a f -- | Types and combinators for storing and manipulating type equality -- evidence. -- -- This module is kind-polymorphic if PolyKinds are available -- (GHC 7.6+). -- -- Notable combinators missing from this module include applyEq, -- constructorEq, and sameOuterEq. -- -- See also Type.Eq.Higher and -- Type.Eq.Poly. module Type.Eq -- | Evidence that type a is the same as type b. -- -- The Functor, Applicative, and -- Monad instances of Maybe are very useful for -- working with values of type Maybe (a :~: b). data (:~:) a b Eq :: a :~: b -- | Unpack equality evidence and use it. -- -- This function compiles with GHC 6.10, but doesn't work. withEq :: (a ~ b => r) -> (a :~: b) -> r -- | Reflexivity idEq :: a :~: a -- | Transitivity composeEq :: (b :~: c) -> (a :~: b) -> (a :~: c) -- | Symmetry flipEq :: (a :~: b) -> (b :~: a) -- | Type constructors are injective argumentEq :: (f a :~: g b) -> (a :~: b) -- | Use equality evidence to cast between types cast :: a -> (a :~: b) -> b -- | Use equality evidence to cast between types (|>) :: a -> (a :~: b) -> b -- | Evidence that f is the outermost type constructor of -- a data OuterEq f a OuterEq :: OuterEq f a -- | Evidence that i is the argument type of the outermost type -- constructor of a data InnerEq i a InnerEq :: InnerEq i a -- | Unpack partial equality evidence and use it. -- -- This function compiles with GHC 6.10, but doesn't work. withOuterEq :: (forall i. f i ~ a => r) -> OuterEq f a -> r -- | 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 -> r outerEq :: f i :~: a -> OuterEq f a innerEq :: f i :~: a -> InnerEq i a assembleEq :: OuterEq f a -> InnerEq i a -> f i :~: a sameInnerEq :: InnerEq i a -> InnerEq j a -> i :~: j -- | Runtime type equality evidence from Typeable dynamicEq :: (Typeable a, Typeable b) => Maybe (a :~: b) -- | 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: -- -- -- -- Due to http://hackage.haskell.org/trac/ghc/ticket/5591 you may -- have to use unsafeOuterEq and/or unsafeInnerEq to define -- some of these. class TypeCompare t where maybeEq = (~~) ~~ = maybeEq maybeOuterEq a b = fst (a <~> b) maybeInnerEq a b = snd (a <~> b) piecewiseMaybeEq a b = (a ~> b, a <~ b) ~> = maybeOuterEq <~ = maybeInnerEq <~> = piecewiseMaybeEq maybeEq, ~~ :: TypeCompare t => t a -> t b -> Maybe (a :~: b) maybeOuterEq, ~> :: TypeCompare t => t (f i) -> t a -> Maybe (OuterEq f a) maybeInnerEq, <~ :: TypeCompare t => t (f i) -> t a -> Maybe (InnerEq i a) piecewiseMaybeEq, <~> :: TypeCompare t => t (f i) -> t a -> (Maybe (OuterEq f a), Maybe (InnerEq i a)) instance TypeCompare k (OuterEq k k1 f) instance TypeCompare k (InnerEq k1 k i) instance TypeCompare k (k :~: a) instance Groupoid ((:~:) *) instance Semigroupoid ((:~:) *) instance Category ((:~:) *) instance Typeable2 ((:~:) *) -- | Types and combinators for storing and manipulating evidence of -- equality between types of higher kind. -- -- Available up to * -> * -> *. Yell if you need more. module Type.Eq.Higher -- | Type constructors are generative constructorEq :: f a :~: g b -> f ::~:: g sameOuterEq :: OuterEq f a -> OuterEq g a -> f ::~:: g data (::~::) (f :: * -> *) (g :: * -> *) Eq1 :: f ::~:: g withEq1 :: (f ~ g => r) -> (f ::~:: g) -> r -- | Reflexivity idEq1 :: f ::~:: f -- | Transitivity composeEq1 :: (g ::~:: h) -> (f ::~:: g) -> (f ::~:: h) -- | Transitivity (|.|) :: (g ::~:: h) -> (f ::~:: g) -> (f ::~:: h) -- | Symmetry flipEq1 :: (f ::~:: g) -> (g ::~:: f) -- | Congruence? applyEq1 :: f ::~:: g -> a :~: b -> f a :~: g b -- | Congruence? (|$|) :: f ::~:: g -> a :~: b -> f a :~: g b -- | Type constructors are generative constructorEq1 :: m a ::~:: n b -> m :::~::: n -- | Type constructors are injective argumentEq1 :: m a ::~:: n b -> a :~: b -- | Runtime type equality evidence from Typeable1 dynamicEq1 :: (Typeable1 f, Typeable1 g) => Maybe (f ::~:: g) data OuterEq1 (m :: * -> * -> *) (f :: * -> *) OuterEq1 :: OuterEq1 m f data InnerEq1 (a :: *) (f :: * -> *) InnerEq1 :: InnerEq1 a f 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 :: * -> * -> *) Eq2 :: m :::~::: n withEq2 :: (m ~ n => r) -> (m :::~::: n) -> r -- | Reflexivity idEq2 :: m :::~::: m -- | Transitivity composeEq2 :: (n :::~::: o) -> (m :::~::: n) -> (m :::~::: o) -- | Transitivity (||.||) :: (n :::~::: o) -> (m :::~::: n) -> (m :::~::: o) -- | Symmetry flipEq2 :: (m :::~::: n) -> (n :::~::: m) -- | Congruence? applyEq2 :: m :::~::: n -> a :~: b -> m a ::~:: n b -- | Congruence? (||$||) :: m :::~::: n -> a :~: b -> m a ::~:: n b -- | Runtime type equality evidence from Typeable2 dynamicEq2 :: (Typeable2 n, Typeable2 m) => Maybe (n :::~::: m) -- | Kind-polymorphic combinators for manipulating type equality evidence. -- -- This module is available only if PolyKinds are available (GHC -- 7.6+). module Type.Eq.Poly -- | Synonym for composeEq. Kind-polymorphic, unlike -- (.). (|.|) :: b :~: c -> a :~: b -> a :~: c -- | Congruence? applyEq :: f :~: g -> a :~: b -> f a :~: g b -- | Congruence? (|$|) :: f :~: g -> a :~: b -> f a :~: g b -- | Type constructors are generative constructorEq :: f a :~: g b -> f :~: g -- | Runtime type equality evidence from Typeable1 dynamicEq1 :: (Typeable1 f, Typeable1 g) => Maybe (f :~: g) -- | Runtime type equality evidence from Typeable2 dynamicEq2 :: (Typeable2 n, Typeable2 m) => Maybe (n :~: m) -- | Runtime type equality evidence from Typeable3 dynamicEq3 :: (Typeable3 x, Typeable3 y) => Maybe (x :~: y) -- | Runtime type equality evidence from Typeable4 dynamicEq4 :: (Typeable4 x, Typeable4 y) => Maybe (x :~: y) -- | Runtime type equality evidence from Typeable5 dynamicEq5 :: (Typeable5 x, Typeable5 y) => Maybe (x :~: y) -- | Runtime type equality evidence from Typeable6 dynamicEq6 :: (Typeable6 x, Typeable6 y) => Maybe (x :~: y) -- | Runtime type equality evidence from Typeable7 dynamicEq7 :: (Typeable7 x, Typeable7 y) => Maybe (x :~: y) sameOuterEq :: OuterEq f a -> OuterEq g a -> f :~: g fromEq1 :: f ::~:: g -> f :~: g toEq1 :: f :~: g -> f ::~:: g fromEq2 :: n :::~::: m -> n :~: m toEq2 :: n :~: m -> n :::~::: m fromOuterEq1 :: OuterEq1 m f -> OuterEq m f toOuterEq1 :: OuterEq m f -> OuterEq1 m f fromInnerEq1 :: InnerEq1 a f -> InnerEq a f toInnerEq1 :: InnerEq a f -> InnerEq1 a f