Safe Haskell	None
Language	GHC2024

Circuit.Par

Contents

Multiplicative disjunction
Linear distributors and mix

Description

Multiplicative disjunction (⅋) and its linear distributors.

This module surfaces the tensor product, its unit ⊥, and the one-way distributors between tensor and tensor. These are "mixed metaphor" structure: they relate a tensor t (typically (,)) with a tensor product p (typically Either).

Synopsis

type family Bot (p :: k -> k -> k) :: k
class Category arr => Par (p :: k -> k -> k) (arr :: k -> k -> Type) where
- parP :: forall (a :: k) (b :: k) (c :: k) (d :: k). arr a b -> arr c d -> arr (p a c) (p b d)
- unitlP :: forall (a :: k). arr (p (Bot p) a) a
- unitlP' :: forall (a :: k). arr a (p (Bot p) a)
- unitrP :: forall (a :: k). arr (p a (Bot p)) a
- unitrP' :: forall (a :: k). arr a (p a (Bot p))
distL :: (a, Either b c) -> Either (a, b) c
distR :: (Either b c, a) -> Either b (c, a)
mix :: Void -> ()

Multiplicative disjunction

type family Bot (p :: k -> k -> k) :: k Source #

Unit of the tensor tensor (⊥).

Instances

Instances details

type Bot Either Source #	The coproduct is the canonical tensor product on functions.
Instance details Defined in Circuit.Par type Bot Either = Void

class Category arr => Par (p :: k -> k -> k) (arr :: k -> k -> Type) where Source #

Multiplicative disjunction action on a category.

parP is the tensor product of morphisms. The unitors witness that ⊥ ⅋ a ≅ a and a ⅋ ⊥ ≅ a.

Methods

parP :: forall (a :: k) (b :: k) (c :: k) (d :: k). arr a b -> arr c d -> arr (p a c) (p b d) Source #

Parallel composition under tensor.

unitlP :: forall (a :: k). arr (p (Bot p) a) a Source #

Left unitor: ⊥ ⅋ a -> a.

unitlP' :: forall (a :: k). arr a (p (Bot p) a) Source #

Inverse left unitor: a -> ⊥ ⅋ a.

unitrP :: forall (a :: k). arr (p a (Bot p)) a Source #

Right unitor: a ⅋ ⊥ -> a.

unitrP' :: forall (a :: k). arr a (p a (Bot p)) Source #

Inverse right unitor: a -> a ⅋ ⊥.

Instances

Instances details

Monad m => Par Either (K m :: Type -> Type -> Type) Source #	Coproduct as multiplicative disjunction on `K` arrows.
Instance details Defined in Circuit.Par Methods parP :: K m a b -> K m c d -> K m (Either a c) (Either b d) Source # unitlP :: K m (Either (Bot Either) a) a Source # unitlP' :: K m a (Either (Bot Either) a) Source # unitrP :: K m (Either a (Bot Either)) a Source # unitrP' :: K m a (Either a (Bot Either)) Source #
Par Either (->) Source #	Coproduct as multiplicative disjunction on functions. The unit is the initial object `Void`; the unitors are the coproduct injections absorbed by the universal property.
Instance details Defined in Circuit.Par Methods parP :: (a -> b) -> (c -> d) -> Either a c -> Either b d Source # unitlP :: Either (Bot Either) a -> a Source # unitlP' :: a -> Either (Bot Either) a Source # unitrP :: Either a (Bot Either) -> a Source # unitrP' :: a -> Either a (Bot Either) Source #

Linear distributors and mix

distL :: (a, Either b c) -> Either (a, b) c Source #

Left linear distributor: A ⊗ (B ⅋ C) -> (A ⊗ B) ⅋ C.

For (,) and Either this is the one-way product-over-coproduct map. Note that (_, Right c) = Right c discards the a; this is legal affinely but not in strict MLL. The distributors already live in the affine fragment.

distR :: (Either b c, a) -> Either b (c, a) Source #

Right linear distributor: (B ⅋ C) ⊗ A -> B ⅋ (C ⊗ A).

Mirror of distL: the same affine discard is present when the left summand is taken.

mix :: Void -> () Source #

Mix: the canonical map ⊥ -> 1 from tensor unit to tensor unit.

Every ⊥-value is vacuous, so it maps to the unique tensor unit.