Safe Haskell	None
Language	Haskell2010

Data.Type.Index.Trans

Synopsis

Documentation

type IxList' = IxList (:~:) Source #

type IxEnv = IxList (IxFirst (:~:)) Source #

class IxLift t x where Source #

Minimal complete definition

ixLift

Associated Types

type LiftI t x :: k Source #

Methods

ixLift :: i (LiftI t x) y -> t i x y Source #

Instances

(~) (m1, k) p ((,) m1 k (Fst m1 k p) (Snd m1 k p)) => IxLift (m1, k) m k (IxSecond m1 m k) p Source #
Associated Types type LiftI (IxSecond m1 m k) p k (t :: (k -> p -> ) -> IxSecond m1 m k -> p -> ) (x :: IxSecond m1 m k) :: k Source # Methods ixLift :: i (LiftI (IxSecond m1 m k) p k t x) y -> t i x y Source #
(~) (k, m1) p ((,) k m1 (Fst k m1 p) (Snd k m1 p)) => IxLift (k, m1) m k (IxFirst m1 m k) p Source #
Associated Types type LiftI (IxFirst m1 m k) p k (t :: (k -> p -> ) -> IxFirst m1 m k -> p -> ) (x :: IxFirst m1 m k) :: k Source # Methods ixLift :: i (LiftI (IxFirst m1 m k) p k t x) y -> t i x y Source #
IxLift (Either k1 k) m k (IxOr k m k1 i) (Right k1 k a) Source #
Associated Types type LiftI (IxOr k m k1 i) (Right k1 k a) k (t :: (k -> Right k1 k a -> ) -> IxOr k m k1 i -> Right k1 k a -> ) (x :: IxOr k m k1 i) :: k Source # Methods ixLift :: i (LiftI (IxOr k m k1 i) (Right k1 k a) k t x) y -> t i x y Source #

data IxList i :: [k] -> l -> * where Source #

Constructors

IxHead :: !(i a b) -> IxList i (a :< as) b
IxTail :: !(IxList i as b) -> IxList i (a :< as) b

Instances

IxFunctor1 k [(m, k)] (IxList k (m, k) (IxSecond m k k ((:~:) k))) (Env k m k1) Source #
Methods imap1 :: (forall a. i b a -> f a -> g a) -> t f b -> t g b Source #

data IxFirst i :: (k, m) -> l -> * where Source #

Constructors

IxFirst :: !(i a b) -> IxFirst i '(a, c) b

Instances

(~) (k, m1) p ((,) k m1 (Fst k m1 p) (Snd k m1 p)) => IxLift (k, m1) m k (IxFirst m1 m k) p Source #
Associated Types type LiftI (IxFirst m1 m k) p k (t :: (k -> p -> ) -> IxFirst m1 m k -> p -> ) (x :: IxFirst m1 m k) :: k Source # Methods ixLift :: i (LiftI (IxFirst m1 m k) p k t x) y -> t i x y Source #
type LiftI (k, m1) m k (IxFirst m1 m k) p Source #
type LiftI (k, m1) m k (IxFirst m1 m k) p = Fst k m1 p

data IxSecond i :: (m, k) -> l -> * where Source #

Constructors

IxSecond :: !(i a b) -> IxSecond i '(c, a) b

Instances

IxFunctor1 k [(m, k)] (IxList k (m, k) (IxSecond m k k ((:~:) k))) (Env k m k1) Source #
Methods imap1 :: (forall a. i b a -> f a -> g a) -> t f b -> t g b Source #
IxFunctor1 k (m, k) (IxSecond m k k ((:~:) k)) ((:*:) k m f) Source #
Methods imap1 :: (forall a. i b a -> f a -> g a) -> t f b -> t g b Source #
(~) (m1, k) p ((,) m1 k (Fst m1 k p) (Snd m1 k p)) => IxLift (m1, k) m k (IxSecond m1 m k) p Source #
Associated Types type LiftI (IxSecond m1 m k) p k (t :: (k -> p -> ) -> IxSecond m1 m k -> p -> ) (x :: IxSecond m1 m k) :: k Source # Methods ixLift :: i (LiftI (IxSecond m1 m k) p k t x) y -> t i x y Source #
type LiftI (m1, k) m k (IxSecond m1 m k) p Source #
type LiftI (m1, k) m k (IxSecond m1 m k) p = Snd m1 k p

data IxOr i j :: Either k l -> m -> * where Source #

Constructors

IxOrL :: !(i a b) -> IxOr i j (Left a) b
IxOrR :: !(j a b) -> IxOr i j (Right a) b

Instances

IxLift (Either k1 k) m k (IxOr k m k1 i) (Right k1 k a) Source #
Associated Types type LiftI (IxOr k m k1 i) (Right k1 k a) k (t :: (k -> Right k1 k a -> ) -> IxOr k m k1 i -> Right k1 k a -> ) (x :: IxOr k m k1 i) :: k Source # Methods ixLift :: i (LiftI (IxOr k m k1 i) (Right k1 k a) k t x) y -> t i x y Source #
type LiftI (Either k1 k) m k (IxOr k m k1 i) (Right k1 k a) Source #
type LiftI (Either k1 k) m k (IxOr k m k1 i) (Right k1 k a) = a

data IxJust i :: Maybe k -> l -> * where Source #

Constructors

IxJust :: !(i a b) -> IxJust i (Just a) b

data IxComp i j :: k -> m -> * where Source #

Constructors

IxComp :: !(i a b) -> !(j b c) -> IxComp i j a c

data (k :~: a) b :: forall k. k -> k -> * where infix 4 #

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: 4.7.0.0

Constructors

Refl :: (:~:) k a a

Instances

Category k ((:~:) k)
Methods id :: cat a a # (.) :: cat b c -> cat a b -> cat a c #
IxFunctor1 k [(m, k)] (IxList k (m, k) (IxSecond m k k ((:~:) k))) (Env k m k1) Source #
Methods imap1 :: (forall a. i b a -> f a -> g a) -> t f b -> t g b Source #
TestCoercion k ((:~:) k a)
Methods testCoercion :: f a -> f b -> Maybe (Coercion (k :~: a) a b) #
TestEquality k ((:~:) k a)
Methods testEquality :: f a -> f b -> Maybe (((k :~: a) :~: a) b) #
(~) k a b => Known k ((:~:) k a) b Source #
Associated Types type KnownC ((:~:) k a) (b :: (:~:) k a -> *) (a :: (:~:) k a) :: Constraint Source # Methods known :: b a Source #
IxFunctor1 k (m, k) (IxSecond m k k ((:~:) k)) ((:*:) k m f) Source #
Methods imap1 :: (forall a. i b a -> f a -> g a) -> t f b -> t g b Source #
Witness ØC ((~) k a b) ((:~:) k a b) Source #	A type equality `a :~: b` is a Witness that `(a ~ b)`.
Associated Types type WitnessC (ØC :: Constraint) ((~) k a b :: Constraint) ((:~:) k a b) :: Constraint Source # Methods (\\) :: ØC => ((k ~ a) b -> r) -> (k :~: a) b -> r Source #
(~) k a b => Bounded ((:~:) k a b)
Methods minBound :: (k :~: a) b # maxBound :: (k :~: a) b #
(~) k a b => Enum ((:~:) k a b)
Methods succ :: (k :~: a) b -> (k :~: a) b # pred :: (k :~: a) b -> (k :~: a) b # toEnum :: Int -> (k :~: a) b # fromEnum :: (k :~: a) b -> Int # enumFrom :: (k :~: a) b -> [(k :~: a) b] # enumFromThen :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] # enumFromTo :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] # enumFromThenTo :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] #
Eq ((:~:) k a b)
Methods (==) :: (k :~: a) b -> (k :~: a) b -> Bool # (/=) :: (k :~: a) b -> (k :~: a) b -> Bool #
Ord ((:~:) k a b)
Methods compare :: (k :~: a) b -> (k :~: a) b -> Ordering # (<) :: (k :~: a) b -> (k :~: a) b -> Bool # (<=) :: (k :~: a) b -> (k :~: a) b -> Bool # (>) :: (k :~: a) b -> (k :~: a) b -> Bool # (>=) :: (k :~: a) b -> (k :~: a) b -> Bool # max :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b # min :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b #
(~) k a b => Read ((:~:) k a b)
Methods readsPrec :: Int -> ReadS ((k :~: a) b) # readList :: ReadS [(k :~: a) b] # readPrec :: ReadPrec ((k :~: a) b) # readListPrec :: ReadPrec [(k :~: a) b] #
Show ((:~:) k a b)
Methods showsPrec :: Int -> (k :~: a) b -> ShowS # show :: (k :~: a) b -> String # showList :: [(k :~: a) b] -> ShowS #
type KnownC k ((:~:) k a) b Source #
type KnownC k ((:~:) k a) b = (~) k a b
type WitnessC ØC ((~) k a b) ((:~:) k a b) Source #
type WitnessC ØC ((~) k a b) ((:~:) k a b) = ØC