-- 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: -- -- -- -- Support for kind-polymorphism first appeared with GHC 7.4, but because -- it is too buggy to be practical, it will only be enabled with GHC 7.6. -- -- 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.1.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 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 -- | 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 extremely 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. Beware! 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 -- | 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. Beware! 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. Beware! 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: -- -- class TypeEq 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, ~~ :: TypeEq t => t a -> t b -> Maybe (a :~: b) maybeOuterEq, ~> :: TypeEq t => t (f i) -> t a -> Maybe (OuterEq f a) maybeInnerEq, <~ :: TypeEq t => t (f i) -> t a -> Maybe (InnerEq i a) piecewiseMaybeEq, <~> :: TypeEq t => t (f i) -> t a -> (Maybe (OuterEq f a), Maybe (InnerEq i a)) instance TypeEq (OuterEq f) instance TypeEq (InnerEq i) instance TypeEq ((:~:) 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) -- | Symmetry flipEq1 :: (f ::~:: g) -> (g ::~:: f) -- | Congruence? applyEq1, |$| :: 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) -- | Symmetry flipEq2 :: (m :::~::: n) -> (n :::~::: m) -- | Congruence? applyEq2, ||$|| :: m :::~::: n -> a :~: b -> m a ::~:: n b -- | Runtime type equality evidence from Typeable2 dynamicEq2 :: (Typeable2 n, Typeable2 m) => Maybe (n :::~::: m)