#if __GLASGOW_HASKELL__ >= 800
#endif
module Control.Category.Constrained (
Category (..)
, Cartesian (..), ObjectPair
, Curry (..), ObjectMorphism
, type (+)()
, CoCartesian (..), ObjectSum
, Isomorphic (..)
, ConstrainedCategory (ConstrainedMorphism)
, constrained, unconstrained
, HasAgent (..)
, genericAlg, genericAgentMap
, GenericAgent (..)
, 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
import Data.Type.Coercion
import qualified Control.Category as Hask
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..)
inCategoryOf :: (Category k) => k a b -> k c d -> k a b
m `inCategoryOf` _ = m
newtype ConstrainedCategory (k :: * -> * -> *) (o :: * -> Constraint) (a :: *) (b :: *)
= ConstrainedMorphism { unconstrainedMorphism :: k a b }
constrained :: (Category k, o a, o b) => k a b -> ConstrainedCategory k o a b
constrained = ConstrainedMorphism
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
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'
class ( Category k
, Monoid (UnitObject k), Object k (UnitObject k)
) => Cartesian k where
type PairObjects k a b :: Constraint
type PairObjects k a b = ()
type UnitObject k :: *
type UnitObject k = ()
swap :: ( ObjectPair k a b, ObjectPair k b a ) => k (a,b) (b,a)
attachUnit :: ( u ~ UnitObject k, ObjectPair k a u ) => k a (a,u)
detachUnit :: ( u ~ UnitObject k, ObjectPair k a u ) => k (a,u) a
regroup :: ( 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' :: ( 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))
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
class ( Category k, Object k (ZeroObject k)
) => CoCartesian k where
type SumObjects k a b :: Constraint
type SumObjects k a b = ()
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
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
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
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
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 $~
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
($~) = ($)
instance Category Coercion where
id = Hask.id
(.) = (Hask..)