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

import Data.Kind (Type)

import Data.Category (Category(..), Obj)
import Data.Category.Functor (Functor(..))
import Data.Category.Limit (HasBinaryProducts(..), HasTerminalObject(..))
import Data.Category.CartesianClosed
import Data.Category.Enriched

-- | Enriched functors.
class (ECategory (EDom ftag), ECategory (ECod ftag), V (EDom ftag) ~ V (ECod ftag)) => EFunctor ftag where

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

  -- | @:%%@ maps objects at the type level
  type ftag :%% a :: Type

  -- | @%%@ maps object at the value level
  (%%) :: ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)

  -- | `map` maps arrows.
  map :: (EDom ftag ~ k) => ftag -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))

type EFunctorOf a b t = (EFunctor t, EDom t ~ a, ECod t ~ b)


data Id (k :: Type -> Type -> Type) = Id
-- | The identity functor on k
instance ECategory k => EFunctor (Id k) where
  type EDom (Id k) = k
  type ECod (Id k) = k
  type Id k :%% a = a
  Id %% a = a
  map Id = hom

data (g :.: h) where
  (:.:) :: (EFunctor g, EFunctor h, ECod h ~ EDom g) => g -> h -> g :.: h
-- | The composition of two functors.
instance (ECategory (ECod g), ECategory (EDom h), V (EDom h) ~ V (ECod g), ECod h ~ EDom g) => EFunctor (g :.: h) where
  type EDom (g :.: h) = EDom h
  type ECod (g :.: h) = ECod g
  type (g :.: h) :%% a = g :%% (h :%% a)
  (g :.: h) %% a = g %% (h %% a)
  map (g :.: h) a b = map g (h %% a) (h %% b) . map h a b

data Const (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) x where
  Const :: Obj c2 x -> Const c1 c2 x
-- | The constant functor.
instance (ECategory c1, ECategory c2, V c1 ~ V c2) => EFunctor (Const c1 c2 x) where
  type EDom (Const c1 c2 x) = c1
  type ECod (Const c1 c2 x) = c2
  type Const c1 c2 x :%% a = x
  Const x %% _ = x
  map (Const x) a b = id x . terminate (hom a b)

data Opposite f where
  Opposite :: EFunctor f => f -> Opposite f
-- | The dual of a functor
instance (EFunctor f) => EFunctor (Opposite f) where
  type EDom (Opposite f) = EOp (EDom f)
  type ECod (Opposite f) = EOp (ECod f)
  type Opposite f :%% a = f :%% a
  Opposite f %% EOp a = EOp (f %% a)
  map (Opposite f) (EOp a) (EOp b) = map f b a

data f1 :<*>: f2 = f1 :<*>: f2
-- | @f1 :<*>: f2@ is the product of the functors @f1@ and @f2@.
instance (EFunctor f1, EFunctor f2, V (ECod f1) ~ V (ECod f2)) => EFunctor (f1 :<*>: f2) where
  type EDom (f1 :<*>: f2) = EDom f1 :<>: EDom f2
  type ECod (f1 :<*>: f2) = ECod f1 :<>: ECod f2
  type (f1 :<*>: f2) :%% (a1, a2) = (f1 :%% a1, f2 :%% a2)
  (f1 :<*>: f2) %% (a1 :<>: a2) = (f1 %% a1) :<>: (f2 %% a2)
  map (f1 :<*>: f2) (a1 :<>: a2) (b1 :<>: b2) = map f1 a1 b1 *** map f2 a2 b2

data DiagProd (k :: Type -> Type -> Type) = DiagProd
-- | 'DiagProd' is the diagonal functor for products.
instance ECategory k => EFunctor (DiagProd k) where
  type EDom (DiagProd k) = k
  type ECod (DiagProd k) = k :<>: k
  type DiagProd k :%% a = (a, a)
  DiagProd %% a = a :<>: a
  map DiagProd a b = hom a b &&& hom a b

newtype UnderlyingF f = UnderlyingF f
-- | The underlying functor of an enriched functor @f@
instance EFunctor f => Functor (UnderlyingF f) where
  type Dom (UnderlyingF f) = Underlying (EDom f)
  type Cod (UnderlyingF f) = Underlying (ECod f)
  type UnderlyingF f :% a = f :%% a
  UnderlyingF f % Underlying a ab b = Underlying (f %% a) (map f a b . ab) (f %% b)

newtype InHaskF f = InHaskF f
-- | A regular functor is a functor enriched in Hask.
instance Functor f => EFunctor (InHaskF f) where
  type EDom (InHaskF f) = InHask (Dom f)
  type ECod (InHaskF f) = InHask (Cod f)
  type InHaskF f :%% a = f :% a
  InHaskF f %% InHask a = InHask (f % a)
  map (InHaskF f) _ _ = \g -> f % g

newtype InHaskToHask f = InHaskToHask f
instance (Functor f, Cod f ~ (->)) => EFunctor (InHaskToHask f) where
  type EDom (InHaskToHask f) = InHask (Dom f)
  type ECod (InHaskToHask f) = Self (->)
  type InHaskToHask f :%% a = f :% a
  InHaskToHask f %% InHask a = Self (f % a)
  map (InHaskToHask f) _ _ = \g -> f % g

newtype UnderlyingHask (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) f = UnderlyingHask f
-- | The underlying functor of an enriched functor @f@ enriched in Hask.
instance (EFunctor f, EDom f ~ InHask c, ECod f ~ InHask d, Category c, Category d) => Functor (UnderlyingHask c d f) where
  type Dom (UnderlyingHask c d f) = c
  type Cod (UnderlyingHask c d f) = d
  type UnderlyingHask c d f :% a = f :%% a
  UnderlyingHask f % g = map f (InHask (src g)) (InHask (tgt g)) g

data EHom (k :: Type -> Type -> Type) = EHom
instance ECategory k => EFunctor (EHom k) where
  type EDom (EHom k) = EOp k :<>: k
  type ECod (EHom k) = Self (V k)
  type EHom k :%% (a, b) = k $ (a, b)
  EHom %% (EOp a :<>: b) = Self (hom a b)
  map EHom (EOp a1 :<>: a2) (EOp b1 :<>: b2) = curry (ba *** ab) a b (comp b1 a1 b2 . (comp a1 a2 b2 . (proj2 ba ab *** a) &&& proj1 ba ab . proj1 (ba *** ab) a))
    where
      a = hom a1 a2
      b = hom b1 b2
      ba = hom b1 a1
      ab = hom a2 b2

-- | The enriched functor @k(x, -)@
data EHomX_ k x = EHomX_ (Obj k x)
instance ECategory k => EFunctor (EHomX_ k x) where
  type EDom (EHomX_ k x) = k
  type ECod (EHomX_ k x) = Self (V k)
  type EHomX_ k x :%% y = k $ (x, y)
  EHomX_ x %% y = Self (hom x y)
  map (EHomX_ x) a b = curry (hom a b) (hom x a) (hom x b) (comp x a b)

-- | The enriched functor @k(-, x)@
data EHom_X k x = EHom_X (Obj (EOp k) x)
instance ECategory k => EFunctor (EHom_X k x) where
  type EDom (EHom_X k x) = EOp k
  type ECod (EHom_X k x) = Self (V k)
  type EHom_X k x :%% y = k $ (y, x)
  EHom_X x %% y = Self (hom x y)
  map (EHom_X x) a b = curry (hom a b) (hom x a) (hom x b) (comp x a b)


-- | A V-enrichment on a functor @F: V -> V@ is the same thing as tensorial strength @(a, f b) -> f (a, b)@.
strength :: EFunctorOf (Self v) (Self v) f => f -> Obj v a -> Obj v b -> v (BinaryProduct v a (f :%% b)) (f :%% (BinaryProduct v a b))
strength f a b = uncurry a fb fab (map f (Self b) (Self (a *** b)) . tuple b a)
  where
    Self fb = f %% Self b
    Self fab = f %% Self (a *** b)


-- | Enriched natural transformations.
data ENat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where
  ENat :: (EFunctorOf c d f, EFunctorOf c d g)
    => f -> g -> (forall z. Obj c z -> Arr d (f :%% z) (g :%% z)) -> ENat c d f g