Safe Haskell	None
Language	GHC2024

Proarrow.Testing.Laws.Run

Contents

Witnesses
Interpreting with testable objects
Interpreting profunctors
Describing arrows

Description

Checking laws stated as code (Proarrow.Tools.Laws) in a Testable category: testLaws runs each law with random objects for its variables and random arrows for the ones it asks for, and compares both sides.

The endpoints of a law's equation are built inside the law, so their TestOb cannot be listed up front. Instead the law is run in TESTED k, whose objects are built from leaves by the structures' object formers; there an object's Ob is Tested, which rebuilds the TestOb of the object of k it stands for from the Witnesses passed at run time: one Witness per structure in the law's list, e.g. a WithTestOb2 for Monoidal.

A structure this module does not cover can be added from outside it, in the same way as the ones here:

a former for each new kind of object (an open data family, or one of the free category's), with a Tested instance giving its Untest and rebuilding its Ob and TestOb;
a Witness instance for the structure, holding how TestOb is closed under its formers;
the structure's class instance for TESTED, whose arrows describe themselves (prim for a named arrow, app, infixlDoc, infixrDoc for operations on arrows).

Synopsis

testLaws :: forall (cs :: [Kind -> Constraint]) k. (Laws cs, Testable k, All cs (TESTED cs k)) => String -> Witnesses cs k -> TestTree
testLawsWith :: forall (cs :: [Kind -> Constraint]) k. (Laws cs, Testable k, All cs (TESTED cs k)) => Property (Some k) -> String -> Witnesses cs k -> TestTree
testProLaws :: forall {j} {k} (csj :: [Kind -> Constraint]) (csk :: [Kind -> Constraint]) (cl :: (TESTED csj j +-> TESTED csk k) -> Constraint) (p :: j +-> k). (ProLaws cl, TestableProfunctor p, cl (TestedP p :: TESTED csk k -> TESTED csj j -> Type)) => TestOptions -> String -> Witnesses csj j -> Witnesses csk k -> TestTree
data family Witness (c :: Kind -> Constraint) k
data Witnesses (cs :: [Kind -> Constraint]) k where
- WNil :: forall k. Witnesses ('[] :: [Kind -> Constraint]) k
- (:&) :: forall (c :: Kind -> Constraint) k (cs1 :: [Kind -> Constraint]). Witness c k -> Witnesses cs1 k -> Witnesses (c ': cs1) k
class HasWitness (c :: Kind -> Constraint) (cs :: [Kind -> Constraint]) where
- witness :: Witnesses cs k -> Witness c k
data TESTED (cs :: [Kind -> Constraint]) k = TLeaf k
class Tested (a :: TESTED cs k) where
- type Untest (a :: TESTED cs k) :: k
- untestOb :: (Ob (Untest a) => r) -> r
- untestTestOb :: Witnesses cs k -> (TestOb (Untest a) => r) -> r
untestOb2 :: forall {cs1 :: [Kind -> Constraint]} {k1} {cs2 :: [Kind -> Constraint]} {k2} (a :: TESTED cs2 k2) (b :: TESTED cs1 k1) r. (Tested a, Tested b) => ((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb3 :: forall {cs1 :: [Kind -> Constraint]} {k1} {cs2 :: [Kind -> Constraint]} {k2} {cs3 :: [Kind -> Constraint]} {k3} (a :: TESTED cs3 k3) (b :: TESTED cs1 k1) (c :: TESTED cs2 k2) r. (Tested a, Tested b, Tested c) => ((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
untestTestOb2 :: forall {cs :: [Kind -> Constraint]} {k} (a :: TESTED cs k) (b :: TESTED cs k) r. (Tested a, Tested b) => Witnesses cs k -> ((TestOb (Untest a), TestOb (Untest b)) => r) -> r
type TestedArr = TestedP (Hom k) :: TESTED cs k -> TESTED cs k -> Type
pattern TestedArr :: forall cs k a b. () => (Tested a, Tested b) => Doc -> (Untest a ~> Untest b) -> TestedArr a b
data TestedP (p :: j +-> k) (a :: TESTED csk k) (b :: TESTED csj j) where
- TestedP :: forall {csk :: [Kind -> Constraint]} {k} {csj :: [Kind -> Constraint]} {j} (a :: TESTED csk k) (b :: TESTED csj j) (p :: j +-> k). (Tested a, Tested b) => Doc -> p (Untest a) (Untest b) -> TestedP p a b
data family RepF (p :: j +-> k) (b :: TESTED csj j) :: o
class RepresentedBy (csj :: [Kind -> Constraint]) (p :: j +-> k) k'
type Doc = Int -> ShowS
prim :: forall {csk :: [Kind -> Constraint]} {k} {csj :: [Kind -> Constraint]} {j} (a :: TESTED csk k) (b :: TESTED csj j) p. (Tested a, Tested b) => String -> p (Untest a) (Untest b) -> TestedP p a b
atom :: String -> Doc
app :: String -> Doc -> Doc
apps :: String -> [Doc] -> Doc
infixlDoc :: Int -> String -> Doc -> Doc -> Doc
infixrDoc :: Int -> String -> Doc -> Doc -> Doc

Documentation

testLaws :: forall (cs :: [Kind -> Constraint]) k. (Laws cs, Testable k, All cs (TESTED cs k)) => String -> Witnesses cs k -> TestTree Source Github #

Check the laws of Laws cs in k, one property per law: run each law in TESTED with random objects for its variables and random arrows for the ones it asks for. The Witnesses say how TestOb is closed under the structures of cs (see Tested).

testLawsWith :: forall (cs :: [Kind -> Constraint]) k. (Laws cs, Testable k, All cs (TESTED cs k)) => Property (Some k) -> String -> Witnesses cs k -> TestTree Source Github #

testLaws with the objects for the variables drawn from the given generator, e.g. genObSmall where the laws build large objects like exponentials.

testProLaws :: forall {j} {k} (csj :: [Kind -> Constraint]) (csk :: [Kind -> Constraint]) (cl :: (TESTED csj j +-> TESTED csk k) -> Constraint) (p :: j +-> k). (ProLaws cl, TestableProfunctor p, cl (TestedP p :: TESTED csk k -> TESTED csj j -> Type)) => TestOptions -> String -> Witnesses csj j -> Witnesses csk k -> TestTree Source Github #

Check the laws of ProLaws c for the profunctor p, one property per law: run each law with p interpreted as TestedP p, its elements drawn by genProfunctorElt (each picks its two object variables), the other variables of a ProLaw drawn along the chain e ~> c ~> a and b ~> d ~> f where those hom-sets are non-empty, and random arrows for the ones it asks for. The two Witnesses are for the domain j and the codomain k of p, and the TestOptions apply to each law's property.

Witnesses

data family Witness (c :: Kind -> Constraint) k Source Github #

How TestOb is closed under the object formers of the structure c, for the category k. Structures without formers of their own have a witness that holds nothing.

Instances

Instances details

newtype Witness Monoidal k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run newtype Witness Monoidal k = MonoidalW (WithTestOb2 k)
data Witness SymMonoidal k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run data Witness SymMonoidal k = SymMonoidalW
newtype Witness Closed k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run newtype Witness Closed k = ClosedW (WithTestObExp k)
data Witness CompactClosed k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run data Witness CompactClosed k = CompactClosedW
data Witness CopyDiscard k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run data Witness CopyDiscard k = CopyDiscardW
data Witness Distributive k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run data Witness Distributive k = DistributiveW
newtype Witness StarAutonomous k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run newtype Witness StarAutonomous k = StarAutonomousW (WithTestObDual k)
data Witness TracedMonoidal k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run data Witness TracedMonoidal k = TracedW
newtype Witness HasBinaryCoproducts k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run newtype Witness HasBinaryCoproducts k = CoproductsW (WithTestObCoprod k)
data Witness HasInitialObject k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run data Witness HasInitialObject k = InitialW
data Witness CategoryOf k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run data Witness CategoryOf k = CategoryW
newtype Witness HasBinaryProducts k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run newtype Witness HasBinaryProducts k = ProductsW (WithTestObProd k)
data Witness HasTerminalObject k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run data Witness HasTerminalObject k = TerminalW
data Witness (Supplies CocommutativeComonoid) k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run data Witness (Supplies CocommutativeComonoid) k = CocommutativeComonoidSupplyW
data Witness (Supplies CommutativeMonoid) k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run data Witness (Supplies CommutativeMonoid) k = CommutativeMonoidSupplyW
data Witness (Supplies Comonoid) k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run data Witness (Supplies Comonoid) k = ComonoidSupplyW
data Witness (Supplies Monoid) k Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run data Witness (Supplies Monoid) k = MonoidSupplyW
data Witness (RepresentedBy csj p) k' Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run data Witness (RepresentedBy csj p) k' = RepresentedW (Witnesses csj j) (WithTestObRep j p)

data Witnesses (cs :: [Kind -> Constraint]) k where Source Github #

One Witness for each structure in cs, in the same order.

Constructors

WNil :: forall k. Witnesses ('[] :: [Kind -> Constraint]) k
(:&) :: forall (c :: Kind -> Constraint) k (cs1 :: [Kind -> Constraint]). Witness c k -> Witnesses cs1 k -> Witnesses (c ': cs1) k infixr 5

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

Look up the witness for the structure c.

Methods

witness :: Witnesses cs k -> Witness c k Source Github #

The witness for c in the list.

Instances

Instances details

HasWitness c (c ': cs) Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run Methods witness :: Witnesses (c ': cs) k -> Witness c k Source Github #
HasWitness c cs => HasWitness c (d ': cs) Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run Methods witness :: Witnesses (d ': cs) k -> Witness c k Source Github #

Interpreting with testable objects

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

Objects of k built from leaves by the structures' object formers. Checking a law interprets it here rather than in k itself: an object's Ob is then Tested, which recovers the TestOb of the object of k it stands for (Untest) from the Witnesses for the structures cs, supplied at run time.

The only constructor is the leaf. Compound objects use the free category's formers, which are open data families of any kind (**!, *!, DualF, ...), so a new structure brings its own former and its own Tested instance.

Constructors

TLeaf k

Instances

Instances details

(Testable k, Monoidal k, TestOb (Unit :: k)) => Tested (UnitF :: TESTED cs k) Source Github #

Instance details

(HasWitness Monoidal cs, Testable k, Monoidal k, Costrong (Tensor :: k -> (k, k) -> Type) p, TestOb (Unit :: k)) => Costrong (Tensor :: TESTED cs k -> (TESTED cs k, TESTED cs k) -> Type) (TestedP p :: TESTED cs k -> TESTED cs k -> Type) Source Github #	`coact` over the tensor of `p`, e.g. the trace of the category the objects stand for.
Instance details Defined in Proarrow.Testing.Laws.Run Methods coact :: forall (a :: TESTED cs k) (x :: TESTED cs k) (y :: TESTED cs k). (Ob a, Ob x, Ob y) => TestedP p (Act (Tensor :: TESTED cs k -> (TESTED cs k, TESTED cs k) -> Type) a x) (Act (Tensor :: TESTED cs k -> (TESTED cs k, TESTED cs k) -> Type) a y) -> TestedP p x y
(HasWitness Monoidal csj, HasWitness Monoidal csk, Testable j, Testable k, MonoidalProfunctor p, TestOb (Unit :: j), TestOb (Unit :: k)) => MonoidalProfunctor (TestedP p :: TESTED csk k -> TESTED csj j -> Type) Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run Methods one :: TestedP p (Unit :: TESTED csk k) (Unit :: TESTED csj j) () :: forall (x1 :: TESTED csk k) (x2 :: TESTED csj j) (y1 :: TESTED csk k) (y2 :: TESTED csj j). TestedP p x1 x2 -> TestedP p y1 y2 -> TestedP p (x1 y1) (x2 ** y2)
Profunctor p => Profunctor (TestedP p :: TESTED csk k -> TESTED csj j -> Type) Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run Methods dimap :: forall (c :: TESTED csk k) (a :: TESTED csk k) (b :: TESTED csj j) (d :: TESTED csj j). (c ~> a) -> (b ~> d) -> TestedP p a b -> TestedP p c d lmap :: forall (c :: TESTED csk k) (a :: TESTED csk k) (b :: TESTED csj j). (c ~> a) -> TestedP p a b -> TestedP p c b rmap :: forall (b :: TESTED csj j) (d :: TESTED csj j) (a :: TESTED csk k). (b ~> d) -> TestedP p a b -> TestedP p a d (\\) :: forall (a :: TESTED csk k) (b :: TESTED csj j) r. ((Ob a, Ob b) => r) -> TestedP p a b -> r
(HasWitness (RepresentedBy csj p) csk, Representable p) => Representable (TestedP p :: TESTED csk k -> TESTED csj j -> Type) Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run Methods index :: forall (a :: TESTED csk k) (b :: TESTED csj j). TestedP p a b -> a ~> ((TestedP p :: TESTED csk k -> TESTED csj j -> Type) % b) tabulate :: forall (b :: TESTED csj j) (a :: TESTED csk k). Ob b => (a ~> ((TestedP p :: TESTED csk k -> TESTED csj j -> Type) % b)) -> TestedP p a b repMap :: forall (a :: TESTED csj j) (b :: TESTED csj j). (a ~> b) -> ((TestedP p :: TESTED csk k -> TESTED csj j -> Type) % a) ~> ((TestedP p :: TESTED csk k -> TESTED csj j -> Type) % b) repUniv :: forall (a :: TESTED csj j). Ob a => TestedP p ((TestedP p :: TESTED csk k -> TESTED csj j -> Type) % a) a
Promonad p => Promonad (TestedP p :: TESTED cs k -> TESTED cs k -> Type) Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run Methods id :: forall (a :: TESTED cs k). Ob a => TestedP p a a (.) :: forall (b :: TESTED cs k) (c :: TESTED cs k) (a :: TESTED cs k). TestedP p b c -> TestedP p a b -> TestedP p a c
type (TestedP p :: TESTED csk k -> TESTED csj j -> Type) % (b :: TESTED csj j) Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run type (TestedP p :: TESTED csk k -> TESTED csj j -> Type) % (b :: TESTED csj j) = RepF p b :: TESTED csk k

RepresentedBy csj (p :: j +-> k) k' Source Github #
Instance details Defined in Proarrow.Testing.Laws.Run

Documentation

Witnesses

Instances

Instances

Interpreting with testable objects

Instances

Instances

Interpreting profunctors

Instances

Instances

Instances

Describing arrows