-- | The __opposite category__: the kind @'OPPOSITE' k@ wraps @k@ in 'OP', and an arrow
-- @'OP' a '~>' 'OP' b@ is an arrow @b '~>' a@ of @k@. 'Op' (and its inverse 'UnOp') also flips
-- profunctors, swapping their two arguments -- the prototypical use of a newtype wrapper on a kind
-- to give one collection of types a second category structure.
module Proarrow.Category.Instance.Opposite where

import Proarrow.Category.Enriched.Thin
  ( AtOb (..)
  , DecidableProfunctor (..)
  , Enumerable (..)
  , Finite (..)
  , FmapWrap
  , Indexed (..)
  , MapWrap
  , Thin
  , ThinProfunctor (..)
  , atOb
  , mapDecision
  , withWrapAtLookup
  , wrapFinite
  )
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), UN, WrappedOb, lmap, type (+->))
import Proarrow.Functor (Functor (..))

newtype OPPOSITE k = OP k

-- | Flips the two arguments of a profunctor, giving a profunctor between the 'OPPOSITE'
-- categories; at @p = ('~>')@ this is the hom of the opposite category.
type Op :: j +-> k -> OPPOSITE k +-> OPPOSITE j
data Op p a b where
  Op :: {forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
Op p ('OP a) ('OP b) -> p b a
unOp :: p b a} -> Op p (OP a) (OP b)

instance (Profunctor p) => Functor (Op p a) where
  map :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(a ~> b) -> Op p a a ~> Op p a b
map (Op b ~> a
f) (Op p b a
p) = p b a -> Op p ('OP a) ('OP b)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op ((b ~> b) -> p b a -> p b a
forall (c :: k) (a :: k) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap b ~> a
b ~> b
f p b a
p)

instance (Profunctor p) => Profunctor (Op p) where
  dimap :: forall (c :: OPPOSITE j) (a :: OPPOSITE j) (b :: OPPOSITE k)
       (d :: OPPOSITE k).
(c ~> a) -> (b ~> d) -> Op p a b -> Op p c d
dimap (Op b ~> a
l) (Op b ~> a
r) = p b a -> Op p ('OP a) ('OP b)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (p b a -> Op p ('OP a) ('OP b))
-> (Op p ('OP b) ('OP a) -> p b a)
-> Op p ('OP b) ('OP a)
-> Op p ('OP a) ('OP b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (b ~> a) -> (b ~> a) -> p a b -> p b a
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap b ~> a
r b ~> a
l (p a b -> p b a)
-> (Op p ('OP b) ('OP a) -> p a b) -> Op p ('OP b) ('OP a) -> p b a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Op p ('OP b) ('OP a) -> p a b
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
Op p ('OP a) ('OP b) -> p b a
unOp
  (Ob a, Ob b) => r
r \\ :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r.
((Ob a, Ob b) => r) -> Op p a b -> r
\\ Op p b a
f = r
(Ob b, Ob a) => r
(Ob a, Ob b) => r
r ((Ob b, Ob a) => r) -> p b a -> r
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p b a
f

instance Functor Op where
  map :: forall (a :: j +-> k) (b :: j +-> k). (a ~> b) -> Op a ~> Op b
map (Prof a :~> b
n) = (Op a :~> Op b) -> Prof (Op a) (Op b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Op a b a
p) -> b b a -> Op b ('OP a) ('OP b)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (a b a -> b b a
a :~> b
n a b a
p)

-- | The opposite category of the category of `k`.
instance (CategoryOf k) => CategoryOf (OPPOSITE k) where
  type (~>) = Op (~>)
  type Ob a = WrappedOb OP a

instance (Promonad c) => Promonad (Op c) where
  id :: forall (a :: OPPOSITE j). Ob a => Op c a a
id = c (UN 'OP a) (UN 'OP a) -> Op c ('OP (UN 'OP a)) ('OP (UN 'OP a))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op c (UN 'OP a) (UN 'OP a)
forall (a :: j). Ob a => c a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  Op c b a
f . :: forall (b :: OPPOSITE j) (c :: OPPOSITE j) (a :: OPPOSITE j).
Op c b c -> Op c a b -> Op c a c
. Op c b a
g = c b a -> Op c ('OP a) ('OP b)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (c b a
g c b a -> c b b -> c b a
forall (b :: j) (c :: j) (a :: j). c b c -> c a b -> c a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c b a
c b b
f)

instance (ThinProfunctor p) => ThinProfunctor (Op p) where
  type HasArrow (Op p) (OP a) (OP b) = HasArrow p b a
  arr :: forall (a :: OPPOSITE j) (b :: OPPOSITE k).
(Ob a, Ob b, HasArrow (Op p) a b) =>
Op p a b
arr = p (UN 'OP b) (UN 'OP a) -> Op p ('OP (UN 'OP a)) ('OP (UN 'OP b))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op p (UN 'OP b) (UN 'OP a)
forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow p a b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr
  withArr :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r.
Op p a b -> ((HasArrow (Op p) a b, Ob a, Ob b) => r) -> r
withArr (Op p b a
f) (HasArrow (Op p) a b, Ob a, Ob b) => r
r = p b a -> ((HasArrow p b a, Ob b, Ob a) => r) -> r
forall (a :: k) (b :: j) r.
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr p b a
f r
(HasArrow p b a, Ob b, Ob a) => r
(HasArrow (Op p) a b, Ob a, Ob b) => r
r

instance (DecidableProfunctor p) => DecidableProfunctor (Op p) where
  type Holds (Op p) (OP a) (OP b) = Holds p b a
  decide :: forall (a :: OPPOSITE j) (b :: OPPOSITE k).
(Ob a, Ob b) =>
Decision (Op p) a b (Holds (Op p) a b)
decide @(OP a) @(OP b) = (p (UN 'OP b) (UN 'OP a) -> Op p a b)
-> Decision p (UN 'OP b) (UN 'OP a) (Holds p (UN 'OP b) (UN 'OP a))
-> Decision (Op p) a b (Holds p (UN 'OP b) (UN 'OP a))
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision p (UN 'OP b) (UN 'OP a) -> Op p a b
p (UN 'OP b) (UN 'OP a) -> Op p ('OP (UN 'OP a)) ('OP (UN 'OP b))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @b @a)
  toHolds :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r.
Op p a b -> ((Holds (Op p) a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds (Op p b a
f) (Holds (Op p) a b ~ 'TRU, Ob a, Ob b) => r
r = p b a -> ((Holds p b a ~ 'TRU, Ob b, Ob a) => r) -> r
forall (a :: k) (b :: j) r.
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds p b a
f r
(Holds p b a ~ 'TRU, Ob b, Ob a) => r
(Holds (Op p) a b ~ 'TRU, Ob a, Ob b) => r
r

-- | Inverse to 'Op': unwraps a profunctor between 'OPPOSITE' categories to one between the
-- underlying kinds.
type UnOp :: OPPOSITE k +-> OPPOSITE j -> j +-> k
data UnOp p a b where
  UnOp :: {forall {k} {k} (p :: OPPOSITE k +-> OPPOSITE k) (b :: k) (a :: k).
UnOp p a b -> p ('OP b) ('OP a)
unUnOp :: p (OP b) (OP a)} -> UnOp p a b

instance (CategoryOf j, CategoryOf k, Profunctor p) => Profunctor (UnOp p :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> UnOp p a b -> UnOp p c d
dimap c ~> a
l b ~> d
r = p ('OP d) ('OP c) -> UnOp p c d
forall {k} {k} (p :: OPPOSITE k +-> OPPOSITE k) (b :: k) (a :: k).
p ('OP b) ('OP a) -> UnOp p a b
UnOp (p ('OP d) ('OP c) -> UnOp p c d)
-> (UnOp p a b -> p ('OP d) ('OP c)) -> UnOp p a b -> UnOp p c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ('OP d ~> 'OP b)
-> ('OP a ~> 'OP c) -> p ('OP b) ('OP a) -> p ('OP d) ('OP c)
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall (c :: OPPOSITE j) (a :: OPPOSITE j) (b :: OPPOSITE k)
       (d :: OPPOSITE k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap ((b ~> d) -> Op (~>) ('OP d) ('OP b)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op b ~> d
r) ((c ~> a) -> Op (~>) ('OP a) ('OP c)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op c ~> a
l) (p ('OP b) ('OP a) -> p ('OP d) ('OP c))
-> (UnOp p a b -> p ('OP b) ('OP a))
-> UnOp p a b
-> p ('OP d) ('OP c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. UnOp p a b -> p ('OP b) ('OP a)
forall {k} {k} (p :: OPPOSITE k +-> OPPOSITE k) (b :: k) (a :: k).
UnOp p a b -> p ('OP b) ('OP a)
unUnOp
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> UnOp p a b -> r
\\ UnOp p ('OP b) ('OP a)
f = r
(Ob a, Ob b) => r
(Ob ('OP b), Ob ('OP a)) => r
r ((Ob ('OP b), Ob ('OP a)) => r) -> p ('OP b) ('OP a) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: OPPOSITE j) (b :: OPPOSITE k) r.
((Ob a, Ob b) => r) -> p a b -> r
\\ p ('OP b) ('OP a)
f

instance (Thin j, Thin k, ThinProfunctor p) => ThinProfunctor (UnOp p :: j +-> k) where
  type HasArrow (UnOp p) a b = HasArrow p (OP b) (OP a)
  arr :: forall (a :: k) (b :: j).
(Ob a, Ob b, HasArrow (UnOp p) a b) =>
UnOp p a b
arr = Op (UnOp p) ('OP b) ('OP a) -> UnOp p a b
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
Op p ('OP a) ('OP b) -> p b a
unOp Op (UnOp p) ('OP b) ('OP a)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (a :: OPPOSITE j) (b :: OPPOSITE k).
(Ob a, Ob b, HasArrow (Op (UnOp p)) a b) =>
Op (UnOp p) a b
arr
  withArr :: forall (a :: k) (b :: j) r.
UnOp p a b -> ((HasArrow (UnOp p) a b, Ob a, Ob b) => r) -> r
withArr UnOp p a b
f (HasArrow (UnOp p) a b, Ob a, Ob b) => r
r = Op (UnOp p) ('OP b) ('OP a)
-> ((HasArrow (Op (UnOp p)) ('OP b) ('OP a), Ob ('OP b),
     Ob ('OP a)) =>
    r)
-> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall (a :: OPPOSITE j) (b :: OPPOSITE k) r.
Op (UnOp p) a b
-> ((HasArrow (Op (UnOp p)) a b, Ob a, Ob b) => r) -> r
withArr (UnOp p a b -> Op (UnOp p) ('OP b) ('OP a)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op UnOp p a b
f) r
(HasArrow (UnOp p) a b, Ob a, Ob b) => r
(HasArrow (Op (UnOp p)) ('OP b) ('OP a), Ob ('OP b), Ob ('OP a)) =>
r
r

instance (Thin j, Thin k, DecidableProfunctor p) => DecidableProfunctor (UnOp p :: j +-> k) where
  type Holds (UnOp p) a b = Holds p (OP b) (OP a)
  decide :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
Decision (UnOp p) a b (Holds (UnOp p) a b)
decide @a @b = (p ('OP b) ('OP a) -> UnOp p a b)
-> Decision p ('OP b) ('OP a) (Holds p ('OP b) ('OP a))
-> Decision (UnOp p) a b (Holds p ('OP b) ('OP a))
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision p ('OP b) ('OP a) -> UnOp p a b
forall {k} {k} (p :: OPPOSITE k +-> OPPOSITE k) (b :: k) (a :: k).
p ('OP b) ('OP a) -> UnOp p a b
UnOp (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: OPPOSITE k +-> OPPOSITE j) (a :: OPPOSITE j)
       (b :: OPPOSITE k).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @(OP b) @(OP a))
  toHolds :: forall (a :: k) (b :: j) r.
UnOp p a b -> ((Holds (UnOp p) a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds (UnOp p ('OP b) ('OP a)
f) (Holds (UnOp p) a b ~ 'TRU, Ob a, Ob b) => r
r = p ('OP b) ('OP a)
-> ((Holds p ('OP b) ('OP a) ~ 'TRU, Ob ('OP b), Ob ('OP a)) => r)
-> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall (a :: OPPOSITE j) (b :: OPPOSITE k) r.
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds p ('OP b) ('OP a)
f r
(Holds (UnOp p) a b ~ 'TRU, Ob a, Ob b) => r
(Holds p ('OP b) ('OP a) ~ 'TRU, Ob ('OP b), Ob ('OP a)) => r
r

-- | The opposite category has the same objects, numbered the same way.
instance (Indexed k) => Indexed (OPPOSITE k) where
  type Index (a :: OPPOSITE k) = Index (UN OP a)
  type At (OPPOSITE k) i = FmapWrap OP (At k i)

instance (Finite k) => Finite (OPPOSITE k) where
  type Objects (OPPOSITE k) = MapWrap OP (Objects k)
  finite :: IndexedList (Objects (OPPOSITE k))
finite = forall {j} {k} (w :: j -> k).
(Finite j, forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList (MapWrap w (Objects j))
forall (w :: k -> OPPOSITE k).
(Finite k, forall (a :: k). KnownIndex a => KnownIndex (w a)) =>
IndexedList (MapWrap w (Objects k))
wrapFinite @OP
  withAtLookup :: forall (i :: Nat) r.
SNat i
-> ((Lookup (Objects (OPPOSITE k)) i ~ At (OPPOSITE k) i) => r)
-> r
withAtLookup = forall {j} {k} (w :: j -> k) (i :: Nat) r.
Finite j =>
SNat i
-> ((Lookup (MapWrap w (Objects j)) i ~ FmapWrap w (At j i)) => r)
-> r
forall (w :: k -> OPPOSITE k) (i :: Nat) r.
Finite k =>
SNat i
-> ((Lookup (MapWrap w (Objects k)) i ~ FmapWrap w (At k i)) => r)
-> r
withWrapAtLookup @OP

instance (Enumerable k) => Enumerable (OPPOSITE k) where
  withIndex :: forall (a :: OPPOSITE k) r. Ob a => (KnownIndex a => r) -> r
withIndex @(OP a) KnownIndex a => r
r = forall k (a :: k) r.
(Enumerable k, Ob a) =>
(KnownIndex a => r) -> r
withIndex @k @a r
KnownIndex (UN 'OP a) => r
KnownIndex a => r
r
  atOb :: forall (i :: Nat). SNat i -> AtOb (OPPOSITE k) (At (OPPOSITE k) i)
atOb SNat i
i = case forall k (i :: Nat). Enumerable k => SNat i -> AtOb k (At k i)
atOb @k SNat i
i of
    AtOb k (At k i)
AtJust -> AtOb (OPPOSITE k) ('Just ('OP a))
AtOb (OPPOSITE k) (At (OPPOSITE k) i)
forall k (a :: k). (Ob a, KnownIndex a) => AtOb k ('Just a)
AtJust
    AtOb k (At k i)
AtNothing -> AtOb (OPPOSITE k) 'Nothing
AtOb (OPPOSITE k) (At (OPPOSITE k) i)
forall k. AtOb k 'Nothing
AtNothing