{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE TypeFamilies #-}

-- | Multiplicative disjunction (@⅋@) and its linear distributors.
--
-- This module surfaces the tensor product, its unit @⊥@, and the one-way
-- distributors between tensor and tensor.  These are "mixed metaphor"
-- structure: they relate a tensor @t@ (typically @(,)@) with a tensor
-- product @p@ (typically 'Either').
module Circuit.Par
  ( -- * Multiplicative disjunction
    Bot,
    Par (..),

    -- * Linear distributors and mix
    distL,
    distR,
    mix,
  )
where

import Circuit.Category (Category (..), K (..))
import Data.Bifunctor (Bifunctor (..))
import Data.Kind (Type)
import Data.Void (Void, absurd)
import Prelude hiding (id, (.))

-- | Unit of the tensor tensor (@⊥@).
type family Bot (p :: k -> k -> k) :: k

-- | Multiplicative disjunction action on a category.
--
-- 'parP' is the tensor product of morphisms.  The unitors witness that
-- @⊥ ⅋ a ≅ a@ and @a ⅋ ⊥ ≅ a@.
class (Category arr) => Par p arr where
  -- | Parallel composition under tensor.
  parP :: arr a b -> arr c d -> arr (p a c) (p b d)

  -- | Left unitor: @⊥ ⅋ a -> a@.
  unitlP :: arr (p (Bot p) a) a

  -- | Inverse left unitor: @a -> ⊥ ⅋ a@.
  unitlP' :: arr a (p (Bot p) a)

  -- | Right unitor: @a ⅋ ⊥ -> a@.
  unitrP :: arr (p a (Bot p)) a

  -- | Inverse right unitor: @a -> a ⅋ ⊥@.
  unitrP' :: arr a (p a (Bot p))

-- | The coproduct is the canonical tensor product on functions.
type instance Bot Either = Void

-- | Coproduct as multiplicative disjunction on functions.
--
-- The unit is the initial object @Void@; the unitors are the coproduct
-- injections absorbed by the universal property.
instance Par Either (->) where
  parP :: forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
parP = (a -> b) -> (c -> d) -> Either a c -> Either b d
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap
  {-# INLINE parP #-}
  unitlP :: forall a. Either (Bot Either) a -> a
unitlP = (Void -> a) -> (a -> a) -> Either Void a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Void -> a
forall a. Void -> a
absurd a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  {-# INLINE unitlP #-}
  unitlP' :: forall a. a -> Either (Bot Either) a
unitlP' = a -> Either Void a
a -> Either (Bot Either) a
forall a b. b -> Either a b
Right
  {-# INLINE unitlP' #-}
  unitrP :: forall a. Either a (Bot Either) -> a
unitrP = (a -> a) -> (Void -> a) -> Either a Void -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id Void -> a
forall a. Void -> a
absurd
  {-# INLINE unitrP #-}
  unitrP' :: forall a. a -> Either a (Bot Either)
unitrP' = a -> Either a Void
a -> Either a (Bot Either)
forall a b. a -> Either a b
Left
  {-# INLINE unitrP' #-}

-- | Coproduct as multiplicative disjunction on @K@ arrows.
instance (Monad m) => Par Either (K m) where
  parP :: forall a b c d. K m a b -> K m c d -> K m (Either a c) (Either b d)
parP (K a -> m b
f) (K c -> m d
g) =
    (Either a c -> m (Either b d)) -> K m (Either a c) (Either b d)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either a c -> m (Either b d)) -> K m (Either a c) (Either b d))
-> (Either a c -> m (Either b d)) -> K m (Either a c) (Either b d)
forall a b. (a -> b) -> a -> b
$ \case
      Left a
a -> b -> Either b d
forall a b. a -> Either a b
Left (b -> Either b d) -> m b -> m (Either b d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a
      Right c
c -> d -> Either b d
forall a b. b -> Either a b
Right (d -> Either b d) -> m d -> m (Either b d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> m d
g c
c
  {-# INLINE parP #-}
  unitlP :: forall a. K m (Either (Bot Either) a) a
unitlP = (Either (Bot Either) a -> m a) -> K m (Either (Bot Either) a) a
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either (Bot Either) a -> m a) -> K m (Either (Bot Either) a) a)
-> (Either (Bot Either) a -> m a) -> K m (Either (Bot Either) a) a
forall a b. (a -> b) -> a -> b
$ (Bot Either -> m a) -> (a -> m a) -> Either (Bot Either) a -> m a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Void -> m a
Bot Either -> m a
forall a. Void -> a
absurd a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  {-# INLINE unitlP #-}
  unitlP' :: forall a. K m a (Either (Bot Either) a)
unitlP' = (a -> m (Either (Bot Either) a)) -> K m a (Either (Bot Either) a)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((a -> m (Either (Bot Either) a)) -> K m a (Either (Bot Either) a))
-> (a -> m (Either (Bot Either) a))
-> K m a (Either (Bot Either) a)
forall a b. (a -> b) -> a -> b
$ Either Void a -> m (Either Void a)
Either Void a -> m (Either (Bot Either) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Void a -> m (Either (Bot Either) a))
-> (a -> Either Void a) -> a -> m (Either (Bot Either) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. a -> Either Void a
forall a b. b -> Either a b
Right
  {-# INLINE unitlP' #-}
  unitrP :: forall a. K m (Either a (Bot Either)) a
unitrP = (Either a (Bot Either) -> m a) -> K m (Either a (Bot Either)) a
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either a (Bot Either) -> m a) -> K m (Either a (Bot Either)) a)
-> (Either a (Bot Either) -> m a) -> K m (Either a (Bot Either)) a
forall a b. (a -> b) -> a -> b
$ (a -> m a) -> (Bot Either -> m a) -> Either a (Bot Either) -> m a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Void -> m a
Bot Either -> m a
forall a. Void -> a
absurd
  {-# INLINE unitrP #-}
  unitrP' :: forall a. K m a (Either a (Bot Either))
unitrP' = (a -> m (Either a (Bot Either))) -> K m a (Either a (Bot Either))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((a -> m (Either a (Bot Either))) -> K m a (Either a (Bot Either)))
-> (a -> m (Either a (Bot Either)))
-> K m a (Either a (Bot Either))
forall a b. (a -> b) -> a -> b
$ Either a Void -> m (Either a Void)
Either a Void -> m (Either a (Bot Either))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either a Void -> m (Either a (Bot Either)))
-> (a -> Either a Void) -> a -> m (Either a (Bot Either))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. a -> Either a Void
forall a b. a -> Either a b
Left
  {-# INLINE unitrP' #-}

-- * Linear distributors and mix

-- | Left linear distributor: @A ⊗ (B ⅋ C) -> (A ⊗ B) ⅋ C@.
--
-- For @(,)@ and @Either@ this is the one-way product-over-coproduct map.
-- Note that @(_, Right c) = Right c@ discards the @a@; this is legal
-- affinely but not in strict MLL. The distributors already live in the
-- affine fragment.
distL :: (a, Either b c) -> Either (a, b) c
distL :: forall a b c. (a, Either b c) -> Either (a, b) c
distL (a
a, Left b
b) = (a, b) -> Either (a, b) c
forall a b. a -> Either a b
Left (a
a, b
b)
distL (a
_, Right c
c) = c -> Either (a, b) c
forall a b. b -> Either a b
Right c
c
{-# INLINE distL #-}

-- | Right linear distributor: @(B ⅋ C) ⊗ A -> B ⅋ (C ⊗ A)@.
--
-- Mirror of 'distL': the same affine discard is present when the left
-- summand is taken.
distR :: (Either b c, a) -> Either b (c, a)
distR :: forall b c a. (Either b c, a) -> Either b (c, a)
distR (Left b
b, a
_) = b -> Either b (c, a)
forall a b. a -> Either a b
Left b
b
distR (Right c
c, a
a) = (c, a) -> Either b (c, a)
forall a b. b -> Either a b
Right (c
c, a
a)
{-# INLINE distR #-}

-- | Mix: the canonical map @⊥ -> 1@ from tensor unit to tensor unit.
--
-- Every @⊥@-value is vacuous, so it maps to the unique tensor unit.
mix :: Void -> ()
mix :: Void -> ()
mix = Void -> ()
forall a. Void -> a
absurd
{-# INLINE mix #-}