-- |
-- 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
            -- * 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
#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 :: Discrete a a
id = Discrete a a
forall k (a :: k). Discrete a a
Refl
  Discrete b c
Refl . :: Discrete b c -> Discrete a b -> Discrete a c
. Discrete a b
Refl = Discrete a c
forall k (a :: k). Discrete a a
Refl

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

instance Category Hask.Op where
  id :: Op a a
id = Op a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
Hask.id
  . :: Op b c -> Op a b -> Op a 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 :: 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 { 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 :: k a b -> (⊢) o k a b
constrained = k a b -> (⊢) o k a b
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 :: (⊢) o k a b -> k a b
unconstrained = (⊢) o k a b -> k a b
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 :: (⊢) isObj k a a
id = k a a -> (⊢) isObj k a a
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k a a
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ConstrainedMorphism k b c
f . :: (⊢) isObj k b c -> (⊢) isObj k a b -> (⊢) isObj k a c
. ConstrainedMorphism k a b
g = k a c -> (⊢) isObj k a c
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (k a c -> (⊢) isObj k a c) -> k a c -> (⊢) isObj k a c
forall a b. (a -> b) -> a -> b
$ k b c
f k b c -> k a b -> k a c
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 = k a (a, u)
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 = k (a, u) a
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 = k (a, u) (u, a)
forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap k (a, u) (u, a) -> k a (a, u) -> k a (u, a)
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 (a, u)
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 = k (a, u) a
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit k (a, u) a -> k (u, a) (a, u) -> k (u, a) a
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 (u, a) (a, u)
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 = k (a, (b, c)) ((a, b), c)
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 = k ((a, b), c) (a, (b, c))
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 = k a (a + u)
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 = k (a + u) a
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 = k (a + u) (u + a)
forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap k (a + u) (u + a) -> k a (a + u) -> k a (u + a)
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 (a + u)
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 = k (a + u) a
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero k (a + u) a -> k (u + a) (a + u) -> k (u + a) a
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 (u + a) (a + u)
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 = k (a + (b + c)) ((a + b) + c)
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 = k ((a + b) + c) (a + (b + c))
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 :: (a, b) -> (b, a)
swap = \(a
a,b
b) -> (b
b,a
a)
  attachUnit :: a -> (a, unit)
attachUnit = \a
a -> (a
a, ())
  detachUnit :: (a, unit) -> a
detachUnit = \(a
a, ()) -> a
a
  regroup :: (a, (b, c)) -> ((a, b), c)
regroup = \(a
a, (b
b, c
c)) -> ((a
a, b
b), c
c)
  regroup' :: ((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 :: Op (a, b) (b, a)
swap = ((b, a) -> (a, b)) -> Op (a, b) (b, a)
forall a b. (b -> a) -> Op a b
Hask.Op (((b, a) -> (a, b)) -> Op (a, b) (b, a))
-> ((b, a) -> (a, b)) -> Op (a, b) (b, a)
forall a b. (a -> b) -> a -> b
$ \(b
a,a
b) -> (a
b,b
a)
  attachUnit :: Op a (a, unit)
attachUnit = ((a, ()) -> a) -> Op a (a, ())
forall a b. (b -> a) -> Op a b
Hask.Op (((a, ()) -> a) -> Op a (a, ())) -> ((a, ()) -> a) -> Op a (a, ())
forall a b. (a -> b) -> a -> b
$ \(a
a, ()) -> a
a
  detachUnit :: Op (a, unit) a
detachUnit = (a -> (a, ())) -> Op (a, ()) a
forall a b. (b -> a) -> Op a b
Hask.Op ((a -> (a, ())) -> Op (a, ()) a) -> (a -> (a, ())) -> Op (a, ()) a
forall a b. (a -> b) -> a -> b
$ \a
a -> (a
a, ())
  regroup :: Op (a, (b, c)) ((a, b), c)
regroup = (((a, b), c) -> (a, (b, c))) -> Op (a, (b, c)) ((a, b), c)
forall a b. (b -> a) -> Op a b
Hask.Op ((((a, b), c) -> (a, (b, c))) -> Op (a, (b, c)) ((a, b), c))
-> (((a, b), c) -> (a, (b, c))) -> Op (a, (b, c)) ((a, b), c)
forall a b. (a -> b) -> a -> b
$ \((a
a, b
b), c
c) -> (a
a, (b
b, c
c))
  regroup' :: Op ((a, b), c) (a, (b, c))
regroup' = ((a, (b, c)) -> ((a, b), c)) -> Op ((a, b), c) (a, (b, c))
forall a b. (b -> a) -> Op a b
Hask.Op (((a, (b, c)) -> ((a, b), c)) -> Op ((a, b), c) (a, (b, c)))
-> ((a, (b, c)) -> ((a, b), c)) -> Op ((a, b), c) (a, (b, c))
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 :: (⊢) o f (a, b) (b, a)
swap = f (a, b) (b, a) -> (⊢) o f (a, b) (b, a)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f (a, b) (b, a)
forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap
  attachUnit :: (⊢) o f a (a, unit)
attachUnit = f a (a, unit) -> (⊢) o f a (a, unit)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f a (a, unit)
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit
  detachUnit :: (⊢) o f (a, unit) a
detachUnit = f (a, unit) a -> (⊢) o f (a, unit) a
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f (a, unit) a
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit
  regroup :: (⊢) o f (a, (b, c)) ((a, b), c)
regroup = f (a, (b, c)) ((a, b), c) -> (⊢) o f (a, (b, c)) ((a, b), c)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f (a, (b, c)) ((a, b), c)
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' :: (⊢) o f ((a, b), c) (a, (b, c))
regroup' = f ((a, b), c) (a, (b, c)) -> (⊢) o f ((a, b), c) (a, (b, c))
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f ((a, b), c) (a, (b, c))
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 :: (a + b) -> b + a
coSwap (Left a
a) = a -> b + a
forall a b. b -> Either a b
Right a
a
  coSwap (Right b
a) = b -> b + a
forall a b. a -> Either a b
Left b
a
  attachZero :: a -> a + zero
attachZero = a -> a + zero
forall a b. a -> Either a b
Left
  detachZero :: (a + zero) -> a
detachZero (Left a
a) = a
a
  detachZero (Right zero
void) = Void -> a
forall a. Void -> a
absurd zero
Void
void
  coRegroup :: (a + (b + c)) -> (a + b) + c
coRegroup (Left a
a) = (a + b) -> (a + b) + c
forall a b. a -> Either a b
Left ((a + b) -> (a + b) + c) -> (a + b) -> (a + b) + c
forall a b. (a -> b) -> a -> b
$ a -> a + b
forall a b. a -> Either a b
Left a
a
  coRegroup (Right (Left b
a)) = (a + b) -> (a + b) + c
forall a b. a -> Either a b
Left ((a + b) -> (a + b) + c) -> (a + b) -> (a + b) + c
forall a b. (a -> b) -> a -> b
$ b -> a + b
forall a b. b -> Either a b
Right b
a
  coRegroup (Right (Right c
a)) = c -> (a + b) + c
forall a b. b -> Either a b
Right c
a
  coRegroup' :: ((a + b) + c) -> a + (b + c)
coRegroup' (Left (Left a
a)) = a -> a + (b + c)
forall a b. a -> Either a b
Left a
a
  coRegroup' (Left (Right b
a)) = (b + c) -> a + (b + c)
forall a b. b -> Either a b
Right ((b + c) -> a + (b + c)) -> (b + c) -> a + (b + c)
forall a b. (a -> b) -> a -> b
$ b -> b + c
forall a b. a -> Either a b
Left b
a
  coRegroup' (Right c
a) = (b + c) -> a + (b + c)
forall a b. b -> Either a b
Right ((b + c) -> a + (b + c)) -> (b + c) -> a + (b + c)
forall a b. (a -> b) -> a -> b
$ c -> b + c
forall a b. b -> Either a b
Right c
a
  maybeAsSum :: Maybe a -> u + a
maybeAsSum Maybe a
Nothing = () -> Either () a
forall a b. a -> Either a b
Left ()
  maybeAsSum (Just a
x) = a -> u + a
forall a b. b -> Either a b
Right a
x
  maybeFromSum :: (u + a) -> Maybe a
maybeFromSum (Left ()) = Maybe a
forall a. Maybe a
Nothing
  maybeFromSum (Right a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
  boolAsSum :: Bool -> u + u
boolAsSum Bool
False = () -> Either () u
forall a b. a -> Either a b
Left ()
  boolAsSum Bool
True = () -> Either u ()
forall a b. b -> Either a b
Right ()
  boolFromSum :: (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 :: Op (a + b) (b + a)
coSwap = ((b + a) -> a + b) -> Op (a + b) (b + a)
forall a b. (b -> a) -> Op a b
Hask.Op (((b + a) -> a + b) -> Op (a + b) (b + a))
-> ((b + a) -> a + b) -> Op (a + b) (b + a)
forall a b. (a -> b) -> a -> b
$ \case Right a
a -> a -> a + b
forall a b. a -> Either a b
Left a
a
                           Left b
a -> b -> a + b
forall a b. b -> Either a b
Right b
a
  attachZero :: Op a (a + zero)
attachZero = (Either a Void -> a) -> Op a (Either a Void)
forall a b. (b -> a) -> Op a b
Hask.Op ((Either a Void -> a) -> Op a (Either a Void))
-> (Either a Void -> a) -> Op a (Either a Void)
forall a b. (a -> b) -> a -> b
$ \case Left a
a -> a
a
                               Right Void
void -> Void -> a
forall a. Void -> a
absurd Void
void
  detachZero :: Op (a + zero) a
detachZero = (a -> a + zero) -> Op (a + zero) a
forall a b. (b -> a) -> Op a b
Hask.Op a -> a + zero
forall a b. a -> Either a b
Left
  coRegroup :: Op (a + (b + c)) ((a + b) + c)
coRegroup = (((a + b) + c) -> a + (b + c)) -> Op (a + (b + c)) ((a + b) + c)
forall a b. (b -> a) -> Op a b
Hask.Op ((((a + b) + c) -> a + (b + c)) -> Op (a + (b + c)) ((a + b) + c))
-> (((a + b) + c) -> a + (b + c)) -> Op (a + (b + c)) ((a + b) + c)
forall a b. (a -> b) -> a -> b
$ \case Left (Left a
a) -> a -> a + (b + c)
forall a b. a -> Either a b
Left a
a
                              Left (Right b
a) -> ((b + c) -> a + (b + c)
forall a b. b -> Either a b
Right (b -> b + c
forall a b. a -> Either a b
Left b
a))
                              Right c
a -> (b + c) -> a + (b + c)
forall a b. b -> Either a b
Right (c -> b + c
forall a b. b -> Either a b
Right c
a)
  coRegroup' :: Op ((a + b) + c) (a + (b + c))
coRegroup' = ((a + (b + c)) -> (a + b) + c) -> Op ((a + b) + c) (a + (b + c))
forall a b. (b -> a) -> Op a b
Hask.Op (((a + (b + c)) -> (a + b) + c) -> Op ((a + b) + c) (a + (b + c)))
-> ((a + (b + c)) -> (a + b) + c) -> Op ((a + b) + c) (a + (b + c))
forall a b. (a -> b) -> a -> b
$ \case (Left a
a) -> (a + b) -> (a + b) + c
forall a b. a -> Either a b
Left (a -> a + b
forall a b. a -> Either a b
Left a
a)
                               Right (Left b
a) -> (a + b) -> (a + b) + c
forall a b. a -> Either a b
Left (b -> a + b
forall a b. b -> Either a b
Right b
a)
                               Right (Right c
a) -> c -> (a + b) + c
forall a b. b -> Either a b
Right c
a
  maybeFromSum :: Op (u + a) (Maybe a)
maybeFromSum = (Maybe a -> Either () a) -> Op (Either () a) (Maybe a)
forall a b. (b -> a) -> Op a b
Hask.Op ((Maybe a -> Either () a) -> Op (Either () a) (Maybe a))
-> (Maybe a -> Either () a) -> Op (Either () a) (Maybe a)
forall a b. (a -> b) -> a -> b
$ \case Maybe a
Nothing -> () -> Either () a
forall a b. a -> Either a b
Left ()
                                 Just a
x -> a -> Either () a
forall a b. b -> Either a b
Right a
x
  maybeAsSum :: Op (Maybe a) (u + a)
maybeAsSum = (Either () a -> Maybe a) -> Op (Maybe a) (Either () a)
forall a b. (b -> a) -> Op a b
Hask.Op ((Either () a -> Maybe a) -> Op (Maybe a) (Either () a))
-> (Either () a -> Maybe a) -> Op (Maybe a) (Either () a)
forall a b. (a -> b) -> a -> b
$ \case Left () -> Maybe a
forall a. Maybe a
Nothing
                               Right a
x -> a -> Maybe a
forall a. a -> Maybe a
Just a
x
  boolFromSum :: Op (u + u) Bool
boolFromSum = (Bool -> Either () ()) -> Op (Either () ()) Bool
forall a b. (b -> a) -> Op a b
Hask.Op ((Bool -> Either () ()) -> Op (Either () ()) Bool)
-> (Bool -> Either () ()) -> Op (Either () ()) Bool
forall a b. (a -> b) -> a -> b
$ \case Bool
False -> () -> Either () ()
forall a b. a -> Either a b
Left ()
                                Bool
True -> () -> Either () ()
forall a b. b -> Either a b
Right ()
  boolAsSum :: Op Bool (u + u)
boolAsSum = (Either () () -> Bool) -> Op Bool (Either () ())
forall a b. (b -> a) -> Op a b
Hask.Op ((Either () () -> Bool) -> Op Bool (Either () ()))
-> (Either () () -> Bool) -> Op Bool (Either () ())
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 :: (⊢) o f (a + b) (b + a)
coSwap = f (a + b) (b + a) -> (⊢) o f (a + b) (b + a)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f (a + b) (b + a)
forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap
  attachZero :: (⊢) o f a (a + zero)
attachZero = f a (a + zero) -> (⊢) o f a (a + zero)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f a (a + zero)
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
attachZero
  detachZero :: (⊢) o f (a + zero) a
detachZero = f (a + zero) a -> (⊢) o f (a + zero) a
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f (a + zero) a
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero
  coRegroup :: (⊢) o f (a + (b + c)) ((a + b) + c)
coRegroup = f (a + (b + c)) ((a + b) + c)
-> (⊢) o f (a + (b + c)) ((a + b) + c)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f (a + (b + c)) ((a + b) + c)
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' :: (⊢) o f ((a + b) + c) (a + (b + c))
coRegroup' = f ((a + b) + c) (a + (b + c))
-> (⊢) o f ((a + b) + c) (a + (b + c))
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f ((a + b) + c) (a + (b + c))
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 :: (⊢) o f (Maybe a) (u + a)
maybeAsSum = f (Maybe a) (u + a) -> (⊢) o f (Maybe a) (u + a)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f (Maybe a) (u + a)
forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (Maybe a) (u + a)
maybeAsSum
  maybeFromSum :: (⊢) o f (u + a) (Maybe a)
maybeFromSum = f (u + a) (Maybe a) -> (⊢) o f (u + a) (Maybe a)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f (u + a) (Maybe a)
forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (u + a) (Maybe a)
maybeFromSum
  boolAsSum :: (⊢) o f Bool (u + u)
boolAsSum = f Bool (u + u) -> (⊢) o f Bool (u + u)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f Bool (u + u)
forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k Bool (u + u)
boolAsSum
  boolFromSum :: (⊢) o f (u + u) Bool
boolFromSum = f (u + u) Bool -> (⊢) o f (u + u) Bool
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism f (u + u) Bool
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 = k (k a b) (k a b) -> k (k a b, a) b
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 k (k a b) (k a b)
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 :: (a -> b -> c) -> (a, b) -> c
uncurry = (a -> b -> c) -> (a, b) -> c
forall a b c. (a -> b -> c) -> (a, b) -> c
Prelude.uncurry
  curry :: ((a, b) -> c) -> a -> b -> c
curry = ((a, b) -> c) -> a -> b -> c
forall a b c. ((a, b) -> c) -> a -> b -> c
Prelude.curry
  apply :: (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 :: (⊢) o f a ((⊢) o f b c) -> (⊢) o f (a, b) c
uncurry (ConstrainedMorphism f a ((⊢) o f b c)
f) = f (a, b) c -> (⊢) o f (a, b) c
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (f (a, b) c -> (⊢) o f (a, b) c) -> f (a, b) c -> (⊢) o f (a, b) c
forall a b. (a -> b) -> a -> b
$ \(a
a,b
b) -> (⊢) o (->) b c -> b -> c
forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
Category k =>
(⊢) o k a b -> k a b
unconstrained (f a ((⊢) o f b c)
a -> (⊢) o (->) b c
f a
a) b
b
  curry :: (⊢) o f (a, b) c -> (⊢) o f a ((⊢) o f b c)
curry (ConstrainedMorphism f (a, b) c
f) = f a ((⊢) o f b c) -> (⊢) o f a ((⊢) o f b c)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (f a ((⊢) o f b c) -> (⊢) o f a ((⊢) o f b c))
-> f a ((⊢) o f b c) -> (⊢) o f a ((⊢) o f b c)
forall a b. (a -> b) -> a -> b
$ \a
a -> (b -> c) -> ConstrainedCategory (->) o b c
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism ((b -> c) -> ConstrainedCategory (->) o b c)
-> (b -> c) -> ConstrainedCategory (->) o b c
forall a b. (a -> b) -> a -> b
$ \b
b -> f (a, b) c
(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 { 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 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 = GenericAgent k a b -> k a b
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
GenericAgent k a v -> k a v
runGenericAgent (GenericAgent k a b -> k a b)
-> (GenericAgent k a a -> GenericAgent k a b)
-> GenericAgent k a a
-> k a b
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
. GenericAgent k a a -> GenericAgent k a b
forall q. Object k q => GenericAgent k q a -> GenericAgent k q b
f (GenericAgent k a a -> k a b) -> GenericAgent k a a -> k a b
forall a b. (a -> b) -> a -> b
$ k a a -> GenericAgent k a a
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent k a a
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 :: k b c -> GenericAgent k a b -> GenericAgent k a c
genericAgentMap k b c
m (GenericAgent k a b
v) = k a c -> GenericAgent k a c
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent (k a c -> GenericAgent k a c) -> k a c -> GenericAgent k a c
forall a b. (a -> b) -> a -> b
$ k b c
m k b c -> k a b -> k a c
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 q. Object (->) q => AgentVal (->) q a -> AgentVal (->) q b)
-> a -> b
alg forall q. Object (->) q => AgentVal (->) q a -> AgentVal (->) q b
f = a -> b
forall q. Object (->) q => AgentVal (->) q a -> AgentVal (->) q b
f
  $~ :: (b -> c) -> AgentVal (->) a b -> AgentVal (->) a c
($~) = (b -> c) -> AgentVal (->) a b -> AgentVal (->) a c
forall a b. (a -> b) -> a -> b
($)

instance HasAgent Discrete where
  alg :: (forall q.
 Object Discrete q =>
 AgentVal Discrete q a -> AgentVal Discrete q b)
-> Discrete a b
alg = (forall q.
 Object Discrete q =>
 AgentVal Discrete q a -> AgentVal Discrete q b)
-> Discrete a b
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
  $~ :: Discrete b c -> AgentVal Discrete a b -> AgentVal Discrete a 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 :: Coercion a a
id = Coercion a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
Hask.id
  . :: Coercion b c -> Coercion a b -> Coercion a 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..)