{-# LANGUAGE DataKinds #-}
module Data.Functor.Square where
import Data.Square
import Data.Functor.Identity
import Data.Functor.Compose
import Data.Profunctor
fromIdentity :: Square '[] '[] '[Identity] '[]
fromIdentity :: Square '[] '[] '[Identity] '[]
fromIdentity = forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
(gs :: [* -> *]).
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
Profunctor (PList qs)) =>
(forall a b.
PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b))
-> Square ps qs fs gs
mkSquare (forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Identity a -> a
runIdentity)
toIdentity :: Square '[] '[] '[] '[Identity]
toIdentity :: Square '[] '[] '[] '[Identity]
toIdentity = forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
(gs :: [* -> *]).
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
Profunctor (PList qs)) =>
(forall a b.
PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b))
-> Square ps qs fs gs
mkSquare (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
.)
fromCompose :: (Functor f, Functor g) => Square '[] '[] '[Compose g f] '[f, g]
fromCompose :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[] '[] '[Compose g f] '[f, g]
fromCompose = forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
(gs :: [* -> *]).
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
Profunctor (PList qs)) =>
(forall a b.
PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b))
-> Square ps qs fs gs
mkSquare ((forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap)
fromComposeStar :: (Functor f, Functor g) => Square '[Star (Compose f g)] '[Star f, Star g] '[] '[]
fromComposeStar :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[Star (Compose f g)] '[Star f, Star g] '[] '[]
fromComposeStar = forall (f :: * -> *). Square '[Star f] '[] '[] '[f]
fromLeft forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *])
(ss :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
(rs :: [* -> * -> *]) (hs :: [* -> *]).
(IsPList ps, IsPList qs, Profunctor (PList qs),
Profunctor (PList ss)) =>
Square ps qs fs gs
-> Square rs ss gs hs -> Square (ps ++ rs) (qs ++ ss) fs hs
=== forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[] '[] '[Compose g f] '[f, g]
fromCompose forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *])
(ss :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
(rs :: [* -> * -> *]) (hs :: [* -> *]).
(IsPList ps, IsPList qs, Profunctor (PList qs),
Profunctor (PList ss)) =>
Square ps qs fs gs
-> Square rs ss gs hs -> Square (ps ++ rs) (qs ++ ss) fs hs
=== forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[] '[Star g, Star f] '[f, g] '[]
toRight2
fromComposeCostar :: (Functor f, Functor g) => Square '[Costar f, Costar g] '[Costar (Compose g f)] '[] '[]
fromComposeCostar :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[Costar f, Costar g] '[Costar (Compose g f)] '[] '[]
fromComposeCostar = forall (f :: * -> *). Functor f => Square '[] '[Costar f] '[] '[f]
fromRight forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *])
(ss :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
(rs :: [* -> * -> *]) (hs :: [* -> *]).
(IsPList ps, IsPList qs, Profunctor (PList qs),
Profunctor (PList ss)) =>
Square ps qs fs gs
-> Square rs ss gs hs -> Square (ps ++ rs) (qs ++ ss) fs hs
=== forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[] '[] '[Compose g f] '[f, g]
fromCompose forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *])
(ss :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
(rs :: [* -> * -> *]) (hs :: [* -> *]).
(IsPList ps, IsPList qs, Profunctor (PList qs),
Profunctor (PList ss)) =>
Square ps qs fs gs
-> Square rs ss gs hs -> Square (ps ++ rs) (qs ++ ss) fs hs
=== forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[Costar f, Costar g] '[] '[f, g] '[]
toLeft2
toCompose :: (Functor f, Functor g) => Square '[] '[] '[f, g] '[Compose g f]
toCompose :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[] '[] '[f, g] '[Compose g f]
toCompose = forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
(gs :: [* -> *]).
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
Profunctor (PList qs)) =>
(forall a b.
PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b))
-> Square ps qs fs gs
mkSquare ((forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap)
toComposeStar :: (Functor f, Functor g) => Square '[Star f, Star g] '[Star (Compose f g)] '[] '[]
toComposeStar :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[Star f, Star g] '[Star (Compose f g)] '[] '[]
toComposeStar = forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[Star g, Star f] '[] '[] '[f, g]
fromLeft2 forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *])
(ss :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
(rs :: [* -> * -> *]) (hs :: [* -> *]).
(IsPList ps, IsPList qs, Profunctor (PList qs),
Profunctor (PList ss)) =>
Square ps qs fs gs
-> Square rs ss gs hs -> Square (ps ++ rs) (qs ++ ss) fs hs
=== forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[] '[] '[f, g] '[Compose g f]
toCompose forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *])
(ss :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
(rs :: [* -> * -> *]) (hs :: [* -> *]).
(IsPList ps, IsPList qs, Profunctor (PList qs),
Profunctor (PList ss)) =>
Square ps qs fs gs
-> Square rs ss gs hs -> Square (ps ++ rs) (qs ++ ss) fs hs
=== forall (f :: * -> *). Functor f => Square '[] '[Star f] '[f] '[]
toRight
toComposeCostar :: (Functor f, Functor g) => Square '[Costar (Compose g f)] '[Costar f, Costar g] '[] '[]
toComposeCostar :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[Costar (Compose g f)] '[Costar f, Costar g] '[] '[]
toComposeCostar = forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[] '[Costar f, Costar g] '[] '[f, g]
fromRight2 forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *])
(ss :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
(rs :: [* -> * -> *]) (hs :: [* -> *]).
(IsPList ps, IsPList qs, Profunctor (PList qs),
Profunctor (PList ss)) =>
Square ps qs fs gs
-> Square rs ss gs hs -> Square (ps ++ rs) (qs ++ ss) fs hs
=== forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[] '[] '[f, g] '[Compose g f]
toCompose forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *])
(ss :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
(rs :: [* -> * -> *]) (hs :: [* -> *]).
(IsPList ps, IsPList qs, Profunctor (PList qs),
Profunctor (PList ss)) =>
Square ps qs fs gs
-> Square rs ss gs hs -> Square (ps ++ rs) (qs ++ ss) fs hs
=== forall (f :: * -> *). Square '[Costar f] '[] '[f] '[]
toLeft