Safe Haskell	None
Language	GHC2024

Proarrow.Category.Monoidal.Closed

Description

Closed monoidal categories: Closed provides the internal hom a ~~> b, right adjoint to tensoring, with curry, apply and functoriality (^^^). Also defines cartesian closed (CCC) and bicartesian closed (BiCCC) categories.

Synopsis

class Monoidal k => Closed k where
- type (a :: k) ~~> (b :: k) :: k
- withObExp :: forall (a :: k) (b :: k) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r
- curry :: forall (a :: k) (b :: k) (c :: k). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c)
- apply :: forall (a :: k) (b :: k). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b
- (^^^) :: forall (a :: k) (b :: k) (x :: k) (y :: k). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
uncurry :: forall {k} (b :: k) (c :: k) (a :: k). (Closed k, Ob b, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c
curryS :: forall {k} (b :: k) (c :: k) (a :: k). Closed k => ('[a, b] ~> '[c]) -> '[a] ~> '[b ~~> c]
curryS' :: forall {k} (as :: [k]) (c :: k) (b :: k). (Closed k, Ob as, Ob b) => ((as ** '[b]) ~> '[c]) -> as ~> '[b ~~> c]
applyS :: forall {k} (a :: k) (b :: k). (Closed k, Ob a, Ob b) => '[a ~~> b, a] ~> '[b]
uncurryS :: forall {k} (b :: k) (c :: k) (a :: k). (Closed k, Ob b, Ob c) => ('[a] ~> '[b ~~> c]) -> '[a, b] ~> '[c]
uncurryS' :: forall {k} (as :: [k]) (b :: k) (c :: k). (Closed k, Ob b, Ob c) => (as ~> '[b ~~> c]) -> (as ** '[b]) ~> '[c]
compS :: forall {k} (a :: k) (b :: k) (c :: k). (Closed k, Ob a, Ob b, Ob c) => '[b ~~> c, a ~~> b] ~> '[a ~~> c]
comp :: forall {k} (a :: k) (b :: k) (c :: k). (Closed k, Ob a, Ob b, Ob c) => ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)
mkExponentialS :: forall {k} (a :: k) (b :: k). Closed k => ('[a] ~> '[b]) -> ('[] :: [k]) ~> '[a ~~> b]
mkExponential :: forall {k} (a :: k) (b :: k). Closed k => (a ~> b) -> (Unit :: k) ~> (a ~~> b)
lowerS :: forall {k} (a :: k) (b :: k). (Closed k, Ob a, Ob b) => (('[] :: [k]) ~> '[a ~~> b]) -> '[a] ~> '[b]
lower :: forall {k} (a :: k) (b :: k). (Closed k, Ob a, Ob b) => ((Unit :: k) ~> (a ~~> b)) -> a ~> b
toEl :: forall {k} (a :: k). (Closed k, Ob a) => a ~> ((Unit :: k) ~~> a)
data family ExpRep :: (OPPOSITE k, k) +-> k
data family Not (r :: k) :: OPPOSITE k +-> k
data family Exp (m :: k) :: k +-> k
swapClosed :: forall {k} (c :: k) (a :: k) (b :: k). (Closed k, SymMonoidal k, Ob b, Ob c) => (a ~> (b ~~> c)) -> b ~> (a ~~> c)
data family (a :: k) --> (b :: k) :: k
type ClosedStructures = '[Monoidal, Closed]

Documentation

class Monoidal k => Closed k where Source Github #

A (right) closed monoidal category: every b ~~> c is an internal hom, right adjoint to tensoring with b. curry and uncurry witness the adjunction Hom(a ** b, c) ≅ Hom(a, b ~~> c).

Laws:

curry and uncurry are mutually inverse: uncurry (curry f) = f and curry (uncurry g) = g
and natural in all three variables: for f :: a' ~> a, g :: b' ~> b, h :: c ~> c', curry . dimap (f ** g) h = dimap f (h ^^^ g) . curry

Together these say curry is a natural isomorphism, which also forces the familiar apply . (curry f ** id) = f. The exponential is thereby functorial: (^^^) is contravariant in its second argument and covariant in its first.

Checked by testClosed.

Minimal complete definition

withObExp, curry, apply

Associated Types

type (a :: k) ~~> (b :: k) :: k infixr 2 Source Github #

The internal hom (exponential) object.

Methods

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

Recovers Ob (a ~~> b) from the objecthood of the ends.

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

Transposes an arrow out of a tensor into one into an exponential.

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

Evaluation: the counit of the adjunction.

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

The exponential's action on arrows: covariant in the result, contravariant in the argument.

Instances

Instances details

Closed Nat Source Github #

Instance details

Defined in Proarrow.Category.Instance.ZX

Associated Types

type (x :: Nat) ~~> (y :: Nat)
Instance details Defined in Proarrow.Category.Instance.ZX type (x :: Nat) ~~> (y :: Nat) = ExpSA x y

Methods

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

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

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

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

Closed BOOL Source Github #

Implication is the internal hom of the walking arrow: a ~~> b is BoolLeq a b.

Instance details

Defined in Proarrow.Category.Monoidal.Closed

Associated Types

type (a :: BOOL) ~~> (b :: BOOL)
Instance details Defined in Proarrow.Category.Monoidal.Closed type (a :: BOOL) ~~> (b :: BOOL) = BoolLeq a b

Methods

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

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

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

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

Closed CONSTRAINT Source Github #

Instance details

Defined in Proarrow.Category.Instance.Constraint

Associated Types

type (a :: CONSTRAINT) ~~> (b :: CONSTRAINT)
Instance details Defined in Proarrow.Category.Instance.Constraint type (a :: CONSTRAINT) ~~> (b :: CONSTRAINT) = 'CNSTRNT (UN 'CNSTRNT a :=> UN 'CNSTRNT b)

Methods

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

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

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

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

Closed FINHASK Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinHask

Associated Types

type (a :: FINHASK) ~~> (b :: FINHASK)
Instance details Defined in Proarrow.Category.Instance.FinHask type (a :: FINHASK) ~~> (b :: FINHASK) = 'FH (FinHask a b)

Methods

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

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

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

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

Closed FINREL Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinRel

Associated Types

type (x :: FINREL) ~~> (y :: FINREL)
Instance details Defined in Proarrow.Category.Instance.FinRel type (x :: FINREL) ~~> (y :: FINREL) = ExpSA x y

Methods

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

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

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

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

Closed FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type ('FS a :: FINSET) ~~> ('FS b :: FINSET)
Instance details Defined in Proarrow.Category.Instance.FinSet type ('FS a :: FINSET) ~~> ('FS b :: FINSET) = 'FS (Exp b a)

Methods

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

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

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

(^^^) :: forall (a :: FINSET) (b :: FINSET) (x :: FINSET) (y :: FINSET). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) 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 #

Closed DOT Source Github #

Instance details

Defined in Proarrow.Tools.Diagrams.Dot

Associated Types

type (a :: DOT) ~~> (b :: DOT)
Instance details Defined in Proarrow.Tools.Diagrams.Dot type (a :: DOT) ~~> (b :: DOT) = ExpHG a b

Methods

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

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

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

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

Closed SVG Source Github #

The exponential is the *-autonomous one, Dual (a ** Dual b), so curried wires show as duals.

Instance details

Defined in Proarrow.Tools.Diagrams.Svg

Associated Types

type (a :: SVG) ~~> (b :: SVG)
Instance details Defined in Proarrow.Tools.Diagrams.Svg type (a :: SVG) ~~> (b :: SVG) = ExpSA a b

Methods

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

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

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

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

Closed () Source Github #

Instance details

Defined in Proarrow.Category.Monoidal.Closed

Associated Types

type '() ~~> '()
Instance details Defined in Proarrow.Category.Monoidal.Closed type '() ~~> '() = '()

Methods

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

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

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

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

Closed Type Source Github #

Instance details

Defined in Proarrow.Category.Monoidal.Closed

Associated Types

type (a :: Type) ~~> (b :: Type)
Instance details Defined in Proarrow.Category.Monoidal.Closed type (a :: Type) ~~> (b :: Type) = a -> b

Methods

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

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

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

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

(HasPushouts k, HasCoproducts k) => Closed (COSPAN k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cospan

Methods

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

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

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

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

TracedMonoidal k => Closed (INT k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

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

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

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

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

Num a => Closed (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

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

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

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

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

(HasPullbacks k, HasProducts k) => Closed (SPAN k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Span

Methods

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

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

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

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

(CategoryOf j, CategoryOf k, HasTerminalObject (SUBCAT ob), HasBinaryProducts (SUBCAT ob), forall (p :: j +-> k) (q :: j +-> k). (ob p, ob q) => IsObProd ob p q, forall (p :: j +-> k) (q :: j +-> k). (ob p, ob q) => IsObExp ob p q) => Closed (PROD (SUBCAT ob)) Source Github #

And then the subcategory is closed, with the ambient exponential and nothing of its own, just as its products are the ambient ones. FINITARY j k is one instance, SHEAVES another. For the first, a hom-set of natural transformations is finitary. For the second, an internal hom into a sheaf is a sheaf.

Instance details

Defined in Proarrow.Profunctor.Instance.Exponential

Methods

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

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

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

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

(CategoryOf j, CategoryOf k) => Closed (PROD (j +-> k)) Source Github #

Instance details

Defined in Proarrow.Profunctor.Instance.Exponential

Methods

withObExp :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r Source Github #

curry :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (c :: PROD (j +-> k)). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) Source Github #

apply :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Github #

(^^^) :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (x :: PROD (j +-> k)) (y :: PROD (j +-> k)). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Github #

CategoryOf k1 => Closed (PROD (k1 -> Type)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Nat

Methods

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

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

apply :: forall (a :: PROD (k1 -> Type)) (b :: PROD (k1 -> Type)). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Github #

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

Closed (KLEISLI (Cont r)) Source Github #

Instance details

Defined in Proarrow.Promonad.Cont

Methods

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

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

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

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

CommutativeMonoid m => Closed (MONOID m) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Monoid

Methods

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

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

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

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

(Monoidal j, Monoidal k) => Closed (j +-> k) Source Github #

Instance details

Defined in Proarrow.Profunctor.Instance.Day

Methods

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

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

apply :: forall (a :: j +-> k) (b :: j +-> k). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Github #

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

(Closed j, Closed k) => Closed (j, k) Source Github #

Instance details

Defined in Proarrow.Category.Monoidal.Closed

Methods

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

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

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

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

Closed (Type -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Nat

Associated Types

type (j :: Type -> Type) ~~> (h :: Type -> Type)
Instance details Defined in Proarrow.Category.Instance.Nat type (j :: Type -> Type) ~~> (h :: Type -> Type) = Ran j h

Methods

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

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

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

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

Elems ClosedStructures cs => Closed (FREE cs p) Source Github #

Instance details

Defined in Proarrow.Category.Monoidal.Closed

Methods

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

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

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

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

uncurry :: forall {k} (b :: k) (c :: k) (a :: k). (Closed k, Ob b, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c Source Github #

curryS :: forall {k} (b :: k) (c :: k) (a :: k). Closed k => ('[a, b] ~> '[c]) -> '[a] ~> '[b ~~> c] Source Github #

curryS' :: forall {k} (as :: [k]) (c :: k) (b :: k). (Closed k, Ob as, Ob b) => ((as ** '[b]) ~> '[c]) -> as ~> '[b ~~> c] Source Github #

applyS :: forall {k} (a :: k) (b :: k). (Closed k, Ob a, Ob b) => '[a ~~> b, a] ~> '[b] Source Github #

uncurryS :: forall {k} (b :: k) (c :: k) (a :: k). (Closed k, Ob b, Ob c) => ('[a] ~> '[b ~~> c]) -> '[a, b] ~> '[c] Source Github #

uncurryS' :: forall {k} (as :: [k]) (b :: k) (c :: k). (Closed k, Ob b, Ob c) => (as ~> '[b ~~> c]) -> (as ** '[b]) ~> '[c] Source Github #

compS :: forall {k} (a :: k) (b :: k) (c :: k). (Closed k, Ob a, Ob b, Ob c) => '[b ~~> c, a ~~> b] ~> '[a ~~> c] Source Github #

comp :: forall {k} (a :: k) (b :: k) (c :: k). (Closed k, Ob a, Ob b, Ob c) => ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c) Source Github #

mkExponentialS :: forall {k} (a :: k) (b :: k). Closed k => ('[a] ~> '[b]) -> ('[] :: [k]) ~> '[a ~~> b] Source Github #

mkExponential :: forall {k} (a :: k) (b :: k). Closed k => (a ~> b) -> (Unit :: k) ~> (a ~~> b) Source Github #

lowerS :: forall {k} (a :: k) (b :: k). (Closed k, Ob a, Ob b) => (('[] :: [k]) ~> '[a ~~> b]) -> '[a] ~> '[b] Source Github #

lower :: forall {k} (a :: k) (b :: k). (Closed k, Ob a, Ob b) => ((Unit :: k) ~> (a ~~> b)) -> a ~> b Source Github #

toEl :: forall {k} (a :: k). (Closed k, Ob a) => a ~> ((Unit :: k) ~~> a) Source Github #

data family ExpRep :: (OPPOSITE k, k) +-> k Source Github #

Instances

Instances details

Closed k => FunctorForRep (ExpRep :: (OPPOSITE k, k) +-> k) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Closed Methods fmap :: forall (a :: (OPPOSITE k, k)) (b :: (OPPOSITE k, k)). (a ~> b) -> ((ExpRep :: (OPPOSITE k, k) +-> k) @ a) ~> ((ExpRep :: (OPPOSITE k, k) +-> k) @ b) Source Github #
type (ExpRep :: (OPPOSITE k, k) +-> k) @ ('('OP a, b) :: (OPPOSITE k, k)) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Closed type (ExpRep :: (OPPOSITE k, k) +-> k) @ ('('OP a, b) :: (OPPOSITE k, k)) = a ~~> b

data family Not (r :: k) :: OPPOSITE k +-> k Source Github #

Instances

Instances details

(Closed k, Ob r) => FunctorForRep (Not r :: OPPOSITE k +-> k) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Closed Methods fmap :: forall (a :: OPPOSITE k) (b :: OPPOSITE k). (a ~> b) -> (Not r @ a) ~> (Not r @ b) Source Github #
(Closed k, SymMonoidal k, Ob r) => Corepresentable (Rep (Not r) :: k -> OPPOSITE k -> Type) Source Github #	The Op-Op adjunction, giving rise to the continuation monad.
Instance details Defined in Proarrow.Category.Monoidal.Closed Methods coindex :: forall (a :: k) (b :: OPPOSITE k). Rep (Not r) a b -> (Rep (Not r) %% a) ~> b Source Github # cotabulate :: forall (a :: k) (b :: OPPOSITE k). Ob a => ((Rep (Not r) %% a) ~> b) -> Rep (Not r) a b Source Github # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Rep (Not r) %% a) ~> (Rep (Not r) %% b) Source Github # corepUniv :: forall (a :: k). Ob a => Rep (Not r) a (Rep (Not r) %% a) Source Github #
type (Rep (Not r) :: k -> OPPOSITE k -> Type) %% (a :: k) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Closed type (Rep (Not r) :: k -> OPPOSITE k -> Type) %% (a :: k) = 'OP (a ~~> r)
type (Not r :: OPPOSITE k +-> k) @ ('OP a :: OPPOSITE k) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Closed type (Not r :: OPPOSITE k +-> k) @ ('OP a :: OPPOSITE k) = a ~~> r

data family Exp (m :: k) :: k +-> k Source Github #

The "reader"/exponential-by-m functor, covariant unlike Not (which fixes the codomain).

Instances

Instances details

(Closed k, SymMonoidal k, Ob m) => Strong (Tensor :: k -> (k, k) -> Type) (Rep (Exp m) :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Monoid Methods act :: forall (a :: k) (x :: k) (y :: k). Ob a => Rep (Exp m) x y -> Rep (Exp m) (Act (Tensor :: k -> (k, k) -> Type) a x) (Act (Tensor :: k -> (k, k) -> Type) a y) Source Github #
(Closed k, Ob m) => FunctorForRep (Exp m :: k +-> k) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Closed Methods fmap :: forall (a :: k) (b :: k). (a ~> b) -> (Exp m @ a) ~> (Exp m @ b) Source Github #
(Closed k, SymMonoidal k, Comonoid m) => MonoidalProfunctor (Rep (Exp m) :: k -> k -> Type) Source Github #	The exponential by a comonoid, `m ~~> -`, is an applicative functor (the reader applicative): `pure` discards the argument with the counit and `*` duplicates it with the comultiplication. Rendered on `Rep (Exp m)` (legs `a ~> (m ~~> b)`) this is a `StrongDistributiveProfunctor`, so a `Grate` is a `Kaleidoscope`.
Instance details Defined in Proarrow.Monoid Methods one :: Rep (Exp m) (Unit :: k) (Unit :: k) Source Github # () :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k). Rep (Exp m) x1 x2 -> Rep (Exp m) y1 y2 -> Rep (Exp m) (x1 y1) (x2 ** y2) Source Github #
(Closed k, Ob d) => GlassFl (Rep (Exp d) :: k -> k -> Type) (Corep (Exp d) :: k -> k -> Type) Source Github #	The exponential pair, a grate witness: the source is ignored, and the consumer is fed the selector `\s -> h s d` for each point `d` of the exponent.
Instance details Defined in Proarrow.Optic.Glass Methods glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k). CCC k => Rep (Exp d) s a -> Corep (Exp d) b t -> (s && Mod s a b) ~> t Source Github #
(Closed k, SymMonoidal k, HasCoproducts k, Comonoid m) => GrateFl (Rep (Exp m) :: k -> k -> Type) (Corep (Exp m) :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Grate Methods zipWithP :: forall (s :: k) (a :: k) (b :: k) (t :: k). (Closed k, SymMonoidal k) => Rep (Exp m) s a -> Corep (Exp m) b t -> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t Source Github #
(Closed k, SymMonoidal k, HasCoproducts k, Comonoid m) => CotravFl (Rep (Exp m) :: k -> k -> Type) (Corep (Exp m) :: k -> k -> Type) Source Github #	The exponential pair for a comonoid exponent: `m ~~> -` is the reader applicative. So every `Grate` is a kaleidoscope.
Instance details Defined in Proarrow.Optic.Kaleidoscope Methods cotravP :: forall r (s :: k) (a :: k) (b :: k) (t :: k). Cotraversable r => Rep (Exp m) s a -> Corep (Exp m) b t -> r a b -> r s t Source Github #
(Closed k, SymMonoidal k, HasCoproducts k, Comonoid m) => KaleidoFl (Rep (Exp m) :: k -> k -> Type) (Corep (Exp m) :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Kaleidoscope Methods kaleidoP :: forall r (s :: k) (a :: k) (b :: k) (t :: k). Kaleidoscopic r => Rep (Exp m) s a -> Corep (Exp m) b t -> r a b -> r s t Source Github #
(Closed k, Ob m) => SetterFl (Rep (Exp m) :: k -> k -> Type) (Corep (Exp m) :: k -> k -> Type) Source Github #	The grate witness is a setter witness: map under the exponential. The `Closed` structure this needs rides in the instance context, not in `overP`'s own (weaker) constraint.
Instance details Defined in Proarrow.Optic.Setter Methods overP :: forall (s :: k) (a :: k) (b :: k) (t :: k). Rep (Exp m) s a -> Corep (Exp m) b t -> (a ~> b) -> s ~> t Source Github #
(Closed k, HasCoproducts k, Comonoid m) => Strong (CoprodAction :: k -> (COPROD k, k) -> Type) (Rep (Exp m) :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Monoid Methods act :: forall (a :: COPROD k) (x :: k) (y :: k). Ob a => Rep (Exp m) x y -> Rep (Exp m) (Act (CoprodAction :: k -> (COPROD k, k) -> Type) a x) (Act (CoprodAction :: k -> (COPROD k, k) -> Type) a y) Source Github #
(Closed k, HasCoproducts k, Ob m) => MonoidalProfunctor (Coprod (Rep (Exp m)) :: COPROD k -> COPROD k -> Type) Source Github #
Instance details Defined in Proarrow.Monoid Methods one :: Coprod (Rep (Exp m)) (Unit :: COPROD k) (Unit :: COPROD k) Source Github # () :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k) (y2 :: COPROD k). Coprod (Rep (Exp m)) x1 x2 -> Coprod (Rep (Exp m)) y1 y2 -> Coprod (Rep (Exp m)) (x1 y1) (x2 ** y2) Source Github #
type (Exp m :: k +-> k) @ (a :: k) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Closed type (Exp m :: k +-> k) @ (a :: k) = m ~~> a

swapClosed :: forall {k} (c :: k) (a :: k) (b :: k). (Closed k, SymMonoidal k, Ob b, Ob c) => (a ~> (b ~~> c)) -> b ~> (a ~~> c) Source Github #

data family (a :: k) --> (b :: k) :: k Source Github #

Instances

Instances details

(IsFreeOb a, IsFreeOb b, Elems ClosedStructures cs) => IsFreeOb (a --> b :: FREE cs p) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Closed Methods lowerOb :: forall k' (f :: k +-> k') r. (Representable f, All cs k') => (Ob (Lower f (a --> b)) => r) -> r Source Github #
type Lower (f :: k +-> k') (a --> b :: FREE cs p) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Closed type Lower (f :: k +-> k') (a --> b :: FREE cs p) = Lower f a ~~> Lower f b

type ClosedStructures = '[Monoidal, Closed] Source Github #

The structures the free category needs for Closed, and those its laws are stated for.