Data.Category.CartesianClosed

Documentation

type family Exponential (~>) y z :: *

class (HasTerminalObject ~>, HasBinaryProducts ~>) => CartesianClosed (~>) where

A category is cartesian closed if it has all products and exponentials for all objects.

Methods

apply :: Obj ~> y -> Obj ~> z -> BinaryProduct ~> (Exponential ~> y z) y ~> z

tuple :: Obj ~> y -> Obj ~> z -> z ~> Exponential ~> y (BinaryProduct ~> z y)

(^^^) :: (z1 ~> z2) -> (y2 ~> y1) -> Exponential ~> y1 z1 ~> Exponential ~> y2 z2

Instances

CartesianClosed (->)

Exponentials in Hask are functions.

CartesianClosed Cat

Exponentials in Cat are the functor categories.

CartesianClosed Boolean

Implication makes the Boolean category cartesian closed.

Category ~> => CartesianClosed (Presheaves ~>)

The category of presheaves on a category C is cartesian closed for any C.

data ExpFunctor (~>)

Constructors

ExpFunctor

Instances

CartesianClosed ~> => Functor (ExpFunctor ~>)

The exponential as a bifunctor.

data Apply y z

Constructors

Apply

Instances

(Category y, Category z) => Functor (Apply y z)

Apply is a bifunctor, Apply :% (f, a) applies f to a, i.e. f :% a.

data ToTuple1 y z

Constructors

ToTuple1

Instances

(Category y, Category z) => Functor (ToTuple1 y z)

ToTuple1 converts an object a to the functor Tuple1 a.

data ToTuple2 y z

Constructors

ToTuple2

Instances

(Category y, Category z) => Functor (ToTuple2 y z)

ToTuple2 converts an object a to the functor Tuple2 a.

curryAdj :: CartesianClosed ~> => Obj ~> y -> Adjunction ~> ~> (ProductFunctor ~> :.: Tuple2 ~> ~> y) (ExpFunctor ~> :.: Tuple1 (Op ~>) ~> y)

The product functor is left adjoint the the exponential functor.

curry :: CartesianClosed ~> => Obj ~> x -> Obj ~> y -> Obj ~> z -> (BinaryProduct ~> x y ~> z) -> x ~> Exponential ~> y z

From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions, generalized to any cartesian closed category.

uncurry :: CartesianClosed ~> => Obj ~> x -> Obj ~> y -> Obj ~> z -> (x ~> Exponential ~> y z) -> BinaryProduct ~> x y ~> z

type State (~>) s a = Exponential ~> s (BinaryProduct ~> a s)

From every adjunction we get a monad, in this case the State monad.

stateMonadReturn :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> a ~> State ~> s a

stateMonadJoin :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> State ~> s (State ~> s a) ~> State ~> s a

type Context (~>) s a = BinaryProduct ~> (Exponential ~> s a) s

contextComonadExtract :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> Context ~> s a ~> a

contextComonadDuplicate :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> Context ~> s a ~> Context ~> s (Context ~> s a)