{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Isomix categories: *-autonomous categories whose two units agree, @'Dual' 'Unit'@, the unit of
-- par, being isomorphic to 'Unit' ('dualUnit'). Then a dual and its object can be joined into the
-- unit of the tensor, not just into the unit of par. Every compact closed category is isomix, and
-- so is 'Proarrow.Category.Instance.Linear.LINEAR', where tensor and par still differ.
module Proarrow.Category.Monoidal.IsoMix where

import Data.Kind (Constraint)
import Prelude qualified as P

import Proarrow.Category.Instance.Free (Elems, FREE (..), Free (..), HasStructure (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), SymMonoidal, UnitF, type (**))
import Proarrow.Category.Monoidal.Closed (Closed)
import Proarrow.Category.Monoidal.StarAutonomous (DualF, StarAutonomous (..), dualityCounitSA)
import Proarrow.Core (CAT, CategoryOf (..), Kind, Promonad (..))
import Proarrow.Tools.Laws (Inverses (..), Law (..), Laws (..), inverses, (===))

class (StarAutonomous k) => IsoMix k where
  -- | The unit of par is isomorphic to the unit of the tensor.
  dualUnit :: Dual (Unit :: k) ~> Unit

  -- | The inverse of 'dualUnit'.
  dualUnitInv :: (Unit :: k) ~> Dual Unit

  -- | Join a dual and its object into the unit. 'dualityCounitDefault' gives it from the
  -- *-autonomous structure; a compact closed category has a counit of its own. (There is no
  -- default method: @a@ occurs only under type families, so GHC could not instantiate one.)
  dualityCounit :: (Ob (a :: k)) => Dual a ** a ~> Unit

-- | 'dualityCounit' from the *-autonomous structure: into the unit of par, then 'dualUnit'.
dualityCounitDefault :: forall {k} (a :: k). (IsoMix k, Ob a) => Dual a ** a ~> Unit
dualityCounitDefault :: forall {k} (a :: k). (IsoMix k, Ob a) => (Dual a ** a) ~> Unit
dualityCounitDefault = Dual Unit ~> Unit
forall k. IsoMix k => Dual Unit ~> Unit
dualUnit (Dual Unit ~> Unit)
-> ((Dual a ** a) ~> Dual Unit) -> (Dual a ** a) ~> Unit
forall (b :: k) (c :: k) (a :: k). (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
. forall (a :: k).
(StarAutonomous k, Ob a) =>
(Dual a ** a) ~> Dual Unit
forall {k} (a :: k).
(StarAutonomous k, Ob a) =>
(Dual a ** a) ~> Dual Unit
dualityCounitSA @a

instance IsoMix () where
  dualUnit :: Dual Unit ~> Unit
dualUnit = Dual Unit ~> Unit
Unit '() '()
U.Unit
  dualUnitInv :: Unit ~> Dual Unit
dualUnitInv = Unit ~> Dual Unit
Unit '() '()
U.Unit
  dualityCounit :: forall (a :: ()). Ob a => (Dual a ** a) ~> Unit
dualityCounit = (Dual a ** a) ~> Unit
Unit '() '()
U.Unit

instance (IsoMix j, IsoMix k) => IsoMix (j, k) where
  dualUnit :: Dual Unit ~> Unit
dualUnit = Dual Unit ~> Unit
forall k. IsoMix k => Dual Unit ~> Unit
dualUnit (Dual Unit ~> Unit)
-> (Dual Unit ~> Unit)
-> (:**:) (~>) (~>) '(Dual Unit, Dual Unit) '(Unit, Unit)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Dual Unit ~> Unit
forall k. IsoMix k => Dual Unit ~> Unit
dualUnit
  dualUnitInv :: Unit ~> Dual Unit
dualUnitInv = Unit ~> Dual Unit
forall k. IsoMix k => Unit ~> Dual Unit
dualUnitInv (Unit ~> Dual Unit)
-> (Unit ~> Dual Unit)
-> (:**:) (~>) (~>) '(Unit, Unit) '(Dual Unit, Dual Unit)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Unit ~> Dual Unit
forall k. IsoMix k => Unit ~> Dual Unit
dualUnitInv
  dualityCounit :: forall (a :: (j, k)). Ob a => (Dual a ** a) ~> Unit
dualityCounit @'(a, a') = forall k (a :: k). (IsoMix k, Ob a) => (Dual a ** a) ~> Unit
dualityCounit @j @a ((Dual (Fst @ a) ** (Fst @ a)) ~> Unit)
-> ((Dual (Snd @ a) ** (Snd @ a)) ~> Unit)
-> (:**:)
     (~>)
     (~>)
     '(Dual (Fst @ a) ** (Fst @ a), Dual (Snd @ a) ** (Snd @ a))
     '(Unit, Unit)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k). (IsoMix k, Ob a) => (Dual a ** a) ~> Unit
dualityCounit @k @a'

-- | The structures the free category needs for 'IsoMix', and those its laws are stated for.
type IsoMixStructures :: [Kind -> Constraint]
type IsoMixStructures = '[Monoidal, SymMonoidal, Closed, StarAutonomous, IsoMix]

instance (IsoMixStructures `Elems` cs) => HasStructure cs (p :: CAT k) IsoMix where
  data Struct IsoMix a b where
    DualUnit :: Struct IsoMix (DualF UnitF) UnitF
    DualUnitInv :: Struct IsoMix UnitF (DualF UnitF)
  foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(IsoMix k', All cs k', Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct IsoMix a b -> Lower f a ~> Lower f b
foldStructure forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ Struct IsoMix a b
R:StructkcspIsoMixab k cs p a b
DualUnit = Lower f a ~> Lower f b
Dual Unit ~> Unit
forall k. IsoMix k => Dual Unit ~> Unit
dualUnit
  foldStructure forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ Struct IsoMix a b
R:StructkcspIsoMixab k cs p a b
DualUnitInv = Lower f a ~> Lower f b
Unit ~> Dual Unit
forall k. IsoMix k => Unit ~> Dual Unit
dualUnitInv
instance P.Show (Struct IsoMix a b) where
  showsPrec :: Int -> Struct IsoMix a b -> ShowS
showsPrec Int
_ Struct IsoMix a b
R:StructkcspIsoMixab k cs p a b
DualUnit = String -> ShowS
P.showString String
"dualUnit"
  showsPrec Int
_ Struct IsoMix a b
R:StructkcspIsoMixab k cs p a b
DualUnitInv = String -> ShowS
P.showString String
"dualUnitInv"

instance (IsoMixStructures `Elems` cs) => IsoMix (FREE cs (p :: CAT k)) where
  dualUnit :: Dual Unit ~> Unit
dualUnit = Struct IsoMix (DualF UnitF) UnitF
-> Free (DualF UnitF) (DualF UnitF) -> Free (DualF UnitF) UnitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
St Struct IsoMix (DualF UnitF) UnitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}.
Struct IsoMix (DualF UnitF) UnitF
DualUnit Free (DualF UnitF) (DualF UnitF)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  dualUnitInv :: Unit ~> Dual Unit
dualUnitInv = Struct IsoMix UnitF (DualF UnitF)
-> Free UnitF UnitF -> Free UnitF (DualF UnitF)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
St Struct IsoMix UnitF (DualF UnitF)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}.
Struct IsoMix UnitF (DualF UnitF)
DualUnitInv Free UnitF UnitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  dualityCounit :: forall (a :: FREE cs p). Ob a => (Dual a ** a) ~> Unit
dualityCounit @a = forall {k} (a :: k). (IsoMix k, Ob a) => (Dual a ** a) ~> Unit
forall (a :: FREE cs p).
(IsoMix (FREE cs p), Ob a) =>
(Dual a ** a) ~> Unit
dualityCounitDefault @a

-- | 'dualUnit' and 'dualUnitInv' are inverses, and 'dualityCounit' is the one from the
-- *-autonomous structure.
instance Laws IsoMixStructures where
  laws :: [Law IsoMixStructures]
laws =
    String
-> PureLawBody IsoMixStructures Inverses -> [Law IsoMixStructures]
forall (cs :: [Type -> Constraint]).
String -> PureLawBody cs Inverses -> [Law cs]
inverses String
"dualUnit" ((Dual Unit ~> Unit) -> (Unit ~> Dual Unit) -> Inverses k
forall {k} (a :: k) (b :: k). (a ~> b) -> (b ~> a) -> Inverses k
Inverses Dual Unit ~> Unit
forall k. IsoMix k => Dual Unit ~> Unit
dualUnit Unit ~> Dual Unit
forall k. IsoMix k => Unit ~> Dual Unit
dualUnitInv)
      [Law IsoMixStructures]
-> [Law IsoMixStructures] -> [Law IsoMixStructures]
forall a. [a] -> [a] -> [a]
P.++ [String -> LawBody IsoMixStructures -> Law IsoMixStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"dualityCounit definition" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @_ @a (forall k (a :: k). (IsoMix k, Ob a) => (Dual a ** a) ~> Unit
dualityCounit @_ @a ((Dual a ** a) ~> Unit)
-> ((Dual a ** a) ~> Unit) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall (a :: k). (IsoMix k, Ob a) => (Dual a ** a) ~> Unit
forall {k} (a :: k). (IsoMix k, Ob a) => (Dual a ** a) ~> Unit
dualityCounitDefault @a)]