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

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

-- | The left Kan extension of a functor @f@ along a profunctor @j@.
--
-- The left Kan extension of a functor @f@ along a functor @g@ is @'Lan' ('Data.Profunctor.Costar' g) f@.
data Lan j f b = forall a. Lan (j a b) (f a)

-- |
-- > +--f--+
-- > |  v  |
-- > j--@  |
-- > |  v  |
-- > +--L--+
lanSquare :: Square '[j] '[] '[f] '[Lan j f]
lanSquare :: forall (j :: * -> * -> *) (f :: * -> *).
Square '[j] '[] '[f] '[Lan j f]
lanSquare = 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 (j :: * -> * -> *) (f :: * -> *) b a.
j a b -> f a -> Lan j f b
Lan

-- |
-- > +--f--+
-- > |  v  |     +--L--+
-- > j-\|  |     |  v  |
-- > |  @  | ==> h--@  |
-- > h-/|  |     |  v  |
-- > |  v  |     +--g--+
-- > +--g--+
--
-- Any square like the one on the left factors through 'lanSquare'.
-- 'lanFactor' gives the remaining square.
lanFactor :: (Profunctor h, IsFList gs) => Square '[j, h] '[] '[f] gs -> Square '[h] '[] '[Lan j f] gs
lanFactor :: forall (h :: * -> * -> *) (gs :: [* -> *]) (j :: * -> * -> *)
       (f :: * -> *).
(Profunctor h, IsFList gs) =>
Square '[j, h] '[] '[f] gs -> Square '[h] '[] '[Lan j f] gs
lanFactor Square '[j, h] '[] '[f] gs
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 '[h] a b
h (Lan j a a
j f a
f) -> 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, h] '[] '[f] gs
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 '[h] a b
h j a a
j) f a
f

-- | The right Kan extension of a functor @f@ along a profunctor @j@.
--
-- The right Kan extension of a functor @f@ along a functor @g@ is @'Ran' ('Data.Profunctor.Star' g) f@.
newtype Ran j f a = Ran { forall (j :: * -> * -> *) (f :: * -> *) a.
Ran j f a -> forall b. j a b -> f b
runRan :: forall b. j a b -> f b }

-- |
-- > +--R--+
-- > |  v  |
-- > j--@  |
-- > |  v  |
-- > +--g--+
ranSquare :: Square '[j] '[] '[Ran j g] '[g]
ranSquare :: forall (j :: * -> * -> *) (g :: * -> *).
Square '[j] '[] '[Ran j g] '[g]
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
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (j :: * -> * -> *) (f :: * -> *) a.
Ran j f a -> forall b. j a b -> f b
runRan

-- |
-- > +--f--+
-- > |  v  |     +--f--+
-- > h-\|  |     |  v  |
-- > |  @  | ==> h--@  |
-- > j-/|  |     |  v  |
-- > |  v  |     +--R--+
-- > +--g--+
--
-- Any square like the one on the left factors through 'ranSquare'.
-- 'ranFactor' gives the remaining square.
ranFactor :: (Profunctor j, IsFList fs) => Square '[h, j] '[] fs '[g] -> Square '[h] '[] fs '[Ran j g]
ranFactor :: forall (j :: * -> * -> *) (fs :: [* -> *]) (h :: * -> * -> *)
       (g :: * -> *).
(Profunctor j, IsFList fs) =>
Square '[h, j] '[] fs '[g] -> Square '[h] '[] fs '[Ran j g]
ranFactor Square '[h, j] '[] fs '[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 a b. (a -> b) -> a -> b
$ \PlainP '[h] a b
h PlainF fs a
f -> forall (j :: * -> * -> *) (f :: * -> *) a.
(forall b. j a b -> f b) -> Ran j f a
Ran forall a b. (a -> b) -> a -> b
$ \j b b
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 '[h, j] '[] fs '[g]
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 b
j PlainP '[h] a b
h) PlainF fs a
f