{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE UndecidableSuperClasses #-}
#endif
module Control.Category.Constrained (
Category (..)
, Cartesian (..), ObjectPair
, Curry (..), ObjectMorphism
, type (+)()
, CoCartesian (..), ObjectSum
, Isomorphic (..)
, ConstrainedCategory (ConstrainedMorphism)
, constrained, unconstrained
, ConstrainedFunction
, 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
import Control.Category.Discrete
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 Discrete where
id = Refl
Refl . Refl = Refl
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
type ConstrainedFunction isObj = ConstrainedCategory (->) isObj
{-# 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'
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 HasAgent Discrete where
alg = genericAlg
($~) = genericAgentMap
instance Category Coercion where
id = Hask.id
(.) = (Hask..)