{-# LANGUAGE AllowAmbiguousTypes #-}

-- the identity laws compose with id on purpose
{- HLINT ignore "Redundant id" -}

-- | Laws stated as code, polymorphic in the category. A law of the structures @cs@ takes five
-- object variables and a supply of named arbitrary arrows, and returns an equation between two
-- arrows. The @proarrow:testing@ library checks laws by running them with random objects and
-- arrows, in a category whose arrows also carry their own description, so that a failing law
-- prints as the code it was built from.
--
-- A derived operation (a function defined from the class methods, like
-- 'Proarrow.Category.Monoidal.StarAutonomous.doubleNeg') would print as its definition. 'label'
-- names it instead.
--
-- A class's laws are an instance of 'Laws' for the list of structures they mention, the same list
-- the class's free-category structure requires, e.g.
-- @'Laws' 'Proarrow.Category.Monoidal.SymMonoidalStructures'@. The instances live next to their
-- classes.
module Proarrow.Tools.Laws where

import Data.Kind (Constraint, Type)
import Prelude (Applicative, Monad, String, pure, (++))

import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Instance.Free (All)
import Proarrow.Core (CategoryOf (..), Hom, Kind, Profunctor (..), Promonad (..), type (+->))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), withObCorep)
import Proarrow.Profunctor.Representable (Representable (..), withObRep)

-- * Laws

-- | The laws of the structures @cs@. A class with a new kind of object also needs support in the
-- testing library before its laws can be checked, see "Proarrow.Testing.Laws.Run".
--
-- For example, the laws of a functor on objects @Sq@ with action @sq@ on arrows:
--
-- @
-- instance Laws '[HasSquare] where
--   laws =
--     [ Law "sq identity" \\ \@a _ -> withObSq \@_ \@a (sq (obj \@a) '===' id)
--     , Law "sq composition" \\ \@a \@b \@c mor -> do
--         f <- mor \@a \@b "f"
--         g <- mor \@b \@c "g"
--         sq (g . f) '===' sq g . sq f
--     ]
-- @
type Laws :: [Kind -> Constraint] -> Constraint
class Laws cs where
  -- | The laws, each tested as its own property.
  laws :: [Law cs]

-- | A named law.
type Law :: [Kind -> Constraint] -> Type
data Law cs = Law String (LawBody cs)

-- | The name of a law, used as its test's name.
lawName :: Law cs -> String
lawName :: forall (cs :: [Kind -> Constraint]). Law cs -> String
lawName (Law String
name LawBody cs
_) = String
name

-- | The body of a 'Law': given five object variables and a supply of named arbitrary arrows,
-- produce an 'Equation'. A body binds as many of the variables as it uses, e.g. @\\ \@a \@b mor -> ...@,
-- and gives each arrow it asks for the name to print it as.
type LawBody :: [Kind -> Constraint] -> Type
type LawBody cs =
  forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) m
   . (Labelled k, All cs k, Monad m, Ob a, Ob b, Ob c, Ob d, Ob e)
  => (forall (x :: k) y. (Ob x, Ob y) => String -> m (x ~> y))
  -> m (Equation k)

-- * Equations

infix 1 :=:

-- | Two parallel elements of a profunctor claimed to be equal, or an equation between arrows of its
-- codomain ('InK') or domain ('InJ').
type ProEquation :: forall {j} {k}. (j +-> k) -> Type
data ProEquation p where
  (:=:) :: forall {j} {k} (p :: j +-> k) a b. p a b -> p a b -> ProEquation p
  InK :: forall {j} {k} (p :: j +-> k). Equation k -> ProEquation p
  InJ :: forall {j} {k} (p :: j +-> k). Equation j -> ProEquation p

-- | Two parallel arrows claimed to be equal: an equation between elements of the hom profunctor.
type Equation :: Kind -> Type
type Equation k = ProEquation (Hom k)

-- | The two sides of an equation between arrows. At the hom profunctor 'InK' and 'InJ' only wrap
-- another equation between arrows of the same category, and are looked through.
withSides :: forall {k} r. Equation k -> (forall (a :: k) b. a ~> b -> a ~> b -> r) -> r
withSides :: forall {k :: Kind} (r :: Kind).
Equation k
-> (forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r) -> r
withSides (Hom k a b
l :=: Hom k a b
r) forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r
f = Hom k a b -> Hom k a b -> r
forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r
f Hom k a b
l Hom k a b
r
withSides (InK ProEquation (Hom k)
e) forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r
f = ProEquation (Hom k)
-> (forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r) -> r
forall {k :: Kind} (r :: Kind).
Equation k
-> (forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r) -> r
withSides ProEquation (Hom k)
e (a ~> b) -> (a ~> b) -> r
forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r
f
withSides (InJ ProEquation (Hom k)
e) forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r
f = ProEquation (Hom k)
-> (forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r) -> r
forall {k :: Kind} (r :: Kind).
Equation k
-> (forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r) -> r
withSides ProEquation (Hom k)
e (a ~> b) -> (a ~> b) -> r
forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r
f

-- | The equations that an equation between arrows of @i@ can be the result of: those of a
-- profunctor law whose codomain ('InK') or domain ('InJ') is @i@. An 'Equation' is one of these,
-- at the hom profunctor. When the codomain and the domain are the same category either
-- constructor says the same, and 'InK' is used.
type ArrowEquation :: Kind -> Type -> Constraint
class ArrowEquation i r where
  -- | An equation between arrows of @i@, as an @r@.
  fromArrowEquation :: Equation i -> r

instance ArrowEquation k (ProEquation (p :: j +-> k)) where
  fromArrowEquation :: Equation k -> ProEquation p
fromArrowEquation = Equation k -> ProEquation p
forall {j :: Kind} {k :: Kind} (p :: j +-> k).
Equation k -> ProEquation p
InK
instance {-# INCOHERENT #-} ArrowEquation j (ProEquation (p :: j +-> k)) where
  fromArrowEquation :: Equation j -> ProEquation p
fromArrowEquation = Equation j -> ProEquation p
forall (j :: Kind) (k :: Kind) (p :: j +-> k).
Equation j -> ProEquation p
InJ

infix 1 ===

-- | An equation between arrows as the result of a law body, in whichever category of the law the
-- arrows are in: @l '===' r = 'pure' ('fromArrowEquation' (l ':=:' r))@.
(===) :: forall {i} m r (a :: i) b. (Applicative m, ArrowEquation i r) => a ~> b -> a ~> b -> m r
a ~> b
l === :: forall {i :: Kind} (m :: Kind -> Kind) (r :: Kind) (a :: i)
       (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== a ~> b
r = r -> m r
forall (a :: Kind). a -> m a
forall (f :: Kind -> Kind) (a :: Kind). Applicative f => a -> f a
pure (Equation i -> r
forall (i :: Kind) (r :: Kind).
ArrowEquation i r =>
Equation i -> r
fromArrowEquation (a ~> b
l (a ~> b) -> (a ~> b) -> Equation i
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j).
p a b -> p a b -> ProEquation p
:=: a ~> b
r :: Equation i))

infix 1 =:=

-- | An equation between elements as the result of a profunctor law body:
-- @l '=:=' r = 'pure' (l ':=:' r)@.
(=:=) :: forall {j} {k} m (p :: j +-> k) a b. (Applicative m) => p a b -> p a b -> m (ProEquation p)
p a b
l =:= :: forall {j :: Kind} {k :: Kind} (m :: Kind -> Kind) (p :: j +-> k)
       (a :: k) (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= p a b
r = ProEquation p -> m (ProEquation p)
forall (a :: Kind). a -> m a
forall (f :: Kind -> Kind) (a :: Kind). Applicative f => a -> f a
pure (p a b
l p a b -> p a b -> ProEquation p
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j).
p a b -> p a b -> ProEquation p
:=: p a b
r)

-- * Inverses

-- | A pair of arrows claimed to be inverse to each other, see 'inverses'.
type Inverses :: Kind -> Type
data Inverses k where
  Inverses :: forall {k} (a :: k) b. a ~> b -> b ~> a -> Inverses k

-- | The body of a law that asks for no arrows: given five object variables, an @r k@.
type PureLawBody :: [Kind -> Constraint] -> (Kind -> Type) -> Type
type PureLawBody cs r =
  forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). (Labelled k, All cs k, Ob a, Ob b, Ob c, Ob d, Ob e) => r k

-- | @g . f = id@ and @f . g = id@ for @'Inverses' f g@.
leftInverse, rightInverse :: (CategoryOf k) => Inverses k -> Equation k
leftInverse :: forall (k :: Kind). CategoryOf k => Inverses k -> Equation k
leftInverse (Inverses a ~> b
f b ~> a
g) = (b ~> a
g (b ~> a) -> (a ~> b) -> a ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f (a ~> a) -> (a ~> a) -> ProEquation (~>)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j).
p a b -> p a b -> ProEquation p
:=: a ~> a
forall (a :: k). Ob a => a ~> a
forall {k :: Kind} (p :: CAT k) (a :: k).
(Promonad p, Ob a) =>
p a a
id) ((Ob a, Ob b) => ProEquation (~>)) -> (a ~> b) -> ProEquation (~>)
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f
rightInverse :: forall (k :: Kind). CategoryOf k => Inverses k -> Equation k
rightInverse (Inverses a ~> b
f b ~> a
g) = (a ~> b
f (a ~> b) -> (b ~> a) -> b ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> a
g (b ~> b) -> (b ~> b) -> ProEquation (~>)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j).
p a b -> p a b -> ProEquation p
:=: b ~> b
forall (a :: k). Ob a => a ~> a
forall {k :: Kind} (p :: CAT k) (a :: k).
(Promonad p, Ob a) =>
p a a
id) ((Ob a, Ob b) => ProEquation (~>)) -> (a ~> b) -> ProEquation (~>)
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

-- | The two laws saying that a pair of arrows @f@, @g@ are inverse to each other: @g@ is a left
-- and a right inverse of @f@.
inverses :: forall cs. String -> PureLawBody cs Inverses -> [Law cs]
inverses :: forall (cs :: [Kind -> Constraint]).
String -> PureLawBody cs Inverses -> [Law cs]
inverses String
name PureLawBody cs Inverses
body = [String
-> (forall (k :: Kind). CategoryOf k => Inverses k -> Equation k)
-> Law cs
side String
" left inverse" Inverses k -> Equation k
forall (k :: Kind). CategoryOf k => Inverses k -> Equation k
leftInverse, String
-> (forall (k :: Kind). CategoryOf k => Inverses k -> Equation k)
-> Law cs
side String
" right inverse" Inverses k -> Equation k
forall (k :: Kind). CategoryOf k => Inverses k -> Equation k
rightInverse]
  where
    side :: String -> (forall k. (CategoryOf k) => Inverses k -> Equation k) -> Law cs
    side :: String
-> (forall (k :: Kind). CategoryOf k => Inverses k -> Equation k)
-> Law cs
side String
suffix forall (k :: Kind). CategoryOf k => Inverses k -> Equation k
eqn = String -> LawBody cs -> Law cs
forall (cs :: [Kind -> Constraint]). String -> LawBody cs -> Law cs
Law (String
name String -> String -> String
forall (a :: Kind). [a] -> [a] -> [a]
++ String
suffix) \ @a @b @c @d @e forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> Equation k -> m (Equation k)
forall (a :: Kind). a -> m a
forall (f :: Kind -> Kind) (a :: Kind). Applicative f => a -> f a
pure (Inverses k -> Equation k
forall (k :: Kind). CategoryOf k => Inverses k -> Equation k
eqn (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
(Labelled k, All cs k, Ob a, Ob b, Ob c, Ob d, Ob e) =>
Inverses k
PureLawBody cs Inverses
body @a @b @c @d @e))

-- * Bijections

-- | Two maps between hom-sets claimed to be inverse to each other, see 'bijection', with how to
-- ask for an arrow of either hom-set.
type Bijection :: (Type -> Type) -> Kind -> Type
data Bijection m k where
  Bijection
    :: forall {k} m (a :: k) (b :: k) (c :: k) (d :: k)
     . m (a ~> b) -> m (c ~> d) -> (a ~> b -> c ~> d) -> (c ~> d -> a ~> b) -> Bijection m k

-- | The body of a 'bijection': given five object variables and a supply of named arbitrary arrows,
-- the two maps, with how to ask for an arrow of each hom-set.
type BijectionBody :: [Kind -> Constraint] -> Type
type BijectionBody cs =
  forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) m
   . (Labelled k, All cs k, Monad m, Ob a, Ob b, Ob c, Ob d, Ob e)
  => (forall (x :: k) y. (Ob x, Ob y) => String -> m (x ~> y))
  -> Bijection m k

-- | The two laws saying that maps @to@ and @from@ between hom-sets are inverse to each other:
-- @from (to f) = f@ and @to (from g) = g@. Each asks only for the arrow it needs, so an empty
-- hom-set on the other side discards nothing.
bijection :: forall cs. String -> BijectionBody cs -> [Law cs]
bijection :: forall (cs :: [Kind -> Constraint]).
String -> BijectionBody cs -> [Law cs]
bijection String
name BijectionBody cs
body =
  [ String -> LawBody cs -> Law cs
forall (cs :: [Kind -> Constraint]). String -> LawBody cs -> Law cs
Law (String
name String -> String -> String
forall (a :: Kind). [a] -> [a] -> [a]
++ String
" left inverse") \ @a @b @c @d @e forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> case forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k)
       (m :: Kind -> Kind).
(Labelled k, All cs k, Monad m, Ob a, Ob b, Ob c, Ob d, Ob e) =>
(forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y))
-> Bijection m k
BijectionBody cs
body @a @b @c @d @e String -> m (x ~> y)
forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor of
      Bijection m (a ~> b)
askF m (c ~> d)
_ (a ~> b) -> c ~> d
to (c ~> d) -> a ~> b
from -> do
        f <- m (a ~> b)
askF
        f === from (to f)
  , String -> LawBody cs -> Law cs
forall (cs :: [Kind -> Constraint]). String -> LawBody cs -> Law cs
Law (String
name String -> String -> String
forall (a :: Kind). [a] -> [a] -> [a]
++ String
" right inverse") \ @a @b @c @d @e forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> case forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k)
       (m :: Kind -> Kind).
(Labelled k, All cs k, Monad m, Ob a, Ob b, Ob c, Ob d, Ob e) =>
(forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y))
-> Bijection m k
BijectionBody cs
body @a @b @c @d @e String -> m (x ~> y)
forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor of
      Bijection m (a ~> b)
_ m (c ~> d)
askG (a ~> b) -> c ~> d
to (c ~> d) -> a ~> b
from -> do
        g <- m (c ~> d)
askG
        g === to (from g)
  ]

-- * The laws of a category

-- | 'id' is a unit for composition, which is associative.
instance Laws '[CategoryOf] where
  laws :: [Law '[CategoryOf]]
laws =
    [ String -> LawBody '[CategoryOf] -> Law '[CategoryOf]
forall (cs :: [Kind -> Constraint]). String -> LawBody cs -> Law cs
Law String
"left identity" \ @a @b forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
        f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @b String
"f"
        f === id . f
    , String -> LawBody '[CategoryOf] -> Law '[CategoryOf]
forall (cs :: [Kind -> Constraint]). String -> LawBody cs -> Law cs
Law String
"right identity" \ @a @b forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
        f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @b String
"f"
        f === f . id
    , String -> LawBody '[CategoryOf] -> Law '[CategoryOf]
forall (cs :: [Kind -> Constraint]). String -> LawBody cs -> Law cs
Law String
"associativity" \ @a @b @c @d forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
        f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @b String
"f"
        g <- mor @b @c "g"
        h <- mor @c @d "h"
        h . (g . f) === (h . g) . f
    ]

-- * Profunctor laws

-- | The laws of the profunctor class @c@, for any profunctor @p@ with @c p@. The instances for
-- classes that "Proarrow.Category.Instance.Free" depends on live here.
type ProLaws :: forall {j} {k}. ((j +-> k) -> Constraint) -> Constraint
class ProLaws c where
  -- | The laws, each tested as its own property.
  proLaws :: [ProLaw c]

-- | A named profunctor law, about one element of the profunctor ('ProLaw') or three ('ProLaw3').
type ProLaw :: forall {j} {k}. ((j +-> k) -> Constraint) -> Type
data ProLaw c = ProLaw String (ProLawBody c) | ProLaw3 String (ProLawBody3 c)

-- | The name of a profunctor law, used as its test's name.
proLawName :: ProLaw c -> String
proLawName :: forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
ProLaw c -> String
proLawName (ProLaw String
name ProLawBody c
_) = String
name
proLawName (ProLaw3 String
name ProLawBody3 c
_) = String
name

-- | The body of a 'ProLaw': given a profunctor @p :: j '+->' k@, six object variables alternating
-- between @k@ and @j@, an element @p :: p a b@ between the first two, and a supply of named
-- arbitrary arrows for each of @k@ and @j@, produce a 'ProEquation'. The element picks its
-- endpoints, so that a test can draw it where @p@ has elements, and a test draws the other
-- variables so that there are arrows @e '~>' c '~>' a@ and @b '~>' d '~>' f@. A body binds as many
-- of the variables as it uses, e.g. @\\ \@_ \@a \@b p morK _ -> ...@.
type ProLawBody :: forall {j} {k}. ((j +-> k) -> Constraint) -> Type
type ProLawBody (cl :: (j +-> k) -> Constraint) =
  forall (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j) (e :: k) (f :: j) m
   . (cl p, Labelled j, Labelled k, Monad m, Ob a, Ob b, Ob c, Ob d, Ob e, Ob f)
  => p a b
  -> (forall (x :: k) y. (Ob x, Ob y) => String -> m (x ~> y))
  -> (forall (x :: j) y. (Ob x, Ob y) => String -> m (x ~> y))
  -> m (ProEquation p)

-- | The body of a 'ProLaw3': a 'ProLawBody' with three elements @p :: p a b@, @p' :: p c d@ and
-- @p'' :: p e f@, which pick all six object variables. A law that needs arbitrary objects uses the
-- endpoints of an element it does not otherwise use.
type ProLawBody3 :: forall {j} {k}. ((j +-> k) -> Constraint) -> Type
type ProLawBody3 (cl :: (j +-> k) -> Constraint) =
  forall (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j) (e :: k) (f :: j) m
   . (cl p, Labelled j, Labelled k, Monad m, Ob a, Ob b, Ob c, Ob d, Ob e, Ob f)
  => p a b
  -> p c d
  -> p e f
  -> (forall (x :: k) y. (Ob x, Ob y) => String -> m (x ~> y))
  -> (forall (x :: j) y. (Ob x, Ob y) => String -> m (x ~> y))
  -> m (ProEquation p)

-- | 'dimap' preserves identities and composition, and 'lmap' and 'rmap' are its two halves.
instance ProLaws Profunctor where
  proLaws :: [ProLaw Profunctor]
proLaws =
    [ String -> ProLawBody Profunctor -> ProLaw Profunctor
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"dimap identity" \p a b
p forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> p a b
p p a b -> p a b -> m (ProEquation p)
forall {j :: Kind} {k :: Kind} (m :: Kind -> Kind) (p :: j +-> k)
       (a :: k) (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= (a ~> a) -> (b ~> b) -> p a b -> p a b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j :: Kind} {k :: Kind} (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 :: Kind} (p :: CAT k) (a :: k).
(Promonad p, Ob a) =>
p a a
id b ~> b
forall (a :: j). Ob a => a ~> a
forall {k :: Kind} (p :: CAT k) (a :: k).
(Promonad p, Ob a) =>
p a a
id p a b
p
    , String -> ProLawBody Profunctor -> ProLaw Profunctor
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"dimap composition" \ @_ @a @b @c @d @e @f p a b
p forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
morK forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morJ -> do
        g <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
morK @c @a String
"g"
        h <- morJ @b @d "h"
        g' <- morK @e @c "g'"
        h' <- morJ @d @f "h'"
        dimap (g . g') (h' . h) p =:= dimap g' h' (dimap g h p)
    , String -> ProLawBody Profunctor -> ProLaw Profunctor
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"lmap" \ @_ @a @_ @c p a b
p forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
morK forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> do
        g <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
morK @c @a String
"g"
        lmap g p =:= dimap g id p
    , String -> ProLawBody Profunctor -> ProLaw Profunctor
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"rmap" \ @_ @_ @b @_ @d p a b
p forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morJ -> do
        h <- forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morJ @b @d String
"h"
        rmap h p =:= dimap id h p
    ]

-- | 'index' and 'tabulate' are inverse and natural, and 'repUniv' is @'tabulate' 'id'@.
instance ProLaws Representable where
  proLaws :: [ProLaw Representable]
proLaws =
    [ String -> ProLawBody Representable -> ProLaw Representable
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"tabulate . index" \p a b
p forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> p a b
p p a b -> p a b -> m (ProEquation p)
forall {j :: Kind} {k :: Kind} (m :: Kind -> Kind) (p :: j +-> k)
       (a :: k) (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= (a ~> (p % b)) -> p a b
forall (b :: j) (a :: k). Ob b => (a ~> (p % b)) -> p a b
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (p a b -> a ~> (p % b)
forall (a :: k) (b :: j). p a b -> a ~> (p % b)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p a b
p)
    , String -> ProLawBody Representable -> ProLaw Representable
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"index . tabulate" \ @p @a @b p a b
_ forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
morK forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: j) (r :: Kind).
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: j +-> k) (a :: j) (r :: Kind).
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @p @b do
        g <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
morK @a @(p % b) String
"g"
        g === index (tabulate @p @b g)
    , String -> ProLawBody Representable -> ProLaw Representable
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"index naturality" \ @p @a @b @c @d p a b
p forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
morK forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morJ -> do
        g <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
morK @c @a String
"g"
        h <- morJ @b @d "h"
        index (dimap g h p) === repMap @p h . index p . g
    , String -> ProLawBody Representable -> ProLaw Representable
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"repUniv" \ @p @_ @b p a b
_ forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: j) (r :: Kind).
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: j +-> k) (a :: j) (r :: Kind).
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @p @b (forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv @p @b p (p % b) b -> p (p % b) b -> m (ProEquation p)
forall {j :: Kind} {k :: Kind} (m :: Kind -> Kind) (p :: j +-> k)
       (a :: k) (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= ((p % b) ~> (p % b)) -> p (p % b) b
forall (b :: j) (a :: k). Ob b => (a ~> (p % b)) -> p a b
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (p % b) ~> (p % b)
forall (a :: k). Ob a => a ~> a
forall {k :: Kind} (p :: CAT k) (a :: k).
(Promonad p, Ob a) =>
p a a
id)
    ]

-- | 'coindex' and 'cotabulate' are inverse and natural, and 'corepUniv' is @'cotabulate' 'id'@.
instance ProLaws Corepresentable where
  proLaws :: [ProLaw Corepresentable]
proLaws =
    [ String -> ProLawBody Corepresentable -> ProLaw Corepresentable
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"cotabulate . coindex" \p a b
p forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> p a b
p p a b -> p a b -> m (ProEquation p)
forall {j :: Kind} {k :: Kind} (m :: Kind -> Kind) (p :: j +-> k)
       (a :: k) (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= ((p %% a) ~> b) -> p a b
forall (a :: k) (b :: j). Ob a => ((p %% a) ~> b) -> p a b
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (p a b -> (p %% a) ~> b
forall (a :: k) (b :: j). p a b -> (p %% a) ~> b
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex p a b
p)
    , String -> ProLawBody Corepresentable -> ProLaw Corepresentable
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"coindex . cotabulate" \ @p @a @b p a b
_ forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morJ -> forall {k1 :: Kind} {k2 :: Kind} (p :: k1 +-> k2) (a :: k2)
       (r :: Kind).
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: j +-> k) (a :: k) (r :: Kind).
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @p @a do
        h <- forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morJ @(p %% a) @b String
"h"
        h === coindex (cotabulate @p @a h)
    , String -> ProLawBody Corepresentable -> ProLaw Corepresentable
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"coindex naturality" \ @p @a @b @c @d p a b
p forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
morK forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morJ -> do
        g <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
morK @c @a String
"g"
        h <- morJ @b @d "h"
        coindex (dimap g h p) === h . coindex p . corepMap @p g
    , String -> ProLawBody Corepresentable -> ProLaw Corepresentable
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"corepUniv" \ @p @a p a b
_ forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall {k1 :: Kind} {k2 :: Kind} (p :: k1 +-> k2) (a :: k2)
       (r :: Kind).
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: j +-> k) (a :: k) (r :: Kind).
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @p @a (forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv @p @a p a (p %% a) -> p a (p %% a) -> m (ProEquation p)
forall {j :: Kind} {k :: Kind} (m :: Kind -> Kind) (p :: j +-> k)
       (a :: k) (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= ((p %% a) ~> (p %% a)) -> p a (p %% a)
forall (a :: k) (b :: j). Ob a => ((p %% a) ~> b) -> p a b
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (p %% a) ~> (p %% a)
forall (a :: j). Ob a => a ~> a
forall {k :: Kind} (p :: CAT k) (a :: k).
(Promonad p, Ob a) =>
p a a
id)
    ]

-- | 'dagger' is an involution that reverses 'dimap'. At the hom profunctor these are the laws of a
-- dagger category.
instance ProLaws DaggerProfunctor where
  proLaws :: [ProLaw DaggerProfunctor]
proLaws =
    [ String -> ProLawBody DaggerProfunctor -> ProLaw DaggerProfunctor
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"dagger involution" \p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> p a b
p p a b -> p a b -> m (ProEquation p)
forall {j :: Kind} {k :: Kind} (m :: Kind -> Kind) (p :: j +-> k)
       (a :: k) (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= p b a -> p a b
forall (a :: j) (b :: j). p a b -> p b a
forall (k :: Kind) (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
dagger (p a b -> p b a
forall (a :: j) (b :: j). p a b -> p b a
forall (k :: Kind) (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
dagger p a b
p)
    , String -> ProLawBody DaggerProfunctor -> ProLaw DaggerProfunctor
forall {j :: Kind} {k :: Kind} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"dagger dimap" \ @_ @a @b @c @d p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morJ -> do
        g <- forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK @c @a String
"g"
        h <- morJ @b @d "h"
        dagger (dimap g h p) =:= dimap (dagger h) (dagger g) (dagger p)
    ]

-- * Naming arrows

-- | Categories whose arrows can be given a name, for printing laws. Naming leaves the arrow as it
-- is.
type Labelled :: Kind -> Constraint
class (CategoryOf k) => Labelled k where
  -- | @'label' s f@ is @f@, printed as @s@.
  label :: String -> (a :: k) ~> b -> a ~> b