circuits
Safe HaskellNone
LanguageGHC2024

Circuit.SMC

Description

Free symmetric monoidal category syntax.

This module packages the symmetric-monoidal layer on top of the generic free-construction substrate in Circuit.Syntax. The signature sum is

SigCompose :+: SigPar w :+: SigSwap w

where SigCompose provides sequential composition, SigPar w provides parallel composition over the wiring tensor w, and SigSwap w provides the symmetry / braiding.

The Tensor and Action instances are the syntactic constructors: tensor f g builds a SigPar node and braid builds a SigSwap node. Folding uses eval or evalInto.

Synopsis

Free symmetric monoidal category

type SMC (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))) arr Source #

Free symmetric monoidal category over wiring tensor w.

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

Lift a base arrow into the free symmetric monoidal category.

Dagger mirror

mirror :: forall (w :: Type -> Type -> Type) (arr :: Type -> Type -> Type) a b. SMC w (Dagger arr) a b -> SMC w (Dagger arr) b a Source #

Mirror an SMC built over Dagger.

Reverses composition, transposes each lifted arrow, and leaves tensor and braid self-dual. This is the structural transpose of the SMC layer that mirror delegates to.

Constraint synonym used by Net's Layer law

class Action w arr => FreeSMC (w :: k -> k -> k) (arr :: k -> k -> Type) Source #

Free SMC folds target any category with w-monoidal action.

Instances

Instances details
Action w arr => FreeSMC (w :: k -> k -> k) (arr :: k -> k -> Type) Source # 
Instance details

Defined in Circuit.SMC

Signatures (exported for other syntax layers)

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

Parallel composition over the wiring tensor w.

Constructors

SigPar :: forall {k} (rec :: Type -> Type -> Type) a1 b1 c d (w :: Type -> Type -> Type) (arr :: k). rec a1 b1 -> rec c d -> SigPar w arr rec (w a1 c) (w b1 d) 

Instances

Instances details
(Category arr, Channel t arr) => Channel (t :: Type -> Type -> Type) (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

assoc :: SMC w arr (t (t a b) c) (t a (t b c)) Source #

assoc' :: SMC w arr (t a (t b c)) (t (t a b) c) Source #

slide :: SMC w arr (t a (t b c)) (t b (t a c)) Source #

(Strength t arr, Action w arr) => Strength (t :: Type -> Type -> Type) (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

strength :: SMC w arr b c -> SMC w arr (t a b) (t a c) Source #

(Traced t arr, Action w arr) => Traced (t :: Type -> Type -> Type) (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

trace :: SMC w arr (t a b) (t a c) -> SMC w arr b c Source #

Action w arr => Action (w :: Type -> Type -> Type) (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

braid :: SMC w arr (w a b) (w b a) Source #

Tensor w arr => Tensor (w :: Type -> Type -> Type) (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

tensor :: SMC w arr a b -> SMC w arr c d -> SMC w arr (w a c) (w b d) Source #

Unital w arr => Unital (w :: Type -> Type -> Type) (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

unitl :: SMC w arr (w (Unit w) a) a Source #

unitl' :: SMC w arr a (w (Unit w) a) Source #

unitr :: SMC w arr (w a (Unit w)) a Source #

unitr' :: SMC w arr a (w a (Unit w)) Source #

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

Defined in Circuit.Net

Methods

id :: Net w arr a a Source #

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

Category arr => Category (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

id :: SMC w arr a a Source #

(.) :: SMC w arr b c -> SMC w arr a b -> SMC 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

Defined in Circuit.Net

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 #

Tensor w arr' => Algebra (SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source # 
Instance details

Defined in Circuit.SMC

Associated Types

type Ctx (SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' 
Instance details

Defined in Circuit.SMC

type Ctx (SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = Tensor w arr'

Methods

alg :: Ctx (SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' => (forall x y. arr x y -> arr' x y) -> (forall x y. rec x y -> arr' x y) -> SigPar w arr rec a b -> arr' a b Source #

type 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 Source # 
Instance details

Defined in Circuit.Net

type 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 = ()
type 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' Source # 
Instance details

Defined in Circuit.Net

type 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' = FreeSMC w arr'
type 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 Source # 
Instance details

Defined in Circuit.Net

type 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 = Action w arr
type Ctx (SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source # 
Instance details

Defined in Circuit.SMC

type Ctx (SigPar w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = Tensor w arr'

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

Symmetric braiding over the wiring tensor w.

Constructors

SigSwap :: forall {k} {k1} (w :: Type -> Type -> Type) (arr :: k) (rec :: k1) a1 b1. SigSwap w arr rec (w a1 b1) (w b1 a1) 

Instances

Instances details
(Category arr, Channel t arr) => Channel (t :: Type -> Type -> Type) (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

assoc :: SMC w arr (t (t a b) c) (t a (t b c)) Source #

assoc' :: SMC w arr (t a (t b c)) (t (t a b) c) Source #

slide :: SMC w arr (t a (t b c)) (t b (t a c)) Source #

(Strength t arr, Action w arr) => Strength (t :: Type -> Type -> Type) (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

strength :: SMC w arr b c -> SMC w arr (t a b) (t a c) Source #

(Traced t arr, Action w arr) => Traced (t :: Type -> Type -> Type) (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

trace :: SMC w arr (t a b) (t a c) -> SMC w arr b c Source #

Action w arr => Action (w :: Type -> Type -> Type) (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

braid :: SMC w arr (w a b) (w b a) Source #

Tensor w arr => Tensor (w :: Type -> Type -> Type) (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

tensor :: SMC w arr a b -> SMC w arr c d -> SMC w arr (w a c) (w b d) Source #

Unital w arr => Unital (w :: Type -> Type -> Type) (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

unitl :: SMC w arr (w (Unit w) a) a Source #

unitl' :: SMC w arr a (w (Unit w) a) Source #

unitr :: SMC w arr (w a (Unit w)) a Source #

unitr' :: SMC w arr a (w a (Unit w)) Source #

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

Defined in Circuit.Net

Methods

id :: Net w arr a a Source #

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

Category arr => Category (SMC w arr :: Type -> Type -> Type) Source # 
Instance details

Defined in Circuit.SMC

Methods

id :: SMC w arr a a Source #

(.) :: SMC w arr b c -> SMC w arr a b -> SMC 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

Defined in Circuit.Net

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 #

Action w arr' => Algebra (SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source # 
Instance details

Defined in Circuit.SMC

Associated Types

type Ctx (SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' 
Instance details

Defined in Circuit.SMC

type Ctx (SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = Action w arr'

Methods

alg :: Ctx (SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' => (forall x y. arr x y -> arr' x y) -> (forall x y. rec x y -> arr' x y) -> SigSwap w arr rec a b -> arr' a b Source #

type 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 Source # 
Instance details

Defined in Circuit.Net

type 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 = ()
type 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' Source # 
Instance details

Defined in Circuit.Net

type 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' = FreeSMC w arr'
type 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 Source # 
Instance details

Defined in Circuit.Net

type 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 = Action w arr
type Ctx (SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source # 
Instance details

Defined in Circuit.SMC

type Ctx (SigSwap w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = Action w arr'