proarrow:testing
Safe HaskellNone
LanguageGHC2024

Proarrow.Testing.Laws

Description

Reusable law-checking properties, parameterized over any Testable kind: propCategory, propMonoidal, propBinaryProducts, propClosed, propProfunctor, propMonoid, and friends. Wiring a new category into a test suite is a Testable instance plus calls to these -- see proarrow's own test suite for many examples.

Many of these take an explicit witness that TestOb is closed under the structure being tested (e.g. that TestOb (a ** b) follows from TestOb a and TestOb b), since in general a category may restrict which objects are testable. The _-suffixed variant (e.g. propMonoidal_) supplies that witness for free, and so carries a TestObIsOb constraint: it applies exactly when every object is a TestOb -- typically a category that leaves TestOb at its Ob default.

Synopsis

Documentation

testEq :: TestingEqShow a => String -> String -> a -> String -> a -> Property () Source Github #

propCategory :: Testable k => TestTree Source Github #

propTerminalObject :: (Testable k, HasTerminalObject k, TestOb (TerminalObject :: k)) => TestTree Source Github #

propInitialObject :: (Testable k, HasInitialObject k, TestOb (InitialObject :: k)) => TestTree Source Github #

propBinaryProducts :: (Testable k, HasBinaryProducts k) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a && b) => r) -> r) -> TestTree Source Github #

propBinaryProducts_ :: (Testable k, HasBinaryProducts k, TestObIsOb k) => TestTree Source Github #

propBinaryCoproducts :: (Testable k, HasBinaryCoproducts k) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a || b) => r) -> r) -> TestTree Source Github #

propBinaryCoproducts_ :: (Testable k, HasBinaryCoproducts k, TestObIsOb k) => TestTree Source Github #

propEqualizers :: (Testable k, HasEqualizers k) => (forall (e :: k) r. Ob e => (TestOb e => r) -> r) -> TestTree Source Github #

Checks the equalizer laws: the equalizer arrow e equalizes f and g; any h that factors through e (built here as e . p for an arbitrary p, so the precondition holds by construction) is correctly recovered by factorEqualizer; and e is mono (composing with it on the left reflects equality).

Unlike propBinaryProducts, the equalizer object isn't computed from a, b by a type family -- it's an arbitrary object revealed at runtime, whose Ob evidence Objs recovers generically from the equalizer arrow. So withTestOb only ever needs to bridge that single recovered Ob to TestOb.

propEqualizers_ :: (Testable k, HasEqualizers k, TestObIsOb k) => TestTree Source Github #

propCoequalizers :: (Testable k, HasCoequalizers k) => (forall (c :: k) r. Ob c => (TestOb c => r) -> r) -> TestTree Source Github #

Checks the coequalizer laws, dual to propEqualizers: the coequalizer arrow c coequalizes f and g; any h that factors through c (built here as p . c for an arbitrary p, so the precondition holds by construction) is correctly recovered by factorCoequalizer; and c is epi (post-composing with it on the right reflects equality).

propCoequalizers_ :: (Testable k, HasCoequalizers k, TestObIsOb k) => TestTree Source Github #

propPullbacks :: (Testable k, HasPullbacks k) => (forall (p :: k) r. Ob p => (TestOb p => r) -> r) -> TestTree Source Github #

Checks the pullback laws: the pullback cone commutes; it's jointly monic (composing with both legs at once reflects equality); and any compatible cone (built here as (p1 . j, p2 . j) for an arbitrary j, so compatibility holds by construction) is correctly recovered by factorPullback.

propPullbacks_ :: (Testable k, HasPullbacks k, TestObIsOb k) => TestTree Source Github #

propPushouts :: (Testable k, HasPushouts k) => (forall (p :: k) r. Ob p => (TestOb p => r) -> r) -> TestTree Source Github #

Checks the pushout laws, dual to propPullbacks: the pushout cocone commutes; it's jointly epic (post-composing with both legs at once reflects equality); and any compatible cocone (built here as (j . p1, j . p2) for an arbitrary j, so compatibility holds by construction) is correctly recovered by factorPushout.

propPushouts_ :: (Testable k, HasPushouts k, TestObIsOb k) => TestTree Source Github #

propMonoidal :: (Testable k, Monoidal k, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> TestTree Source Github #

propMonoidal_ :: (Testable k, Monoidal k, TestObIsOb k) => TestTree Source Github #

propSymMonoidal :: (Testable k, SymMonoidal k, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> TestTree Source Github #

propSymMonoidal_ :: (Testable k, SymMonoidal k, TestObIsOb k) => TestTree Source Github #

propCopyDiscard :: (Testable k, CopyDiscard k, TestOb (Unit :: k)) => (forall (a :: k) r. TestOb a => ((Ob a, CocommutativeComonoid a) => r) -> r) -> (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> TestTree Source Github #

propCopyDiscard_ :: (Testable k, CopyDiscard k, TestObIsOb k) => TestTree Source Github #

The cocommutative comonoid on each object is supplied by CopyDiscard itself (its Supplies CocommutativeComonoid k superclass), so only Ob a has to be recovered from TestOb a -- through obFromTestOb, because with that quantified superclass in scope GHC no longer finds the TestOb a => Ob' a => Ob a route on its own.

propCartesian :: (Testable k, Cartesian k, TestOb (Unit :: k)) => (forall (a :: k) r. TestOb a => (Ob a => r) -> r) -> (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> TestTree Source Github #

The coherence law tying Cartesian to its CopyDiscard superclass (Fox's theorem): the comonoid supplied on every object is the natural one, copy = id &&& id and discard = terminate.

propCartesianAt :: forall {k} (a :: k). (Testable k, Cartesian k, TensorIsProduct a a, TestOb (Unit :: k), TestOb a, Ob a, TestOb (a ** a)) => Property () Source Github #

propCartesian_ :: (Testable k, Cartesian k, TestObIsOb k, TestOb (Unit :: k)) => TestTree Source Github #

propDistributive :: (Testable k, Distributive k, TestOb (InitialObject :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a || b) => r) -> r) -> TestTree Source Github #

propDistributive_ :: (Testable k, Distributive k, TestObIsOb k) => TestTree Source Github #

propClosed :: (Testable k, Closed k, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ~~> b) => r) -> r) -> TestTree Source Github #

propClosed_ :: (Testable k, Closed k, TestObIsOb k) => TestTree Source Github #

propStarAutonomous :: (Testable k, StarAutonomous k, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> (forall (a :: k) r. TestOb a => (TestOb (Dual a) => r) -> r) -> TestTree Source Github #

Laws of a *-autonomous category: dual is a contravariant functor and, together with dualInv, establishes a bijection on hom-sets; linDist/linDistInv establish a bijection Hom(a ** b, Dual c) ≅ Hom(a, Dual (b ** c)), natural in all three variables; and doubleNegIso witnesses that double dualization is (naturally) isomorphic to the identity.

propStarAutonomous_ :: (Testable k, StarAutonomous k, TestObIsOb k) => TestTree Source Github #

propCompactClosed :: (Testable k, CompactClosed k, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> (forall (a :: k) r. TestOb a => (TestOb (Dual a) => r) -> r) -> TestTree Source Github #

Laws of a compact closed category: distribDual/combineDual establish an isomorphism Dual (a ** b) ≅ Dual a ** Dual b and dualUnit/dualUnitInv establish Dual Unit ≅ Unit (i.e. Dual is a strong monoidal functor); and the yanking/zigzag identities witness that a and Dual a are genuinely dual to one another via dualityUnit/dualityCounit.

propCompactClosed_ :: (Testable k, CompactClosed k, TestObIsOb k) => TestTree Source Github #

propFrobenius :: forall {k} (m :: k). (Testable k, SymMonoidal k, CommutativeMonoid m, CocommutativeComonoid m, TestOb m, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> Property () Source Github #

Check that the object m is a special commutative Frobenius algebra: it is a CommutativeMonoid (via propCommutativeMonoid) and a CocommutativeComonoid (via propCocommutativeComonoid), and satisfies speciality (mappend . comult = id) and the Frobenius condition. This is the structure a Hypergraph category supplies -- propHypergraph samples an object and delegates here.

propHypergraph :: (Testable k, SymMonoidal k, TestOb (Unit :: k)) => (forall (a :: k) r. TestOb a => ((Ob a, Frobenius a) => r) -> r) -> (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> TestTree Source Github #

Check propFrobenius at randomly sampled objects.

propHypergraph_ :: (Testable k, SymMonoidal k, TestObIsOb k, forall (a :: k). TestOb a => Frobenius a) => TestTree Source Github #

testProfunctor :: forall {j} {k} (p :: j +-> k). TestableProfunctor p => TestTree Source Github #

propProfunctor :: forall {j} {k} (p :: j +-> k). TestableProfunctor p => Property () Source Github #

propProfunctorWith :: (Profunctor p, Testable j, Testable k) => Property (SomeProfunctorElt p) -> (forall (a :: k) (b :: j) r. (TestOb a, TestOb b) => (TestingEqShow (p a b) => r) -> r) -> Property () Source Github #

propFunctor :: forall {k1} {k2} (f :: k1 -> k2). (Functor f, Testable k1, Testable k2) => (forall (a :: k1) r. TestOb a => (TestOb (f a) => r) -> r) -> Property () Source Github #

Check the functor laws of a Functor f: map id = id and map (g . f) = map g . map f. The witness lifts TestOb along f (usually \ @a r -> r when TestOb (f a) follows from TestOb a). Functors encoded as representable profunctors (FunctorForRep) are instead tested via their Rep with propProfunctor, since the profunctor laws on Rep f are the functor laws on f.

testFunctor :: forall {k1} {k2} (f :: k1 -> k2). (Functor f, Testable k1, Testable k2) => (forall (a :: k1) r. TestOb a => (TestOb (f a) => r) -> r) -> TestTree Source Github #

testFunctor_ :: forall {k1} {k2} (f :: k1 -> k2). (Functor f, Testable k1, Testable k2, forall (a :: k1). TestOb a => TestOb' (f a)) => TestTree Source Github #

propNaturalTransformation :: forall {j} {k} (p :: j +-> k) (q :: j +-> k). (TestableProfunctor p, TestableProfunctor q) => (p :~> q) -> Property () Source Github #

propRepresentable :: forall {j} {k} (p :: j +-> k). (Representable p, TestableProfunctor p) => (forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r) -> Property () Source Github #

Check the Representable laws of p: index and tabulate are mutually inverse (p a b is naturally isomorphic to a ~> p % b), and that iso is natural -- index (dimap f g p) = repMap g . index p . f -- which is what pins repMap down as the functorial action of the representing functor p % -. The witness lifts TestOb along p % -. Unlike the hom-level propAdjunction, this generates p a b elements, so it needs p to be an element-generatable TestableProfunctor.

testRepresentable :: forall {j} {k} (p :: j +-> k). (Representable p, TestableProfunctor p) => (forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r) -> TestTree Source Github #

testRepresentable_ :: forall {j} {k} (p :: j +-> k). (Representable p, TestableProfunctor p, TestObIsOb k) => TestTree Source Github #

propCorepresentable :: forall {j} {k} (p :: j +-> k). (Corepresentable p, TestableProfunctor p) => (forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r) -> Property () Source Github #

Check the Corepresentable laws of p, dual to propRepresentable: coindex and cotabulate are mutually inverse (p a b is naturally isomorphic to p %% a ~> b), and that iso is natural -- coindex (dimap f g p) = g . coindex p . corepMap f, pinning down corepMap as the functorial action of the corepresenting functor p %% -. The witness lifts TestOb along p %% -.

testCorepresentable :: forall {j} {k} (p :: j +-> k). (Corepresentable p, TestableProfunctor p) => (forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r) -> TestTree Source Github #

testCorepresentable_ :: forall {j} {k} (p :: j +-> k). (Corepresentable p, TestableProfunctor p, TestObIsOb j) => TestTree Source Github #

propAdjunction :: forall {j} {k} (p :: j +-> k). (Adjunction p, TestableProfunctor p) => (forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r) -> (forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r) -> Property () Source Github #

Check the adjunction laws of an Adjunction p. An adjunction here is exactly a profunctor that is both Representable and Corepresentable -- its left adjoint is L = p %% - and its right adjoint R = p % - -- and it carries no laws of its own beyond theirs (leftAdjunct/rightAdjunct are just index . cotabulate and coindex . tabulate). So this simply delegates to propCorepresentable (for L) and propRepresentable (for R); the two witnesses lift TestOb along L and R respectively.

testAdjunction :: forall {j} {k} (p :: j +-> k). (Adjunction p, TestableProfunctor p) => (forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r) -> (forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r) -> TestTree Source Github #

testAdjunction_ :: forall {j} {k} (p :: j +-> k). (Adjunction p, TestableProfunctor p, TestObIsOb j, TestObIsOb k) => TestTree Source Github #

propIso :: forall {k} (a :: k) (b :: k). (Testable k, TestOb a, TestOb b) => (a ~> b) -> (b ~> a) -> Property () Source Github #

propIso' :: forall {k} (c :: (k -> k -> Type) -> Constraint) (a :: k) (b :: k). (Testable k, TestOb a, TestOb b, Ob b => c (ExOptic (GetterFl :: (k +-> k) -> (k +-> k) -> Constraint) b b), Ob b => c (ExOptic (Flip (GetterFl :: (k +-> k) -> (k +-> k) -> Constraint)) b b)) => Optic c a a b b -> Property () Source Github #

propIsoP :: forall {j1} {k1} {j2} {k2} p q (a :: k1) (b :: j1) (c :: k2) (d :: j2). (TestableTypeP p, TestableTypeP q, TestOb a, TestOb b, TestOb c, TestOb d) => (p a b -> q c d) -> (q c d -> p a b) -> Property () Source Github #

propNaturalIsoP :: forall {j} {k} (p :: j +-> k) (q :: j +-> k). (TestableProfunctor p, TestableTypeP p, TestableProfunctor q, TestableTypeP q) => (p :~> q) -> (q :~> p) -> Property () Source Github #

propMonoid :: forall {k} (m :: k). (Testable k, Monoid m, TestOb m, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> Property () Source Github #

propCommutativeMonoid :: forall {k} (m :: k). (Testable k, CommutativeMonoid m, TestOb m, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> Property () Source Github #

propCocommutativeComonoid :: forall {k} (m :: k). (Testable k, CocommutativeComonoid m, TestOb m, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> Property () Source Github #

testMonoid :: forall {k} (m :: k). (Testable k, Monoid m, TestOb m, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> TestTree Source Github #

testMonoid_ :: forall {k} (m :: k). (Testable k, Monoid m, TestObIsOb k) => TestTree Source Github #

testComonoid :: forall {k} (m :: k). (Testable k, Comonoid m, TestOb m, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> TestTree Source Github #

testComonoid_ :: forall {k} (m :: k). (Testable k, Comonoid m, TestObIsOb k) => TestTree Source Github #

testCommutativeMonoid :: forall {k} (m :: k). (Testable k, CommutativeMonoid m, TestOb m, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> TestTree Source Github #

testCommutativeMonoid_ :: forall {k} (m :: k). (Testable k, CommutativeMonoid m, TestObIsOb k) => TestTree Source Github #

testCocommutativeComonoid :: forall {k} (m :: k). (Testable k, CocommutativeComonoid m, TestOb m, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> TestTree Source Github #

testCocommutativeComonoid_ :: forall {k} (m :: k). (Testable k, CocommutativeComonoid m, TestObIsOb k) => TestTree Source Github #

testFrobenius :: forall {k} (m :: k). (Testable k, CommutativeMonoid m, CocommutativeComonoid m, TestOb m, TestOb (Unit :: k)) => (forall (a :: k) (b :: k) r. (TestOb a, TestOb b) => (TestOb (a ** b) => r) -> r) -> TestTree Source Github #

testFrobenius_ :: forall {k} (m :: k). (Testable k, CommutativeMonoid m, CocommutativeComonoid m, TestObIsOb k) => TestTree Source Github #