Out is the companion of the identity functor. Covariant in a (sits in the output position).

In is the conjoint of the identity functor. Contravariant in a (sits in the input position).

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.

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.

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
()

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

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)

Convenience version of poles when the dualising object is ().

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.

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)

Convenience version of splay when the dualising object is ().

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

Convenience version of compose when the dualising object is ().

Forward-composition operator for Poles. p1 >:> p2 = compose p1 p2.

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)

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

Precompose the input of a Poles.

Postcompose the output of a 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.

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.

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

Asymmetric box with the dualising object exposed on opposite sides.

Uses 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)

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)

Bias for ordered choice in scheduling and additive disjunction.

LeftFirst and RightFirst are used by shared-medium fusion in Circuit.Shared and by additive disjunction in Circuit.Poles.

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