{-|
Description: <<===================================== Start here!
-}
module Proarrow.Core
  ( -- * Type Infrastructure
    -- ** Basic Type Definitions
    type (+->), CAT, OB, Kind
    -- ** Universal Constraint
  , Any
    -- * Category Infrastructure
    -- ** CategoryOf Class
  , CategoryOf(..)
    -- ** Category Class
  , Category
    -- * Profunctors
    -- ** Profunctor Class
  , Profunctor(..)
    -- ** Natural Transformations
  , type (:~>)
    -- ** Profunctor Utilities
  , (//), lmap, rmap
    -- ** Default Implementation
  , dimapDefault
    -- * Promonads
    -- ** Promonad Class
  , Promonad(..)
    -- ** Promonad Utilities
  , arr
    -- * Object Identities
  , Obj, obj, src, tgt
    -- * Type Family Utilities
    -- ** Kind Unwrapping
  , UN, Is
  ) where

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

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

-- * Type Infrastructure

-- ** Basic Type Definitions

-- | The kind @j +-> k@ of profunctors from category @j@ to category @k@.
-- Note that this follows mathematical convention,
-- swapping the order compared to Haskell's contravariant-first ordering.
type j +-> k = k -> j -> Type

-- | The kind of categories on kind @k@.
type CAT k = k +-> k

-- | Object constraints for kind @k@.
type OB k = k -> Constraint

-- | Alias for 'Type' for clarity in kind signatures.
type Kind = Type

-- ** Universal Constraint

-- | A constraint that's always satisfied, used as a default when no specific
-- object constraints are needed.
class Any (a :: k)
instance Any a

-- * Category Infrastructure

-- ** CategoryOf Class

-- | Establishes that @k@ is a category by specifying the morphism type and object constraints.
class (Promonad ((~>) :: CAT k)) => CategoryOf k where
  -- | The type of morphisms in the category.
  type (~>) :: CAT k
  -- | What constraints objects must satisfy.
  type Ob (a :: k) :: Constraint
  type Ob a = Any a  -- ^ Default: no constraints

-- ** Category Class

-- | A convenience class that bundles together the requirements for a well-formed category.
-- The automatic instance means you get 'Category' for free once you have 'CategoryOf' and 'Promonad'.
class (Promonad cat, CategoryOf k, cat ~ (~>) @k) => Category (cat :: CAT k)
instance (Promonad cat, CategoryOf k, cat ~ (~>) @k) => Category (cat :: CAT k)

-- * Profunctors

-- ** Profunctor Class

-- | The core profunctor abstraction. A profunctor is contravariant in its first
-- argument and covariant in its second argument.
--
-- __Laws:__
--
-- * @'dimap' 'id' 'id' = 'id'@
-- * @'dimap' (f . g) (h . i) = 'dimap' g h . 'dimap' f i@
type Profunctor :: forall {j} {k}. j +-> k -> Constraint
class (CategoryOf j, CategoryOf k) => Profunctor (p :: j +-> k) where
  -- | Map contravariantly over the first argument and covariantly over the second.
  dimap :: c ~> a -> b ~> d -> p a b -> p c d
  -- | Constraint elimination, extracts object constraints from a profunctor heteromorphism..
  (\\) :: ((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

-- ** Natural Transformations

-- | Natural transformation between profunctors.
type p :~> q = forall a b. p a b -> q a b

-- ** Profunctor Utilities

-- | Flipped version of '(\\)'.
(//) :: (Profunctor p) => p a b -> ((Ob a, Ob b) => r) -> r
p a b
p // :: forall {k} {k} (p :: 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

-- | Left mapping (contravariant mapping over first argument).
lmap :: (Profunctor p) => c ~> a -> p a b -> p c b
lmap :: forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
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 :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
l b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: 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 :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

-- | Right mapping (covariant mapping over second argument).
rmap :: (Profunctor p) => b ~> d -> p a b -> p a d
rmap :: forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
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 :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: 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 :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

-- ** Default Implementation

-- | Default implementation of 'dimap' for promonads using composition.
dimapDefault :: (Promonad p) => p c a -> p b d -> p a b -> p c d
dimapDefault :: forall {k} (p :: 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 :: 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 :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p c a
f

-- * Promonads

-- ** Promonad Class

-- | A promonad is a category-like profunctor with identity morphisms and composition.
--
-- __Laws:__
--
-- * Left identity: @'id' . f = f@
-- * Right identity: @f . 'id' = f@
-- * Associativity: @(h . g) . f = h . (g . f)@
class (Profunctor p) => Promonad p where
  -- | Identity morphisms.
  id :: (Ob a) => p a a
  -- | Composition (note the parameter order matches function composition).
  (.) :: p b c -> p a b -> p a c

-- ** Promonad Utilities

-- | Lifts morphisms from the base category into the promonad.
arr :: (Promonad p) => a ~> b -> p a b
arr :: forall {k} (p :: 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 :: j +-> k) (b :: j) (d :: j) (a :: k).
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 :: 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

-- * Object Identities

-- | Type of identity morphism for object @a@.
type Obj a = a ~> a

-- | The identity morphism for a given object.
-- Compared to @id@ this makes the kind argument implicit,
-- allowing to write @obj \@a@ instead of @id \@k \@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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id @_ @a

-- | Extract source identity morphism from a profunctor heteromorphism.
src :: forall {k} a b p. (Profunctor p) => p (a :: k) b -> Obj a
src :: forall {j} {k} (a :: k) (b :: j) (p :: j +-> 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 :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

-- | Extract target identity morphism from a profunctor heteromorphism.
tgt :: forall {k} a b p. (Profunctor p) => p (a :: k) b -> Obj b
tgt :: forall {k} {k} (a :: k) (b :: k) (p :: 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

-- * Standard Instances

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 :: 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)

-- | The category of Haskell types (a.k.a @Hask@), where the arrows are functions.
instance CategoryOf Type where
  type (~>) = (->)

-- * Type Family Utilities

-- ** Kind Unwrapping

-- | 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)