{-# LANGUAGE CPP               #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE PolyKinds         #-}
{-# LANGUAGE TypeFamilies      #-}
-- | Overloaded Categories, desugar @Arrow@ into classes in this module.
--
-- == Enabled with
--
-- @
-- {-\# OPTIONS -fplugin=Overloaded -fplugin-opt=Overloaded:Categories #-}
-- @
--
-- == Description
--
-- @Arrows@ notation - [GHC manual chapter](https://downloads.haskell.org/~ghc/8.10.1/docs/html/users_guide/glasgow_exts.html#arrow-notation) -
-- is cool, but it desugars into /"wrong"/ classes.
-- The 'arr' combinator is used for plumbing. We should desugar to proper
-- type-classes:
--
-- * 'CartesianCategory', not 'A.Arrow'
-- * 'CocartesianCategory', not 'A.ArrowChoice' (implementation relies on 'BicartesianCategory')
-- * 'CCC', not 'A.ArrowApply' (not implemented yet)
--
-- == Examples
--
-- Expression like
--
-- @
-- catAssoc
--     :: 'CartesianCategory' cat
--     => cat ('Product' cat ('Product' cat a b) c) ('Product' cat a ('Product' cat b c))
-- catAssoc = proc ((x, y), z) -> 'identity' -< (x, (y, z))
-- @
--
-- are desugared to (a mess which is)
--
-- @
-- 'fanout' ('proj1' '%%' 'proj1') ('fanout' ('proj2' '%%' 'proj1') 'proj2')
-- @
--
-- If you are familiar with arrows-operators, this is similar to
--
-- @
-- ('fst' . 'fst') '&&&' ('snd' . 'fst' '&&&' 'snd')
-- @
--
-- expression.
--
-- The @catAssoc@ could be instantiated to @cat = (->)@,
-- or more interestingly for example instantiate it to STLC morphisms to get an expression
-- like:
--
-- @
-- Lam (Pair (Fst (Fst (Var Here))) (Pair (Snd (Fst (Var Here))) (Snd (Var Here))))
-- @
--
-- @proc@ notation is nicer than writing de Bruijn indices.
--
-- This is very similar idea to Conal Elliott's [Compiling to Categories](http://conal.net/papers/compiling-to-categories/) work.
-- This approach is syntactically more heavy, but works in more correct
-- stage of compiler, before actual desugarer.
--
-- As one more example, we implement the automatic differentiation,
-- as in Conal's paper(s).
-- To keep things simple we use
--
-- @
-- newtype AD a b = AD (a -> (b, a -> b))
-- @
--
-- representation, i.e. use ordinary maps to represent linear maps.
-- We then define a function
--
-- @
-- evaluateAD :: Functor f => AD a b -> a -> f a -> (b, f b)
-- evaluateAD (AD f) x xs = let (y, f') = f x in (y, fmap f' xs)
-- @
--
-- which would allow to calculuate function value and
-- derivatives in given directions. Then we can define
-- simple quadratic function:
--
-- @
-- quad :: AD (Double, Double) Double
-- quad = proc (x, y) -> do
--     x2 <- mult -< (x, x)
--     y2 <- mult -< (y, y)
--     plus -< (x2, y2)
-- @
--
-- It's not as simple as writing @quad x y = x * x + y * y@,
-- but not /too far/.
--
-- Then we can play with it. At origo everything is zero:
--
-- @
-- let sqrthf = 1 / sqrt 2
-- in evaluateAD quad (0, 0) [(1,0), (0,1), (sqrthf, sqrthf)] = (0.0,[0.0,0.0,0.0])
-- @
--
-- If we evaluate at some other point, we see things working:
--
-- @
-- evaluateAD quad (1, 2) [(1,0), (0,1), (sqrthf, sqrthf)] = (5.0,[2.0,4.0,4.242640687119285])
-- @
--
-- Obviously, if we would use inspectable representation for linear maps,
-- as Conal describe, we'd get more benefits. And then 'arr' wouldn't
-- be definable!
--
module Overloaded.Categories (
    -- * Category
    C.Category,
    identity,
    (%%),
    -- * Monoidial
    SemigroupalCategory (..),
    defaultAssoc, defaultUnassoc,
    MonoidalCategory (..),
    defaultLunit, defaultRunit, defaultUnrunit, defaultUnlunit,
    CommutativeCategory (..),
    defaultSwap,
    -- * Product and Terminal
    CartesianCategory (..),
    CategoryWith1 (..),
    -- * Coproduct and initial
    CategoryWith0 (..),
    CocartesianCategory (..),
    -- * Bicartesian
    BicartesianCategory (..),
    -- * Closed cartesian category
    CCC (..),
    -- * Generalized element
    GeneralizedElement (..),
    -- * WrappedArrow
    WrappedArrow (..),
    ) where

import qualified Control.Arrow    as A
import qualified Control.Category as C

import Control.Applicative        (liftA2)
import Control.Arrow              (Kleisli (..))
import Data.Functor.Contravariant (Op (..))
import Data.Kind                  (Type)
import Data.Profunctor            (Star (..))
import Data.Semigroupoid.Dual     (Dual (..))
import Data.Void                  (Void, absurd)

-------------------------------------------------------------------------------
-- Category
-------------------------------------------------------------------------------

-- | A non-clashing name for 'C.id'.
identity :: C.Category cat => cat a a
identity :: cat a a
identity = cat a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
C.id
{-# INLINE identity #-}

-- | A non-clashing name for @('C..')@.
(%%) :: C.Category cat => cat b c -> cat a b -> cat a c
%% :: cat b c -> cat a b -> cat a c
(%%) = cat b c -> cat a b -> cat a c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
(C..)
{-# INLINE (%%) #-}
infixr 9 %%

-------------------------------------------------------------------------------
-- Monoidal
-------------------------------------------------------------------------------

class C.Category cat => SemigroupalCategory (cat :: k -> k -> Type) where
    type Tensor cat :: k -> k -> k

    assoc :: cat (Tensor cat (Tensor cat a b) c)
                 (Tensor cat a (Tensor cat b c))

    unassoc :: cat (Tensor cat a (Tensor cat b c))
                   (Tensor cat (Tensor cat a b) c)

defaultAssoc :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat (Tensor cat a b) c) (Tensor cat a (Tensor cat b c))
defaultAssoc :: cat (Tensor cat (Tensor cat a b) c) (Tensor cat a (Tensor cat b c))
defaultAssoc = cat (Product cat (Product cat a b) c) a
-> cat (Product cat (Product cat a b) c) (Product cat b c)
-> cat
     (Product cat (Product cat a b) c) (Product cat a (Product cat b c))
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
CartesianCategory cat =>
cat a b -> cat a c -> cat a (Product cat b c)
fanout (cat (Product cat a b) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) a
proj1 cat (Product cat a b) a
-> cat (Product cat (Product cat a b) c) (Product cat a b)
-> cat (Product cat (Product cat a b) c) a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
%% cat (Product cat (Product cat a b) c) (Product cat a b)
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) a
proj1) (cat (Product cat (Product cat a b) c) b
-> cat (Product cat (Product cat a b) c) c
-> cat (Product cat (Product cat a b) c) (Product cat b c)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
CartesianCategory cat =>
cat a b -> cat a c -> cat a (Product cat b c)
fanout (cat (Product cat a b) b
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) b
proj2 cat (Product cat a b) b
-> cat (Product cat (Product cat a b) c) (Product cat a b)
-> cat (Product cat (Product cat a b) c) b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
%% cat (Product cat (Product cat a b) c) (Product cat a b)
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) a
proj1) cat (Product cat (Product cat a b) c) c
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) b
proj2)

defaultUnassoc :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat a (Tensor cat b c)) (Tensor cat (Tensor cat a b) c)
defaultUnassoc :: cat (Tensor cat a (Tensor cat b c)) (Tensor cat (Tensor cat a b) c)
defaultUnassoc = cat (Product cat a (Product cat b c)) (Product cat a b)
-> cat (Product cat a (Product cat b c)) c
-> cat
     (Product cat a (Product cat b c)) (Product cat (Product cat a b) c)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
CartesianCategory cat =>
cat a b -> cat a c -> cat a (Product cat b c)
fanout (cat (Product cat a (Product cat b c)) a
-> cat (Product cat a (Product cat b c)) b
-> cat (Product cat a (Product cat b c)) (Product cat a b)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
CartesianCategory cat =>
cat a b -> cat a c -> cat a (Product cat b c)
fanout cat (Product cat a (Product cat b c)) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) a
proj1 (cat (Product cat b c) b
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) a
proj1 cat (Product cat b c) b
-> cat (Product cat a (Product cat b c)) (Product cat b c)
-> cat (Product cat a (Product cat b c)) b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
%% cat (Product cat a (Product cat b c)) (Product cat b c)
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) b
proj2)) (cat (Product cat b c) c
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) b
proj2 cat (Product cat b c) c
-> cat (Product cat a (Product cat b c)) (Product cat b c)
-> cat (Product cat a (Product cat b c)) c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
%% cat (Product cat a (Product cat b c)) (Product cat b c)
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) b
proj2)

class SemigroupalCategory cat => MonoidalCategory (cat :: k -> k -> Type) where
    type Unit cat :: k

    lunit :: cat (Tensor cat (Unit cat) a) a
    runit :: cat (Tensor cat a (Unit cat)) a

    unlunit :: cat a (Tensor cat (Unit cat) a)
    unrunit :: cat a (Tensor cat a (Unit cat))

defaultLunit :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat (Unit cat) a) a
defaultLunit :: cat (Tensor cat (Unit cat) a) a
defaultLunit = cat (Tensor cat (Unit cat) a) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) b
proj2

defaultRunit :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat a (Unit cat)) a
defaultRunit :: cat (Tensor cat a (Unit cat)) a
defaultRunit = cat (Tensor cat a (Unit cat)) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) a
proj1

defaultUnlunit :: (CategoryWith1 cat, Tensor cat ~ Product cat, Unit cat ~ Terminal cat) => cat a (Tensor cat (Unit cat) a)
defaultUnlunit :: cat a (Tensor cat (Unit cat) a)
defaultUnlunit = cat a (Terminal cat)
-> cat a a -> cat a (Product cat (Terminal cat) a)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
CartesianCategory cat =>
cat a b -> cat a c -> cat a (Product cat b c)
fanout cat a (Terminal cat)
forall k (cat :: k -> k -> *) (a :: k).
CategoryWith1 cat =>
cat a (Terminal cat)
terminal cat a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
identity

defaultUnrunit :: (CategoryWith1 cat, Tensor cat ~ Product cat, Unit cat ~ Terminal cat) => cat a (Tensor cat a (Unit cat))
defaultUnrunit :: cat a (Tensor cat a (Unit cat))
defaultUnrunit = cat a a
-> cat a (Terminal cat) -> cat a (Product cat a (Terminal cat))
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
CartesianCategory cat =>
cat a b -> cat a c -> cat a (Product cat b c)
fanout cat a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
identity cat a (Terminal cat)
forall k (cat :: k -> k -> *) (a :: k).
CategoryWith1 cat =>
cat a (Terminal cat)
terminal

class SemigroupalCategory cat => CommutativeCategory cat where
    swap :: cat (Tensor cat a b) (Tensor cat b a)

defaultSwap :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat a b) (Tensor cat b a)
defaultSwap :: cat (Tensor cat a b) (Tensor cat b a)
defaultSwap = cat (Product cat a b) b
-> cat (Product cat a b) a
-> cat (Product cat a b) (Product cat b a)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
CartesianCategory cat =>
cat a b -> cat a c -> cat a (Product cat b c)
fanout cat (Product cat a b) b
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) b
proj2 cat (Product cat a b) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) a
proj1

-------------------------------------------------------------------------------
-- Product
-------------------------------------------------------------------------------

-- | Category with terminal object.
class CartesianCategory cat => CategoryWith1 (cat :: k -> k -> Type) where
    type Terminal cat :: k

    terminal :: cat a (Terminal cat)

-- | Cartesian category is a monoidal category
-- where monoidal product is the categorical product.
--
class C.Category cat => CartesianCategory (cat :: k -> k -> Type) where
    type Product cat :: k -> k -> k

    proj1 :: cat (Product cat a b) a
    proj2 :: cat (Product cat a b) b

    -- | @'fanout' f g@ is written as \(\langle f, g \rangle\) in category theory literature.
    fanout :: cat a b -> cat a c -> cat a (Product cat b c)

instance CategoryWith1 (->) where
    type Terminal (->) = ()

    terminal :: a -> Terminal (->)
terminal a
_ = ()

instance CartesianCategory (->) where
    type Product (->) = (,)

    proj1 :: Product (->) a b -> a
proj1 = Product (->) a b -> a
forall a b. (a, b) -> a
fst
    proj2 :: Product (->) a b -> b
proj2 = Product (->) a b -> b
forall a b. (a, b) -> b
snd
    fanout :: (a -> b) -> (a -> c) -> a -> Product (->) b c
fanout a -> b
f a -> c
g a
x = (a -> b
f a
x , a -> c
g a
x)

instance CategoryWith1 Op where
    type Terminal Op = Void

    terminal :: Op a (Terminal Op)
terminal = (Void -> a) -> Op a Void
forall a b. (b -> a) -> Op a b
Op Void -> a
forall a. Void -> a
absurd

instance CartesianCategory Op where
    type Product Op = Either

    proj1 :: Op (Product Op a b) a
proj1 = (a -> Either a b) -> Op (Either a b) a
forall a b. (b -> a) -> Op a b
Op a -> Either a b
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CocartesianCategory cat =>
cat a (Coproduct cat a b)
inl
    proj2 :: Op (Product Op a b) b
proj2 = (b -> Either a b) -> Op (Either a b) b
forall a b. (b -> a) -> Op a b
Op b -> Either a b
forall k (cat :: k -> k -> *) (b :: k) (a :: k).
CocartesianCategory cat =>
cat b (Coproduct cat a b)
inr
    fanout :: Op a b -> Op a c -> Op a (Product Op b c)
fanout (Op b -> a
f) (Op c -> a
g) = (Either b c -> a) -> Op a (Either b c)
forall a b. (b -> a) -> Op a b
Op ((b -> a) -> (c -> a) -> Coproduct (->) b c -> a
forall k (cat :: k -> k -> *) (a :: k) (c :: k) (b :: k).
CocartesianCategory cat =>
cat a c -> cat b c -> cat (Coproduct cat a b) c
fanin b -> a
f c -> a
g)

-------------------------------------------------------------------------------
-- Coproduct
-------------------------------------------------------------------------------

-- | Category with initial object.
class CocartesianCategory cat => CategoryWith0 (cat :: k -> k -> Type) where
    type Initial cat :: k

    initial :: cat (Initial cat) a

-- | Cocartesian category is a monoidal category
-- where monoidal product is the categorical coproduct.
--
class C.Category cat => CocartesianCategory (cat :: k -> k -> Type) where
    type Coproduct cat :: k -> k -> k

    inl :: cat a (Coproduct cat a b)
    inr :: cat b (Coproduct cat a b)

    -- | @'fanin' f g@ is written as \([f, g]\) in category theory literature.
    fanin :: cat a c -> cat b c -> cat (Coproduct cat a b) c

instance CategoryWith0 (->) where
    type Initial (->) = Void

    initial :: Initial (->) -> a
initial = Initial (->) -> a
forall a. Void -> a
absurd

instance CocartesianCategory (->) where
    type Coproduct (->) = Either

    inl :: a -> Coproduct (->) a b
inl = a -> Coproduct (->) a b
forall a b. a -> Either a b
Left
    inr :: b -> Coproduct (->) a b
inr = b -> Coproduct (->) a b
forall a b. b -> Either a b
Right
    fanin :: (a -> c) -> (b -> c) -> Coproduct (->) a b -> c
fanin = (a -> c) -> (b -> c) -> Coproduct (->) a b -> c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either

instance CategoryWith0 Op where
    type Initial Op = ()

    initial :: Op (Initial Op) a
initial = (a -> ()) -> Op () a
forall a b. (b -> a) -> Op a b
Op (() -> a -> ()
forall a b. a -> b -> a
const ())

instance CocartesianCategory Op where
    type Coproduct Op = (,)

    inl :: Op a (Coproduct Op a b)
inl = ((a, b) -> a) -> Op a (a, b)
forall a b. (b -> a) -> Op a b
Op (a, b) -> a
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) a
proj1
    inr :: Op b (Coproduct Op a b)
inr = ((a, b) -> b) -> Op b (a, b)
forall a b. (b -> a) -> Op a b
Op (a, b) -> b
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) b
proj2
    fanin :: Op a c -> Op b c -> Op (Coproduct Op a b) c
fanin (Op c -> a
f) (Op c -> b
g) = (c -> (a, b)) -> Op (a, b) c
forall a b. (b -> a) -> Op a b
Op ((c -> a) -> (c -> b) -> c -> Product (->) a b
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
CartesianCategory cat =>
cat a b -> cat a c -> cat a (Product cat b c)
fanout c -> a
f c -> b
g)

-- | Bicartesian category is category which is
-- both cartesian and cocartesian.
--
-- We also require distributive morpism.
class (CartesianCategory cat, CocartesianCategory cat) => BicartesianCategory cat where
    distr :: cat (Product cat (Coproduct cat a b) c)
                 (Coproduct cat (Product cat a c) (Product cat b c))

instance BicartesianCategory (->) where
    distr :: Product (->) (Coproduct (->) a b) c
-> Coproduct (->) (Product (->) a c) (Product (->) b c)
distr (Left x,  z) = (a, c) -> Either (a, c) (b, c)
forall a b. a -> Either a b
Left (a
x, c
z)
    distr (Right y, z) = (b, c) -> Either (a, c) (b, c)
forall a b. b -> Either a b
Right (b
y, c
z)

-------------------------------------------------------------------------------
-- Dual
-------------------------------------------------------------------------------

instance CategoryWith1 cat => CategoryWith0 (Dual cat) where
    type Initial (Dual cat) = Terminal cat
    initial :: Dual cat (Initial (Dual cat)) a
initial = cat a (Terminal cat) -> Dual cat (Terminal cat) a
forall k k1 (k2 :: k -> k1 -> *) (a :: k1) (b :: k).
k2 b a -> Dual k2 a b
Dual cat a (Terminal cat)
forall k (cat :: k -> k -> *) (a :: k).
CategoryWith1 cat =>
cat a (Terminal cat)
terminal

instance CategoryWith0 cat => CategoryWith1 (Dual cat) where
    type Terminal (Dual cat) = Initial cat
    terminal :: Dual cat a (Terminal (Dual cat))
terminal = cat (Initial cat) a -> Dual cat a (Initial cat)
forall k k1 (k2 :: k -> k1 -> *) (a :: k1) (b :: k).
k2 b a -> Dual k2 a b
Dual cat (Initial cat) a
forall k (cat :: k -> k -> *) (a :: k).
CategoryWith0 cat =>
cat (Initial cat) a
initial

instance CartesianCategory cat => CocartesianCategory (Dual cat) where
    type Coproduct (Dual cat) = Product cat

    inl :: Dual cat a (Coproduct (Dual cat) a b)
inl = cat (Product cat a b) a -> Dual cat a (Product cat a b)
forall k k1 (k2 :: k -> k1 -> *) (a :: k1) (b :: k).
k2 b a -> Dual k2 a b
Dual cat (Product cat a b) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) a
proj1
    inr :: Dual cat b (Coproduct (Dual cat) a b)
inr = cat (Product cat a b) b -> Dual cat b (Product cat a b)
forall k k1 (k2 :: k -> k1 -> *) (a :: k1) (b :: k).
k2 b a -> Dual k2 a b
Dual cat (Product cat a b) b
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) b
proj2

    fanin :: Dual cat a c
-> Dual cat b c -> Dual cat (Coproduct (Dual cat) a b) c
fanin (Dual cat c a
f) (Dual cat c b
g) = cat c (Product cat a b) -> Dual cat (Product cat a b) c
forall k k1 (k2 :: k -> k1 -> *) (a :: k1) (b :: k).
k2 b a -> Dual k2 a b
Dual (cat c a -> cat c b -> cat c (Product cat a b)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
CartesianCategory cat =>
cat a b -> cat a c -> cat a (Product cat b c)
fanout cat c a
f cat c b
g)

instance CocartesianCategory cat => CartesianCategory (Dual cat) where
    type Product (Dual cat) = Coproduct cat

    proj1 :: Dual cat (Product (Dual cat) a b) a
proj1 = cat a (Coproduct cat a b) -> Dual cat (Coproduct cat a b) a
forall k k1 (k2 :: k -> k1 -> *) (a :: k1) (b :: k).
k2 b a -> Dual k2 a b
Dual cat a (Coproduct cat a b)
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CocartesianCategory cat =>
cat a (Coproduct cat a b)
inl
    proj2 :: Dual cat (Product (Dual cat) a b) b
proj2 = cat b (Coproduct cat a b) -> Dual cat (Coproduct cat a b) b
forall k k1 (k2 :: k -> k1 -> *) (a :: k1) (b :: k).
k2 b a -> Dual k2 a b
Dual cat b (Coproduct cat a b)
forall k (cat :: k -> k -> *) (b :: k) (a :: k).
CocartesianCategory cat =>
cat b (Coproduct cat a b)
inr

    fanout :: Dual cat a b -> Dual cat a c -> Dual cat a (Product (Dual cat) b c)
fanout (Dual cat b a
f) (Dual cat c a
g) = cat (Coproduct cat b c) a -> Dual cat a (Coproduct cat b c)
forall k k1 (k2 :: k -> k1 -> *) (a :: k1) (b :: k).
k2 b a -> Dual k2 a b
Dual (cat b a -> cat c a -> cat (Coproduct cat b c) a
forall k (cat :: k -> k -> *) (a :: k) (c :: k) (b :: k).
CocartesianCategory cat =>
cat a c -> cat b c -> cat (Coproduct cat a b) c
fanin cat b a
f cat c a
g)

-------------------------------------------------------------------------------
-- Exponential
-------------------------------------------------------------------------------

-- | Closed cartesian category.
--
class CartesianCategory cat => CCC (cat :: k -> k -> Type) where
    -- | @'Exponential' cat a b@ represents \(B^A\). This is due how (->) works.
    type Exponential cat :: k -> k -> k

    eval :: cat (Product cat (Exponential cat a b) a) b

    transpose :: cat (Product cat a b) c -> cat a (Exponential cat b c)

instance CCC (->) where
    type Exponential (->) = (->)

    eval :: Product (->) (Exponential (->) a b) a -> b
eval      = ((a -> b) -> a -> b) -> (a -> b, a) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)
    transpose :: (Product (->) a b -> c) -> a -> Exponential (->) b c
transpose = (Product (->) a b -> c) -> a -> Exponential (->) b c
forall a b c. ((a, b) -> c) -> a -> b -> c
curry

-------------------------------------------------------------------------------
-- Generalized Element
-------------------------------------------------------------------------------

class C.Category cat => GeneralizedElement (cat :: k -> k -> Type) where
    type Object cat (a :: k) :: Type

    konst :: Object cat a -> cat x a

instance GeneralizedElement (->) where
    type Object (->) a = a

    konst :: Object (->) a -> x -> a
konst = Object (->) a -> x -> a
forall a b. a -> b -> a
const

-------------------------------------------------------------------------------
-- Star
-------------------------------------------------------------------------------

instance Monad m => CartesianCategory (Star m) where
    type Product (Star m) = (,)

    proj1 :: Star m (Product (Star m) a b) a
proj1 = ((a, b) -> m a) -> Star m (a, b) a
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> ((a, b) -> a) -> (a, b) -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> a
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) a
proj1)
    proj2 :: Star m (Product (Star m) a b) b
proj2 = ((a, b) -> m b) -> Star m (a, b) b
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (b -> m b
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> m b) -> ((a, b) -> b) -> (a, b) -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> b
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) b
proj2)

    fanout :: Star m a b -> Star m a c -> Star m a (Product (Star m) b c)
fanout (Star a -> m b
f) (Star a -> m c
g) = (a -> m (b, c)) -> Star m a (b, c)
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star ((a -> m (b, c)) -> Star m a (b, c))
-> (a -> m (b, c)) -> Star m a (b, c)
forall a b. (a -> b) -> a -> b
$ \a
a -> (b -> c -> (b, c)) -> m b -> m c -> m (b, c)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) (a -> m b
f a
a) (a -> m c
g a
a)

instance Monad m => CategoryWith1 (Star m) where
    type Terminal (Star m) = ()

    terminal :: Star m a (Terminal (Star m))
terminal = (a -> m ()) -> Star m a ()
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> m ()) -> (a -> ()) -> a -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ()
forall k (cat :: k -> k -> *) (a :: k).
CategoryWith1 cat =>
cat a (Terminal cat)
terminal)

instance Monad m => CocartesianCategory (Star m) where
    type Coproduct (Star m) = Either

    inl :: Star m a (Coproduct (Star m) a b)
inl = (a -> m (Either a b)) -> Star m a (Either a b)
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (Either a b -> m (Either a b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either a b -> m (Either a b))
-> (a -> Either a b) -> a -> m (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either a b
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CocartesianCategory cat =>
cat a (Coproduct cat a b)
inl)
    inr :: Star m b (Coproduct (Star m) a b)
inr = (b -> m (Either a b)) -> Star m b (Either a b)
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (Either a b -> m (Either a b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either a b -> m (Either a b))
-> (b -> Either a b) -> b -> m (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Either a b
forall k (cat :: k -> k -> *) (b :: k) (a :: k).
CocartesianCategory cat =>
cat b (Coproduct cat a b)
inr)

    fanin :: Star m a c -> Star m b c -> Star m (Coproduct (Star m) a b) c
fanin (Star a -> m c
f) (Star b -> m c
g) = (Either a b -> m c) -> Star m (Either a b) c
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star ((a -> m c) -> (b -> m c) -> Coproduct (->) a b -> m c
forall k (cat :: k -> k -> *) (a :: k) (c :: k) (b :: k).
CocartesianCategory cat =>
cat a c -> cat b c -> cat (Coproduct cat a b) c
fanin a -> m c
f b -> m c
g)

instance Monad m => CategoryWith0 (Star m) where
    type Initial (Star m) = Void

    initial :: Star m (Initial (Star m)) a
initial = (Void -> m a) -> Star m Void a
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> (Void -> a) -> Void -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Void -> a
forall k (cat :: k -> k -> *) (a :: k).
CategoryWith0 cat =>
cat (Initial cat) a
initial)

instance Monad m => BicartesianCategory (Star m) where
    distr :: Star
  m
  (Product (Star m) (Coproduct (Star m) a b) c)
  (Coproduct (Star m) (Product (Star m) a c) (Product (Star m) b c))
distr = ((Either a b, c) -> m (Either (a, c) (b, c)))
-> Star m (Either a b, c) (Either (a, c) (b, c))
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (Either (a, c) (b, c) -> m (Either (a, c) (b, c))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (a, c) (b, c) -> m (Either (a, c) (b, c)))
-> ((Either a b, c) -> Either (a, c) (b, c))
-> (Either a b, c)
-> m (Either (a, c) (b, c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either a b, c) -> Either (a, c) (b, c)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
BicartesianCategory cat =>
cat
  (Product cat (Coproduct cat a b) c)
  (Coproduct cat (Product cat a c) (Product cat b c))
distr)

instance Monad m => CCC (Star m) where
    type Exponential (Star m) = Star m

    eval :: Star m (Product (Star m) (Exponential (Star m) a b) a) b
eval = ((Star m a b, a) -> m b) -> Star m (Star m a b, a) b
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (((Star m a b, a) -> m b) -> Star m (Star m a b, a) b)
-> ((Star m a b, a) -> m b) -> Star m (Star m a b, a) b
forall a b. (a -> b) -> a -> b
$ (Star m a b -> a -> m b) -> (Star m a b, a) -> m b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Star m a b -> a -> m b
forall k (f :: k -> *) d (c :: k). Star f d c -> d -> f c
runStar
    transpose :: Star m (Product (Star m) a b) c
-> Star m a (Exponential (Star m) b c)
transpose (Star Product (Star m) a b -> m c
f) = (a -> m (Star m b c)) -> Star m a (Star m b c)
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star ((a -> m (Star m b c)) -> Star m a (Star m b c))
-> (a -> m (Star m b c)) -> Star m a (Star m b c)
forall a b. (a -> b) -> a -> b
$ \a
a -> Star m b c -> m (Star m b c)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Star m b c -> m (Star m b c)) -> Star m b c -> m (Star m b c)
forall a b. (a -> b) -> a -> b
$ (b -> m c) -> Star m b c
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star ((b -> m c) -> Star m b c) -> (b -> m c) -> Star m b c
forall a b. (a -> b) -> a -> b
$ \b
b -> Product (Star m) a b -> m c
f (a
a, b
b)

-------------------------------------------------------------------------------
-- Kleisli
-------------------------------------------------------------------------------

instance Monad m => CartesianCategory (Kleisli m) where
    type Product (Kleisli m) = (,)

    proj1 :: Kleisli m (Product (Kleisli m) a b) a
proj1 = ((a, b) -> m a) -> Kleisli m (a, b) a
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> ((a, b) -> a) -> (a, b) -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> a
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) a
proj1)
    proj2 :: Kleisli m (Product (Kleisli m) a b) b
proj2 = ((a, b) -> m b) -> Kleisli m (a, b) b
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (b -> m b
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> m b) -> ((a, b) -> b) -> (a, b) -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> b
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) b
proj2)

    fanout :: Kleisli m a b
-> Kleisli m a c -> Kleisli m a (Product (Kleisli m) b c)
fanout (Kleisli a -> m b
f) (Kleisli a -> m c
g) = (a -> m (b, c)) -> Kleisli m a (b, c)
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli ((a -> m (b, c)) -> Kleisli m a (b, c))
-> (a -> m (b, c)) -> Kleisli m a (b, c)
forall a b. (a -> b) -> a -> b
$ \a
a -> (b -> c -> (b, c)) -> m b -> m c -> m (b, c)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) (a -> m b
f a
a) (a -> m c
g a
a)

instance Monad m => CategoryWith1 (Kleisli m) where
    type Terminal (Kleisli m) = ()

    terminal :: Kleisli m a (Terminal (Kleisli m))
terminal = (a -> m ()) -> Kleisli m a ()
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> m ()) -> (a -> ()) -> a -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ()
forall k (cat :: k -> k -> *) (a :: k).
CategoryWith1 cat =>
cat a (Terminal cat)
terminal)

instance Monad m => CocartesianCategory (Kleisli m) where
    type Coproduct (Kleisli m) = Either

    inl :: Kleisli m a (Coproduct (Kleisli m) a b)
inl = (a -> m (Either a b)) -> Kleisli m a (Either a b)
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (Either a b -> m (Either a b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either a b -> m (Either a b))
-> (a -> Either a b) -> a -> m (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either a b
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CocartesianCategory cat =>
cat a (Coproduct cat a b)
inl)
    inr :: Kleisli m b (Coproduct (Kleisli m) a b)
inr = (b -> m (Either a b)) -> Kleisli m b (Either a b)
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (Either a b -> m (Either a b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either a b -> m (Either a b))
-> (b -> Either a b) -> b -> m (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Either a b
forall k (cat :: k -> k -> *) (b :: k) (a :: k).
CocartesianCategory cat =>
cat b (Coproduct cat a b)
inr)

    fanin :: Kleisli m a c
-> Kleisli m b c -> Kleisli m (Coproduct (Kleisli m) a b) c
fanin (Kleisli a -> m c
f) (Kleisli b -> m c
g) = (Either a b -> m c) -> Kleisli m (Either a b) c
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli ((a -> m c) -> (b -> m c) -> Coproduct (->) a b -> m c
forall k (cat :: k -> k -> *) (a :: k) (c :: k) (b :: k).
CocartesianCategory cat =>
cat a c -> cat b c -> cat (Coproduct cat a b) c
fanin a -> m c
f b -> m c
g)

instance Monad m => CategoryWith0 (Kleisli m) where
    type Initial (Kleisli m) = Void

    initial :: Kleisli m (Initial (Kleisli m)) a
initial = (Void -> m a) -> Kleisli m Void a
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> (Void -> a) -> Void -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Void -> a
forall k (cat :: k -> k -> *) (a :: k).
CategoryWith0 cat =>
cat (Initial cat) a
initial)

instance Monad m => BicartesianCategory (Kleisli m) where
    distr :: Kleisli
  m
  (Product (Kleisli m) (Coproduct (Kleisli m) a b) c)
  (Coproduct
     (Kleisli m) (Product (Kleisli m) a c) (Product (Kleisli m) b c))
distr = ((Either a b, c) -> m (Either (a, c) (b, c)))
-> Kleisli m (Either a b, c) (Either (a, c) (b, c))
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (Either (a, c) (b, c) -> m (Either (a, c) (b, c))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (a, c) (b, c) -> m (Either (a, c) (b, c)))
-> ((Either a b, c) -> Either (a, c) (b, c))
-> (Either a b, c)
-> m (Either (a, c) (b, c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either a b, c) -> Either (a, c) (b, c)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
BicartesianCategory cat =>
cat
  (Product cat (Coproduct cat a b) c)
  (Coproduct cat (Product cat a c) (Product cat b c))
distr)

instance Monad m => CCC (Kleisli m) where
    type Exponential (Kleisli m) = Kleisli m

    eval :: Kleisli m (Product (Kleisli m) (Exponential (Kleisli m) a b) a) b
eval = ((Kleisli m a b, a) -> m b) -> Kleisli m (Kleisli m a b, a) b
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (((Kleisli m a b, a) -> m b) -> Kleisli m (Kleisli m a b, a) b)
-> ((Kleisli m a b, a) -> m b) -> Kleisli m (Kleisli m a b, a) b
forall a b. (a -> b) -> a -> b
$ (Kleisli m a b -> a -> m b) -> (Kleisli m a b, a) -> m b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Kleisli m a b -> a -> m b
forall (m :: * -> *) a b. Kleisli m a b -> a -> m b
runKleisli
    transpose :: Kleisli m (Product (Kleisli m) a b) c
-> Kleisli m a (Exponential (Kleisli m) b c)
transpose (Kleisli Product (Kleisli m) a b -> m c
f) = (a -> m (Kleisli m b c)) -> Kleisli m a (Kleisli m b c)
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli ((a -> m (Kleisli m b c)) -> Kleisli m a (Kleisli m b c))
-> (a -> m (Kleisli m b c)) -> Kleisli m a (Kleisli m b c)
forall a b. (a -> b) -> a -> b
$ \a
a -> Kleisli m b c -> m (Kleisli m b c)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kleisli m b c -> m (Kleisli m b c))
-> Kleisli m b c -> m (Kleisli m b c)
forall a b. (a -> b) -> a -> b
$ (b -> m c) -> Kleisli m b c
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli ((b -> m c) -> Kleisli m b c) -> (b -> m c) -> Kleisli m b c
forall a b. (a -> b) -> a -> b
$ \b
b -> Product (Kleisli m) a b -> m c
f (a
a, b
b)

-------------------------------------------------------------------------------
-- WrappedArrow
-------------------------------------------------------------------------------

newtype WrappedArrow arr a b = WrapArrow { WrappedArrow arr a b -> arr a b
unwrapArrow :: arr a b }

instance C.Category arr => C.Category (WrappedArrow arr) where
    id :: WrappedArrow arr a a
id = arr a a -> WrappedArrow arr a a
forall k k (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> WrappedArrow arr a b
WrapArrow arr a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
identity
    WrapArrow arr b c
f . :: WrappedArrow arr b c
-> WrappedArrow arr a b -> WrappedArrow arr a c
. WrapArrow arr a b
g = arr a c -> WrappedArrow arr a c
forall k k (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> WrappedArrow arr a b
WrapArrow (arr b c
f arr b c -> arr a b -> arr a c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
%% arr a b
g)

instance A.Arrow arr => CategoryWith1 (WrappedArrow arr) where
    type Terminal (WrappedArrow arr) = ()
    terminal :: WrappedArrow arr a (Terminal (WrappedArrow arr))
terminal = arr a () -> WrappedArrow arr a ()
forall k k (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> WrappedArrow arr a b
WrapArrow ((a -> ()) -> arr a ()
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
A.arr a -> ()
forall k (cat :: k -> k -> *) (a :: k).
CategoryWith1 cat =>
cat a (Terminal cat)
terminal)

instance A.Arrow arr => CartesianCategory (WrappedArrow arr) where
    type Product (WrappedArrow arr) = (,)
    proj1 :: WrappedArrow arr (Product (WrappedArrow arr) a b) a
proj1 = arr (a, b) a -> WrappedArrow arr (a, b) a
forall k k (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> WrappedArrow arr a b
WrapArrow (((a, b) -> a) -> arr (a, b) a
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
A.arr (a, b) -> a
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) a
proj1)
    proj2 :: WrappedArrow arr (Product (WrappedArrow arr) a b) b
proj2 = arr (a, b) b -> WrappedArrow arr (a, b) b
forall k k (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> WrappedArrow arr a b
WrapArrow (((a, b) -> b) -> arr (a, b) b
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
A.arr (a, b) -> b
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CartesianCategory cat =>
cat (Product cat a b) b
proj2)
    fanout :: WrappedArrow arr a b
-> WrappedArrow arr a c
-> WrappedArrow arr a (Product (WrappedArrow arr) b c)
fanout (WrapArrow arr a b
f) (WrapArrow arr a c
g) = arr a (b, c) -> WrappedArrow arr a (b, c)
forall k k (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> WrappedArrow arr a b
WrapArrow (arr a b
f arr a b -> arr a c -> arr a (b, c)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
A.&&& arr a c
g)

instance A.ArrowChoice arr => CategoryWith0 (WrappedArrow arr) where
    type Initial (WrappedArrow arr) = Void
    initial :: WrappedArrow arr (Initial (WrappedArrow arr)) a
initial = arr Void a -> WrappedArrow arr Void a
forall k k (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> WrappedArrow arr a b
WrapArrow ((Void -> a) -> arr Void a
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
A.arr Void -> a
forall a. Void -> a
absurd)

instance A.ArrowChoice arr => CocartesianCategory (WrappedArrow arr) where
    type Coproduct (WrappedArrow arr) = Either
    inl :: WrappedArrow arr a (Coproduct (WrappedArrow arr) a b)
inl = arr a (Either a b) -> WrappedArrow arr a (Either a b)
forall k k (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> WrappedArrow arr a b
WrapArrow ((a -> Either a b) -> arr a (Either a b)
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
A.arr a -> Either a b
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
CocartesianCategory cat =>
cat a (Coproduct cat a b)
inl)
    inr :: WrappedArrow arr b (Coproduct (WrappedArrow arr) a b)
inr = arr b (Either a b) -> WrappedArrow arr b (Either a b)
forall k k (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> WrappedArrow arr a b
WrapArrow ((b -> Either a b) -> arr b (Either a b)
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
A.arr b -> Either a b
forall k (cat :: k -> k -> *) (b :: k) (a :: k).
CocartesianCategory cat =>
cat b (Coproduct cat a b)
inr)
    fanin :: WrappedArrow arr a c
-> WrappedArrow arr b c
-> WrappedArrow arr (Coproduct (WrappedArrow arr) a b) c
fanin (WrapArrow arr a c
f) (WrapArrow arr b c
g) = arr (Either a b) c -> WrappedArrow arr (Either a b) c
forall k k (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> WrappedArrow arr a b
WrapArrow (arr a c
f arr a c -> arr b c -> arr (Either a b) c
forall (a :: * -> * -> *) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
A.||| arr b c
g)

instance A.ArrowChoice arr => BicartesianCategory (WrappedArrow arr) where
    distr :: WrappedArrow
  arr
  (Product (WrappedArrow arr) (Coproduct (WrappedArrow arr) a b) c)
  (Coproduct
     (WrappedArrow arr)
     (Product (WrappedArrow arr) a c)
     (Product (WrappedArrow arr) b c))
distr = arr (Either a b, c) (Either (a, c) (b, c))
-> WrappedArrow arr (Either a b, c) (Either (a, c) (b, c))
forall k k (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> WrappedArrow arr a b
WrapArrow (((Either a b, c) -> Either (a, c) (b, c))
-> arr (Either a b, c) (Either (a, c) (b, c))
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
A.arr (Either a b, c) -> Either (a, c) (b, c)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
BicartesianCategory cat =>
cat
  (Product cat (Coproduct cat a b) c)
  (Coproduct cat (Product cat a c) (Product cat b c))
distr)

instance A.ArrowApply arr => CCC (WrappedArrow arr) where
    type Exponential (WrappedArrow arr) = arr

    eval :: WrappedArrow
  arr
  (Product (WrappedArrow arr) (Exponential (WrappedArrow arr) a b) a)
  b
eval = arr (arr a b, a) b -> WrappedArrow arr (arr a b, a) b
forall k k (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> WrappedArrow arr a b
WrapArrow arr (arr a b, a) b
forall (a :: * -> * -> *) b c. ArrowApply a => a (a b c, b) c
A.app
    transpose :: WrappedArrow arr (Product (WrappedArrow arr) a b) c
-> WrappedArrow arr a (Exponential (WrappedArrow arr) b c)
transpose = [Char] -> WrappedArrow arr (a, b) c -> WrappedArrow arr a (arr b c)
forall a. HasCallStack => [Char] -> a
error [Char]
"ArrowApply @(WrappedArrow arr) is not implemented"

instance A.Arrow arr => GeneralizedElement (WrappedArrow arr) where
    type Object (WrappedArrow arr) a = a
    konst :: Object (WrappedArrow arr) a -> WrappedArrow arr x a
konst = arr x a -> WrappedArrow arr x a
forall k k (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> WrappedArrow arr a b
WrapArrow (arr x a -> WrappedArrow arr x a)
-> (a -> arr x a) -> a -> WrappedArrow arr x a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x -> a) -> arr x a
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
A.arr ((x -> a) -> arr x a) -> (a -> x -> a) -> a -> arr x a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> x -> a
forall a b. a -> b -> a
const