{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- | The free dagger category over a base arrow.
--
-- A 'Dagger' value pairs a forward arrow with a backward arrow.
-- Composition is covariant forward and contravariant backward;
-- 'transpose' swaps the two directions.
--
-- The structural rules ('Copy' / 'Discard' / 'Merge' / 'Zero' and their
-- tensor-generic forms) live in "Circuit.Bimonoid".  This module only
-- provides the free dagger construction and the way it dualises a bimonoid:
-- forward copy corresponds to backward merge, forward discard to backward
-- zero, and vice versa.
module Circuit.Dagger
  ( -- * Free dagger category
    Dagger (..),
    transpose,
  )
where

import Circuit.Bimonoid
  ( Copy (..),
    CopyT (..),
    Discard (..),
    DiscardT (..),
    Merge (..),
    MergeT (..),
    Zero (..),
    ZeroT (..),
  )
import Circuit.Category (Category (..))
import Circuit.Channel (Channel (..), Strength (..), Traced (..))
import Circuit.Tensor (Action (..), Tensor (..), Unital (..))
import Prelude hiding (id, (.))

-- $setup
-- >>> import Circuit.Dagger
-- >>> import Circuit.Bimonoid
-- >>> import Circuit.Tensor (Action (..), Tensor (..), Unital (..))
-- >>> import Circuit.Channel (Traced (..))
-- >>> import Circuit.Category (Category (..), (.>))
-- >>> import Prelude hiding (id, (.))

-- | The free dagger category over a base arrow.
--
-- @Dagger arr a b@ is a pair of arrows @arr a b@ (forward) and
-- @arr b a@ (backward).  Composition is covariant forward, contravariant
-- backward: @Dagger f g . Dagger f' g' = Dagger (f . f') (g' . g)@.
--
-- >>> let d = Dagger (+1) (subtract 1) :: Dagger (->) Int Int
-- >>> front d 5
-- 6
-- >>> back d 6
-- 5
data Dagger arr a b = Dagger
  { -- | The forward direction.
    forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Dagger arr a b -> arr a b
front :: arr a b,
    -- | The backward direction.
    forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Dagger arr a b -> arr b a
back :: arr b a
  }

-- | The dagger operation: braid forward and backward.
--
-- Involutive: @transpose . transpose = id@.
transpose :: Dagger arr a b -> Dagger arr b a
transpose :: forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Dagger arr a b -> Dagger arr b a
transpose (Dagger arr a b
f arr b a
g) = arr b a -> arr a b -> Dagger arr b a
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr b a
g arr a b
f

instance (Category arr) => Category (Dagger arr) where
  id :: forall (a :: k). Dagger arr a a
id = arr a a -> arr a a -> Dagger arr a a
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr a a
forall (a :: k). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id arr a a
forall (a :: k). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  {-# INLINE id #-}

  Dagger arr b c
f arr c b
g . :: forall (b :: k) (c :: k) (a :: k).
Dagger arr b c -> Dagger arr a b -> Dagger arr a c
. Dagger arr a b
f' arr b a
g' = arr a c -> arr c a -> Dagger arr a c
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger (arr b c
f arr b c -> arr a b -> arr a c
forall (b :: k) (c :: k) (a :: k). arr b c -> arr a b -> arr a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. arr a b
f') (arr b a
g' arr b a -> arr c b -> arr c a
forall (b :: k) (c :: k) (a :: k). arr b c -> arr a b -> arr a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. arr c b
g)
  {-# INLINE (.) #-}

instance (Strength t arr) => Strength t (Dagger arr) where
  strength :: forall (b :: k) (c :: k) (a :: k).
Dagger arr b c -> Dagger arr (t a b) (t a c)
strength (Dagger arr b c
f arr c b
g) = arr (t a b) (t a c)
-> arr (t a c) (t a b) -> Dagger arr (t a b) (t a c)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger (arr b c -> arr (t a b) (t a c)
forall (b :: k) (c :: k) (a :: k). arr b c -> arr (t a b) (t a c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (b :: k)
       (c :: k) (a :: k).
Strength t arr =>
arr b c -> arr (t a b) (t a c)
strength arr b c
f) (arr c b -> arr (t a c) (t a b)
forall (b :: k) (c :: k) (a :: k). arr b c -> arr (t a b) (t a c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (b :: k)
       (c :: k) (a :: k).
Strength t arr =>
arr b c -> arr (t a b) (t a c)
strength arr c b
g)
  {-# INLINE strength #-}

instance (Traced t arr) => Traced t (Dagger arr) where
  trace :: forall (a :: k) (b :: k) (c :: k).
Dagger arr (t a b) (t a c) -> Dagger arr b c
trace (Dagger arr (t a b) (t a c)
f arr (t a c) (t a b)
g) = arr b c -> arr c b -> Dagger arr b c
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger (arr (t a b) (t a c) -> arr b c
forall (a :: k) (b :: k) (c :: k). arr (t a b) (t a c) -> arr b c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Traced t arr =>
arr (t a b) (t a c) -> arr b c
trace arr (t a b) (t a c)
f) (arr (t a c) (t a b) -> arr c b
forall (a :: k) (b :: k) (c :: k). arr (t a b) (t a c) -> arr b c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Traced t arr =>
arr (t a b) (t a c) -> arr b c
trace arr (t a c) (t a b)
g)
  {-# INLINE trace #-}

-- | Forward copy, backward add — the bimonoid self-duality.
--
-- The interlock is the point to notice: 'Copy' on the dagger requires
-- 'Merge' on the base.  The comonoid and monoid cannot be granted
-- separately in this construction; @Dagger (FinRel k)@ is where that
-- collapse becomes observable (see the @circuits-axioma@ oracle).
instance (Copy arr a, Merge arr a) => Copy (Dagger arr) a where
  copy :: Dagger arr a (a, a)
copy = arr a (a, a) -> arr (a, a) a -> Dagger arr a (a, a)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr a (a, a)
forall (arr :: * -> * -> *) a. Copy arr a => arr a (a, a)
copy arr (a, a) a
forall (arr :: * -> * -> *) a. Merge arr a => arr (a, a) a
plus
  {-# INLINE copy #-}

instance (Discard arr a, Zero arr a) => Discard (Dagger arr) a where
  discard :: Dagger arr a ()
discard = arr a () -> arr () a -> Dagger arr a ()
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr a ()
forall {k} (arr :: k -> * -> *) (a :: k). Discard arr a => arr a ()
discard arr () a
forall {k} (arr :: * -> k -> *) (a :: k). Zero arr a => arr () a
zero
  {-# INLINE discard #-}

-- | Forward add, backward copy.
instance (Merge arr a, Copy arr a) => Merge (Dagger arr) a where
  plus :: Dagger arr (a, a) a
plus = arr (a, a) a -> arr a (a, a) -> Dagger arr (a, a) a
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr (a, a) a
forall (arr :: * -> * -> *) a. Merge arr a => arr (a, a) a
plus arr a (a, a)
forall (arr :: * -> * -> *) a. Copy arr a => arr a (a, a)
copy
  {-# INLINE plus #-}

instance (Zero arr a, Discard arr a) => Zero (Dagger arr) a where
  zero :: Dagger arr () a
zero = arr () a -> arr a () -> Dagger arr () a
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr () a
forall {k} (arr :: * -> k -> *) (a :: k). Zero arr a => arr () a
zero arr a ()
forall {k} (arr :: k -> * -> *) (a :: k). Discard arr a => arr a ()
discard
  {-# INLINE zero #-}

-- | Tensor-generic bimonoid interlock through @Dagger@.
--
-- These instances mirror the cartesian ones above, but work for any wiring
-- tensor @t@.  They are the missing lemma that makes 'Circuit.Net.mirror'
-- total: a 'Circuit.Net.Net' over 'Dagger arr' can transpose its bimonoid rows because
-- the dagger swaps the tensor-comonoid and tensor-monoid dictionaries.
--
-- >>> let d = copyT @(,) @(Dagger (->)) @Int :: Dagger (->) Int (Int, Int)
-- >>> front d 5
-- (5,5)
-- >>> back d (2, 3)
-- 5
instance {-# INCOHERENT #-} (CopyT t arr a, MergeT t arr a) => CopyT t (Dagger arr) a where
  copyT :: Dagger arr a (t a a)
copyT = arr a (t a a) -> arr (t a a) a -> Dagger arr a (t a a)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger (forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
CopyT t arr a =>
arr a (t a a)
forall (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
CopyT t arr a =>
arr a (t a a)
copyT @t) (forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
MergeT t arr a =>
arr (t a a) a
forall (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
MergeT t arr a =>
arr (t a a) a
plusT @t)
  {-# INLINE copyT #-}

instance {-# INCOHERENT #-} (DiscardT t arr a, ZeroT t arr a) => DiscardT t (Dagger arr) a where
  discardT :: Dagger arr a (Unit t)
discardT = arr a (Unit t) -> arr (Unit t) a -> Dagger arr a (Unit t)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger (forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
DiscardT t arr a =>
arr a (Unit t)
forall (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
DiscardT t arr a =>
arr a (Unit t)
discardT @t) (forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
ZeroT t arr a =>
arr (Unit t) a
forall (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
ZeroT t arr a =>
arr (Unit t) a
zeroT @t)
  {-# INLINE discardT #-}

instance {-# INCOHERENT #-} (MergeT t arr a, CopyT t arr a) => MergeT t (Dagger arr) a where
  plusT :: Dagger arr (t a a) a
plusT = arr (t a a) a -> arr a (t a a) -> Dagger arr (t a a) a
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger (forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
MergeT t arr a =>
arr (t a a) a
forall (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
MergeT t arr a =>
arr (t a a) a
plusT @t) (forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
CopyT t arr a =>
arr a (t a a)
forall (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
CopyT t arr a =>
arr a (t a a)
copyT @t)
  {-# INLINE plusT #-}

instance {-# INCOHERENT #-} (ZeroT t arr a, DiscardT t arr a) => ZeroT t (Dagger arr) a where
  zeroT :: Dagger arr (Unit t) a
zeroT = arr (Unit t) a -> arr a (Unit t) -> Dagger arr (Unit t) a
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger (forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
ZeroT t arr a =>
arr (Unit t) a
forall (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
ZeroT t arr a =>
arr (Unit t) a
zeroT @t) (forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
DiscardT t arr a =>
arr a (Unit t)
forall (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
DiscardT t arr a =>
arr a (Unit t)
discardT @t)
  {-# INLINE zeroT #-}

instance (Unital t arr) => Unital t (Dagger arr) where
  unitl :: forall (a :: k). Dagger arr (t (Unit t) a) a
unitl = arr (t (Unit t) a) a
-> arr a (t (Unit t) a) -> Dagger arr (t (Unit t) a) a
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr (t (Unit t) a) a
forall (a :: k). arr (t (Unit t) a) a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr (t (Unit t) a) a
unitl arr a (t (Unit t) a)
forall (a :: k). arr a (t (Unit t) a)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr a (t (Unit t) a)
unitl'
  {-# INLINE unitl #-}
  unitl' :: forall (a :: k). Dagger arr a (t (Unit t) a)
unitl' = arr a (t (Unit t) a)
-> arr (t (Unit t) a) a -> Dagger arr a (t (Unit t) a)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr a (t (Unit t) a)
forall (a :: k). arr a (t (Unit t) a)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr a (t (Unit t) a)
unitl' arr (t (Unit t) a) a
forall (a :: k). arr (t (Unit t) a) a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr (t (Unit t) a) a
unitl
  {-# INLINE unitl' #-}
  unitr :: forall (a :: k). Dagger arr (t a (Unit t)) a
unitr = arr (t a (Unit t)) a
-> arr a (t a (Unit t)) -> Dagger arr (t a (Unit t)) a
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr (t a (Unit t)) a
forall (a :: k). arr (t a (Unit t)) a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr (t a (Unit t)) a
unitr arr a (t a (Unit t))
forall (a :: k). arr a (t a (Unit t))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr a (t a (Unit t))
unitr'
  {-# INLINE unitr #-}
  unitr' :: forall (a :: k). Dagger arr a (t a (Unit t))
unitr' = arr a (t a (Unit t))
-> arr (t a (Unit t)) a -> Dagger arr a (t a (Unit t))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr a (t a (Unit t))
forall (a :: k). arr a (t a (Unit t))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr a (t a (Unit t))
unitr' arr (t a (Unit t)) a
forall (a :: k). arr (t a (Unit t)) a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr (t a (Unit t)) a
unitr
  {-# INLINE unitr' #-}

instance (Tensor t arr) => Tensor t (Dagger arr) where
  tensor :: forall (a :: k) (b :: k) (c :: k) (d :: k).
Dagger arr a b -> Dagger arr c d -> Dagger arr (t a c) (t b d)
tensor (Dagger arr a b
f arr b a
g) (Dagger arr c d
f' arr d c
g') = arr (t a c) (t b d)
-> arr (t b d) (t a c) -> Dagger arr (t a c) (t b d)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger (arr a b -> arr c d -> arr (t a c) (t b d)
forall (a :: k) (b :: k) (c :: k) (d :: k).
arr a b -> arr c d -> arr (t a c) (t b d)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k) (d :: k).
Tensor t arr =>
arr a b -> arr c d -> arr (t a c) (t b d)
tensor arr a b
f arr c d
f') (arr b a -> arr d c -> arr (t b d) (t a c)
forall (a :: k) (b :: k) (c :: k) (d :: k).
arr a b -> arr c d -> arr (t a c) (t b d)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k) (d :: k).
Tensor t arr =>
arr a b -> arr c d -> arr (t a c) (t b d)
tensor arr b a
g arr d c
g')
  {-# INLINE tensor #-}

instance (Action t arr) => Action t (Dagger arr) where
  braid :: forall (a :: k) (b :: k). Dagger arr (t a b) (t b a)
braid = arr (t a b) (t b a)
-> arr (t b a) (t a b) -> Dagger arr (t a b) (t b a)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr (t a b) (t b a)
forall (a :: k) (b :: k). arr (t a b) (t b a)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k).
Action t arr =>
arr (t a b) (t b a)
braid arr (t b a) (t a b)
forall (a :: k) (b :: k). arr (t a b) (t b a)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k).
Action t arr =>
arr (t a b) (t b a)
braid
  {-# INLINE braid #-}

instance (Channel t arr) => Channel t (Dagger arr) where
  assoc :: forall (a :: k) (b :: k) (c :: k).
Dagger arr (t (t a b) c) (t a (t b c))
assoc = arr (t (t a b) c) (t a (t b c))
-> arr (t a (t b c)) (t (t a b) c)
-> Dagger arr (t (t a b) c) (t a (t b c))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr (t (t a b) c) (t a (t b c))
forall (a :: k) (b :: k) (c :: k). arr (t (t a b) c) (t a (t b c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t (t a b) c) (t a (t b c))
assoc arr (t a (t b c)) (t (t a b) c)
forall (a :: k) (b :: k) (c :: k). arr (t a (t b c)) (t (t a b) c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t (t a b) c)
assoc'
  assoc' :: forall (a :: k) (b :: k) (c :: k).
Dagger arr (t a (t b c)) (t (t a b) c)
assoc' = arr (t a (t b c)) (t (t a b) c)
-> arr (t (t a b) c) (t a (t b c))
-> Dagger arr (t a (t b c)) (t (t a b) c)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr (t a (t b c)) (t (t a b) c)
forall (a :: k) (b :: k) (c :: k). arr (t a (t b c)) (t (t a b) c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t (t a b) c)
assoc' arr (t (t a b) c) (t a (t b c))
forall (a :: k) (b :: k) (c :: k). arr (t (t a b) c) (t a (t b c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t (t a b) c) (t a (t b c))
assoc
  slide :: forall (a :: k) (b :: k) (c :: k).
Dagger arr (t a (t b c)) (t b (t a c))
slide = arr (t a (t b c)) (t b (t a c))
-> arr (t b (t a c)) (t a (t b c))
-> Dagger arr (t a (t b c)) (t b (t a c))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> arr b a -> Dagger arr a b
Dagger arr (t a (t b c)) (t b (t a c))
forall (a :: k) (b :: k) (c :: k). arr (t a (t b c)) (t b (t a c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t b (t a c))
slide arr (t b (t a c)) (t a (t b c))
forall (a :: k) (b :: k) (c :: k). arr (t a (t b c)) (t b (t a c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t b (t a c))
slide