{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#endif
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Square
-- License     :  BSD-style (see the file LICENSE)
-- Maintainer  :  sjoerd@w3future.com
--
-----------------------------------------------------------------------------

module Data.Square where

import Data.Functor.Compose.List
import Data.Profunctor
import qualified Data.Profunctor.Composition as P
import Data.Profunctor.Composition.List
import Data.Type.List
#if __GLASGOW_HASKELL__ >= 810
import Data.Kind
#endif

-- * Double category

-- $doubleCategory
-- There is a double category of Haskell functors and profunctors.
--
-- The squares in this double category are natural transformations.

-- |
-- > +-----+
-- > |     |
-- > |     |
-- > |     |
-- > +-----+
--
-- > forall a b. (a -> b) -> (a -> b)
--
-- The empty square is the identity transformation.
emptySquare :: Square '[] '[] '[] '[]
emptySquare :: Square '[] '[] '[] '[]
emptySquare = 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 -> a
id

-- |
-- > +-----+
-- > |     |
-- > p-----p
-- > |     |
-- > +-----+
--
-- > forall a b. p a b -> p a b
--
-- Profunctors are drawn as horizontal lines.
--
-- Note that `emptySquare` is `proId` for the profunctor @(->)@.
-- We don't draw a line for @(->)@ because it is the identity for profunctor composition.
proId :: Profunctor p => Square '[p] '[p] '[] '[]
proId :: forall (p :: * -> * -> *). Profunctor p => Square '[p] '[p] '[] '[]
proId = 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 -> a
id

-- |
-- > +--f--+
-- > |  |  |
-- > |  v  |
-- > |  |  |
-- > +--f--+
--
-- > forall a b. (a -> b) -> (f a -> f b)
--
-- Functors are drawn with vertical lines with arrow heads.
-- You will recognize the above type as `fmap`!
--
-- We don't draw lines for the identity functor, because it is the identity for functor composition.
funId :: Functor f => Square '[] '[] '[f] '[f]
funId :: forall (f :: * -> *). Functor f => Square '[] '[] '[f] '[f]
funId = 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap

-- |
-- > +--f--+
-- > |  |  |
-- > |  @  |
-- > |  |  |
-- > +--g--+
--
-- > forall a b. (a -> b) -> (f a -> g b)
--
-- Non-identity transformations are drawn with an @\@@ in the middle.
-- Natural transformations between haskell functors are usualy given the type
-- @forall a. f a -> g a@. The type above you get when `fmap`ping before or after.
-- (It doesn't matter which, because of naturality!)
funNat :: (Functor f, Functor g) => (f ~> g) -> Square '[] '[] '[f] '[g]
funNat :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
(f ~> g) -> Square '[] '[] '[f] '[g]
funNat f ~> g
n = 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 ((f ~> g
n 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)

-- |
-- > +-----+
-- > |     |
-- > p--@--q
-- > |     |
-- > +-----+
--
-- > forall a b. p a b -> q a b
--
-- Natural transformations between profunctors.
proNat :: (Profunctor p, Profunctor q) => (p :-> q) -> Square '[p] '[q] '[] '[]
proNat :: forall (p :: * -> * -> *) (q :: * -> * -> *).
(Profunctor p, Profunctor q) =>
(p :-> q) -> Square '[p] '[q] '[] '[]
proNat = 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

-- |
-- > +--f--+
-- > |  v  |
-- > p--@--q
-- > |  v  |
-- > +--g--+
--
-- > forall a b. p a b -> q (f a) (g b)
--
-- The complete definition of a square is a combination of natural transformations
-- between functors and natural transformations between profunctors.
--
-- To make type inferencing easier the above type is wrapped by a newtype.
#if __GLASGOW_HASKELL__ >= 810
type SquareNT :: (a -> b -> Type) -> (c -> d -> Type) -> (a -> c) -> (b -> d) -> Type
#endif
newtype SquareNT p q f g = Square { forall a b c d (p :: a -> b -> *) (q :: c -> d -> *) (f :: a -> c)
       (g :: b -> d).
SquareNT p q f g
-> forall (a :: a) (b :: b). p a b -> q (f a) (g b)
unSquare :: forall a b. p a b -> q (f a) (g b) }

-- | To make composing squares associative, this library uses squares with lists of functors and profunctors,
-- which are composed together.
--
-- > FList '[] a ~ a
-- > FList '[f, g, h] a ~ h (g (f a))
-- > PList '[] a b ~ a -> b
-- > PList '[p, q, r] a b ~ (p a x, q x y, r y b)
type Square ps qs fs gs = SquareNT (PList ps) (PList qs) (FList fs) (FList gs)

-- | A helper function to add the wrappers needed for `PList` and `FList`.
mkSquare
  :: (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 (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 b. PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b)
n = forall a b c d (p :: a -> b -> *) (q :: c -> d -> *) (f :: a -> c)
       (g :: b -> d).
(forall (a :: a) (b :: b). p a b -> q (f a) (g b))
-> SquareNT p q f g
Square (forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall (fs :: [* -> *]) a. IsFList fs => FList fs a -> PlainF fs a
toPlainF forall (fs :: [* -> *]) a. IsFList fs => PlainF fs a -> FList fs a
fromPlainF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall (ps :: [* -> * -> *]). IsPList ps => PList ps :-> PlainP ps
toPlainP forall (ps :: [* -> * -> *]). IsPList ps => PlainP ps :-> PList ps
fromPlainP forall a b. PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b)
n)

-- | A helper function to remove the wrappers needed for `PList` and `FList`.
runSquare
  :: (IsPList ps, IsPList qs, IsFList fs, IsFList gs, Profunctor (PList qs))
  => Square ps qs fs gs
  -> PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b) -- ^
runSquare :: forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
       (gs :: [* -> *]) a b.
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
 Profunctor (PList qs)) =>
Square ps qs fs gs
-> PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b)
runSquare (Square forall a b. PList ps a b -> PList qs (FList fs a) (FList gs b)
n) = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall (ps :: [* -> * -> *]). IsPList ps => PlainP ps :-> PList ps
fromPlainP forall (ps :: [* -> * -> *]). IsPList ps => PList ps :-> PlainP ps
toPlainP (forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall (fs :: [* -> *]) a. IsFList fs => PlainF fs a -> FList fs a
fromPlainF forall (fs :: [* -> *]) a. IsFList fs => FList fs a -> PlainF fs a
toPlainF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. PList ps a b -> PList qs (FList fs a) (FList gs b)
n)

-- |
-- > +--f--+     +--h--+       +--f--h--+
-- > |  v  |     |  v  |       |  v  v  |
-- > p--@--q ||| q--@--r  ==>  p--@--@--r
-- > |  v  |     |  v  |       |  v  v  |
-- > +--g--+     +--i--+       +--g--i--+
--
-- Horizontal composition of squares. `proId` is the identity of `(|||)`.
-- This is regular function composition of the underlying functions.
infixl 6 |||
(|||) :: (Profunctor (PList rs), IsFList fs, IsFList gs, Functor (FList hs), Functor (FList is))
      => Square ps qs fs gs -> Square qs rs hs is -> Square ps rs (fs ++ hs) (gs ++ is) -- ^
Square forall a b. PList ps a b -> PList qs (FList fs a) (FList gs b)
pq ||| :: forall (rs :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
       (hs :: [* -> *]) (is :: [* -> *]) (ps :: [* -> * -> *])
       (qs :: [* -> * -> *]).
(Profunctor (PList rs), IsFList fs, IsFList gs, Functor (FList hs),
 Functor (FList is)) =>
Square ps qs fs gs
-> Square qs rs hs is -> Square ps rs (fs ++ hs) (gs ++ is)
||| Square forall a b. PList qs a b -> PList rs (FList hs a) (FList is b)
qr = forall a b c d (p :: a -> b -> *) (q :: c -> d -> *) (f :: a -> c)
       (g :: b -> d).
(forall (a :: a) (b :: b). p a b -> q (f a) (g b))
-> SquareNT p q f g
Square (forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall (fs :: [* -> *]) (gs :: [* -> *]) a.
(IsFList fs, Functor (FList gs)) =>
FList (fs ++ gs) a -> FList gs (FList fs a)
funappend forall (fs :: [* -> *]) (gs :: [* -> *]) a.
(IsFList fs, Functor (FList gs)) =>
FList gs (FList fs a) -> FList (fs ++ gs) a
fappend forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. PList qs a b -> PList rs (FList hs a) (FList is b)
qr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. PList ps a b -> PList qs (FList fs a) (FList gs b)
pq)

-- |
-- > +--f--+
-- > |  v  |
-- > p--@--q              +--f--+
-- > |  v  |              |  v  |
-- > +--g--+              p--@--q
-- >   ===        ==>     |  v  |
-- > +--g--+              r--@--s
-- > |  v  |              |  v  |
-- > r--@--s              +--h--+
-- > |  v  |
-- > +--h--+
--
-- Vertical composition of squares. `funId` is the identity of `(===)`.
infixl 5 ===
(===) :: (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 -- ^
Square forall a b. PList ps a b -> PList qs (FList fs a) (FList gs b)
pq === :: 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
=== Square forall a b. PList rs a b -> PList ss (FList gs a) (FList hs b)
rs = forall a b c d (p :: a -> b -> *) (q :: c -> d -> *) (f :: a -> c)
       (g :: b -> d).
(forall (a :: a) (b :: b). p a b -> q (f a) (g b))
-> SquareNT p q f g
Square (\PList (ps ++ rs) a b
pr -> case forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]).
IsPList ps =>
PList (ps ++ qs) :-> Procompose (PList qs) (PList ps)
punappend PList (ps ++ rs) a b
pr of P.Procompose PList rs x b
r PList ps a x
p -> forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]).
(IsPList ps, Profunctor (PList ps), Profunctor (PList qs)) =>
Procompose (PList qs) (PList ps) :-> PList (ps ++ qs)
pappend (forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
       (q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
P.Procompose (forall a b. PList rs a b -> PList ss (FList gs a) (FList hs b)
rs PList rs x b
r) (forall a b. PList ps a b -> PList qs (FList fs a) (FList gs b)
pq PList ps a x
p)))


-- * Proarrow equipment
--
-- $proarrowEquipment
-- The double category of haskell functors and profunctors is a proarrow equipment.
-- Which means that we can "bend" functors to become profunctors.

-- |
-- > +--f--+
-- > |  v  |
-- > |  \->f
-- > |     |
-- > +-----+
--
-- A functor @f@ can be bent to the right to become the profunctor @`Star` f@.
toRight :: Functor f => Square '[] '[Star f] '[f] '[]
toRight :: forall (f :: * -> *). Functor f => Square '[] '[Star f] '[f] '[]
toRight = 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} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap)

-- |
-- > +--f--+
-- > |  v  |
-- > f<-/  |
-- > |     |
-- > +-----+
--
-- A functor @f@ can be bent to the left to become the profunctor @`Costar` f@.
toLeft :: Square '[Costar f] '[] '[f] '[]
toLeft :: forall (f :: * -> *). Square '[Costar f] '[] '[f] '[]
toLeft = 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} (f :: k -> *) (d :: k) c. Costar f d c -> f d -> c
runCostar

-- |
-- > +-----+
-- > |     |
-- > |  /-<f
-- > |  v  |
-- > +--f--+
--
-- The profunctor @`Costar` f@ can be bent down to become the functor @f@ again.
fromRight :: Functor f => Square '[] '[Costar f] '[] '[f]
fromRight :: forall (f :: * -> *). Functor f => Square '[] '[Costar f] '[] '[f]
fromRight = 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} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap)

-- |
-- > +-----+
-- > |     |
-- > f>-\  |
-- > |  v  |
-- > +--f--+
--
-- The profunctor @`Star` f@ can be bent down to become the functor @f@ again.
fromLeft :: Square '[Star f] '[] '[] '[f]
fromLeft :: forall (f :: * -> *). Square '[Star f] '[] '[] '[f]
fromLeft = 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} (f :: k -> *) d (c :: k). Star f d c -> d -> f c
runStar

-- |
-- > +-----+
-- > f>-\  |         fromLeft
-- > |  v  |         ===
-- > f<-/  |         toLeft
-- > +-----+
--
-- `fromLeft` and `toLeft` can be composed vertically to bend @`Star` f@ back to @`Costar` f@.
uLeft :: Functor f => Square '[Star f, Costar f] '[] '[] '[]
uLeft :: forall (f :: * -> *).
Functor f =>
Square '[Star f, Costar f] '[] '[] '[]
uLeft =
  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 :: * -> *). Square '[Costar f] '[] '[f] '[]
toLeft

-- |
-- > +-----+
-- > |  /-<f         fromRight
-- > |  v  |         ===
-- > |  \->f         toRight
-- > +-----+
--
-- `fromRight` and `toRight` can be composed vertically to bend @`Costar` f@ to @`Star` f@.
uRight :: Functor f => Square '[] '[Costar f, Star f] '[] '[]
uRight :: forall (f :: * -> *).
Functor f =>
Square '[] '[Costar f, Star f] '[] '[]
uRight =
  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 :: * -> *). Functor f => Square '[] '[Star f] '[f] '[]
toRight

-- |
-- > +-f-g-+
-- > | v \>g         funId ||| toRight
-- > | |   |         ===
-- > | \-->f         toRight
-- > +-----+
toRight2 :: (Functor f, Functor g) => Square '[] '[Star g, Star f] '[f, g] '[]
toRight2 :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[] '[Star g, Star f] '[f, g] '[]
toRight2 = (forall (f :: * -> *). Functor f => Square '[] '[] '[f] '[f]
funId forall (rs :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
       (hs :: [* -> *]) (is :: [* -> *]) (ps :: [* -> * -> *])
       (qs :: [* -> * -> *]).
(Profunctor (PList rs), IsFList fs, IsFList gs, Functor (FList hs),
 Functor (FList is)) =>
Square ps qs fs gs
-> Square qs rs hs is -> Square ps rs (fs ++ hs) (gs ++ is)
||| forall (f :: * -> *). Functor f => Square '[] '[Star f] '[f] '[]
toRight) 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

-- |
-- > +-f-g-+
-- > f</ v |         toLeft ||| funId
-- > |   | |         ===
-- > g<--/ |         toLeft
-- > +-----+
toLeft2 :: (Functor f, Functor g) => Square '[Costar f, Costar g] '[] '[f, g] '[]
toLeft2 :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[Costar f, Costar g] '[] '[f, g] '[]
toLeft2 = (forall (f :: * -> *). Square '[Costar f] '[] '[f] '[]
toLeft forall (rs :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
       (hs :: [* -> *]) (is :: [* -> *]) (ps :: [* -> * -> *])
       (qs :: [* -> * -> *]).
(Profunctor (PList rs), IsFList fs, IsFList gs, Functor (FList hs),
 Functor (FList is)) =>
Square ps qs fs gs
-> Square qs rs hs is -> Square ps rs (fs ++ hs) (gs ++ is)
||| forall (f :: * -> *). Functor f => Square '[] '[] '[f] '[f]
funId) 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

-- |
-- > +-----+
-- > | /--<f         fromRight
-- > | |   |         ===
-- > | v /<g         funId ||| fromRight
-- > +-f-g-+
fromRight2 :: (Functor f, Functor g) => Square '[] '[Costar f, Costar g] '[] '[f, g]
fromRight2 :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[] '[Costar f, Costar g] '[] '[f, g]
fromRight2 = 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 :: * -> *). Functor f => Square '[] '[] '[f] '[f]
funId forall (rs :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
       (hs :: [* -> *]) (is :: [* -> *]) (ps :: [* -> * -> *])
       (qs :: [* -> * -> *]).
(Profunctor (PList rs), IsFList fs, IsFList gs, Functor (FList hs),
 Functor (FList is)) =>
Square ps qs fs gs
-> Square qs rs hs is -> Square ps rs (fs ++ hs) (gs ++ is)
||| forall (f :: * -> *). Functor f => Square '[] '[Costar f] '[] '[f]
fromRight)

-- |
-- > +-----+
-- > g>--\ |         fromLeft
-- > |   | |         ===
-- > f>\ | |         fromLeft ||| funId
-- > +-f-g-+
fromLeft2 :: (Functor f, Functor g) => Square '[Star g, Star f] '[] '[] '[f, g]
fromLeft2 :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Square '[Star g, Star f] '[] '[] '[f, g]
fromLeft2 = 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 :: * -> *). Square '[Star f] '[] '[] '[f]
fromLeft forall (rs :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
       (hs :: [* -> *]) (is :: [* -> *]) (ps :: [* -> * -> *])
       (qs :: [* -> * -> *]).
(Profunctor (PList rs), IsFList fs, IsFList gs, Functor (FList hs),
 Functor (FList is)) =>
Square ps qs fs gs
-> Square qs rs hs is -> Square ps rs (fs ++ hs) (gs ++ is)
||| forall (f :: * -> *). Functor f => Square '[] '[] '[f] '[f]
funId)

-- |
-- > +f-f-f+     +--f--+     spiderLemma n =
-- > |v v v|     f> v <f       fromLeft ||| funId ||| fromRight
-- > | \|/ |     | \|/ |       ===
-- > p--@--q ==> p--@--q       n
-- > | /|\ |     | /|\ |       ===
-- > |v v v|     g< v >g       toLeft ||| funId ||| toRight
-- > +g-g-g+     +--g--+
--
-- The spider lemma is an example how bending wires can also be seen as sliding functors around corners.
spiderLemma :: (Profunctor p, Profunctor q, Functor f1, Functor f2, Functor f3, Functor g1, Functor g2, Functor g3)
  => Square '[p] '[q] '[f1, f2, f3] '[g1, g2, g3]
  -> Square '[Star f1, p, Costar g1] '[Costar f3, q, Star g3] '[f2] '[g2] -- ^
spiderLemma :: forall (p :: * -> * -> *) (q :: * -> * -> *) (f1 :: * -> *)
       (f2 :: * -> *) (f3 :: * -> *) (g1 :: * -> *) (g2 :: * -> *)
       (g3 :: * -> *).
(Profunctor p, Profunctor q, Functor f1, Functor f2, Functor f3,
 Functor g1, Functor g2, Functor g3) =>
Square '[p] '[q] '[f1, f2, f3] '[g1, g2, g3]
-> Square
     '[Star f1, p, Costar g1] '[Costar f3, q, Star g3] '[f2] '[g2]
spiderLemma Square '[p] '[q] '[f1, f2, f3] '[g1, g2, g3]
n =
  forall (f :: * -> *). Square '[Star f] '[] '[] '[f]
fromLeft forall (rs :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
       (hs :: [* -> *]) (is :: [* -> *]) (ps :: [* -> * -> *])
       (qs :: [* -> * -> *]).
(Profunctor (PList rs), IsFList fs, IsFList gs, Functor (FList hs),
 Functor (FList is)) =>
Square ps qs fs gs
-> Square qs rs hs is -> Square ps rs (fs ++ hs) (gs ++ is)
||| forall (f :: * -> *). Functor f => Square '[] '[] '[f] '[f]
funId forall (rs :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
       (hs :: [* -> *]) (is :: [* -> *]) (ps :: [* -> * -> *])
       (qs :: [* -> * -> *]).
(Profunctor (PList rs), IsFList fs, IsFList gs, Functor (FList hs),
 Functor (FList is)) =>
Square ps qs fs gs
-> Square qs rs hs is -> Square ps rs (fs ++ hs) (gs ++ is)
||| 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
===
  Square '[p] '[q] '[f1, f2, f3] '[g1, g2, g3]
n
  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 forall (rs :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
       (hs :: [* -> *]) (is :: [* -> *]) (ps :: [* -> * -> *])
       (qs :: [* -> * -> *]).
(Profunctor (PList rs), IsFList fs, IsFList gs, Functor (FList hs),
 Functor (FList is)) =>
Square ps qs fs gs
-> Square qs rs hs is -> Square ps rs (fs ++ hs) (gs ++ is)
||| forall (f :: * -> *). Functor f => Square '[] '[] '[f] '[f]
funId forall (rs :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
       (hs :: [* -> *]) (is :: [* -> *]) (ps :: [* -> * -> *])
       (qs :: [* -> * -> *]).
(Profunctor (PList rs), IsFList fs, IsFList gs, Functor (FList hs),
 Functor (FList is)) =>
Square ps qs fs gs
-> Square qs rs hs is -> Square ps rs (fs ++ hs) (gs ++ is)
||| forall (f :: * -> *). Functor f => Square '[] '[Star f] '[f] '[]
toRight

-- |> spiderLemma' n = (toRight === proId === fromRight) ||| n ||| (toLeft === proId === fromLeft)
--
-- The spider lemma in the other direction.
spiderLemma' :: (Profunctor p, Profunctor q, Functor f1, Functor f2, Functor f3, Functor g1, Functor g2, Functor g3)
  => Square '[Star f1, p, Costar g1] '[Costar f3, q, Star g3] '[f2] '[g2]
  -> Square '[p] '[q] '[f1, f2, f3] '[g1, g2, g3] -- ^
spiderLemma' :: forall (p :: * -> * -> *) (q :: * -> * -> *) (f1 :: * -> *)
       (f2 :: * -> *) (f3 :: * -> *) (g1 :: * -> *) (g2 :: * -> *)
       (g3 :: * -> *).
(Profunctor p, Profunctor q, Functor f1, Functor f2, Functor f3,
 Functor g1, Functor g2, Functor g3) =>
Square
  '[Star f1, p, Costar g1] '[Costar f3, q, Star g3] '[f2] '[g2]
-> Square '[p] '[q] '[f1, f2, f3] '[g1, g2, g3]
spiderLemma' Square
  '[Star f1, p, Costar g1] '[Costar f3, q, Star g3] '[f2] '[g2]
n = (forall (f :: * -> *). Functor f => Square '[] '[Star f] '[f] '[]
toRight 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 (p :: * -> * -> *). Profunctor p => Square '[p] '[p] '[] '[]
proId 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 '[] '[Costar f] '[] '[f]
fromRight) forall (rs :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
       (hs :: [* -> *]) (is :: [* -> *]) (ps :: [* -> * -> *])
       (qs :: [* -> * -> *]).
(Profunctor (PList rs), IsFList fs, IsFList gs, Functor (FList hs),
 Functor (FList is)) =>
Square ps qs fs gs
-> Square qs rs hs is -> Square ps rs (fs ++ hs) (gs ++ is)
||| Square
  '[Star f1, p, Costar g1] '[Costar f3, q, Star g3] '[f2] '[g2]
n forall (rs :: [* -> * -> *]) (fs :: [* -> *]) (gs :: [* -> *])
       (hs :: [* -> *]) (is :: [* -> *]) (ps :: [* -> * -> *])
       (qs :: [* -> * -> *]).
(Profunctor (PList rs), IsFList fs, IsFList gs, Functor (FList hs),
 Functor (FList is)) =>
Square ps qs fs gs
-> Square qs rs hs is -> Square ps rs (fs ++ hs) (gs ++ is)
||| (forall (f :: * -> *). Square '[Costar f] '[] '[f] '[]
toLeft 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 (p :: * -> * -> *). Profunctor p => Square '[p] '[p] '[] '[]
proId 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 '[Star f] '[] '[] '[f]
fromLeft)

-- * In other categories than Hask

-- $otherCategories
-- > A--f--C
-- > |  v  |
-- > p--@--q
-- > |  v  |
-- > B--g--D
--
-- Squares can be generalized further by choosing a different category for each quadrant.
-- To use this, `SquareNT` has been made kind polymorphic:
--
-- > type SquareNT :: (a -> b -> Type) -> (c -> d -> Type) -> (a -> c) -> (b -> d) -> Type
--
-- This library is mostly about staying in Hask, but it is interesting to use f.e. the
-- product category @Hask × Hask@ or the unit category.

-- |
-- > H²-f--H
-- > |  v  |
-- > p--@--q     H = Hask, H² = Hask x Hask
-- > |  v  |
-- > H²-g--H
--
type Square21 ps1 ps2 qs f g = SquareNT (PList ps1 :**: PList ps2) (PList qs) (UncurryF f) (UncurryF g)

-- | Combine two profunctors from Hask to a profunctor from Hask x Hask
data (p1 :**: p2) a b where
  (:**:) :: p1 a1 b1 -> p2 a2 b2 -> (p1 :**: p2) '(a1, a2) '(b1, b2)

-- | Uncurry the kind of a bifunctor.
--
-- > type UncurryF :: (a -> b -> Type) -> (a, b) -> Type
#if __GLASGOW_HASKELL__ >= 810
type UncurryF :: (a -> b -> Type) -> (a, b) -> Type
#endif
data UncurryF f a where
  UncurryF :: { forall {a} {b} (f :: a -> b -> *) (a :: a) (b :: b).
UncurryF f '(a, b) -> f a b
curryF :: f a b } -> UncurryF f '(a, b)

-- |
-- > 1--a--H
-- > |  v  |
-- > U--@--q     1 = Hask^0 = (), H = Hask
-- > |  v  |
-- > 1--b--H
--
type Square01 qs a b = SquareNT Unit (PList qs) (ValueF a) (ValueF b)

-- | The boring profunctor from and to the unit category.
data Unit a b where
  Unit :: Unit '() '()

-- | Values as a functor from the unit category.
data ValueF x u where
  ValueF :: a -> ValueF a '()