{-# 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, Functor, Monad, String, fmap, pure, (++))

import Proarrow.Category.Instance.Free (All)
import Proarrow.Core (CategoryOf (..), Hom, Kind, Profunctor (..), Promonad (..), type (+->))
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

infix 1 ===

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

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)

-- | An equation between arrows of the codomain, as the result of a profunctor law body.
inK :: forall {j} {k} m (p :: j +-> k). (Functor m) => m (Equation k) -> m (ProEquation p)
inK :: forall {j :: Kind} {k :: Kind} (m :: Kind -> Kind) (p :: j +-> k).
Functor m =>
m (Equation k) -> m (ProEquation p)
inK = (ProEquation (~>) -> ProEquation p)
-> m (ProEquation (~>)) -> m (ProEquation p)
forall (a :: Kind) (b :: Kind). (a -> b) -> m a -> m b
forall (f :: Kind -> Kind) (a :: Kind) (b :: Kind).
Functor f =>
(a -> b) -> f a -> f b
fmap ProEquation (~>) -> ProEquation p
forall {j :: Kind} {k :: Kind} (p :: j +-> k).
Equation k -> ProEquation p
InK

-- | An equation between arrows of the domain, as the result of a profunctor law body.
inJ :: forall {j} {k} m (p :: j +-> k). (Functor m) => m (Equation j) -> m (ProEquation p)
inJ :: forall {j :: Kind} {k :: Kind} (m :: Kind -> Kind) (p :: j +-> k).
Functor m =>
m (Equation j) -> m (ProEquation p)
inJ = (ProEquation (~>) -> ProEquation p)
-> m (ProEquation (~>)) -> m (ProEquation p)
forall (a :: Kind) (b :: Kind). (a -> b) -> m a -> m b
forall (f :: Kind -> Kind) (a :: Kind) (b :: Kind).
Functor f =>
(a -> b) -> f a -> f b
fmap ProEquation (~>) -> ProEquation p
forall {j :: Kind} {k :: Kind} (p :: j +-> k).
Equation j -> ProEquation p
InJ

-- * 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"
        inK (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"
        inK (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)
    ]

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