module Kindly.Class where

--------------------------------------------------------------------------------

import Control.Category
import Data.Kind (Constraint)
import Data.Semigroupoid (Semigroupoid (..))
import GHC.Base (Type)

--------------------------------------------------------------------------------

-- | A functor @f@ between categories @from@ and @to@ sends objects in
-- @Dom f@ to objects in @Cod f@ and morphisms in @Dom f@ to
-- morphisms in @Dom f@.
--
-- === Laws
--
-- [Identity]    @'map' 'id' == 'id'@
-- [Composition] @'map' (f . g) == 'map' f . 'map' g@
type CategoricalFunctor :: (from -> to) -> Constraint
class (Category (Dom f), Category (Cod f)) => CategoricalFunctor (f :: from -> to) where
  -- | @Dom f@ is the source category for the functor @f@.
  type Dom f :: from -> from -> Type

  -- | @Cod f@ is the target category for the functor @f@.
  type Cod f :: to -> to -> Type

  -- | Lift a function of type @Dom f a b@ into a function of type @Cod f (f a) (f b)@.
  map :: Dom f a b -> Cod f (f a) (f b)

type Cat i = i -> i -> Type

-- | A Natural Transformation betweeen two functors @f@ and @g@.
type Nat :: Cat s -> Cat t -> Cat (s -> t)
newtype Nat source target f g where
  Nat :: (forall x. target (f x) (g x)) -> Nat source target f g

runNat :: Nat source target f g -> (forall x. target (f x) (g x))
runNat :: forall {s} {t} (source :: Cat s) (target :: Cat t) (f :: s -> t)
       (g :: s -> t).
Nat source target f g -> forall (x :: s). target (f x) (g x)
runNat (Nat forall (x :: s). target (f x) (g x)
f) = target (f x) (g x)
forall (x :: s). target (f x) (g x)
f

infixr 0 ~>

type (~>) c1 c2 = Nat c1 c2

instance (Semigroupoid c1, Semigroupoid c2) => Semigroupoid (Nat c1 c2) where
  o :: Nat c1 c2 j k1 -> Nat c1 c2 i j -> Nat c1 c2 i k1
  Nat forall (x :: s). c2 (j x) (k1 x)
c1 o :: forall (j :: s -> t) (k1 :: s -> t) (i :: s -> t).
Nat c1 c2 j k1 -> Nat c1 c2 i j -> Nat c1 c2 i k1
`o` Nat forall (x :: s). c2 (i x) (j x)
c2 = (forall (x :: s). c2 (i x) (k1 x)) -> Nat c1 c2 i k1
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat (c2 (j x) (k1 x)
forall (x :: s). c2 (j x) (k1 x)
c1 c2 (j x) (k1 x) -> c2 (i x) (j x) -> c2 (i x) (k1 x)
forall (j :: t) (k1 :: t) (i :: t). c2 j k1 -> c2 i j -> c2 i k1
forall {k} (c :: k -> k -> *) (j :: k) (k1 :: k) (i :: k).
Semigroupoid c =>
c j k1 -> c i j -> c i k1
`o` c2 (i x) (j x)
forall (x :: s). c2 (i x) (j x)
c2)

instance (Semigroupoid c1, Semigroupoid c2, Category c1, Category c2) => Category (c1 ~> c2) where
  id :: (c1 ~> c2) a a
  id :: forall (a :: s -> t). (~>) c1 c2 a a
id = (forall (x :: s). c2 (a x) (a x)) -> Nat c1 c2 a a
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat c2 (a x) (a x)
forall (x :: s). c2 (a x) (a x)
forall (a :: t). c2 a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

  . :: forall (b :: s -> t) (c :: s -> t) (a :: s -> t).
(~>) c1 c2 b c -> (~>) c1 c2 a b -> (~>) c1 c2 a c
(.) = Nat c1 c2 b c -> Nat c1 c2 a b -> Nat c1 c2 a c
forall {k} (c :: k -> k -> *) (j :: k) (k1 :: k) (i :: k).
Semigroupoid c =>
c j k1 -> c i j -> c i k1
forall (b :: s -> t) (c :: s -> t) (a :: s -> t).
(~>) c1 c2 b c -> (~>) c1 c2 a b -> (~>) c1 c2 a c
o

type FunctorOf :: Cat from -> Cat to -> (from -> to) -> Constraint
class (CategoricalFunctor f, dom ~ Dom f, cod ~ Cod f) => FunctorOf dom cod f

instance (CategoricalFunctor f, dom ~ Dom f, cod ~ Cod f) => FunctorOf dom cod f

--------------------------------------------------------------------------------
-- NOTE: These these classes go from right to left:

class (FunctorOf cat1 (->) p) => MapArg1 cat1 p | p -> cat1 where
  map1 :: (a `cat1` b) -> p a -> p b
  map1 = cat1 a b -> p a -> p b
Dom p a b -> Cod p (p a) (p b)
forall (a :: from) (b :: from). Dom p a b -> Cod p (p a) (p b)
forall from to (f :: from -> to) (a :: from) (b :: from).
CategoricalFunctor f =>
Dom f a b -> Cod f (f a) (f b)
map

class (FunctorOf cat1 (cat2 ~> (->)) p, forall x. MapArg1 cat2 (p x)) => MapArg2 cat1 cat2 p | p -> cat2 cat2 where
  map2 :: (a `cat1` b) -> forall x. p a x -> p b x
  map2 = Nat cat2 (->) (p a) (p b) -> p a x -> p b x
Nat cat2 (->) (p a) (p b) -> forall (x :: s). p a x -> p b x
forall {s} {t} (source :: Cat s) (target :: Cat t) (f :: s -> t)
       (g :: s -> t).
Nat source target f g -> forall (x :: s). target (f x) (g x)
runNat (Nat cat2 (->) (p a) (p b) -> p a x -> p b x)
-> (cat1 a b -> Nat cat2 (->) (p a) (p b))
-> cat1 a b
-> p a x
-> p b x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. cat1 a b -> Nat cat2 (->) (p a) (p b)
Dom p a b -> Cod p (p a) (p b)
forall (a :: from) (b :: from). Dom p a b -> Cod p (p a) (p b)
forall from to (f :: from -> to) (a :: from) (b :: from).
CategoricalFunctor f =>
Dom f a b -> Cod f (f a) (f b)
map

class (FunctorOf cat1 (cat2 ~> cat3 ~> (->)) p, forall x. MapArg2 cat2 cat3 (p x)) => MapArg3 cat1 cat2 cat3 p | p -> cat1 cat2 cat3 where
  map3 :: (a `cat1` b) -> forall x y. p a x y -> p b x y
  map3 cat1 a b
f = Nat cat3 (->) (p a x) (p b x)
-> forall (x :: s). p a x x -> p b x x
forall {s} {t} (source :: Cat s) (target :: Cat t) (f :: s -> t)
       (g :: s -> t).
Nat source target f g -> forall (x :: s). target (f x) (g x)
runNat (Nat cat2 (cat3 ~> (->)) (p a) (p b)
-> forall (x :: s). Nat cat3 (->) (p a x) (p b x)
forall {s} {t} (source :: Cat s) (target :: Cat t) (f :: s -> t)
       (g :: s -> t).
Nat source target f g -> forall (x :: s). target (f x) (g x)
runNat (Dom p a b -> Cod p (p a) (p b)
forall (a :: from) (b :: from). Dom p a b -> Cod p (p a) (p b)
forall from to (f :: from -> to) (a :: from) (b :: from).
CategoricalFunctor f =>
Dom f a b -> Cod f (f a) (f b)
map cat1 a b
Dom p a b
f))