data-category-0.5.1: Category theory

Portabilitynon-portable
Stabilityexperimental
Maintainersjoerd@w3future.com
Safe HaskellSafe-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.

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

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 Source

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 Source

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 Source

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