Proarrow equipment in Hask

equipment.hs

{-# LANGUAGE
    GADTs
  , DataKinds
  , PolyKinds
  , RankNTypes
  , TypeOperators
  , KindSignatures
  , TypeApplications
  , FlexibleContexts
  , FlexibleInstances
  , AllowAmbiguousTypes
  , ScopedTypeVariables
  , QuantifiedConstraints
  , MultiParamTypeClasses
  , StandaloneKindSignatures
  #-}
module Equipment where

import Prelude hiding ((.), id, curry)
import Data.Profunctor
import Data.Bifunctor.Tannen
import qualified Data.Profunctor.Composition as P
import Data.Singletons.Prelude.List
import Data.Kind
import Control.Category
import qualified Control.Arrow as A

-- A--f--B
-- |  v  |
-- p--@--q
-- |  v  |
-- C--g--D
type GSquare :: (a -> b -> Type) -> (c -> d -> Type) -> (a -> c) -> (b -> d) -> Type
type GSquare p q f g = forall a b. p a b -> q (f a) (g b)

type Square p q f g = GSquare (PList p) (PList q) (FList f) (FList g)


-- | Combine two profunctors from Hask to a profunctor from Hask x Hask
data (p1 :**: p2) a b where
  (:**:) :: p1 a1 b1 -> p2 a2 b2 -> (p1 :**: p2) '(a1, a2) '(b1, b2)

data UncurryF f a where
  UncurryF :: { curryF :: f a b } -> UncurryF f '(a, b)

-- 2--f--1
-- |  v  |
-- p--@--q     1 = Hask, 2 = Hask x Hask
-- |  v  |
-- 2--g--1
type Square21 p1 p2 q f g = GSquare (PList p1 :**: PList p2) (PList q) (UncurryF f) (UncurryF g)


data Unit a b where
  Unit :: Unit '() '()

data ValueF x u where
  ValueF :: a -> ValueF a '()

-- 0--a--1
-- |  v  |
-- |  @--q     0 = Hask^0 = (), 1 = Hask
-- |  v  |
-- 0--b--1
type Square01 q a b = GSquare Unit (PList q) (ValueF a) (ValueF b)


-- FList '[f, g, h] = h (g (f a))
data FList (fs :: [* -> *]) (a :: *) where
  Id :: { unId :: a } -> FList '[] a
  F :: { unF :: f a } -> FList '[f] a
  Compose :: { getCompose :: FList (g ': gs) (f a) } -> FList (f ': g ': gs) a

instance Functor (FList '[]) where
  fmap f = Id . f . unId
instance Functor f => Functor (FList '[f]) where
  fmap f = F . fmap f . unF
instance (Functor f, Functor (FList (g ': gs))) => Functor (FList (f ': g ': gs)) where
  fmap f = Compose . fmap (fmap f) . getCompose

class FAppend f where
  fappend :: Functor (FList g) => FList g (FList f a) -> FList (f ++ g) a
  funappend :: Functor (FList g) => FList (f ++ g) a -> FList g (FList f a)
instance FAppend '[] where
  fappend = fmap unId
  funappend = fmap Id
instance FAppend '[f] where
  fappend (Id fa) = F (unF fa)
  fappend f@F{} = Compose $ fmap unF f
  fappend f@Compose{} = Compose $ fmap unF f
  funappend fa@F{} = Id fa
  funappend (Compose fga@F{}) = fmap F fga
  funappend (Compose fga@Compose{}) = fmap F fga
instance (Functor f, FAppend (g ': gs)) => FAppend (f ': g ': gs) where
  fappend = Compose . fappend . fmap getCompose
  funappend = fmap Compose . funappend . getCompose


-- +--f--+     +--h--+       +-f;h-+
-- |  v  |     |  v  |       |  v  |
-- p--@--q ||| q--@--r  ==>  p--@--r
-- |  v  |     |  v  |       |  v  |
-- +--g--+     +--i--+       +-g;i-+

infixl 6 |||
(|||) :: (Profunctor (PList r), FAppend f, FAppend g, Functor (FList h), Functor (FList i)) => Square p q f g -> Square q r h i -> Square p r (f ++ h) (g ++ i)
pq ||| qr = dimap funappend fappend . qr . pq

-- +-----+
-- |     |
-- p-----p
-- |     |
-- +-----+
type Pro p = Square '[p] '[p] '[] '[]
idPro :: Profunctor p => Pro p
idPro = dimap unId Id


data PList (ps :: [* -> * -> *]) (a :: *) (b :: *) where
  Hom :: { unHom :: a -> b } -> PList '[] a b
  P :: { unP :: p a b } -> PList '[p] a b
  Procompose :: p a x -> PList (q ': qs) x b -> PList (p ': q ': qs) a b

instance Profunctor (PList '[]) where
  dimap l r (Hom f) = Hom (r . f . l)
instance Profunctor p => Profunctor (PList '[p]) where
  dimap l r (P p) = P (dimap l r p)
instance (Profunctor p, Profunctor (PList (q ': qs))) => Profunctor (PList (p ': q ': qs)) where
  dimap l r (Procompose p ps) = Procompose (lmap l p) (rmap r ps)

class PAppend p where
  pappend :: Profunctor (PList q) => P.Procompose (PList q) (PList p) a b -> PList (p ++ q) a b
  punappend :: PList (p ++ q) a b -> P.Procompose (PList q) (PList p) a b
instance PAppend '[] where
  pappend (P.Procompose q (Hom f)) = lmap f q
  punappend q = P.Procompose q (Hom id)
instance Profunctor p => PAppend '[p] where
  pappend (P.Procompose (Hom f) (P p)) = P (rmap f p)
  pappend (P.Procompose q@P{} (P p)) = Procompose p q
  pappend (P.Procompose q@Procompose{} (P p)) = Procompose p q
  punappend p@P{} = P.Procompose (Hom id) p
  punappend (Procompose p qs) = P.Procompose qs (P p)
instance (Profunctor p, PAppend (q ': qs)) => PAppend (p ': q ': qs) where
  pappend (P.Procompose q (Procompose p ps)) = Procompose p (pappend (P.Procompose q ps))
  punappend (Procompose p pq) = case punappend pq of P.Procompose q ps -> P.Procompose q (Procompose p ps)


-- +--f--+
-- |  v  |
-- p--@--q
-- |  v  |
-- +--g--+
--   ===
-- +--g--+
-- |  v  |
-- r--@--s
-- |  v  |
-- +--h--+
--
--   ==>
--
-- +--f--+
-- p  v  q
-- ;--@--;
-- r  v  s
-- +--h--+

infixl 5 ===
(===) :: (PAppend p, PAppend q, Profunctor (PList s)) => Square p q f g -> Square r s g h -> Square (p ++ r) (q ++ s) f h
(pq === rs) pr = case punappend pr of P.Procompose r p -> pappend (P.Procompose (rs r) (pq p))

-- +--f--+
-- |  |  |
-- |  v  |
-- |  |  |
-- +--f--+
type Fun f = Square '[] '[] '[f] '[f]
idArr :: Functor f => Fun f
idArr (Hom f) = Hom (fmap f)

-- +-----+
-- |     |
-- |  /-<f
-- |  v  |
-- +--f--+
fromRight :: Functor f => Square '[] '[Costar f] '[] '[f]
fromRight (Hom f) = P (Costar (F . fmap (f . unId)))

-- +--f--+
-- |  v  |
-- f<-/  |
-- |     |
-- +-----+
toLeft :: Square '[Costar f] '[] '[f] '[]
toLeft (P (Costar f)) = Hom (Id . f . unF)

-- +-----+
-- |     |
-- f>-\  |
-- |  v  |
-- +--f--+
fromLeft :: Square '[Star f] '[] '[] '[f]
fromLeft (P (Star f)) = Hom (F . f . unId)

-- +--f--+
-- |  v  |
-- |  \->f
-- |     |
-- +-----+
toRight :: Functor f => Square '[] '[Star f] '[f] '[]
toRight (Hom f) = P (Star (fmap (Id . f) . unF))

-- +-----+
-- |  /-<f
-- |  v  |
-- f<-/  |
-- +-----+
companionPcomp :: Functor f => Pro (Costar f)
companionPcomp =
  fromRight
  ===
  toLeft

-- +---f-+
-- |   v |
-- | /</ |
-- | v   |
-- +-f---+
companionFcomp :: Functor f => Fun f
companionFcomp = fromRight ||| toLeft

-- +-----+
-- f>-\  |
-- |  v  |
-- |  \->f
-- +-----+
conjointPcomp :: Functor f => Pro (Star f)
conjointPcomp =
  fromLeft
  ===
  toRight

-- +-f---+
-- | v   |
-- | \>\ |
-- |   v |
-- +---f-+
conjointFcomp :: Functor f => Fun f
conjointFcomp = toRight ||| fromLeft

-- +-----+
-- f>-\  |
-- |  v  |
-- f<-/  |
-- +-----+
uLeft :: Functor f => Square '[Star f, Costar f] '[] '[] '[]
uLeft =
  fromLeft
  ===
  toLeft

-- +-----+
-- |  /-<f
-- |  v  |
-- |  \->f
-- +-----+
uRight :: Functor f => Square '[] '[Costar f, Star f] '[] '[]
uRight =
  fromRight
  ===
  toRight


centralLemma :: (Profunctor p, Profunctor q, Functor f1, Functor f2, Functor f3, Functor g1, Functor g2, Functor g3)
  => Square '[p] '[q] '[f1, f2, f3] '[g1, g2, g3]
  -> Square '[Star f1, p, Costar g1] '[Costar f3, q, Star g3] '[f2] '[g2]
centralLemma n =
  fromLeft ||| idArr ||| fromRight
  ===
  n
  ===
  toLeft ||| idArr ||| toRight

centralLemma' :: (Profunctor p, Profunctor q, Functor f1, Functor f2, Functor f3, Functor g1, Functor g2, Functor g3)
  => Square '[Star f1, p, Costar g1] '[Costar f3, q, Star g3] '[f2] '[g2]
  -> Square '[p] '[q] '[f1, f2, f3] '[g1, g2, g3]
centralLemma' n = (toRight === idPro === fromRight) ||| n ||| (toLeft === idPro === fromLeft)



-- +-----+
-- |     |
-- |  @  |
-- |  v  |
-- +--X--+
value :: x -> Square '[] '[] '[] '[(,) x]
value x (Hom f) = Hom $ \(Id a) -> F (x, f a)

-- +--f--+
-- |  v  |
-- |  @  |
-- |  v  |
-- +--g--+
nat :: (Functor f, Functor g) => (forall a. f a -> g a) -> Square '[] '[] '[f] '[g]
nat n (Hom f) = Hom $ \(F g) -> F (fmap f (n g))

-- +-----+
-- |     |
-- |  @  |
-- |  v  |
-- +--f--+
pureSq :: Applicative f => Square '[] '[] '[] '[f]
pureSq (Hom f) = Hom $ \(Id a) -> F (pure (f a))

-- +--f--+
-- |  v  |
-- T--@  |
-- |  v  |
-- +--f--+
apSq :: Applicative f => Square '[Tannen f (->)] '[] '[f] '[f]
apSq (P (Tannen fab)) = Hom $ \(F fa) -> F (fab <*> fa)

-- +--t--+
-- |  v  |
-- f>-@->f
-- |  v  |
-- +--t--+
traverseSq :: (Traversable t, Applicative f) => Square '[Star f] '[Star f] '[t] '[t]
traverseSq (P (Star afb)) = P (Star (fmap F . traverse afb . unF))

-- +-f-t---+
-- | v v   |
-- | \-@-\ |
-- |   v v |
-- +---t-f-+
sequenceSq :: (Traversable t, Applicative f) => Square '[] '[] '[f, t] '[t, f]
sequenceSq = toRight ||| traverseSq ||| fromLeft

-- +-f-----+
-- | v /--<t
-- | \-@-\ |
-- t<--/ v |
-- +-----f-+
-- (t a -> b) -> t (f a) -> f b
cocollectSq :: (Traversable t, Applicative f) => Square '[Costar t] '[Costar t] '[f] '[f]
cocollectSq =
  idArr  ||| fromRight
  ===
  sequenceSq
  ===
  toLeft ||| idArr

-- +--t---+
-- |  v   |
-- f>-@-\ |
-- |  v | |
-- t<-/ v |
-- +----f-+
-- (a -> f x) -> (t x -> b) -> t a -> f b
someTravSq :: (Traversable t, Applicative f) => Square '[Star f, Costar t] '[] '[t] '[f]
someTravSq =
  traverseSq ||| fromLeft
  ===
  toLeft     ||| idArr


-- +--m--+
-- |  v  |
-- m>-@  |
-- |  v  |
-- +--m--+
-- (>>=)
bindSq :: (Monad m) => Square '[Star m] '[] '[m] '[m]
bindSq (P (Star amb)) = Hom $ \(F ma) -> F (ma >>= amb)

-- +-m-m-+
-- | v v |
-- | \-@ |
-- |   v |
-- +---m-+
joinSq :: (Monad m) => Square '[] '[] '[m, m] '[m]
joinSq = toRight ||| bindSq

-- +-----+
-- m>-\  |
-- m>-@  |
-- |  \->m
-- +-----+
-- (>=>)
kleisliCompSq :: (Monad m) => Square '[Star m, Star m] '[Star m] '[] '[]
kleisliCompSq = fromLeft === bindSq === toRight


-- +-----+
-- |     |
-- →--@  |
-- |     |
-- +-----+
homSq :: Square '[(->)] '[] '[] '[]
homSq (P f) = Hom (dimap unId Id f)

-- +-----+
-- →-\   |
-- p--@--p
-- →-/   |
-- +-----+
dimapSq :: Profunctor p => Square '[(->), p, (->)] '[p] '[] '[]
dimapSq = homSq === idPro === homSq

-- +-_⊗a-+
-- |  v  |
-- p--@--p
-- |  v  |
-- +-_⊗a-+
secondSq :: Strong p => Square '[p] '[p] '[(,) a] '[(,) a]
secondSq (P p) = P (dimap unF F (second' p))

-- +-_⊕a-+
-- |  v  |
-- p--@--p
-- |  v  |
-- +-_⊕a-+
rightSq :: Choice p => Square '[p] '[p] '[Either a] '[Either a]
rightSq (P p) = P (dimap unF F (right' p))

-- +-a→_-+
-- |  v  |
-- p--@--p
-- |  v  |
-- +-a→_-+
closedSq :: Closed p => Square '[p] '[p] '[(->) a] '[(->) a]
closedSq (P p) = P (dimap unF F (closed p))

-- +--f--+
-- |  v  |
-- p--@--p
-- |  v  |
-- +--f--+
mapSq :: (Mapping p, Functor f) => Square '[p] '[p] '[f] '[f]
mapSq (P p) = P (dimap unF F (map' p))

-- 0--()-1
-- |  v  |
-- |  @--p
-- |  v  |
-- 0--()-1
pureP :: (forall a. Applicative (p a), Profunctor p) => Square01 '[p] () ()
pureP Unit = P (pure (ValueF ()))

-- 2-(,)-1
-- |  v  |
-- p²-@--p
-- |  v  |
-- 2-(,)-1
-- p a b -> p c d -> p (a, c) (b, d)
apP :: (forall a. Applicative (p a), Profunctor p) => Square21 '[p] '[p] '[p] (,) (,)
apP (P f :**: P g) = P ((\b1 b2 -> UncurryF (b1, b2)) <$> lmap (fst . curryF) f <*> lmap (snd . curryF) g)


-- +-----+
-- |     |
-- |  @--a
-- |     |
-- +-----+
arrowArr :: A.Arrow a => Square '[] '[a] '[] '[]
arrowArr (Hom f) = P (A.arr (Id . f . unId))

-- +-----+
-- a--\  |
-- |  @--a
-- a--/  |
-- +-----+
arrowComp :: A.Arrow a => Square '[a, a] '[a] '[] '[]
arrowComp (Procompose p (P q)) = P (A.arr Id . q . p . A.arr unId)

-- +-_⊗d-+
-- |  v  |
-- a--@--a
-- |  v  |
-- +-_⊗d-+
arrowSecond :: A.Arrow a => Square '[a] '[a] '[(,) d] '[(,) d]
arrowSecond (P p) = P (A.arr F . A.second p . A.arr unF)

-- 2--⊗--1
-- |  v  |
-- a²-@--a
-- |  v  |
-- 2--⊗--1
arrowProd :: A.Arrow a => Square21 '[a] '[a] '[a] (,) (,)
arrowProd (P p1 :**: P p2) = P (A.arr UncurryF . (p1 A.*** p2) . A.arr curryF)

-- +-_⊕d-+
-- |  v  |
-- a--@--a
-- |  v  |
-- +-_⊕d-+
arrowRight :: A.ArrowChoice a => Square '[a] '[a] '[Either d] '[Either d]
arrowRight (P p) = P (A.arr F . A.right p . A.arr unF)

-- 2--⊕--1
-- |  v  |
-- a²-@--a
-- |  v  |
-- 2--⊕--1
arrowSum :: A.ArrowChoice a => Square21 '[a] '[a] '[a] Either Either
arrowSum (P p1 :**: P p2) = P (A.arr UncurryF . (p1 A.+++ p2) . A.arr curryF)


class (Functor f, Functor g) => Adjunction f g where
  -- +-----+
  -- |     |
  -- f<-@->g
  -- |     |
  -- +-----+
  leftAdj :: Square '[Costar f] '[Star g] '[] '[]
  -- +-----+
  -- |     |
  -- g>-@-<f
  -- |     |
  -- +-----+
  rightAdj :: Square '[Star g] '[Costar f] '[] '[]

-- +---------+
-- |         |
-- | /<-@->\ |
-- | v     v |
-- +-f-----g-+
unitAdj :: Adjunction f g => Square '[] '[] '[] '[f, g]
unitAdj = fromRight ||| leftAdj ||| fromLeft

-- +-g-----f-+
-- | v     v |
-- | \>-@-</ |
-- |         |
-- +---------+
counitAdj :: Adjunction f g => Square '[] '[] '[g, f] '[]
counitAdj = toRight ||| rightAdj ||| toLeft

-- +-------------f-+
-- | /<-@->\     | |
-- | v     v     | |
-- | |     \>-@-</ |
-- +-f-------------+
zigzagf :: forall f g. Adjunction f g => Fun f
zigzagf =
  unitAdj @f @g ||| idArr
  ===
  idArr ||| counitAdj @f @g

-- +-g-------------+
-- | |     /<-@->\ |
-- | v     v     | |
-- | \>-@-</     | |
-- +-------------g-+
zigzagg :: forall f g. Adjunction f g => Fun g
zigzagg =
  idArr ||| unitAdj @f @g
  ===
  counitAdj @f @g ||| idArr


newtype WLimit j f a = WLimit { getWLimit :: forall b. j a b -> f b }
instance Profunctor j => Functor (WLimit j f) where
  fmap f (WLimit g) = WLimit (g . lmap f)

-- +--l--+
-- |  v  |
-- j--@  |
-- |  v  |
-- +--f--+
-- forall a b. j a b -> WLimit j f b -> f a
wlimit :: Square '[j] '[] '[WLimit j f] '[f]
wlimit (P j) = Hom (F . ($ j) . getWLimit . unF)

fromWLimit :: Functor h => Square '[j] '[] '[h] '[f] -> Square '[] '[] '[h] '[WLimit j f]
fromWLimit n (Hom f) = Hom $ \h -> F (WLimit (unF . ($ fmap f h) . unHom . n . P))

FYI toLeft doesn't require a Functor f constraint.

It seems like fromLeft shouldn't require a Functor f constraint either, because it's doing (a -> f b) -> a -> f b. I can't see how to remove it though.

Anyway, these are very minor observations. This is very cool stuff!