circuits
Safe HaskellNone
LanguageGHC2024

Circuit.Net

Description

The free symmetric monoidal category with a bimonoid over a primitive set.

Net extends SMC with structural rows for the bimonoid operations: copy, discard, addition, and zero. Where Trace keeps only base and yank in normal form, Net keeps the wiring inspectable — the difference between wiring you can read backwards and wiring that has been melted into a single loop.

The bimonoid rows are the dagger's fixed structure: they are owned by Circuit.Dagger, and BimonoidT is exactly the precondition that lets Net mirror over Dagger (see mirror).

Free = Lift + Compose
SMC  = Free + Par + Swap
Net  = SMC + Copy + Discard + Plus + Zero

run Net interprets a Net to a plain arrow. melt interprets the structural rows into the free Trace syntax.

Synopsis

Net

type Net (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type))))))) arr Source #

The free symmetric monoidal category with a bimonoid.

Net is the free Syntax over the signature sum

SigCompose :+: SigPar w :+: SigSwap w :+: SigCopy w :+: SigDiscard w :+: SigPlus w :+: SigZero w

The Lift constructor embeds a base arrow; the Op constructor holds one of the signature nodes. Smart constructors lift and braid build the common cases, and widen embeds an entire SMC circuit.

Smart constructors

lift :: forall arr a b (w :: Type -> Type -> Type). arr a b -> Net w arr a b Source #

Lift a base arrow into Net.

braid :: forall w (arr :: Type -> Type -> Type) a b. Net w arr (w a b) (w b a) Source #

Symmetric braiding in Net.

Conversion

widen :: forall (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) a b. SMC w arr a b -> Net w arr a b Source #

Include an SMC circuit into Net.

The injection recurses through the SMC signature sum and rebuilds each node in the larger Net signature sum. This gives the adjunction between SMC and Net together with sift.

>>> let m = SMC.lift (+1) . SMC.lift (*2) :: SMC (,) (->) Int Int
>>> run (widen m :: Net (,) (->) Int Int) 5
11

Coherence: sift projects widen back to the original SMC.

>>> eval (sift (widen m :: Net (,) (->) Int Int)) 5
11
>>> eval m 5
11

Coherence: melt agrees with the function fold on SMC circuits.

>>> eval (melt (widen m :: Net (,) (->) Int Int) :: Trace (,) (->) Int Int) 5
11
>>> eval m 5
11

Coherence: Net folds through widen match SMC folds.

>>> let h f = f
>>> (bind h (widen m :: Net (,) (->) Int Int) :: Int -> Int) 5
11
>>> (evalInto h m :: Int -> Int) 5
11

Coherence: mirroring commutes with widen.

>>> let dm = SMC.lift (Dg.Dagger (+1) (subtract 1)) . SMC.lift (Dg.Dagger (*2) (\x -> x `div` 2)) :: SMC (,) (Dg.Dagger (->)) Int Int
>>> Dg.front (Dg.transpose (eval dm)) 10
4
>>> Dg.front (Dg.transpose (run (widen dm :: Net (,) (Dg.Dagger (->)) Int Int))) 10
4

sift :: forall (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) a b. Action w arr => Net w arr a b -> SMC w arr a b Source #

Forget the bimonoid rows of a Net, keeping only the SMC wiring.

sift collapses the bimonoid rows into lift while leaving SigCompose and SigPar inspectable. Together with widen it gives the adjunction between SMC and Net. Note the converse does not hold: widen . sift ≠ id because sift forgets bimonoid structure.

Interpretation

melt :: forall (w :: Type -> Type -> Type) (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) a b. (Traced t arr, Action w arr) => Net w arr a b -> Trace t arr a b Source #

Melt the structural rows of a Net into the free Trace syntax.

The interpretation from the free symmetric monoidal category with bimonoid to the free traced monoidal category. Structural rows (SigPar, SigCopy, SigPlus, etc.) become opaque base-arrow operations wrapped in base; SigCompose uses the Category instance of Trace.

run Net = eval . melt@.

>>> eval (melt (lift (+1) :: Net (,) (->) Int Int) :: Trace (,) (->) Int Int) 5
6

Dagger

mirror :: forall (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) a b. (forall x. BimonoidT w arr x) => Net w (Dagger arr) a b -> Net w (Dagger arr) b a Source #

Mirror a Net over Dagger.

The dagger dualizes the bimonoid rows: SigCopy becomes SigPlus, SigDiscard becomes SigZero, and vice versa. Composition is reversed; parallel composition and the braiding are self-dual.

This operation is total exactly when the base arrow carries a bimonoid on the wiring tensor for every object, i.e. when BimonoidT w arr x holds for all x. That precondition is the tensor-generic form of the Bimonoid law that makes Dagger and the bimonoid rows presentable as one structure.

Bimonoid syntax fragments (re-exported compatibility aliases)

type AlgRelevant (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))) arr Source #

Free relevant symmetric monoidal category over wiring tensor w.

type AlgAffine (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))) arr Source #

Free affine symmetric monoidal category over wiring tensor w.

type AlgCartesian (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type))))) arr Source #

Free cartesian symmetric monoidal category over wiring tensor w.

type AlgCoRelevant (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))) arr Source #

Free co-relevant symmetric monoidal category over wiring tensor w.

type AlgCoAffine (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))) arr Source #

Free co-affine symmetric monoidal category over wiring tensor w.

type AlgCocartesian (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type))))) arr Source #

Free cocartesian symmetric monoidal category over wiring tensor w.

type AlgBimonoidal (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type))))))) arr Source #

Free bimonoidal category over wiring tensor w.

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

Synonym for the full Net syntax.

Orphan instances

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

Methods

id :: Net w arr a a Source #

(.) :: Net w arr b c -> Net w arr a b -> Net w arr a c Source #

Layer (Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))))))) Source #

Free symmetric monoidal category with a bimonoid.

Structural rows are interpreted in the target category: parallel composition uses tensor, braiding uses braid, and the bimonoid generators are the images under h of the source dictionaries carried by the SigCopy, SigDiscard, SigPlus, and SigZero constructors.

Conditional
bind h interprets bimonoid generators as images under h of the source arrow's dictionaries. This is the free-PROP fold only when h is a bimonoid homomorphism (automatic for the generator embedding, but must be verified for custom h).
Instance details

Methods

unit :: forall (arr :: Type -> Type -> Type). Category arr => arr :~> Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type))))))) arr Source #

run :: (Run (Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))))))) arr, Law (Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))))))) arr, Bind (Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))))))) arr) => Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type))))))) arr a b -> arr a b Source #

bind :: forall arr' (arr :: Cat2) a b. (Law (Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))))))) arr', Bind (Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)))))))) arr) => (arr :~> arr') -> Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: ((SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type))))))) arr a b -> arr' a b Source #