Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Linear

Description

The category of Haskell types and linear functions: the kind LINEAR wraps Type in L, and a morphism is a a %1 -> b function. Symmetric monoidal closed with L a ** L b = L (a, b). The categorical product is With, and only comonoid objects (such as L (Ur a)) can be copied or discarded, so it is deliberately not CopyDiscard.

Synopsis

data LINEAR = L Type
data Linear (a :: LINEAR) (b :: LINEAR) where
- Linear :: forall a1 b1. (a1 %1 -> b1) -> Linear ('L a1) ('L b1)
unLinear :: ('L a ~> 'L b) %1 -> a %1 -> b
data family Forget :: LINEAR +-> Type
data Ur a where
- Ur :: forall a. a -> Ur a
counitUr :: Ur a %1 -> a
dupUr :: Ur a %1 -> Ur (Ur a)
data Top where
- Top :: forall a. a -> Top
data With a b where
- With :: forall x a b. x -> (x %1 -> a) -> (x %1 -> b) -> With a b
urWith :: Ur (With a b) %1 -> (Ur a, Ur b)
mkWith :: a -> b -> With a b
type Not a = a %1 -> ()
not :: (Not b %1 -> Not a) %1 -> a %1 -> b
not' :: (a %1 -> b) %1 -> Not b %1 -> Not a
newtype Par a b = Par (Not (Not a, Not b))
mkPar :: a %1 -> b %1 -> Par a b
pairFst :: (a, Par b c) %1 -> Par (a, b) c
pairSnd :: (Par a b, c) %1 -> Par a (b, c)
parAppL :: Par a b %1 -> Not a %1 -> b
parAppR :: Par a b %1 -> Not b %1 -> a
newtype Quest a = Quest (Not (Ur (Not a)))
notQuest :: Not (Quest a) %1 -> Ur (Not a)
unitQuest :: a %1 -> Quest a
multQuest :: Quest (Quest a) %1 -> Quest a
questPar :: Par (Quest a) (Quest b) %1 -> Quest (Either a b)
dn :: Not (Not a) %1 -> a
unsafeLinear :: (a -> b) -> a %1 -> b
unit :: 'L () ~> 'L (Par a (Not a))
counit :: 'L (Not a, a) ~> 'L ()
type (!~>) (p :: k -> k1 -> Type) (q :: k -> k1 -> Type) = forall (a :: k) (b :: k1). p a b %1 -> q a b
data NegComp (p :: j +-> k) (q :: i +-> j) (a :: k) (c :: i) where
- NegComp :: forall {j} {k} {i} (p :: j +-> k) (a :: k) (q :: i +-> j) (c :: i). (forall (b :: j). Par (p a b) (q b c)) -> NegComp p q a c
newtype Neg (p :: k -> k1 -> Type) (a :: k1) (b :: k) = Neg (Not (p b a))
getNeg :: forall {k1} {k2} p (a :: k2) (b :: k1). Neg p a b %1 -> Not (p b a)
conv1 :: forall {k1} {k2} {k3} (p :: k1 +-> k2) (q :: k3 +-> k1) (a :: k2) (b :: k3). NegComp p q a b %1 -> Neg (Neg q :.: Neg p) a b
conv2 :: forall {j} {i} {k} (q :: j -> i -> Type) (p :: k -> j -> Type) (a :: k) (b :: i). Neg (Neg q :.: Neg p) a b %1 -> NegComp p q a b
asCocat :: forall {i} (p :: i -> i -> Type). ((Neg p :.: Neg p) !~> Neg p) -> p !~> NegComp p p

Documentation

data LINEAR Source Github #

Constructors

L Type

Instances

Instances details

Monoidal LINEAR Source Github #

Tuples as monoidal tensor. Tuples are not the binary product in LINEAR.

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.Linear type Unit = 'L ()
type ('L a :: LINEAR) ** ('L b :: LINEAR)
Instance details Defined in Proarrow.Category.Instance.Linear type ('L a :: LINEAR) ** ('L b :: LINEAR) = 'L (a, b)

Methods

withOb2 :: forall (a :: LINEAR) (b :: LINEAR) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Github #

leftUnitor :: forall (a :: LINEAR). Ob a => ((Unit :: LINEAR) ** a) ~> a Source Github #

leftUnitorInv :: forall (a :: LINEAR). Ob a => a ~> ((Unit :: LINEAR) ** a) Source Github #

rightUnitor :: forall (a :: LINEAR). Ob a => (a ** (Unit :: LINEAR)) ~> a Source Github #

rightUnitorInv :: forall (a :: LINEAR). Ob a => a ~> (a ** (Unit :: LINEAR)) Source Github #

associator :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Github #

associatorInv :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Github #

SymMonoidal LINEAR Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

swap :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Github #

Closed LINEAR Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type (a :: LINEAR) ~~> (b :: LINEAR)
Instance details Defined in Proarrow.Category.Instance.Linear type (a :: LINEAR) ~~> (b :: LINEAR) = 'L (UN 'L a %1 -> UN 'L b)

Methods

withObExp :: forall (a :: LINEAR) (b :: LINEAR) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r Source Github #

curry :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) Source Github #

apply :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Github #

(^^^) :: forall (a :: LINEAR) (b :: LINEAR) (x :: LINEAR) (y :: LINEAR). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Github #

Distributive LINEAR Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

distL :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR). (Ob a, Ob b, Ob c) => (a ** (b || c)) ~> ((a ** b) || (a ** c)) Source Github #

distR :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR). (Ob a, Ob b, Ob c) => ((a || b) ** c) ~> ((a ** c) || (b ** c)) Source Github #

absorbL :: forall (a :: LINEAR). Ob a => (a ** (InitialObject :: LINEAR)) ~> (InitialObject :: LINEAR) Source Github #

absorbR :: forall (a :: LINEAR). Ob a => ((InitialObject :: LINEAR) ** a) ~> (InitialObject :: LINEAR) Source Github #

StarAutonomous LINEAR Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type Dual ('L a :: LINEAR)
Instance details Defined in Proarrow.Category.Instance.Linear type Dual ('L a :: LINEAR) = 'L (Not a)

Methods

withObDual :: forall (a :: LINEAR) r. Ob a => (Ob (Dual a) => r) -> r Source Github #

dual :: forall (a :: LINEAR) (b :: LINEAR). (a ~> b) -> Dual b ~> Dual a Source Github #

dualInv :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> a Source Github #

linDist :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR). (Ob a, Ob b, Ob c) => ((a ** b) ~> Dual c) -> a ~> Dual (b ** c) Source Github #

linDistInv :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR). (Ob a, Ob b, Ob c) => (a ~> Dual (b ** c)) -> (a ** b) ~> Dual c Source Github #

doubleNeg :: forall (a :: LINEAR). Ob a => Dual (Dual a) ~> a Source Github #

doubleNegInv :: forall (a :: LINEAR). Ob a => a ~> Dual (Dual a) Source Github #

HasBinaryCoproducts LINEAR Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type ('L a :: LINEAR) \|\| ('L b :: LINEAR)
Instance details Defined in Proarrow.Category.Instance.Linear type ('L a :: LINEAR) \|\| ('L b :: LINEAR) = 'L (Either a b)

Methods

withObCoprod :: forall (a :: LINEAR) (b :: LINEAR) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Github #

lft :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => a ~> (a || b) Source Github #

rgt :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => b ~> (a || b) Source Github #

(|||) :: forall (x :: LINEAR) (a :: LINEAR) (y :: LINEAR). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Github #

(+++) :: forall (a :: LINEAR) (b :: LINEAR) (x :: LINEAR) (y :: LINEAR). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Github #

HasInitialObject LINEAR Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Linear type InitialObject = 'L Void

Methods

initiate :: forall (a :: LINEAR). Ob a => (InitialObject :: LINEAR) ~> a Source Github #

CategoryOf LINEAR Source Github #

Category of linear functions.

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Linear type (~>) = Linear
type Ob (a :: LINEAR)
Instance details Defined in Proarrow.Category.Instance.Linear type Ob (a :: LINEAR) = Is 'L a

HasBinaryProducts LINEAR Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type ('L a :: LINEAR) && ('L b :: LINEAR)
Instance details Defined in Proarrow.Category.Instance.Linear type ('L a :: LINEAR) && ('L b :: LINEAR) = 'L (With a b)

Methods

withObProd :: forall (a :: LINEAR) (b :: LINEAR) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: LINEAR) (x :: LINEAR) (y :: LINEAR). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: LINEAR) (b :: LINEAR) (x :: LINEAR) (y :: LINEAR). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

HasTerminalObject LINEAR Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Linear type TerminalObject = 'L Top

Methods

terminate :: forall (a :: LINEAR). Ob a => a ~> (TerminalObject :: LINEAR) Source Github #

Copowered Type LINEAR Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type (n :: Type) *. ('L a :: LINEAR)
Instance details Defined in Proarrow.Category.Instance.Linear type (n :: Type) *. ('L a :: LINEAR) = 'L (Ur n, a)

Methods

withObCopower :: forall (a :: LINEAR) n r. (Ob a, Ob n) => (Ob (n *. a) => r) -> r Source Github #

copower :: forall (a :: LINEAR) (b :: LINEAR) n. (Ob a, Ob b) => (n ~> HomObj Type a b) -> (n *. a) ~> b Source Github #

uncopower :: forall (a :: LINEAR) n (b :: LINEAR). (Ob a, Ob n) => ((n *. a) ~> b) -> n ~> HomObj Type a b Source Github #

Promonad Linear Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

id :: forall (a :: LINEAR). Ob a => Linear a a Source Github #

(.) :: forall (b :: LINEAR) (c :: LINEAR) (a :: LINEAR). Linear b c -> Linear a b -> Linear a c Source Github #

Powered Type LINEAR Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type ('L a :: LINEAR) ^ (n :: Type)
Instance details Defined in Proarrow.Category.Instance.Linear type ('L a :: LINEAR) ^ (n :: Type) = 'L (n -> a)

Methods

withObPower :: forall (a :: LINEAR) n r. (Ob a, Ob n) => (Ob (a ^ n) => r) -> r Source Github #

power :: forall (a :: LINEAR) (b :: LINEAR) n. (Ob a, Ob b) => (n ~> HomObj Type a b) -> a ~> (b ^ n) Source Github #

unpower :: forall (b :: LINEAR) n (a :: LINEAR). (Ob b, Ob n) => (a ~> (b ^ n)) -> n ~> HomObj Type a b Source Github #

MonoidalProfunctor Linear Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

one :: Linear (Unit :: LINEAR) (Unit :: LINEAR) Source Github #

(**) :: forall (x1 :: LINEAR) (x2 :: LINEAR) (y1 :: LINEAR) (y2 :: LINEAR). Linear x1 x2 -> Linear y1 y2 -> Linear (x1 ** y1) (x2 ** y2) Source Github #

Profunctor Linear Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

dimap :: forall (c :: LINEAR) (a :: LINEAR) (b :: LINEAR) (d :: LINEAR). (c ~> a) -> (b ~> d) -> Linear a b -> Linear c d Source Github #

lmap :: forall (c :: LINEAR) (a :: LINEAR) (b :: LINEAR). (c ~> a) -> Linear a b -> Linear c b Source Github #

rmap :: forall (b :: LINEAR) (d :: LINEAR) (a :: LINEAR). (b ~> d) -> Linear a b -> Linear a d Source Github #

(\\) :: forall (a :: LINEAR) (b :: LINEAR) r. ((Ob a, Ob b) => r) -> Linear a b -> r Source Github #

FunctorForRep Forget Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type Forget @ (a :: LINEAR)
Instance details Defined in Proarrow.Category.Instance.Linear type Forget @ (a :: LINEAR) = UN 'L a

Methods

fmap :: forall (a :: LINEAR) (b :: LINEAR). (a ~> b) -> (Forget @ a) ~> (Forget @ b) Source Github #

MonoidalProfunctor (Rep Forget) Source Github #

Forget is a lax monoidal functor

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

one :: Rep Forget (Unit :: Type) (Unit :: LINEAR) Source Github #

(**) :: forall x1 (x2 :: LINEAR) y1 (y2 :: LINEAR). Rep Forget x1 x2 -> Rep Forget y1 y2 -> Rep Forget (x1 ** y1) (x2 ** y2) Source Github #

MonoidalProfunctor (Corep Forget) Source Github #

Forget is also a colax monoidal functor

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

one :: Corep Forget (Unit :: LINEAR) (Unit :: Type) Source Github #

(**) :: forall (x1 :: LINEAR) x2 (y1 :: LINEAR) y2. Corep Forget x1 x2 -> Corep Forget y1 y2 -> Corep Forget (x1 ** y1) (x2 ** y2) Source Github #

Corepresentable (Rep Forget) Source Github #

By creating the left adjoint to the forgetful functor, we obtain the free-forgetful adjunction between Hask and LINEAR

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type (Rep Forget) %% (a :: Type)
Instance details Defined in Proarrow.Category.Instance.Linear type (Rep Forget) %% (a :: Type) = 'L (Ur a)

Methods

coindex :: forall a (b :: LINEAR). Rep Forget a b -> (Rep Forget %% a) ~> b Source Github #

cotabulate :: forall a (b :: LINEAR). Ob a => ((Rep Forget %% a) ~> b) -> Rep Forget a b Source Github #

corepMap :: (a ~> b) -> (Rep Forget %% a) ~> (Rep Forget %% b) Source Github #

corepUniv :: Ob a => Rep Forget a (Rep Forget %% a) Source Github #

Comonoid ('L (Ur a) :: LINEAR) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

counit :: 'L (Ur a) ~> (Unit :: LINEAR) Source Github #

comult :: 'L (Ur a) ~> ('L (Ur a) ** 'L (Ur a)) Source Github #

Comonoid ('L Bool) Source Github #

L Bool is a comonoid: a Bool is duplicated and discarded by case analysis, which is linear (it consumes the input exactly once). The same holds for any finite, pattern-matchable classical type. Only the Bool instance is spelled out here.

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

counit :: 'L Bool ~> (Unit :: LINEAR) Source Github #

comult :: 'L Bool ~> ('L Bool ** 'L Bool) Source Github #

Costrong (CoprodAction :: LINEAR -> (COPROD LINEAR, LINEAR) -> Type) Linear Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

coact :: forall (a :: COPROD LINEAR) (x :: LINEAR) (y :: LINEAR). (Ob a, Ob x, Ob y) => Linear (Act (CoprodAction :: LINEAR -> (COPROD LINEAR, LINEAR) -> Type) a x) (Act (CoprodAction :: LINEAR -> (COPROD LINEAR, LINEAR) -> Type) a y) -> Linear x y Source Github #

MonoidalProfunctor (Coprod Linear) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

one :: Coprod Linear (Unit :: COPROD LINEAR) (Unit :: COPROD LINEAR) Source Github #

(**) :: forall (x1 :: COPROD LINEAR) (x2 :: COPROD LINEAR) (y1 :: COPROD LINEAR) (y2 :: COPROD LINEAR). Coprod Linear x1 x2 -> Coprod Linear y1 y2 -> Coprod Linear (x1 ** y1) (x2 ** y2) Source Github #

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type Unit = 'L ()

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type InitialObject = 'L Void

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type (~>) = Linear

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type TerminalObject = 'L Top

type Ob (a :: LINEAR) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type Ob (a :: LINEAR) = Is 'L a

type (a :: LINEAR) ~~> (b :: LINEAR) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type (a :: LINEAR) ~~> (b :: LINEAR) = 'L (UN 'L a %1 -> UN 'L b)

type Forget @ (a :: LINEAR) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type Forget @ (a :: LINEAR) = UN 'L a

type (n :: Type) *. ('L a :: LINEAR) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type (n :: Type) *. ('L a :: LINEAR) = 'L (Ur n, a)

type ('L a :: LINEAR) ^ (n :: Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type ('L a :: LINEAR) ^ (n :: Type) = 'L (n -> a)

type (Rep Forget) %% (a :: Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type (Rep Forget) %% (a :: Type) = 'L (Ur a)

type Dual ('L a :: LINEAR) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type Dual ('L a :: LINEAR) = 'L (Not a)

type ('L a :: LINEAR) ** ('L b :: LINEAR) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type ('L a :: LINEAR) ** ('L b :: LINEAR) = 'L (a, b)

type ('L a :: LINEAR) || ('L b :: LINEAR) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type ('L a :: LINEAR) || ('L b :: LINEAR) = 'L (Either a b)

type ('L a :: LINEAR) && ('L b :: LINEAR) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type ('L a :: LINEAR) && ('L b :: LINEAR) = 'L (With a b)

data Linear (a :: LINEAR) (b :: LINEAR) where Source Github #

Constructors

Linear :: forall a1 b1. (a1 %1 -> b1) -> Linear ('L a1) ('L b1)

Instances

Instances details

Promonad Linear Source Github #
Instance details Defined in Proarrow.Category.Instance.Linear Methods id :: forall (a :: LINEAR). Ob a => Linear a a Source Github # (.) :: forall (b :: LINEAR) (c :: LINEAR) (a :: LINEAR). Linear b c -> Linear a b -> Linear a c Source Github #
MonoidalProfunctor Linear Source Github #
Instance details Defined in Proarrow.Category.Instance.Linear Methods one :: Linear (Unit :: LINEAR) (Unit :: LINEAR) Source Github # () :: forall (x1 :: LINEAR) (x2 :: LINEAR) (y1 :: LINEAR) (y2 :: LINEAR). Linear x1 x2 -> Linear y1 y2 -> Linear (x1 y1) (x2 ** y2) Source Github #
Profunctor Linear Source Github #
Instance details Defined in Proarrow.Category.Instance.Linear Methods dimap :: forall (c :: LINEAR) (a :: LINEAR) (b :: LINEAR) (d :: LINEAR). (c ~> a) -> (b ~> d) -> Linear a b -> Linear c d Source Github # lmap :: forall (c :: LINEAR) (a :: LINEAR) (b :: LINEAR). (c ~> a) -> Linear a b -> Linear c b Source Github # rmap :: forall (b :: LINEAR) (d :: LINEAR) (a :: LINEAR). (b ~> d) -> Linear a b -> Linear a d Source Github # (\\) :: forall (a :: LINEAR) (b :: LINEAR) r. ((Ob a, Ob b) => r) -> Linear a b -> r Source Github #
Costrong (CoprodAction :: LINEAR -> (COPROD LINEAR, LINEAR) -> Type) Linear Source Github #
Instance details Defined in Proarrow.Category.Instance.Linear Methods coact :: forall (a :: COPROD LINEAR) (x :: LINEAR) (y :: LINEAR). (Ob a, Ob x, Ob y) => Linear (Act (CoprodAction :: LINEAR -> (COPROD LINEAR, LINEAR) -> Type) a x) (Act (CoprodAction :: LINEAR -> (COPROD LINEAR, LINEAR) -> Type) a y) -> Linear x y Source Github #
MonoidalProfunctor (Coprod Linear) Source Github #
Instance details Defined in Proarrow.Category.Instance.Linear Methods one :: Coprod Linear (Unit :: COPROD LINEAR) (Unit :: COPROD LINEAR) Source Github # () :: forall (x1 :: COPROD LINEAR) (x2 :: COPROD LINEAR) (y1 :: COPROD LINEAR) (y2 :: COPROD LINEAR). Coprod Linear x1 x2 -> Coprod Linear y1 y2 -> Coprod Linear (x1 y1) (x2 ** y2) Source Github #

unLinear :: ('L a ~> 'L b) %1 -> a %1 -> b Source Github #

data family Forget :: LINEAR +-> Type Source Github #

Instances

Instances details

FunctorForRep Forget Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type Forget @ (a :: LINEAR)
Instance details Defined in Proarrow.Category.Instance.Linear type Forget @ (a :: LINEAR) = UN 'L a

Methods

fmap :: forall (a :: LINEAR) (b :: LINEAR). (a ~> b) -> (Forget @ a) ~> (Forget @ b) Source Github #

MonoidalProfunctor (Rep Forget) Source Github #

Forget is a lax monoidal functor

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

one :: Rep Forget (Unit :: Type) (Unit :: LINEAR) Source Github #

(**) :: forall x1 (x2 :: LINEAR) y1 (y2 :: LINEAR). Rep Forget x1 x2 -> Rep Forget y1 y2 -> Rep Forget (x1 ** y1) (x2 ** y2) Source Github #

MonoidalProfunctor (Corep Forget) Source Github #

Forget is also a colax monoidal functor

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

one :: Corep Forget (Unit :: LINEAR) (Unit :: Type) Source Github #

(**) :: forall (x1 :: LINEAR) x2 (y1 :: LINEAR) y2. Corep Forget x1 x2 -> Corep Forget y1 y2 -> Corep Forget (x1 ** y1) (x2 ** y2) Source Github #

Corepresentable (Rep Forget) Source Github #

By creating the left adjoint to the forgetful functor, we obtain the free-forgetful adjunction between Hask and LINEAR

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type (Rep Forget) %% (a :: Type)
Instance details Defined in Proarrow.Category.Instance.Linear type (Rep Forget) %% (a :: Type) = 'L (Ur a)

Methods

coindex :: forall a (b :: LINEAR). Rep Forget a b -> (Rep Forget %% a) ~> b Source Github #

cotabulate :: forall a (b :: LINEAR). Ob a => ((Rep Forget %% a) ~> b) -> Rep Forget a b Source Github #

corepMap :: (a ~> b) -> (Rep Forget %% a) ~> (Rep Forget %% b) Source Github #

corepUniv :: Ob a => Rep Forget a (Rep Forget %% a) Source Github #

type Forget @ (a :: LINEAR) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type Forget @ (a :: LINEAR) = UN 'L a

type (Rep Forget) %% (a :: Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Linear

type (Rep Forget) %% (a :: Type) = 'L (Ur a)

data Ur a where Source Github #

Constructors

Ur :: forall a. a -> Ur a

Instances

Instances details

Functor Ur Source Github #
Instance details Defined in Proarrow.Category.Instance.Linear Methods map :: (a ~> b) -> Ur a ~> Ur b Source Github #
Comonoid ('L (Ur a) :: LINEAR) Source Github #
Instance details Defined in Proarrow.Category.Instance.Linear Methods counit :: 'L (Ur a) ~> (Unit :: LINEAR) Source Github # comult :: 'L (Ur a) ~> ('L (Ur a) ** 'L (Ur a)) Source Github #

counitUr :: Ur a %1 -> a Source Github #

dupUr :: Ur a %1 -> Ur (Ur a) Source Github #

data Top where Source Github #

Constructors

Top :: forall a. a -> Top

Instances

Instances details

Show Top Source Github #
Instance details Defined in Proarrow.Category.Instance.Linear Methods showsPrec :: Int -> Top -> ShowS Github # show :: Top -> String Github # showList :: [Top] -> ShowS Github #
Eq Top Source Github #
Instance details Defined in Proarrow.Category.Instance.Linear Methods (==) :: Top -> Top -> Bool Github # (/=) :: Top -> Top -> Bool Github #

data With a b where Source Github #

Constructors

With :: forall x a b. x -> (x %1 -> a) -> (x %1 -> b) -> With a b

Instances

Instances details

(Show a, Show b) => Show (With a b) Source Github #
Instance details Defined in Proarrow.Category.Instance.Linear Methods showsPrec :: Int -> With a b -> ShowS Github # show :: With a b -> String Github # showList :: [With a b] -> ShowS Github #
(Eq a, Eq b) => Eq (With a b) Source Github #
Instance details Defined in Proarrow.Category.Instance.Linear Methods (==) :: With a b -> With a b -> Bool Github # (/=) :: With a b -> With a b -> Bool Github #

urWith :: Ur (With a b) %1 -> (Ur a, Ur b) Source Github #

mkWith :: a -> b -> With a b Source Github #

type Not a = a %1 -> () Source Github #

not :: (Not b %1 -> Not a) %1 -> a %1 -> b Source Github #

not' :: (a %1 -> b) %1 -> Not b %1 -> Not a Source Github #

newtype Par a b Source Github #

Constructors

Par (Not (Not a, Not b))

mkPar :: a %1 -> b %1 -> Par a b Source Github #

pairFst :: (a, Par b c) %1 -> Par (a, b) c Source Github #

pairSnd :: (Par a b, c) %1 -> Par a (b, c) Source Github #

parAppL :: Par a b %1 -> Not a %1 -> b Source Github #

parAppR :: Par a b %1 -> Not b %1 -> a Source Github #

newtype Quest a Source Github #

Constructors

Quest (Not (Ur (Not a)))

notQuest :: Not (Quest a) %1 -> Ur (Not a) Source Github #

unitQuest :: a %1 -> Quest a Source Github #

multQuest :: Quest (Quest a) %1 -> Quest a Source Github #

questPar :: Par (Quest a) (Quest b) %1 -> Quest (Either a b) Source Github #

dn :: Not (Not a) %1 -> a Source Github #

Double negation is possible with linear functions, though using unsafeDupablePerformIO. Derived from https://gist.github.com/ant-arctica/7563282c57d9d1ce0c4520c543187932 TODO: only tested in GHCi, might get ruined by optimizations

unsafeLinear :: (a -> b) -> a %1 -> b Source Github #

unit :: 'L () ~> 'L (Par a (Not a)) Source Github #

counit :: 'L (Not a, a) ~> 'L () Source Github #

type (!~>) (p :: k -> k1 -> Type) (q :: k -> k1 -> Type) = forall (a :: k) (b :: k1). p a b %1 -> q a b Source Github #

data NegComp (p :: j +-> k) (q :: i +-> j) (a :: k) (c :: i) where Source Github #

Constructors

NegComp :: forall {j} {k} {i} (p :: j +-> k) (a :: k) (q :: i +-> j) (c :: i). (forall (b :: j). Par (p a b) (q b c)) -> NegComp p q a c

newtype Neg (p :: k -> k1 -> Type) (a :: k1) (b :: k) Source Github #

Constructors

Neg (Not (p b a))

getNeg :: forall {k1} {k2} p (a :: k2) (b :: k1). Neg p a b %1 -> Not (p b a) Source Github #

conv1 :: forall {k1} {k2} {k3} (p :: k1 +-> k2) (q :: k3 +-> k1) (a :: k2) (b :: k3). NegComp p q a b %1 -> Neg (Neg q :.: Neg p) a b Source Github #

conv2 :: forall {j} {i} {k} (q :: j -> i -> Type) (p :: k -> j -> Type) (a :: k) (b :: i). Neg (Neg q :.: Neg p) a b %1 -> NegComp p q a b Source Github #

asCocat :: forall {i} (p :: i -> i -> Type). ((Neg p :.: Neg p) !~> Neg p) -> p !~> NegComp p p Source Github #