{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Markov-category tests for affine structural morphisms.
--
-- A Markov category is a semicartesian symmetric monoidal category in which
-- every object carries a distinguished commutative comonoid (copy, discard)
-- and the monoidal unit is terminal.  In our setting the structural morphisms
-- are explicit capabilities ('Copy' / 'Discard'), so this module provides
-- /law tests/ rather than a bundled class.
--
-- The key observation from the excavation (Ex9) is that copyability and
-- discardability are morphism-level properties, not object-level modalities:
--
-- * A map @f :: a -> b@ is /discard-natural/ when
--   @discard . f = discard@.  In 'Prob' this is exactly the mass-1 fragment;
--   in 'FinRel' it is the total relations.
-- * A map @f :: a -> b@ is /copy-natural/ when
--   @copy . f = tensor f f . copy@.  These are the deterministic maps: partial
--   functions in 'FinRel', embedded functions in 'Prob'.
--
-- The copy-natural maps form a cartesian subcategory; the discard-natural
-- maps form a semicartesian one.
module Circuit.Markov
  ( -- * Naturality tests
    copyNatural,
    discardNatural,

    -- * Deterministic centre
    deterministic,
  )
where

import Circuit.Bimonoid (Copy (..), Discard (..))
import Circuit.Category (Category (..))
import Circuit.Tensor (Tensor (..))
import Prelude hiding (id, (.))

-- | Test whether @f@ is a homomorphism from the copy comonoid on @a@ to the
-- copy comonoid on @b@.
--
-- > copy . f == tensor f f . copy
--
-- The equality predicate is supplied by the caller because many bases
-- (notably 'Prob') do not admit decidable equality of morphisms.  A finite
-- /separator/ — a set of continuations and inputs — is the usual way to
-- produce this predicate for such bases.
copyNatural ::
  (Tensor (,) arr, Copy arr a, Copy arr b) =>
  (arr a (b, b) -> arr a (b, b) -> Bool) ->
  arr a b ->
  Bool
copyNatural :: forall (arr :: * -> * -> *) a b.
(Tensor (,) arr, Copy arr a, Copy arr b) =>
(arr a (b, b) -> arr a (b, b) -> Bool) -> arr a b -> Bool
copyNatural arr a (b, b) -> arr a (b, b) -> Bool
eq arr a b
f = arr a (b, b) -> arr a (b, b) -> Bool
eq (arr b (b, b)
forall (arr :: * -> * -> *) a. Copy arr a => arr a (a, a)
copy arr b (b, b) -> arr a b -> arr a (b, b)
forall b c a. 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 a b -> arr a b -> arr (a, a) (b, b)
forall a b c d. arr a b -> arr c d -> arr (a, c) (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 a b
f arr (a, a) (b, b) -> arr a (a, a) -> arr a (b, b)
forall b c a. 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 (a, a)
forall (arr :: * -> * -> *) a. Copy arr a => arr a (a, a)
copy)
{-# INLINE copyNatural #-}

-- | Test whether @f@ is a homomorphism from the discard comonoid on @a@ to
-- the discard comonoid on @b@.
--
-- > discard . f == discard
--
-- The equality predicate is supplied by the caller for the same reason as
-- 'copyNatural'.
discardNatural ::
  (Category arr, Discard arr a, Discard arr b) =>
  (arr a () -> arr a () -> Bool) ->
  arr a b ->
  Bool
discardNatural :: forall (arr :: * -> * -> *) a b.
(Category arr, Discard arr a, Discard arr b) =>
(arr a () -> arr a () -> Bool) -> arr a b -> Bool
discardNatural arr a () -> arr a () -> Bool
eq arr a b
f = arr a () -> arr a () -> Bool
eq (arr b ()
forall {k} (arr :: k -> * -> *) (a :: k). Discard arr a => arr a ()
discard arr b () -> arr a b -> arr a ()
forall b c a. 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 a ()
forall {k} (arr :: k -> * -> *) (a :: k). Discard arr a => arr a ()
discard
{-# INLINE discardNatural #-}

-- | A map is deterministic precisely when it is both copy-natural and
-- discard-natural: it preserves the full cartesian comonoid.
deterministic ::
  ( Tensor (,) arr,
    Copy arr a,
    Copy arr b,
    Discard arr a,
    Discard arr b
  ) =>
  (arr a (b, b) -> arr a (b, b) -> Bool) ->
  (arr a () -> arr a () -> Bool) ->
  arr a b ->
  Bool
deterministic :: forall (arr :: * -> * -> *) a b.
(Tensor (,) arr, Copy arr a, Copy arr b, Discard arr a,
 Discard arr b) =>
(arr a (b, b) -> arr a (b, b) -> Bool)
-> (arr a () -> arr a () -> Bool) -> arr a b -> Bool
deterministic arr a (b, b) -> arr a (b, b) -> Bool
eqCopy arr a () -> arr a () -> Bool
eqDiscard arr a b
f = (arr a (b, b) -> arr a (b, b) -> Bool) -> arr a b -> Bool
forall (arr :: * -> * -> *) a b.
(Tensor (,) arr, Copy arr a, Copy arr b) =>
(arr a (b, b) -> arr a (b, b) -> Bool) -> arr a b -> Bool
copyNatural arr a (b, b) -> arr a (b, b) -> Bool
eqCopy arr a b
f Bool -> Bool -> Bool
&& (arr a () -> arr a () -> Bool) -> arr a b -> Bool
forall (arr :: * -> * -> *) a b.
(Category arr, Discard arr a, Discard arr b) =>
(arr a () -> arr a () -> Bool) -> arr a b -> Bool
discardNatural arr a () -> arr a () -> Bool
eqDiscard arr a b
f
{-# INLINE deterministic #-}