{-# LANGUAGE DataKinds #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Profunctor.Square
-- License     :  BSD-style (see the file LICENSE)
-- Maintainer  :  sjoerd@w3future.com
--
-----------------------------------------------------------------------------
module Data.Profunctor.Square where

import Data.Square
import qualified Data.Profunctor as P
import Data.Profunctor.Composition
import Data.Bifunctor.Biff

-- * Squares for profunctor subclasses

-- |
-- > +-a⊗_-+
-- > |  v  |
-- > p--@--p
-- > |  v  |
-- > +-a⊗_-+
second :: P.Strong p => Square '[p] '[p] '[(,) a] '[(,) a]
second :: forall (p :: * -> * -> *) a.
Strong p =>
Square '[p] '[p] '[(,) a] '[(,) a]
second = 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 (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (c, a) (c, b)
P.second'

-- |
-- > +-a⊕_-+
-- > |  v  |
-- > p--@--p
-- > |  v  |
-- > +-a⊕_-+
right :: P.Choice p => Square '[p] '[p] '[Either a] '[Either a]
right :: forall (p :: * -> * -> *) a.
Choice p =>
Square '[p] '[p] '[Either a] '[Either a]
right = 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 (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
P.right'

-- |
-- > +-a→_-+
-- > |  v  |
-- > p--@--p
-- > |  v  |
-- > +-a→_-+
closed :: P.Closed p => Square '[p] '[p] '[(->) a] '[(->) a]
closed :: forall (p :: * -> * -> *) a.
Closed p =>
Square '[p] '[p] '[(->) a] '[(->) a]
closed = 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 (p :: * -> * -> *) a b x.
Closed p =>
p a b -> p (x -> a) (x -> b)
P.closed

-- |
-- > +--f--+
-- > |  v  |
-- > p--@--p
-- > |  v  |
-- > +--f--+
map :: (P.Mapping p, Functor f) => Square '[p] '[p] '[f] '[f]
map :: forall (p :: * -> * -> *) (f :: * -> *).
(Mapping p, Functor f) =>
Square '[p] '[p] '[f] '[f]
map = 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 (p :: * -> * -> *) (f :: * -> *) a b.
(Mapping p, Functor f) =>
p a b -> p (f a) (f b)
P.map'

-- * Squares for @(->)@

-- |
-- >  +-----+
-- >  |     |
-- > (→)-@  |
-- >  |     |
-- >  +-----+
fromHom :: Square '[(->)] '[] '[] '[]
fromHom :: Square '[(->)] '[] '[] '[]
fromHom = 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

-- |
-- > +-----+
-- > |     |
-- > |  @-(→)
-- > |     |
-- > +-----+
toHom :: Square '[] '[(->)] '[] '[]
toHom :: Square '[] '[(->)] '[] '[]
toHom = 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

-- * Squares for `Procompose`

-- |
-- >  +-----+
-- >  |   /-p
-- > q.p-@  |
-- >  |   \-q
-- >  +-----+
fromProcompose :: (P.Profunctor p, P.Profunctor q) => Square '[Procompose q p] '[p, q] '[] '[]
fromProcompose :: forall (p :: * -> * -> *) (q :: * -> * -> *).
(Profunctor p, Profunctor q) =>
Square '[Procompose q p] '[p, q] '[] '[]
fromProcompose = 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-\   |
-- >  |  @-q.p
-- >  q-/   |
-- >  +-----+
toProcompose :: (P.Profunctor p, P.Profunctor q) => Square '[p, q] '[Procompose q p] '[] '[]
toProcompose :: forall (p :: * -> * -> *) (q :: * -> * -> *).
(Profunctor p, Profunctor q) =>
Square '[p, q] '[Procompose q p] '[] '[]
toProcompose = 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

-- * Squares for `Biff`

-- |
-- > +--f--+                                                       +--f--+
-- > |  v  |                                                             |
-- > B--@--q   Biff q f g is the "universal filler for the niche":       q
-- > |  v  |                                                             |
-- > +--g--+                                                       +--g--+
fromBiff :: P.Profunctor q => Square '[Biff q f g] '[q] '[f] '[g]
fromBiff :: forall (q :: * -> * -> *) (f :: * -> *) (g :: * -> *).
Profunctor q =>
Square '[Biff q f g] '[q] '[f] '[g]
fromBiff = 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 {k1} {k2} {k3} {k4} (p :: k1 -> k2 -> *) (f :: k3 -> k1)
       (g :: k4 -> k2) (a :: k3) (b :: k4).
Biff p f g a b -> p (f a) (g b)
runBiff

-- |
-- > +-h-f-+
-- > | v v |      +--h--+
-- > | \ / |      |  v  |
-- > p--@--q  ->  p--@--B
-- > | / \ |      |  v  |
-- > | v v |      +--k--+
-- > +-k-g-+
--
-- This is the universal property of `Biff`.
toBiff :: (P.Profunctor q, Functor f, Functor g) => Square '[p] '[q] '[h, f] '[k, g] -> Square '[p] '[Biff q f g] '[h] '[k]
toBiff :: forall (q :: * -> * -> *) (f :: * -> *) (g :: * -> *)
       (p :: * -> * -> *) (h :: * -> *) (k :: * -> *).
(Profunctor q, Functor f, Functor g) =>
Square '[p] '[q] '[h, f] '[k, g]
-> Square '[p] '[Biff q f g] '[h] '[k]
toBiff Square '[p] '[q] '[h, f] '[k, g]
sq = 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} {k2} {k3} (p :: k -> k1 -> *) (f :: k2 -> k)
       (g :: k3 -> k1) (a :: k2) (b :: k3).
p (f a) (g b) -> Biff p f g a b
Biff forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 '[p] '[q] '[h, f] '[k, g]
sq)