module Proarrow.Functor where

import Data.Functor.Compose (Compose (..))
import Data.Functor.Const (Const (..))
import Data.Functor.Identity (Identity)
import Data.Kind (Constraint, Type)
import Data.List.NonEmpty qualified as P
import Prelude qualified as P

import Proarrow.Core (CategoryOf (..), Promonad (..), Profunctor, rmap)
import Proarrow.Object (Ob')

infixr 0 .~>
type f .~> g = forall a. (Ob a) => f a ~> g a

type Functor :: forall {k1} {k2}. (k1 -> k2) -> Constraint
class (CategoryOf k1, CategoryOf k2, forall a. (Ob a) => Ob' (f a)) => Functor (f :: k1 -> k2) where
  map :: a ~> b -> f a ~> f b

-- Can't make an instance Functor (f :: Type -> Type) because that would overlap with instances of kind k -> Type
newtype Prelude f a = Prelude {forall {k} (f :: k -> Type) (a :: k). Prelude f a -> f a
unPrelude :: f a}
instance (P.Functor f) => Functor (Prelude f) where
  map :: forall a b. (a ~> b) -> Prelude f a ~> Prelude f b
map a ~> b
f = f b -> Prelude f b
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude (f b -> Prelude f b)
-> (Prelude f a -> f b) -> Prelude f a -> Prelude f 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) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap a ~> b
a -> b
f (f a -> f b) -> (Prelude f a -> f a) -> Prelude f a -> f 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
. Prelude f a -> f a
forall {k} (f :: k -> Type) (a :: k). Prelude f a -> f a
unPrelude

deriving via Prelude ((,) a) instance Functor ((,) a)
deriving via Prelude (P.Either a) instance Functor (P.Either a)
deriving via Prelude P.Maybe instance Functor P.Maybe
deriving via Prelude P.NonEmpty instance Functor P.NonEmpty
deriving via Prelude ((->) a) instance Functor ((->) a)
deriving via Prelude [] instance Functor []
deriving via Prelude Identity instance Functor Identity

instance (CategoryOf k) => Functor (Const x :: k -> Type) where
  map :: forall (a :: k) (b :: k). (a ~> b) -> Const x a ~> Const x b
map a ~> b
_ (Const x
x) = x -> Const x b
forall {k} a (b :: k). a -> Const a b
Const x
x

instance (Functor f, Functor g) => Functor (Compose f g) where
  map :: forall (a :: k1) (b :: k1).
(a ~> b) -> Compose f g a ~> Compose f g b
map a ~> b
f = f (g b) -> Compose f g b
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g b) -> Compose f g b)
-> (Compose f g a -> f (g b)) -> Compose f g a -> Compose f g 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
. (g a ~> g b) -> f (g a) ~> f (g b)
forall (a :: k) (b :: k). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map ((a ~> b) -> g a ~> g b
forall (a :: k1) (b :: k1). (a ~> b) -> g a ~> g b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> b
f) (f (g a) -> f (g b))
-> (Compose f g a -> f (g a)) -> Compose f g a -> f (g 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
. Compose f g a -> f (g a)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose

newtype FromProfunctor p a b = FromProfunctor {forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
FromProfunctor p a b -> p a b
unFromProfunctor :: p a b}
instance (Profunctor p) => Functor (FromProfunctor p a) where
  map :: forall (a :: k1) (b :: k1).
(a ~> b) -> FromProfunctor p a a ~> FromProfunctor p a b
map a ~> b
f = p a b -> FromProfunctor p a b
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
p a b -> FromProfunctor p a b
FromProfunctor (p a b -> FromProfunctor p a b)
-> (FromProfunctor p a a -> p a b)
-> FromProfunctor p a a
-> FromProfunctor p 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) -> p a a -> p a b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap a ~> b
f (p a a -> p a b)
-> (FromProfunctor p a a -> p a a) -> FromProfunctor p a a -> p 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
. FromProfunctor p a a -> p a a
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
FromProfunctor p a b -> p a b
unFromProfunctor