data-category-0.5.1.1: Category theory

Portability non-portable experimental sjoerd@w3future.com Safe-Inferred

Data.Category.CartesianClosed

Description

Synopsis

# Documentation

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

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

Associated Types

type Exponential k y z :: *Source

Methods

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

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

(^^^) :: k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)Source

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`.

data ExpFunctor k Source

Constructors

 ExpFunctor

Instances

 CartesianClosed k => Functor (ExpFunctor k) The exponential as a bifunctor.

data Apply y z Source

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 Source

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 Source

Constructors

 ToTuple2

Instances

 (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)Source

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

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) zSource

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

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

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

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

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

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