{-# LANGUAGE
    GADTs
  , PolyKinds
  , RankNTypes
  , ConstraintKinds
  , NoImplicitPrelude
  , TypeOperators
  , TypeFamilies
  , PatternSynonyms
  , FlexibleContexts
  , FlexibleInstances
  , UndecidableInstances
  , GeneralizedNewtypeDeriving
  #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Functor
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category.Functor (

  -- * Cat
    Cat(..)

  -- * Functors
  , Functor(..)
  , FunctorOf

  -- ** Functor instances
  , Id(..)
  , (:.:)(..)
  , Const(..), ConstF
  , OpOp(..)
  , OpOpInv(..)
  , Any(..)

  -- *** Related to the product category
  , Proj1(..)
  , Proj2(..)
  , (:***:)(..)
  , DiagProd(..)
  , Tuple1, pattern Tuple1
  , Tuple2, pattern Tuple2
  , Swap, pattern Swap

  -- *** Hom functors
  , Hom(..)
  , (:*-:), pattern HomX_
  , (:-*:), pattern Hom_X

  -- *** Profunctors
  , ProfunctorOf

) where

import Data.Kind (Type)

import Data.Category
import Data.Category.Product

infixr 9 %
infixr 9 :%



-- | Functors map objects and arrows.
class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where

  -- | The domain, or source category, of the functor.
  type Dom ftag :: Type -> Type -> Type
  -- | The codomain, or target category, of the functor.
  type Cod ftag :: Type -> Type -> Type

  -- | @:%@ maps objects.
  type ftag :% a :: Type

  -- | @%@ maps arrows.
  (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)

type FunctorOf a b t = (Functor t, Dom t ~ a, Cod t ~ b)


-- | Functors are arrows in the category Cat.
data Cat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type where
  CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (Dom ftag) (Cod ftag)


-- | @Cat@ is the category with categories as objects and funtors as arrows.
instance Category Cat where

  src :: forall (a :: * -> * -> *) (b :: * -> * -> *). Cat a b -> Obj Cat a
src (CatA ftag
_)      = forall a1.
(Functor a1, Category (Dom a1), Category (Cod a1)) =>
a1 -> Cat (Dom a1) (Cod a1)
CatA forall (k :: * -> * -> *). Id k
Id
  tgt :: forall (a :: * -> * -> *) (b :: * -> * -> *). Cat a b -> Obj Cat b
tgt (CatA ftag
_)      = forall a1.
(Functor a1, Category (Dom a1), Category (Cod a1)) =>
a1 -> Cat (Dom a1) (Cod a1)
CatA forall (k :: * -> * -> *). Id k
Id

  CatA ftag
f1 . :: forall (b :: * -> * -> *) (c :: * -> * -> *) (a :: * -> * -> *).
Cat b c -> Cat a b -> Cat a c
. CatA ftag
f2 = forall a1.
(Functor a1, Category (Dom a1), Category (Cod a1)) =>
a1 -> Cat (Dom a1) (Cod a1)
CatA (ftag
f1 forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: ftag
f2)



data Id (k :: Type -> Type -> Type) = Id

-- | The identity functor on k
instance Category k => Functor (Id k) where
  type Dom (Id k) = k
  type Cod (Id k) = k
  type Id k :% a = a

  Id k
_ % :: forall a b.
Id k -> Dom (Id k) a b -> Cod (Id k) (Id k :% a) (Id k :% b)
% Dom (Id k) a b
f = Dom (Id k) a b
f


data (g :.: h) where
  (:.:) :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h

-- | The composition of two functors.
instance (Category (Cod g), Category (Dom h)) => Functor (g :.: h) where
  type Dom (g :.: h) = Dom h
  type Cod (g :.: h) = Cod g
  type (g :.: h) :% a = g :% (h :% a)

  (g
g :.: h
h) % :: forall a b.
(g :.: h)
-> Dom (g :.: h) a b
-> Cod (g :.: h) ((g :.: h) :% a) ((g :.: h) :% b)
% Dom (g :.: h) a b
f = g
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (h
h forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom (g :.: h) a b
f)



data Const (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) x where
  Const :: Obj c2 x -> Const c1 c2 x

-- | The constant functor.
instance (Category c1, Category c2) => Functor (Const c1 c2 x) where
  type Dom (Const c1 c2 x) = c1
  type Cod (Const c1 c2 x) = c2
  type Const c1 c2 x :% a = x

  Const Obj c2 x
x % :: forall a b.
Const c1 c2 x
-> Dom (Const c1 c2 x) a b
-> Cod (Const c1 c2 x) (Const c1 c2 x :% a) (Const c1 c2 x :% b)
% Dom (Const c1 c2 x) a b
_ = Obj c2 x
x

-- | The constant functor with the same domain and codomain as f.
type ConstF f = Const (Dom f) (Cod f)



data OpOp (k :: Type -> Type -> Type) = OpOp

-- | The @Op (Op x) = x@ functor.
instance Category k => Functor (OpOp k) where
  type Dom (OpOp k) = Op (Op k)
  type Cod (OpOp k) = k
  type OpOp k :% a = a

  OpOp k
OpOp % :: forall a b.
OpOp k
-> Dom (OpOp k) a b -> Cod (OpOp k) (OpOp k :% a) (OpOp k :% b)
% Op (Op k a b
f) = k a b
f


data OpOpInv (k :: Type -> Type -> Type) = OpOpInv

-- | The @x = Op (Op x)@ functor.
instance Category k => Functor (OpOpInv k) where
  type Dom (OpOpInv k) = k
  type Cod (OpOpInv k) = Op (Op k)
  type OpOpInv k :% a = a

  OpOpInv k
OpOpInv % :: forall a b.
OpOpInv k
-> Dom (OpOpInv k) a b
-> Cod (OpOpInv k) (OpOpInv k :% a) (OpOpInv k :% b)
% Dom (OpOpInv k) a b
f = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Dom (OpOpInv k) a b
f)


-- | A functor wrapper in case of conflicting family instance declarations
newtype Any f = Any f deriving forall ftag.
Category (Dom ftag)
-> Category (Cod ftag)
-> (forall a b.
    ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b))
-> Functor ftag
forall {f}. Functor f => Category (Dom (Any f))
forall {f}. Functor f => Category (Cod (Any f))
forall f a b.
Functor f =>
Any f -> Dom (Any f) a b -> Cod (Any f) (Any f :% a) (Any f :% b)
forall a b.
Any f -> Dom (Any f) a b -> Cod (Any f) (Any f :% a) (Any f :% b)
% :: forall a b.
Any f -> Dom (Any f) a b -> Cod (Any f) (Any f :% a) (Any f :% b)
$c% :: forall f a b.
Functor f =>
Any f -> Dom (Any f) a b -> Cod (Any f) (Any f :% a) (Any f :% b)
Functor


data Proj1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Proj1

-- | 'Proj1' is a bifunctor that projects out the first component of a product.
instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where
  type Dom (Proj1 c1 c2) = c1 :**: c2
  type Cod (Proj1 c1 c2) = c1
  type Proj1 c1 c2 :% (a1, a2) = a1

  Proj1 c1 c2
Proj1 % :: forall a b.
Proj1 c1 c2
-> Dom (Proj1 c1 c2) a b
-> Cod (Proj1 c1 c2) (Proj1 c1 c2 :% a) (Proj1 c1 c2 :% b)
% (c1 a1 b1
f1 :**: c2 a2 b2
_) = c1 a1 b1
f1


data Proj2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Proj2

-- | 'Proj2' is a bifunctor that projects out the second component of a product.
instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where
  type Dom (Proj2 c1 c2) = c1 :**: c2
  type Cod (Proj2 c1 c2) = c2
  type Proj2 c1 c2 :% (a1, a2) = a2

  Proj2 c1 c2
Proj2 % :: forall a b.
Proj2 c1 c2
-> Dom (Proj2 c1 c2) a b
-> Cod (Proj2 c1 c2) (Proj2 c1 c2 :% a) (Proj2 c1 c2 :% b)
% (c1 a1 b1
_ :**: c2 a2 b2
f2) = c2 a2 b2
f2


data f1 :***: f2 where (:***:) :: (Functor f1, Functor f2) => f1 -> f2 -> f1 :***: f2

-- | @f1 :***: f2@ is the product of the functors @f1@ and @f2@.
instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where
  type Dom (f1 :***: f2) = Dom f1 :**: Dom f2
  type Cod (f1 :***: f2) = Cod f1 :**: Cod f2
  type (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)

  (f1
g1 :***: f2
g2) % :: forall a b.
(f1 :***: f2)
-> Dom (f1 :***: f2) a b
-> Cod (f1 :***: f2) ((f1 :***: f2) :% a) ((f1 :***: f2) :% b)
% (Dom f1 a1 b1
f1 :**: Dom f2 a2 b2
f2) = (f1
g1 forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f1 a1 b1
f1) forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: (f2
g2 forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f2 a2 b2
f2)


data DiagProd (k :: Type -> Type -> Type) = DiagProd

-- | 'DiagProd' is the diagonal functor for products.
instance Category k => Functor (DiagProd k) where
  type Dom (DiagProd k) = k
  type Cod (DiagProd k) = k :**: k
  type DiagProd k :% a = (a, a)

  DiagProd k
DiagProd % :: forall a b.
DiagProd k
-> Dom (DiagProd k) a b
-> Cod (DiagProd k) (DiagProd k :% a) (DiagProd k :% b)
% Dom (DiagProd k) a b
f = Dom (DiagProd k) a b
f forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Dom (DiagProd k) a b
f


type Tuple1 c1 c2 a = (Const c2 c1 a :***: Id c2) :.: DiagProd c2
-- | 'Tuple1' tuples with a fixed object on the left.
pattern Tuple1 :: (Category c1, Category c2) => Obj c1 a -> Tuple1 c1 c2 a
pattern $bTuple1 :: forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Obj c1 a -> Tuple1 c1 c2 a
$mTuple1 :: forall {r} {c1 :: * -> * -> *} {c2 :: * -> * -> *} {a}.
(Category c1, Category c2) =>
Tuple1 c1 c2 a -> (Obj c1 a -> r) -> ((# #) -> r) -> r
Tuple1 a = (Const a :***: Id) :.: DiagProd

type Swap (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2)
-- | 'swap' swaps the 2 categories of the product of categories.
pattern Swap :: (Category c1, Category c2) => Swap c1 c2
pattern $bSwap :: forall (c1 :: * -> * -> *) (c2 :: * -> * -> *).
(Category c1, Category c2) =>
Swap c1 c2
$mSwap :: forall {r} {c1 :: * -> * -> *} {c2 :: * -> * -> *}.
(Category c1, Category c2) =>
Swap c1 c2 -> ((# #) -> r) -> ((# #) -> r) -> r
Swap = (Proj2 :***: Proj1) :.: DiagProd

type Tuple2 c1 c2 a = Swap c2 c1 :.: Tuple1 c2 c1 a
-- | 'Tuple2' tuples with a fixed object on the right.
pattern Tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a
pattern $bTuple2 :: forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Obj c2 a -> Tuple2 c1 c2 a
$mTuple2 :: forall {r} {c1 :: * -> * -> *} {c2 :: * -> * -> *} {a}.
(Category c1, Category c2) =>
Tuple2 c1 c2 a -> (Obj c2 a -> r) -> ((# #) -> r) -> r
Tuple2 a = Swap :.: Tuple1 a



data Hom (k :: Type -> Type -> Type) = Hom

-- | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument.
instance Category k => Functor (Hom k) where
  type Dom (Hom k) = Op k :**: k
  type Cod (Hom k) = (->)
  type (Hom k) :% (a1, a2) = k a1 a2

  Hom k
Hom % :: forall a b.
Hom k -> Dom (Hom k) a b -> Cod (Hom k) (Hom k :% a) (Hom k :% b)
% (Op k b1 a1
f1 :**: k a2 b2
f2) = \k a1 a2
g -> k a2 b2
f2 forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k a1 a2
g forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k b1 a1
f1


type x :*-: k = Hom k :.: Tuple1 (Op k) k x
-- | The covariant functor Hom(X,--)
pattern HomX_ :: Category k => Obj k x -> x :*-: k
pattern $bHomX_ :: forall (k :: * -> * -> *) x. Category k => Obj k x -> x :*-: k
$mHomX_ :: forall {r} {k :: * -> * -> *} {x}.
Category k =>
(x :*-: k) -> (Obj k x -> r) -> ((# #) -> r) -> r
HomX_ x = Hom :.: Tuple1 (Op x)

type k :-*: x = Hom k :.: Tuple2 (Op k) k x
-- | The contravariant functor Hom(--,X)
pattern Hom_X :: Category k => Obj k x -> k :-*: x
pattern $bHom_X :: forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
$mHom_X :: forall {r} {k :: * -> * -> *} {x}.
Category k =>
(k :-*: x) -> (Obj k x -> r) -> ((# #) -> r) -> r
Hom_X x = Hom :.: Tuple2 x


type ProfunctorOf c d t = (FunctorOf (Op c :**: d) (->) t, Category c, Category d)