License | BSD-style (see the file LICENSE) |
---|---|
Maintainer | sjoerd@w3future.com |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe |
Language | Haskell2010 |
- class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where
- type Exponential k y z :: *
- data ExpFunctor k = ExpFunctor
- type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite ((ProductFunctor (Presheaves k) :.: Tuple2 (Presheaves k) (Presheaves k) y) :.: YonedaEmbedding k)
- 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 => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z)
- 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)
- 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))
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.
type Exponential k y z :: * Source #
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 #
CartesianClosed (->) Source # | Exponentials in |
CartesianClosed Cat Source # | Exponentials in |
CartesianClosed Boolean Source # | Implication makes the Boolean category cartesian closed. |
Category k => CartesianClosed (Presheaves k) Source # | The category of presheaves on a category |
CartesianClosed (f (Fix f)) => CartesianClosed (Fix f) Source # |
|
data ExpFunctor k Source #
CartesianClosed k => Functor (ExpFunctor k) Source # | The exponential as a bifunctor. |
type Dom (ExpFunctor k) Source # | |
type Cod (ExpFunctor k) Source # | |
type (ExpFunctor k) :% (y, z) Source # | |
type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite ((ProductFunctor (Presheaves k) :.: Tuple2 (Presheaves k) (Presheaves k) y) :.: YonedaEmbedding k) Source #
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 => 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) 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 => 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) s Source #
contextComonadExtract :: CartesianClosed k => Obj k s -> Obj k a -> k (Context k s a) a Source #
contextComonadDuplicate :: CartesianClosed k => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a)) Source #