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

import Data.Square
import Data.Profunctor
import Data.Profunctor.Composition
import Data.Functor.Compose.List

-- | The right Kan extension of a profunctor @p@ along a profunctor @j@.
newtype Ran j p a b = Ran { forall (j :: * -> * -> *) (p :: * -> * -> *) a b.
Ran j p a b -> forall c. j c a -> p c b
runRan :: forall c. j c a -> p c b }
instance Profunctor p => Functor (Ran j p a) where
  fmap :: forall a b. (a -> b) -> Ran j p a a -> Ran j p a b
fmap a -> b
f (Ran forall c. j c a -> p c a
jp) = forall (j :: * -> * -> *) (p :: * -> * -> *) a b.
(forall c. j c a -> p c b) -> Ran j p a b
Ran forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. j c a -> p c a
jp
instance (Profunctor j, Profunctor p) => Profunctor (Ran j p) where
  lmap :: forall a b c. (a -> b) -> Ran j p b c -> Ran j p a c
lmap a -> b
l (Ran forall c. j c b -> p c c
jp) = forall (j :: * -> * -> *) (p :: * -> * -> *) a b.
(forall c. j c a -> p c b) -> Ran j p a b
Ran forall a b. (a -> b) -> a -> b
$ forall c. j c b -> p c c
jp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap a -> b
l
  rmap :: forall b c a. (b -> c) -> Ran j p a b -> Ran j p a c
rmap b -> c
r (Ran forall c. j c a -> p c b
jp) = forall (j :: * -> * -> *) (p :: * -> * -> *) a b.
(forall c. j c a -> p c b) -> Ran j p a b
Ran forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap b -> c
r forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. j c a -> p c b
jp
  dimap :: forall a b c d. (a -> b) -> (c -> d) -> Ran j p b c -> Ran j p a d
dimap a -> b
l c -> d
r (Ran forall c. j c b -> p c c
jp) = forall (j :: * -> * -> *) (p :: * -> * -> *) a b.
(forall c. j c a -> p c b) -> Ran j p a b
Ran forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap c -> d
r forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. j c b -> p c c
jp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap a -> b
l

-- |
-- > +-----+
-- > j-\   |
-- > |  @--p
-- > R-/   |
-- > +-----+
ranSquare :: (Profunctor j, Profunctor p) => Square '[j, Ran j p] '[p] '[] '[]
ranSquare :: forall (j :: * -> * -> *) (p :: * -> * -> *).
(Profunctor j, Profunctor p) =>
Square '[j, Ran j p] '[p] '[] '[]
ranSquare = 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. (a -> b) -> a -> b
$ \(Procompose Ran j p x b
r j a x
j) -> forall (j :: * -> * -> *) (p :: * -> * -> *) a b.
Ran j p a b -> forall c. j c a -> p c b
runRan Ran j p x b
r j a x
j

-- |
-- > +-----+     +-----+
-- > j-\   |     |     |
-- > |  @--p ==> q--@--R
-- > q-/   |     |     |
-- > +-----+     +-----+
--
-- Any square like the one on the left factors through 'ranSquare'.
-- 'ranFactor' gives the remaining square.
ranFactor
  :: (Profunctor j, Profunctor p, Profunctor q)
  => Square '[j, q] '[p] '[] '[] -> Square '[q] '[Ran j p] '[] '[]
ranFactor :: forall (j :: * -> * -> *) (p :: * -> * -> *) (q :: * -> * -> *).
(Profunctor j, Profunctor p, Profunctor q) =>
Square '[j, q] '[p] '[] '[] -> Square '[q] '[Ran j p] '[] '[]
ranFactor Square '[j, q] '[p] '[] '[]
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 a b. (a -> b) -> a -> b
$ \PlainP '[q] a b
q -> forall (j :: * -> * -> *) (p :: * -> * -> *) a b.
(forall c. j c a -> p c b) -> Ran j p a b
Ran forall a b. (a -> b) -> a -> b
$ \j c a
j -> 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 '[j, q] '[p] '[] '[]
sq (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
Procompose PlainP '[q] a b
q j c a
j)

-- |
-- > +-----+
-- > R-\   |
-- > |  @--p
-- > j-/   |
-- > +-----+
riftSquare :: (Profunctor j, Profunctor p) => Square '[Rift j p, j] '[p] '[] '[]
riftSquare :: forall (j :: * -> * -> *) (p :: * -> * -> *).
(Profunctor j, Profunctor p) =>
Square '[Rift j p, j] '[p] '[] '[]
riftSquare = 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. (a -> b) -> a -> b
$ \(Procompose j x b
j Rift j p a x
r) -> forall {k1} {k2} {k3} (p :: k1 -> k2 -> *) (q :: k3 -> k2 -> *)
       (a :: k3) (b :: k1).
Rift p q a b -> forall (x :: k2). p b x -> q a x
runRift Rift j p a x
r j x b
j

-- |
-- > +-----+     +-----+
-- > q-\   |     |     |
-- > |  @--p ==> q--@--R
-- > j-/   |     |     |
-- > +-----+     +-----+
--
-- Any square like the one on the left factors through 'riftSquare'.
-- 'riftFactor' gives the remaining square.
riftFactor
  :: (Profunctor j, Profunctor p, Profunctor q)
  => Square '[q, j] '[p] '[] '[] -> Square '[q] '[Rift j p] '[] '[]
riftFactor :: forall (j :: * -> * -> *) (p :: * -> * -> *) (q :: * -> * -> *).
(Profunctor j, Profunctor p, Profunctor q) =>
Square '[q, j] '[p] '[] '[] -> Square '[q] '[Rift j p] '[] '[]
riftFactor Square '[q, j] '[p] '[] '[]
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 a b. (a -> b) -> a -> b
$ \PlainP '[q] a b
q -> forall {k} {k1} {k2} (p :: k -> k1 -> *) (q :: k2 -> k1 -> *)
       (a :: k2) (b :: k).
(forall (x :: k1). p b x -> q a x) -> Rift p q a b
Rift forall a b. (a -> b) -> a -> b
$ \j b x
j -> 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 '[q, j] '[p] '[] '[]
sq (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
Procompose j b x
j PlainP '[q] a b
q)