Portability | non-portable |
---|---|
Stability | experimental |
Maintainer | sjoerd@w3future.com |
- type family Exponential (~>) y z :: *
- class (HasTerminalObject ~>, HasBinaryProducts ~>) => CartesianClosed (~>) where
- apply :: Obj ~> y -> Obj ~> z -> BinaryProduct ~> (Exponential ~> y z) y ~> z
- tuple :: Obj ~> y -> Obj ~> z -> z ~> Exponential ~> y (BinaryProduct ~> z y)
- (^^^) :: (z1 ~> z2) -> (y2 ~> y1) -> Exponential ~> y1 z1 ~> Exponential ~> y2 z2
- data ExpFunctor (~>) = ExpFunctor
- data Apply y z = Apply
- data ToTuple1 y z = ToTuple1
- data ToTuple2 y z = ToTuple2
- curryAdj :: CartesianClosed ~> => Obj ~> y -> Adjunction ~> ~> (ProductFunctor ~> :.: Tuple2 ~> ~> y) (ExpFunctor ~> :.: Tuple1 (Op ~>) ~> y)
- curry :: CartesianClosed ~> => Obj ~> x -> Obj ~> y -> Obj ~> z -> (BinaryProduct ~> x y ~> z) -> x ~> Exponential ~> y z
- uncurry :: CartesianClosed ~> => Obj ~> x -> Obj ~> y -> Obj ~> z -> (x ~> Exponential ~> y z) -> BinaryProduct ~> x y ~> z
- type State (~>) s a = Exponential ~> s (BinaryProduct ~> a s)
- stateMonadReturn :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> a ~> State ~> s a
- stateMonadJoin :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> State ~> s (State ~> s a) ~> State ~> s a
- type Context (~>) s a = BinaryProduct ~> (Exponential ~> s a) s
- contextComonadExtract :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> Context ~> s a ~> a
- contextComonadDuplicate :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> Context ~> s a ~> Context ~> s (Context ~> s a)
Documentation
type family Exponential (~>) y z :: *Source
class (HasTerminalObject ~>, HasBinaryProducts ~>) => CartesianClosed (~>) whereSource
A category is cartesian closed if it has all products and exponentials for all objects.
apply :: Obj ~> y -> Obj ~> z -> BinaryProduct ~> (Exponential ~> y z) y ~> zSource
tuple :: Obj ~> y -> Obj ~> z -> z ~> Exponential ~> y (BinaryProduct ~> z y)Source
(^^^) :: (z1 ~> z2) -> (y2 ~> y1) -> Exponential ~> y1 z1 ~> Exponential ~> y2 z2Source
CartesianClosed (->) | Exponentials in |
CartesianClosed Cat | Exponentials in |
CartesianClosed Boolean | Implication makes the Boolean category cartesian closed. |
Category ~> => CartesianClosed (Presheaves ~>) | The category of presheaves on a category |
data ExpFunctor (~>) Source
CartesianClosed ~> => Functor (ExpFunctor ~>) | The exponential as a bifunctor. |
curryAdj :: CartesianClosed ~> => Obj ~> y -> Adjunction ~> ~> (ProductFunctor ~> :.: Tuple2 ~> ~> y) (ExpFunctor ~> :.: Tuple1 (Op ~>) ~> y)Source
The product functor is left adjoint the the exponential functor.
curry :: CartesianClosed ~> => Obj ~> x -> Obj ~> y -> Obj ~> z -> (BinaryProduct ~> x y ~> z) -> x ~> Exponential ~> y zSource
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 ~> => Obj ~> x -> Obj ~> y -> Obj ~> z -> (x ~> Exponential ~> y z) -> BinaryProduct ~> x y ~> zSource
type State (~>) s a = Exponential ~> s (BinaryProduct ~> a s)Source
From every adjunction we get a monad, in this case the State monad.
stateMonadReturn :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> a ~> State ~> s aSource
stateMonadJoin :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> State ~> s (State ~> s a) ~> State ~> s aSource
type Context (~>) s a = BinaryProduct ~> (Exponential ~> s a) sSource
contextComonadExtract :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> Context ~> s a ~> aSource
contextComonadDuplicate :: CartesianClosed ~> => Obj ~> s -> Obj ~> a -> Context ~> s a ~> Context ~> s (Context ~> s a)Source