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

import Data.Square
import Data.Profunctor
import qualified Control.Comonad as W

-- |
-- > +--w--+
-- > |  v  |
-- > |  X  |
-- > |     |
-- > +-----+
extract :: W.Comonad w => Square '[] '[] '[w] '[]
extract :: forall (w :: * -> *). Comonad w => Square '[] '[] '[w] '[]
extract = 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 b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: * -> *) a. Comonad w => w a -> a
W.extract)

-- |
-- > +--w--+
-- > |  v  |
-- > w<-E  |
-- > |  v  |
-- > +--w--+
--
-- `W.extend` as a square
--
-- Right identity law:
--
-- > +--w--+
-- > |  v  |     +--w--+
-- > w<-E  |     |  v  |
-- > |  v  | === w<-/  |
-- > |  X  |     |     |
-- > +-----+     +-----+
--
-- Left identity law:
--
-- > +---w-+
-- > |   v |     +--w--+
-- > | /-E |     |  |  |
-- > | v | | === |  v  |
-- > | X v |     |  |  |
-- > +---w-+     +--w--+
--
-- Associativity law:
--
-- > +--w--+     +---w-+
-- > |  v  |     |   v |
-- > w<-E  |     | /-E |
-- > |  v  | === w<E | |
-- > w<-E  |     | | | |
-- > |  v  |     w</ v |
-- > +--w--+     +---w-+
extend :: W.Comonad w => Square '[Costar w] '[] '[w] '[w]
extend :: forall (w :: * -> *). Comonad w => Square '[Costar w] '[] '[w] '[w]
extend = 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 (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
W.extend forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (d :: k) c. Costar f d c -> f d -> c
runCostar)

-- |
-- > +---w-+
-- > |   v |
-- > | /-@ |
-- > | v v |
-- > +-w-w-+
--
-- > duplicate = fromRight ||| extend
duplicate :: W.Comonad w => Square '[] '[] '[w] '[w, w]
duplicate :: forall (w :: * -> *). Comonad w => Square '[] '[] '[w] '[w, w]
duplicate = 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)
||| forall (w :: * -> *). Comonad w => Square '[Costar w] '[] '[w] '[w]
extend

-- |
-- > +-----+
-- > |  /-<w
-- > w<-@  |
-- > w<-/  |
-- > +-----+
--
-- Cokleisli composition `(W.<=<)`
--
-- > (<=<) = fromRight === extend === toLeft
(<=<) :: W.Comonad w => Square '[Costar w, Costar w] '[Costar w] '[] '[]
<=< :: forall (w :: * -> *).
Comonad w =>
Square '[Costar w, Costar w] '[Costar w] '[] '[]
(<=<) = 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 (w :: * -> *). Comonad w => Square '[Costar w] '[] '[w] '[w]
extend 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