License	BSD-style (see the file LICENSE)
Maintainer	sjoerd@w3future.com
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Category.CartesianClosed

Description

Synopsis

class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where
- type Exponential k (y :: Kind k) (z :: Kind k) :: Kind k
- 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)
data ExpFunctor (k :: Type -> Type -> Type) = ExpFunctor
flip :: CartesianClosed k => Obj k a -> Obj k b -> Obj k c -> k (Exponential k a (Exponential k b c)) (Exponential k b (Exponential k a c))
type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite ((ProductFunctor (Presheaves k) :.: Tuple2 (Presheaves k) (Presheaves k) y) :.: YonedaEmbedding k)
pattern PshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z
curryAdj :: CartesianClosed k => Obj k y -> Adjunction k k (ProductFunctor k :.: Tuple2 k k y) (ExpFunctor k :.: Tuple1 (Op k) k y)
curry :: (CartesianClosed k, Kind k ~ Type) => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z)
uncurry :: (CartesianClosed k, Kind k ~ Type) => 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)
stateMonadReturn :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k a (State k s a)
stateMonadJoin :: (CartesianClosed k, Kind k ~ Type) => 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, Kind k ~ Type) => Obj k s -> Obj k a -> k (Context k s a) a
contextComonadDuplicate :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a))

Documentation

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

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

Associated Types

type Exponential k (y :: Kind k) (z :: Kind k) :: Kind k Source #

Methods

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

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

Instances details

CartesianClosed Boolean Source #	Implication makes the Boolean category cartesian closed.
Instance details Defined in Data.Category.Boolean Associated Types type Exponential Boolean y z :: Kind k Source # Methods apply :: forall (y :: k) (z :: k). Obj Boolean y -> Obj Boolean z -> Boolean (BinaryProduct Boolean (Exponential Boolean y z) y) z Source # tuple :: forall (y :: k) (z :: k). Obj Boolean y -> Obj Boolean z -> Boolean z (Exponential Boolean y (BinaryProduct Boolean z y)) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). Boolean z1 z2 -> Boolean y2 y1 -> Boolean (Exponential Boolean y1 z1) (Exponential Boolean y2 z2) Source #
CartesianClosed Unit Source #
Instance details Defined in Data.Category.CartesianClosed Associated Types type Exponential Unit y z :: Kind k Source # Methods apply :: forall (y :: k) (z :: k). Obj Unit y -> Obj Unit z -> Unit (BinaryProduct Unit (Exponential Unit y z) y) z Source # tuple :: forall (y :: k) (z :: k). Obj Unit y -> Obj Unit z -> Unit z (Exponential Unit y (BinaryProduct Unit z y)) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). Unit z1 z2 -> Unit y2 y1 -> Unit (Exponential Unit y1 z1) (Exponential Unit y2 z2) Source #
CartesianClosed (f (Fix f)) => CartesianClosed (Fix f :: Type -> Type -> Type) Source #	`Fix f` inherits its exponentials from `f (Fix f)`.
Instance details Defined in Data.Category.Fix Associated Types type Exponential (Fix f) y z :: Kind k Source # Methods apply :: forall (y :: k) (z :: k). Obj (Fix f) y -> Obj (Fix f) z -> Fix f (BinaryProduct (Fix f) (Exponential (Fix f) y z) y) z Source # tuple :: forall (y :: k) (z :: k). Obj (Fix f) y -> Obj (Fix f) z -> Fix f z (Exponential (Fix f) y (BinaryProduct (Fix f) z y)) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). Fix f z1 z2 -> Fix f y2 y1 -> Fix f (Exponential (Fix f) y1 z1) (Exponential (Fix f) y2 z2) Source #
Category k => CartesianClosed (Presheaves k :: Type -> Type -> Type) Source #	The category of presheaves on a category `C` is cartesian closed for any `C`.
Instance details Defined in Data.Category.CartesianClosed Associated Types type Exponential (Presheaves k) y z :: Kind k Source # Methods apply :: forall (y :: k0) (z :: k0). Obj (Presheaves k) y -> Obj (Presheaves k) z -> Presheaves k (BinaryProduct (Presheaves k) (Exponential (Presheaves k) y z) y) z Source # tuple :: forall (y :: k0) (z :: k0). Obj (Presheaves k) y -> Obj (Presheaves k) z -> Presheaves k z (Exponential (Presheaves k) y (BinaryProduct (Presheaves k) z y)) Source # (^^^) :: forall (z1 :: k0) (z2 :: k0) (y2 :: k0) (y1 :: k0). Presheaves k z1 z2 -> Presheaves k y2 y1 -> Presheaves k (Exponential (Presheaves k) y1 z1) (Exponential (Presheaves k) y2 z2) Source #
(Ord a, Bounded a) => CartesianClosed (Preorder a :: Type -> Type -> Type) Source #
Instance details Defined in Data.Category.Preorder Associated Types type Exponential (Preorder a) y z :: Kind k Source # Methods apply :: forall (y :: k) (z :: k). Obj (Preorder a) y -> Obj (Preorder a) z -> Preorder a (BinaryProduct (Preorder a) (Exponential (Preorder a) y z) y) z Source # tuple :: forall (y :: k) (z :: k). Obj (Preorder a) y -> Obj (Preorder a) z -> Preorder a z (Exponential (Preorder a) y (BinaryProduct (Preorder a) z y)) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). Preorder a z1 z2 -> Preorder a y2 y1 -> Preorder a (Exponential (Preorder a) y1 z1) (Exponential (Preorder a) y2 z2) Source #
CartesianClosed (->) Source #	Exponentials in `Hask` are functions.
Instance details Defined in Data.Category.CartesianClosed Associated Types type Exponential (->) y z :: Kind k Source # Methods apply :: forall (y :: k) (z :: k). Obj (->) y -> Obj (->) z -> BinaryProduct (->) (Exponential (->) y z) y -> z Source # tuple :: forall (y :: k) (z :: k). Obj (->) y -> Obj (->) z -> z -> Exponential (->) y (BinaryProduct (->) z y) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). (z1 -> z2) -> (y2 -> y1) -> Exponential (->) y1 z1 -> Exponential (->) y2 z2 Source #
CartesianClosed (LTE ('S n)) => CartesianClosed (LTE ('S ('S n)) :: Fin ('S ('S n)) -> Fin ('S ('S n)) -> Type) Source #
Instance details Defined in Data.Category.Fin Associated Types type Exponential (LTE ('S ('S n))) y z :: Kind k Source # Methods apply :: forall (y :: k) (z :: k). Obj (LTE ('S ('S n))) y -> Obj (LTE ('S ('S n))) z -> LTE ('S ('S n)) (BinaryProduct (LTE ('S ('S n))) (Exponential (LTE ('S ('S n))) y z) y) z Source # tuple :: forall (y :: k) (z :: k). Obj (LTE ('S ('S n))) y -> Obj (LTE ('S ('S n))) z -> LTE ('S ('S n)) z (Exponential (LTE ('S ('S n))) y (BinaryProduct (LTE ('S ('S n))) z y)) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). LTE ('S ('S n)) z1 z2 -> LTE ('S ('S n)) y2 y1 -> LTE ('S ('S n)) (Exponential (LTE ('S ('S n))) y1 z1) (Exponential (LTE ('S ('S n))) y2 z2) Source #
CartesianClosed (LTE ('S 'Z)) Source #
Instance details Defined in Data.Category.Fin Associated Types type Exponential (LTE ('S 'Z)) y z :: Kind k Source # Methods apply :: forall (y :: k) (z :: k). Obj (LTE ('S 'Z)) y -> Obj (LTE ('S 'Z)) z -> LTE ('S 'Z) (BinaryProduct (LTE ('S 'Z)) (Exponential (LTE ('S 'Z)) y z) y) z Source # tuple :: forall (y :: k) (z :: k). Obj (LTE ('S 'Z)) y -> Obj (LTE ('S 'Z)) z -> LTE ('S 'Z) z (Exponential (LTE ('S 'Z)) y (BinaryProduct (LTE ('S 'Z)) z y)) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). LTE ('S 'Z) z1 z2 -> LTE ('S 'Z) y2 y1 -> LTE ('S 'Z) (Exponential (LTE ('S 'Z)) y1 z1) (Exponential (LTE ('S 'Z)) y2 z2) Source #
CartesianClosed Cat Source #	Exponentials in `Cat` are the functor categories.
Instance details Defined in Data.Category.CartesianClosed Associated Types type Exponential Cat y z :: Kind k Source # Methods apply :: forall (y :: k) (z :: k). Obj Cat y -> Obj Cat z -> Cat (BinaryProduct Cat (Exponential Cat y z) y) z Source # tuple :: forall (y :: k) (z :: k). Obj Cat y -> Obj Cat z -> Cat z (Exponential Cat y (BinaryProduct Cat z y)) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). Cat z1 z2 -> Cat y2 y1 -> Cat (Exponential Cat y1 z1) (Exponential Cat y2 z2) Source #

data ExpFunctor (k :: Type -> Type -> Type) Source #

Constructors

ExpFunctor

Instances

Instances details

CartesianClosed k => Functor (ExpFunctor k) Source #	The exponential as a bifunctor.
Instance details Defined in Data.Category.CartesianClosed Associated Types type Dom (ExpFunctor k) :: Type -> Type -> Type Source # type Cod (ExpFunctor k) :: Type -> Type -> Type Source # type (ExpFunctor k) :% a Source # Methods (%) :: ExpFunctor k -> Dom (ExpFunctor k) a b -> Cod (ExpFunctor k) (ExpFunctor k :% a) (ExpFunctor k :% b) Source #
type Cod (ExpFunctor k) Source #
Instance details Defined in Data.Category.CartesianClosed type Cod (ExpFunctor k) = k
type Dom (ExpFunctor k) Source #
Instance details Defined in Data.Category.CartesianClosed type Dom (ExpFunctor k) = Op k :**: k
type (ExpFunctor k) :% (y, z) Source #
Instance details Defined in Data.Category.CartesianClosed type (ExpFunctor k) :% (y, z) = Exponential k y z

flip :: CartesianClosed k => Obj k a -> Obj k b -> Obj k c -> k (Exponential k a (Exponential k b c)) (Exponential k b (Exponential k a c)) Source #

type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite ((ProductFunctor (Presheaves k) :.: Tuple2 (Presheaves k) (Presheaves k) y) :.: YonedaEmbedding k) Source #

pattern PshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z Source #

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, Kind k ~ Type) => 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, Kind k ~ Type) => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z Source #

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, Kind k ~ Type) => Obj k s -> Obj k a -> k a (State k s a) Source #

stateMonadJoin :: (CartesianClosed k, Kind k ~ Type) => 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) s Source #

contextComonadExtract :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k (Context k s a) a Source #

contextComonadDuplicate :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a)) Source #