{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE UndecidableSuperClasses #-}
#endif
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Control.Arrow.Constrained (
Arrow, Morphism(..), PreArrow(..), WellPointed(..),ObjectPoint, EnhancedCat(..)
, ArrowChoice, MorphChoice(..), PreArrChoice(..)
, SPDistribute(..)
, Function, ($)
, (>>>), (<<<)
, CartesianAgent(..)
, genericAgentCombine, genericUnit, genericAlg1to2, genericAlg2to1, genericAlg2to2
, PointAgent(..), genericPoint
, choose, ifThenElse
, follow, flout, pretend, swallow, pretendLike, swallowLike
) where
import Prelude hiding (id, const, fst, snd, (.), ($), Functor(..), Monad(..), (=<<))
import Control.Category.Constrained
import qualified Control.Category.Hask as Hask
import GHC.Exts (Constraint)
import Data.Tagged
import Data.Void
import Data.Coerce
import Data.Type.Coercion
import qualified Control.Arrow as Arr
import Control.Category.Discrete
import qualified Data.Functor.Contravariant as Hask
infixr 1 >>>, <<<
infixr 3 &&&, ***
(>>>) :: (Category k, Object k a, Object k b, Object k c)
=> k a b -> k b c -> k a c
>>> :: k a b -> k b c -> k a c
(>>>) = (k b c -> k a b -> k a c) -> k a b -> k b c -> k a c
forall a b c. (a -> b -> c) -> b -> a -> c
flip 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
(.)
(<<<) :: (Category k, Object k a, Object k b, Object k c)
=> k b c -> k a b -> k a c
<<< :: k b c -> k a b -> k a c
(<<<) = 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
(.)
class (Cartesian a) => Morphism a where
first :: ( ObjectPair a b d, ObjectPair a c d )
=> a b c -> a (b, d) (c, d)
first = (a b c -> a d d -> a (b, d) (c, d)
forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
***a d d
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id)
second :: ( ObjectPair a d b, ObjectPair a d c )
=> a b c -> a (d, b) (d, c)
second = (a d d
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
ida d d -> a b c -> a (d, b) (d, c)
forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
***)
(***) :: ( ObjectPair a b b', ObjectPair a c c' )
=> a b c -> a b' c' -> a (b,b') (c,c')
class (CoCartesian a) => MorphChoice a where
left :: ( ObjectSum a b d, ObjectSum a c d )
=> a b c -> a (b+d) (c+d)
left = (a b c -> a d d -> a (b + d) (c + d)
forall (a :: * -> * -> *) b b' c c'.
(MorphChoice a, ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
+++a d d
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id)
right :: ( ObjectSum a d b, ObjectSum a d c )
=> a b c -> a (d+b) (d+c)
right = (a d d
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
ida d d -> a b c -> a (d + b) (d + c)
forall (a :: * -> * -> *) b b' c c'.
(MorphChoice a, ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
+++)
(+++) :: ( ObjectSum a b b', ObjectSum a c c' )
=> a b c -> a b' c' -> a (b+b') (c+c')
class (Morphism a) => PreArrow a where
(&&&) :: ( Object a b, ObjectPair a c c' )
=> a b c -> a b c' -> a b (c,c')
terminal :: ( Object a b ) => a b (UnitObject a)
fst :: (ObjectPair a x y) => a (x,y) x
snd :: (ObjectPair a x y) => a (x,y) y
infixr 2 |||
class (MorphChoice k) => PreArrChoice k where
(|||) :: ( ObjectSum k b b', Object k c )
=> k b c -> k b' c -> k (b+b') c
initial :: ( Object k b ) => k (ZeroObject k) b
coFst :: (ObjectSum k a b) => k a (a+b)
coSnd :: (ObjectSum k a b) => k b (a+b)
class (PreArrow k, PreArrChoice k) => SPDistribute k where
distribute :: ( ObjectSum k (a,b) (a,c), ObjectPair k a (b+c)
, ObjectSum k b c, PairObjects k a b, PairObjects k a c )
=> k (a, b+c) ((a,b)+(a,c))
unDistribute :: ( ObjectSum k (a,b) (a,c), ObjectPair k a (b+c)
, ObjectSum k b c, PairObjects k a b, PairObjects k a c )
=> k ((a,b)+(a,c)) (a, b+c)
boolAsSwitch :: ( ObjectSum k a a, ObjectPair k Bool a ) => k (Bool,a) (a+a)
boolFromSwitch :: ( ObjectSum k a a, ObjectPair k Bool a ) => k (a+a) (Bool,a)
instance ( SPDistribute k
, ObjectSum k (a,b) (a,c), ObjectPair k a (b+c)
, ObjectSum k b c, PairObjects k a b, PairObjects k a c
) => Isomorphic k (a, b+c) ((a,b)+(a,c)) where
iso :: k (a, b + c) ((a, b) + (a, c))
iso = k (a, b + c) ((a, b) + (a, c))
forall (k :: * -> * -> *) a b c.
(SPDistribute k, ObjectSum k (a, b) (a, c), ObjectPair k a (b + c),
ObjectSum k b c, PairObjects k a b, PairObjects k a c) =>
k (a, b + c) ((a, b) + (a, c))
distribute
instance ( SPDistribute k
, ObjectSum k (a,b) (a,c), ObjectPair k a (b+c)
, ObjectSum k b c, PairObjects k a b, PairObjects k a c
) => Isomorphic k ((a,b)+(a,c)) (a, b+c) where
iso :: k ((a, b) + (a, c)) (a, b + c)
iso = k ((a, b) + (a, c)) (a, b + c)
forall (k :: * -> * -> *) a b c.
(SPDistribute k, ObjectSum k (a, b) (a, c), ObjectPair k a (b + c),
ObjectSum k b c, PairObjects k a b, PairObjects k a c) =>
k ((a, b) + (a, c)) (a, b + c)
unDistribute
instance ( SPDistribute k
, ObjectSum k a a, ObjectPair k Bool a
) => Isomorphic k (Bool, a) (a+a) where
iso :: k (Bool, a) (a + a)
iso = k (Bool, a) (a + a)
forall (k :: * -> * -> *) a.
(SPDistribute k, ObjectSum k a a, ObjectPair k Bool a) =>
k (Bool, a) (a + a)
boolAsSwitch
instance ( SPDistribute k
, ObjectSum k a a, ObjectPair k Bool a
) => Isomorphic k (a+a) (Bool, a) where
iso :: k (a + a) (Bool, a)
iso = k (a + a) (Bool, a)
forall (k :: * -> * -> *) a.
(SPDistribute k, ObjectSum k a a, ObjectPair k Bool a) =>
k (a + a) (Bool, a)
boolFromSwitch
class (PreArrow a, ObjectPoint a (UnitObject a)) => WellPointed a where
{-# MINIMAL unit, (globalElement | const) #-}
type PointObject a x :: Constraint
type PointObject a x = ()
globalElement :: (ObjectPoint a x) => x -> a (UnitObject a) x
globalElement = x -> a (UnitObject a) x
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const
unit :: CatTagged a (UnitObject a)
const :: (Object a b, ObjectPoint a x)
=> x -> a b x
const x
x = x -> a (UnitObject a) x
forall (a :: * -> * -> *) x.
(WellPointed a, ObjectPoint a x) =>
x -> a (UnitObject a) x
globalElement x
x a (UnitObject a) x -> a b (UnitObject a) -> a b x
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
. a b (UnitObject a)
forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal
type ObjectPoint k a = (Object k a, PointObject k a)
value :: forall f x . (WellPointed f, Function f, Object f x)
=> f (UnitObject f) x -> x
value :: f (UnitObject f) x -> x
value f (UnitObject f) x
f = f (UnitObject f) x
f f (UnitObject f) x -> UnitObject f -> x
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ Tagged (f (UnitObject f) (UnitObject f)) (UnitObject f)
-> UnitObject f
forall k (s :: k) b. Tagged s b -> b
untag(Tagged (f (UnitObject f) (UnitObject f)) (UnitObject f)
forall (a :: * -> * -> *).
WellPointed a =>
CatTagged a (UnitObject a)
unit :: Tagged (f (UnitObject f) (UnitObject f)) (UnitObject f))
class (Category a, Category k) => EnhancedCat a k where
arr :: (Object k b, Object k c, Object a b, Object a c)
=> k b c -> a b c
instance (Category k) => EnhancedCat k k where
arr :: k b c -> k b c
arr = k b c -> k b c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance EnhancedCat (->) Discrete where
arr :: Discrete b c -> b -> c
arr Discrete b c
Refl = b -> c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance EnhancedCat Coercion Discrete where
arr :: Discrete b c -> Coercion b c
arr Discrete b c
Refl = Coercion b c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance Category f => EnhancedCat (o⊢f) Discrete where
arr :: Discrete b c -> (⊢) o f b c
arr Discrete b c
Refl = (⊢) o f b c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
type Function f = EnhancedCat (->) f
infixr 0 $
($) :: (Function f, Object f a, Object f b) => f a b -> a -> b
f a b
f $ :: f a b -> a -> b
$ a
x = f a b -> a -> b
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr f a b
f a
x
instance (Function f) => EnhancedCat (->) (o⊢f) where
arr :: (⊢) o f b c -> b -> c
arr (ConstrainedMorphism f b c
q) = f b c -> b -> c
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr f b c
q
instance (EnhancedCat Discrete f) => EnhancedCat Discrete (o⊢f) where
arr :: (⊢) o f b c -> Discrete b c
arr (ConstrainedMorphism f b c
q) = f b c -> Discrete b c
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr f b c
q
instance EnhancedCat (->) Coercion where
arr :: Coercion b c -> b -> c
arr = Coercion b c -> b -> c
forall a b. Coercion a b -> a -> b
coerceWith
type Arrow a k = (WellPointed a, EnhancedCat a k)
type ArrowChoice a k = (WellPointed a, PreArrChoice a, EnhancedCat a k)
instance Morphism (->) where
first :: (b -> c) -> (b, d) -> (c, d)
first = (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
Arr.first
second :: (b -> c) -> (d, b) -> (d, c)
second = (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
Arr.second
*** :: (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
(***) = (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
(Arr.***)
instance MorphChoice (->) where
left :: (b -> c) -> (b + d) -> c + d
left = (b -> c) -> (b + d) -> c + d
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
Arr.left
right :: (b -> c) -> (d + b) -> d + c
right = (b -> c) -> (d + b) -> d + c
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either d b) (Either d c)
Arr.right
+++ :: (b -> c) -> (b' -> c') -> (b + b') -> c + c'
(+++) = (b -> c) -> (b' -> c') -> (b + b') -> c + c'
forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
(Arr.+++)
instance PreArrow (->) where
&&& :: (b -> c) -> (b -> c') -> b -> (c, c')
(&&&) = (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
(Arr.&&&)
fst :: (x, y) -> x
fst (x
a,y
_) = x
a
snd :: (x, y) -> y
snd (x
_,y
b) = y
b
terminal :: b -> UnitObject (->)
terminal = () -> b -> ()
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const ()
instance PreArrChoice (->) where
||| :: (b -> c) -> (b' -> c) -> (b + b') -> c
(|||) = (b -> c) -> (b' -> c) -> (b + b') -> c
forall (a :: * -> * -> *) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
(Arr.|||)
coFst :: a -> a + b
coFst a
a = a -> a + b
forall a b. a -> Either a b
Left a
a
coSnd :: b -> a + b
coSnd b
b = b -> a + b
forall a b. b -> Either a b
Right b
b
initial :: ZeroObject (->) -> b
initial = ZeroObject (->) -> b
forall a. Void -> a
absurd
instance SPDistribute (->) where
distribute :: (a, b + c) -> (a, b) + (a, c)
distribute (a
a, Left b
b) = (a, b) -> (a, b) + (a, c)
forall a b. a -> Either a b
Left (a
a,b
b)
distribute (a
a, Right c
c) = (a, c) -> (a, b) + (a, c)
forall a b. b -> Either a b
Right (a
a,c
c)
unDistribute :: ((a, b) + (a, c)) -> (a, b + c)
unDistribute (Left (a
a,b
b)) = (a
a, b -> b + c
forall a b. a -> Either a b
Left b
b)
unDistribute (Right (a
a,c
c)) = (a
a, c -> b + c
forall a b. b -> Either a b
Right c
c)
boolAsSwitch :: (Bool, a) -> a + a
boolAsSwitch (Bool
False, a
a) = a -> a + a
forall a b. a -> Either a b
Left a
a
boolAsSwitch (Bool
True, a
a) = a -> a + a
forall a b. b -> Either a b
Right a
a
boolFromSwitch :: (a + a) -> (Bool, a)
boolFromSwitch (Left a
a) = (Bool
False, a
a)
boolFromSwitch (Right a
a) = (Bool
True, a
a)
instance WellPointed (->) where
globalElement :: x -> UnitObject (->) -> x
globalElement = x -> UnitObject (->) -> x
forall a b. a -> b -> a
Hask.const
unit :: CatTagged (->) (UnitObject (->))
unit = () -> Tagged (() -> ()) ()
forall (f :: * -> *) a. Applicative f => a -> f a
Hask.pure ()
const :: x -> b -> x
const = x -> b -> x
forall a b. a -> b -> a
Hask.const
constrainedArr :: (Category k, Category a, o b, o c ) => ( k b c -> a b c )
-> k b c -> (o⊢a) b c
constrainedArr :: (k b c -> a b c) -> k b c -> (⊢) o a b c
constrainedArr k b c -> a b c
ar = a b c -> (⊢) o a b c
forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
(Category k, o a, o b) =>
k a b -> (⊢) o k a b
constrained (a b c -> (⊢) o a b c) -> (k b c -> a b c) -> k b c -> (⊢) o a b 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 b c -> a b c
ar
constrainedFirst :: ( Category a, Cartesian a, ObjectPair a b d, ObjectPair a c d )
=> ( a b c -> a (b, d) (c, d) )
-> (o⊢a) b c -> (o⊢a) (b, d) (c, d)
constrainedFirst :: (a b c -> a (b, d) (c, d)) -> (⊢) o a b c -> (⊢) o a (b, d) (c, d)
constrainedFirst a b c -> a (b, d) (c, d)
fs = a (b, d) (c, d) -> (⊢) o a (b, d) (c, d)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (a (b, d) (c, d) -> (⊢) o a (b, d) (c, d))
-> ((⊢) o a b c -> a (b, d) (c, d))
-> (⊢) o a b c
-> (⊢) o a (b, d) (c, d)
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
. a b c -> a (b, d) (c, d)
fs (a b c -> a (b, d) (c, d))
-> ((⊢) o a b c -> a b c) -> (⊢) o a b c -> a (b, d) (c, d)
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
. (⊢) o a b c -> a b c
forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
Category k =>
(⊢) o k a b -> k a b
unconstrained
constrainedSecond :: ( Category a, Cartesian a, ObjectPair a d b, ObjectPair a d c )
=> ( a b c -> a (d, b) (d, c) )
-> (o⊢a) b c -> (o⊢a) (d, b) (d, c)
constrainedSecond :: (a b c -> a (d, b) (d, c)) -> (⊢) o a b c -> (⊢) o a (d, b) (d, c)
constrainedSecond a b c -> a (d, b) (d, c)
sn = a (d, b) (d, c) -> (⊢) o a (d, b) (d, c)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (a (d, b) (d, c) -> (⊢) o a (d, b) (d, c))
-> ((⊢) o a b c -> a (d, b) (d, c))
-> (⊢) o a b c
-> (⊢) o a (d, b) (d, 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
. a b c -> a (d, b) (d, c)
sn (a b c -> a (d, b) (d, c))
-> ((⊢) o a b c -> a b c) -> (⊢) o a b c -> a (d, b) (d, 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
. (⊢) o a b c -> a b c
forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
Category k =>
(⊢) o k a b -> k a b
unconstrained
instance Morphism Hask.Op where
first :: Op b c -> Op (b, d) (c, d)
first (Hask.Op c -> b
f) = ((c, d) -> (b, d)) -> Op (b, d) (c, d)
forall a b. (b -> a) -> Op a b
Hask.Op (((c, d) -> (b, d)) -> Op (b, d) (c, d))
-> ((c, d) -> (b, d)) -> Op (b, d) (c, d)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (c -> b) -> (c, d) -> (b, d)
forall (a :: * -> * -> *) b d c.
(Morphism a, ObjectPair a b d, ObjectPair a c d) =>
a b c -> a (b, d) (c, d)
first c -> b
f
second :: Op b c -> Op (d, b) (d, c)
second (Hask.Op c -> b
f) = ((d, c) -> (d, b)) -> Op (d, b) (d, c)
forall a b. (b -> a) -> Op a b
Hask.Op (((d, c) -> (d, b)) -> Op (d, b) (d, c))
-> ((d, c) -> (d, b)) -> Op (d, b) (d, c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (c -> b) -> (d, c) -> (d, b)
forall (a :: * -> * -> *) d b c.
(Morphism a, ObjectPair a d b, ObjectPair a d c) =>
a b c -> a (d, b) (d, c)
second c -> b
f
Hask.Op c -> b
f *** :: Op b c -> Op b' c' -> Op (b, b') (c, c')
*** Hask.Op c' -> b'
g = ((c, c') -> (b, b')) -> Op (b, b') (c, c')
forall a b. (b -> a) -> Op a b
Hask.Op (((c, c') -> (b, b')) -> Op (b, b') (c, c'))
-> ((c, c') -> (b, b')) -> Op (b, b') (c, c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ c -> b
f (c -> b) -> (c' -> b') -> (c, c') -> (b, b')
forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
*** c' -> b'
g
instance MorphChoice Hask.Op where
left :: Op b c -> Op (b + d) (c + d)
left (Hask.Op c -> b
f) = ((c + d) -> b + d) -> Op (b + d) (c + d)
forall a b. (b -> a) -> Op a b
Hask.Op (((c + d) -> b + d) -> Op (b + d) (c + d))
-> ((c + d) -> b + d) -> Op (b + d) (c + d)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (c -> b) -> (c + d) -> b + d
forall (a :: * -> * -> *) b d c.
(MorphChoice a, ObjectSum a b d, ObjectSum a c d) =>
a b c -> a (b + d) (c + d)
left c -> b
f
right :: Op b c -> Op (d + b) (d + c)
right (Hask.Op c -> b
f) = ((d + c) -> d + b) -> Op (d + b) (d + c)
forall a b. (b -> a) -> Op a b
Hask.Op (((d + c) -> d + b) -> Op (d + b) (d + c))
-> ((d + c) -> d + b) -> Op (d + b) (d + c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (c -> b) -> (d + c) -> d + b
forall (a :: * -> * -> *) d b c.
(MorphChoice a, ObjectSum a d b, ObjectSum a d c) =>
a b c -> a (d + b) (d + c)
right c -> b
f
Hask.Op c -> b
f +++ :: Op b c -> Op b' c' -> Op (b + b') (c + c')
+++ Hask.Op c' -> b'
g = ((c + c') -> b + b') -> Op (b + b') (c + c')
forall a b. (b -> a) -> Op a b
Hask.Op (((c + c') -> b + b') -> Op (b + b') (c + c'))
-> ((c + c') -> b + b') -> Op (b + b') (c + c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ c -> b
f (c -> b) -> (c' -> b') -> (c + c') -> b + b'
forall (a :: * -> * -> *) b b' c c'.
(MorphChoice a, ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
+++ c' -> b'
g
instance (Morphism a, o (UnitObject a)) => Morphism (o⊢a) where
first :: (⊢) o a b c -> (⊢) o a (b, d) (c, d)
first = (a b c -> a (b, d) (c, d)) -> (⊢) o a b c -> (⊢) o a (b, d) (c, d)
forall (a :: * -> * -> *) b d c (o :: * -> Constraint).
(Category a, Cartesian a, ObjectPair a b d, ObjectPair a c d) =>
(a b c -> a (b, d) (c, d)) -> (⊢) o a b c -> (⊢) o a (b, d) (c, d)
constrainedFirst a b c -> a (b, d) (c, d)
forall (a :: * -> * -> *) b d c.
(Morphism a, ObjectPair a b d, ObjectPair a c d) =>
a b c -> a (b, d) (c, d)
first
second :: (⊢) o a b c -> (⊢) o a (d, b) (d, c)
second = (a b c -> a (d, b) (d, c)) -> (⊢) o a b c -> (⊢) o a (d, b) (d, c)
forall (a :: * -> * -> *) d b c (o :: * -> Constraint).
(Category a, Cartesian a, ObjectPair a d b, ObjectPair a d c) =>
(a b c -> a (d, b) (d, c)) -> (⊢) o a b c -> (⊢) o a (d, b) (d, c)
constrainedSecond a b c -> a (d, b) (d, c)
forall (a :: * -> * -> *) d b c.
(Morphism a, ObjectPair a d b, ObjectPair a d c) =>
a b c -> a (d, b) (d, c)
second
ConstrainedMorphism a b c
a *** :: (⊢) o a b c -> (⊢) o a b' c' -> (⊢) o a (b, b') (c, c')
*** ConstrainedMorphism a b' c'
b = a (b, b') (c, c') -> (⊢) o a (b, b') (c, c')
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (a (b, b') (c, c') -> (⊢) o a (b, b') (c, c'))
-> a (b, b') (c, c') -> (⊢) o a (b, b') (c, c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a b c
a a b c -> a b' c' -> a (b, b') (c, c')
forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a b' c'
b
instance (PreArrow a, o (UnitObject a)) => PreArrow (o⊢a) where
ConstrainedMorphism a b c
a &&& :: (⊢) o a b c -> (⊢) o a b c' -> (⊢) o a b (c, c')
&&& ConstrainedMorphism a b c'
b = a b (c, c') -> (⊢) o a b (c, c')
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (a b (c, c') -> (⊢) o a b (c, c'))
-> a b (c, c') -> (⊢) o a b (c, c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a b c
a a b c -> a b c' -> a b (c, c')
forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& a b c'
b
terminal :: (⊢) o a b (UnitObject (o ⊢ a))
terminal = a b (UnitObject a) -> ConstrainedCategory a o b (UnitObject a)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism a b (UnitObject a)
forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal
fst :: (⊢) o a (x, y) x
fst = a (x, y) x -> (⊢) o a (x, y) x
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism a (x, y) x
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst
snd :: (⊢) o a (x, y) y
snd = a (x, y) y -> (⊢) o a (x, y) y
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism a (x, y) y
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd
instance (WellPointed a, o (UnitObject a)) => WellPointed (o⊢a) where
type PointObject (o⊢a) x = PointObject a x
globalElement :: x -> (⊢) o a (UnitObject (o ⊢ a)) x
globalElement x
x = a (UnitObject a) x -> ConstrainedCategory a o (UnitObject a) x
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (a (UnitObject a) x -> ConstrainedCategory a o (UnitObject a) x)
-> a (UnitObject a) x -> ConstrainedCategory a o (UnitObject a) x
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ x -> a (UnitObject a) x
forall (a :: * -> * -> *) x.
(WellPointed a, ObjectPoint a x) =>
x -> a (UnitObject a) x
globalElement x
x
unit :: CatTagged (o ⊢ a) (UnitObject (o ⊢ a))
unit = CatTagged (o ⊢ a) (UnitObject (o ⊢ a))
forall (a :: * -> * -> *) (o :: * -> Constraint).
(WellPointed a, o (UnitObject a)) =>
CatTagged (o ⊢ a) (UnitObject a)
cstrCatUnit
const :: x -> (⊢) o a b x
const x
x = a b x -> (⊢) o a b x
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (a b x -> (⊢) o a b x) -> a b x -> (⊢) o a b x
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ x -> a b x
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const x
x
cstrCatUnit :: forall a o . (WellPointed a, o (UnitObject a))
=> CatTagged (o⊢a) (UnitObject a)
cstrCatUnit :: CatTagged (o ⊢ a) (UnitObject a)
cstrCatUnit = Tagged (a (UnitObject a) (UnitObject a)) (UnitObject a)
-> Tagged ((⊢) o a (UnitObject a) (UnitObject a)) (UnitObject a)
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged (a (UnitObject a) (UnitObject a)) (UnitObject a)
forall (a :: * -> * -> *).
WellPointed a =>
CatTagged a (UnitObject a)
unit :: CatTagged a (UnitObject a))
instance (EnhancedCat a k, o (UnitObject a))
=> EnhancedCat (o⊢a) k where
arr :: k b c -> (⊢) o a b c
arr = (k b c -> a b c) -> k b c -> (⊢) o a b c
forall (k :: * -> * -> *) (a :: * -> * -> *) (o :: * -> Constraint)
b c.
(Category k, Category a, o b, o c) =>
(k b c -> a b c) -> k b c -> (⊢) o a b c
constrainedArr k b c -> a b c
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr
constrainedLeft :: ( CoCartesian k, ObjectSum k b d, ObjectSum k c d )
=> ( k b c -> k (b+d) (c+d) )
-> (o⊢k) b c -> (o⊢k) (b+d) (c+d)
constrainedLeft :: (k b c -> k (b + d) (c + d))
-> (⊢) o k b c -> (⊢) o k (b + d) (c + d)
constrainedLeft k b c -> k (b + d) (c + d)
fs = k (b + d) (c + d) -> (⊢) o k (b + d) (c + d)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (k (b + d) (c + d) -> (⊢) o k (b + d) (c + d))
-> ((⊢) o k b c -> k (b + d) (c + d))
-> (⊢) o k b c
-> (⊢) o k (b + d) (c + d)
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 b c -> k (b + d) (c + d)
fs (k b c -> k (b + d) (c + d))
-> ((⊢) o k b c -> k b c) -> (⊢) o k b c -> k (b + d) (c + d)
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
. (⊢) o k b c -> k b c
forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
Category k =>
(⊢) o k a b -> k a b
unconstrained
constrainedRight :: ( CoCartesian k, ObjectSum k b c, ObjectSum k b d )
=> ( k c d -> k (b+c) (b+d) )
-> (o⊢k) c d -> (o⊢k) (b+c) (b+d)
constrainedRight :: (k c d -> k (b + c) (b + d))
-> (⊢) o k c d -> (⊢) o k (b + c) (b + d)
constrainedRight k c d -> k (b + c) (b + d)
fs = k (b + c) (b + d) -> (⊢) o k (b + c) (b + d)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (k (b + c) (b + d) -> (⊢) o k (b + c) (b + d))
-> ((⊢) o k c d -> k (b + c) (b + d))
-> (⊢) o k c d
-> (⊢) o k (b + c) (b + d)
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 c d -> k (b + c) (b + d)
fs (k c d -> k (b + c) (b + d))
-> ((⊢) o k c d -> k c d) -> (⊢) o k c d -> k (b + c) (b + d)
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
. (⊢) o k c d -> k c d
forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
Category k =>
(⊢) o k a b -> k a b
unconstrained
instance (MorphChoice k, o (ZeroObject k)) => MorphChoice (o⊢k) where
left :: (⊢) o k b c -> (⊢) o k (b + d) (c + d)
left = (k b c -> k (b + d) (c + d))
-> (⊢) o k b c -> (⊢) o k (b + d) (c + d)
forall (k :: * -> * -> *) b d c (o :: * -> Constraint).
(CoCartesian k, ObjectSum k b d, ObjectSum k c d) =>
(k b c -> k (b + d) (c + d))
-> (⊢) o k b c -> (⊢) o k (b + d) (c + d)
constrainedLeft k b c -> k (b + d) (c + d)
forall (a :: * -> * -> *) b d c.
(MorphChoice a, ObjectSum a b d, ObjectSum a c d) =>
a b c -> a (b + d) (c + d)
left
right :: (⊢) o k b c -> (⊢) o k (d + b) (d + c)
right = (k b c -> k (d + b) (d + c))
-> (⊢) o k b c -> (⊢) o k (d + b) (d + c)
forall (k :: * -> * -> *) b c d (o :: * -> Constraint).
(CoCartesian k, ObjectSum k b c, ObjectSum k b d) =>
(k c d -> k (b + c) (b + d))
-> (⊢) o k c d -> (⊢) o k (b + c) (b + d)
constrainedRight k b c -> k (d + b) (d + c)
forall (a :: * -> * -> *) d b c.
(MorphChoice a, ObjectSum a d b, ObjectSum a d c) =>
a b c -> a (d + b) (d + c)
right
ConstrainedMorphism k b c
a +++ :: (⊢) o k b c -> (⊢) o k b' c' -> (⊢) o k (b + b') (c + c')
+++ ConstrainedMorphism k b' c'
b = k (b + b') (c + c') -> (⊢) o k (b + b') (c + c')
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (k (b + b') (c + c') -> (⊢) o k (b + b') (c + c'))
-> k (b + b') (c + c') -> (⊢) o k (b + b') (c + c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k b c
a k b c -> k b' c' -> k (b + b') (c + c')
forall (a :: * -> * -> *) b b' c c'.
(MorphChoice a, ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
+++ k b' c'
b
instance (PreArrChoice k, o (ZeroObject k)) => PreArrChoice (o⊢k) where
ConstrainedMorphism k b c
a ||| :: (⊢) o k b c -> (⊢) o k b' c -> (⊢) o k (b + b') c
||| ConstrainedMorphism k b' c
b = k (b + b') c -> (⊢) o k (b + b') c
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (k (b + b') c -> (⊢) o k (b + b') c)
-> k (b + b') c -> (⊢) o k (b + b') c
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k b c
a k b c -> k b' c -> k (b + b') c
forall (k :: * -> * -> *) b b' c.
(PreArrChoice k, ObjectSum k b b', Object k c) =>
k b c -> k b' c -> k (b + b') c
||| k b' c
b
initial :: (⊢) o k (ZeroObject (o ⊢ k)) b
initial = k (ZeroObject k) b -> ConstrainedCategory k o (ZeroObject k) b
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k (ZeroObject k) b
forall (k :: * -> * -> *) b.
(PreArrChoice k, Object k b) =>
k (ZeroObject k) b
initial
coFst :: (⊢) o k a (a + b)
coFst = k a (a + b) -> (⊢) o k a (a + b)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k a (a + b)
forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k a (a + b)
coFst
coSnd :: (⊢) o k b (a + b)
coSnd = k b (a + b) -> (⊢) o k b (a + b)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k b (a + b)
forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k b (a + b)
coSnd
instance (SPDistribute k, o (ZeroObject k), o (UnitObject k))
=> SPDistribute (o⊢k) where
distribute :: (⊢) o k (a, b + c) ((a, b) + (a, c))
distribute = k (a, b + c) ((a, b) + (a, c))
-> (⊢) o k (a, b + c) ((a, b) + (a, c))
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k (a, b + c) ((a, b) + (a, c))
forall (k :: * -> * -> *) a b c.
(SPDistribute k, ObjectSum k (a, b) (a, c), ObjectPair k a (b + c),
ObjectSum k b c, PairObjects k a b, PairObjects k a c) =>
k (a, b + c) ((a, b) + (a, c))
distribute
unDistribute :: (⊢) o k ((a, b) + (a, c)) (a, b + c)
unDistribute = k ((a, b) + (a, c)) (a, b + c)
-> (⊢) o k ((a, b) + (a, c)) (a, b + c)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k ((a, b) + (a, c)) (a, b + c)
forall (k :: * -> * -> *) a b c.
(SPDistribute k, ObjectSum k (a, b) (a, c), ObjectPair k a (b + c),
ObjectSum k b c, PairObjects k a b, PairObjects k a c) =>
k ((a, b) + (a, c)) (a, b + c)
unDistribute
boolAsSwitch :: (⊢) o k (Bool, a) (a + a)
boolAsSwitch = k (Bool, a) (a + a) -> (⊢) o k (Bool, a) (a + a)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k (Bool, a) (a + a)
forall (k :: * -> * -> *) a.
(SPDistribute k, ObjectSum k a a, ObjectPair k Bool a) =>
k (Bool, a) (a + a)
boolAsSwitch
boolFromSwitch :: (⊢) o k (a + a) (Bool, a)
boolFromSwitch = k (a + a) (Bool, a) -> (⊢) o k (a + a) (Bool, a)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k (a + a) (Bool, a)
forall (k :: * -> * -> *) a.
(SPDistribute k, ObjectSum k a a, ObjectPair k Bool a) =>
k (a + a) (Bool, a)
boolFromSwitch
choose :: (Arrow f (->), Function f, Object f Bool, Object f a)
=> f (UnitObject f) a
-> f (UnitObject f) a
-> f Bool a
choose :: f (UnitObject f) a -> f (UnitObject f) a -> f Bool a
choose f (UnitObject f) a
fv f (UnitObject f) a
tv = (Bool -> a) -> f Bool a
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr ((Bool -> a) -> f Bool a) -> (Bool -> a) -> f Bool a
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Bool
c -> if Bool
c then f (UnitObject f) a -> a
forall (f :: * -> * -> *) x.
(WellPointed f, Function f, Object f x) =>
f (UnitObject f) x -> x
value f (UnitObject f) a
tv else f (UnitObject f) a -> a
forall (f :: * -> * -> *) x.
(WellPointed f, Function f, Object f x) =>
f (UnitObject f) x -> x
value f (UnitObject f) a
fv
ifThenElse :: ( EnhancedCat f (->), Function f
, Object f Bool, Object f a, Object f (f a a), Object f (f a (f a a))
) => Bool `f` (a `f` (a `f` a))
ifThenElse :: f Bool (f a (f a a))
ifThenElse = (Bool -> f a (f a a)) -> f Bool (f a (f a a))
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr ((Bool -> f a (f a a)) -> f Bool (f a (f a a)))
-> (Bool -> f a (f a a)) -> f Bool (f a (f a a))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Bool
c -> (a -> f a a) -> f a (f a a)
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr ((a -> f a a) -> f a (f a a)) -> (a -> f a a) -> f a (f a a)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \a
tv -> (a -> a) -> f a a
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr ((a -> a) -> f a a) -> (a -> a) -> f a a
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \a
fv -> if Bool
c then a
tv else a
fv
genericAgentCombine :: ( HasAgent k, PreArrow k
, Object k a, ObjectPair k b c, Object k d )
=> k (b,c) d -> GenericAgent k a b -> GenericAgent k a c -> GenericAgent k a d
genericAgentCombine :: k (b, c) d
-> GenericAgent k a b -> GenericAgent k a c -> GenericAgent k a d
genericAgentCombine k (b, c) d
m (GenericAgent k a b
v) (GenericAgent k a c
w)
= k a d -> GenericAgent k a d
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent (k a d -> GenericAgent k a d) -> k a d -> GenericAgent k a d
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (b, c) d
m k (b, c) d -> k a (b, c) -> k a d
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 k a b -> k a c -> k a (b, c)
forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& k a c
w)
genericUnit :: ( PreArrow k, HasAgent k, Object k a )
=> GenericAgent k a (UnitObject k)
genericUnit :: GenericAgent k a (UnitObject k)
genericUnit = k a (UnitObject k) -> GenericAgent k a (UnitObject k)
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent k a (UnitObject k)
forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal
class (Morphism k, HasAgent k) => CartesianAgent k where
alg1to2 :: ( Object k a, ObjectPair k b c
) => (forall q . Object k q
=> AgentVal k q a -> (AgentVal k q b, AgentVal k q c) )
-> k a (b,c)
alg2to1 :: ( ObjectPair k a b, Object k c
) => (forall q . Object k q
=> AgentVal k q a -> AgentVal k q b -> AgentVal k q c )
-> k (a,b) c
alg2to2 :: ( ObjectPair k a b, ObjectPair k c d
) => (forall q . Object k q
=> AgentVal k q a -> AgentVal k q b -> (AgentVal k q c, AgentVal k q d) )
-> k (a,b) (c,d)
genericAlg1to2 :: ( PreArrow k, u ~ UnitObject k
, Object k a, ObjectPair k b c
) => ( forall q . Object k q
=> GenericAgent k q a -> (GenericAgent k q b, GenericAgent k q c) )
-> k a (b,c)
genericAlg1to2 :: (forall q.
Object k q =>
GenericAgent k q a -> (GenericAgent k q b, GenericAgent k q c))
-> k a (b, c)
genericAlg1to2 forall q.
Object k q =>
GenericAgent k q a -> (GenericAgent k q b, GenericAgent k q c)
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
b k a b -> k a c -> k a (b, c)
forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& GenericAgent k a c -> k a c
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
GenericAgent k a v -> k a v
runGenericAgent GenericAgent k a c
c
where (GenericAgent k a b
b,GenericAgent k a c
c) = GenericAgent k a a -> (GenericAgent k a b, GenericAgent k a c)
forall q.
Object k q =>
GenericAgent k q a -> (GenericAgent k q b, GenericAgent k q c)
f (GenericAgent k a a -> (GenericAgent k a b, GenericAgent k a c))
-> GenericAgent k a a -> (GenericAgent k a b, GenericAgent k a c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f 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
genericAlg2to1 :: ( PreArrow k, u ~ UnitObject k
, ObjectPair k a u, ObjectPair k a b, ObjectPair k b u, ObjectPair k b a
) => ( forall q . Object k q
=> GenericAgent k q a -> GenericAgent k q b -> GenericAgent k q c )
-> k (a,b) c
genericAlg2to1 :: (forall q.
Object k q =>
GenericAgent k q a -> GenericAgent k q b -> GenericAgent k q c)
-> k (a, b) c
genericAlg2to1 forall q.
Object k q =>
GenericAgent k q a -> GenericAgent k q b -> GenericAgent k q c
f = GenericAgent k (a, b) c -> k (a, b) c
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
GenericAgent k a v -> k a v
runGenericAgent (GenericAgent k (a, b) c -> k (a, b) c)
-> GenericAgent k (a, b) c -> k (a, b) c
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ GenericAgent k (a, b) a
-> GenericAgent k (a, b) b -> GenericAgent k (a, b) c
forall q.
Object k q =>
GenericAgent k q a -> GenericAgent k q b -> GenericAgent k q c
f (k (a, b) a -> GenericAgent k (a, b) a
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent k (a, b) a
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst) (k (a, b) b -> GenericAgent k (a, b) b
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent k (a, b) b
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd)
genericAlg2to2 :: ( PreArrow k, u ~ UnitObject k
, ObjectPair k a u, ObjectPair k a b, ObjectPair k c d
, ObjectPair k b u, ObjectPair k b a
) => ( forall q . Object k q
=> GenericAgent k q a -> GenericAgent k q b
-> (GenericAgent k q c, GenericAgent k q d) )
-> k (a,b) (c,d)
genericAlg2to2 :: (forall q.
Object k q =>
GenericAgent k q a
-> GenericAgent k q b -> (GenericAgent k q c, GenericAgent k q d))
-> k (a, b) (c, d)
genericAlg2to2 forall q.
Object k q =>
GenericAgent k q a
-> GenericAgent k q b -> (GenericAgent k q c, GenericAgent k q d)
f = GenericAgent k (a, b) c -> k (a, b) c
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
GenericAgent k a v -> k a v
runGenericAgent GenericAgent k (a, b) c
c k (a, b) c -> k (a, b) d -> k (a, b) (c, d)
forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& GenericAgent k (a, b) d -> k (a, b) d
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
GenericAgent k a v -> k a v
runGenericAgent GenericAgent k (a, b) d
d
where (GenericAgent k (a, b) c
c,GenericAgent k (a, b) d
d) = GenericAgent k (a, b) a
-> GenericAgent k (a, b) b
-> (GenericAgent k (a, b) c, GenericAgent k (a, b) d)
forall q.
Object k q =>
GenericAgent k q a
-> GenericAgent k q b -> (GenericAgent k q c, GenericAgent k q d)
f (k (a, b) a -> GenericAgent k (a, b) a
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent k (a, b) a
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst) (k (a, b) b -> GenericAgent k (a, b) b
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent k (a, b) b
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd)
class (HasAgent k, AgentVal k a x ~ p a x)
=> PointAgent p k a x | p -> k where
point :: (Object k a, Object k x) => x -> p a x
genericPoint :: ( WellPointed k, Object k a, ObjectPoint k x )
=> x -> GenericAgent k a x
genericPoint :: x -> GenericAgent k a x
genericPoint x
x = k a x -> GenericAgent k a x
forall k k (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent (k a x -> GenericAgent k a x) -> k a x -> GenericAgent k a x
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ x -> k a x
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const x
x
follow :: (EnhancedCat k Coercion, Coercible a b, Object k a, Object k b)
=> p a b -> k a b
follow :: p a b -> k a b
follow p a b
_ = Coercion a b -> k a b
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr Coercion a b
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
flout :: (EnhancedCat k Coercion, Coercible b a, Object k a, Object k b)
=> p a b -> k b a
flout :: p a b -> k b a
flout p a b
_ = Coercion b a -> k b a
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr Coercion b a
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
pretend :: (EnhancedCat k Coercion, Object k a, Object k b)
=> Coercion a b -> k a a -> k b b
pretend :: Coercion a b -> k a a -> k b b
pretend Coercion a b
crc k a a
f = Coercion a b -> k a b
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr Coercion a b
crc k a b -> k b a -> k b 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
. k a a
f k a a -> k b a -> k b 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
. Coercion b a -> k b a
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr (Coercion a b -> Coercion b a
forall k (a :: k) (b :: k). Coercion a b -> Coercion b a
sym Coercion a b
crc)
swallow :: (EnhancedCat k Coercion, Object k a, Object k b)
=> Coercion b a -> k a a -> k b b
swallow :: Coercion b a -> k a a -> k b b
swallow Coercion b a
crc k a a
f = Coercion a b -> k a b
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr (Coercion b a -> Coercion a b
forall k (a :: k) (b :: k). Coercion a b -> Coercion b a
sym Coercion b a
crc) k a b -> k b a -> k b 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
. k a a
f k a a -> k b a -> k b 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
. Coercion b a -> k b a
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr Coercion b a
crc
pretendLike :: ( EnhancedCat k Coercion, Coercible b a, Coercible c d
, Object k a, Object k b, Object k c, Object k d )
=> p c d -> k a c -> k b d
pretendLike :: p c d -> k a c -> k b d
pretendLike p c d
_ k a c
f = Coercion c d -> k c d
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr Coercion c d
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion k c d -> k b c -> k b d
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 c
f k a c -> k b a -> k b 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
. Coercion b a -> k b a
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr Coercion b a
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
swallowLike :: ( EnhancedCat k Coercion, Coercible b a, Coercible c d
, Object k a, Object k b, Object k c, Object k d )
=> p b a -> k a c -> k b d
swallowLike :: p b a -> k a c -> k b d
swallowLike p b a
_ k a c
f = Coercion c d -> k c d
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr Coercion c d
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion k c d -> k b c -> k b d
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 c
f k a c -> k b a -> k b 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
. Coercion b a -> k b a
forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
Object a c) =>
k b c -> a b c
arr Coercion b a
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion