-- |
-- Module : Control.Category.Constrained
-- Copyright : (c) 2013 Justus Sagemüller
-- License : GPL v3 (see COPYING)
-- Maintainer : (@) sagemueller $ geo.uni-koeln.de
--
--
-- The most basic category theory tools are included partly in this
-- module, partly in "Control.Arrow.Constrained".
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeOperators #-}
module Control.Category.Constrained (
-- * The category class
Category (..)
-- * Monoidal categories
, Cartesian (..), ObjectPair
, Curry (..), ObjectMorphism
-- * Monoidal with coproducts
, (+)()
, CoCartesian (..), ObjectSum
-- * Isomorphisms
, Isomorphic (..)
-- * Constraining a category
, ConstrainedCategory (ConstrainedMorphism)
, constrained, unconstrained
-- * Global-element proxies
, HasAgent (..)
, genericAlg, genericAgentMap
, GenericAgent (..)
-- * Utility
, inCategoryOf
, CatTagged
) where
import Prelude hiding (id, (.), curry, uncurry)
import qualified Prelude
import GHC.Exts (Constraint)
import Data.Tagged
import Data.Monoid
import Data.Void
-- | In mathematics, a category is defined as a class of /objects/, plus a class of
-- /morphisms/ between those objects. In Haskell, one traditionally works in
-- the category @(->)@ (called /Hask/), in which /any Haskell type/ is an object.
-- But of course
-- there are lots of useful categories where the objects are much more specific,
-- e.g. vector spaces with linear maps as morphisms. The obvious way to express
-- this in Haskell is as type class constraints, and the @ConstraintKinds@ extension
-- allows quantifying over such object classes.
--
-- Like in "Control.Category", \"the category @k@\" means actually @k@ is the
-- /morphism type constructor/. From a mathematician's point of view this may
-- seem a bit strange way to define the category, but it just turns out to
-- be quite convenient for practical purposes.
class Category k where
type Object k o :: Constraint
type Object k o = ()
id :: Object k a => k a a
(.) :: (Object k a, Object k b, Object k c)
=> k b c -> k a b -> k a c
infixr 9 .
instance Category (->) where
id = Prelude.id
(.) = (Prelude..)
-- | Analogue to 'asTypeOf', this does not actually do anything but can
-- give the compiler type unification hints in a convenient manner.
inCategoryOf :: (Category k) => k a b -> k c d -> k a b
m `inCategoryOf` _ = m
-- | A given category can be specialised, by using the same morphisms but adding
-- extra constraints to what is considered an object.
--
-- For instance, @'ConstrainedCategory' (->) 'Ord'@ is the category of all
-- totally ordered data types (but with arbitrary functions; this does not require
-- monotonicity or anything).
newtype ConstrainedCategory (k :: * -> * -> *) (o :: * -> Constraint) (a :: *) (b :: *)
= ConstrainedMorphism { unconstrainedMorphism :: k a b }
-- | Cast a morphism to its equivalent in a more constrained category,
-- provided it connects objects that actually satisfy the extra constraint.
constrained :: (Category k, o a, o b) => k a b -> ConstrainedCategory k o a b
constrained = ConstrainedMorphism
-- | \"Unpack\" a constrained morphism again (forgetful functor).
--
-- Note that you may often not need to do that; in particular
-- morphisms that are actually 'Function's can just be applied
-- to their objects with '$' right away, no need to go back to
-- Hask first.
unconstrained :: (Category k) => ConstrainedCategory k o a b -> k a b
unconstrained = unconstrainedMorphism
instance (Category k) => Category (ConstrainedCategory k isObj) where
type Object (ConstrainedCategory k isObj) o = (Object k o, isObj o)
id = ConstrainedMorphism id
ConstrainedMorphism f . ConstrainedMorphism g = ConstrainedMorphism $ f . g
-- | Apart from /the/ identity morphism, 'id', there are other morphisms that
-- can basically be considered identies. For instance, in any cartesian
-- category (where it makes sense to have tuples and unit @()@ at all), it should be
-- possible to switch between @a@ and the isomorphic @(a, ())@. 'iso' is
-- the method for such \"pseudo-identities\", the most basic of which
-- are required as methods of the 'Cartesian' class.
--
-- Why it is necessary to make these morphisms explicit: they are needed
-- for a couple of general-purpose category-theory methods, but even though
-- they're normally trivial to define there is no uniform way to do so.
-- For instance, for vector spaces, the baseis of @(a, (b,c))@ and @((a,b), c)@
-- are sure enough structurally equivalent, but not in the same way the spaces
-- themselves are (sum vs. product types).
{-# DEPRECATED iso "This generic method, while looking nicely uniform, relies on OverlappingInstances and is therefore probably a bad idea. Use the specialised methods in classes like 'SPDistribute' instead." #-}
class (Category k) => Isomorphic k a b where
iso :: k a b
instance (Cartesian k, Object k a, u ~ UnitObject k, ObjectPair k a u) => Isomorphic k a (a,u) where
iso = attachUnit
instance (Cartesian k, Object k a, u ~ UnitObject k, ObjectPair k a u) => Isomorphic k (a,u) a where
iso = detachUnit
instance (Cartesian k, Object k a, u ~ UnitObject k, ObjectPair k a u, ObjectPair k u a, Object k (u, a), Object k (a, u) )
=> Isomorphic k a (u,a) where
iso = swap . attachUnit
instance (Cartesian k, Object k a, u ~ UnitObject k, ObjectPair k a u, ObjectPair k u a, Object k (u, a), Object k (a, u) )
=> Isomorphic k (u,a) a where
iso = detachUnit . swap
instance ( Cartesian k, Object k a, ObjectPair k a b, ObjectPair k b c
, ObjectPair k a (b,c), ObjectPair k (a,b) c, Object k c )
=> Isomorphic k (a,(b,c)) ((a,b),c) where
iso = regroup
instance ( Cartesian k, Object k a, ObjectPair k a b, ObjectPair k b c
, ObjectPair k a (b,c), ObjectPair k (a,b) c, Object k c )
=> Isomorphic k ((a,b),c) (a,(b,c)) where
iso = regroup'
instance (CoCartesian k, Object k a, u ~ ZeroObject k, ObjectSum k a u) => Isomorphic k a (a+u) where
iso = attachZero
instance (CoCartesian k, Object k a, u ~ ZeroObject k, ObjectSum k a u) => Isomorphic k (a+u) a where
iso = detachZero
instance (CoCartesian k, Object k a, u ~ ZeroObject k, ObjectSum k a u, ObjectSum k u a, Object k (u+a), Object k (a+u) )
=> Isomorphic k a (u+a) where
iso = coSwap . attachZero
instance (CoCartesian k, Object k a, u ~ ZeroObject k, ObjectSum k a u, ObjectSum k u a, Object k (u+a), Object k (a+u) )
=> Isomorphic k (u+a) a where
iso = detachZero . coSwap
instance ( CoCartesian k, Object k a, ObjectSum k a b, ObjectSum k b c
, ObjectSum k a (b+c), ObjectSum k (a+b) c, Object k c )
=> Isomorphic k (a+(b+c)) ((a+b)+c) where
iso = coRegroup
instance ( CoCartesian k, Object k a, ObjectSum k a b, ObjectSum k b c
, ObjectSum k a (b+c), ObjectSum k (a+b) c, Object k c )
=> Isomorphic k ((a+b)+c) (a+(b+c)) where
iso = coRegroup'
-- | Quite a few categories (/monoidal categories/) will permit \"products\" of
-- objects as objects again – in the Haskell sense those are tuples – allowing
-- for \"dyadic morphisms\" @(x,y) ~> r@.
--
-- Together with a unique 'UnitObject', this makes for a monoidal
-- structure, with a few natural isomorphisms. Ordinary tuples may not
-- always be powerful enough to express the product objects; we avoid
-- making a dedicated associated type for the sake of simplicity,
-- but allow for an extra constraint to be imposed on objects prior
-- to consideration of pair-building.
--
-- The name 'Cartesian' is disputable: in category theory that would rather
-- Imply /cartesian closed category/ (which we represent with 'Curry').
-- 'Monoidal' would make sense, but we reserve that to 'Functors'.
class ( Category k
, Monoid (UnitObject k), Object k (UnitObject k)
-- , PairObject k (UnitObject k) (UnitObject k), Object k (UnitObject k,UnitObject k)
) => Cartesian k where
-- | Extra properties two types @a, b@ need to fulfill so @(a,b)@ can be an
-- object of the category. This need /not/ take care for @a@ and @b@ themselves
-- being objects, we do that seperately: every function that actually deals
-- with @(a,b)@ objects should require the stronger @'ObjectPair' k a b@.
--
-- If /any/ two object types of your category make up a pair object, then
-- just leave 'PairObjects' at the default (empty constraint).
type PairObjects k a b :: Constraint
type PairObjects k a b = ()
-- | Defaults to '()', and should normally be left at that.
type UnitObject k :: *
type UnitObject k = ()
swap :: ( ObjectPair k a b, ObjectPair k b a ) => k (a,b) (b,a)
attachUnit :: ( Object k a, u ~ UnitObject k, ObjectPair k a u ) => k a (a,u)
detachUnit :: ( Object k a, u ~ UnitObject k, ObjectPair k a u ) => k (a,u) a
regroup :: ( Object k a, Object k c, ObjectPair k a b, ObjectPair k b c
, ObjectPair k a (b,c), ObjectPair k (a,b) c
) => k (a, (b, c)) ((a, b), c)
regroup' :: ( Object k a, Object k c, ObjectPair k a b, ObjectPair k b c
, ObjectPair k a (b,c), ObjectPair k (a,b) c
) => k ((a, b), c) (a, (b, c))
-- | Use this constraint to ensure that @a@, @b@ and @(a,b)@ are all \"fully valid\" objects
-- of your category (meaning, you can use them with the 'Cartesian' combinators).
type ObjectPair k a b = ( Category k, Object k a, Object k b
, PairObjects k a b, Object k (a,b) )
instance Cartesian (->) where
swap = \(a,b) -> (b,a)
attachUnit = \a -> (a, ())
detachUnit = \(a, ()) -> a
regroup = \(a, (b, c)) -> ((a, b), c)
regroup' = \((a, b), c) -> (a, (b, c))
instance (Cartesian f, o (UnitObject f)) => Cartesian (ConstrainedCategory f o) where
type PairObjects (ConstrainedCategory f o) a b = (PairObjects f a b)
type UnitObject (ConstrainedCategory f o) = UnitObject f
swap = ConstrainedMorphism swap
attachUnit = ConstrainedMorphism attachUnit
detachUnit = ConstrainedMorphism detachUnit
regroup = ConstrainedMorphism regroup
regroup' = ConstrainedMorphism regroup'
type (+) = Either
-- | Monoidal categories need not be based on a cartesian product.
-- The relevant alternative is coproducts.
--
-- The dual notion to 'Cartesian' replaces such products (pairs) with
-- sums ('Either'), and unit '()' with void types.
--
-- Basically, the only thing that doesn't mirror 'Cartesian' here
-- is that we don't require @CoMonoid ('ZeroObject' k)@. Comonoids
-- do in principle make sense, but not from a Haskell viewpoint
-- (every type is trivially a comonoid).
--
-- Haskell of course uses sum types, /variants/, most often without
-- 'Either' appearing. But variants are generally isomorphic to sums;
-- the most important (sums of unit) are methods here.
class ( Category k, Object k (ZeroObject k)
) => CoCartesian k where
type SumObjects k a b :: Constraint
type SumObjects k a b = ()
-- | Defaults to 'Void'.
type ZeroObject k :: *
type ZeroObject k = Void
coSwap :: ( ObjectSum k a b, ObjectSum k b a ) => k (a+b) (b+a)
attachZero :: ( Object k a, z ~ ZeroObject k, ObjectSum k a z ) => k a (a+z)
detachZero :: ( Object k a, z ~ ZeroObject k, ObjectSum k a z ) => k (a+z) a
coRegroup :: ( Object k a, Object k c, ObjectSum k a b, ObjectSum k b c
, ObjectSum k a (b+c), ObjectSum k (a+b) c
) => k (a+(b+c)) ((a+b)+c)
coRegroup' :: ( Object k a, Object k c, ObjectSum k a b, ObjectSum k b c
, ObjectSum k a (b+c), ObjectSum k (a+b) c
) => k ((a+b)+c) (a+(b+c))
maybeAsSum :: ( ObjectSum k u a, u ~ UnitObject k, Object k (Maybe a) )
=> k (Maybe a) (u + a)
maybeFromSum :: ( ObjectSum k u a, u ~ UnitObject k, Object k (Maybe a) )
=> k (u + a) (Maybe a)
boolAsSum :: ( ObjectSum k u u, u ~ UnitObject k, Object k Bool )
=> k Bool (u + u)
boolFromSum :: ( ObjectSum k u u, u ~ UnitObject k, Object k Bool )
=> k (u + u) Bool
type ObjectSum k a b = ( Category k, Object k a, Object k b
, SumObjects k a b, Object k (a+b) )
instance CoCartesian (->) where
coSwap (Left a) = Right a
coSwap (Right a) = Left a
attachZero = Left
detachZero (Left a) = a
detachZero (Right void) = absurd void
coRegroup (Left a) = Left $ Left a
coRegroup (Right (Left a)) = Left $ Right a
coRegroup (Right (Right a)) = Right a
coRegroup' (Left (Left a)) = Left a
coRegroup' (Left (Right a)) = Right $ Left a
coRegroup' (Right a) = Right $ Right a
maybeAsSum Nothing = Left ()
maybeAsSum (Just x) = Right x
maybeFromSum (Left ()) = Nothing
maybeFromSum (Right x) = Just x
boolAsSum False = Left ()
boolAsSum True = Right ()
boolFromSum (Left ()) = False
boolFromSum (Right ()) = True
-- boolAsSwitch (False,x) = Left x
-- boolAsSwitch (True,x) = Right x
-- boolFromSwitch (Left x) = (False,x)
-- boolFromSwitch (Right x) = (True,x)
--
instance (CoCartesian f, o (ZeroObject f)) => CoCartesian (ConstrainedCategory f o) where
type SumObjects (ConstrainedCategory f o) a b = (SumObjects f a b)
type ZeroObject (ConstrainedCategory f o) = ZeroObject f
coSwap = ConstrainedMorphism coSwap
attachZero = ConstrainedMorphism attachZero
detachZero = ConstrainedMorphism detachZero
coRegroup = ConstrainedMorphism coRegroup
coRegroup' = ConstrainedMorphism coRegroup'
maybeAsSum = ConstrainedMorphism maybeAsSum
maybeFromSum = ConstrainedMorphism maybeFromSum
boolAsSum = ConstrainedMorphism boolAsSum
boolFromSum = ConstrainedMorphism boolFromSum
-- boolAsSwitch = ConstrainedMorphism boolAsSwitch
-- boolFromSwitch = ConstrainedMorphism boolFromSwitch
-- | Tagged type for values that depend on some choice of category, but not on some
-- particular object / arrow therein.
type CatTagged k x = Tagged (k (UnitObject k) (UnitObject k)) x
class (Cartesian k) => Curry k where
type MorphObjects k b c :: Constraint
type MorphObjects k b c = ()
uncurry :: (ObjectPair k a b, ObjectMorphism k b c)
=> k a (k b c) -> k (a, b) c
-- uncurry f = apply . (f &&& id)
curry :: (ObjectPair k a b, ObjectMorphism k b c)
=> k (a, b) c -> k a (k b c)
apply :: (ObjectMorphism k a b, ObjectPair k (k a b) a)
=> k (k a b, a) b
apply = uncurry id
-- | Analogous to 'ObjectPair': express that @k b c@ be an exponential object
-- representing the morphism.
type ObjectMorphism k b c = (Object k b, Object k c, MorphObjects k b c, Object k (k b c))
instance Curry (->) where
uncurry = Prelude.uncurry
curry = Prelude.curry
apply (f,x) = f x
instance (Curry f, o (UnitObject f)) => Curry (ConstrainedCategory f o) where
type MorphObjects (ConstrainedCategory f o) a c = ( MorphObjects f a c, f ~ (->) )
uncurry (ConstrainedMorphism f) = ConstrainedMorphism $ \(a,b) -> unconstrained (f a) b
curry (ConstrainedMorphism f) = ConstrainedMorphism $ \a -> ConstrainedMorphism $ \b -> f (a, b)
infixr 0 $~
-- | An agent value is a \"general representation\" of a category's
-- values, i.e. /global elements/. This is useful to define certain
-- morphisms (including ones that can't just \"inherit\" from '->'
-- with 'Control.Arrow.Constrained.arr') in ways other than point-free
-- composition pipelines. Instead, you can write algebraic expressions
-- much as if dealing with actual values of your category's objects,
-- but using the agent type which is restricted so any function
-- defined as such a lambda-expression qualifies as a morphism
-- of that category.
class (Category k) => HasAgent k where
type AgentVal k a v :: *
type AgentVal k a v = GenericAgent k a v
alg :: ( Object k a, Object k b
) => (forall q . Object k q
=> AgentVal k q a -> AgentVal k q b) -> k a b
($~) :: ( Object k a, Object k b, Object k c
) => k b c -> AgentVal k a b -> AgentVal k a c
data GenericAgent k a v = GenericAgent { runGenericAgent :: k a v }
genericAlg :: ( HasAgent k, Object k a, Object k b )
=> ( forall q . Object k q
=> GenericAgent k q a -> GenericAgent k q b ) -> k a b
genericAlg f = runGenericAgent . f $ GenericAgent id
genericAgentMap :: ( HasAgent k, Object k a, Object k b, Object k c )
=> k b c -> GenericAgent k a b -> GenericAgent k a c
genericAgentMap m (GenericAgent v) = GenericAgent $ m . v
instance HasAgent (->) where
type AgentVal (->) a b = b
alg f = f
($~) = ($)