Safe Haskell	None
Language	GHC2024

Circuit.Linear

Contents

Linear implication (internal hom)
Exponentials

Description

Linear-logic connectives over a base category.

This module surfaces linear implication (⊸) and the exponential modalities ! / ? as type-class structure. The tensor product ⅋ and its unit ⊥ live in Circuit.Par.

Synopsis

class Category arr => Lolli (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) where
- type LolliT (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) a b
- lolli :: arr a b -> arr (LolliT t arr a b) (LolliT t arr a b)
- eval :: arr (t a (LolliT t arr a b)) b
- curry :: arr (t a b) c -> arr a (LolliT t arr b c)
- uncurry :: arr a (LolliT t arr b c) -> arr (t a b) c
class Tensor t arr => Exponential (t :: k -> k -> k) (arr :: k -> k -> Type) where
- type Bang (t :: k -> k -> k) (arr :: k -> k -> Type) a
- type WhyNot (t :: k -> k -> k) (arr :: k -> k -> Type) a = (result :: Type) | result -> a
class Exponential t arr => BangCopy (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) where
- copyE :: arr (Bang t arr a) (t (Bang t arr a) (Bang t arr a))
class Exponential t arr => BangWeaken (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) where
- discardE :: arr (Bang t arr a) (Unit t)
- derelict :: arr (Bang t arr a) a
class Exponential t arr => WhyNotIntro (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) where
- introduce :: arr a (WhyNot t arr a)
class (Exponential t arr, Par p arr) => WhyNotMonoid (t :: Type -> Type -> Type) (p :: Type -> Type -> Type) (arr :: Type -> Type -> Type) where
- mergeE :: arr (p (WhyNot t arr a) (WhyNot t arr a)) (WhyNot t arr a)
- zeroE :: arr (Bot p) (WhyNot t arr a)
type LinearBang (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = (Exponential t arr, BangCopy t arr, BangWeaken t arr)
type AffineBang (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = (Exponential t arr, BangWeaken t arr)
type RelevantBang (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = (Exponential t arr, BangCopy t arr)

Linear implication (internal hom)

class Category arr => Lolli (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) where Source #

Closed monoidal structure: A ⊸ B is the right adjoint of tensor.

Maps A ⊗ B -> C correspond to maps A -> B ⊸ C via curry/uncurry. eval is the counit A ⊗ (A ⊸ B) -> B (hom on the right of the tensor). That is the existing Chu convention; it differs from uncurry id by a braid. lolli is identity on the implication object, used to mention it.

Kind is fixed to Type so type applications stay concrete (GHC 9.14 panics on kind-polymorphic TypeApplications here).

Associated Types

type LolliT (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) a b Source #

The implication object A ⊸ B.

Indexed by the base arrow as well as the tensor, so (->) and Mat can both close (,) without colliding.

Methods

lolli :: arr a b -> arr (LolliT t arr a b) (LolliT t arr a b) Source #

Identity at the implication object. The argument is a type proxy.

eval :: arr (t a (LolliT t arr a b)) b Source #

Evaluation counit A ⊗ (A ⊸ B) -> B.

curry :: arr (t a b) c -> arr a (LolliT t arr b c) Source #

Curry the left factor: (A ⊗ B -> C) -> (A -> B ⊸ C).

uncurry :: arr a (LolliT t arr b c) -> arr (t a b) c Source #

Uncurry the left factor: (A -> B ⊸ C) -> (A ⊗ B -> C).

Instances

Instances details

Lolli (,) (->) Source #

Cartesian closed structure on functions: implication collapses to function space.

Instance details

Defined in Circuit.Linear

Associated Types

type LolliT (,) (->) a b
Instance details Defined in Circuit.Linear type LolliT (,) (->) a b = a -> b

Methods

lolli :: (a -> b) -> LolliT (,) (->) a b -> LolliT (,) (->) a b Source #

eval :: (a, LolliT (,) (->) a b) -> b Source #

curry :: ((a, b) -> c) -> a -> LolliT (,) (->) b c Source #

uncurry :: (a -> LolliT (,) (->) b c) -> (a, b) -> c Source #

Exponentials

class Tensor t arr => Exponential (t :: k -> k -> k) (arr :: k -> k -> Type) Source #

Exponential modality: object-level types for !A and ?A.

The structural rules are split into independent subclasses so that affine and linear uses of the modality differ only in their constraint sets, mirroring the Copy/Discard split at the base-arrow level.

!A has a contraction half (BangCopy) and a weakening half (BangWeaken). Linear logic requires both; affine logic requires only weakening.
?A currently exposes only its unit rule (WhyNotIntro); the ⅋-monoid multiplication on ?A (WhyNotMerge) is missing. In the vocabulary of Dagger, ?A is currently CoAffine-only (the unit Zero) and the missing half is CoRelevant (the merge Merge).

Associated Types

type Bang (t :: k -> k -> k) (arr :: k -> k -> Type) a Source #

type WhyNot (t :: k -> k -> k) (arr :: k -> k -> Type) a = (result :: Type) | result -> a Source #

Instances

Instances details

Exponential (,) (->) Source #

Cartesian collapse: !A ≅ A, and ?A is the free monoid of lists.

Instance details

Defined in Circuit.Linear

Associated Types

type Bang (,) (->) a
Instance details Defined in Circuit.Linear type Bang (,) (->) a = a
type WhyNot (,) (->) a
Instance details Defined in Circuit.Linear type WhyNot (,) (->) a = [a]

class Exponential t arr => BangCopy (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) where Source #

Contraction half of !A: copy !A → !A ⊗ !A.

Methods

copyE :: arr (Bang t arr a) (t (Bang t arr a) (Bang t arr a)) Source #

Instances

Instances details

BangCopy (,) (->) Source #
Instance details Defined in Circuit.Linear Methods copyE :: Bang (,) (->) a -> (Bang (,) (->) a, Bang (,) (->) a) Source #

class Exponential t arr => BangWeaken (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) where Source #

Weakening half of !A: dereliction !A → A and discard !A → I.

Methods

discardE :: arr (Bang t arr a) (Unit t) Source #

derelict :: arr (Bang t arr a) a Source #

Instances

Instances details

BangWeaken (,) (->) Source #
Instance details Defined in Circuit.Linear Methods discardE :: Bang (,) (->) a -> Unit (,) Source # derelict :: Bang (,) (->) a -> a Source #

class Exponential t arr => WhyNotIntro (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) where Source #

Unit rule for ?A: introduction A → ?A.

Methods

introduce :: arr a (WhyNot t arr a) Source #

Instances

Instances details

WhyNotIntro (,) (->) Source #
Instance details Defined in Circuit.Linear Methods introduce :: a -> WhyNot (,) (->) a Source #

class (Exponential t arr, Par p arr) => WhyNotMonoid (t :: Type -> Type -> Type) (p :: Type -> Type -> Type) (arr :: Type -> Type -> Type) where Source #

The ⅋-monoid structure on ?A.

Dual to the !-comonoid (BangCopy / BangWeaken), but living on the tensor product rather than the tensor product. mergeE is the multiplication ?A ⅋ ?A → ?A and zeroE is the unit ⊥ → ?A.

Methods

mergeE :: arr (p (WhyNot t arr a) (WhyNot t arr a)) (WhyNot t arr a) Source #

zeroE :: arr (Bot p) (WhyNot t arr a) Source #

Instances

Instances details

WhyNotMonoid (,) Either (->) Source #
Instance details Defined in Circuit.Linear Methods mergeE :: Either (WhyNot (,) (->) a) (WhyNot (,) (->) a) -> WhyNot (,) (->) a Source # zeroE :: Bot Either -> WhyNot (,) (->) a Source #

type LinearBang (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = (Exponential t arr, BangCopy t arr, BangWeaken t arr) Source #

Linear !A: both contraction and weakening.

type AffineBang (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = (Exponential t arr, BangWeaken t arr) Source #

Affine !A: weakening only.

type RelevantBang (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) = (Exponential t arr, BangCopy t arr) Source #

Relevant !A: contraction only.