-- |
-- Module      :  Control.Category.Constrained
-- Copyright   :  (c) 2013-2016 Justus Sagemüller
-- License     :  GPL v3 (see COPYING)
-- Maintainer  :  (@) jsag $ hvl.no
-- 
-- 
-- The most basic category theory tools are included partly in this
-- module, partly in "Control.Arrow.Constrained".

{-# LANGUAGE ConstraintKinds              #-}
{-# LANGUAGE PolyKinds                    #-}
{-# LANGUAGE TypeFamilies                 #-}
{-# LANGUAGE MultiParamTypeClasses        #-}
{-# LANGUAGE FlexibleContexts             #-}
{-# LANGUAGE RankNTypes                   #-}
{-# LANGUAGE UnicodeSyntax                #-}
{-# LANGUAGE AllowAmbiguousTypes          #-}
{-# LANGUAGE TypeOperators                #-}
{-# LANGUAGE ExplicitNamespaces           #-}
{-# LANGUAGE CPP                          #-}
#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE UndecidableSuperClasses      #-}
#endif
{-# LANGUAGE LambdaCase                   #-}

module Control.Category.Constrained ( 
            -- * The category class
            Category (..)
            -- * Monoidal categories
          , Cartesian (..), ObjectPair
          , Curry (..), ObjectMorphism
            -- * Monoidal with coproducts
          , type (+)()
          , CoCartesian (..), ObjectSum
            -- * The standard function category
          , type Hask
            -- * Isomorphisms
          , Isomorphic (..)
            -- * Constraining a category
          , ConstrainedCategory (ConstrainedMorphism)
          , type (⊢)()
          , constrained, unconstrained
          , ConstrainedFunction
            -- * Product categories
          , ProductCategory(..), type (×)()
            -- * 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
import Data.CategoryObject.Product
#if MIN_VERSION_base(4,9,0)
import Data.Kind (Type)
#endif
import Data.Type.Coercion
import qualified Control.Category as Hask
import qualified Data.Functor.Contravariant as Hask (Op(..))

import Data.Constraint.Trivial (Unconstrained)

import Control.Category.Discrete

-- | 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.
#if MIN_VERSION_base(4,9,0)
class Category (k :: κ -> κ -> Type) where
#else
class Category (k :: κ -> κ -> *) where
#endif
  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 :: forall (a :: κ). Object Discrete a => Discrete a a
id = forall {k} (a :: k). Discrete a a
Refl
  Discrete b c
Refl . :: forall (a :: κ) (b :: κ) (c :: κ).
(Object Discrete a, Object Discrete b, Object Discrete c) =>
Discrete b c -> Discrete a b -> Discrete a c
. Discrete a b
Refl = forall {k} (a :: k). Discrete a a
Refl

instance Category (->) where
  id :: forall a. Object (->) a => a -> a
id = forall a. a -> a
Prelude.id
  . :: forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> a -> c
(.) = forall b c a. (b -> c) -> (a -> b) -> a -> c
(Prelude..)

instance Category Hask.Op where
  id :: forall a. Object Op a => Op a a
id = forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
Hask.id
  . :: forall a b c.
(Object Op a, Object Op b, Object Op c) =>
Op b c -> Op a b -> Op a c
(.) = forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
(Hask..)

-- | The category of all Haskell types, with (wrapped) Haskell functions as morphisms.
--   This is just a type-wrapper, morally equivalent to the @(->)@ category itself.
--   The difference is that 'Control.Functor.Constrained.Functor' instances in the '(->)'
--   category are automatically inherited from the standard 'Prelude.Functor' instances
--   that most packages define their type for. The benefit of that is that normal
--   Haskell code keeps working when the "Prelude" classes are replaced with the ones
--   from this library, but the downside is that you can't make /more gradual/ instances
--   when this is desired. This is where the 'Hask' category comes in: it only has functors
--   that are explicitly declared as such.
type Hask = Unconstrained⊢(->)

-- | 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
k a b
m inCategoryOf :: forall {κ} (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ) (d :: κ).
Category k =>
k a b -> k c d -> k a b
`inCategoryOf` k c d
_ = k a b
m


-- | A given category can be specialised, by using the same morphisms but adding
--   extra constraints to what is considered an object. 
-- 
--   For instance, @'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 { forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
ConstrainedCategory k o a b -> k a b
unconstrainedMorphism :: k a b }

type o ⊢ k = ConstrainedCategory k o

-- | Cast a morphism to its equivalent in a more constrained category,
--   provided it connects objects that actually satisfy the extra constraint.
-- 
--   In practice, it is often necessary to specify to what typeclass it should be
--   constrained. The most convenient way of doing that is with
--   <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-TypeApplications type-applications syntax>.
--   E.g. @'constrained' \@Ord length@ is the 'length' function considered as a morphism in the subcategory of Hask in which all types are orderable. (Which makes it suitable for e.g. fmapping over a set.)
constrained :: ∀ o k a b . (Category k, o a, o b) => k a b -> (o⊢k) a b
constrained :: forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
(Category k, o a, o b) =>
k a b -> (⊢) o k a b
constrained = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
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 :: ∀ o k a b . (Category k) => (o⊢k) a b -> k a b
unconstrained :: forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
Category k =>
(⊢) o k a b -> k a b
unconstrained = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
ConstrainedCategory k o a b -> k a b
unconstrainedMorphism

instance (Category k) => Category (isObj⊢k) where
  type Object (isObj⊢k) o = (Object k o, isObj o)
  id :: forall a. Object (isObj ⊢ k) a => (⊢) isObj k a a
id = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ConstrainedMorphism k b c
f . :: forall a b c.
(Object (isObj ⊢ k) a, Object (isObj ⊢ k) b,
 Object (isObj ⊢ k) c) =>
(⊢) isObj k b c -> (⊢) isObj k a b -> (⊢) isObj k a c
. ConstrainedMorphism k a b
g = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall a b. (a -> b) -> a -> b
$ k b c
f forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a b
g

type ConstrainedFunction isObj = ConstrainedCategory (->) isObj


-- | 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 :: k a (a, u)
iso = forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit
instance (Cartesian k, Object k a, u ~ UnitObject k, ObjectPair k a u) => Isomorphic k (a,u) a where
  iso :: k (a, u) a
iso = forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
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 :: k a (u, a)
iso = forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
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 :: k (u, a) a
iso = forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
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 :: k (a, (b, c)) ((a, b), c)
iso = forall (k :: * -> * -> *) a b c.
(Cartesian k, 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
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 :: k ((a, b), c) (a, (b, c))
iso = forall (k :: * -> * -> *) a b c.
(Cartesian k, 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'


instance (CoCartesian k, Object k a, u ~ ZeroObject k, ObjectSum k a u) => Isomorphic k a (a+u) where
  iso :: k a (a + u)
iso = forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
attachZero
instance (CoCartesian k, Object k a, u ~ ZeroObject k, ObjectSum k a u) => Isomorphic k (a+u) a where
  iso :: k (a + u) a
iso = forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
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 :: k a (u + a)
iso = forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
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 :: k (u + a) a
iso = forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
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 :: k (a + (b + c)) ((a + b) + c)
iso = forall (k :: * -> * -> *) a c b.
(CoCartesian k, 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
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 :: k ((a + b) + c) (a + (b + c))
iso = forall (k :: * -> * -> *) a c b.
(CoCartesian k, 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'


-- | 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 :: ( unit ~ UnitObject k, ObjectPair k a unit ) => k a (a,unit)
  detachUnit :: ( unit ~ UnitObject k, ObjectPair k a unit ) => k (a,unit) 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))

-- | 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 :: forall a b.
(ObjectPair (->) a b, ObjectPair (->) b a) =>
(a, b) -> (b, a)
swap = \(a
a,b
b) -> (b
b,a
a)
  attachUnit :: forall unit a.
(unit ~ UnitObject (->), ObjectPair (->) a unit) =>
a -> (a, unit)
attachUnit = \a
a -> (a
a, ())
  detachUnit :: forall unit a.
(unit ~ UnitObject (->), ObjectPair (->) a unit) =>
(a, unit) -> a
detachUnit = \(a
a, ()) -> a
a
  regroup :: forall a b c.
(ObjectPair (->) a b, ObjectPair (->) b c,
 ObjectPair (->) a (b, c), ObjectPair (->) (a, b) c) =>
(a, (b, c)) -> ((a, b), c)
regroup = \(a
a, (b
b, c
c)) -> ((a
a, b
b), c
c)
  regroup' :: forall a b c.
(ObjectPair (->) a b, ObjectPair (->) b c,
 ObjectPair (->) a (b, c), ObjectPair (->) (a, b) c) =>
((a, b), c) -> (a, (b, c))
regroup' = \((a
a, b
b), c
c) -> (a
a, (b
b, c
c))

instance Cartesian Hask.Op where
  swap :: forall a b.
(ObjectPair Op a b, ObjectPair Op b a) =>
Op (a, b) (b, a)
swap = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. (a -> b) -> a -> b
$ \(b
a,a
b) -> (a
b,b
a)
  attachUnit :: forall unit a.
(unit ~ UnitObject Op, ObjectPair Op a unit) =>
Op a (a, unit)
attachUnit = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. (a -> b) -> a -> b
$ \(a
a, ()) -> a
a
  detachUnit :: forall unit a.
(unit ~ UnitObject Op, ObjectPair Op a unit) =>
Op (a, unit) a
detachUnit = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. (a -> b) -> a -> b
$ \a
a -> (a
a, ())
  regroup :: forall a b c.
(ObjectPair Op a b, ObjectPair Op b c, ObjectPair Op a (b, c),
 ObjectPair Op (a, b) c) =>
Op (a, (b, c)) ((a, b), c)
regroup = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. (a -> b) -> a -> b
$ \((a
a, b
b), c
c) -> (a
a, (b
b, c
c))
  regroup' :: forall a b c.
(ObjectPair Op a b, ObjectPair Op b c, ObjectPair Op a (b, c),
 ObjectPair Op (a, b) c) =>
Op ((a, b), c) (a, (b, c))
regroup' = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. (a -> b) -> a -> b
$ \(a
a, (b
b, c
c)) -> ((a
a, b
b), c
c)
                        
instance (Cartesian f, o (UnitObject f)) => Cartesian (o⊢f) where
  type PairObjects (o⊢f) a b = (PairObjects f a b)
  type UnitObject (o⊢f) = UnitObject f

  swap :: forall a b.
(ObjectPair (o ⊢ f) a b, ObjectPair (o ⊢ f) b a) =>
(⊢) o f (a, b) (b, a)
swap = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap
  attachUnit :: forall unit a.
(unit ~ UnitObject (o ⊢ f), ObjectPair (o ⊢ f) a unit) =>
(⊢) o f a (a, unit)
attachUnit = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit
  detachUnit :: forall unit a.
(unit ~ UnitObject (o ⊢ f), ObjectPair (o ⊢ f) a unit) =>
(⊢) o f (a, unit) a
detachUnit = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit
  regroup :: forall a b c.
(ObjectPair (o ⊢ f) a b, ObjectPair (o ⊢ f) b c,
 ObjectPair (o ⊢ f) a (b, c), ObjectPair (o ⊢ f) (a, b) c) =>
(⊢) o f (a, (b, c)) ((a, b), c)
regroup = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a b c.
(Cartesian k, 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
  regroup' :: forall a b c.
(ObjectPair (o ⊢ f) a b, ObjectPair (o ⊢ f) b c,
 ObjectPair (o ⊢ f) a (b, c), ObjectPair (o ⊢ f) (a, b) c) =>
(⊢) o f ((a, b), c) (a, (b, c))
regroup' = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a b c.
(Cartesian k, 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'


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, zero ~ ZeroObject k, ObjectSum k a zero ) => k a (a+zero)
  detachZero :: ( Object k a, zero ~ ZeroObject k, ObjectSum k a zero ) => k (a+zero) 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 :: forall a b.
(ObjectSum (->) a b, ObjectSum (->) b a) =>
(a + b) -> (b + a)
coSwap (Left a
a) = forall a b. b -> Either a b
Right a
a
  coSwap (Right b
a) = forall a b. a -> Either a b
Left b
a
  attachZero :: forall a zero.
(Object (->) a, zero ~ ZeroObject (->), ObjectSum (->) a zero) =>
a -> (a + zero)
attachZero = forall a b. a -> Either a b
Left
  detachZero :: forall a zero.
(Object (->) a, zero ~ ZeroObject (->), ObjectSum (->) a zero) =>
(a + zero) -> a
detachZero (Left a
a) = a
a
  detachZero (Right zero
void) = forall a. Void -> a
absurd zero
void
  coRegroup :: forall a c b.
(Object (->) a, Object (->) c, ObjectSum (->) a b,
 ObjectSum (->) b c, ObjectSum (->) a (b + c),
 ObjectSum (->) (a + b) c) =>
(a + (b + c)) -> ((a + b) + c)
coRegroup (Left a
a) = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left a
a
  coRegroup (Right (Left b
a)) = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right b
a
  coRegroup (Right (Right c
a)) = forall a b. b -> Either a b
Right c
a
  coRegroup' :: forall a c b.
(Object (->) a, Object (->) c, ObjectSum (->) a b,
 ObjectSum (->) b c, ObjectSum (->) a (b + c),
 ObjectSum (->) (a + b) c) =>
((a + b) + c) -> (a + (b + c))
coRegroup' (Left (Left a
a)) = forall a b. a -> Either a b
Left a
a
  coRegroup' (Left (Right b
a)) = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left b
a
  coRegroup' (Right c
a) = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right c
a
  maybeAsSum :: forall u a.
(ObjectSum (->) u a, u ~ UnitObject (->), Object (->) (Maybe a)) =>
Maybe a -> (u + a)
maybeAsSum Maybe a
Nothing = forall a b. a -> Either a b
Left ()
  maybeAsSum (Just a
x) = forall a b. b -> Either a b
Right a
x
  maybeFromSum :: forall u a.
(ObjectSum (->) u a, u ~ UnitObject (->), Object (->) (Maybe a)) =>
(u + a) -> Maybe a
maybeFromSum (Left ()) = forall a. Maybe a
Nothing
  maybeFromSum (Right a
x) = forall a. a -> Maybe a
Just a
x
  boolAsSum :: forall u.
(ObjectSum (->) u u, u ~ UnitObject (->), Object (->) Bool) =>
Bool -> (u + u)
boolAsSum Bool
False = forall a b. a -> Either a b
Left ()
  boolAsSum Bool
True = forall a b. b -> Either a b
Right ()
  boolFromSum :: forall u.
(ObjectSum (->) u u, u ~ UnitObject (->), Object (->) Bool) =>
(u + u) -> Bool
boolFromSum (Left ()) = Bool
False
  boolFromSum (Right ()) = Bool
True
--   boolAsSwitch (False,x) = Left x
--   boolAsSwitch (True,x) = Right x
--   boolFromSwitch (Left x) = (False,x)
--   boolFromSwitch (Right x) = (True,x)
--                         
instance CoCartesian Hask.Op where
  coSwap :: forall a b.
(ObjectSum Op a b, ObjectSum Op b a) =>
Op (a + b) (b + a)
coSwap = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. (a -> b) -> a -> b
$ \case Right a
a -> forall a b. a -> Either a b
Left a
a
                           Left b
a -> forall a b. b -> Either a b
Right b
a
  attachZero :: forall a zero.
(Object Op a, zero ~ ZeroObject Op, ObjectSum Op a zero) =>
Op a (a + zero)
attachZero = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. (a -> b) -> a -> b
$ \case Left a
a -> a
a
                               Right zero
void -> forall a. Void -> a
absurd zero
void
  detachZero :: forall a zero.
(Object Op a, zero ~ ZeroObject Op, ObjectSum Op a zero) =>
Op (a + zero) a
detachZero = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. a -> Either a b
Left
  coRegroup :: forall a c b.
(Object Op a, Object Op c, ObjectSum Op a b, ObjectSum Op b c,
 ObjectSum Op a (b + c), ObjectSum Op (a + b) c) =>
Op (a + (b + c)) ((a + b) + c)
coRegroup = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. (a -> b) -> a -> b
$ \case Left (Left a
a) -> forall a b. a -> Either a b
Left a
a
                              Left (Right b
a) -> (forall a b. b -> Either a b
Right (forall a b. a -> Either a b
Left b
a))
                              Right c
a -> forall a b. b -> Either a b
Right (forall a b. b -> Either a b
Right c
a)
  coRegroup' :: forall a c b.
(Object Op a, Object Op c, ObjectSum Op a b, ObjectSum Op b c,
 ObjectSum Op a (b + c), ObjectSum Op (a + b) c) =>
Op ((a + b) + c) (a + (b + c))
coRegroup' = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. (a -> b) -> a -> b
$ \case (Left a
a) -> forall a b. a -> Either a b
Left (forall a b. a -> Either a b
Left a
a)
                               Right (Left b
a) -> forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right b
a)
                               Right (Right c
a) -> forall a b. b -> Either a b
Right c
a
  maybeFromSum :: forall u a.
(ObjectSum Op u a, u ~ UnitObject Op, Object Op (Maybe a)) =>
Op (u + a) (Maybe a)
maybeFromSum = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. (a -> b) -> a -> b
$ \case Maybe a
Nothing -> forall a b. a -> Either a b
Left ()
                                 Just a
x -> forall a b. b -> Either a b
Right a
x
  maybeAsSum :: forall u a.
(ObjectSum Op u a, u ~ UnitObject Op, Object Op (Maybe a)) =>
Op (Maybe a) (u + a)
maybeAsSum = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. (a -> b) -> a -> b
$ \case Left () -> forall a. Maybe a
Nothing
                               Right a
x -> forall a. a -> Maybe a
Just a
x
  boolFromSum :: forall u.
(ObjectSum Op u u, u ~ UnitObject Op, Object Op Bool) =>
Op (u + u) Bool
boolFromSum = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. (a -> b) -> a -> b
$ \case Bool
False -> forall a b. a -> Either a b
Left ()
                                Bool
True -> forall a b. b -> Either a b
Right ()
  boolAsSum :: forall u.
(ObjectSum Op u u, u ~ UnitObject Op, Object Op Bool) =>
Op Bool (u + u)
boolAsSum = forall a b. (b -> a) -> Op a b
Hask.Op forall a b. (a -> b) -> a -> b
$ \case Left () -> Bool
False
                              Right () -> Bool
True

instance (CoCartesian f, o (ZeroObject f)) => CoCartesian (o⊢f) where
  type SumObjects (o⊢f) a b = (SumObjects f a b)
  type ZeroObject (o⊢f) = ZeroObject f

  coSwap :: forall a b.
(ObjectSum (o ⊢ f) a b, ObjectSum (o ⊢ f) b a) =>
(⊢) o f (a + b) (b + a)
coSwap = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap
  attachZero :: forall a zero.
(Object (o ⊢ f) a, zero ~ ZeroObject (o ⊢ f),
 ObjectSum (o ⊢ f) a zero) =>
(⊢) o f a (a + zero)
attachZero = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
attachZero
  detachZero :: forall a zero.
(Object (o ⊢ f) a, zero ~ ZeroObject (o ⊢ f),
 ObjectSum (o ⊢ f) a zero) =>
(⊢) o f (a + zero) a
detachZero = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero
  coRegroup :: forall a c b.
(Object (o ⊢ f) a, Object (o ⊢ f) c, ObjectSum (o ⊢ f) a b,
 ObjectSum (o ⊢ f) b c, ObjectSum (o ⊢ f) a (b + c),
 ObjectSum (o ⊢ f) (a + b) c) =>
(⊢) o f (a + (b + c)) ((a + b) + c)
coRegroup = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a c b.
(CoCartesian k, 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
  coRegroup' :: forall a c b.
(Object (o ⊢ f) a, Object (o ⊢ f) c, ObjectSum (o ⊢ f) a b,
 ObjectSum (o ⊢ f) b c, ObjectSum (o ⊢ f) a (b + c),
 ObjectSum (o ⊢ f) (a + b) c) =>
(⊢) o f ((a + b) + c) (a + (b + c))
coRegroup' = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a c b.
(CoCartesian k, 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'
  maybeAsSum :: forall u a.
(ObjectSum (o ⊢ f) u a, u ~ UnitObject (o ⊢ f),
 Object (o ⊢ f) (Maybe a)) =>
(⊢) o f (Maybe a) (u + a)
maybeAsSum = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (Maybe a) (u + a)
maybeAsSum
  maybeFromSum :: forall u a.
(ObjectSum (o ⊢ f) u a, u ~ UnitObject (o ⊢ f),
 Object (o ⊢ f) (Maybe a)) =>
(⊢) o f (u + a) (Maybe a)
maybeFromSum = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (u + a) (Maybe a)
maybeFromSum
  boolAsSum :: forall u.
(ObjectSum (o ⊢ f) u u, u ~ UnitObject (o ⊢ f),
 Object (o ⊢ f) Bool) =>
(⊢) o f Bool (u + u)
boolAsSum = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k Bool (u + u)
boolAsSum
  boolFromSum :: forall u.
(ObjectSum (o ⊢ f) u u, u ~ UnitObject (o ⊢ f),
 Object (o ⊢ f) Bool) =>
(⊢) o f (u + u) Bool
boolFromSum = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k (u + u) Bool
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 = forall (k :: * -> * -> *) a b c.
(Curry k, ObjectPair k a b, ObjectMorphism k b c) =>
k a (k b c) -> k (a, b) c
uncurry forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
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 :: forall a b c.
(ObjectPair (->) a b, ObjectMorphism (->) b c) =>
(a -> (b -> c)) -> (a, b) -> c
uncurry = forall a b c. (a -> b -> c) -> (a, b) -> c
Prelude.uncurry
  curry :: forall a b c.
(ObjectPair (->) a b, ObjectMorphism (->) b c) =>
((a, b) -> c) -> a -> (b -> c)
curry = forall a b c. ((a, b) -> c) -> a -> b -> c
Prelude.curry
  apply :: forall a b.
(ObjectMorphism (->) a b, ObjectPair (->) (a -> b) a) =>
(a -> b, a) -> b
apply (a -> b
f,a
x) = a -> b
f a
x
      

instance (Curry f, o (UnitObject f)) => Curry (o⊢f) where
  type MorphObjects (o⊢f) a c = ( MorphObjects f a c, f ~ (->) )
  uncurry :: forall a b c.
(ObjectPair (o ⊢ f) a b, ObjectMorphism (o ⊢ f) b c) =>
(⊢) o f a ((⊢) o f b c) -> (⊢) o f (a, b) c
uncurry (ConstrainedMorphism f a ((⊢) o f b c)
f) = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall a b. (a -> b) -> a -> b
$ \(a
a,b
b) -> forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
Category k =>
(⊢) o k a b -> k a b
unconstrained (f a ((⊢) o f b c)
f a
a) b
b
  curry :: forall a b c.
(ObjectPair (o ⊢ f) a b, ObjectMorphism (o ⊢ f) b c) =>
(⊢) o f (a, b) c -> (⊢) o f a ((⊢) o f b c)
curry (ConstrainedMorphism f (a, b) c
f) = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall a b. (a -> b) -> a -> b
$ \a
a -> forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall a b. (a -> b) -> a -> b
$ \b
b -> f (a, b) c
f (a
a, b
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 { forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
GenericAgent k a v -> k a v
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 :: forall (k :: * -> * -> *) a b.
(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 forall q. Object k q => GenericAgent k q a -> GenericAgent k q b
f = forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
GenericAgent k a v -> k a v
runGenericAgent forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall q. Object k q => GenericAgent k q a -> GenericAgent k q b
f forall a b. (a -> b) -> a -> b
$ forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
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 :: forall (k :: * -> * -> *) a b c.
(HasAgent k, Object k a, Object k b, Object k c) =>
k b c -> GenericAgent k a b -> GenericAgent k a c
genericAgentMap k b c
m (GenericAgent k a b
v) = forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent forall a b. (a -> b) -> a -> b
$ k b c
m forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a b
v



instance HasAgent (->) where
  type AgentVal (->) a b = b
  alg :: forall a b.
(Object (->) a, Object (->) b) =>
(forall q. Object (->) q => AgentVal (->) q a -> AgentVal (->) q b)
-> a -> b
alg forall q. Object (->) q => AgentVal (->) q a -> AgentVal (->) q b
f = forall q. Object (->) q => AgentVal (->) q a -> AgentVal (->) q b
f
  $~ :: forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> AgentVal (->) a b -> AgentVal (->) a c
($~) = forall a b. (a -> b) -> a -> b
($)

instance HasAgent Discrete where
  alg :: forall a b.
(Object Discrete a, Object Discrete b) =>
(forall q.
 Object Discrete q =>
 AgentVal Discrete q a -> AgentVal Discrete q b)
-> Discrete a b
alg = forall (k :: * -> * -> *) a b.
(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
  $~ :: forall a b c.
(Object Discrete a, Object Discrete b, Object Discrete c) =>
Discrete b c -> AgentVal Discrete a b -> AgentVal Discrete a c
($~) = forall (k :: * -> * -> *) a b c.
(HasAgent k, Object k a, Object k b, Object k c) =>
k b c -> GenericAgent k a b -> GenericAgent k a c
genericAgentMap

instance Category Coercion where
  id :: forall (a :: κ). Object Coercion a => Coercion a a
id = forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
Hask.id
  . :: forall (a :: κ) (b :: κ) (c :: κ).
(Object Coercion a, Object Coercion b, Object Coercion c) =>
Coercion b c -> Coercion a b -> Coercion a c
(.) = forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
(Hask..)


infixr 3 :***:

data ProductCategory k l p q = k (LFactor p) (LFactor q) :***: l (RFactor p) (RFactor q)

type (×) = ProductCategory

instance (Category k, Category l) => Category (k×l) where
  type Object (k×l) o = (IsProduct o, Object k (LFactor o), Object l (RFactor o))
  id :: forall a. Object (k × l) a => (×) k l a a
id = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
idforall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***:forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  (k (LFactor b) (LFactor c)
f:***:l (RFactor b) (RFactor c)
g) . :: forall a b c.
(Object (k × l) a, Object (k × l) b, Object (k × l) c) =>
(×) k l b c -> (×) k l a b -> (×) k l a c
. (k (LFactor a) (LFactor b)
h:***:l (RFactor a) (RFactor b)
i) = (k (LFactor b) (LFactor c)
fforall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
.k (LFactor a) (LFactor b)
h)forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***:(l (RFactor b) (RFactor c)
gforall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
.l (RFactor a) (RFactor b)
i)

instance (Cartesian k, Cartesian l) => Cartesian (k×l) where
  type UnitObject (k×l) = ProductCatObj (UnitObject k) (UnitObject l)
  type PairObjects (k×l) a b = ( PairObjects k (LFactor a) (LFactor b)
                               , PairObjects l (RFactor a) (RFactor b) )
  swap :: forall a b.
(ObjectPair (k × l) a b, ObjectPair (k × l) b a) =>
(×) k l (a, b) (b, a)
swap = forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap
  attachUnit :: forall unit a.
(unit ~ UnitObject (k × l), ObjectPair (k × l) a unit) =>
(×) k l a (a, unit)
attachUnit = forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit
  detachUnit :: forall unit a.
(unit ~ UnitObject (k × l), ObjectPair (k × l) a unit) =>
(×) k l (a, unit) a
detachUnit = forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit
  regroup :: forall a b c.
(ObjectPair (k × l) a b, ObjectPair (k × l) b c,
 ObjectPair (k × l) a (b, c), ObjectPair (k × l) (a, b) c) =>
(×) k l (a, (b, c)) ((a, b), c)
regroup = forall (k :: * -> * -> *) a b c.
(Cartesian k, 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 forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: forall (k :: * -> * -> *) a b c.
(Cartesian k, 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
  regroup' :: forall a b c.
(ObjectPair (k × l) a b, ObjectPair (k × l) b c,
 ObjectPair (k × l) a (b, c), ObjectPair (k × l) (a, b) c) =>
(×) k l ((a, b), c) (a, (b, c))
regroup' = forall (k :: * -> * -> *) a b c.
(Cartesian k, 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' forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: forall (k :: * -> * -> *) a b c.
(Cartesian k, 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'