module Data.Type.Index.Trans
( module Data.Type.Index.Trans
, (:~:)(..)
) where
import Type.Class.Witness ((:~:)(..))
import Type.Family.List
import Type.Family.Tuple
type IxList' = IxList (:~:)
type IxEnv = IxList (IxFirst (:~:))
class IxLift (t :: (k -> m -> *) -> l -> m -> *) (x :: l) where
type LiftI t x :: k
ixLift :: i (LiftI t x) y
-> t i x y
data IxList (i :: k -> l -> *) :: [k] -> l -> * where
IxHead :: !(i a b)
-> IxList i (a :< as) b
IxTail :: !(IxList i as b)
-> IxList i (a :< as) b
data IxFirst (i :: k -> l -> *) :: (k,m) -> l -> * where
IxFirst :: !(i a b)
-> IxFirst i '(a,c) b
instance (p ~ '(Fst p,Snd p)) => IxLift IxFirst p where
type LiftI IxFirst p = Fst p
ixLift = IxFirst
data IxSecond (i :: k -> l -> *) :: (m,k) -> l -> * where
IxSecond :: !(i a b)
-> IxSecond i '(c,a) b
instance (p ~ '(Fst p,Snd p)) => IxLift IxSecond p where
type LiftI IxSecond p = Snd p
ixLift = IxSecond
data IxOr (i :: k -> m -> *) (j :: l -> m -> *) :: Either k l -> m -> * where
IxOrL :: !(i a b)
-> IxOr i j (Left a) b
IxOrR :: !(j a b)
-> IxOr i j (Right a) b
instance IxLift (IxOr i) (Right a) where
type LiftI (IxOr i) (Right a) = a
ixLift = IxOrR
data IxJust (i :: k -> l -> *) :: Maybe k -> l -> * where
IxJust :: !(i a b)
-> IxJust i (Just a) b
data IxComp (i :: k -> l -> *) (j :: l -> m -> *) :: k -> m -> * where
IxComp :: !(i a b)
-> !(j b c)
-> IxComp i j a c