circuits
Safe HaskellNone
LanguageGHC2024

Circuit.Body

Description

A span-shaped Mealy machine: a morphism across a tensored channel.

  Body t ch arr a b  =  arr (t ch a) (t ch b)

Both the channel and the payload enter together, and both exit together. System specializes this shape to a Moore machine over a polynomial interface; Process is the pointed monomial special case of that.

Anatomy

  • t — tensor: the bifunctor that pairs a channel with a payload. Common choices are (,) for simultaneous sharing, Either for sequential iteration, and These for scheduled interleaving.
  • ch — channel: the value threaded alongside the payload. It may be state, residual, a stream, or a feedback wire.
  • arr — arrow / morphism: the base category. Usually (->) or a Kleisli arrow K m.

This arrangement is the common shape underlying loops, processes, systems, and channel ends: a morphism whose input and output both carry an ambient channel. Body makes that shape explicit before any tracing, scheduling, or pole-splitting is added.

Synopsis

Knot-body category

newtype Body (t :: k -> k1 -> k2) (ch :: k) (arr :: k2 -> k2 -> Type) (a :: k1) (b :: k1) Source #

A morphism across a tensored channel.

Body t ch arr a b is a morphism arr (t ch a) (t ch b). The channel ch is threaded alongside the payload by the tensor t; it may be state, residual, a stream, or any other value the base arrow arr carries along with the input and output. Composition threads the same channel through both morphisms.

Constructors

Body 

Fields

Instances

Instances details
(Monad m, Pointed s) => HasDual Void (Body Either s (K m) :: Type -> Type -> Type) Source #

Unit poles for Body Either s (K m) at Void.

Instance details

Defined in Circuit.Body

Methods

open :: Poles (Body Either s (K m)) Void Void Source #

Pointed s => HasDual Void (Body Either s (->) :: Type -> Type -> Type) Source #

Unit poles for Body Either s (->) at the unit object Void.

The coproduct case needs a distinguished element of the carrier s: on a Right x input the companion must return Left s for some s, and there is no ambient state to use. Pointed captures exactly that, which is weaker than Monoid. This is the structural pointedness requirement that makes Either differ from (,).

Instance details

Defined in Circuit.Body

Methods

open :: Poles (Body Either s (->)) Void Void Source #

Monad m => HasDual () (Body (,) s (K m) :: Type -> Type -> Type) Source #

Unit poles for Body (,) s (K m).

Same shape as the (->) instance, but the companion returns () in the monad and threads the ambient state through unchanged.

Instance details

Defined in Circuit.Body

Methods

open :: Poles (Body (,) s (K m)) () () Source #

HasDual () (Body (,) s (->) :: Type -> Type -> Type) Source #

Unit poles for Body (,) s (->) at the unit object ().

The companion discards its input and returns (); the conjoint delegates to the companion. Yanking recovers the identity on ().

Instance details

Defined in Circuit.Body

Methods

open :: Poles (Body (,) s (->)) () () Source #

Category arr => Category (Body t ch arr :: k3 -> k3 -> Type) Source # 
Instance details

Defined in Circuit.Body

Methods

id :: forall (a :: k3). Body t ch arr a a Source #

(.) :: forall (b :: k3) (c :: k3) (a :: k3). Body t ch arr b c -> Body t ch arr a b -> Body t ch arr a c Source #

data SomeBody (t :: Type -> k -> k1) (arr :: k1 -> k1 -> Type) (a :: k) (b :: k) where Source #

A Body with its channel type hidden.

Constructors

SomeBody :: forall {k} {k1} ch (t :: Type -> k -> k1) (arr :: k1 -> k1 -> Type) (a :: k) (b :: k). ch -> Body t ch arr a b -> SomeBody t arr a b 

Instances

Instances details
(Strength t arr, Pointed (Unit t), TensorSeed t) => Category (SomeBody t arr :: Type -> Type -> Type) Source #

Category instance for SomeBody.

The carrier of the composite is the tensor of the two carriers, and the stored seed is combined with seedPair. Identity needs a seed at the tensor unit, hence the 'Pointed (Unit t)' requirement. Tensors whose unit is uninhabited (e.g. Either with Unit Either = Void) therefore do not admit an identity; tensors without a canonical value-level pairing (also Either, These) do not admit composition.

Instance details

Defined in Circuit.Body

Methods

id :: SomeBody t arr a a Source #

(.) :: SomeBody t arr b c -> SomeBody t arr a b -> SomeBody t arr a c Source #

runSomeBody :: SomeBody (,) (->) a b -> [a] -> [b] Source #

Run an existentially-packed cartesian body over a list of inputs.

This is the (,) / list specialisation of SomeBody.

runFlowchart :: Body Either ch (->) a b -> Int -> a -> (Maybe b, Int) Source #

Run an Either body as a partial function a -> b with a fuel bound. Execution starts with the external input a; if the body emits a label ch the runner feeds Left ch back in, decrementing the fuel.

Returns the result (if any) and the number of steps taken. A flowchart has no stored state — the input is the entire initial configuration — so there is no seed parameter. This is the coproduct analogue of runSomeBody: where (,) bodies run as stream functions, Either bodies run as halting computations.

Carrier-tensoring composition

cascadeBody :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> Type) (ch' :: k) (b :: k) (c :: k) (ch :: k) (a :: k). Strength t arr => Body t ch' arr b c -> Body t ch arr a b -> Body t (t ch ch') arr a c Source #

Compose two bodies at carriers ch and ch' into a body at carrier t ch ch'. This is the body-level building block of horizontal 2-cell algebra and of the Category instance for SomeBody.

The composite is

  assoc .> slide .> strength f .> slide .> strength g .> assoc'

cascadeSome :: SomeBody (,) (->) b c -> SomeBody (,) (->) a b -> SomeBody (,) (->) a c Source #

Pointed carrier-tensoring composition for t = (,) and arr = (->).

Seeds pair under the tensor, and the composite can be run with runSomeBody. This is the pointed counterpart to the unpointed cascadeBody.