{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Redundant lambda" #-}
{-# HLINT ignore "Avoid lambda" #-}
module Proarrow.Core where

import Data.Kind (Constraint, Type)
import Prelude (type (~))

infixr 0 ~>, :~>, +->
infixl 1 \\
infixr 0 //
infixr 9 .

type PRO j k = j -> k -> Type
type j +-> k = PRO k j

type CAT k = PRO k k
type BI k = (k, k) -> k
type OB k = k -> Constraint
type Kind = Type

class Any (a :: k)
instance Any a

class (Promonad ((~>) :: CAT k)) => CategoryOf k where
  type (~>) :: CAT k
  type Ob (a :: k) :: Constraint
  type Ob a = Any a

class (Promonad cat, CategoryOf k, cat ~ (~>) @k) => Category (cat :: CAT k)
instance (Promonad cat, CategoryOf k, cat ~ (~>) @k) => Category (cat :: CAT k)

type p :~> q = forall a b. p a b -> q a b

type Profunctor :: forall {j} {k}. PRO j k -> Constraint
class (CategoryOf j, CategoryOf k) => Profunctor (p :: PRO j k) where
  dimap :: c ~> a -> b ~> d -> p a b -> p c d
  (\\) :: ((Ob a, Ob b) => r) -> p a b -> r
  default (\\) :: (Ob a, Ob b) => ((Ob a, Ob b) => r) -> p a b -> r
  (Ob a, Ob b) => r
r \\ p a b
_ = r
(Ob a, Ob b) => r
r

(//) :: (Profunctor p) => p a b -> ((Ob a, Ob b) => r) -> r
p a b
p // :: forall {k} {k} (p :: PRO k k) (a :: k) (b :: k) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (Ob a, Ob b) => r
r = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p

lmap :: (Profunctor p) => c ~> a -> p a b -> p c b
lmap :: forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap c ~> a
l p a b
p = (c ~> a) -> (b ~> b) -> p a b -> p c b
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
l b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id p a b
p ((Ob a, Ob b) => p c b) -> p a b -> p c b
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p

rmap :: (Profunctor p) => b ~> d -> p a b -> p a d
rmap :: forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> d
r p a b
p = (a ~> a) -> (b ~> d) -> p a b -> p a d
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> d
r p a b
p ((Ob a, Ob b) => p a d) -> p a b -> p a d
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p

dimapDefault :: (Promonad p) => p c a -> p b d -> p a b -> p c d
dimapDefault :: forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault p c a
f p b d
g p a b
h = p b d
g p b d -> p c b -> p c d
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p 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
. p a b
h p a b -> p c a -> p c b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p 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
. p c a
f

class (Profunctor p) => Promonad p where
  id :: (Ob a) => p a a
  (.) :: p b c -> p a b -> p a c

arr :: (Promonad p) => a ~> b -> p a b
arr :: forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> p a b
arr a ~> b
f = (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
forall (a :: k). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob a, Ob b) => p a b) -> (a ~> b) -> p a b
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

type Obj a = a ~> a

obj :: forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj :: forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj = forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id @_ @a

src :: forall {k} a b p. (Profunctor p) => p (a :: k) b -> Obj a
src :: forall {k} {k} (a :: k) (b :: k) (p :: PRO k k).
Profunctor p =>
p a b -> Obj a
src p a b
p = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a ((Ob a, Ob b) => a ~> a) -> p a b -> a ~> a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p

tgt :: forall {k} a b p. (Profunctor p) => p (a :: k) b -> Obj b
tgt :: forall {k} {k} (a :: k) (b :: k) (p :: PRO k k).
Profunctor p =>
p a b -> Obj b
tgt p a b
p = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b ((Ob a, Ob b) => b ~> b) -> p a b -> b ~> b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p

instance Profunctor (->) where
  dimap :: forall c a b d. (c ~> a) -> (b ~> d) -> (a -> b) -> c -> d
dimap = (c ~> a) -> (b ~> d) -> (a -> b) -> c -> d
(c -> a) -> (b -> d) -> (a -> b) -> c -> d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault

instance Promonad (->) where
  id :: forall a. Ob a => a -> a
id = \a
a -> a
a
  b -> c
f . :: forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
g = \a
x -> b -> c
f (a -> b
g a
x)

instance CategoryOf Type where
  type (~>) = (->)

-- | A helper type family to unwrap a wrapped kind.
-- This is needed because the field selector functions of newtypes have to be
-- lower case and therefore cannot be used at the type level.
type family UN (w :: j -> k) (wa :: k) :: j

-- | @Is w a@ checks that the kind @a@ is a kind wrapped by @w@.
type Is w a = a ~ w (UN w a)