Safe Haskell	None
Language	GHC2024

Proarrow.Tools.Laws

Contents

Laws
Equations
Inverses
Bijections
The laws of a category
Profunctor laws
Naming arrows

Description

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 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 SymMonoidalStructures. The instances live next to their classes.

Synopsis

class Laws (cs :: [Kind -> Constraint]) where
- laws :: [Law cs]
data Law (cs :: [Kind -> Constraint]) = Law String (LawBody cs)
lawName :: forall (cs :: [Kind -> Constraint]). Law cs -> String
type LawBody (cs :: [Kind -> Constraint]) = forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (m :: Type -> Type). (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)) -> m (Equation k)
data ProEquation (p :: j +-> k) where
- (:=:) :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). 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
type Equation k = ProEquation (Hom k)
withSides :: Equation k -> (forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r) -> r
(===) :: forall {k} m (a :: k) (b :: k). Applicative m => (a ~> b) -> (a ~> b) -> m (Equation k)
(=:=) :: forall {j} {k} m p (a :: k) (b :: j). Applicative m => p a b -> p a b -> m (ProEquation p)
inK :: forall {j} {k} m (p :: j +-> k). Functor m => m (Equation k) -> m (ProEquation p)
inJ :: forall {j} {k} m (p :: j +-> k). Functor m => m (Equation j) -> m (ProEquation p)
data Inverses k where
- Inverses :: forall {k} (a :: k) (b :: k). (a ~> b) -> (b ~> a) -> Inverses k
type PureLawBody (cs :: [Kind -> Constraint]) (r :: Kind -> Type) = 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
leftInverse :: CategoryOf k => Inverses k -> Equation k
rightInverse :: CategoryOf k => Inverses k -> Equation k
inverses :: forall (cs :: [Kind -> Constraint]). String -> PureLawBody cs Inverses -> [Law cs]
data Bijection (m :: Type -> Type) k where
- Bijection :: forall {k} (m :: Type -> Type) (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
type BijectionBody (cs :: [Kind -> Constraint]) = forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (m :: Type -> Type). (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
bijection :: forall (cs :: [Kind -> Constraint]). String -> BijectionBody cs -> [Law cs]
class ProLaws (c :: (j +-> k) -> Constraint) where
- proLaws :: [ProLaw c]
data ProLaw (c :: (j +-> k) -> Constraint)
- = ProLaw String (ProLawBody c)
- | ProLaw3 String (ProLawBody3 c)
proLawName :: forall {j} {k} (c :: (j +-> k) -> Constraint). ProLaw c -> String
type ProLawBody (cl :: (j +-> k) -> Constraint) = forall (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j) (e :: k) (f :: j) (m :: Type -> Type). (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 :: k). (Ob x, Ob y) => String -> m (x ~> y)) -> (forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)) -> m (ProEquation p)
type ProLawBody3 (cl :: (j +-> k) -> Constraint) = forall (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j) (e :: k) (f :: j) (m :: Type -> Type). (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 :: k). (Ob x, Ob y) => String -> m (x ~> y)) -> (forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)) -> m (ProEquation p)
class CategoryOf k => Labelled k where
- label :: forall (a :: k) (b :: k). String -> (a ~> b) -> a ~> b

Laws

class Laws (cs :: [Kind -> Constraint]) where Source Github #

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
    ]

Methods

laws :: [Law cs] Source Github #

The laws, each tested as its own property.

Instances

Instances details

Laws SymMonoidalStructures Source Github #	`swap` is a natural self-inverse satisfying the hexagon identity.
Instance details Defined in Proarrow.Category.Monoidal Methods laws :: [Law SymMonoidalStructures] Source Github #
Laws ClosedStructures Source Github #	`apply` undoes `curry` and every arrow into an exponential is the `curry` of one (`curry` is a bijection with inverse `f \|-> apply . (f id)`), `curry` is natural in all three objects, and `^^^` is the exponential's action on arrows defined from `curry` and `apply`. Together these make `(- b)` left adjoint to `(b ~~> -)`, and `^^^` a profunctor.
Instance details Defined in Proarrow.Category.Monoidal.Closed Methods laws :: [Law ClosedStructures] Source Github #
Laws CompactClosedStructures Source Github #	`distribDual` and `dualUnit` are isomorphisms (so `Dual` is strong monoidal), and `dualityUnit` and `dualityCounit` satisfy the zigzag identities, making `Dual a` dual to `a`.
Instance details Defined in Proarrow.Category.Monoidal.CompactClosed Methods laws :: [Law CompactClosedStructures] Source Github #
Laws CopyDiscardStructures Source Github #	`copy` and `discard` are the supplied comonoid, and they respect the tensor: copying or discarding `a ** b` is copying or discarding both parts, and on the unit they do nothing. The comonoid laws and cocommutativity are those of the supply, in Proarrow.Monoid.
Instance details Defined in Proarrow.Category.Monoidal.CopyDiscard Methods laws :: [Law CopyDiscardStructures] Source Github #
Laws DistributiveStructures Source Github #	The tensor distributes over coproducts and is absorbed by the initial object: `distL`, `distR`, `absorbL` and `absorbR` are isomorphisms, with the inverses `distLInv`, `distRInv` and `initiate`.
Instance details Defined in Proarrow.Category.Monoidal.Distributive Methods laws :: [Law DistributiveStructures] Source Github #
Laws FrobeniusStructures Source Github #	The supplied monoids and comonoids are special and satisfy the Frobenius law. Their monoid and comonoid laws, and their commutativity, are separate instances, in Proarrow.Monoid.
Instance details Defined in Proarrow.Category.Monoidal.Hypergraph Methods laws :: [Law FrobeniusStructures] Source Github #
Laws StarAutonomousStructures Source Github #	`dual` is a contravariant functor, bijective on hom-sets with inverse `dualInv`; `doubleNeg` is an isomorphism; and `linDist` is a natural bijection `Hom(a b, Dual c) ≅ Hom(a, Dual (b c))` with inverse `linDistInv`.
Instance details Defined in Proarrow.Category.Monoidal.StarAutonomous Methods laws :: [Law StarAutonomousStructures] Source Github #
Laws TracedStructures Source Github #	The trace laws, for `trace` over `u` of `f : x u ~> y u`: natural in `x` and `y`, dinatural in `u` (sliding), trivial over the unit and iterated over a tensor (vanishing), compatible with tensoring on the left (superposing), and the trace of a swap is the identity (yanking).
Instance details Defined in Proarrow.Category.Monoidal.Strength Methods laws :: [Law TracedStructures] Source Github #
Laws '[Monoidal, SymMonoidal, Supplies CocommutativeComonoid] Source Github #	The supplied comonoids are cocommutative: `comult` is unchanged by `swap`.
Instance details Defined in Proarrow.Monoid Methods laws :: [Law '[Monoidal, SymMonoidal, Supplies CocommutativeComonoid]] Source Github #
Laws '[Monoidal, SymMonoidal, Supplies CommutativeMonoid] Source Github #	The supplied monoids are commutative: `mappend` is unchanged by `swap`.
Instance details Defined in Proarrow.Monoid Methods laws :: [Law '[Monoidal, SymMonoidal, Supplies CommutativeMonoid]] Source Github #
Laws '[Monoidal, Supplies Comonoid] Source Github #	In a category that supplies comonoids, every object is one: `counit` is a unit for `comult`, and `comult` is coassociative.
Instance details Defined in Proarrow.Monoid Methods laws :: [Law '[Monoidal, Supplies Comonoid]] Source Github #
Laws '[Monoidal, Supplies Monoid] Source Github #	In a category that supplies monoids, every object is one: `mempty` is a unit for `mappend` (up to the unitors), and `mappend` is associative (up to the associator).
Instance details Defined in Proarrow.Monoid Methods laws :: [Law '[Monoidal, Supplies Monoid]] Source Github #
Laws '[Monoidal] Source Github #	The tensor is a bifunctor, and the unitors and the associator are natural isomorphisms satisfying the triangle and pentagon identities.
Instance details Defined in Proarrow.Category.Monoidal Methods laws :: [Law '[Monoidal]] Source Github #
Laws '[HasBinaryCoproducts] Source Github #	The universal property of the binary coproduct: the injections recover the components of `f \|\|\| g`, and every arrow out of the coproduct is the copairing of its components.
Instance details Defined in Proarrow.Colimit.BinaryCoproduct Methods laws :: [Law '[HasBinaryCoproducts]] Source Github #
Laws '[HasInitialObject] Source Github #	Every arrow out of the initial object is `initiate`.
Instance details Defined in Proarrow.Colimit.Initial Methods laws :: [Law '[HasInitialObject]] Source Github #
Laws '[CategoryOf] Source Github #	`id` is a unit for composition, which is associative.
Instance details Defined in Proarrow.Tools.Laws Methods laws :: [Law '[CategoryOf]] Source Github #
Laws '[HasBinaryProducts] Source Github #	The universal property of the binary product: the projections recover the components of `f &&& g`, and every arrow into the product is the pairing of its components.
Instance details Defined in Proarrow.Limit.BinaryProduct Methods laws :: [Law '[HasBinaryProducts]] Source Github #
Laws '[HasTerminalObject] Source Github #	Every arrow into the terminal object is `terminate`.
Instance details Defined in Proarrow.Limit.Terminal Methods laws :: [Law '[HasTerminalObject]] Source Github #

data Law (cs :: [Kind -> Constraint]) Source Github #

A named law.

Constructors

Law String (LawBody cs)

lawName :: forall (cs :: [Kind -> Constraint]). Law cs -> String Source Github #

The name of a law, used as its test's name.

type LawBody (cs :: [Kind -> Constraint]) = forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (m :: Type -> Type). (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)) -> m (Equation k) Source Github #

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.

Equations

data ProEquation (p :: j +-> k) where Source Github #

Two parallel elements of a profunctor claimed to be equal, or an equation between arrows of its codomain (InK) or domain (InJ).

Constructors

(:=:) :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). p a b -> p a b -> ProEquation p infix 1
InK :: forall {j} {k} (p :: j +-> k). Equation k -> ProEquation p
InJ :: forall {j} {k} (p :: j +-> k). Equation j -> ProEquation p

type Equation k = ProEquation (Hom k) Source Github #

Two parallel arrows claimed to be equal: an equation between elements of the hom profunctor.

withSides :: Equation k -> (forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r) -> r Source Github #

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.

(===) :: forall {k} m (a :: k) (b :: k). Applicative m => (a ~> b) -> (a ~> b) -> m (Equation k) infix 1 Source Github #

An equation between arrows as the result of a law body: l === r = pure (l :=: r).

(=:=) :: forall {j} {k} m p (a :: k) (b :: j). Applicative m => p a b -> p a b -> m (ProEquation p) infix 1 Source Github #

An equation between elements as the result of a profunctor law body: l =:= r = pure (l :=: r).

inK :: forall {j} {k} m (p :: j +-> k). Functor m => m (Equation k) -> m (ProEquation p) Source Github #

An equation between arrows of the codomain, as the result of a profunctor law body.

inJ :: forall {j} {k} m (p :: j +-> k). Functor m => m (Equation j) -> m (ProEquation p) Source Github #

An equation between arrows of the domain, as the result of a profunctor law body.

Inverses

data Inverses k where Source Github #

A pair of arrows claimed to be inverse to each other, see inverses.

Constructors

Inverses :: forall {k} (a :: k) (b :: k). (a ~> b) -> (b ~> a) -> Inverses k

type PureLawBody (cs :: [Kind -> Constraint]) (r :: Kind -> Type) = 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 Source Github #

The body of a law that asks for no arrows: given five object variables, an r k.

leftInverse :: CategoryOf k => Inverses k -> Equation k Source Github #

g . f = id and f . g = id for Inverses f g.

rightInverse :: CategoryOf k => Inverses k -> Equation k Source Github #

g . f = id and f . g = id for Inverses f g.

inverses :: forall (cs :: [Kind -> Constraint]). String -> PureLawBody cs Inverses -> [Law cs] Source Github #

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.

Bijections

data Bijection (m :: Type -> Type) k where Source Github #

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.

Constructors

Bijection :: forall {k} (m :: Type -> Type) (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

type BijectionBody (cs :: [Kind -> Constraint]) = forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (m :: Type -> Type). (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 Source Github #

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.

bijection :: forall (cs :: [Kind -> Constraint]). String -> BijectionBody cs -> [Law cs] Source Github #

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.

The laws of a category

Profunctor laws

class ProLaws (c :: (j +-> k) -> Constraint) where Source Github #

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.

Methods

proLaws :: [ProLaw c] Source Github #

The laws, each tested as its own property.

Instances

Instances details

ProLaws (MonoidalProfunctor :: (j +-> k) -> Constraint) Source Github #	`one` is a unit for `` up to the unitors, `` is associative up to the associators, and `**` is natural.
Instance details Defined in Proarrow.Category.Monoidal Methods proLaws :: [ProLaw (MonoidalProfunctor :: (j +-> k) -> Constraint)] Source Github #
ProLaws (Profunctor :: (j +-> k) -> Constraint) Source Github #	`dimap` preserves identities and composition, and `lmap` and `rmap` are its two halves.
Instance details Defined in Proarrow.Tools.Laws Methods proLaws :: [ProLaw (Profunctor :: (j +-> k) -> Constraint)] Source Github #
ProLaws (Representable :: (j +-> k) -> Constraint) Source Github #	`index` and `tabulate` are inverse and natural, and `repUniv` is `tabulate id`.
Instance details Defined in Proarrow.Tools.Laws Methods proLaws :: [ProLaw (Representable :: (j +-> k) -> Constraint)] Source Github #

data ProLaw (c :: (j +-> k) -> Constraint) Source Github #

A named profunctor law, about one element of the profunctor (ProLaw) or three (ProLaw3).

Constructors

ProLaw String (ProLawBody c)
ProLaw3 String (ProLawBody3 c)

proLawName :: forall {j} {k} (c :: (j +-> k) -> Constraint). ProLaw c -> String Source Github #

The name of a profunctor law, used as its test's name.

type ProLawBody (cl :: (j +-> k) -> Constraint) = forall (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j) (e :: k) (f :: j) (m :: Type -> Type). (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 :: k). (Ob x, Ob y) => String -> m (x ~> y)) -> (forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)) -> m (ProEquation p) Source Github #

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 ProLawBody3 (cl :: (j +-> k) -> Constraint) = forall (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j) (e :: k) (f :: j) (m :: Type -> Type). (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 :: k). (Ob x, Ob y) => String -> m (x ~> y)) -> (forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)) -> m (ProEquation p) Source Github #

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.

Naming arrows

class CategoryOf k => Labelled k where Source Github #

Categories whose arrows can be given a name, for printing laws. Naming leaves the arrow as it is.

Methods

label :: forall (a :: k) (b :: k). String -> (a ~> b) -> a ~> b Source Github #

label s f is f, printed as s.

Instances

Instances details

Labelled SVG Source Github #	Derived operations are drawn as what they are made of.
Instance details Defined in Proarrow.Tools.Diagrams.Svg Methods label :: forall (a :: SVG) (b :: SVG). String -> (a ~> b) -> a ~> b Source Github #