Safe Haskell	None
Language	GHC2024

Circuit.Syntax

Contents

Signatures
Syntax and algebra
Sequential composition
Free category

Description

The generic substrate for modular circuit syntax.

This module holds the à-la-carte machinery: signatures, the free construction over a signature, algebras, and the universal folds. Each concrete language layer (Trace, SMC, Net, ...) is obtained by choosing a signature sum and adding smart constructors and structural instances on top of this substrate.

The design is a profunctor-shaped variation of the classic "datatypes à la carte":

A Sig is a signature functor indexed by a base arrow arr and a recursive arrow rec.
Syntax sig arr is the free construction over sig with generators drawn from arr.
An Algebra interprets the operations of a signature into a target arrow.
evalInto is the universal fold out of the free construction; eval is the same fold back into the base arrow.

Synopsis

type Sig = (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type
data ((sig1 :: k -> k1 -> k2 -> k3 -> Type) :+: (sig2 :: k -> k1 -> k2 -> k3 -> Type)) (arr :: k) (rec :: k1) (a :: k2) (b :: k3) where
- L :: forall {k} {k1} {k2} {k3} (sig1 :: k -> k1 -> k2 -> k3 -> Type) (arr :: k) (rec :: k1) (a :: k2) (b :: k3) (sig2 :: k -> k1 -> k2 -> k3 -> Type). sig1 arr rec a b -> (sig1 :+: sig2) arr rec a b
- R :: forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> Type) (arr :: k) (rec :: k1) (a :: k2) (b :: k3) (sig1 :: k -> k1 -> k2 -> k3 -> Type). sig2 arr rec a b -> (sig1 :+: sig2) arr rec a b
data Syntax (sig :: Sig) (arr :: Type -> Type -> Type) a b where
- Lift :: forall (arr :: Type -> Type -> Type) a b (sig :: Sig). arr a b -> Syntax sig arr a b
- Op :: forall (sig :: Sig) (arr :: Type -> Type -> Type) a b. sig arr (Syntax sig arr) a b -> Syntax sig arr a b
class Algebra (sig :: Sig) (arr :: Type -> Type -> Type) (arr' :: Type -> Type -> Type) where
- type Ctx (sig :: Sig) (arr :: Type -> Type -> Type) (arr' :: Type -> Type -> Type)
- alg :: Ctx sig arr arr' => (forall x y. arr x y -> arr' x y) -> (forall x y. rec x y -> arr' x y) -> sig arr rec a b -> arr' a b
eval :: forall arr (sig :: Sig) a b. (Category arr, Algebra sig arr arr, Ctx sig arr arr) => Syntax sig arr a b -> arr a b
evalInto :: forall arr' (sig :: Sig) arr a b. (Category arr', Algebra sig arr arr', Ctx sig arr arr') => (forall x y. arr x y -> arr' x y) -> Syntax sig arr a b -> arr' a b
data SigCompose (arr :: k) (rec :: k1 -> k1 -> Type) (a :: k1) (b :: k1) where
- SigCompose :: forall {k1} {k} (rec :: k1 -> k1 -> Type) (b1 :: k1) (b :: k1) (a :: k1) (arr :: k). rec b1 b -> rec a b1 -> SigCompose arr rec a b
type AlgCat (arr :: Type -> Type -> Type) = Syntax (SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr

Signatures

type Sig = (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type Source #

A signature describes a set of constructors for a profunctor.

arr — the base arrow (used for constructor constraints)
rec — the recursive arrow type being defined
a, b — input and output objects

data ((sig1 :: k -> k1 -> k2 -> k3 -> Type) :+: (sig2 :: k -> k1 -> k2 -> k3 -> Type)) (arr :: k) (rec :: k1) (a :: k2) (b :: k3) where infixr 6 Source #

Coproduct of signatures.

Constructors

L :: forall {k} {k1} {k2} {k3} (sig1 :: k -> k1 -> k2 -> k3 -> Type) (arr :: k) (rec :: k1) (a :: k2) (b :: k3) (sig2 :: k -> k1 -> k2 -> k3 -> Type). sig1 arr rec a b -> (sig1 :+: sig2) arr rec a b
R :: forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> Type) (arr :: k) (rec :: k1) (a :: k2) (b :: k3) (sig1 :: k -> k1 -> k2 -> k3 -> Type). sig2 arr rec a b -> (sig1 :+: sig2) arr rec a b

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 #

(Category arr, Channel t arr) => Channel (t :: Type -> Type -> Type) (Trace t arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Trace

Methods

assoc :: Trace t arr (t (t a b) c) (t a (t b c)) Source #

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

slide :: Trace t 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 #

(Strength t arr, Traced t arr) => Strength (t :: Type -> Type -> Type) (Trace t arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Trace

Methods

strength :: Trace t arr b c -> Trace t 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 #

Traced t arr => Traced (t :: Type -> Type -> Type) (Trace t arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Trace

Methods

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

(Action t arr, Traced t' arr) => Action (t :: Type -> Type -> Type) (Trace t' arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Tensor

Methods

braid :: Trace t' arr (t a b) (t b a) 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 t arr, Traced t' arr) => Tensor (t :: Type -> Type -> Type) (Trace t' arr :: Type -> Type -> Type) Source #

Lift Tensor/Action through Trace.

This is the single lawful instance: it evaluates each Trace branch independently with eval and combines the results using the base arrow's tensor. It is correct and black-hole-free, but does not fuse feedback loops. For the fused superposition of two yanks, use superpose.

Instance details

Defined in Circuit.Tensor

Methods

tensor :: Trace t' arr a b -> Trace t' arr c d -> Trace t' arr (t a c) (t b d) 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 t arr => Unital (t :: Type -> Type -> Type) (Trace t' arr :: Type -> Type -> Type) Source #

Lift Unital through Trace.

Instance details

Defined in Circuit.Tensor

Methods

unitl :: Trace t' arr (t (Unit t) a) a Source #

unitl' :: Trace t' arr a (t (Unit t) a) Source #

unitr :: Trace t' arr (t a (Unit t)) a Source #

unitr' :: Trace t' arr a (t a (Unit t)) 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 #

Category arr => Category (Trace t arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Trace

Methods

id :: Trace t arr a a Source #

(.) :: Trace t arr b c -> Trace t arr a b -> Trace t arr a c 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 #

(Algebra sig1 arr arr', Algebra sig2 arr arr') => Algebra (sig1 :+: sig2) arr arr' Source #

Coproduct algebra dispatches to the appropriate component.

Instance details

Defined in Circuit.Syntax

Associated Types

type Ctx (sig1 :+: sig2) arr arr'
Instance details Defined in Circuit.Syntax type Ctx (sig1 :+: sig2) arr arr' = (Ctx sig1 arr arr', Ctx sig2 arr arr')

Methods

alg :: Ctx (sig1 :+: sig2) arr arr' => (forall x y. arr x y -> arr' x y) -> (forall x y. rec x y -> arr' x y) -> (sig1 :+: sig2) 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 (sig1 :+: sig2) arr arr' Source #

Instance details

Defined in Circuit.Syntax

type Ctx (sig1 :+: sig2) arr arr' = (Ctx sig1 arr arr', Ctx sig2 arr arr')

Syntax and algebra

data Syntax (sig :: Sig) (arr :: Type -> Type -> Type) a b where Source #

The free construction over a signature.

Constructors

Lift :: forall (arr :: Type -> Type -> Type) a b (sig :: Sig). arr a b -> Syntax sig arr a b
Op :: forall (sig :: Sig) (arr :: Type -> Type -> Type) a b. sig arr (Syntax sig arr) a b -> Syntax sig arr a b

Instances

Instances details

(Category arr, Channel t arr) => Channel (t :: Type -> Type -> Type) (AlgCat arr :: Type -> Type -> Type) Source #
Instance details Defined in Circuit.Syntax Methods assoc :: AlgCat arr (t (t a b) c) (t a (t b c)) Source # assoc' :: AlgCat arr (t a (t b c)) (t (t a b) c) Source # slide :: AlgCat arr (t a (t b c)) (t b (t a c)) Source #
(Category arr, Strength t arr) => Strength (t :: Type -> Type -> Type) (AlgCat arr :: Type -> Type -> Type) Source #
Instance details Defined in Circuit.Syntax Methods strength :: AlgCat arr b c -> AlgCat arr (t a b) (t a c) Source #
(Category arr, Traced t arr) => Traced (t :: Type -> Type -> Type) (AlgCat arr :: Type -> Type -> Type) Source #
Instance details Defined in Circuit.Syntax Methods trace :: AlgCat arr (t a b) (t a c) -> AlgCat arr b c Source #
(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 #
(Category arr, Channel t arr) => Channel (t :: Type -> Type -> Type) (Trace t arr :: Type -> Type -> Type) Source #
Instance details Defined in Circuit.Trace Methods assoc :: Trace t arr (t (t a b) c) (t a (t b c)) Source # assoc' :: Trace t arr (t a (t b c)) (t (t a b) c) Source # slide :: Trace t 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 #
(Strength t arr, Traced t arr) => Strength (t :: Type -> Type -> Type) (Trace t arr :: Type -> Type -> Type) Source #
Instance details Defined in Circuit.Trace Methods strength :: Trace t arr b c -> Trace t 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 #
Traced t arr => Traced (t :: Type -> Type -> Type) (Trace t arr :: Type -> Type -> Type) Source #
Instance details Defined in Circuit.Trace Methods trace :: Trace t arr (t a b) (t a c) -> Trace t arr b c Source #
(Action t arr, Traced t' arr) => Action (t :: Type -> Type -> Type) (Trace t' arr :: Type -> Type -> Type) Source #
Instance details Defined in Circuit.Tensor Methods braid :: Trace t' arr (t a b) (t b a) 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 t arr, Traced t' arr) => Tensor (t :: Type -> Type -> Type) (Trace t' arr :: Type -> Type -> Type) Source #	Lift `Tensor`/`Action` through `Trace`. This is the single lawful instance: it evaluates each `Trace` branch independently with `eval` and combines the results using the base arrow's tensor. It is correct and black-hole-free, but does not fuse feedback loops. For the fused superposition of two `yank`s, use `superpose`.
Instance details Defined in Circuit.Tensor Methods tensor :: Trace t' arr a b -> Trace t' arr c d -> Trace t' arr (t a c) (t b d) 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 t arr => Unital (t :: Type -> Type -> Type) (Trace t' arr :: Type -> Type -> Type) Source #	Lift `Unital` through `Trace`.
Instance details Defined in Circuit.Tensor Methods unitl :: Trace t' arr (t (Unit t) a) a Source # unitl' :: Trace t' arr a (t (Unit t) a) Source # unitr :: Trace t' arr (t a (Unit t)) a Source # unitr' :: Trace t' arr a (t a (Unit t)) 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 (AlgCat arr :: Type -> Type -> Type) Source #
Instance details Defined in Circuit.Syntax Methods id :: AlgCat arr a a Source # (.) :: AlgCat arr b c -> AlgCat arr a b -> AlgCat arr a c 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 #
Category arr => Category (Trace t arr :: Type -> Type -> Type) Source #
Instance details Defined in Circuit.Trace Methods id :: Trace t arr a a Source # (.) :: Trace t arr b c -> Trace t arr a b -> Trace t 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 #
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

class Algebra (sig :: Sig) (arr :: Type -> Type -> Type) (arr' :: Type -> Type -> Type) where Source #

Algebra for a signature. Interprets operations of a signature over source arrow arr into a target arrow arr'.

emb maps base arrows of the source into the target.
rec maps recursive sub-terms into the target.

Associated Types

type Ctx (sig :: Sig) (arr :: Type -> Type -> Type) (arr' :: Type -> Type -> Type) Source #

type Ctx (sig :: Sig) (arr :: Type -> Type -> Type) (arr' :: Type -> Type -> Type) = ()

Methods

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

Instances

Instances details

Algebra (SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source #

Instance details

Defined in Circuit.Bimonoid

Associated Types

type Ctx (SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr'
Instance details Defined in Circuit.Bimonoid type Ctx (SigCopy w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = ()

Methods

alg :: Ctx (SigCopy 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) -> SigCopy w arr rec a b -> arr' a b Source #

Algebra (SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source #

Instance details

Defined in Circuit.Bimonoid

Associated Types

type Ctx (SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr'
Instance details Defined in Circuit.Bimonoid type Ctx (SigDiscard w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = ()

Methods

alg :: Ctx (SigDiscard 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) -> SigDiscard w arr rec a b -> arr' a b Source #

Algebra (SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source #

Instance details

Defined in Circuit.Bimonoid

Associated Types

type Ctx (SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr'
Instance details Defined in Circuit.Bimonoid type Ctx (SigPlus w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = ()

Methods

alg :: Ctx (SigPlus 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) -> SigPlus w arr rec a b -> arr' a b Source #

Algebra (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source #

Instance details

Defined in Circuit.Bimonoid

Associated Types

type Ctx (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr'
Instance details Defined in Circuit.Bimonoid type Ctx (SigZero w :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = ()

Methods

alg :: Ctx (SigZero 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) -> SigZero w arr rec 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 #

Shared t arr' => Algebra (SigShared t :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source #

Instance details

Defined in Circuit.Shared

Associated Types

type Ctx (SigShared t :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr'
Instance details Defined in Circuit.Shared type Ctx (SigShared t :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = Shared t arr'

Methods

alg :: Ctx (SigShared t :: (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) -> SigShared t arr rec a b -> arr' a b Source #

Algebra (SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source #

Instance details

Defined in Circuit.Syntax

Associated Types

type Ctx (SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr'
Instance details Defined in Circuit.Syntax type Ctx (SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = Category arr'

Methods

alg :: Ctx (SigCompose :: (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) -> SigCompose arr rec a b -> arr' a b Source #

Traced t arr' => Algebra (SigYank t :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source #

Instance details

Defined in Circuit.Trace

Associated Types

type Ctx (SigYank t :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr'
Instance details Defined in Circuit.Trace type Ctx (SigYank t :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = Traced t arr'

Methods

alg :: Ctx (SigYank t :: (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) -> SigYank t arr rec 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 #

(Algebra sig1 arr arr', Algebra sig2 arr arr') => Algebra (sig1 :+: sig2) arr arr' Source #

Coproduct algebra dispatches to the appropriate component.

Instance details

Defined in Circuit.Syntax

Associated Types

type Ctx (sig1 :+: sig2) arr arr'
Instance details Defined in Circuit.Syntax type Ctx (sig1 :+: sig2) arr arr' = (Ctx sig1 arr arr', Ctx sig2 arr arr')

Methods

alg :: Ctx (sig1 :+: sig2) arr arr' => (forall x y. arr x y -> arr' x y) -> (forall x y. rec x y -> arr' x y) -> (sig1 :+: sig2) arr rec a b -> arr' a b Source #

eval :: forall arr (sig :: Sig) a b. (Category arr, Algebra sig arr arr, Ctx sig arr arr) => Syntax sig arr a b -> arr a b Source #

Fold a free construction into its own base arrow.

evalInto :: forall arr' (sig :: Sig) arr a b. (Category arr', Algebra sig arr arr', Ctx sig arr arr') => (forall x y. arr x y -> arr' x y) -> Syntax sig arr a b -> arr' a b Source #

Fold a free construction into a target arrow using its algebra.

The embedding emb maps base arrows of the source into the target. For folding to the same arrow, use eval.

Sequential composition

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

Sequential composition.

Constructors

SigCompose :: forall {k1} {k} (rec :: k1 -> k1 -> Type) (b1 :: k1) (b :: k1) (a :: k1) (arr :: k). rec b1 b -> rec a b1 -> SigCompose arr rec a b

Instances

Instances details

(Category arr, Channel t arr) => Channel (t :: Type -> Type -> Type) (AlgCat arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Syntax

Methods

assoc :: AlgCat arr (t (t a b) c) (t a (t b c)) Source #

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

slide :: AlgCat arr (t a (t b c)) (t b (t a c)) Source #

(Category arr, Strength t arr) => Strength (t :: Type -> Type -> Type) (AlgCat arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Syntax

Methods

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

(Category arr, Traced t arr) => Traced (t :: Type -> Type -> Type) (AlgCat arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Syntax

Methods

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

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

(Category arr, Channel t arr) => Channel (t :: Type -> Type -> Type) (Trace t arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Trace

Methods

assoc :: Trace t arr (t (t a b) c) (t a (t b c)) Source #

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

slide :: Trace t 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 #

(Strength t arr, Traced t arr) => Strength (t :: Type -> Type -> Type) (Trace t arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Trace

Methods

strength :: Trace t arr b c -> Trace t 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 #

Traced t arr => Traced (t :: Type -> Type -> Type) (Trace t arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Trace

Methods

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

(Action t arr, Traced t' arr) => Action (t :: Type -> Type -> Type) (Trace t' arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Tensor

Methods

braid :: Trace t' arr (t a b) (t b a) 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 t arr, Traced t' arr) => Tensor (t :: Type -> Type -> Type) (Trace t' arr :: Type -> Type -> Type) Source #

Lift Tensor/Action through Trace.

This is the single lawful instance: it evaluates each Trace branch independently with eval and combines the results using the base arrow's tensor. It is correct and black-hole-free, but does not fuse feedback loops. For the fused superposition of two yanks, use superpose.

Instance details

Defined in Circuit.Tensor

Methods

tensor :: Trace t' arr a b -> Trace t' arr c d -> Trace t' arr (t a c) (t b d) 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 t arr => Unital (t :: Type -> Type -> Type) (Trace t' arr :: Type -> Type -> Type) Source #

Lift Unital through Trace.

Instance details

Defined in Circuit.Tensor

Methods

unitl :: Trace t' arr (t (Unit t) a) a Source #

unitl' :: Trace t' arr a (t (Unit t) a) Source #

unitr :: Trace t' arr (t a (Unit t)) a Source #

unitr' :: Trace t' arr a (t a (Unit t)) 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 (AlgCat arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Syntax

Methods

id :: AlgCat arr a a Source #

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

Category arr => Category (Trace t arr :: Type -> Type -> Type) Source #

Instance details

Defined in Circuit.Trace

Methods

id :: Trace t arr a a Source #

(.) :: Trace t arr b c -> Trace t arr a b -> Trace t arr a c 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 #

Algebra (SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source #

Instance details

Defined in Circuit.Syntax

Associated Types

type Ctx (SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr'
Instance details Defined in Circuit.Syntax type Ctx (SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = Category arr'

Methods

alg :: Ctx (SigCompose :: (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) -> SigCompose 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 (SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source #

Instance details

Defined in Circuit.Syntax

type Ctx (SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = Category arr'

Free category

type AlgCat (arr :: Type -> Type -> Type) = Syntax (SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr Source #

Free category.