Data.Category.CartesianClosed

Documentation

type family Exponential k y z :: *

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

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

Methods

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

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

(^^^) :: k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k 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.

(HasTerminalObject (Presheaves k), HasBinaryProducts (Presheaves k), Category k) => CartesianClosed (Presheaves k)

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

data ExpFunctor k

Constructors

ExpFunctor

Instances

(Category (Dom (ExpFunctor k)), Category (Cod (ExpFunctor k)), CartesianClosed k) => Functor (ExpFunctor k)

The exponential as a bifunctor.

data Apply y z

Constructors

Apply

Instances

(Category (Dom (Apply y z)), Category (Cod (Apply y z)), 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 (Dom (ToTuple1 y z)), Category (Cod (ToTuple1 y z)), 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 (Dom (ToTuple2 y z)), Category (Cod (ToTuple2 y z)), Category y, Category z) => Functor (ToTuple2 y z)

ToTuple2 converts an object a to the functor Tuple2 a.

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

The product functor is left adjoint the the exponential functor.

curry :: CartesianClosed k => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k 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 k => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z

type State k s a = Exponential k s (BinaryProduct k a s)

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

stateMonadReturn :: CartesianClosed k => Obj k s -> Obj k a -> k a (State k s a)

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

type Context k s a = BinaryProduct k (Exponential k s a) s

contextComonadExtract :: CartesianClosed k => Obj k s -> Obj k a -> k (Context k s a) a

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