Safe Haskell	None
Language	GHC2024

Circuit.Dagger

Contents

Free dagger category

Description

The free dagger category over a base arrow.

A Dagger value pairs a forward arrow with a backward arrow. Composition is covariant forward and contravariant backward; transpose swaps the two directions.

The structural rules (Copy Discard Merge / Zero and their tensor-generic forms) live in Circuit.Bimonoid. This module only provides the free dagger construction and the way it dualises a bimonoid: forward copy corresponds to backward merge, forward discard to backward zero, and vice versa.

Synopsis

data Dagger (arr :: k -> k -> Type) (a :: k) (b :: k) = Dagger {
- front :: arr a b
- back :: arr b a
}
transpose :: forall {k} (arr :: k -> k -> Type) (a :: k) (b :: k). Dagger arr a b -> Dagger arr b a

Free dagger category

data Dagger (arr :: k -> k -> Type) (a :: k) (b :: k) Source #

The free dagger category over a base arrow.

Dagger arr a b is a pair of arrows arr a b (forward) and arr b a (backward). Composition is covariant forward, contravariant backward: Dagger f g . Dagger f' g' = Dagger (f . f') (g' . g).

>>> let d = Dagger (+1) (subtract 1) :: Dagger (->) Int Int
>>> front d 5
6
>>> back d 6
5

Constructors

Dagger
Fields front :: arr a b The forward direction. back :: arr b a The backward direction.

Instances

Instances details

Channel t arr => Channel (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) Source #
Instance details Defined in Circuit.Dagger Methods assoc :: forall (a :: k) (b :: k) (c :: k). Dagger arr (t (t a b) c) (t a (t b c)) Source # assoc' :: forall (a :: k) (b :: k) (c :: k). Dagger arr (t a (t b c)) (t (t a b) c) Source # slide :: forall (a :: k) (b :: k) (c :: k). Dagger arr (t a (t b c)) (t b (t a c)) Source #
Strength t arr => Strength (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) Source #
Instance details Defined in Circuit.Dagger Methods strength :: forall (b :: k) (c :: k) (a :: k). Dagger arr b c -> Dagger arr (t a b) (t a c) Source #
Traced t arr => Traced (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) Source #
Instance details Defined in Circuit.Dagger Methods trace :: forall (a :: k) (b :: k) (c :: k). Dagger arr (t a b) (t a c) -> Dagger arr b c Source #
Action t arr => Action (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) Source #
Instance details Defined in Circuit.Dagger Methods braid :: forall (a :: k) (b :: k). Dagger arr (t a b) (t b a) Source #
Tensor t arr => Tensor (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) Source #
Instance details Defined in Circuit.Dagger Methods tensor :: forall (a :: k) (b :: k) (c :: k) (d :: k). Dagger arr a b -> Dagger arr c d -> Dagger arr (t a c) (t b d) Source #
Unital t arr => Unital (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) Source #
Instance details Defined in Circuit.Dagger Methods unitl :: forall (a :: k). Dagger arr (t (Unit t) a) a Source # unitl' :: forall (a :: k). Dagger arr a (t (Unit t) a) Source # unitr :: forall (a :: k). Dagger arr (t a (Unit t)) a Source # unitr' :: forall (a :: k). Dagger arr a (t a (Unit t)) Source #
(CopyT t arr a, MergeT t arr a) => CopyT (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) (a :: k) Source #	Tensor-generic bimonoid interlock through `Dagger`. These instances mirror the cartesian ones above, but work for any wiring tensor `t`. They are the missing lemma that makes `mirror` total: a `Net` over 'Dagger arr' can transpose its bimonoid rows because the dagger swaps the tensor-comonoid and tensor-monoid dictionaries. `>>>` `let d = copyT @(,) @(Dagger (->)) @Int :: Dagger (->) Int (Int, Int)``>>>` `front d 5`(5,5) `>>>` `back d (2, 3)`5
Instance details Defined in Circuit.Dagger Methods copyT :: Dagger arr a (t a a) Source #
(DiscardT t arr a, ZeroT t arr a) => DiscardT (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) (a :: k) Source #
Instance details Defined in Circuit.Dagger Methods discardT :: Dagger arr a (Unit t) Source #
(MergeT t arr a, CopyT t arr a) => MergeT (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) (a :: k) Source #
Instance details Defined in Circuit.Dagger Methods plusT :: Dagger arr (t a a) a Source #
(ZeroT t arr a, DiscardT t arr a) => ZeroT (t :: k -> k -> k) (Dagger arr :: k -> k -> Type) (a :: k) Source #
Instance details Defined in Circuit.Dagger Methods zeroT :: Dagger arr (Unit t) a Source #
Category arr => Category (Dagger arr :: k -> k -> Type) Source #
Instance details Defined in Circuit.Dagger Methods id :: forall (a :: k). Dagger arr a a Source # (.) :: forall (b :: k) (c :: k) (a :: k). Dagger arr b c -> Dagger arr a b -> Dagger arr a c Source #
(Discard arr a, Zero arr a) => Discard (Dagger arr :: Type -> Type -> Type) (a :: Type) Source #
Instance details Defined in Circuit.Dagger Methods discard :: Dagger arr a () Source #
(Zero arr a, Discard arr a) => Zero (Dagger arr :: Type -> Type -> Type) (a :: Type) Source #
Instance details Defined in Circuit.Dagger Methods zero :: Dagger arr () a Source #
(Copy arr a, Merge arr a) => Copy (Dagger arr) a Source #	Forward copy, backward add — the bimonoid self-duality. The interlock is the point to notice: `Copy` on the dagger requires `Merge` on the base. The comonoid and monoid cannot be granted separately in this construction; `Dagger (FinRel k)` is where that collapse becomes observable (see the `circuits-axioma` oracle).
Instance details Defined in Circuit.Dagger Methods copy :: Dagger arr a (a, a) Source #
(Merge arr a, Copy arr a) => Merge (Dagger arr) a Source #	Forward add, backward copy.
Instance details Defined in Circuit.Dagger Methods plus :: Dagger arr (a, a) a Source #

transpose :: forall {k} (arr :: k -> k -> Type) (a :: k) (b :: k). Dagger arr a b -> Dagger arr b a Source #

The dagger operation: braid forward and backward.

Involutive: transpose . transpose = id.