Safe Haskell	None
Language	GHC2024

Circuit.Trace

Contents

Free traced category
Trace signature

Description

Free traced monoidal category syntax.

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

SigCompose :+: SigYank t

where SigCompose provides sequential composition and SigYank provides feedback / trace over the channel tensor t.

Higher-level signatures (parallel composition, braid, copy/discard, shared-medium fusion, mediators) live in Circuit.SMC, Circuit.Bimonoid, and Circuit.Shared.

Synopsis

type Trace (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigYank t :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)) arr
base :: forall arr a b (t :: Type -> Type -> Type). arr a b -> Trace t arr a b
yank :: forall t (arr :: Type -> Type -> Type) s a b. Trace t arr (t s a) (t s b) -> Trace t arr a b
data SigYank (t :: Type -> Type -> Type) (arr :: k) (rec :: Type -> Type -> Type) a b where
- Yank :: forall {k} (rec :: Type -> Type -> Type) (t :: Type -> Type -> Type) s a b (arr :: k). rec (t s a) (t s b) -> SigYank t arr rec a b

Free traced category

type Trace (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = Syntax ((SigCompose :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) :+: (SigYank t :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type)) arr Source #

Free traced monoidal category over tensor t.

base :: forall arr a b (t :: Type -> Type -> Type). arr a b -> Trace t arr a b Source #

Lift a base arrow into the free traced category.

yank :: forall t (arr :: Type -> Type -> Type) s a b. Trace t arr (t s a) (t s b) -> Trace t arr a b Source #

Close a feedback loop over the channel tensor t.

Trace signature

data SigYank (t :: Type -> Type -> Type) (arr :: k) (rec :: Type -> Type -> Type) a b where Source #

Feedback loop / trace over tensor t.

Constructors

Yank :: forall {k} (rec :: Type -> Type -> Type) (t :: Type -> Type -> Type) s a b (arr :: k). rec (t s a) (t s b) -> SigYank t arr rec a b

Instances

Instances details

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

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

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 #

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 #

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 #

type Ctx (SigYank t :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' Source #

Instance details

Defined in Circuit.Trace

type Ctx (SigYank t :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type) arr arr' = Traced t arr'