Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- prepropCommutative :: 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)) -> Property
- prepropEquivalent :: forall effs x r1 r2. (Eq x, Show x, Inject effs r1, Inject effs r2, Members effs effs) => (forall a. Sem r1 a -> IO a) -> (forall a. Sem r2 a -> IO a) -> (forall r. Proxy r -> Members effs r => Gen (Sem r x)) -> Property
- prepropLaw :: (Eq x, Show x) => Gen (Sem r a, Sem r a) -> (Sem r a -> IO x) -> Property
- arbitraryAction :: forall e r. ArbitraryAction (TypesOf e) e r => Gen (SomeAction e r)
- arbitraryActionOfType :: forall e a r. (GenericK (e (Sem r) a), GArbitraryK a (RepK (e (Sem 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
- class GArbitraryK (a :: Type) (f :: LoT Type -> 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 :: [(Type -> Type) -> Type -> Type]) a. Member e r => e (Sem r) a -> Sem r a
- deriveGenericK :: Name -> Q [Dec]
- class GenericK (f :: k)
Effect Properties
:: 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 |
-> 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.
:: forall effs x r1 r2. (Eq x, Show x, Inject effs r1, Inject effs r2, Members effs effs) | |
=> (forall a. Sem r1 a -> IO a) | The first interpreter for the effect stack.Pure effect stacks can
be lifted into |
-> (forall a. Sem r2 a -> IO 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 |
-> 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.
:: (Eq x, Show x) | |
=> Gen (Sem r a, Sem r a) | A generator for two equivalent programs. |
-> (Sem r a -> IO x) | 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.
Generators for Effects
:: forall e r. ArbitraryAction (TypesOf e) e r | |
=> Gen (SomeAction e r) |
Generate any action for effect e
.
arbitraryActionOfType Source #
Generate any action for effect e
that produces type a
.
arbitraryActionFromRow Source #
:: forall (effs :: EffectRow) r. ArbitraryEff effs r | |
=> Gen (SomeEff r) |
Generate any action from any effect in effs
.
arbitraryActionFromRowOfType Source #
:: 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 #
is some action for effect SomeAction
e re
in effect row r
.
SomeAction | |
|
Instances
Show (SomeAction e r) Source # | |
Defined in Polysemy.Check.Arbitrary.AnyEff showsPrec :: Int -> SomeAction e r -> ShowS # show :: SomeAction e r -> String # showList :: [SomeAction e r] -> ShowS # |
data SomeEff (r :: EffectRow) where Source #
is some action for some effect in the effect row SomeEff
rr
.
data SomeEffOfType (r :: EffectRow) a where Source #
is some action for some effect in the effect row SomeEff
rr
.
SomeEffOfType | |
|
Constraints for Generators of Effects
class GArbitraryK (a :: Type) (f :: LoT Type -> Type) Source #
Given
, this typeclass computes
generators for every well-typed constructor of GArbitraryK
a (RepK
(e m a))e m a
. It is capable of
building generators for GADTs.
Instances
GArbitraryK a (U1 :: LoT Type -> Type) Source # | |
Defined in Polysemy.Check.Arbitrary.Generic | |
GArbitraryK1 (Field b) => GArbitraryK a (Field b) Source # | |
Defined in Polysemy.Check.Arbitrary.Generic | |
GArbitraryK a (('Kon (b ~~ c) :: Atom Type Constraint) :=>: f) Source # | |
Defined in Polysemy.Check.Arbitrary.Generic | |
GArbitraryK a (('Kon (a ~~ b) :: Atom Type Constraint) :=>: f) Source # | |
Defined in Polysemy.Check.Arbitrary.Generic | |
GArbitraryK1 f => GArbitraryK a (('Kon (a ~~ a) :: Atom Type Constraint) :=>: f) Source # | |
Defined in Polysemy.Check.Arbitrary.Generic | |
(GArbitraryK a f, GArbitraryK a g) => GArbitraryK a (f :+: g) Source # | |
Defined in Polysemy.Check.Arbitrary.Generic | |
GArbitraryK1 (f :*: g) => GArbitraryK a (f :*: g) Source # | |
Defined in Polysemy.Check.Arbitrary.Generic | |
GArbitraryK a f => GArbitraryK a (M1 _1 _2 f) Source # | |
Defined in Polysemy.Check.Arbitrary.Generic |
class ArbitraryAction (as :: [Type]) (e :: Effect) (r :: EffectRow) Source #
lets you randomly generate an action
producing any type in ArbitraryAction
as e ras
from the effect e
.
Instances
ArbitraryAction ('[] :: [Type]) e r Source # | |
Defined in Polysemy.Check.Arbitrary.AnyEff genSomeAction :: [Gen (SomeAction e r)] Source # | |
(ArbitraryAction as e r, Eq a, Show a, Member e r, Show (e (Sem r) a), GenericK (e (Sem r) a), CoArbitrary a, GArbitraryK a (RepK (e (Sem r) a))) => ArbitraryAction (a ': as) e r Source # | |
Defined in Polysemy.Check.Arbitrary.AnyEff genSomeAction :: [Gen (SomeAction e r)] Source # |
class ArbitraryEff (es :: EffectRow) (r :: EffectRow) Source #
lets you randomly generate an action in any of
the effects ArbitraryEff
es res
.
Instances
ArbitraryEff ('[] :: [Effect]) r Source # | |
Defined in Polysemy.Check.Arbitrary.AnyEff genSomeEff :: [Gen (SomeEff r)] Source # | |
(ArbitraryEff es r, ArbitraryAction (TypesOf e) e r) => ArbitraryEff (e ': es) r Source # | |
Defined in Polysemy.Check.Arbitrary.AnyEff genSomeEff :: [Gen (SomeEff r)] Source # |
class ArbitraryEffOfType (a :: Type) (es :: EffectRow) (r :: EffectRow) Source #
lets you randomly generate an action in any of
the effects ArbitraryEffOfType
a es res
that produces type a
.
Instances
ArbitraryEffOfType a ('[] :: [Effect]) r Source # | |
Defined in Polysemy.Check.Arbitrary.AnyEff genSomeEffOfType :: [Gen (SomeEffOfType r a)] Source # | |
(Eq a, Show a, Show (e (Sem r) a), ArbitraryEffOfType a es r, GenericK (e (Sem r) a), GArbitraryK a (RepK (e (Sem r) a)), CoArbitrary a, Member e r) => ArbitraryEffOfType a (e ': es) r Source # | |
Defined in Polysemy.Check.Arbitrary.AnyEff genSomeEffOfType :: [Gen (SomeEffOfType r a)] Source # |
Re-exports
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)