Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Instance.Linear

Synopsis

data LINEAR = L Type
data Linear (a :: LINEAR) (b :: LINEAR) where
- Linear :: forall a1 b1. {..} -> Linear ('L a1) ('L b1)
data Forget a (b :: LINEAR) where
- Forget :: forall a b1. (a -> b1) -> Forget a ('L b1)
data Ur a where
- Ur :: forall a. a -> Ur a
counitUr :: Ur a %1 -> a
dupUr :: Ur a %1 -> Ur (Ur a)
data Free (a :: LINEAR) b where
- Free :: forall a1 b. (a1 %1 -> Ur b) -> Free ('L a1) b
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)
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))
toPar :: (a, 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) %1 -> 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 Comments #

Constructors

L Type

Instances

Instances details

Monoidal LINEAR Source Comments #

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

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

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

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

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

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

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

SymMonoidal LINEAR Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

swap' :: forall (a :: LINEAR) (a' :: LINEAR) (b :: LINEAR) (b' :: LINEAR). (a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a') Source Comments #

CategoryOf LINEAR Source Comments #

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

HasBinaryCoproducts LINEAR Source Comments #

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

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

lft' :: forall (a :: LINEAR) (a' :: LINEAR) (b :: LINEAR). (a ~> a') -> Obj b -> a ~> (a' || b) Source Comments #

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

rgt' :: forall (a :: LINEAR) (b :: LINEAR) (b' :: LINEAR). Obj a -> (b ~> b') -> b ~> (a || b') Source Comments #

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

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

HasBinaryProducts LINEAR Source Comments #

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

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

fst' :: forall (a :: LINEAR) (a' :: LINEAR) (b :: LINEAR). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments #

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

snd' :: forall (a :: LINEAR) (b :: LINEAR) (b' :: LINEAR). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments #

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

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

StarAutonomous LINEAR Source Comments #

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

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

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

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

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

Closed LINEAR Source Comments #

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

curry' :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR). Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c) Source Comments #

uncurry' :: forall (b :: LINEAR) (c :: LINEAR) (a :: LINEAR). Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c Source Comments #

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

HasInitialObject LINEAR Source Comments #

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 Comments #

initiate' :: forall (a' :: LINEAR) (a :: LINEAR). (a' ~> a) -> (InitialObject :: LINEAR) ~> a Source Comments #

HasTerminalObject LINEAR Source Comments #

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 Comments #

terminate' :: forall (a :: LINEAR) (a' :: LINEAR). (a ~> a') -> a ~> (TerminalObject :: LINEAR) Source Comments #

Promonad Linear Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

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

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

MonoidalProfunctor Linear Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

par0 :: Linear (Unit :: LINEAR) (Unit :: LINEAR) Source Comments #

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

MonoidalProfunctor Forget Source Comments #

Forget is a lax monoidal functor

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

par0 :: Forget (Unit :: Type) (Unit :: LINEAR) Source Comments #

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

MonoidalProfunctor Free Source Comments #

Free is a lax monoidal functor

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

par0 :: Free (Unit :: LINEAR) (Unit :: Type) Source Comments #

par :: forall (x1 :: LINEAR) x2 (y1 :: LINEAR) y2. Free x1 x2 -> Free y1 y2 -> Free (x1 ** y1) (x2 ** y2) Source Comments #

Profunctor Linear Source Comments #

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 Comments #

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

Profunctor Free Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

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

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

Profunctor Forget Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

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

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

Representable Forget Source Comments #

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

index :: forall a (b :: LINEAR). Forget a b -> a ~> (Forget % b) Source Comments #

tabulate :: forall (b :: LINEAR) a. Ob b => (a ~> (Forget % b)) -> Forget a b Source Comments #

repMap :: forall (a :: LINEAR) (b :: LINEAR). (a ~> b) -> (Forget % a) ~> (Forget % b) Source Comments #

Representable Free Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

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

Methods

index :: forall (a :: LINEAR) b. Free a b -> a ~> (Free % b) Source Comments #

tabulate :: forall b (a :: LINEAR). Ob b => (a ~> (Free % b)) -> Free a b Source Comments #

repMap :: (a ~> b) -> (Free % a) ~> (Free % b) Source Comments #

Adjunction Free Forget Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

unit :: Ob a => (Forget :.: Free) a a Source Comments #

counit :: (Free :.: Forget) :~> ((~>) :: CAT LINEAR) Source Comments #

MonoidalProfunctor (RepCostar Free) Source Comments #

Free is also a colax monoidal functor

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

par0 :: RepCostar Free (Unit :: Type) (Unit :: LINEAR) Source Comments #

par :: forall x1 (x2 :: LINEAR) y1 (y2 :: LINEAR). RepCostar Free x1 x2 -> RepCostar Free y1 y2 -> RepCostar Free (x1 ** y1) (x2 ** y2) Source Comments #

MonoidalProfunctor (RepCostar Forget) Source Comments #

Forget is also a colax monoidal functor

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

par0 :: RepCostar Forget (Unit :: LINEAR) (Unit :: Type) Source Comments #

par :: forall (x1 :: LINEAR) x2 (y1 :: LINEAR) y2. RepCostar Forget x1 x2 -> RepCostar Forget y1 y2 -> RepCostar Forget (x1 ** y1) (x2 ** y2) Source Comments #

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

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

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

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

type Unit Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

type Unit = 'L ()

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

type (~>) = Linear

type InitialObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

type InitialObject = 'L Void

type TerminalObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

type TerminalObject = 'L Top

type Ob (a :: LINEAR) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

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

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

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 Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

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

type Free % (a :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

type Free % (a :: Type) = 'L (Ur a)

type UN 'L ('L a :: LINEAR) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

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

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

Instance details

Defined in Proarrow.Category.Instance.Linear

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

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

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 Comments #

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 Comments #

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 Comments #

Constructors

Linear
Fields :: forall a1 b1. { unLinear :: a1 %1 -> b1 } -> Linear ('L a1) ('L b1)

Instances

Instances details

Promonad Linear Source Comments #
Instance details Defined in Proarrow.Category.Instance.Linear Methods id :: forall (a :: LINEAR). Ob a => Linear a a Source Comments # (.) :: forall (b :: LINEAR) (c :: LINEAR) (a :: LINEAR). Linear b c -> Linear a b -> Linear a c Source Comments #
MonoidalProfunctor Linear Source Comments #
Instance details Defined in Proarrow.Category.Instance.Linear Methods par0 :: Linear (Unit :: LINEAR) (Unit :: LINEAR) Source Comments # par :: forall (x1 :: LINEAR) (x2 :: LINEAR) (y1 :: LINEAR) (y2 :: LINEAR). Linear x1 x2 -> Linear y1 y2 -> Linear (x1 y1) (x2 y2) Source Comments #
Profunctor Linear Source Comments #
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 Comments # (\\) :: forall (a :: LINEAR) (b :: LINEAR) r. ((Ob a, Ob b) => r) -> Linear a b -> r Source Comments #

data Forget a (b :: LINEAR) where Source Comments #

Constructors

Forget :: forall a b1. (a -> b1) -> Forget a ('L b1)

Instances

Instances details

MonoidalProfunctor Forget Source Comments #

Forget is a lax monoidal functor

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

par0 :: Forget (Unit :: Type) (Unit :: LINEAR) Source Comments #

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

Profunctor Forget Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

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

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

Representable Forget Source Comments #

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

index :: forall a (b :: LINEAR). Forget a b -> a ~> (Forget % b) Source Comments #

tabulate :: forall (b :: LINEAR) a. Ob b => (a ~> (Forget % b)) -> Forget a b Source Comments #

repMap :: forall (a :: LINEAR) (b :: LINEAR). (a ~> b) -> (Forget % a) ~> (Forget % b) Source Comments #

Adjunction Free Forget Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

unit :: Ob a => (Forget :.: Free) a a Source Comments #

counit :: (Free :.: Forget) :~> ((~>) :: CAT LINEAR) Source Comments #

MonoidalProfunctor (RepCostar Forget) Source Comments #

Forget is also a colax monoidal functor

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

par0 :: RepCostar Forget (Unit :: LINEAR) (Unit :: Type) Source Comments #

par :: forall (x1 :: LINEAR) x2 (y1 :: LINEAR) y2. RepCostar Forget x1 x2 -> RepCostar Forget y1 y2 -> RepCostar Forget (x1 ** y1) (x2 ** y2) Source Comments #

type Forget % (a :: LINEAR) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

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

data Ur a where Source Comments #

Constructors

Ur :: forall a. a -> Ur a

Instances

Instances details

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

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

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

data Free (a :: LINEAR) b where Source Comments #

Constructors

Free :: forall a1 b. (a1 %1 -> Ur b) -> Free ('L a1) b

Instances

Instances details

MonoidalProfunctor Free Source Comments #

Free is a lax monoidal functor

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

par0 :: Free (Unit :: LINEAR) (Unit :: Type) Source Comments #

par :: forall (x1 :: LINEAR) x2 (y1 :: LINEAR) y2. Free x1 x2 -> Free y1 y2 -> Free (x1 ** y1) (x2 ** y2) Source Comments #

Profunctor Free Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

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

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

Representable Free Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

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

Methods

index :: forall (a :: LINEAR) b. Free a b -> a ~> (Free % b) Source Comments #

tabulate :: forall b (a :: LINEAR). Ob b => (a ~> (Free % b)) -> Free a b Source Comments #

repMap :: (a ~> b) -> (Free % a) ~> (Free % b) Source Comments #

Adjunction Free Forget Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

unit :: Ob a => (Forget :.: Free) a a Source Comments #

counit :: (Free :.: Forget) :~> ((~>) :: CAT LINEAR) Source Comments #

MonoidalProfunctor (RepCostar Free) Source Comments #

Free is also a colax monoidal functor

Instance details

Defined in Proarrow.Category.Instance.Linear

Methods

par0 :: RepCostar Free (Unit :: Type) (Unit :: LINEAR) Source Comments #

par :: forall x1 (x2 :: LINEAR) y1 (y2 :: LINEAR). RepCostar Free x1 x2 -> RepCostar Free y1 y2 -> RepCostar Free (x1 ** y1) (x2 ** y2) Source Comments #

type Free % (a :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Linear

type Free % (a :: Type) = 'L (Ur a)

data Top where Source Comments #

Constructors

Top :: forall a. a -> Top

data With a b where Source Comments #

Constructors

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) Source Comments #

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

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

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

newtype Par a b Source Comments #

Constructors

Par (Not (Not a, Not b))

toPar :: (a, b) %1 -> Par a b Source Comments #

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

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

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

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

newtype Quest a Source Comments #

Constructors

Quest (Not (Ur (Not a)))

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

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

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

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

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

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) %1 -> a %1 -> b Source Comments #

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

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

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

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

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 Comments #

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 Comments #

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 Comments #

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 Comments #

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