polysemy-check-0.5.0.0: QuickCheck for Polysemy

Polysemy.Check

Synopsis

# Effect Properties

Arguments

 :: forall e1 e2 r f. (forall a. Show a => Show (f a), forall a. Eq a => Eq (f a)) => (ArbitraryEff r r, ArbitraryEff '[e1] r, ArbitraryEff '[e2] r) => (forall a. Sem r a -> IO (f a)) An interpreter for the effect stack down to IO. Pure effect stacks can be lifted into IO via pure after the final run. -> Property

Prove that two effects are commutative (a la Reasoning about effect interaction by fusion) under the given interpreter.

Humans naturally expect that disparate effects do not interact, thus commutativity is an important property for reasoning about the correctness of your program.

For example,

prepropCommutative @(State Int) @Trace @EffStack runEffStack


will interleave random State Int and Trace actions, within a bigger context of EffStack actions. The resulting Property will fail if permuting the State Int and Trace effects changes the outcome of the entire computation.

Arguments

 :: forall effs x r1 r2 f. (forall a. Show a => Show (f a), forall a. Eq a => Eq (f a)) => (Eq x, Show x, Inject effs r1, Inject effs r2, Members effs effs) => (forall a. Sem r1 a -> IO (f a)) The first interpreter for the effect stack.Pure effect stacks can be lifted into IO via pure after the final run. -> (forall a. Sem r2 a -> IO (f a)) The second interpreter to prove equivalence for. -> (forall r. Proxy r -> Members effs r => Gen (Sem r x)) A generator producing arbitrary programs in r. The property will hold true if both interpreters produce the same output for every program generated by this. -> Property

Prove that two interpreters are equivalent. For the given generator, this property ensures that the two interpreters give the same result for every arbitrary program.

Arguments

 :: forall effs r a f. (forall z. Eq z => Eq (f z), forall z. Show z => Show (f z)) => (Eq a, Show a, ArbitraryEff effs r) => Gen (Sem r a, Sem r a) A generator for two equivalent programs. -> (forall z. Sem r (a, z) -> IO (f (a, z))) An interpreter for the effect stack down to IO. Pure effect stacks can be lifted into IO via pure after the final run. -> Property

Prove that two programs in r are equivalent under a given interpretation. This is useful for proving laws about particular effects (or stacks of effects).

For example, any lawful interpretation of State must satisfy the put s1 >> put s2 = put s2 law.

# Generators for Effects

Arguments

 :: forall e r. ArbitraryAction (TypesOf e) e r => Gen (SomeAction e r)

Generate any action for effect e.

Arguments

 :: forall e a r. (GenericK e, GArbitraryK e (RepK e) r a) => Gen (e (Sem r) a)

Generate any action for effect e that produces type a.

Arguments

 :: forall (effs :: EffectRow) r. ArbitraryEff effs r => Gen (SomeEff r)

Generate any action from any effect in effs.

Arguments

 :: forall (effs :: EffectRow) r a. ArbitraryEffOfType a effs r => Gen (SomeEffOfType r a)

Generate any action from any effect in effs that produces type a.

# Types for Generators for Effects

data SomeAction e (r :: EffectRow) where Source #

SomeAction e r is some action for effect e in effect row r.

Constructors

 SomeAction Fields:: (Member e r, Eq a, Show a, CoArbitrary a, Show (e (Sem r) a)) => e (Sem r) a -> SomeAction e r

#### Instances

Instances details
 Show (SomeAction e r) Source # Instance detailsDefined in Polysemy.Check.Arbitrary MethodsshowsPrec :: Int -> SomeAction e r -> ShowS #show :: SomeAction e r -> String #showList :: [SomeAction e r] -> ShowS #

data SomeEff (r :: EffectRow) where Source #

SomeEff r is some action for some effect in the effect row r.

Constructors

 SomeEff Fields:: (Member e r, Eq a, Show a, CoArbitrary a, Show (e (Sem r) a)) => e (Sem r) a -> SomeEff r

#### Instances

Instances details
 Show (SomeEff r) Source # Instance detailsDefined in Polysemy.Check.Arbitrary MethodsshowsPrec :: Int -> SomeEff r -> ShowS #show :: SomeEff r -> String #showList :: [SomeEff r] -> ShowS #

data SomeEffOfType (r :: EffectRow) a where Source #

SomeEff r is some action for some effect in the effect row r.

Constructors

 SomeEffOfType Fields:: (Member e r, Eq a, Show a, CoArbitrary a, Show (e (Sem r) a)) => e (Sem r) a -> SomeEffOfType r a

#### Instances

Instances details
 Show (SomeEffOfType r a) Source # Instance detailsDefined in Polysemy.Check.Arbitrary MethodsshowsPrec :: Int -> SomeEffOfType r a -> ShowS #show :: SomeEffOfType r a -> String #showList :: [SomeEffOfType r a] -> ShowS #

# Support for Existential Types

data family ExistentialFor (e :: Effect) Source #

Data family for the instantiation of existential variables. If you want to check properties for an effect e that contains an existential type, the synthesized Arbitrary instance will instantiate all of e's existential types at ExistentialFor e.

ExistentialFor e must have instances for every dictionary required by e, and will likely require an Arbitrary instance.

# Constraints for Generators of Effects

class GArbitraryK (e :: Effect) (f :: LoT Effect -> Type) (r :: EffectRow) (a :: Type) Source #

Given GArbitraryK e (RepK e) r a, this typeclass computes generators for every well-typed constructor of e (Sem r) a. It is capable of building generators for GADTs.

Minimal complete definition

garbitraryk

#### Instances

Instances details
 GArbitraryK e (U1 :: LoT Effect -> Type) r a Source # Instance detailsDefined in Polysemy.Check.Arbitrary Methodsgarbitraryk :: [Gen (U1 (LoT2 (Sem r) a))] Source # Arbitrary (Interpret f (LoT2 (Sem r) a)) => GArbitraryK e (Field f) r a Source # Instance detailsDefined in Polysemy.Check.Arbitrary Methodsgarbitraryk :: [Gen (Field f (LoT2 (Sem r) a))] Source # GArbitraryK e (((('Kon ((~~) :: Type -> k1 -> Constraint) :: Atom ((Type -> Type) -> Type -> Type) (Type -> k1 -> Constraint)) :@: (Var1 :: Atom ((Type -> Type) -> Type -> Type) Type)) :@: ('Kon b :: Atom ((Type -> Type) -> Type -> Type) k1)) :=>: f) r a Source # Instance detailsDefined in Polysemy.Check.Arbitrary Methodsgarbitraryk :: [Gen (((('Kon (~~) :@: Var1) :@: 'Kon b) :=>: f) (LoT2 (Sem r) a))] Source # GArbitraryK e ((('Kon ((~~) b :: Type -> Constraint) :: Atom ((Type -> Type) -> Type -> Type) (Type -> Constraint)) :@: (Var1 :: Atom ((Type -> Type) -> Type -> Type) Type)) :=>: f) r a Source # Instance detailsDefined in Polysemy.Check.Arbitrary Methodsgarbitraryk :: [Gen ((('Kon ((~~) b) :@: Var1) :=>: f) (LoT2 (Sem r) a))] Source # GArbitraryK e f r a => GArbitraryK e (((('Kon ((~~) :: Type -> Type -> Constraint) :: Atom ((Type -> Type) -> Type -> Type) (Type -> Type -> Constraint)) :@: (Var1 :: Atom ((Type -> Type) -> Type -> Type) Type)) :@: ('Kon a :: Atom ((Type -> Type) -> Type -> Type) Type)) :=>: f) r a Source # Instance detailsDefined in Polysemy.Check.Arbitrary Methodsgarbitraryk :: [Gen (((('Kon (~~) :@: Var1) :@: 'Kon a) :=>: f) (LoT2 (Sem r) a))] Source # GArbitraryK e f r a => GArbitraryK e ((('Kon ((~~) a :: Type -> Constraint) :: Atom ((Type -> Type) -> Type -> Type) (Type -> Constraint)) :@: (Var1 :: Atom ((Type -> Type) -> Type -> Type) Type)) :=>: f) r a Source # Instance detailsDefined in Polysemy.Check.Arbitrary Methodsgarbitraryk :: [Gen ((('Kon ((~~) a) :@: Var1) :=>: f) (LoT2 (Sem r) a))] Source # GArbitraryK e (c1 :=>: (c2 :=>: f)) r a => GArbitraryK e ((c1 :&: c2) :=>: f) r a Source # Instance detailsDefined in Polysemy.Check.Arbitrary Methodsgarbitraryk :: [Gen (((c1 :&: c2) :=>: f) (LoT2 (Sem r) a))] Source # (Interpret c (LoT2 (Sem r) a), GArbitraryK e f r a) => GArbitraryK e (c :=>: f) r a Source # Instance detailsDefined in Polysemy.Check.Arbitrary Methodsgarbitraryk :: [Gen ((c :=>: f) (LoT2 (Sem r) a))] Source # (GArbitraryK e f r a, GArbitraryK e g r a) => GArbitraryK e (f :+: g) r a Source # Instance detailsDefined in Polysemy.Check.Arbitrary Methodsgarbitraryk :: [Gen ((f :+: g) (LoT2 (Sem r) a))] Source # (GArbitraryK e (SubstRep f (ExistentialFor e)) r a, SubstRep' f (ExistentialFor e) (LoT2 (Sem r) a)) => GArbitraryK e (Exists Type f) r a Source # Instance detailsDefined in Polysemy.Check.Arbitrary Methodsgarbitraryk :: [Gen (Exists Type f (LoT2 (Sem r) a))] Source # (GArbitraryK e f r a, GArbitraryK e g r a) => GArbitraryK e (f :*: g) r a Source # Instance detailsDefined in Polysemy.Check.Arbitrary Methodsgarbitraryk :: [Gen ((f :*: g) (LoT2 (Sem r) a))] Source # GArbitraryK e f r a => GArbitraryK e (M1 _1 _2 f) r a Source # Instance detailsDefined in Polysemy.Check.Arbitrary Methodsgarbitraryk :: [Gen (M1 _1 _2 f (LoT2 (Sem r) a))] Source #

class ArbitraryAction (as :: [Type]) (e :: Effect) (r :: EffectRow) Source #

ArbitraryAction as e r lets you randomly generate an action producing any type in as from the effect e.

Minimal complete definition

genSomeAction

#### Instances

Instances details
 ArbitraryAction ('[] :: [Type]) e r Source # Instance detailsDefined in Polysemy.Check.Arbitrary MethodsgenSomeAction :: [Gen (SomeAction e r)] Source # (ArbitraryAction as e r, Eq a, Show a, Member e r, Show (e (Sem r) a), GenericK e, CoArbitrary a, GArbitraryK e (RepK e) r a) => ArbitraryAction (a ': as) e r Source # Instance detailsDefined in Polysemy.Check.Arbitrary MethodsgenSomeAction :: [Gen (SomeAction e r)] Source #

class ArbitraryEff (es :: EffectRow) (r :: EffectRow) Source #

ArbitraryEff es r lets you randomly generate an action in any of the effects es.

Minimal complete definition

genSomeEff

#### Instances

Instances details
 ArbitraryEff ('[] :: [Effect]) r Source # Instance detailsDefined in Polysemy.Check.Arbitrary MethodsgenSomeEff :: [Gen (SomeEff r)] Source # (ArbitraryEff es r, ArbitraryAction (TypesOf e) e r) => ArbitraryEff (e ': es) r Source # Instance detailsDefined in Polysemy.Check.Arbitrary MethodsgenSomeEff :: [Gen (SomeEff r)] Source #

class ArbitraryEffOfType (a :: Type) (es :: EffectRow) (r :: EffectRow) Source #

ArbitraryEffOfType a es r lets you randomly generate an action in any of the effects es that produces type a.

Minimal complete definition

genSomeEffOfType

#### Instances

Instances details
 ArbitraryEffOfType a ('[] :: [Effect]) r Source # Instance detailsDefined in Polysemy.Check.Arbitrary MethodsgenSomeEffOfType :: [Gen (SomeEffOfType r a)] Source # (Eq a, Show a, Show (e (Sem r) a), ArbitraryEffOfType a es r, GenericK e, GArbitraryK e (RepK e) r a, CoArbitrary a, Member e r) => ArbitraryEffOfType a (e ': es) r Source # Instance detailsDefined in Polysemy.Check.Arbitrary MethodsgenSomeEffOfType :: [Gen (SomeEffOfType r a)] Source #

type TypesOf (e :: Effect) = GTypesOf (RepK e) Source #

TypesOf e is a list of every type that can be bound via e's actions.

For example, given:

data MyEffect m a where
Foo :: MyEffect m Int
Blah :: Bool -> MyEffect m String


the result of TypesOf MyEffect is '[Int, String].

# Re-exports

send :: forall e (r :: [(Type -> Type) -> Type -> Type]) a. Member e r => e (Sem r) a -> Sem r a #

Embed an effect into a Sem. This is used primarily via makeSem to implement smart constructors.

deriveGenericK :: Name -> Q [Dec] #

Given the Name of a data type (or, the Name of a constructor belonging to a data type), generate GenericK instances for that data type. You will likely need to enable most of these language extensions in order for GHC to accept the generated code:

• DataKinds
• EmptyCase (if using an empty data type)
• FlexibleInstances
• MultiParamTypeClasses
• PolyKinds (if using a poly-kinded data type)
• TemplateHaskell
• TypeFamilies

class GenericK (f :: k) #

Representable types of any kind. Examples:

instance GenericK Int
instance GenericK []
instance GenericK Either
instance GenericK (Either a)
instance GenericK (Either a b)

#### Instances

Instances details