module Type.Family.Tuple where
import Type.Family.Monoid
import Type.Class.Witness
type (#) = '(,)
infixr 6 #
type family Fst (p :: (k,l)) :: k where
Fst '(a,b) = a
fstCong :: (p ~ q) :- (Fst p ~ Fst q)
fstCong = Sub Wit
type family Snd (p :: (k,l)) :: l where
Snd '(a,b) = b
sndCong :: (p ~ q) :- (Snd p ~ Snd q)
sndCong = Sub Wit
type family Fst3 (p :: (k,l,m)) :: k where
Fst3 '(a,b,c) = a
fst3Cong :: (p ~ q) :- (Fst3 p ~ Fst3 q)
fst3Cong = Sub Wit
type family Snd3 (p :: (k,l,m)) :: l where
Snd3 '(a,b,c) = b
snd3Cong :: (p ~ q) :- (Snd3 p ~ Snd3 q)
snd3Cong = Sub Wit
type family Thd3 (p :: (k,l,m)) :: m where
Thd3 '(a,b,c) = c
thd3Cong :: (p ~ q) :- (Thd3 p ~ Thd3 q)
thd3Cong = Sub Wit
type family (f :: k -> l) <$> (a :: (m,k)) :: (m,l) where
f <$> (a#b) = a # f b
infixr 4 <$>
pairMapCong :: (f ~ g,a ~ b) :- ((f <$> a) ~ (g <$> b))
pairMapCong = Sub Wit
type family (f :: (m,k -> l)) <&> (a :: k) :: (m,l) where
(r#f) <&> a = r # f a
infixr 4 <&>
type family (f :: (m,k -> l)) <*> (a :: (m,k)) :: (m,l) where
(r#f) <*> (s#a) = (r <> s) # f a
infixr 4 <*>
type instance Mempty = Mempty # Mempty
type instance (r#a) <> (s#b) = (r <> s) # (a <> b)
type instance Mempty = '(Mempty,Mempty,Mempty)
type instance '(a,b,c) <> '(d,e,f) = '(a<>d,b<>e,c<>f)