| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Polysemy.Check
Synopsis
- prepropCommutative :: forall effs1 effs2 r f. (forall a. Show a => Show (f a), forall a. Eq a => Eq (f a)) => (ArbitraryEff r r, ArbitraryEff effs1 r, ArbitraryEff effs2 r) => (forall a. Sem r a -> IO (f a)) -> Property
- prepropAllCommutative :: (AllCommutative effs r, forall a. Show a => Show (f a), forall a. Eq a => Eq (f a), Members effs r) => (forall a. Sem r a -> IO (f a)) -> [Property]
- prepropEquivalent :: forall effs r1 r2 f. (forall a. Show a => Show (f a), forall a. Eq a => Eq (f a)) => (Inject effs r1, Inject effs r2, Arbitrary (Sem effs Int)) => (forall a. Sem r1 a -> IO (f a)) -> (forall a. Sem r2 a -> IO (f a)) -> Property
- prepropLaw :: forall effs x r a f. (forall z. Eq z => Eq (f z), forall z. Show z => Show (f z)) => (Eq a, Show a, Functor f, ArbitraryEff effs r, Eq x, Show x) => Gen (Law r x a) -> Maybe (f a -> String) -> (forall z. Sem r (a, z) -> IO (f (a, z))) -> Property
- data Law r z a = Law {
- lawLhs :: Sem r a
- lawRhs :: Sem r a
- lawPrelude :: [Sem r ()]
- lawPostlude :: [Sem r z]
- simpleLaw :: Sem r a -> Sem r a -> Law r () a
- arbitraryAction :: forall e r. ArbitraryAction (TypesOf e) e r => Gen (SomeAction e r)
- arbitraryActionOfType :: forall e a r. (GenericK e, GArbitraryK e (RepK e) r a) => Gen (e (Sem r) a)
- arbitraryActionFromRow :: forall (effs :: EffectRow) r. ArbitraryEff effs r => Gen (SomeEff r)
- arbitraryActionFromRowOfType :: forall (effs :: EffectRow) r a. ArbitraryEffOfType a effs r => Gen (SomeEffOfType r a)
- data SomeAction e (r :: EffectRow) where
- SomeAction :: (Member e r, Eq a, Show a, CoArbitrary a, Show (e (Sem r) a)) => e (Sem r) a -> SomeAction e r
- data SomeEff (r :: EffectRow) where
- data SomeEffOfType (r :: EffectRow) a where
- SomeEffOfType :: (Member e r, Eq a, Show a, CoArbitrary a, Show (e (Sem r) a)) => e (Sem r) a -> SomeEffOfType r a
- constructorLabel :: Data a => a -> String
- data family ExistentialFor (e :: Effect)
- class GArbitraryK (e :: Effect) (f :: LoT Effect -> Type) (r :: EffectRow) (a :: Type)
- class ArbitraryAction (as :: [Type]) (e :: Effect) (r :: EffectRow)
- class ArbitraryEff (es :: EffectRow) (r :: EffectRow)
- class ArbitraryEffOfType (a :: Type) (es :: EffectRow) (r :: EffectRow)
- type TypesOf (e :: Effect) = GTypesOf (RepK e)
- send :: forall e (r :: EffectRow) a. Member e r => e (Sem r) a -> Sem r a
- deriveGenericK :: Name -> Q [Dec]
- class GenericK (f :: k)
Effect Properties
Arguments
| :: forall effs1 effs2 r f. (forall a. Show a => Show (f a), forall a. Eq a => Eq (f a)) | |
| => (ArbitraryEff r r, ArbitraryEff effs1 r, ArbitraryEff effs2 r) | |
| => (forall a. Sem r a -> IO (f a)) | An interpreter for the effect stack down to |
| -> 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.
prepropAllCommutative :: (AllCommutative effs r, forall a. Show a => Show (f a), forall a. Eq a => Eq (f a), Members effs r) => (forall a. Sem r a -> IO (f a)) -> [Property] Source #
prepropAllCommutative @effs @r interpreterprepropCommutative for every tail in effs. In essence, this ensures
that every effect in effs commutes with every other one.
Arguments
| :: forall effs r1 r2 f. (forall a. Show a => Show (f a), forall a. Eq a => Eq (f a)) | |
| => (Inject effs r1, Inject effs r2, Arbitrary (Sem effs Int)) | |
| => (forall a. Sem r1 a -> IO (f a)) | The first interpreter for the effect stack.Pure effect stacks can
be lifted into |
| -> (forall a. Sem r2 a -> IO (f a)) | The second interpreter to prove equivalence for. |
| -> Property |
Prove that two interpreters are equivalent. This property ensures that the two interpreters give the same result for every arbitrary program.
Arguments
| :: forall effs x r a f. (forall z. Eq z => Eq (f z), forall z. Show z => Show (f z)) | |
| => (Eq a, Show a, Functor f, ArbitraryEff effs r, Eq x, Show x) | |
| => Gen (Law r x a) | A generator for two equivalent programs. |
| -> Maybe (f a -> String) | How to label the results for QuickCheck coverage. |
| -> (forall z. Sem r (a, z) -> IO (f (a, z))) | An interpreter for the effect stack down to |
| -> 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.
Law Constructors
Data structure containing programs that should be equal, and under which circumstances.
Since: 0.9.0.0
Constructors
| Law | |
Fields
| |
simpleLaw :: Sem r a -> Sem r a -> Law r () a Source #
Like Law, but for the common case when you don't need a custom prelude
or postlude.
Since: 0.9.0.0
Generators for Effects
Arguments
| :: forall e r. ArbitraryAction (TypesOf e) e r | |
| => Gen (SomeAction e r) |
Generate any action for effect e.
arbitraryActionOfType Source #
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.
arbitraryActionFromRow Source #
Arguments
| :: forall (effs :: EffectRow) r. ArbitraryEff effs r | |
| => Gen (SomeEff r) |
Generate any action from any effect in effs.
arbitraryActionFromRowOfType Source #
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 re in effect row r.
Constructors
| SomeAction | |
Fields
| |
Instances
| Show (SomeAction e r) Source # | |
Defined in Polysemy.Check.Arbitrary Methods showsPrec :: Int -> SomeAction e r -> ShowS # show :: SomeAction e r -> String # showList :: [SomeAction e r] -> ShowS # | |
data SomeEff (r :: EffectRow) where Source #
SomeEff rr.
Constructors
| SomeEff | |
data SomeEffOfType (r :: EffectRow) a where Source #
SomeEff rr.
Constructors
| SomeEffOfType | |
Fields
| |
Instances
| Show (SomeEffOfType r a) Source # | |
Defined in Polysemy.Check.Arbitrary Methods showsPrec :: Int -> SomeEffOfType r a -> ShowS # show :: SomeEffOfType r a -> String # showList :: [SomeEffOfType r a] -> ShowS # | |
Common labeling functions
constructorLabel :: Data a => a -> String Source #
Label an example with its data constructor.
Since: 0.9.0.0
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 ee, 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 ae (Sem r) a. It is capable
of building generators for GADTs.
Minimal complete definition
Instances
class ArbitraryAction (as :: [Type]) (e :: Effect) (r :: EffectRow) Source #
ArbitraryAction as e ras from the effect e.
Minimal complete definition
Instances
| ArbitraryAction ('[] :: [Type]) e r Source # | |
Defined in Polysemy.Check.Arbitrary Methods genSomeAction :: [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 # | |
Defined in Polysemy.Check.Arbitrary Methods genSomeAction :: [Gen (SomeAction e r)] Source # | |
class ArbitraryEff (es :: EffectRow) (r :: EffectRow) Source #
ArbitraryEff es res.
Minimal complete definition
Instances
| ArbitraryEff ('[] :: [Effect]) r Source # | |
Defined in Polysemy.Check.Arbitrary Methods genSomeEff :: [Gen (SomeEff r)] Source # | |
| (ArbitraryEff es r, ArbitraryAction (TypesOf e) e r) => ArbitraryEff (e ': es) r Source # | |
Defined in Polysemy.Check.Arbitrary Methods genSomeEff :: [Gen (SomeEff r)] Source # | |
class ArbitraryEffOfType (a :: Type) (es :: EffectRow) (r :: EffectRow) Source #
ArbitraryEffOfType a es res that produces type a.
Minimal complete definition
Instances
| ArbitraryEffOfType a ('[] :: [Effect]) r Source # | |
Defined in Polysemy.Check.Arbitrary Methods genSomeEffOfType :: [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 # | |
Defined in Polysemy.Check.Arbitrary Methods genSomeEffOfType :: [Gen (SomeEffOfType r a)] Source # | |
Re-exports
send :: forall e (r :: EffectRow) a. Member e r => e (Sem r) a -> Sem r a #
Execute an action of an effect.
This is primarily used to create methods for actions of effects:
data FooBar m a where Foo :: String -> m a -> FooBar m a Bar :: FooBar m Int foo :: Member FooBar r => String -> Sem r a -> Sem r a foo s m = send (Foo s m) bar :: Member FooBar r => Sem r Int bar = send Bar
makeSem allows you to eliminate this boilerplate.
@since TODO
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
Representable types of any kind. Examples:
instance GenericK Int instance GenericK [] instance GenericK Either instance GenericK (Either a) instance GenericK (Either a b)