{-# 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
import Data.Functor.Kan.Lan
import Data.Functor.Kan.Ran

-- |
-- > +--f--+
-- > |  v  |
-- > |  @  |
-- > | / \ |
-- > | v v |
-- > +-j-L-+
lanSquare :: Functor f => Square '[] '[] '[f] '[j, Lan j f]
lanSquare :: forall (f :: * -> *) (j :: * -> *).
Functor f =>
Square '[] '[] '[f] '[j, 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 a b. (a -> b) -> a -> b
$ \PlainP '[] a b
k -> forall {k} (h :: k -> *) (a :: k) (g :: k -> *).
h a -> Lan g h (g a)
glan forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PlainP '[] a b
k

-- |
-- > +--f--+     +--L--+
-- > |  v  |     |  v  |
-- > |  @  | ==> |  @  |
-- > | / \ |     |  |  |
-- > | v v |     |  v  |
-- > +-j-g-+     +--g--+
--
-- Any square like the one on the left factors through 'lanSquare'.
-- 'lanFactor' gives the remaining square.
lanFactor :: Functor g => Square '[] '[] '[f] '[j, g] -> Square '[] '[] '[Lan j f] '[g]
lanFactor :: forall (g :: * -> *) (f :: * -> *) (j :: * -> *).
Functor g =>
Square '[] '[] '[f] '[j, g] -> Square '[] '[] '[Lan j f] '[g]
lanFactor Square '[] '[] '[f] '[j, 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 '[] a b
k -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PlainP '[] a b
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: * -> *) (h :: k -> *) (g :: k -> *) b.
Functor f =>
(forall (a :: k). h a -> f (g a)) -> Lan g h b -> f b
toLan (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 '[] '[] '[f] '[j, g]
sq forall a. a -> a
id)

-- |
-- > +-j-R-+
-- > | v v |
-- > | \ / |
-- > |  @  |
-- > |  v  |
-- > +--g--+
ranSquare :: Functor g => Square '[] '[] '[j, Ran j g] '[g]
ranSquare :: forall (g :: * -> *) (j :: * -> *).
Functor 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
$ \PlainP '[] a b
k -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PlainP '[] a b
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (g :: k -> *) (h :: k -> *) (a :: k).
Ran g h (g a) -> h a
gran

-- |
-- > +-j-f-+     +--f--+
-- > | v v |     |  v  |
-- > | \ / | ==> |  @  |
-- > |  @  |     |  |  |
-- > |  v  |     |  v  |
-- > +--g--+     +--R--+
--
-- Any square like the one on the left factors through 'ranSquare'.
-- 'ranFactor' gives the remaining square.
ranFactor :: Functor f => Square '[] '[] '[j, f] '[g] -> Square '[] '[] '[f] '[Ran j g]
ranFactor :: forall (f :: * -> *) (j :: * -> *) (g :: * -> *).
Functor f =>
Square '[] '[] '[j, f] '[g] -> Square '[] '[] '[f] '[Ran j g]
ranFactor Square '[] '[] '[j, f] '[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 '[] a b
k -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PlainP '[] a b
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (k2 :: * -> *) (g :: k1 -> *) (h :: k1 -> *) b.
Functor k2 =>
(forall (a :: k1). k2 (g a) -> h a) -> k2 b -> Ran g h b
toRan (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, f] '[g]
sq forall a. a -> a
id)