Data.Category.CartesianClosed

Documentation

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

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

Associated Types

type Exponential k y z :: *

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.

Category k => CartesianClosed (Presheaves k)

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

CartesianClosed (f (Fix f)) => CartesianClosed (Fix f)

Fix f inherits its exponentials from f (Fix f).

data ExpFunctor k

Constructors

ExpFunctor

Instances

CartesianClosed k => Functor (ExpFunctor k)

The exponential as a bifunctor.

data Apply c1 c2

Constructors

Apply

Instances

(Category c1, Category c2) => Functor (Apply c1 c2)

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

data Tuple c1 c2

Constructors

Tuple

Instances

(Category c1, Category c2) => Functor (Tuple c1 c2)

Tuple converts an object a to the functor Tuple1 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))