{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Free channel poles over a base arrow, plus concrete box helpers.
--
-- A channel has exactly two poles:
--
--   * @Out@ — the companion (read / emit pole), covariant in the payload.
--   * @In@  — the conjoint (write / commit pole), contravariant in the payload.
--
-- @Poles@ is the record that pairs one @In@ with one @Out@.  The poles are
-- defined purely in terms of the base arrow @arr@.
--
-- 'open' produces a matched pair; 'close' plugs the pair back together by
-- feeding the @Out@ into the @In@.
--
-- A /symmetric/ pole @Poles arr a a@ with @close (conjoint p) (companion p) = id@
-- is the copycat strategy for the multiplicative excluded middle @A ⅋ A⊥@:
-- it routes traffic between the two poles without ever deciding which side is
-- true.  For the unit object use 'open' (also exported as 'copycat').
--
-- == Relationship to 'Circuit.Poly.Channel'
--
-- @Poles@ is the bi-polar / effectful API: it is the right tool for
-- @K IO/STM@ process plumbing where the channel is a write pole paired
-- with a read pole.  For pure @(->)@ Moore-style channels indexed by a
-- polynomial, prefer 'Circuit.Poly.Channel'.
--
-- There is no deprecation shim yet: the relationship between the bi-polar
-- and polynomial views is still being settled.  This module stays unchanged
-- until the polynomial 'Channel' gains an equivalent effectful story.
module Circuit.Poles
  ( -- * Channel poles (bi-polar contract)
    Out (..),
    In (..),

    -- * Matched pair
    Poles (..),

    -- * Counit
    close,

    -- * Prefixing an action to an @In@
    prefixIn,

    -- * Suffixing an action to an @Out@
    suffixOut,

    -- * Build a @Poles@ from primitive actions
    poles,
    poles0,
    polesK,

    -- * Extract primitive actions from a @Poles@
    splay,
    splay0,

    -- * Sequential composition
    compose,
    compose0,
    (>:>),

    -- * Parallel composition
    polesTensor,

    -- * Morphism-level mapping
    iomap,
    imap,
    omap,

    -- * Dualising object / unit poles (requires constant morphisms)
    HasDual (..),

    -- * Copycat / multiplicative excluded middle
    copycat,

    -- * Boxes
    box,
    boxAsymmetric,

    -- * Additive connectives
    pair,
    Bias (..),
    race,
  )
where

import Circuit.Bimonoid (Copy (copy))
import Circuit.Category (Category (..), FunctionLike (..), K (..), (.>))
import Circuit.Channel (Channel (..), Strength (..), Traced (..))
import Circuit.Tensor (Bias (..), Tensor, Unit)
import Circuit.Tensor qualified as Tensor
import Data.Bifunctor (bimap)
import Data.Kind (Type)
import Prelude hiding (id, (.))

-- $setup
-- >>> :set -XTypeApplications
-- >>> import Circuit.Category ((.>))
-- >>> import Circuit.Poles
-- >>> import Circuit.Syntax (eval)
-- >>> import Circuit.Category (K(..), runK)
-- >>> import Data.Maybe (isNothing)

-- * Channel poles — the companion and conjoint of the identity functor.

-- | @Out@ is the companion of the identity functor.  Covariant in @a@
-- (sits in the output position).
newtype Out arr a = Out
  { -- | Emit through the companion, supplying the other pole.
    forall {k} {k} (arr :: k -> k -> *) (a :: k).
Out arr a -> forall (x :: k). In arr x -> arr x a
emit :: forall x. In arr x -> arr x a
  }

-- | @In@ is the conjoint of the identity functor.  Contravariant in
-- @a@ (sits in the input position).
newtype In arr a = In
  { -- | Commit through the conjoint, supplying the other pole.
    forall {k} {k} (arr :: k -> k -> *) (a :: k).
In arr a -> forall (x :: k). Out arr x -> arr a x
commit :: forall x. Out arr x -> arr a x
  }

-- | A matched pair of channel poles: one @In@ and one @Out@.
--
-- This is the bi-polar communication contract.  The conjoint (@In@)
-- consumes payloads of type @a@; the companion (@Out@) produces payloads
-- of type @b@.  For symmetric channels such as queues @a = b@.
--
-- Together with 'prefixIn' and 'suffixOut', @Poles@ carries an /enriched/
-- profunctor structure over the base category @arr@: 'prefixIn' is the
-- left action of @arr@ on @In@ poles, and 'suffixOut' is the right action
-- of @arr@ on @Out@ poles.
data Poles arr a b = Poles
  { -- | Write pole (producer), the conjoint.
    forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> In arr a
conjoint :: In arr a,
    -- | Read pole  (consumer), the companion.
    forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> Out arr b
companion :: Out arr b
  }

-- | Plug an @In@ and an @Out@ of the same payload type together.
--
-- 'close' feeds the @Out@ into the @In@ pole, producing a morphism
-- @arr a a@ from the paired payload type.
--
-- Yanking: for the unit poles from 'open',
-- @close (conjoint p) (companion p) = id@.
close :: In arr a -> Out arr a -> arr a a
close :: forall {k} (arr :: k -> k -> *) (a :: k).
In arr a -> Out arr a -> arr a a
close In arr a
contra = In arr a -> forall (x :: k). Out arr x -> arr a x
forall {k} {k} (arr :: k -> k -> *) (a :: k).
In arr a -> forall (x :: k). Out arr x -> arr a x
commit In arr a
contra

-- | Precompose an @arr@-morphism with an @In@ pole.
--
-- Given @f :: arr a b@ and an @In@ pole at type @b@, produce an @In@ pole
-- at type @a@.  Running the resulting pole first executes @f@ and then
-- commits through the original pole.
--
-- This is the left (contravariant) action of the base category on @In@
-- poles.  Specialised to unit poles it is the canonical way to build
-- effectful write poles.
--
-- >>> let polesU = open :: Poles (->) () ()
-- >>> let inA = prefixIn (const ()) (conjoint polesU) :: In (->) Int
-- >>> commit inA (companion polesU) 42
-- ()
prefixIn :: forall arr a b. (Category arr) => arr a b -> In arr b -> In arr a
prefixIn :: forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Category arr =>
arr a b -> In arr b -> In arr a
prefixIn arr a b
f In arr b
i = (forall (x :: k). Out arr x -> arr a x) -> In arr a
forall {k} {k} (arr :: k -> k -> *) (a :: k).
(forall (x :: k). Out arr x -> arr a x) -> In arr a
In ((forall (x :: k). Out arr x -> arr a x) -> In arr a)
-> (forall (x :: k). Out arr x -> arr a x) -> In arr a
forall a b. (a -> b) -> a -> b
$ \(Out arr x
o :: Out arr x) -> arr a b
f arr a b -> arr b x -> arr a x
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> In arr b -> forall (x :: k). Out arr x -> arr b x
forall {k} {k} (arr :: k -> k -> *) (a :: k).
In arr a -> forall (x :: k). Out arr x -> arr a x
commit In arr b
i Out arr x
o

-- | Postcompose an @arr@-morphism with an @Out@ pole.
--
-- Given an @Out@ pole at type @a@ and @g :: arr a b@, produce an @Out@
-- pole at type @b@.  Running the resulting pole first emits through the
-- original pole and then executes @g@ on the emitted value.
--
-- This is the right (covariant) action of the base category on @Out@
-- poles.  Specialised to unit poles it is the canonical way to build
-- effectful read poles.
--
-- >>> let polesU = open :: Poles (->) () ()
-- >>> let outA = suffixOut (companion polesU) (const 42) :: Out (->) Int
-- >>> emit outA (conjoint polesU) ()
-- 42
suffixOut :: forall arr a b. (Category arr) => Out arr a -> arr a b -> Out arr b
suffixOut :: forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Category arr =>
Out arr a -> arr a b -> Out arr b
suffixOut Out arr a
o arr a b
g = (forall (x :: k). In arr x -> arr x b) -> Out arr b
forall {k} {k} (arr :: k -> k -> *) (a :: k).
(forall (x :: k). In arr x -> arr x a) -> Out arr a
Out ((forall (x :: k). In arr x -> arr x b) -> Out arr b)
-> (forall (x :: k). In arr x -> arr x b) -> Out arr b
forall a b. (a -> b) -> a -> b
$ \(In arr x
i :: In arr x) -> Out arr a -> forall (x :: k). In arr x -> arr x a
forall {k} {k} (arr :: k -> k -> *) (a :: k).
Out arr a -> forall (x :: k). In arr x -> arr x a
emit Out arr a
o In arr x
i arr x a -> arr a b -> arr x b
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr a b
g

-- * Dualising object / unit poles

-- | Arrows that have channel poles for a given dualising object @bot@.
--
-- The dualising object is the target of the polar pairing and the object
-- through which the two poles of a 'Poles' are plugged together.  In the
-- cartesian case it is the monoidal unit @()@; for halt-mark / delivery
-- pairings it can be 'Bool'.
--
-- The poles are the identity-on-@bot@ morphism split into its two polar
-- halves.  The companion is constant; the conjoint delegates to the
-- opposing companion.
--
-- These poles require the base arrow to support constant morphisms, so
-- they are captured by this class rather than being definable for all
-- arrows.
class (Category arr) => HasDual bot arr where
  -- | The dualising object as channel poles.
  --
  -- === Yank
  --
  -- >>> let poles = open :: Poles (->) () ()
  -- >>> close (conjoint poles) (companion poles) ()
  -- ()
  --
  -- === Plug
  --
  -- >>> let polesA = open :: Poles (->) () ()
  -- >>> let polesU = open :: Poles (->) () ()
  -- >>> commit (conjoint polesA) (companion polesU) ()
  -- ()
  -- >>> emit (companion polesA) (conjoint polesU) ()
  -- ()
  open :: Poles arr bot bot

-- | The copycat strategy at the dualising object @bot@.
--
-- This is the multiplicative excluded middle @bot ⅋ bot⊥@ for arrows that
-- have poles at @bot@: a self-dual channel whose 'close' is the identity on
-- @bot@.  It routes between the two poles without ever deciding which one
-- holds.
--
-- The additive excluded middle @bot ⊕ bot⊥@ — a verdict, now — is /not/
-- supported; there is no @decide :: Either bot bot@ here, because only the
-- routing witness is provable.
copycat :: forall arr bot. (HasDual bot arr) => Poles arr bot bot
copycat :: forall {k} (arr :: k -> k -> *) (bot :: k).
HasDual bot arr =>
Poles arr bot bot
copycat = Poles arr bot bot
forall {k} (bot :: k) (arr :: k -> k -> *).
HasDual bot arr =>
Poles arr bot bot
open
{-# INLINE copycat #-}

-- | Build a @Poles@ from a write morphism and a read morphism.
--
-- @write :: arr a bot@ consumes the input payload and produces the dualising
-- object; @read :: arr bot b@ consumes the dualising object and produces the
-- output payload.  The dualising-object poles wire the two halves together.
--
-- This is the canonical way to turn a pair of primitive channel actions
-- into a matched pair of @In@ and @Out@ poles.
--
-- Compositional spelling:
--
-- @
-- poles write receive =
--   Poles (prefixIn write (conjoint open)) (suffixOut (companion open) receive)
-- @
poles ::
  forall arr a b bot.
  (HasDual bot arr) =>
  arr a bot ->
  arr bot b ->
  Poles arr a b
poles :: forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (bot :: k).
HasDual bot arr =>
arr a bot -> arr bot b -> Poles arr a b
poles arr a bot
write arr bot b
receive =
  In arr a -> Out arr b -> Poles arr a b
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
In arr a -> Out arr b -> Poles arr a b
Poles
    (arr a bot -> In arr bot -> In arr a
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Category arr =>
arr a b -> In arr b -> In arr a
prefixIn arr a bot
write (Poles arr bot bot -> In arr bot
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> In arr a
conjoint Poles arr bot bot
forall {k} (bot :: k) (arr :: k -> k -> *).
HasDual bot arr =>
Poles arr bot bot
open))
    (Out arr bot -> arr bot b -> Out arr b
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Category arr =>
Out arr a -> arr a b -> Out arr b
suffixOut (Poles arr bot bot -> Out arr bot
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> Out arr b
companion Poles arr bot bot
forall {k} (bot :: k) (arr :: k -> k -> *).
HasDual bot arr =>
Poles arr bot bot
open) arr bot b
receive)

-- | Convenience version of 'poles' when the dualising object is @()@.
poles0 ::
  (HasDual () arr) =>
  arr a () ->
  arr () b ->
  Poles arr a b
poles0 :: forall (arr :: * -> * -> *) a b.
HasDual () arr =>
arr a () -> arr () b -> Poles arr a b
poles0 = forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (bot :: k).
HasDual bot arr =>
arr a bot -> arr bot b -> Poles arr a b
forall (arr :: * -> * -> *) a b bot.
HasDual bot arr =>
arr a bot -> arr bot b -> Poles arr a b
poles @_ @_ @_ @()
{-# INLINE poles0 #-}

-- | Specialization of 'poles' for @K@ actions.
--
-- @write :: a -> m ()@ consumes the input payload; @receive :: m b@
-- produces the output payload. The dualising-object handling is hidden
-- inside the @K@ wrappers.
polesK ::
  forall m a b.
  (Monad m) =>
  (a -> m ()) ->
  m b ->
  Poles (K m) a b
polesK :: forall (m :: * -> *) a b.
Monad m =>
(a -> m ()) -> m b -> Poles (K m) a b
polesK a -> m ()
write m b
receive = K m a () -> K m () b -> Poles (K m) a b
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (bot :: k).
HasDual bot arr =>
arr a bot -> arr bot b -> Poles arr a b
poles ((a -> m ()) -> K m a ()
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K a -> m ()
write) ((() -> m b) -> K m () b
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((() -> m b) -> K m () b) -> (() -> m b) -> K m () b
forall a b. (a -> b) -> a -> b
$ m b -> () -> m b
forall a b. a -> b -> a
const m b
receive)

-- | Extract the primitive write and read actions from a @Poles@ by
-- plugging each pole with the dualising-object poles.
--
-- For a @Poles@ built with 'poles', this recovers the original
-- @write :: arr a bot@ and @receive :: arr bot b@.
--
-- >>> let p = poles0 (\() -> ()) (const (42 :: Int)) :: Poles (->) () Int
-- >>> let (write, receive) = splay0 p
-- >>> (write (), receive ())
-- ((),42)
splay ::
  forall arr a b bot.
  (HasDual bot arr) =>
  Poles arr a b ->
  (arr a bot, arr bot b)
splay :: forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (bot :: k).
HasDual bot arr =>
Poles arr a b -> (arr a bot, arr bot b)
splay Poles arr a b
p =
  ( In arr a -> forall (x :: k). Out arr x -> arr a x
forall {k} {k} (arr :: k -> k -> *) (a :: k).
In arr a -> forall (x :: k). Out arr x -> arr a x
commit (Poles arr a b -> In arr a
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> In arr a
conjoint Poles arr a b
p) (Poles arr bot bot -> Out arr bot
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> Out arr b
companion (Poles arr bot bot
forall {k} (bot :: k) (arr :: k -> k -> *).
HasDual bot arr =>
Poles arr bot bot
open :: Poles arr bot bot)),
    Out arr b -> forall (x :: k). In arr x -> arr x b
forall {k} {k} (arr :: k -> k -> *) (a :: k).
Out arr a -> forall (x :: k). In arr x -> arr x a
emit (Poles arr a b -> Out arr b
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> Out arr b
companion Poles arr a b
p) (Poles arr bot bot -> In arr bot
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> In arr a
conjoint (Poles arr bot bot
forall {k} (bot :: k) (arr :: k -> k -> *).
HasDual bot arr =>
Poles arr bot bot
open :: Poles arr bot bot))
  )

-- | Convenience version of 'splay' when the dualising object is @()@.
splay0 ::
  (HasDual () arr) =>
  Poles arr a b ->
  (arr a (), arr () b)
splay0 :: forall (arr :: * -> * -> *) a b.
HasDual () arr =>
Poles arr a b -> (arr a (), arr () b)
splay0 = forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (bot :: k).
HasDual bot arr =>
Poles arr a b -> (arr a bot, arr bot b)
forall (arr :: * -> * -> *) a b bot.
HasDual bot arr =>
Poles arr a b -> (arr a bot, arr bot b)
splay @_ @_ @_ @()
{-# INLINE splay0 #-}

-- * Composition

-- | Sequential composition of @Poles@.
--
-- Given @p1 :: Poles arr a b@ and @p2 :: Poles arr b c@, produce an
-- @Poles arr a c@ by connecting the @b@ pole of @p1@ to the @b@ pole of
-- @p2@.  The primitive actions are extracted via 'splay' and reassembled
-- with 'poles', so 'box' preserves the composition:
--
-- @box (compose p1 p2) = box p2 . box p1@
--
-- Identity exists at the chosen unit type: @open :: Poles arr u u@ is
-- the identity for composition.
--
-- >>> let p1 = poles0 (const ()) (const 1 :: () -> Int) :: Poles (->) () Int
-- >>> let p2 = poles0 (const ()) (const 2 :: () -> Int) :: Poles (->) Int Int
-- >>> box @() (compose0 p1 p2) ()
-- 2
--
-- 'open' at the dualising object is the identity for composition:
--
-- >>> let r = poles @(->) @Bool @Bool @Bool not not
-- >>> box @Bool (compose @_ @_ @_ @_ @Bool (open :: Poles (->) Bool Bool) r) True
-- True
compose ::
  forall arr a b c bot.
  (HasDual bot arr) =>
  Poles arr a b ->
  Poles arr b c ->
  Poles arr a c
compose :: forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k)
       (bot :: k).
HasDual bot arr =>
Poles arr a b -> Poles arr b c -> Poles arr a c
compose Poles arr a b
p1 Poles arr b c
p2 =
  let (arr a bot
write1, arr bot b
read1) = Poles arr a b -> (arr a bot, arr bot b)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (bot :: k).
HasDual bot arr =>
Poles arr a b -> (arr a bot, arr bot b)
splay Poles arr a b
p1 :: (arr a bot, arr bot b)
      (arr b bot
write2, arr bot c
read2) = Poles arr b c -> (arr b bot, arr bot c)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (bot :: k).
HasDual bot arr =>
Poles arr a b -> (arr a bot, arr bot b)
splay Poles arr b c
p2 :: (arr b bot, arr bot c)
   in arr a bot -> arr bot c -> Poles arr a c
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (bot :: k).
HasDual bot arr =>
arr a bot -> arr bot b -> Poles arr a b
poles arr a bot
write1 (arr bot b
read1 arr bot b -> arr b bot -> arr bot bot
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr b bot
write2 arr bot bot -> arr bot c -> arr bot c
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr bot c
read2)

-- | Convenience version of 'compose' when the dualising object is @()@.
compose0 ::
  (HasDual () arr) =>
  Poles arr a b ->
  Poles arr b c ->
  Poles arr a c
compose0 :: forall (arr :: * -> * -> *) a b c.
HasDual () arr =>
Poles arr a b -> Poles arr b c -> Poles arr a c
compose0 = forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k)
       (bot :: k).
HasDual bot arr =>
Poles arr a b -> Poles arr b c -> Poles arr a c
forall (arr :: * -> * -> *) a b c bot.
HasDual bot arr =>
Poles arr a b -> Poles arr b c -> Poles arr a c
compose @_ @_ @_ @_ @()
{-# INLINE compose0 #-}

-- | Forward-composition operator for @Poles@.  @p1 >:> p2 = compose p1 p2@.
(>:>) ::
  forall arr a b c bot.
  (HasDual bot arr) =>
  Poles arr a b ->
  Poles arr b c ->
  Poles arr a c
Poles arr a b
p1 >:> :: forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k)
       (bot :: k).
HasDual bot arr =>
Poles arr a b -> Poles arr b c -> Poles arr a c
>:> Poles arr b c
p2 = forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k)
       (bot :: k).
HasDual bot arr =>
Poles arr a b -> Poles arr b c -> Poles arr a c
forall (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k) (bot :: k).
HasDual bot arr =>
Poles arr a b -> Poles arr b c -> Poles arr a c
compose @arr @a @b @c @bot Poles arr a b
p1 Poles arr b c
p2

infixr 1 >:>

-- | Parallel composition of @Poles@.
--
-- Pair two @Poles@ side by side on the tensor @t@.  The primitive
-- actions are tensored and then collapsed to and from the dualising object
-- with the tensor unitors.  This requires the tensor unit to coincide with
-- the dualising object @bot@; in practice this is the cartesian @(,)@ tensor
-- with @bot = ()@.
--
-- >>> let p1 = poles0 (const ()) (const 1 :: () -> Int) :: Poles (->) () Int
-- >>> let p2 = poles0 (const ()) (const 2 :: () -> Int) :: Poles (->) () Int
-- >>> box @() (polesTensor p1 p2) ((), ())
-- (1,2)
polesTensor ::
  forall t arr a b c d bot.
  (Tensor t arr, HasDual bot arr, Unit t ~ bot) =>
  Poles arr a b ->
  Poles arr c d ->
  Poles arr (t a c) (t b d)
polesTensor :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k) (d :: k) (bot :: k).
(Tensor t arr, HasDual bot arr, Unit t ~ bot) =>
Poles arr a b -> Poles arr c d -> Poles arr (t a c) (t b d)
polesTensor Poles arr a b
p1 Poles arr c d
p2 =
  let (arr a bot
write1, arr bot b
read1) = Poles arr a b -> (arr a bot, arr bot b)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (bot :: k).
HasDual bot arr =>
Poles arr a b -> (arr a bot, arr bot b)
splay Poles arr a b
p1 :: (arr a bot, arr bot b)
      (arr c bot
write2, arr bot d
read2) = Poles arr c d -> (arr c bot, arr bot d)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (bot :: k).
HasDual bot arr =>
Poles arr a b -> (arr a bot, arr bot b)
splay Poles arr c d
p2 :: (arr c bot, arr bot d)
      write :: arr (t a c) bot
write = arr (t bot bot) bot
arr (t bot (Unit t)) bot
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
Tensor.unitr arr (t bot bot) bot -> arr (t a c) (t bot bot) -> arr (t a c) bot
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 bot -> arr c bot -> arr (t a c) (t bot bot)
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.tensor arr a bot
write1 arr c bot
write2
      readPoles :: arr bot (t b d)
readPoles = arr bot b -> arr bot d -> arr (t bot bot) (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.tensor arr bot b
read1 arr bot d
read2 arr (t bot bot) (t b d) -> arr bot (t bot bot) -> arr bot (t b d)
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 bot (t bot bot)
arr bot (t (Unit t) bot)
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)
Tensor.unitl'
   in arr (t a c) bot -> arr bot (t b d) -> Poles arr (t a c) (t b d)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (bot :: k).
HasDual bot arr =>
arr a bot -> arr bot b -> Poles arr a b
poles arr (t a c) bot
write arr bot (t b d)
readPoles

-- | Precompose the input and postcompose the output of a @Poles@.
--
-- This is the morphism-level profunctor action: @f :: arr a' a@ shapes
-- what the conjoint sees, and @g :: arr b b'@ shapes what the companion
-- emits.
--
-- >>> let p = poles0 (const ()) (const 42 :: () -> Int) :: Poles (->) () Int
-- >>> let p' = iomap (const ()) ((+1) :: Int -> Int) p :: Poles (->) () Int
-- >>> box @() p' ()
-- 43
iomap ::
  forall arr a a' b b'.
  (Category arr) =>
  arr a' a ->
  arr b b' ->
  Poles arr a b ->
  Poles arr a' b'
iomap :: forall {k} (arr :: k -> k -> *) (a :: k) (a' :: k) (b :: k)
       (b' :: k).
Category arr =>
arr a' a -> arr b b' -> Poles arr a b -> Poles arr a' b'
iomap arr a' a
f arr b b'
g (Poles In arr a
i Out arr b
o) = In arr a' -> Out arr b' -> Poles arr a' b'
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
In arr a -> Out arr b -> Poles arr a b
Poles (arr a' a -> In arr a -> In arr a'
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Category arr =>
arr a b -> In arr b -> In arr a
prefixIn arr a' a
f In arr a
i) (Out arr b -> arr b b' -> Out arr b'
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Category arr =>
Out arr a -> arr a b -> Out arr b
suffixOut Out arr b
o arr b b'
g)

-- | Precompose the input of a @Poles@.
imap ::
  forall arr a a' b.
  (Category arr) =>
  arr a' a ->
  Poles arr a b ->
  Poles arr a' b
imap :: forall {k} (arr :: k -> k -> *) (a :: k) (a' :: k) (b :: k).
Category arr =>
arr a' a -> Poles arr a b -> Poles arr a' b
imap arr a' a
f (Poles In arr a
i Out arr b
o) = In arr a' -> Out arr b -> Poles arr a' b
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
In arr a -> Out arr b -> Poles arr a b
Poles (arr a' a -> In arr a -> In arr a'
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Category arr =>
arr a b -> In arr b -> In arr a
prefixIn arr a' a
f In arr a
i) Out arr b
o

-- | Postcompose the output of a @Poles@.
omap ::
  forall arr a b b'.
  (Category arr) =>
  arr b b' ->
  Poles arr a b ->
  Poles arr a b'
omap :: forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (b' :: k).
Category arr =>
arr b b' -> Poles arr a b -> Poles arr a b'
omap arr b b'
g (Poles In arr a
i Out arr b
o) = In arr a -> Out arr b' -> Poles arr a b'
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
In arr a -> Out arr b -> Poles arr a b
Poles In arr a
i (Out arr b -> arr b b' -> Out arr b'
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Category arr =>
Out arr a -> arr a b -> Out arr b
suffixOut Out arr b
o arr b b'
g)

-- | Dualising object @()@ for @(->)@.
--
-- The companion is the constant function returning @()@; the conjoint
-- recursively emits through the supplied companion.
instance HasDual () (->) where
  open :: Poles (->) () ()
open = In (->) () -> Out (->) () -> Poles (->) () ()
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
In arr a -> Out arr b -> Poles arr a b
Poles In (->) ()
forall {k} {k} {arr :: k -> k -> *} {a :: k}. In arr a
inU Out (->) ()
outU
    where
      outU :: Out (->) ()
outU = (forall x. In (->) x -> x -> ()) -> Out (->) ()
forall {k} {k} (arr :: k -> k -> *) (a :: k).
(forall (x :: k). In arr x -> arr x a) -> Out arr a
Out ((forall x. In (->) x -> x -> ()) -> Out (->) ())
-> (forall x. In (->) x -> x -> ()) -> Out (->) ()
forall a b. (a -> b) -> a -> b
$ \In (->) x
_ -> () -> x -> ()
forall a b. a -> b -> a
const ()
      inU :: In arr a
inU = (forall (x :: k). Out arr x -> arr a x) -> In arr a
forall {k} {k} (arr :: k -> k -> *) (a :: k).
(forall (x :: k). Out arr x -> arr a x) -> In arr a
In ((forall (x :: k). Out arr x -> arr a x) -> In arr a)
-> (forall (x :: k). Out arr x -> arr a x) -> In arr a
forall a b. (a -> b) -> a -> b
$ \Out arr x
o -> Out arr x -> forall (x :: k). In arr x -> arr x x
forall {k} {k} (arr :: k -> k -> *) (a :: k).
Out arr a -> forall (x :: k). In arr x -> arr x a
emit Out arr x
o In arr a
inU

-- | Dualising object @()@ for @K@ @m@.
--
-- Same shape as the @(->)@ instance, but the constant companion returns
-- @()@ in the monad.
instance (Monad m) => HasDual () (K m) where
  open :: Poles (K m) () ()
open = In (K m) () -> Out (K m) () -> Poles (K m) () ()
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
In arr a -> Out arr b -> Poles arr a b
Poles In (K m) ()
forall {k} {k} {arr :: k -> k -> *} {a :: k}. In arr a
inU Out (K m) ()
outU
    where
      outU :: Out (K m) ()
outU = (forall x. In (K m) x -> K m x ()) -> Out (K m) ()
forall {k} {k} (arr :: k -> k -> *) (a :: k).
(forall (x :: k). In arr x -> arr x a) -> Out arr a
Out ((forall x. In (K m) x -> K m x ()) -> Out (K m) ())
-> (forall x. In (K m) x -> K m x ()) -> Out (K m) ()
forall a b. (a -> b) -> a -> b
$ \In (K m) x
_ -> (x -> m ()) -> K m x ()
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((x -> m ()) -> K m x ()) -> (x -> m ()) -> K m x ()
forall a b. (a -> b) -> a -> b
$ \x
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      inU :: In arr a
inU = (forall (x :: k). Out arr x -> arr a x) -> In arr a
forall {k} {k} (arr :: k -> k -> *) (a :: k).
(forall (x :: k). Out arr x -> arr a x) -> In arr a
In ((forall (x :: k). Out arr x -> arr a x) -> In arr a)
-> (forall (x :: k). Out arr x -> arr a x) -> In arr a
forall a b. (a -> b) -> a -> b
$ \Out arr x
o -> Out arr x -> forall (x :: k). In arr x -> arr x x
forall {k} {k} (arr :: k -> k -> *) (a :: k).
Out arr a -> forall (x :: k). In arr x -> arr x a
emit Out arr x
o In arr a
inU

-- $dualising-object
--
-- The class parameter @bot@ is the object through which the two poles of a
-- 'Poles' are plugged.  For the cartesian @(,)@ tensor this is the monoidal
-- unit @()@, which is terminal.  'copycat' yanks to the identity on @bot@
-- exactly when @bot@ is terminal; for non-terminal objects such as 'Bool'
-- the same 'open' still typechecks but 'copycat' becomes a constant
-- endomorphism rather than the identity.  The 'Bool' instances below make
-- that plumbing explicit.

-- | Dualising object 'Bool' for @(->)@.
--
-- The companion is the constant function returning 'False'; the conjoint
-- recursively emits through the supplied companion.  Because 'Bool' is not
-- terminal, 'copycat' at 'Bool' is the constant function, not the identity.
instance HasDual Bool (->) where
  open :: Poles (->) Bool Bool
open = In (->) Bool -> Out (->) Bool -> Poles (->) Bool Bool
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
In arr a -> Out arr b -> Poles arr a b
Poles In (->) Bool
forall {k} {k} {arr :: k -> k -> *} {a :: k}. In arr a
inU Out (->) Bool
outU
    where
      outU :: Out (->) Bool
outU = (forall x. In (->) x -> x -> Bool) -> Out (->) Bool
forall {k} {k} (arr :: k -> k -> *) (a :: k).
(forall (x :: k). In arr x -> arr x a) -> Out arr a
Out ((forall x. In (->) x -> x -> Bool) -> Out (->) Bool)
-> (forall x. In (->) x -> x -> Bool) -> Out (->) Bool
forall a b. (a -> b) -> a -> b
$ \In (->) x
_ -> Bool -> x -> Bool
forall a b. a -> b -> a
const Bool
False
      inU :: In arr a
inU = (forall (x :: k). Out arr x -> arr a x) -> In arr a
forall {k} {k} (arr :: k -> k -> *) (a :: k).
(forall (x :: k). Out arr x -> arr a x) -> In arr a
In ((forall (x :: k). Out arr x -> arr a x) -> In arr a)
-> (forall (x :: k). Out arr x -> arr a x) -> In arr a
forall a b. (a -> b) -> a -> b
$ \Out arr x
o -> Out arr x -> forall (x :: k). In arr x -> arr x x
forall {k} {k} (arr :: k -> k -> *) (a :: k).
Out arr a -> forall (x :: k). In arr x -> arr x a
emit Out arr x
o In arr a
inU

-- | Dualising object 'Bool' for @K@ @m@.
--
-- Same shape as the @(->)@ instance, but the constant companion returns
-- 'False' in the monad.
instance (Monad m) => HasDual Bool (K m) where
  open :: Poles (K m) Bool Bool
open = In (K m) Bool -> Out (K m) Bool -> Poles (K m) Bool Bool
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
In arr a -> Out arr b -> Poles arr a b
Poles In (K m) Bool
forall {k} {k} {arr :: k -> k -> *} {a :: k}. In arr a
inU Out (K m) Bool
outU
    where
      outU :: Out (K m) Bool
outU = (forall x. In (K m) x -> K m x Bool) -> Out (K m) Bool
forall {k} {k} (arr :: k -> k -> *) (a :: k).
(forall (x :: k). In arr x -> arr x a) -> Out arr a
Out ((forall x. In (K m) x -> K m x Bool) -> Out (K m) Bool)
-> (forall x. In (K m) x -> K m x Bool) -> Out (K m) Bool
forall a b. (a -> b) -> a -> b
$ \In (K m) x
_ -> (x -> m Bool) -> K m x Bool
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((x -> m Bool) -> K m x Bool) -> (x -> m Bool) -> K m x Bool
forall a b. (a -> b) -> a -> b
$ \x
_ -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
      inU :: In arr a
inU = (forall (x :: k). Out arr x -> arr a x) -> In arr a
forall {k} {k} (arr :: k -> k -> *) (a :: k).
(forall (x :: k). Out arr x -> arr a x) -> In arr a
In ((forall (x :: k). Out arr x -> arr a x) -> In arr a)
-> (forall (x :: k). Out arr x -> arr a x) -> In arr a
forall a b. (a -> b) -> a -> b
$ \Out arr x
o -> Out arr x -> forall (x :: k). In arr x -> arr x x
forall {k} {k} (arr :: k -> k -> *) (a :: k).
Out arr a -> forall (x :: k). In arr x -> arr x a
emit Out arr x
o In arr a
inU

-- | Close a @Poles@ to a plain base-arrow morphism.
--
-- A matched pair of free poles (@Poles@) is a box with one input wire and
-- one output wire.  This helper embeds that box into a traced monoidal
-- category by unit-plugging the remaining two slots, giving a plain
-- @arr a b@: input on the left, output on the right, with the unit plumbing
-- hidden.
--
-- >>> let p = poles0 (const ()) (const 42) :: Poles (->) () Int
-- >>> box @() p ()
-- 42
box ::
  forall bot arr a b.
  (HasDual bot arr) =>
  Poles arr a b ->
  arr a b
box :: forall {k} (bot :: k) (arr :: k -> k -> *) (a :: k) (b :: k).
HasDual bot arr =>
Poles arr a b -> arr a b
box Poles arr a b
p =
  In arr a -> forall (x :: k). Out arr x -> arr a x
forall {k} {k} (arr :: k -> k -> *) (a :: k).
In arr a -> forall (x :: k). Out arr x -> arr a x
commit (Poles arr a b -> In arr a
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> In arr a
conjoint Poles arr a b
p) (Poles arr bot bot -> Out arr bot
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> Out arr b
companion (Poles arr bot bot
forall {k} (bot :: k) (arr :: k -> k -> *).
HasDual bot arr =>
Poles arr bot bot
open :: Poles arr bot bot))
    arr a bot -> arr bot b -> arr a b
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> Out arr b -> forall (x :: k). In arr x -> arr x b
forall {k} {k} (arr :: k -> k -> *) (a :: k).
Out arr a -> forall (x :: k). In arr x -> arr x a
emit (Poles arr a b -> Out arr b
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> Out arr b
companion Poles arr a b
p) (Poles arr bot bot -> In arr bot
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> In arr a
conjoint (Poles arr bot bot
forall {k} (bot :: k) (arr :: k -> k -> *).
HasDual bot arr =>
Poles arr bot bot
open :: Poles arr bot bot))

-- | Asymmetric box with the dualising object exposed on opposite sides.
--
-- Uses 'Circuit.Tensor.tensor' at the base arrow level. The input carries the dualising object
-- on the right and the output carries it on the left; most users will prefer
-- the dualising-object-normalised 'box'.
--
-- >>> let p = poles0 (const ()) (const 42) :: Poles (->) () Int
-- >>> boxAsymmetric @() p ((), ())
-- ((),42)
boxAsymmetric ::
  forall bot t arr a b.
  (HasDual bot arr, Tensor t arr) =>
  Poles arr a b ->
  arr (t a bot) (t bot b)
boxAsymmetric :: forall {k} (bot :: k) (t :: k -> k -> k) (arr :: k -> k -> *)
       (a :: k) (b :: k).
(HasDual bot arr, Tensor t arr) =>
Poles arr a b -> arr (t a bot) (t bot b)
boxAsymmetric Poles arr a b
p =
  arr a bot -> arr bot b -> arr (t a bot) (t bot b)
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.tensor
    (In arr a -> forall (x :: k). Out arr x -> arr a x
forall {k} {k} (arr :: k -> k -> *) (a :: k).
In arr a -> forall (x :: k). Out arr x -> arr a x
commit (Poles arr a b -> In arr a
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> In arr a
conjoint Poles arr a b
p) (Poles arr bot bot -> Out arr bot
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> Out arr b
companion Poles arr bot bot
forall {k} (bot :: k) (arr :: k -> k -> *).
HasDual bot arr =>
Poles arr bot bot
open))
    (Out arr b -> forall (x :: k). In arr x -> arr x b
forall {k} {k} (arr :: k -> k -> *) (a :: k).
Out arr a -> forall (x :: k). In arr x -> arr x a
emit (Poles arr a b -> Out arr b
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> Out arr b
companion Poles arr a b
p) (Poles arr bot bot -> In arr bot
forall {k} {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Poles arr a b -> In arr a
conjoint Poles arr bot bot
forall {k} (bot :: k) (arr :: k -> k -> *).
HasDual bot arr =>
Poles arr bot bot
open))

-- * Additive connectives

-- $setup
-- >>> import Circuit.Poles
-- >>> import Circuit.Layer (run)
-- >>> import Data.Maybe (isNothing)

-- | Additive conjunction: both sub-poles receive the same input and their
-- outputs are paired.
--
-- This is the @&@ connective / @await@ fragment: every branch sees the
-- input, and the composite emits all of their results.
--
-- >>> let p1 = poles0 (const ()) (const 1 :: () -> Int) :: Poles (->) () Int
-- >>> let p2 = poles0 (const ()) (const 2 :: () -> Int) :: Poles (->) () Int
-- >>> box @() (pair p1 p2) ()
-- (1,2)
pair ::
  forall arr a b c.
  (HasDual () arr, Tensor (,) arr, Copy arr a) =>
  Poles arr a b ->
  Poles arr a c ->
  Poles arr a (b, c)
pair :: forall (arr :: * -> * -> *) a b c.
(HasDual () arr, Tensor (,) arr, Copy arr a) =>
Poles arr a b -> Poles arr a c -> Poles arr a (b, c)
pair Poles arr a b
p1 Poles arr a c
p2 =
  let (arr a ()
w1, arr () b
r1) = Poles arr a b -> (arr a (), arr () b)
forall (arr :: * -> * -> *) a b.
HasDual () arr =>
Poles arr a b -> (arr a (), arr () b)
splay0 Poles arr a b
p1
      (arr a ()
w2, arr () c
r2) = Poles arr a c -> (arr a (), arr () c)
forall (arr :: * -> * -> *) a b.
HasDual () arr =>
Poles arr a b -> (arr a (), arr () b)
splay0 Poles arr a c
p2
      w :: arr a ()
w = arr ((), ()) ()
arr ((), Unit (,)) ()
forall a. arr (a, Unit (,)) a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr (t a (Unit t)) a
Tensor.unitr arr ((), ()) () -> arr (a, a) ((), ()) -> arr (a, 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 () -> arr a () -> arr (a, a) ((), ())
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.tensor arr a ()
w1 arr a ()
w2 arr (a, a) () -> arr a (a, a) -> 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 (a, a)
forall (arr :: * -> * -> *) a. Copy arr a => arr a (a, a)
copy
      r :: arr () (b, c)
r = arr () b -> arr () c -> arr ((), ()) (b, c)
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.tensor arr () b
r1 arr () c
r2 arr ((), ()) (b, c) -> arr () ((), ()) -> arr () (b, c)
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 () ((), ())
arr () (Unit (,), ())
forall a. arr a (Unit (,), a)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr a (t (Unit t) a)
Tensor.unitl'
   in arr a () -> arr () (b, c) -> Poles arr a (b, c)
forall (arr :: * -> * -> *) a b.
HasDual () arr =>
arr a () -> arr () b -> Poles arr a b
poles0 arr a ()
w arr () (b, c)
r

-- | Additive disjunction / race: both sub-poles receive the same input, but
-- only the first output satisfying the predicate is emitted.
--
-- The predicate selects "silent" values that should be skipped. The bias
-- chooses which side to prefer when both are non-silent. The picking logic is
-- lifted into the base arrow via 'FunctionLike'.
--
-- >>> let eL = poles0 (const ()) (const (Just 1)) :: Poles (->) () (Maybe Int)
-- >>> let eR = poles0 (const ()) (const (Just 2)) :: Poles (->) () (Maybe Int)
-- >>> box @() (race isNothing LeftFirst eL eR) ()
-- Just 1
-- >>> box @() (race isNothing RightFirst eL eR) ()
-- Just 2
race ::
  forall arr a b.
  (HasDual () arr, Tensor (,) arr, Copy arr a, FunctionLike arr) =>
  (b -> Bool) ->
  Bias ->
  Poles arr a b ->
  Poles arr a b ->
  Poles arr a b
race :: forall (arr :: * -> * -> *) a b.
(HasDual () arr, Tensor (,) arr, Copy arr a, FunctionLike arr) =>
(b -> Bool)
-> Bias -> Poles arr a b -> Poles arr a b -> Poles arr a b
race b -> Bool
isSilent Bias
bias Poles arr a b
p1 Poles arr a b
p2 = arr (b, b) b -> Poles arr a (b, b) -> Poles arr a b
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (b' :: k).
Category arr =>
arr b b' -> Poles arr a b -> Poles arr a b'
omap (((b, b) -> b) -> arr (b, b) b
forall a b. (a -> b) -> arr a b
forall (arr :: * -> * -> *) a b.
FunctionLike arr =>
(a -> b) -> arr a b
function (Bias -> (b, b) -> b
pick Bias
bias)) (Poles arr a b -> Poles arr a b -> Poles arr a (b, b)
forall (arr :: * -> * -> *) a b c.
(HasDual () arr, Tensor (,) arr, Copy arr a) =>
Poles arr a b -> Poles arr a c -> Poles arr a (b, c)
pair Poles arr a b
p1 Poles arr a b
p2)
  where
    pick :: Bias -> (b, b) -> b
pick Bias
LeftFirst (b
x, b
y) = if b -> Bool
isSilent b
x then b
y else b
x
    pick Bias
RightFirst (b
x, b
y) = if b -> Bool
isSilent b
y then b
x else b
y