Copyright | (c) 2013 Justus Sagemüller |
---|---|
License | GPL v3 (see COPYING) |
Maintainer | (@) sagemueller $ geo.uni-koeln.de |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
Haskell's Arrow
s, going back to [Hughes 2000], combine multiple ideas from
category theory:
- They expand upon cartesian categories, by offering ways to combine arrows between simple objects to composite ones working on tuples (i.e. products) thereof.
- They constitute a "profunctor" interface, allowing to "
fmap
" both covariantly over the second parameter, as well as contravariantly over the first. As in case of Control.Functor.Constrained, we wish the underlying category to fmap from not to be limited to Hask, soArrow
also has an extra parameter.
To facilitate these somewhat divergent needs, Arrow
is split up in three classes.
These do not even form an ordinary hierarchy, to allow categories to implement
only one or the other aspect.
That's not the only significant difference of this module, compared to Control.Arrow:
- Kleisli arrows are not defined here, but in Control.Monad.Constrained. Monads are really a much more specific concept than category arrows.
- Some extra utilities are included that don't apparently have much to
do with
Arrow
at all, but require the expanded cartesian-category tools and are therefore not in Control.Category.Constrained.
- type Arrow a k = (WellPointed a, EnhancedCat a k)
- class Cartesian a => Morphism a where
- first :: (ObjectPair a b d, ObjectPair a c d) => a b c -> a (b, d) (c, d)
- second :: (ObjectPair a d b, ObjectPair a d c) => a b c -> a (d, b) (d, c)
- (***) :: (ObjectPair a b b', ObjectPair a c c') => a b c -> a b' c' -> a (b, b') (c, c')
- class Morphism a => PreArrow a where
- (&&&) :: (Object a b, ObjectPair a c c') => a b c -> a b c' -> a b (c, c')
- terminal :: Object a b => a b (UnitObject a)
- fst :: ObjectPair a x y => a (x, y) x
- snd :: ObjectPair a x y => a (x, y) y
- class (PreArrow a, ObjectPoint a (UnitObject a)) => WellPointed a where
- type PointObject a x :: Constraint
- globalElement :: ObjectPoint a x => x -> a (UnitObject a) x
- unit :: CatTagged a (UnitObject a)
- const :: (Object a b, ObjectPoint a x) => x -> a b x
- type ObjectPoint k a = (Object k a, PointObject k a)
- class Category k => EnhancedCat a k where
- type ArrowChoice a k = (WellPointed a, PreArrChoice a, EnhancedCat a k)
- class CoCartesian a => MorphChoice a where
- class MorphChoice k => PreArrChoice k where
- class (PreArrow k, PreArrChoice k) => SPDistribute k where
- distribute :: (ObjectSum k (a, b) (a, c), ObjectPair k a (b + c), ObjectSum k b c, PairObjects k a b, PairObjects k a c) => k (a, b + c) ((a, b) + (a, c))
- unDistribute :: (ObjectSum k (a, b) (a, c), ObjectPair k a (b + c), ObjectSum k b c, PairObjects k a b, PairObjects k a c) => k ((a, b) + (a, c)) (a, b + c)
- boolAsSwitch :: (ObjectSum k a a, ObjectPair k Bool a) => k (Bool, a) (a + a)
- boolFromSwitch :: (ObjectSum k a a, ObjectPair k Bool a) => k (a + a) (Bool, a)
- type Function f = EnhancedCat (->) f
- ($) :: (Function f, Object f a, Object f b) => f a b -> a -> b
- (>>>) :: (Category k, Object k a, Object k b, Object k c) => k a b -> k b c -> k a c
- (<<<) :: (Category k, Object k a, Object k b, Object k c) => k b c -> k a b -> k a c
- class (Morphism k, HasAgent k) => CartesianAgent k where
- alg1to2 :: (Object k a, ObjectPair k b c) => (forall q. Object k q => AgentVal k q a -> (AgentVal k q b, AgentVal k q c)) -> k a (b, c)
- alg2to1 :: (ObjectPair k a b, Object k c) => (forall q. Object k q => AgentVal k q a -> AgentVal k q b -> AgentVal k q c) -> k (a, b) c
- alg2to2 :: (ObjectPair k a b, ObjectPair k c d) => (forall q. Object k q => AgentVal k q a -> AgentVal k q b -> (AgentVal k q c, AgentVal k q d)) -> k (a, b) (c, d)
- genericAgentCombine :: (HasAgent k, PreArrow k, Object k a, ObjectPair k b c, Object k d) => k (b, c) d -> GenericAgent k a b -> GenericAgent k a c -> GenericAgent k a d
- genericUnit :: (PreArrow k, HasAgent k, Object k a) => GenericAgent k a (UnitObject k)
- genericAlg1to2 :: (PreArrow k, u ~ UnitObject k, Object k a, ObjectPair k b c) => (forall q. Object k q => GenericAgent k q a -> (GenericAgent k q b, GenericAgent k q c)) -> k a (b, c)
- genericAlg2to1 :: (PreArrow k, u ~ UnitObject k, ObjectPair k a u, ObjectPair k a b, ObjectPair k b u, ObjectPair k b a) => (forall q. Object k q => GenericAgent k q a -> GenericAgent k q b -> GenericAgent k q c) -> k (a, b) c
- genericAlg2to2 :: (PreArrow k, u ~ UnitObject k, ObjectPair k a u, ObjectPair k a b, ObjectPair k c d, ObjectPair k b u, ObjectPair k b a) => (forall q. Object k q => GenericAgent k q a -> GenericAgent k q b -> (GenericAgent k q c, GenericAgent k q d)) -> k (a, b) (c, d)
- class (HasAgent k, AgentVal k a x ~ p a x) => PointAgent p k a x | p -> k where
- genericPoint :: (WellPointed k, Object k a, ObjectPoint k x) => x -> GenericAgent k a x
- choose :: (Arrow f (->), Function f, Object f Bool, Object f a) => f (UnitObject f) a -> f (UnitObject f) a -> f Bool a
- ifThenElse :: (EnhancedCat f (->), Function f, Object f Bool, Object f a, Object f (f a a), Object f (f a (f a a))) => Bool `f` (a `f` (a `f` a))
The Arrow type classes
type Arrow a k = (WellPointed a, EnhancedCat a k) Source
class Cartesian a => Morphism a where Source
first :: (ObjectPair a b d, ObjectPair a c d) => a b c -> a (b, d) (c, d) Source
second :: (ObjectPair a d b, ObjectPair a d c) => a b c -> a (d, b) (d, c) Source
(***) :: (ObjectPair a b b', ObjectPair a c c') => a b c -> a b' c' -> a (b, b') (c, c') infixr 3 Source
Morphism (->) | |
(Morphism a, o (UnitObject a)) => Morphism (ConstrainedCategory a o) | |
(Monad m a, Morphism a, Curry a) => Morphism (Kleisli m a) |
class Morphism a => PreArrow a where Source
Unlike first
, second
, ***
and arr
, &&&
has an intrinsic notion
of "direction": it is basically equivalent to precomposing the result
of ***
with a b -> (b,b)
, but that is in general only available
for arrows that generalise ordinary functions, in their native direction.
((b,b) ->b
is specific to semigroups.) It is for this reason the only constituent
class of Arrow
that actually has "arrow" in its name.
In terms of category theory, this "direction" reflects the distinction
between initial- and terminal objects. The latter are more interesting,
basically what UnitObject
is useful for. It gives rise to the tuple
selector morphisms as well.
(&&&) :: (Object a b, ObjectPair a c c') => a b c -> a b c' -> a b (c, c') infixr 3 Source
terminal :: Object a b => a b (UnitObject a) Source
fst :: ObjectPair a x y => a (x, y) x Source
snd :: ObjectPair a x y => a (x, y) y Source
PreArrow (->) | |
(PreArrow a, o (UnitObject a)) => PreArrow (ConstrainedCategory a o) | |
(Monad m a, PreArrow a, Curry a) => PreArrow (Kleisli m a) |
class (PreArrow a, ObjectPoint a (UnitObject a)) => WellPointed a where Source
WellPointed
expresses the relation between your category's objects
and the values of the Haskell data types (which is, after all, what objects are
in this library). Specifically, this class allows you to "point" on
specific objects, thus making out a value of that type as a point of the object.
Perhaps easier than thinking about what that's supposed to mean is noting
this class contains const
. Thus WellPointed
is almost the
traditional Arrow
: it lets you express all the natural transformations
and inject constant values, only you can't just promote arbitrary functions
to arrows of the category.
Unlike with Morphism
and PreArrow
, a literal dual of WellPointed
does
not seem useful.
unit, (globalElement | const)
type PointObject a x :: Constraint Source
globalElement :: ObjectPoint a x => x -> a (UnitObject a) x Source
unit :: CatTagged a (UnitObject a) Source
const :: (Object a b, ObjectPoint a x) => x -> a b x Source
WellPointed (->) | |
(WellPointed a, o (UnitObject a)) => WellPointed (ConstrainedCategory a o) | |
(Monad m a, WellPointed a, ObjectPoint a (m (UnitObject a))) => WellPointed (Kleisli m a) |
type ObjectPoint k a = (Object k a, PointObject k a) Source
class Category k => EnhancedCat a k where Source
Category k => EnhancedCat k k | |
Function f => EnhancedCat (->) (ConstrainedCategory f o) | |
(Arrow a k, o (UnitObject a)) => EnhancedCat (ConstrainedCategory a o) k | |
(Monad m a, Arrow a q, Cartesian a) => EnhancedCat (Kleisli m a) q |
Dual / "choice" arrows
type ArrowChoice a k = (WellPointed a, PreArrChoice a, EnhancedCat a k) Source
class CoCartesian a => MorphChoice a where Source
Dual to Morphism
, dealing with sums instead of products.
left :: (ObjectSum a b d, ObjectSum a c d) => a b c -> a (b + d) (c + d) Source
right :: (ObjectSum a d b, ObjectSum a d c) => a b c -> a (d + b) (d + c) Source
(+++) :: (ObjectSum a b b', ObjectSum a c c') => a b c -> a b' c' -> a (b + b') (c + c') Source
MorphChoice (->) | |
(MorphChoice k, o (ZeroObject k)) => MorphChoice (ConstrainedCategory k o) | |
(Monad m k, Arrow k (->), Function k, PreArrChoice k, Object k (m (ZeroObject k)), Object k (m (m (ZeroObject k)))) => MorphChoice (Kleisli m k) | Hask-Kleislis inherit more or less trivially |
class MorphChoice k => PreArrChoice k where Source
Dual to PreArrow
, this class deals with the vacuous initial (zero) objects,
but also more usefully with choices / sums.
This represents the most part of ArrowChoice
.
(|||) :: (ObjectSum k b b', Object k c) => k b c -> k b' c -> k (b + b') c infixr 2 Source
initial :: Object k b => k (ZeroObject k) b Source
This is basically absurd
.
coFst :: ObjectSum k a b => k a (a + b) Source
Perhaps lft
and rgt
would be more consequent names, but likely more confusing as well.
PreArrChoice (->) | |
(PreArrChoice k, o (ZeroObject k)) => PreArrChoice (ConstrainedCategory k o) | |
(Monad m k, Arrow k (->), Function k, PreArrChoice k, Object k (m (ZeroObject k)), Object k (m (m (ZeroObject k)))) => PreArrChoice (Kleisli m k) |
Distributive law between sum- and product objects
class (PreArrow k, PreArrChoice k) => SPDistribute k where Source
Like in arithmetics, the distributive law
a ⋅ (b + c) ≈ (a ⋅ b) + (a ⋅ c)
holds for Haskell types – in the usual isomorphism sense. But like many such
isomorphisms that are trivial to inline in Hask, this is not necessarily the case
for general categories.
distribute :: (ObjectSum k (a, b) (a, c), ObjectPair k a (b + c), ObjectSum k b c, PairObjects k a b, PairObjects k a c) => k (a, b + c) ((a, b) + (a, c)) Source
unDistribute :: (ObjectSum k (a, b) (a, c), ObjectPair k a (b + c), ObjectSum k b c, PairObjects k a b, PairObjects k a c) => k ((a, b) + (a, c)) (a, b + c) Source
boolAsSwitch :: (ObjectSum k a a, ObjectPair k Bool a) => k (Bool, a) (a + a) Source
boolFromSwitch :: (ObjectSum k a a, ObjectPair k Bool a) => k (a + a) (Bool, a) Source
SPDistribute (->) | |
(SPDistribute k, o (ZeroObject k), o (UnitObject k)) => SPDistribute (ConstrainedCategory k o) | |
(SPDistribute k, Monad m k, PreArrow (Kleisli m k), PreArrChoice (Kleisli m k)) => SPDistribute (Kleisli m k) |
Function-like categories
type Function f = EnhancedCat (->) f Source
Many categories have as morphisms essentially functions with extra properties: group homomorphisms, linear maps, continuous functions...
It makes sense to generalise the notion of function application to these
morphisms; we can't do that for the simple juxtaposition writing f x
,
but it is possible for the function-application operator $
.
This is particularly useful for ConstrainedCategory
versions of Hask,
where after all the morphisms are nothing but functions.
Alternative composition notation
(>>>) :: (Category k, Object k a, Object k b, Object k c) => k a b -> k b c -> k a c infixr 1 Source
(<<<) :: (Category k, Object k a, Object k b, Object k c) => k b c -> k a b -> k a c infixr 1 Source
Proxies for cartesian categories
class (Morphism k, HasAgent k) => CartesianAgent k where Source
alg1to2 :: (Object k a, ObjectPair k b c) => (forall q. Object k q => AgentVal k q a -> (AgentVal k q b, AgentVal k q c)) -> k a (b, c) Source
alg2to1 :: (ObjectPair k a b, Object k c) => (forall q. Object k q => AgentVal k q a -> AgentVal k q b -> AgentVal k q c) -> k (a, b) c Source
alg2to2 :: (ObjectPair k a b, ObjectPair k c d) => (forall q. Object k q => AgentVal k q a -> AgentVal k q b -> (AgentVal k q c, AgentVal k q d)) -> k (a, b) (c, d) Source
genericAgentCombine :: (HasAgent k, PreArrow k, Object k a, ObjectPair k b c, Object k d) => k (b, c) d -> GenericAgent k a b -> GenericAgent k a c -> GenericAgent k a d Source
genericUnit :: (PreArrow k, HasAgent k, Object k a) => GenericAgent k a (UnitObject k) Source
genericAlg1to2 :: (PreArrow k, u ~ UnitObject k, Object k a, ObjectPair k b c) => (forall q. Object k q => GenericAgent k q a -> (GenericAgent k q b, GenericAgent k q c)) -> k a (b, c) Source
genericAlg2to1 :: (PreArrow k, u ~ UnitObject k, ObjectPair k a u, ObjectPair k a b, ObjectPair k b u, ObjectPair k b a) => (forall q. Object k q => GenericAgent k q a -> GenericAgent k q b -> GenericAgent k q c) -> k (a, b) c Source
genericAlg2to2 :: (PreArrow k, u ~ UnitObject k, ObjectPair k a u, ObjectPair k a b, ObjectPair k c d, ObjectPair k b u, ObjectPair k b a) => (forall q. Object k q => GenericAgent k q a -> GenericAgent k q b -> (GenericAgent k q c, GenericAgent k q d)) -> k (a, b) (c, d) Source
class (HasAgent k, AgentVal k a x ~ p a x) => PointAgent p k a x | p -> k where Source
genericPoint :: (WellPointed k, Object k a, ObjectPoint k x) => x -> GenericAgent k a x Source
Misc utility
Conditionals
:: (Arrow f (->), Function f, Object f Bool, Object f a) | |
=> f (UnitObject f) a | " |
-> f (UnitObject f) a | " |
-> f Bool a |
Basically ifThenElse
with inverted argument order, and
"morphismised" arguments.
ifThenElse :: (EnhancedCat f (->), Function f, Object f Bool, Object f a, Object f (f a a), Object f (f a (f a a))) => Bool `f` (a `f` (a `f` a)) Source