module Proarrow.Profunctor.Forget where

import Prelude (Monoid(..), map, foldMap)
import Data.Kind (Type)

import Proarrow.Category.Instance.Sub (SUBCAT(..), Sub (..))
import Proarrow.Core (OB, PRO, Profunctor(..), CategoryOf(..), Promonad(..))
import Proarrow.Adjunction (Adjunction(..))
import Proarrow.Profunctor.Composition ((:.:)(..))
import Proarrow.Profunctor.Representable (Representable(..), dimapRep)


type Forget :: forall (ob :: OB k) -> PRO k (SUBCAT ob)
data Forget ob a b where
  Forget :: ob b => a ~> b -> Forget ob a (SUB b)

instance CategoryOf k => Profunctor (Forget (ob :: OB k)) where
  dimap :: forall (c :: k) (a :: k) (b :: SUBCAT ob) (d :: SUBCAT ob).
(c ~> a) -> (b ~> d) -> Forget ob a b -> Forget ob c d
dimap c ~> a
l (Sub a1 ~> b1
r) (Forget a ~> b
f) = (c ~> b1) -> Forget ob c (SUB b1)
forall {k} (ob :: k -> Constraint) (a :: k) (a :: k).
ob a =>
(a ~> a) -> Forget ob a (SUB a)
Forget (a1 ~> b1
r (a1 ~> b1) -> (c ~> a1) -> c ~> b1
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a1
a ~> b
f (a ~> a1) -> (c ~> a) -> c ~> a1
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
l)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: SUBCAT ob) r.
((Ob a, Ob b) => r) -> Forget ob a b -> r
\\ Forget a ~> b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

instance CategoryOf k => Representable (Forget (ob :: OB k)) where
  type Forget ob % (SUB a) = a
  index :: forall (a :: k) (b :: SUBCAT ob).
Forget ob a b -> a ~> (Forget ob % b)
index (Forget a ~> b
f) = a ~> b
a ~> (Forget ob % b)
f
  tabulate :: forall (b :: SUBCAT ob) (a :: k).
Ob b =>
(a ~> (Forget ob % b)) -> Forget ob a b
tabulate = (a ~> UN SUB b) -> Forget ob a (SUB (UN SUB b))
(a ~> (Forget ob % b)) -> Forget ob a b
forall {k} (ob :: k -> Constraint) (a :: k) (a :: k).
ob a =>
(a ~> a) -> Forget ob a (SUB a)
Forget
  repMap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
(a ~> b) -> (Forget ob % a) ~> (Forget ob % b)
repMap (Sub a1 ~> b1
f) = a1 ~> b1
(Forget ob % a) ~> (Forget ob % b)
f

type List :: PRO (SUBCAT Monoid) Type
data List a b where
  List :: Monoid a => (a -> [b]) -> List (SUB a) b
instance Profunctor List where
  dimap :: forall (c :: SUBCAT Monoid) (a :: SUBCAT Monoid) b d.
(c ~> a) -> (b ~> d) -> List a b -> List c d
dimap = (c ~> a) -> (b ~> d) -> List a b -> List c d
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (c :: j) (d :: k).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: SUBCAT Monoid) b r.
((Ob a, Ob b) => r) -> List a b -> r
\\ List{} = r
(Ob a, Ob b) => r
r

instance Representable List where
  type List % a = SUB [a]
  index :: forall (a :: SUBCAT Monoid) b. List a b -> a ~> (List % b)
index (List a -> [b]
f) = (a ~> [b]) -> Sub (SUB a) (SUB [b])
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k).
(ob a1, ob b1) =>
(a1 ~> b1) -> Sub (SUB a1) (SUB b1)
Sub a ~> [b]
a -> [b]
f
  tabulate :: forall b (a :: SUBCAT Monoid).
Ob b =>
(a ~> (List % b)) -> List a b
tabulate (Sub a1 ~> b1
f) = (a1 -> [b]) -> List (SUB a1) b
forall a b. Monoid a => (a -> [b]) -> List (SUB a) b
List a1 ~> b1
a1 -> [b]
f
  repMap :: forall a b. (a ~> b) -> (List % a) ~> (List % b)
repMap a ~> b
f = ([a] ~> [b]) -> Sub (SUB [a]) (SUB [b])
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k).
(ob a1, ob b1) =>
(a1 ~> b1) -> Sub (SUB a1) (SUB b1)
Sub ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a ~> b
a -> b
f)

instance Adjunction List (Forget Monoid) where
  unit :: forall a. Ob a => (:.:) (Forget Monoid) List a a
unit = (a ~> [a]) -> Forget Monoid a (SUB [a])
forall {k} (ob :: k -> Constraint) (a :: k) (a :: k).
ob a =>
(a ~> a) -> Forget ob a (SUB a)
Forget (a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[]) Forget Monoid a (SUB [a])
-> List (SUB [a]) a -> (:.:) (Forget Monoid) List a a
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: ([a] -> [a]) -> List (SUB [a]) a
forall a b. Monoid a => (a -> [b]) -> List (SUB a) b
List [a] -> [a]
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  counit :: (List :.: Forget Monoid) :~> (~>)
counit (List a -> [b]
g :.: Forget b ~> b
f) = (a ~> b) -> Sub (SUB a) (SUB b)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k).
(ob a1, ob b1) =>
(a1 ~> b1) -> Sub (SUB a1) (SUB b1)
Sub ((b -> b) -> [b] -> b
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap b ~> b
b -> b
f ([b] -> b) -> (a -> [b]) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a -> [b]
g)