module Data.Yoko.W where
data family W (t :: k) :: (* -> * -> *) -> * -> * -> *
newtype instance W (t :: *) s p1 p0 = W0 (t -> s p1 p0)
newtype instance W (t :: * -> *) s p1 p0 = W1 (t p0 -> s p1 p0)
newtype instance W (t :: * -> * -> *) s p1 p0 = W2 (t p1 p0 -> s p1 p0)
unW0 (W0 f) = f
unW1 (W1 f) = f
unW2 (W2 f) = f
data family W' (s :: k) :: (* -> * -> *) -> * -> * -> *
newtype instance W' (s :: *) t p1 p0 = W'0 (t p1 p0 -> s )
newtype instance W' (s :: * -> *) t p1 p0 = W'1 (t p1 p0 -> s p0)
newtype instance W' (s :: * -> * -> *) t p1 p0 = W'2 (t p1 p0 -> s p1 p0)
unW'0 (W'0 f) = f
unW'1 (W'1 f) = f
unW'2 (W'2 f) = f
data family Sym (t :: k) :: k -> * -> * -> *
newtype instance Sym (t :: *) s p1 p0 = Sym0 (t -> s )
newtype instance Sym (t :: * -> *) s p1 p0 = Sym1 (t p0 -> s p0)
newtype instance Sym (t :: * -> * -> *) s p1 p0 = Sym2 (t p1 p0 -> s p1 p0)
unSym0 (Sym0 f) = f
unSym1 (Sym1 f) = f
unSym2 (Sym2 f) = f
class ComposeW (t :: k) where
composeW :: (s p1 p0 -> s' p1 p0) -> W t s p1 p0 -> W t s' p1 p0
composeW' :: W' t s' p1 p0 -> (s p1 p0 -> s' p1 p0) -> W' t s p1 p0
sym :: W' t' s p1 p0 -> W t s p1 p0 -> Sym t t' p1 p0
unSym :: W t s' p1 p0 -> W' t s p1 p0 -> s p1 p0 -> s' p1 p0
composeSymW' :: Sym t t' p1 p0 -> W' t s p1 p0 -> W' t' s p1 p0
composeWSym :: W t' s p1 p0 -> Sym t t' p1 p0 -> W t s p1 p0
instance ComposeW (t :: *) where
composeW f (W0 g) = W0 (f . g)
composeW' (W'0 f) g = W'0 (f . g)
sym (W'0 f) (W0 g) = Sym0 (f . g)
unSym (W0 f) (W'0 g) = f . g
composeSymW' (Sym0 f) (W'0 g) = W'0 (f . g)
composeWSym (W0 f) (Sym0 g) = W0 (f . g)
instance ComposeW (t :: * -> *) where
composeW f (W1 g) = W1 (f . g)
composeW' (W'1 f) g = W'1 (f . g)
sym (W'1 f) (W1 g) = Sym1 (f . g)
unSym (W1 f) (W'1 g) = f . g
composeSymW' (Sym1 f) (W'1 g) = W'1 (f . g)
composeWSym (W1 f) (Sym1 g) = W1 (f . g)
instance ComposeW (t :: * -> * -> *) where
composeW f (W2 g) = W2 (f . g)
composeW' (W'2 f) g = W'2 (f . g)
sym (W'2 f) (W2 g) = Sym2 (f . g)
unSym (W2 f) (W'2 g) = f . g
composeSymW' (Sym2 f) (W'2 g) = W'2 (f . g)
composeWSym (W2 f) (Sym2 g) = W2 (f . g)