{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE PartialTypeSignatures #-}

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Wno-unused-imports #-} -- TEMP

{-# OPTIONS_GHC -fprint-potential-instances #-} -- TEMP

#include "ConCat/AbsTy.inc"
AbsTyPragmas

-- | Dual category for additive types. Use with GAD for efficient reverse mode AD.

module ConCat.Dual where

import Prelude hiding (id,(.),zip,unzip,zipWith,const)
import qualified Prelude as P

import Data.Constraint (Dict(..),(:-)(..))
import Data.Pointed
import Data.Key
import Data.Distributive (Distributive(..))
import Data.Functor.Rep (Representable)

import ConCat.Misc ((:*),(:^),inNew2,unzip,type (&+&))
import ConCat.Rep
import qualified ConCat.Category as C
-- import qualified ConCat.AltCat as A
import ConCat.AltCat
import ConCat.AdditiveFun (Additive,Additive1(..))

AbsTyImports

-- Category dual
newtype Dual k a b = Dual (b `k` a)

unDual :: Dual k a b -> b `k` a
unDual :: forall (k :: * -> * -> *) a b. Dual k a b -> k b a
unDual (Dual k b a
f) = k b a
f

-- I'd use newtype, but then I run into some coercion challenges.
-- TODO: investigate.

instance HasRep (Dual k a b) where
  type Rep (Dual k a b) = b `k` a
  abst :: Rep (Dual k a b) -> Dual k a b
abst = k b a -> Dual k a b
Rep (Dual k a b) -> Dual k a b
forall (k :: * -> * -> *) a b. k b a -> Dual k a b
Dual
  repr :: Dual k a b -> Rep (Dual k a b)
repr = Dual k a b -> k b a
Dual k a b -> Rep (Dual k a b)
forall (k :: * -> * -> *) a b. Dual k a b -> k b a
unDual
  {-# INLINE abst #-}
  {-# INLINE repr #-}

AbsTy(Dual k a b)

instance Category k => Category (Dual k) where
  type Ok (Dual k) = Ok k &+& Additive -- for ProductCat instance
  id :: forall a. Ok (Dual k) a => Dual k a a
id = Rep (Dual k a a) -> Dual k a a
forall a. HasRep a => Rep a -> a
abst k a a
Rep (Dual k a a)
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id
  . :: forall b c a.
Ok3 (Dual k) a b c =>
Dual k b c -> Dual k a b -> Dual k a c
(.) = (Rep (Dual k b c) -> Rep (Dual k a b) -> Rep (Dual k a c))
-> Dual k b c -> Dual k a b -> Dual k a c
forall p q r.
(HasRep p, HasRep q, HasRep r) =>
(Rep p -> Rep q -> Rep r) -> p -> q -> r
inAbst2 ((k b a -> k c b -> k c a) -> k c b -> k b a -> k c a
forall a b c. (a -> b -> c) -> b -> a -> c
flip k b a -> k c b -> k c a
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
(.))
  {-# INLINE id #-}
  {-# INLINE (.) #-}

-- I could define Ok (Dual k) = Ok k, and rely on Ok k and OkAdd k for Additive,
-- but doing do requires a lot of entailments and explicit signatures.

instance AssociativePCat k => AssociativePCat (Dual k) where
  lassocP :: forall a b c.
Ok3 (Dual k) a b c =>
Dual
  k
  (Prod (Dual k) a (Prod (Dual k) b c))
  (Prod (Dual k) (Prod (Dual k) a b) c)
lassocP = Rep (Dual k (a :* (b :* c)) ((a :* b) :* c))
-> Dual k (a :* (b :* c)) ((a :* b) :* c)
forall a. HasRep a => Rep a -> a
abst k ((a :* b) :* c) (a :* (b :* c))
Rep (Dual k (a :* (b :* c)) ((a :* b) :* c))
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
rassocP
  rassocP :: forall a b c.
Ok3 (Dual k) a b c =>
Dual
  k
  (Prod (Dual k) (Prod (Dual k) a b) c)
  (Prod (Dual k) a (Prod (Dual k) b c))
rassocP = Rep (Dual k ((a :* b) :* c) (a :* (b :* c)))
-> Dual k ((a :* b) :* c) (a :* (b :* c))
forall a. HasRep a => Rep a -> a
abst k (a :* (b :* c)) ((a :* b) :* c)
Rep (Dual k ((a :* b) :* c) (a :* (b :* c)))
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
lassocP
  {-# INLINE lassocP #-}
  {-# INLINE rassocP #-}

instance BraidedPCat k => BraidedPCat (Dual k) where
  swapP :: forall a b.
Ok2 (Dual k) a b =>
Dual k (Prod (Dual k) a b) (Prod (Dual k) b a)
swapP = Rep (Dual k (a :* b) (b :* a)) -> Dual k (a :* b) (b :* a)
forall a. HasRep a => Rep a -> a
abst k (b :* a) (a :* b)
Rep (Dual k (a :* b) (b :* a))
forall (k :: * -> * -> *) a b.
(BraidedPCat k, Ok2 k a b) =>
k (Prod k a b) (Prod k b a)
swapP
  {-# INLINE swapP #-}

instance MonoidalPCat k => MonoidalPCat (Dual k) where
  *** :: forall a b c d.
Ok4 (Dual k) a b c d =>
Dual k a c
-> Dual k b d -> Dual k (Prod (Dual k) a b) (Prod (Dual k) c d)
(***) = (Rep (Dual k a c)
 -> Rep (Dual k b d) -> Rep (Dual k (a :* b) (c :* d)))
-> Dual k a c -> Dual k b d -> Dual k (a :* b) (c :* d)
forall p q r.
(HasRep p, HasRep q, HasRep r) =>
(Rep p -> Rep q -> Rep r) -> p -> q -> r
inAbst2 k c a -> k d b -> k (c :* d) (a :* b)
Rep (Dual k a c)
-> Rep (Dual k b d) -> Rep (Dual k (a :* b) (c :* d))
forall (k :: * -> * -> *) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (Prod k a b) (Prod k c d)
(***)
  {-# INLINE (***) #-}

instance CoproductPCat k => ProductCat (Dual k) where
  exl :: forall a b. Ok2 (Dual k) a b => Dual k (Prod (Dual k) a b) a
exl   = Rep (Dual k (a :* b) a) -> Dual k (a :* b) a
forall a. HasRep a => Rep a -> a
abst k a (a :* b)
Rep (Dual k (a :* b) a)
forall (k :: * -> * -> *) a b.
(CoproductPCat k, Ok2 k a b) =>
k a (CoprodP k a b)
inlP
  exr :: forall a b. Ok2 (Dual k) a b => Dual k (Prod (Dual k) a b) b
exr   = Rep (Dual k (a :* b) b) -> Dual k (a :* b) b
forall a. HasRep a => Rep a -> a
abst k b (a :* b)
Rep (Dual k (a :* b) b)
forall (k :: * -> * -> *) a b.
(CoproductPCat k, Ok2 k a b) =>
k b (CoprodP k a b)
inrP
  dup :: forall a. Ok (Dual k) a => Dual k a (Prod (Dual k) a a)
dup   = Rep (Dual k a (a :* a)) -> Dual k a (a :* a)
forall a. HasRep a => Rep a -> a
abst k (a :* a) a
Rep (Dual k a (a :* a))
forall (k :: * -> * -> *) a.
(CoproductPCat k, Ok k a) =>
k (CoprodP k a a) a
jamP
  {-# INLINE exl #-}
  {-# INLINE exr #-}
  {-# INLINE dup #-}

instance UnitCat k => UnitCat (Dual k) where
  lunit :: forall a.
Ok (Dual k) a =>
Dual k a (Prod (Dual k) (Unit (Dual k)) a)
lunit = Rep (Dual k a (Unit (Dual k) :* a))
-> Dual k a (Unit (Dual k) :* a)
forall a. HasRep a => Rep a -> a
abst k (Unit (Dual k) :* a) a
Rep (Dual k a (Unit (Dual k) :* a))
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k (Prod k (Unit (Dual k)) a) a
lcounit
  runit :: forall a.
Ok (Dual k) a =>
Dual k a (Prod (Dual k) a (Unit (Dual k)))
runit = Rep (Dual k a (a :* Unit (Dual k)))
-> Dual k a (a :* Unit (Dual k))
forall a. HasRep a => Rep a -> a
abst k (a :* Unit (Dual k)) a
Rep (Dual k a (a :* Unit (Dual k)))
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k (Prod k a (Unit (Dual k))) a
rcounit
  lcounit :: forall a.
Ok (Dual k) a =>
Dual k (Prod (Dual k) (Unit (Dual k)) a) a
lcounit = Rep (Dual k (Unit (Dual k) :* a) a)
-> Dual k (Unit (Dual k) :* a) a
forall a. HasRep a => Rep a -> a
abst k a (Unit (Dual k) :* a)
Rep (Dual k (Unit (Dual k) :* a) a)
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k a (Prod k (Unit (Dual k)) a)
lunit
  rcounit :: forall a.
Ok (Dual k) a =>
Dual k (Prod (Dual k) a (Unit (Dual k))) a
rcounit = Rep (Dual k (a :* Unit (Dual k)) a)
-> Dual k (a :* Unit (Dual k)) a
forall a. HasRep a => Rep a -> a
abst k a (a :* Unit (Dual k))
Rep (Dual k (a :* Unit (Dual k)) a)
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k a (Prod k a (Unit (Dual k)))
runit
  {-# INLINE lunit #-}
  {-# INLINE runit #-}
  {-# INLINE lcounit #-}
  {-# INLINE rcounit #-}

-- TODO: drop the M in MProductCat when I move (||||) out of CoproductPCat
instance (BraidedPCat k, ProductCat k) => CoproductPCat (Dual k) where
  inlP :: forall a b. Ok2 (Dual k) a b => Dual k a (CoprodP (Dual k) a b)
inlP = Rep (Dual k a (CoprodP (Dual k) a b))
-> Dual k a (CoprodP (Dual k) a b)
forall a. HasRep a => Rep a -> a
abst k (CoprodP (Dual k) a b) a
Rep (Dual k a (CoprodP (Dual k) a b))
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exl
  inrP :: forall a b. Ok2 (Dual k) a b => Dual k b (CoprodP (Dual k) a b)
inrP = Rep (Dual k b (CoprodP (Dual k) a b))
-> Dual k b (CoprodP (Dual k) a b)
forall a. HasRep a => Rep a -> a
abst k (CoprodP (Dual k) a b) b
Rep (Dual k b (CoprodP (Dual k) a b))
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr
  jamP :: forall a. Ok (Dual k) a => Dual k (CoprodP (Dual k) a a) a
jamP = Rep (Dual k (CoprodP (Dual k) a a) a)
-> Dual k (CoprodP (Dual k) a a) a
forall a. HasRep a => Rep a -> a
abst k a (CoprodP (Dual k) a a)
Rep (Dual k (CoprodP (Dual k) a a) a)
forall (k :: * -> * -> *) a.
(ProductCat k, Ok k a) =>
k a (Prod k a a)
dup
  {-# INLINE inlP #-}
  {-# INLINE inrP #-}
  {-# INLINE jamP #-}

instance ScalarCat k s => ScalarCat (Dual k) s where
  scale :: s -> Dual k s s
scale s
s = Rep (Dual k s s) -> Dual k s s
forall a. HasRep a => Rep a -> a
abst (s -> k s s
forall (k :: * -> * -> *) a. ScalarCat k a => a -> k a a
scale s
s)

instance (OkIxProd k h, Additive1 h) => OkIxProd (Dual k) h where
  okIxProd :: forall a. Ok' (Dual k) a |- Ok' (Dual k) (h a)
  okIxProd :: forall a. Ok' (Dual k) a |- Ok' (Dual k) (h a)
okIxProd = (Con (Sat (Ok k &+& Additive) a)
 :- Con (Sat (Ok k &+& Additive) (h a)))
-> Sat (Ok k &+& Additive) a |- Sat (Ok k &+& Additive) (h a)
forall a b. (Con a :- Con b) -> a |- b
Entail (((&+&) (Ok k) Additive a => Dict ((&+&) (Ok k) Additive (h a)))
-> (&+&) (Ok k) Additive a :- (&+&) (Ok k) Additive (h a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Dict ((&+&) (Ok k) Additive (h a))
Con (Sat (Ok k) (h a)) => Dict ((&+&) (Ok k) Additive (h a))
forall (a :: Constraint). a => Dict a
Dict (Con (Sat (Ok k) (h a)) => Dict ((&+&) (Ok k) Additive (h a)))
-> (Sat (Ok k) a |- Sat (Ok k) (h a))
-> Dict ((&+&) (Ok k) Additive (h a))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) (h :: * -> *) a.
OkIxProd k h =>
Ok' k a |- Ok' k (h a)
okIxProd @k @h @a (Con (Sat Additive (h a)) => Dict ((&+&) (Ok k) Additive (h a)))
-> (Sat Additive a |- Sat Additive (h a))
-> Dict ((&+&) (Ok k) Additive (h a))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (h :: * -> *) a.
Additive1 h =>
Sat Additive a |- Sat Additive (h a)
additive1 @h @a))

instance (IxMonoidalPCat k h, Functor h, Additive1 h) => IxMonoidalPCat (Dual k) h where
  crossF :: forall a b.
Ok2 (Dual k) a b =>
h (Dual k a b) -> Dual k (h a) (h b)
crossF = (h (Rep (Dual k a b)) -> Rep (Dual k (h a) (h b)))
-> h (Dual k a b) -> Dual k (h a) (h b)
forall p q (f :: * -> *).
(HasRep p, HasRep q, Functor f) =>
(f (Rep p) -> Rep q) -> f p -> q
inAbstF1 h (k b a) -> k (h b) (h a)
h (Rep (Dual k a b)) -> Rep (Dual k (h a) (h b))
forall (k :: * -> * -> *) (h :: * -> *) a b.
(IxMonoidalPCat k h, Ok2 k a b) =>
h (k a b) -> k (h a) (h b)
crossF -- plusPF
  {-# INLINE crossF #-}

instance (IxCoproductPCat k h, Functor h, Additive1 h) => IxProductCat (Dual k) h where
  exF :: forall a. Ok (Dual k) a => h (Dual k (h a) a)
exF    = k a (h a) -> Dual k (h a) a
Rep (Dual k (h a) a) -> Dual k (h a) a
forall a. HasRep a => Rep a -> a
abst (k a (h a) -> Dual k (h a) a)
-> h (k a (h a)) -> h (Dual k (h a) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> h (k a (h a))
forall (k :: * -> * -> *) (h :: * -> *) a.
(IxCoproductPCat k h, Ok k a) =>
h (k a (h a))
inPF
  forkF :: forall a b. Ok2 (Dual k) a b => h (Dual k a b) -> Dual k a (h b)
forkF  = (h (Rep (Dual k a b)) -> Rep (Dual k a (h b)))
-> h (Dual k a b) -> Dual k a (h b)
forall p q (f :: * -> *).
(HasRep p, HasRep q, Functor f) =>
(f (Rep p) -> Rep q) -> f p -> q
inAbstF1 h (k b a) -> k (h b) a
h (Rep (Dual k a b)) -> Rep (Dual k a (h b))
forall (k :: * -> * -> *) (h :: * -> *) a b.
(IxCoproductPCat k h, Ok2 k a b) =>
h (k b a) -> k (h b) a
joinPF
  replF :: forall a. Ok (Dual k) a => Dual k a (h a)
replF  = Rep (Dual k a (h a)) -> Dual k a (h a)
forall a. HasRep a => Rep a -> a
abst k (h a) a
Rep (Dual k a (h a))
forall (k :: * -> * -> *) (h :: * -> *) a.
(IxCoproductPCat k h, Ok k a) =>
k (h a) a
jamPF
  {-# INLINE exF #-}
  {-# INLINE forkF #-}
  {-# INLINE replF #-}

-- instance ({- IxProductCat k h, Functor h, Additive1 h -}) => IxMonoidalPCat (Dual k) h where
--   plusPF = inAbstF1 crossF
--   {-# INLINE plusPF #-}

instance (IxProductCat k h, Functor h, Additive1 h) => IxCoproductPCat (Dual k) h where
  inPF :: forall a. Ok (Dual k) a => h (Dual k a (h a))
inPF   = k (h a) a -> Dual k a (h a)
Rep (Dual k a (h a)) -> Dual k a (h a)
forall a. HasRep a => Rep a -> a
abst (k (h a) a -> Dual k a (h a))
-> h (k (h a) a) -> h (Dual k a (h a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> h (k (h a) a)
forall (k :: * -> * -> *) (h :: * -> *) a.
(IxProductCat k h, Ok k a) =>
h (k (h a) a)
exF
  joinPF :: forall a b. Ok2 (Dual k) a b => h (Dual k b a) -> Dual k (h b) a
joinPF = (h (Rep (Dual k b a)) -> Rep (Dual k (h b) a))
-> h (Dual k b a) -> Dual k (h b) a
forall p q (f :: * -> *).
(HasRep p, HasRep q, Functor f) =>
(f (Rep p) -> Rep q) -> f p -> q
inAbstF1 h (k a b) -> k a (h b)
h (Rep (Dual k b a)) -> Rep (Dual k (h b) a)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(IxProductCat k h, Ok2 k a b) =>
h (k a b) -> k a (h b)
forkF
  jamPF :: forall a. Ok (Dual k) a => Dual k (h a) a
jamPF  = Rep (Dual k (h a) a) -> Dual k (h a) a
forall a. HasRep a => Rep a -> a
abst k a (h a)
Rep (Dual k (h a) a)
forall (k :: * -> * -> *) (h :: * -> *) a.
(IxProductCat k h, Ok k a) =>
k a (h a)
replF
  {-# INLINE inPF #-}
  {-# INLINE joinPF #-}
  {-# INLINE jamPF #-}

#if 1

-- This ProductCat definition corresponds to the *coproduct* (direct sum) for
-- the Ab category, following duality. TODO: when we have associated products,
-- coproducts, etc, generalize Dual to operate on any category, not just (->).

-- instance (ConstCat k b, Ok k b) => ConstCat (Dual k) b where
--   -- const _ = abst (const zero)  -- TODO: justify via specification
--   const _ = abst ()
--   {-# INLINE const #-}

instance TerminalCat k => CoterminalCat (Dual k) where
  ti :: forall a. Ok (Dual k) a => Dual k (Unit (Dual k)) a
ti = Rep (Dual k (Unit (Dual k)) a) -> Dual k (Unit (Dual k)) a
forall a. HasRep a => Rep a -> a
abst k a (Unit (Dual k))
Rep (Dual k (Unit (Dual k)) a)
forall (k :: * -> * -> *) a.
(TerminalCat k, Ok k a) =>
k a (Unit (Dual k))
it

instance CoterminalCat k => TerminalCat (Dual k) where
  it :: forall a. Ok (Dual k) a => Dual k a (Unit (Dual k))
it = Rep (Dual k a (Unit (Dual k))) -> Dual k a (Unit (Dual k))
forall a. HasRep a => Rep a -> a
abst k (Unit (Dual k)) a
Rep (Dual k a (Unit (Dual k)))
forall (k :: * -> * -> *) a.
(CoterminalCat k, Ok k a) =>
k (Unit (Dual k)) a
ti

-- const b :: a -> b
-- ?? :: a `k` b

-- it :: a `k` ()
-- ti :: () `k` b
-- ti . it :: a `k` b

-- Is there a standard name for ti . it ?

instance (Category k, TerminalCat k, CoterminalCat k, Ok (Dual k) b) => ConstCat (Dual k) b where
  const :: forall a.
Ok (Dual k) a =>
ConstObj (Dual k) b -> Dual k a (ConstObj (Dual k) b)
const ConstObj (Dual k) b
_ = Rep (Dual k a (ConstObj (Dual k) b))
-> Dual k a (ConstObj (Dual k) b)
forall a. HasRep a => Rep a -> a
abst (k (Unit (Dual k)) a
forall (k :: * -> * -> *) a.
(CoterminalCat k, Ok k a) =>
k (Unit (Dual k)) a
ti k (Unit (Dual k)) a
-> k (ConstObj (Dual k) b) (Unit (Dual k))
-> k (ConstObj (Dual k) b) a
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k (ConstObj (Dual k) b) (Unit (Dual k))
forall (k :: * -> * -> *) a.
(TerminalCat k, Ok k a) =>
k a (Unit (Dual k))
it)
  {-# INLINE const #-}

-- I'm unsure about this ConstCat instance.

#endif

instance CoerceCat k b a => CoerceCat (Dual k) a b where
  coerceC :: Dual k a b
coerceC = Rep (Dual k a b) -> Dual k a b
forall a. HasRep a => Rep a -> a
abst k b a
Rep (Dual k a b)
forall (k :: * -> * -> *) a b. CoerceCat k a b => k a b
coerceC

instance RepCat k a r => RepCat (Dual k) a r where
  abstC :: Dual k r a
abstC = k a r -> Dual k r a
forall (k :: * -> * -> *) a b. k b a -> Dual k a b
Dual (forall (k :: * -> * -> *) a r. RepCat k a r => k a r
reprC @k @a @r)
  reprC :: Dual k a r
reprC = k r a -> Dual k a r
forall (k :: * -> * -> *) a b. k b a -> Dual k a b
Dual (forall (k :: * -> * -> *) a r. RepCat k a r => k r a
abstC @k @a @r)
  {-# INLINE abstC #-}
  {-# INLINE reprC #-}

-- abstC :: a `k` r
-- Dual abstC :: Dual k r a
-- 
-- reprC :: r `k` a
-- Dual reprC :: Dual k a r

---- Functor-level:

type OkF k h = (Additive1 h, OkFunctor k h)

instance (OkFunctor k h, Additive1 h) => OkFunctor (Dual k) h where
  okFunctor :: forall a. Ok' (Dual k) a |- Ok' (Dual k) (h a)
  okFunctor :: forall a. Ok' (Dual k) a |- Ok' (Dual k) (h a)
okFunctor = (Con (Sat (Ok k &+& Additive) a)
 :- Con (Sat (Ok k &+& Additive) (h a)))
-> Sat (Ok k &+& Additive) a |- Sat (Ok k &+& Additive) (h a)
forall a b. (Con a :- Con b) -> a |- b
Entail (((&+&) (Ok k) Additive a => Dict ((&+&) (Ok k) Additive (h a)))
-> (&+&) (Ok k) Additive a :- (&+&) (Ok k) Additive (h a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Dict ((&+&) (Ok k) Additive (h a))
Con (Sat (Ok k) (h a)) => Dict ((&+&) (Ok k) Additive (h a))
forall (a :: Constraint). a => Dict a
Dict (Con (Sat (Ok k) (h a)) => Dict ((&+&) (Ok k) Additive (h a)))
-> (Sat (Ok k) a |- Sat (Ok k) (h a))
-> Dict ((&+&) (Ok k) Additive (h a))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) (h :: * -> *) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor @k @h @a (Con (Sat Additive (h a)) => Dict ((&+&) (Ok k) Additive (h a)))
-> (Sat Additive a |- Sat Additive (h a))
-> Dict ((&+&) (Ok k) Additive (h a))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (h :: * -> *) a.
Additive1 h =>
Sat Additive a |- Sat Additive (h a)
additive1 @h @a))
  {-# INLINE okFunctor #-}

instance (Functor h, ZipCat k h, Additive1 h, FunctorCat k h) => FunctorCat (Dual k) h where
  fmapC :: forall a b. Ok2 (Dual k) a b => Dual k a b -> Dual k (h a) (h b)
fmapC  = (Rep (Dual k a b) -> Rep (Dual k (h a) (h b)))
-> Dual k a b -> Dual k (h a) (h b)
forall p q. (HasRep p, HasRep q) => (Rep p -> Rep q) -> p -> q
inAbst k b a -> k (h b) (h a)
Rep (Dual k a b) -> Rep (Dual k (h a) (h b))
forall (k :: * -> * -> *) (h :: * -> *) a b.
(FunctorCat k h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC
  unzipC :: forall a b. Ok2 (Dual k) a b => Dual k (h (a :* b)) (h a :* h b)
unzipC = Rep (Dual k (h (a :* b)) (h a :* h b))
-> Dual k (h (a :* b)) (h a :* h b)
forall a. HasRep a => Rep a -> a
abst k (h a :* h b) (h (a :* b))
Rep (Dual k (h (a :* b)) (h a :* h b))
forall (k :: * -> * -> *) (h :: * -> *) a b.
(ZipCat k h, Ok2 k a b) =>
k (h a :* h b) (h (a :* b))
zipC
  {-# INLINE fmapC #-}
  {-# INLINE unzipC #-}

instance (Zip h, Additive1 h, FunctorCat k h) => ZipCat (Dual k) h where
  zipC :: forall a b. Ok2 (Dual k) a b => Dual k (h a :* h b) (h (a :* b))
zipC = Rep (Dual k (h a :* h b) (h (a :* b)))
-> Dual k (h a :* h b) (h (a :* b))
forall a. HasRep a => Rep a -> a
abst k (h (a :* b)) (h a :* h b)
Rep (Dual k (h a :* h b) (h (a :* b)))
forall (k :: * -> * -> *) (h :: * -> *) a b.
(FunctorCat k h, Ok2 k a b) =>
k (h (a :* b)) (h a :* h b)
unzipC
  {-# INLINE zipC #-}
  -- {-# INLINE zipWithC #-}

instance (Zip h, ZapCat k h, OkF k h) => ZapCat (Dual k) h where
  zapC :: Ok2 k a b => h (Dual k a b) -> Dual k (h a) (h b)
  -- zapC = A.abstC . A.zapC . A.fmapC A.reprC
  -- zapC = abst . A.zapC . fmap repr
  zapC :: forall a b. Ok2 k a b => h (Dual k a b) -> Dual k (h a) (h b)
zapC = k (h b) (h a) -> Dual k (h a) (h b)
Rep (Dual k (h a) (h b)) -> Dual k (h a) (h b)
forall a. HasRep a => Rep a -> a
abst (k (h b) (h a) -> Dual k (h a) (h b))
-> (h (Dual k a b) -> k (h b) (h a))
-> h (Dual k a b)
-> Dual k (h a) (h b)
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. h (k b a) -> k (h b) (h a)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(ZapCat k h, Ok2 k a b) =>
h (k a b) -> k (h a) (h b)
zapC (h (k b a) -> k (h b) (h a))
-> (h (Dual k a b) -> h (k b a)) -> h (Dual k a b) -> k (h b) (h a)
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Dual k a b -> k b a) -> h (Dual k a b) -> h (k b a)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(FunctorCat k h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC Dual k a b -> k b a
Dual k a b -> Rep (Dual k a b)
forall a. HasRep a => a -> Rep a
repr
  {-# INLINE zapC #-}

-- fmap repr :: h (a `Dual` b) -> h (b -> a)
-- zapC      :: h (b -> a) -> (h b -> h a)
-- abst      :: (h b -> h a) -> (h a `Dual` h b)

instance (PointedCat k h a, Additive a) => AddCat (Dual k) h a where
  sumAC :: Dual k (h a) a
sumAC = Rep (Dual k (h a) a) -> Dual k (h a) a
forall a. HasRep a => Rep a -> a
abst k a (h a)
Rep (Dual k (h a) a)
forall (k :: * -> * -> *) (h :: * -> *) a.
PointedCat k h a =>
k a (h a)
pointC
  {-# INLINE sumAC #-}

instance (AddCat k h a, Additive a, OkF k h) => PointedCat (Dual k) h a where
  pointC :: Dual k a (h a)
pointC = Rep (Dual k a (h a)) -> Dual k a (h a)
forall a. HasRep a => Rep a -> a
abst k (h a) a
Rep (Dual k a (h a))
forall (k :: * -> * -> *) (h :: * -> *) a.
AddCat k h a =>
k (h a) a
sumAC
  {-# INLINE pointC #-}

-- instance (Category k, FunctorCat k h, ZipCat k h, Zip h, AddCat k h) => Strong (Dual k) h where
--   -- TODO: maybe eliminate strength as method
--   strength :: forall a b. Ok2 k a b => Dual k (a :* h b) (h (a :* b))
--   strength = abst (first sumAC . unzipC)
--   {-# INLINE strength #-}

-- -- TODO: can I use sumA instead of A.sumAC?

instance TraversableCat k f t => TraversableCat (Dual k) t f where
  sequenceAC :: forall a. Ok (Dual k) a => Dual k (t (f a)) (f (t a))
sequenceAC = Rep (Dual k (t (f a)) (f (t a))) -> Dual k (t (f a)) (f (t a))
forall a. HasRep a => Rep a -> a
abst k (f (t a)) (t (f a))
Rep (Dual k (t (f a)) (f (t a)))
forall (k :: * -> * -> *) (t :: * -> *) (f :: * -> *) a.
(TraversableCat k t f, Ok k a) =>
k (t (f a)) (f (t a))
sequenceAC
  {-# INLINE sequenceAC #-}

instance DistributiveCat k f g => DistributiveCat (Dual k) g f where
  distributeC :: forall a. Ok (Dual k) a => Dual k (f (g a)) (g (f a))
distributeC = Rep (Dual k (f (g a)) (g (f a))) -> Dual k (f (g a)) (g (f a))
forall a. HasRep a => Rep a -> a
abst k (g (f a)) (f (g a))
Rep (Dual k (f (g a)) (g (f a)))
forall (k :: * -> * -> *) (g :: * -> *) (f :: * -> *) a.
(DistributiveCat k g f, Ok k a) =>
k (f (g a)) (g (f a))
distributeC
  {-# INLINE distributeC #-}

instance RepresentableCat k g => RepresentableCat (Dual k) g where
  indexC :: forall a. Ok (Dual k) a => Dual k (g a) (Rep g -> a)
indexC    = Rep (Dual k (g a) (Rep g -> a)) -> Dual k (g a) (Rep g -> a)
forall a. HasRep a => Rep a -> a
abst k (Rep g -> a) (g a)
Rep (Dual k (g a) (Rep g -> a))
forall (k :: * -> * -> *) (f :: * -> *) a.
(RepresentableCat k f, Ok k a) =>
k (Rep f -> a) (f a)
tabulateC
  tabulateC :: forall a. Ok (Dual k) a => Dual k (Rep g -> a) (g a)
tabulateC = Rep (Dual k (Rep g -> a) (g a)) -> Dual k (Rep g -> a) (g a)
forall a. HasRep a => Rep a -> a
abst k (g a) (Rep g -> a)
Rep (Dual k (Rep g -> a) (g a))
forall (k :: * -> * -> *) (f :: * -> *) a.
(RepresentableCat k f, Ok k a) =>
k (f a) (Rep f -> a)
indexC
  {-# INLINE indexC #-}
  {-# INLINE tabulateC #-}

instance (Additive a, Additive1 h, MinMaxFunctorCat (->) h a, PointedCat k h a) => MinMaxFFunctorCat (Dual k) h a where
  minimumCF :: h a -> a :* Dual k (h a) a
minimumCF h a
h = (h a -> a
forall (k :: * -> * -> *) (h :: * -> *) a.
(MinMaxFunctorCat k h a, OkFunctor k h, Ok k a) =>
k (h a) a
minimumC h a
h, Rep (Dual k (h a) a) -> Dual k (h a) a
forall a. HasRep a => Rep a -> a
abst k a (h a)
Rep (Dual k (h a) a)
forall (k :: * -> * -> *) (h :: * -> *) a.
PointedCat k h a =>
k a (h a)
pointC)
  {-# INLINE minimumCF #-}
  maximumCF :: h a -> a :* Dual k (h a) a
maximumCF h a
h = (h a -> a
forall (k :: * -> * -> *) (h :: * -> *) a.
(MinMaxFunctorCat k h a, OkFunctor k h, Ok k a) =>
k (h a) a
maximumC h a
h, Rep (Dual k (h a) a) -> Dual k (h a) a
forall a. HasRep a => Rep a -> a
abst k a (h a)
Rep (Dual k (h a) a)
forall (k :: * -> * -> *) (h :: * -> *) a.
PointedCat k h a =>
k a (h a)
pointC)
  {-# INLINE maximumCF #-}

{--------------------------------------------------------------------
    CCC interface
--------------------------------------------------------------------}

toDual :: forall k a b. (a -> b) -> (b `k` a)
toDual :: forall (k :: * -> * -> *) a b. (a -> b) -> k b a
toDual a -> b
f = Dual k a b -> k b a
forall (k :: * -> * -> *) a b. Dual k a b -> k b a
unDual ((a -> b) -> Dual k a b
forall (k :: * -> * -> *) a b. (a -> b) -> k a b
toCcc a -> b
f)
{-# INLINE toDual #-}