circuits
Safe HaskellNone
LanguageGHC2024

Circuit.Circ

Description

Loose bicategory of Body values with varying carriers.

A KSW loose 1-cell is a body arr (t ch a) (t ch b) with its carrier ch hidden. The 2-cells are carrier intertwiners: maps α : ch -> ch' that make the Mealy square commute. Body is the fibre at fixed carrier; Circ is the coproduct of those fibres, and Sq / Intertwiner move between them.

Carrier-tensoring composition

cascade composes two bodies whose carriers are tensored:

  f :: Body t ch  arr a b
  g :: Body t ch' arr b c
  cascade g f :: Circ t arr a c   -- carrier  t ch ch'

The composite is

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

using assoc, assoc', slide and strength. No braiding/Action is needed because slide already swaps the second carrier past the payload.

Law witnesses

The bicategory laws hold only up to invertible Sq witnesses: carriers ch ⊗ (ch' ⊗ ch'') and (ch ⊗ ch') ⊗ ch'' are different Haskell types, so on-the-nose associativity is impossible. The proof artifact is the intertwiner itself; the falsification artifact is observational, via the pointed specialisation cascadeSome and runSomeBody.

Synopsis
  • data Circ (t :: k -> k1 -> k2) (arr :: k2 -> k2 -> Type) (a :: k1) (b :: k1) where
    • Circ :: forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k) (arr :: k2 -> k2 -> Type) (a :: k1) (b :: k1). Body t ch arr a b -> Circ t arr a b
  • idCirc :: forall {k2} (t :: k2 -> k2 -> k2) (arr :: k2 -> k2 -> Type) (a :: k2). Strength t arr => Circ t arr a a
  • data Sq (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> Type) (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1) = Sq {}
  • idSq :: forall {k2} {k1} (arr :: k2 -> k2 -> Type) (t :: k2 -> k1 -> k2) (ch :: k2) (a :: k1) (b :: k1). Category arr => Body t ch arr a b -> Sq t arr ch ch a b
  • vcomp :: forall {k2} {k1} (arr :: k2 -> k2 -> Type) (t :: k2 -> k1 -> k2) (ch' :: k2) (ch'' :: k2) (a :: k1) (b :: k1) (ch :: k2). Category arr => Sq t arr ch' ch'' a b -> Sq t arr ch ch' a b -> Sq t arr ch ch'' a b
  • data Intertwiner (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> Type) (a :: k1) (b :: k1) where
    • Intertwiner :: forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> Type) (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1). Sq t arr ch ch' a b -> Intertwiner t arr a b
  • withIntertwiner :: forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> Type) (a :: k1) (b :: k1) r. Intertwiner t arr a b -> (forall (ch :: k2) (ch' :: k2). Sq t arr ch ch' a b -> r) -> r
  • downThenAcross :: forall {k1} (t :: k1 -> k1 -> k1) arr (ch :: k1) (ch' :: k1) (a :: k1) (b :: k1). Tensor t arr => Sq t arr ch ch' a b -> arr (t ch a) (t ch' b)
  • acrossThenDown :: forall {k1} (t :: k1 -> k1 -> k1) arr (ch :: k1) (ch' :: k1) (a :: k1) (b :: k1). Tensor t arr => Sq t arr ch ch' a b -> arr (t ch a) (t ch' b)
  • cascade :: forall {k2} (t :: k2 -> k2 -> k2) (arr :: k2 -> k2 -> Type) (b :: k2) (c :: k2) (a :: k2). Strength t arr => Circ t arr b c -> Circ t arr a b -> Circ t arr a c
  • unitorLeft :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (ch :: k1) (a :: k1) (b :: k1). (Unital t arr, Strength t arr) => Body t ch arr a b -> Intertwiner t arr a b
  • unitorRight :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (ch :: k1) (a :: k1) (b :: k1). (Unital t arr, Strength t arr) => Body t ch arr a b -> Intertwiner t arr a b
  • unitorLeftSq :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> Type) (ch :: k) (a :: k) (b :: k). (Unital t arr, Strength t arr) => Body t ch arr a b -> Sq t arr (t (Unit t) ch) ch a b
  • unitorRightSq :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> Type) (ch :: k) (a :: k) (b :: k). (Unital t arr, Strength t arr) => Body t ch arr a b -> Sq t arr (t ch (Unit t)) ch a b
  • associator :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (ch3 :: k1) (c :: k1) (d :: k1) (ch2 :: k1) (b :: k1) (ch1 :: k1) (a :: k1). Strength t arr => Body t ch3 arr c d -> Body t ch2 arr b c -> Body t ch1 arr a b -> Intertwiner t arr a d
  • associatorSq :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (ch3 :: k1) (c :: k1) (d :: k1) (ch2 :: k1) (b :: k1) (ch1 :: k1) (a :: k1). Strength t arr => Body t ch3 arr c d -> Body t ch2 arr b c -> Body t ch1 arr a b -> Sq t arr (t (t ch1 ch2) ch3) (t ch1 (t ch2 ch3)) a d
  • feedback :: forall {k2} (t :: k2 -> k2 -> k2) (arr :: k2 -> k2 -> Type) (s :: k2) (a :: k2) (b :: k2). Channel t arr => Circ t arr (t s a) (t s b) -> Circ t arr a b
  • elgotBody :: (a -> Either a b) -> Body Either Void (->) (Either a a) (Either a b)
  • elgotDagger :: (a -> Either a b) -> Circ Either (->) a b
  • elgotFeedbackBody :: (a -> Either a b) -> Body Either (Either Void a) (->) a b
  • bisimilarStates :: (Eq s1, Eq s2, Eq b) => [a] -> [s1] -> [s2] -> Body (,) s1 (->) a b -> Body (,) s2 (->) a b -> s1 -> s2 -> Bool
  • isBisimulation :: (Eq s1, Eq s2, Eq b) => [a] -> Body (,) s1 (->) a b -> Body (,) s2 (->) a b -> [(s1, s2)] -> Bool
  • maxBisimulation :: (Eq s1, Eq s2, Eq b) => [a] -> [s1] -> [s2] -> Body (,) s1 (->) a b -> Body (,) s2 (->) a b -> [(s1, s2)]
  • rightWhisker :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (ch :: k1) (ch' :: k1) (a :: k1) (b :: k1) (d :: k1) (c :: k1). (Tensor t arr, Strength t arr) => Sq t arr ch ch' a b -> Body t d arr b c -> Sq t arr (t ch d) (t ch' d) a c
  • leftWhisker :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (d :: k1) (a' :: k1) (a :: k1) (ch :: k1) (ch' :: k1) (b :: k1). (Tensor t arr, Strength t arr) => Body t d arr a' a -> Sq t arr ch ch' a b -> Sq t arr (t d ch) (t d ch') a' b
  • hcompose :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (ch2 :: k1) (ch2' :: k1) (b :: k1) (c :: k1) (ch1 :: k1) (ch1' :: k1) (a :: k1). (Tensor t arr, Strength t arr) => Sq t arr ch2 ch2' b c -> Sq t arr ch1 ch1' a b -> Sq t arr (t ch1 ch2) (t ch1' ch2') a c
  • whiskerSq :: forall {k1} (t :: k1 -> k1 -> k1) arr (a' :: k1) (a :: k1) (b :: k1) (b' :: k1) (ch :: k1) (ch' :: k1). Tensor t arr => arr a' a -> arr b b' -> Sq t arr ch ch' a b -> Sq t arr ch ch' a' b'

Loose 1-cell (carrier hidden)

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

Loose 1-cell: a body with its carrier type hidden.

Constructors

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

Instances

Instances details
Strength t arr => Category (Circ t arr :: k -> k -> Type) Source #

Category instance for Circ.

The laws hold only up to invertible Sq: on-the-nose associativity and unitality are impossible as Haskell values because the carriers of the two sides differ. Observational witnesses live in Axioma.Circ.

Instance details

Defined in Circuit.Circ

Methods

id :: forall (a :: k). Circ t arr a a Source #

(.) :: forall (b :: k) (c :: k) (a :: k). Circ t arr b c -> Circ t arr a b -> Circ t arr a c Source #

idCirc :: forall {k2} (t :: k2 -> k2 -> k2) (arr :: k2 -> k2 -> Type) (a :: k2). Strength t arr => Circ t arr a a Source #

Identity loose 1-cell at the tensor unit carrier.

The carrier is pinned to Unit so that the unit law can be witnessed with the unitor; without the annotation GHC would instantiate the hidden carrier to Any.

Indexed 2-cell (carrier map + commuting square)

data Sq (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> Type) (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1) Source #

Square (indexed 2-cell). The carrier maps compose; the middle body must match (a caller side condition).

Constructors

Sq 

Fields

  • carrierMap :: arr ch ch'

    Map between carriers.

  • sqSrc :: Body t ch arr a b

    Source body, over the source carrier.

  • sqTgt :: Body t ch' arr a b

    Target body, over the target carrier.

idSq :: forall {k2} {k1} (arr :: k2 -> k2 -> Type) (t :: k2 -> k1 -> k2) (ch :: k2) (a :: k1) (b :: k1). Category arr => Body t ch arr a b -> Sq t arr ch ch a b Source #

Identity square on a body.

vcomp :: forall {k2} {k1} (arr :: k2 -> k2 -> Type) (t :: k2 -> k1 -> k2) (ch' :: k2) (ch'' :: k2) (a :: k1) (b :: k1) (ch :: k2). Category arr => Sq t arr ch' ch'' a b -> Sq t arr ch ch' a b -> Sq t arr ch ch'' a b Source #

Vertical composition of squares.

The middle body must match; this is a caller side condition.

Existential closure of Sq

data Intertwiner (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> Type) (a :: k1) (b :: k1) where Source #

Existential closure of Sq, for stating "there exists a 2-cell".

Constructors

Intertwiner :: forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> Type) (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1). Sq t arr ch ch' a b -> Intertwiner t arr a b 

withIntertwiner :: forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> Type) (a :: k1) (b :: k1) r. Intertwiner t arr a b -> (forall (ch :: k2) (ch' :: k2). Sq t arr ch ch' a b -> r) -> r Source #

Eliminator for the existential carrier types of an Intertwiner.

The two paths whose equality is the square

downThenAcross :: forall {k1} (t :: k1 -> k1 -> k1) arr (ch :: k1) (ch' :: k1) (a :: k1) (b :: k1). Tensor t arr => Sq t arr ch ch' a b -> arr (t ch a) (t ch' b) Source #

Go down (carrier map) then across (target body).

A nondegenerate intertwiner witness: counter state quotiented by parity. The payload is Char so the carrier slot and payload slot are type-distinct; slot confusion is a type error. These examples exercise both parities and both reset branches. A paired perturbation doctest on acrossThenDown shows the equality can fail, so these agreement cases are not vacuous.

>>> let counter = (Body $ \(n, r) -> let n' = if r then 0 else n + 1 in (n', if odd n' then 'x' else 'y')) :: Body (,) Int (->) Bool Char
>>> let parity = (Body $ \(b, r) -> let b' = not r && not b in (b', if b' then 'x' else 'y')) :: Body (,) Bool (->) Bool Char
>>> let sq = Sq odd counter parity :: Sq (,) (->) Int Bool Bool Char
>>> downThenAcross sq (4, False)
(True,'x')
>>> downThenAcross sq (4, True)
(False,'y')
>>> downThenAcross sq (5, False)
(False,'y')

acrossThenDown :: forall {k1} (t :: k1 -> k1 -> k1) arr (ch :: k1) (ch' :: k1) (a :: k1) (b :: k1). Tensor t arr => Sq t arr ch ch' a b -> arr (t ch a) (t ch' b) Source #

Go across (source body) then down (carrier map).

Agreement cases for the same witness:

>>> let counter = (Body $ \(n, r) -> let n' = if r then 0 else n + 1 in (n', if odd n' then 'x' else 'y')) :: Body (,) Int (->) Bool Char
>>> let parity = (Body $ \(b, r) -> let b' = not r && not b in (b', if b' then 'x' else 'y')) :: Body (,) Bool (->) Bool Char
>>> let sq = Sq odd counter parity :: Sq (,) (->) Int Bool Bool Char
>>> acrossThenDown sq (4, False)
(True,'x')
>>> acrossThenDown sq (4, True)
(False,'y')
>>> acrossThenDown sq (5, False)
(False,'y')

Perturbation: observe even-ness instead of odd-ness. The two paths now disagree, which proves the agreement cases above are not vacuous.

>>> let badCounter = (Body $ \(n, r) -> let n' = if r then 0 else n + 1 in (n', if even n' then 'x' else 'y')) :: Body (,) Int (->) Bool Char
>>> let bad = Sq odd badCounter parity :: Sq (,) (->) Int Bool Bool Char
>>> downThenAcross bad (4, False)
(True,'x')
>>> acrossThenDown bad (4, False)
(True,'y')

Carrier-tensoring composition

cascade :: forall {k2} (t :: k2 -> k2 -> k2) (arr :: k2 -> k2 -> Type) (b :: k2) (c :: k2) (a :: k2). Strength t arr => Circ t arr b c -> Circ t arr a b -> Circ t arr a c Source #

Carrier-tensoring composition of loose 1-cells.

The composite has carrier t ch ch' when the first body has carrier ch and the second has carrier ch'.

Structural proof witnesses (unitors and associator)

unitorLeft :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (ch :: k1) (a :: k1) (b :: k1). (Unital t arr, Strength t arr) => Body t ch arr a b -> Intertwiner t arr a b Source #

Left unitor witness: composing a body with the identity at the unit carrier is isomorphic to the original body.

unitorRight :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (ch :: k1) (a :: k1) (b :: k1). (Unital t arr, Strength t arr) => Body t ch arr a b -> Intertwiner t arr a b Source #

Right unitor witness.

unitorLeftSq :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> Type) (ch :: k) (a :: k) (b :: k). (Unital t arr, Strength t arr) => Body t ch arr a b -> Sq t arr (t (Unit t) ch) ch a b Source #

Indexed left unitor square.

unitorRightSq :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> Type) (ch :: k) (a :: k) (b :: k). (Unital t arr, Strength t arr) => Body t ch arr a b -> Sq t arr (t ch (Unit t)) ch a b Source #

Indexed right unitor square.

associator :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (ch3 :: k1) (c :: k1) (d :: k1) (ch2 :: k1) (b :: k1) (ch1 :: k1) (a :: k1). Strength t arr => Body t ch3 arr c d -> Body t ch2 arr b c -> Body t ch1 arr a b -> Intertwiner t arr a d Source #

Associator witness: carrier bracketing of three composed bodies is isomorphic up to the associator of the tensor.

associatorSq :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (ch3 :: k1) (c :: k1) (d :: k1) (ch2 :: k1) (b :: k1) (ch1 :: k1) (a :: k1). Strength t arr => Body t ch3 arr c d -> Body t ch2 arr b c -> Body t ch1 arr a b -> Sq t arr (t (t ch1 ch2) ch3) (t ch1 (t ch2 ch3)) a d Source #

Indexed associator square.

Feedback (closed loop over a carrier component)

feedback :: forall {k2} (t :: k2 -> k2 -> k2) (arr :: k2 -> k2 -> Type) (s :: k2) (a :: k2) (b :: k2). Channel t arr => Circ t arr (t s a) (t s b) -> Circ t arr a b Source #

Close a feedback loop over a component s of the input/output object.

The 1-cell must be of the form Circ t arr (t s a) (t s b): the feedback value s appears as the first component of the tensor in both domain and codomain. The result moves s into the hidden carrier, turning it into state. This is the guarded / state-bootstrapping feedback of KSW, not the immediate fixed-point trace: yanking fails here, which is the expected behaviour for a feedback category.

Implemented by reassociating so that s becomes part of the carrier:

  feedback (Circ (Body f)) = Circ (Body (assoc .> f .> assoc'))

Elgot dagger (feedback over Either as iteration)

elgotBody :: (a -> Either a b) -> Body Either Void (->) (Either a a) (Either a b) Source #

Build the Elgot coalgebra [Left, f] from a loop body f :: a -> Either a b.

The resulting body has the Void unit carrier and payload Either a a -> Either a b, so it can be passed to feedback. The dagger of f is then a morphism a -> b in Circ.

elgotDagger :: (a -> Either a b) -> Circ Either (->) a b Source #

Elgot dagger of f :: a -> Either a b via feedback.

elgotFeedbackBody :: (a -> Either a b) -> Body Either (Either Void a) (->) a b Source #

The feedback body of the Elgot dagger of f :: a -> Either a b.

Exposed so that callers can run it directly with a seed of type Either Void a, which is the hidden carrier produced by feedback.

Bisimulation (behavioural quotient of bodies)

bisimilarStates :: (Eq s1, Eq s2, Eq b) => [a] -> [s1] -> [s2] -> Body (,) s1 (->) a b -> Body (,) s2 (->) a b -> s1 -> s2 -> Bool Source #

Check whether two specific states are bisimilar.

isBisimulation :: (Eq s1, Eq s2, Eq b) => [a] -> Body (,) s1 (->) a b -> Body (,) s2 (->) a b -> [(s1, s2)] -> Bool Source #

Check whether a relation is a bisimulation between two finite-state bodies.

The relation must be over the provided state spaces; the check is exact over the bounded input alphabet. A relation R is a bisimulation when for every (s1, s2) ∈ R and every input a, the outputs coincide and the successor states are again R-related.

maxBisimulation :: (Eq s1, Eq s2, Eq b) => [a] -> [s1] -> [s2] -> Body (,) s1 (->) a b -> Body (,) s2 (->) a b -> [(s1, s2)] Source #

Compute the maximal bisimulation between two finite-state bodies over a bounded input alphabet. The state spaces are supplied explicitly because a Body is a function and does not enumerate its own states.

Horizontal 2-cell algebra

rightWhisker :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (ch :: k1) (ch' :: k1) (a :: k1) (b :: k1) (d :: k1) (c :: k1). (Tensor t arr, Strength t arr) => Sq t arr ch ch' a b -> Body t d arr b c -> Sq t arr (t ch d) (t ch' d) a c Source #

Right whisker: tensor a square with an identity-on-boundaries 1-cell on the right.

leftWhisker :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (d :: k1) (a' :: k1) (a :: k1) (ch :: k1) (ch' :: k1) (b :: k1). (Tensor t arr, Strength t arr) => Body t d arr a' a -> Sq t arr ch ch' a b -> Sq t arr (t d ch) (t d ch') a' b Source #

Left whisker: tensor an identity-on-boundaries 1-cell on the left of a square.

hcompose :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> Type) (ch2 :: k1) (ch2' :: k1) (b :: k1) (c :: k1) (ch1 :: k1) (ch1' :: k1) (a :: k1). (Tensor t arr, Strength t arr) => Sq t arr ch2 ch2' b c -> Sq t arr ch1 ch1' a b -> Sq t arr (t ch1 ch2) (t ch1' ch2') a c Source #

Horizontal composition of two squares.

whiskerSq :: forall {k1} (t :: k1 -> k1 -> k1) arr (a' :: k1) (a :: k1) (b :: k1) (b' :: k1) (ch :: k1) (ch' :: k1). Tensor t arr => arr a' a -> arr b b' -> Sq t arr ch ch' a b -> Sq t arr ch ch' a' b' Source #

Boundary whisker: apply tight maps to the input and output boundaries of a square. This is the Sq side of the interchange law; the Poles side is iomap on the Moore-split representation.