Safe Haskell	None
Language	GHC2024

Circuit.Bimonoid

Contents

Copy
Discard
Merge
Zero
Bundled synonyms
Free-syntax signatures
The substructural square
Tensor-generic capabilities

Description

The bimonoid layer of circuit wiring.

This module collects the algebraic structure that every wire may carry in a circuit category:

Copy Discard — the comonoid on channel objects (fan-out weakening).
Merge Zero — the monoid on channel objects (fan-in introduction).
Bimonoid — all four together, the precondition for mirror to be total on a cartesian base arrow.

For a generic wiring tensor t the tensor-generic classes CopyT, DiscardT, MergeT and ZeroT play the same role. The cartesian classes are the special case t = (,), recovered via the OVERLAPPABLE default instances at the bottom of this module.

The free dagger category itself (pairing a forward arrow with a backward arrow and swapping them with transpose) lives in Circuit.Dagger; this module is only the structural rules.

Design note: $copy-discard-design.

Synopsis

class Copy (arr :: Type -> Type -> Type) a where
- copy :: arr a (a, a)
class Discard (arr :: k -> Type -> Type) (a :: k) where
- discard :: arr a ()
class Merge (arr :: Type -> Type -> Type) a where
- plus :: arr (a, a) a
class Zero (arr :: Type -> k -> Type) (a :: k) where
- zero :: arr () a
type CopyDiscard (arr :: Type -> Type -> Type) a = (Copy arr a, Discard arr a)
type MergeZero (arr :: Type -> Type -> Type) a = (Merge arr a, Zero arr a)
type Bimonoid (arr :: Type -> Type -> Type) a = (Copy arr a, Discard arr a, Merge arr a, Zero arr a)
data SigCopy (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) (rec :: k) a b where
- SigCopy :: forall {k} (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) a (rec :: k). CopyT w arr a => SigCopy w arr rec a (w a a)
data SigDiscard (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) (rec :: k) a b where
- SigDiscard :: forall {k} (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) a (rec :: k). DiscardT w arr a => SigDiscard w arr rec a (Unit w)
type SigCopyDiscard (w :: Type -> Type -> Type) = (SigCopy w :: (Type -> Type -> Type) -> k1 -> Type -> Type -> Type) :+: (SigDiscard w :: (Type -> Type -> Type) -> k1 -> Type -> Type -> Type)
data SigPlus (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) (rec :: k) a b where
- SigPlus :: forall {k} (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) b (rec :: k). MergeT w arr b => SigPlus w arr rec (w b b) b
data SigZero (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) (rec :: k) a b where
- SigZero :: forall {k} (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) b (rec :: k). ZeroT w arr b => SigZero w arr rec (Unit w) b
type SigMergeZero (w :: Type -> Type -> Type) = (SigPlus w :: (Type -> Type -> Type) -> k1 -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> k1 -> Type -> Type -> Type)
type Affine (arr :: k -> Type -> Type) (a :: k) = Discard arr a
type Relevant (arr :: Type -> Type -> Type) a = Copy arr a
type Cartesian (arr :: Type -> Type -> Type) a = (Copy arr a, Discard arr a)
type CoAffine (arr :: Type -> k -> Type) (a :: k) = Zero arr a
type CoRelevant (arr :: Type -> Type -> Type) a = Merge arr a
class Tensor t arr => CopyT (t :: k -> k -> k) (arr :: k -> k -> Type) (a :: k) where
- copyT :: arr a (t a a)
class Tensor t arr => DiscardT (t :: k -> k -> k) (arr :: k -> k -> Type) (a :: k) where
- discardT :: arr a (Unit t)
class Tensor t arr => MergeT (t :: k -> k -> k) (arr :: k -> k -> Type) (a :: k) where
- plusT :: arr (t a a) a
class Tensor t arr => ZeroT (t :: k -> k -> k) (arr :: k -> k -> Type) (a :: k) where
- zeroT :: arr (Unit t) a
class (CopyT t arr a, DiscardT t arr a, MergeT t arr a, ZeroT t arr a) => BimonoidT (t :: k -> k -> k) (arr :: k -> k -> Type) (a :: k)

Copy

class Copy (arr :: Type -> Type -> Type) a where Source #

Copy a value into a pair.

Laws:

  fst . copy = id              -- left unit
  snd . copy = id              -- right unit
  (copy × id) . copy = (id × copy) . copy  -- coassociativity
  braid . copy = copy            -- cocommutativity

Methods

copy :: arr a (a, a) Source #

Instances

Instances details

Copy FinRel () Source #
Instance details Defined in Circuit.FinRel Methods copy :: FinRel () ((), ()) Source #
Copy (->) a => Copy Process a Source #
Instance details Defined in Circuit.Process Methods copy :: Process a (a, a) Source #
Copy Pullback a Source #	Pullback-instance of the comonoid structure. Copy's pullback is addition; discard's pullback is the zero cotangent. These are not used by the transposition step of reverse-mode AD (which encodes structural rows as `Lift`s to avoid channel-type constraints), but they make `Pullback` a full bimonoid carrier. `>>>` `runPullback (copy :: Pullback Int (Int, Int)) 3`(3,3) `>>>` `runPullback (discard :: Pullback Int ()) 5`() NOTE: neither method here uses an `Additive (->) a` constraint — copying and discarding are linear as they stand. If the class head permits, drop the constraint; keeping a stray `Additive` reads as "addition happens in this instance", which is the confusion the paragraph above tries to dispel.
Instance details Defined in Circuit.Pullback Methods copy :: Pullback a (a, a) Source #
KnownNat n => Copy FinRel (FinObj n) Source #
Instance details Defined in Circuit.FinRel Methods copy :: FinRel (FinObj n) (FinObj n, FinObj n) Source #
(Copy arr a, Merge arr a) => Copy (Dagger arr) a Source #	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 details Defined in Circuit.Dagger Methods copy :: Dagger arr a (a, a) Source #
Copy (->) Integer Source #
Instance details Defined in Circuit.Bimonoid Methods copy :: Integer -> (Integer, Integer) Source #
Copy (->) () Source #	Unit trivially copies and discards. `>>>` `copy (() :: ())`((),()) `>>>` `discard (() :: ())`()
Instance details Defined in Circuit.Bimonoid Methods copy :: () -> ((), ()) Source #
Copy (->) Bool Source #	Booleans copy and discard. `>>>` `copy True`(True,True) `>>>` `discard True`()
Instance details Defined in Circuit.Bimonoid Methods copy :: Bool -> (Bool, Bool) Source #
Copy (->) Double Source #
Instance details Defined in Circuit.Bimonoid Methods copy :: Double -> (Double, Double) Source #
Copy (->) Float Source #
Instance details Defined in Circuit.Bimonoid Methods copy :: Float -> (Float, Float) Source #
Copy (->) Int Source #	Numeric scalars copy and discard pointwise. `>>>` `copy (42 :: Int)`(42,42) `>>>` `discard (42 :: Int)`()
Instance details Defined in Circuit.Bimonoid Methods copy :: Int -> (Int, Int) Source #
Copy (->) (Maybe a) Source #	Maybe copies and discards as a whole value.
Instance details Defined in Circuit.Bimonoid Methods copy :: Maybe a -> (Maybe a, Maybe a) Source #
Copy (->) [a] Source #	Lists copy and discard as a whole value.
Instance details Defined in Circuit.Bimonoid Methods copy :: [a] -> ([a], [a]) Source #
Copy (->) (a, b) Source #	Products copy and discard as a whole value.
Instance details Defined in Circuit.Bimonoid Methods copy :: (a, b) -> ((a, b), (a, b)) Source #

Discard

class Discard (arr :: k -> Type -> Type) (a :: k) where Source #

Discard a value.

Methods

discard :: arr a () Source #

Instances

Instances details

Discard FinRel () Source #
Instance details Defined in Circuit.FinRel Methods discard :: FinRel () () Source #
Discard Process (a :: Type) Source #
Instance details Defined in Circuit.Process Methods discard :: Process a () Source #
Discard Pullback (a :: Type) Source #
Instance details Defined in Circuit.Pullback Methods discard :: Pullback a () Source #
KnownNat n => Discard FinRel (FinObj n :: Type) Source #
Instance details Defined in Circuit.FinRel Methods discard :: FinRel (FinObj n) () Source #
(Discard arr a, Zero arr a) => Discard (Dagger arr :: Type -> Type -> Type) (a :: Type) Source #
Instance details Defined in Circuit.Dagger Methods discard :: Dagger arr a () Source #
Discard (->) Integer Source #
Instance details Defined in Circuit.Bimonoid Methods discard :: Integer -> () Source #
Discard (->) () Source #
Instance details Defined in Circuit.Bimonoid Methods discard :: () -> () Source #
Discard (->) Bool Source #
Instance details Defined in Circuit.Bimonoid Methods discard :: Bool -> () Source #
Discard (->) Double Source #
Instance details Defined in Circuit.Bimonoid Methods discard :: Double -> () Source #
Discard (->) Float Source #
Instance details Defined in Circuit.Bimonoid Methods discard :: Float -> () Source #
Discard (->) Int Source #
Instance details Defined in Circuit.Bimonoid Methods discard :: Int -> () Source #
Discard (->) (Maybe a :: Type) Source #
Instance details Defined in Circuit.Bimonoid Methods discard :: Maybe a -> () Source #
Discard (->) ([a] :: Type) Source #
Instance details Defined in Circuit.Bimonoid Methods discard :: [a] -> () Source #
Discard (->) ((a, b) :: Type) Source #
Instance details Defined in Circuit.Bimonoid Methods discard :: (a, b) -> () Source #

Merge

class Merge (arr :: Type -> Type -> Type) a where Source #

Combine two values of the channel type.

Not the same as arithmetic +; this is the monoid operation by which parallel contributions to the same wire combine.

Methods

plus :: arr (a, a) a Source #

Instances

Instances details

Merge FinRel () Source #
Instance details Defined in Circuit.FinRel Methods plus :: FinRel ((), ()) () Source #
Merge (->) a => Merge Process a Source #
Instance details Defined in Circuit.Process Methods plus :: Process (a, a) a Source #
Merge (->) a => Merge Pullback a Source #	Pullback-instance of the additive/monoid structure. Addition's pullback is copying; zero's pullback is discarding. `>>>` `runPullback (plus :: Pullback (Int, Int) Int) (1, 2)`3 `>>>` `runPullback (zero :: Pullback () Int) ()`0
Instance details Defined in Circuit.Pullback Methods plus :: Pullback (a, a) a Source #
KnownNat n => Merge FinRel (FinObj n) Source #
Instance details Defined in Circuit.FinRel Methods plus :: FinRel (FinObj n, FinObj n) (FinObj n) Source #
(Merge arr a, Copy arr a) => Merge (Dagger arr) a Source #	Forward add, backward copy.
Instance details Defined in Circuit.Dagger Methods plus :: Dagger arr (a, a) a Source #
Merge (->) Integer Source #
Instance details Defined in Circuit.Bimonoid Methods plus :: (Integer, Integer) -> Integer Source #
Merge (->) () Source #	The unit type carries the trivial monoid. `>>>` `plus ((), ()) :: ()`() `>>>` `zero () :: ()`()
Instance details Defined in Circuit.Bimonoid Methods plus :: ((), ()) -> () Source #
Merge (->) Bool Source #	Boolean monoid under disjunction. Idempotent because `True \|\| True = True`. `>>>` `plus (True, False) :: Bool`True `>>>` `zero () :: Bool`False
Instance details Defined in Circuit.Bimonoid Methods plus :: (Bool, Bool) -> Bool Source #
Merge (->) Double Source #
Instance details Defined in Circuit.Bimonoid Methods plus :: (Double, Double) -> Double Source #
Merge (->) Float Source #
Instance details Defined in Circuit.Bimonoid Methods plus :: (Float, Float) -> Float Source #
Merge (->) Int Source #	Numeric carriers. `plus` is addition, `zero` is 0. `>>>` `plus (1, 2) :: Int`3 `>>>` `zero () :: Int`0 `>>>` `plus (1.0, 2.0) :: Double`3.0 `>>>` `zero () :: Double`0.0
Instance details Defined in Circuit.Bimonoid Methods plus :: (Int, Int) -> Int Source #
(Merge (->) a, Zero (->) a) => Merge (->) [a] Source #	Lists via elementwise `plus`, padded with `zero`. For lists of unequal length, the shorter list is implicitly extended with the element `zero`. The unit is the empty list. `>>>` `plus ([1, 2], [3, 4, 5]) :: [Int]`[4,6,5] `>>>` `plus ([], [3, 4, 5]) :: [Int]`[3,4,5]
Instance details Defined in Circuit.Bimonoid Methods plus :: ([a], [a]) -> [a] Source #
(Merge (->) a, Merge (->) b) => Merge (->) (a, b) Source #	Componentwise `plus` on pairs. `>>>` `plus ((3, 4), (5, 6)) :: (Int, Int)`(8,10)
Instance details Defined in Circuit.Bimonoid Methods plus :: ((a, b), (a, b)) -> (a, b) Source #

Zero

class Zero (arr :: Type -> k -> Type) (a :: k) where Source #

The neutral element for plus.

Methods

zero :: arr () a Source #

Instances

Instances details

Zero FinRel () Source #
Instance details Defined in Circuit.FinRel Methods zero :: FinRel () () Source #
Zero (->) a => Zero Process (a :: Type) Source #
Instance details Defined in Circuit.Process Methods zero :: Process () a Source #
Zero (->) a => Zero Pullback (a :: Type) Source #
Instance details Defined in Circuit.Pullback Methods zero :: Pullback () a Source #
KnownNat n => Zero FinRel (FinObj n :: Type) Source #
Instance details Defined in Circuit.FinRel Methods zero :: FinRel () (FinObj n) Source #
(Zero arr a, Discard arr a) => Zero (Dagger arr :: Type -> Type -> Type) (a :: Type) Source #
Instance details Defined in Circuit.Dagger Methods zero :: Dagger arr () a Source #
Zero (->) Integer Source #
Instance details Defined in Circuit.Bimonoid Methods zero :: () -> Integer Source #
Zero (->) () Source #
Instance details Defined in Circuit.Bimonoid Methods zero :: () -> () Source #
Zero (->) Bool Source #
Instance details Defined in Circuit.Bimonoid Methods zero :: () -> Bool Source #
Zero (->) Double Source #
Instance details Defined in Circuit.Bimonoid Methods zero :: () -> Double Source #
Zero (->) Float Source #
Instance details Defined in Circuit.Bimonoid Methods zero :: () -> Float Source #
Zero (->) Int Source #
Instance details Defined in Circuit.Bimonoid Methods zero :: () -> Int Source #
Zero (->) ([a] :: Type) Source #
Instance details Defined in Circuit.Bimonoid Methods zero :: () -> [a] Source #
(Zero (->) a, Zero (->) b) => Zero (->) ((a, b) :: Type) Source #
Instance details Defined in Circuit.Bimonoid Methods zero :: () -> (a, b) Source #

Bundled synonyms

type CopyDiscard (arr :: Type -> Type -> Type) a = (Copy arr a, Discard arr a) Source #

The bundled comonoid class, retained as a synonym.

type MergeZero (arr :: Type -> Type -> Type) a = (Merge arr a, Zero arr a) Source #

The bundled monoid class, retained as a synonym.

type Bimonoid (arr :: Type -> Type -> Type) a = (Copy arr a, Discard arr a, Merge arr a, Zero arr a) Source #

Both the comonoid and monoid on a channel object.

A constraint synonym — no instance required. On a cartesian base arrow, every type carries both structures. This is the precondition for mirror to be total on that base arrow.

Free-syntax signatures

data SigCopy (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) (rec :: k) a b where Source #

Copy: the contraction half of the comonoid.

The constructor carries a CopyT constraint on the wiring tensor w, resolved at pattern-match time rather than in the algebra context.

Constructors

SigCopy :: forall {k} (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) a (rec :: k). CopyT w arr a => SigCopy w arr rec a (w a a)

Instances

Instances details

Category arr => Category (Net w arr :: Type -> Type -> Type) Source #

The Category instance is the generic free-category instance: id is a lifted identity and composition is a SigCompose node.

Instance details

(Copy arr a, Tensor (,) arr) => CopyT (,) (arr :: Type -> Type -> Type) (a :: Type) Source #	Every `Copy` instance gives a `CopyT` instance for the cartesian tensor.
Instance details Defined in Circuit.Bimonoid Methods copyT :: arr a (a, a) Source #
(CopyT t arr a, MergeT t arr a) => CopyT (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) (a :: k) Source #	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 `mirror` total: a `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 details Defined in Circuit.Dagger Methods copyT :: Dagger arr a (t a a) Source #

(Discard arr a, Tensor (,) arr) => DiscardT (,) (arr :: Type -> Type -> Type) (a :: Type) Source #	Every `Discard` instance gives a `DiscardT` instance for the cartesian tensor.
Instance details Defined in Circuit.Bimonoid Methods discardT :: arr a (Unit (,)) Source #
(DiscardT t arr a, ZeroT t arr a) => DiscardT (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) (a :: k) Source #
Instance details Defined in Circuit.Dagger Methods discardT :: Dagger arr a (Unit t) Source #

(Merge arr a, Tensor (,) arr) => MergeT (,) (arr :: Type -> Type -> Type) (a :: Type) Source #	Every `Merge` instance gives a `MergeT` instance for the cartesian tensor.
Instance details Defined in Circuit.Bimonoid Methods plusT :: arr (a, a) a Source #
(MergeT t arr a, CopyT t arr a) => MergeT (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) (a :: k) Source #
Instance details Defined in Circuit.Dagger Methods plusT :: Dagger arr (t a a) a Source #

(Zero arr a, Tensor (,) arr) => ZeroT (,) (arr :: Type -> Type -> Type) (a :: Type) Source #	Every `Zero` instance gives a `ZeroT` instance for the cartesian tensor.
Instance details Defined in Circuit.Bimonoid Methods zeroT :: arr (Unit (,)) a Source #
(ZeroT t arr a, DiscardT t arr a) => ZeroT (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) (a :: k) Source #
Instance details Defined in Circuit.Dagger Methods zeroT :: Dagger arr (Unit t) a Source #

(CopyT t arr a, DiscardT t arr a, MergeT t arr a, ZeroT t arr a) => BimonoidT (t :: k -> k -> k) (arr :: k -> k -> Type) (a :: k) Source #
Instance details Defined in Circuit.Bimonoid

Copy

Instances

Discard

Instances

Merge

Instances

Zero

Instances

Bundled synonyms

Free-syntax signatures

Instances

Instances

Instances

Instances

The substructural square

Tensor-generic capabilities

Instances

Instances

Instances

Instances

Instances