module Proarrow.Functor where

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

import Proarrow.Core (CategoryOf(..), Promonad(..))
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


newtype Prelude f a = Prelude { forall {k} (f :: k -> Type) (a :: k). Prelude f a -> f a
getPrelude :: 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
getPrelude

deriving via Prelude ((,) a) instance Functor ((,) a)
deriving via Prelude (P.Either a) instance Functor (P.Either a)
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