{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal.Hypergraph where

import Data.Type.Nat (Nat (..), SNat (..), SNatI, snat)

import Proarrow.Category (Supplies)
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , leftUnitorInvWith
  , leftUnitorWith
  , par
  , rightUnitorInvWith
  , rightUnitorWith
  , (==)
  , (||)
  )
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj)
import Proarrow.Monoid (Comonoid (..), Monoid (..))
import Proarrow.Object.Dual (CompactClosed)

type family NFold (n :: Nat) (x :: k) :: k where
  NFold Z x = Unit
  NFold (S n) x = x ** NFold n x

withObNFold :: forall {k} n (a :: k) r. (SNatI n, Ob a, Monoidal k) => ((Ob (NFold n a)) => r) -> r
withObNFold :: forall {k} (n :: Nat) (a :: k) r.
(SNatI n, Ob a, Monoidal k) =>
(Ob (NFold n a) => r) -> r
withObNFold Ob (NFold n a) => r
r = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> r
Ob (NFold n a) => r
r
  SS @n' -> forall {k} (n :: Nat) (a :: k) r.
(SNatI n, Ob a, Monoidal k) =>
(Ob (NFold n a) => r) -> r
forall (n :: Nat) (a :: k) r.
(SNatI n, Ob a, Monoidal k) =>
(Ob (NFold n a) => r) -> r
withObNFold @n' @a (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @(NFold n' a) r
Ob (a ** NFold n1 a) => r
Ob (NFold n a) => r
r)

fanIn :: forall n a. (SNatI n, Monoid a) => NFold n a ~> a
fanIn :: forall {k} (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFold n a ~> a
fanIn = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> Unit ~> a
NFold n a ~> a
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  SS @n' -> forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a ((a ** a) ~> a)
-> ((a ** NFold n1 a) ~> (a ** a)) -> (a ** NFold n1 a) ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (NFold n1 a ~> a) -> (a ** NFold n1 a) ~> (a ** a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall {k} (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFold n a ~> a
forall (n :: Nat) (a :: k). (SNatI n, Monoid a) => NFold n a ~> a
fanIn @n' @a)

fanOut :: forall n a. (SNatI n, Comonoid a) => a ~> NFold n a
fanOut :: forall {k} (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
a ~> NFold n a
fanOut = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> a ~> Unit
a ~> NFold n a
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
  SS @n' -> (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (a ~> NFold n1 a) -> (a ** a) ~> (a ** NFold n1 a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall {k} (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
a ~> NFold n a
forall (n :: Nat) (a :: k). (SNatI n, Comonoid a) => a ~> NFold n a
fanOut @n' @a) ((a ** a) ~> (a ** NFold n1 a))
-> (a ~> (a ** a)) -> a ~> (a ** NFold n1 a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a

-- | We have a special frobenius algebra for an object if it is a monoid and a comonoid in a nice compatible way.
-- Then there's a unique way to go from n-fold @a@ to m-fold @a@.
class (Monoid a, Comonoid a) => Frobenius a where
  spider :: (SNatI n, SNatI m) => NFold n a ~> NFold m a

cup :: (Frobenius a) => Unit ~> a ** a
cup :: forall {k} (a :: k). Frobenius a => Unit ~> (a ** a)
cup @a = forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a (a ~> (a ** a)) -> (Unit ~> a) -> Unit ~> (a ** a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (m :: k). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty @a

cap :: (Frobenius a) => a ** a ~> Unit
cap :: forall {k} (a :: k). Frobenius a => (a ** a) ~> Unit
cap @a = forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @a (a ~> Unit) -> ((a ** a) ~> a) -> (a ** a) ~> Unit
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a

-- | Since spider has a (very) ambiguous type, it's not possible to give a default implementation.
-- Use this function to provide the implementation as follows:
--
-- > spider @n @m = spiderDefault @n @m @a
spiderDefault :: forall n m a. (Monoid a, Comonoid a, SNatI n, SNatI m) => NFold n a ~> NFold m a
spiderDefault :: forall {k} (n :: Nat) (m :: Nat) (a :: k).
(Monoid a, Comonoid a, SNatI n, SNatI m) =>
NFold n a ~> NFold m a
spiderDefault = forall {k} (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
a ~> NFold n a
forall (n :: Nat) (a :: k). (SNatI n, Comonoid a) => a ~> NFold n a
fanOut @m @a (a ~> NFold m a) -> (NFold n a ~> a) -> NFold n a ~> NFold m a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {k} (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFold n a ~> a
forall (n :: Nat) (a :: k). (SNatI n, Monoid a) => NFold n a ~> a
fanIn @n @a

-- | A hypergraph category has a special frobenius algebra for every object, and the
-- frobenius algebra of any tensor product X ⊗ Y is induced in the canonical way from those of X and Y.
class (k `Supplies` Frobenius, CompactClosed k) => Hypergraph k

-- | A hypergraph category is self-dual compact closed.
dualHG :: forall {k} (a :: k) b. (Hypergraph k) => a ~> b -> b ~> a
dualHG :: forall {k} (a :: k) (b :: k). Hypergraph k => (a ~> b) -> b ~> a
dualHG a ~> b
f =
  (Unit ~> (a ** a)) -> b ~> ((a ** a) ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(Unit ~> b) -> a ~> (b ** a)
leftUnitorInvWith (forall (a :: k). Frobenius a => Unit ~> (a ** a)
forall {k} (a :: k). Frobenius a => Unit ~> (a ** a)
cup @a)
    (b ~> ((a ** a) ** b))
-> (((a ** a) ** b) ~> ((a ** b) ** b)) -> b ~> ((a ** b) ** b)
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (a ~> b) -> (a ** a) ~> (a ** b)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
|| a ~> b
f ((a ** a) ~> (a ** b))
-> (b ~> b) -> ((a ** a) ** b) ~> ((a ** b) ** b)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
|| forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b
    (b ~> ((a ** b) ** b))
-> (((a ** b) ** b) ~> (a ** (b ** b))) -> b ~> (a ** (b ** b))
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @a @b @b
    (b ~> (a ** (b ** b))) -> ((a ** (b ** b)) ~> a) -> b ~> a
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== ((b ** b) ~> Unit) -> (a ** (b ** b)) ~> a
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (a ** b) ~> a
rightUnitorWith (forall (a :: k). Frobenius a => (a ** a) ~> Unit
forall {k} (a :: k). Frobenius a => (a ** a) ~> Unit
cap @b)
    ((Ob a, Ob b) => b ~> a) -> (a ~> b) -> b ~> a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> b
f

linDistHG :: forall {k} (a :: k) b c. (Hypergraph k, Ob a, Ob b) => a ** b ~> c -> a ~> b ** c
linDistHG :: forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ** c)
linDistHG (a ** b) ~> c
f =
  (Unit ~> (b ** b)) -> a ~> (a ** (b ** b))
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(Unit ~> b) -> a ~> (a ** b)
rightUnitorInvWith (forall (a :: k). Frobenius a => Unit ~> (a ** a)
forall {k} (a :: k). Frobenius a => Unit ~> (a ** a)
cup @b)
    (a ~> (a ** (b ** b)))
-> ((a ** (b ** b)) ~> ((a ** b) ** b)) -> a ~> ((a ** b) ** b)
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @a @b @b
    (a ~> ((a ** b) ** b))
-> (((a ** b) ** b) ~> (c ** b)) -> a ~> (c ** b)
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== (a ** b) ~> c
f ((a ** b) ~> c) -> (b ~> b) -> ((a ** b) ** b) ~> (c ** b)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
|| forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b
    (a ~> (c ** b)) -> ((c ** b) ~> (b ** c)) -> a ~> (b ** c)
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @c @b
    ((Ob (a ** b), Ob c) => a ~> (b ** c))
-> ((a ** b) ~> c) -> a ~> (b ** c)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ (a ** b) ~> c
f

linDistInvHG :: forall {k} (a :: k) b c. (Hypergraph k, Ob b, Ob c) => a ~> b ** c -> a ** b ~> c
linDistInvHG :: forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob b, Ob c) =>
(a ~> (b ** c)) -> (a ** b) ~> c
linDistInvHG a ~> (b ** c)
f =
  forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @b
    ((a ** b) ~> (b ** a))
-> ((b ** a) ~> (b ** (b ** c))) -> (a ** b) ~> (b ** (b ** c))
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b -> (a ~> (b ** c)) -> (b ** a) ~> (b ** (b ** c))
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
|| a ~> (b ** c)
f
    ((a ** b) ~> (b ** (b ** c)))
-> ((b ** (b ** c)) ~> ((b ** b) ** c))
-> (a ** b) ~> ((b ** b) ** c)
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @b @b @c
    ((a ** b) ~> ((b ** b) ** c))
-> (((b ** b) ** c) ~> c) -> (a ** b) ~> c
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== ((b ** b) ~> Unit) -> ((b ** b) ** c) ~> c
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
leftUnitorWith (forall (a :: k). Frobenius a => (a ** a) ~> Unit
forall {k} (a :: k). Frobenius a => (a ** a) ~> Unit
cap @b)
    ((Ob a, Ob (b ** c)) => (a ** b) ~> c)
-> (a ~> (b ** c)) -> (a ** b) ~> c
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> (b ** c)
f

-- | A hypergraph category has a trace
traceHG :: forall {k} u (x :: k) y. (Hypergraph k, Ob x, Ob y, Ob u) => u ** x ~> u ** y -> x ~> y
traceHG :: forall {k} (u :: k) (x :: k) (y :: k).
(Hypergraph k, Ob x, Ob y, Ob u) =>
((u ** x) ~> (u ** y)) -> x ~> y
traceHG (u ** x) ~> (u ** y)
f =
  (Unit ~> (u ** u)) -> x ~> ((u ** u) ** x)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(Unit ~> b) -> a ~> (b ** a)
leftUnitorInvWith (forall (a :: k). Frobenius a => Unit ~> (a ** a)
forall {k} (a :: k). Frobenius a => Unit ~> (a ** a)
cup @u)
    (x ~> ((u ** u) ** x))
-> (((u ** u) ** x) ~> (u ** (u ** x))) -> x ~> (u ** (u ** x))
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @u @u @x
    (x ~> (u ** (u ** x)))
-> ((u ** (u ** x)) ~> (u ** (u ** y))) -> x ~> (u ** (u ** y))
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @u Obj u
-> ((u ** x) ~> (u ** y)) -> (u ** (u ** x)) ~> (u ** (u ** y))
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
|| (u ** x) ~> (u ** y)
f
    (x ~> (u ** (u ** y)))
-> ((u ** (u ** y)) ~> ((u ** u) ** y)) -> x ~> ((u ** u) ** y)
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @u @u @y
    (x ~> ((u ** u) ** y)) -> (((u ** u) ** y) ~> y) -> x ~> y
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== ((u ** u) ~> Unit) -> ((u ** u) ** y) ~> y
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
leftUnitorWith (forall (a :: k). Frobenius a => (a ** a) ~> Unit
forall {k} (a :: k). Frobenius a => (a ** a) ~> Unit
cap @u)

type ExpHG a b = a ** b

curryHG :: forall {k} (a :: k) b c. (Hypergraph k, Ob a, Ob b) => a ** b ~> c -> a ~> ExpHG b c
curryHG :: forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ** c)
curryHG = forall (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ** c)
forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ** c)
linDistHG @a @b @c

applyHG :: forall {k} (b :: k) c. (Hypergraph k, Ob b, Ob c) => ExpHG b c ** b ~> c
applyHG :: forall {k} (b :: k) (c :: k).
(Hypergraph k, Ob b, Ob c) =>
(ExpHG b c ** b) ~> c
applyHG = forall (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob b, Ob c) =>
(a ~> (b ** c)) -> (a ** b) ~> c
forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob b, Ob c) =>
(a ~> (b ** c)) -> (a ** b) ~> c
linDistInvHG @_ @b (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b -> (c ~> c) -> (b ** c) ~> (b ** c)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c)