packages feed

polysemy-check (empty) → 0.1.0.0

raw patch · 16 files changed

+929/−0 lines, 16 filesdep +QuickCheckdep +basedep +containerssetup-changed

Dependencies added: QuickCheck, base, containers, hspec, kind-generics, kind-generics-th, polysemy, polysemy-check, polysemy-plugin

Files

+ ChangeLog.md view
@@ -0,0 +1,8 @@+# Changelog for polysemy-check++## v0.1.0.0 (2021-10-08)++- Released!++## Unreleased changes+
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Sandy Maguire (c) 2021++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Sandy Maguire nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,52 @@+# polysemy-check++[![Hackage](https://img.shields.io/hackage/v/polysemy-check.svg?logo=haskell&label=polysemy-check)](https://hackage.haskell.org/package/polysemy-check)++## Dedication++> Success is most often achieved by those who don't know that failure is+> inevitable.+>+> --Coco Chanel++## Overview++`polysemy-check` is a little package that integrates+[`polysemy`](https://hackage.haskell.org/package/polysemy) with+[`QuickCheck`](https://hackage.haskell.org/package/QuickCheck). It allows you to+prove the equivalence of effects (see `prepropLaw`), the equivalence of+interpreters (`prepropEquivalent`), and that two effects don't affect one+another (`prepropCommutative`). These three things are about the only problems+you could possibly run into with Polysemy --- and now you won't.++In addition `polysemy-check` provides lots of machinery to help avoid+boilerplate, such as free `Arbitrary` instances for effects.+++## Usage++`polysemy-check` requires a `Show` and `GenericK` instance for every effect+you'd like to run tests over.++```haskell+{-# LANGUAGE TemplateHaskell #-}++import Polysemy+import Polysemy.Check++data Stack m a where+  Push :: Int -> Stack m ()+  Pop  :: Stack m (Maybe Int)+  Size :: Stack m Int++deriving instance Show (Stack m a)+makeSem ''Stack+deriveGenericK ''Stack+```+++## Examples++Check the [test+suite](https://github.com/polysemy-research/polysemy-check/tree/master/test).+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ polysemy-check.cabal view
@@ -0,0 +1,109 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.34.4.+--+-- see: https://github.com/sol/hpack++name:           polysemy-check+version:        0.1.0.0+synopsis:       QuickCheck for Polysemy+description:    Please see the README on GitHub at <https://github.com/polysemy-research/polysemy-check#readme>+category:       Polysemy+homepage:       https://github.com/polysemy-research/polysemy-check#readme+bug-reports:    https://github.com/polysemy-research/polysemy-check/issues+author:         Sandy Maguire+maintainer:     sandy@sandymaguire.me+copyright:      Sandy Maguire+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    ChangeLog.md++source-repository head+  type: git+  location: https://github.com/polysemy-research/polysemy-check++library+  exposed-modules:+      Polysemy.Check+      Polysemy.Check.Arbitrary+      Polysemy.Check.Arbitrary.AnyEff+      Polysemy.Check.Arbitrary.Generic+      Polysemy.Check.Orphans+      Polysemy.Internal.Union.Inject+  other-modules:+      Paths_polysemy_check+  hs-source-dirs:+      src+  default-extensions:+      AllowAmbiguousTypes+      ConstraintKinds+      DataKinds+      FlexibleContexts+      FlexibleInstances+      GADTs+      LambdaCase+      MultiParamTypeClasses+      PolyKinds+      RankNTypes+      ScopedTypeVariables+      StandaloneDeriving+      TemplateHaskell+      TypeApplications+      TypeFamilies+      TypeOperators+      UndecidableInstances+  ghc-options: -Wall+  build-depends:+      QuickCheck+    , base >=4.7 && <5+    , containers+    , kind-generics+    , kind-generics-th+    , polysemy+  default-language: Haskell2010++test-suite test+  type: exitcode-stdio-1.0+  main-is: Main.hs+  other-modules:+      CommutativeSpec+      EquivSpec+      LawSpec+      Paths_polysemy_check+  hs-source-dirs:+      test+  default-extensions:+      AllowAmbiguousTypes+      ConstraintKinds+      DataKinds+      FlexibleContexts+      FlexibleInstances+      GADTs+      LambdaCase+      MultiParamTypeClasses+      PolyKinds+      RankNTypes+      ScopedTypeVariables+      StandaloneDeriving+      TemplateHaskell+      TypeApplications+      TypeFamilies+      TypeOperators+      UndecidableInstances+  ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N+  build-tool-depends:+      hspec-discover:hspec-discover >=2.0+  build-depends:+      QuickCheck+    , base >=4.7 && <5+    , containers+    , hspec+    , kind-generics+    , kind-generics-th+    , polysemy+    , polysemy-check+    , polysemy-plugin+  default-language: Haskell2010
+ src/Polysemy/Check.hs view
@@ -0,0 +1,157 @@+{-# LANGUAGE QuantifiedConstraints #-}+module Polysemy.Check+  ( -- * Effect Properties+    prepropCommutative+  , prepropEquivalent+  , prepropLaw++    -- * Generators for Effects+  , arbitraryAction+  , arbitraryActionOfType+  , arbitraryActionFromRow+  , arbitraryActionFromRowOfType++    -- * Types for Generators for Effects+  , SomeAction (..)+  , SomeEff (..)+  , SomeEffOfType (..)++    -- * Constraints for Generators of Effects+  , GArbitraryK+  , ArbitraryAction+  , ArbitraryEff+  , ArbitraryEffOfType+  , TypesOf++    -- * Re-exports+  , send+  , deriveGenericK+  , GenericK+  ) where++import Generics.Kind (GenericK)+import Generics.Kind.TH (deriveGenericK)+import Polysemy+import Polysemy.Check.Arbitrary+import Polysemy.Check.Arbitrary.AnyEff+import Polysemy.Check.Arbitrary.Generic (GArbitraryK)+import Polysemy.Check.Orphans ()+import Polysemy.Internal+import Polysemy.Internal.Union.Inject (Inject, inject)+import Test.QuickCheck+++------------------------------------------------------------------------------+-- | Prove that two effects are commutative (a la+-- <https://dl.acm.org/doi/10.1145/3473578 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.+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))+       -- ^ An interpreter for the effect stack down to 'IO'. Pure effect+       -- stacks can be lifted into 'IO' via 'pure' after the final 'run'.+    -> Property+prepropCommutative lower = property @(Gen Property) $ do+  SomeEff m1 <- arbitraryActionFromRow @r @r+  SomeEff e1 <- arbitraryActionFromRow @'[e1] @r+  SomeEff e2 <- arbitraryActionFromRow @'[e2] @r+  SomeEff m2 <- arbitraryActionFromRow @r @r+  pure $+    counterexample "Effects are not commutative!" $+    counterexample "" $+    counterexample ("k1  = " <> show m1) $+    counterexample ("e1 = " <> show e1) $+    counterexample ("e2 = " <> show e2) $+    counterexample ("k2  = " <> show m2) $+    counterexample "" $+    counterexample "(e1 >> e2 >> k) /= (e2 >> e1 >> k)" $+      ioProperty $ do+        r1 <- lower $ send m1 >> send e1 >> send e2 >> send m2+        r2 <- lower $ send m1 >> send e2 >> send e1 >> send m2+        pure $ r1 === r2+++------------------------------------------------------------------------------+-- | 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.+prepropLaw+    :: (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 'IO'. Pure effect+       -- stacks can be lifted into 'IO' via 'pure' after the final 'run'.+    -> Property+prepropLaw g lower = property $ do+  (m1, m2) <- g+  pure $ ioProperty $ do+    a1 <- lower m1+    a2 <- lower m2+    pure $ a1 === a2+++------------------------------------------------------------------------------+-- | 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.+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)+       -- ^ 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 a)+       -- ^ The second interpreter to prove equivalence for.+    -> (forall 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+prepropEquivalent int1 int2 mksem = property $ do+  SomeSem sem <- liftGen @effs @x mksem+  pure $ ioProperty $ do+    a1 <- int1 sem+    a2 <- int2 sem+    pure $ a1 === a2+++newtype SomeSem effs a = SomeSem+  { _getSomeSem :: forall r. (Inject effs r) => Sem r a+  }+++liftGen+    :: forall effs a+     . Members effs effs+    => (forall r. Members effs r => Gen (Sem r a))+    -> Gen (SomeSem effs a)+liftGen g = do+  a <- g @effs+  pure $ SomeSem $ inject a+
+ src/Polysemy/Check/Arbitrary.hs view
@@ -0,0 +1,48 @@+module Polysemy.Check.Arbitrary where++import Generics.Kind+import Polysemy+import Polysemy.Check.Arbitrary.AnyEff+import Polysemy.Check.Arbitrary.Generic+import Test.QuickCheck+++------------------------------------------------------------------------------+-- | Generate any action for effect @e@.+arbitraryAction+    :: forall e r+     . ArbitraryAction (TypesOf e) e r+    => Gen (SomeAction e r)+       -- ^+arbitraryAction = oneof $ genSomeAction @(TypesOf e) @e @r+++------------------------------------------------------------------------------+-- | Generate any action for effect @e@ that produces type @a@.+arbitraryActionOfType+    :: forall e a r+     . (GenericK (e (Sem r) a), GArbitraryK a (RepK (e (Sem r) a)))+    => Gen (e (Sem r) a)+       -- ^+arbitraryActionOfType = genEff @e @a @(Sem r)+++------------------------------------------------------------------------------+-- | Generate any action from any effect in @effs@.+arbitraryActionFromRow+    :: forall (effs :: EffectRow) r+     . ArbitraryEff effs r+    => Gen (SomeEff r)+       -- ^+arbitraryActionFromRow = oneof $ genSomeEff @effs @r+++------------------------------------------------------------------------------+-- | Generate any action from any effect in @effs@ that produces type @a@.+arbitraryActionFromRowOfType+    :: forall (effs :: EffectRow) r a+     . ArbitraryEffOfType a effs r+    => Gen (SomeEffOfType r a)+       -- ^+arbitraryActionFromRowOfType = oneof $ genSomeEffOfType @a @effs @r+
+ src/Polysemy/Check/Arbitrary/AnyEff.hs view
@@ -0,0 +1,149 @@+module Polysemy.Check.Arbitrary.AnyEff where++import Data.Kind (Type, Constraint)+import GHC.Exts (type (~~))+import Generics.Kind+import Polysemy+import Polysemy.Internal+import {-# SOURCE #-} Polysemy.Check.Arbitrary.Generic+import Test.QuickCheck+++------------------------------------------------------------------------------+-- | Helper function for implementing 'GTypesOf'+type family GTypesOf (f :: LoT Effect -> Type) :: [Type] where+  GTypesOf (M1 _1 _2 f) = GTypesOf f+  GTypesOf (f :+: g) = Append (GTypesOf f) (GTypesOf g)+  GTypesOf (('Kon (~~) ':@: Var1 ':@: 'Kon a) :=>: f) = '[a]+  GTypesOf (('Kon ((~~) a) ':@: Var1) :=>: f) = '[a]+  -- Otherwise, we don't have any constraints on @a@, so we can instantiate it+  -- how we please. Just assume ().+  GTypesOf _1 = '[()]+++------------------------------------------------------------------------------+-- | @'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]@.+type TypesOf (e :: Effect) = GTypesOf (RepK e)+++------------------------------------------------------------------------------+-- | A type family that expands to a 'GArbitraryK' constaint for every type in+-- the first list.+type family ArbitraryForAll (as :: [Type]) (m :: Type -> Type) :: Constraint where+  ArbitraryForAll '[] f = ()+  ArbitraryForAll (a ': as) f = (Eq a, Show a, GArbitraryK a (RepK (f a)), ArbitraryForAll as f)+++------------------------------------------------------------------------------+-- | @'SomeAction' e r@ is some action for effect @e@ in effect row @r@.+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+         -- ^++instance Show (SomeAction e r) where+  show (SomeAction ema) = show ema++instance Show (SomeEff r) where+  show (SomeEff sse) = show sse+++------------------------------------------------------------------------------+-- | @'SomeEff' r@ is some action for some effect in the effect row @r@.+data SomeEff (r :: EffectRow) where+  SomeEff+      :: (Member e r, Eq a, Show a, CoArbitrary a, Show (e (Sem r) a))+      => e (Sem r) a+         -- ^+      -> SomeEff r+         -- ^++------------------------------------------------------------------------------+-- | @'SomeEff' r@ is some action for some effect in the effect row @r@.+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+         -- ^+++------------------------------------------------------------------------------+-- | @'ArbitraryEff' es r@ lets you randomly generate an action in any of+-- the effects @es@.+class ArbitraryEff (es :: EffectRow) (r :: EffectRow) where+  genSomeEff :: [Gen (SomeEff r)]++instance ArbitraryEff '[] r where+  genSomeEff = []++instance+    (ArbitraryEff es r, ArbitraryAction (TypesOf e) e r)+    => ArbitraryEff (e ': es) r+    where+  genSomeEff = fmap (fmap (\(SomeAction e) -> SomeEff e)) (genSomeAction @(TypesOf e) @e @r)+             <> genSomeEff @es @r++------------------------------------------------------------------------------+-- | @'ArbitraryEffOfType' a es r@ lets you randomly generate an action in any of+-- the effects @es@ that produces type @a@.+class ArbitraryEffOfType (a :: Type) (es :: EffectRow) (r :: EffectRow) where+  genSomeEffOfType :: [Gen (SomeEffOfType r a)]++instance ArbitraryEffOfType a '[] r where+  genSomeEffOfType = []++instance+    ( 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+    where+  genSomeEffOfType+    = fmap SomeEffOfType (genEff @e @a @(Sem r))+    : genSomeEffOfType @a @es @r+++------------------------------------------------------------------------------+-- | @'ArbitraryAction' as e r@ lets you randomly generate an action+-- producing any type in @as@ from the effect @e@.+class ArbitraryAction (as :: [Type]) (e :: Effect) (r :: EffectRow) where+  genSomeAction :: [Gen (SomeAction e r)]++instance ArbitraryAction '[] e r where+  genSomeAction = []++instance+    ( 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+    where+  genSomeAction = (fmap SomeAction $ genEff @e @a @(Sem r)) : genSomeAction @as @e @r+
+ src/Polysemy/Check/Arbitrary/Generic.hs view
@@ -0,0 +1,91 @@+module Polysemy.Check.Arbitrary.Generic where++import Control.Applicative (liftA2)+import Data.Kind (Type)+import GHC.Exts (type (~~))+import Generics.Kind+import Test.QuickCheck+import Polysemy+import Polysemy.Check.Arbitrary.AnyEff+import Polysemy.Internal (send)+++------------------------------------------------------------------------------++type a :~~~: b = 'Kon (~~) ':@: a ':@: b+++------------------------------------------------------------------------------+-- | Given @'GArbitraryK' a ('RepK' (e m a))@, this typeclass computes+-- generators for every well-typed constructor of @e m a@. It is capable of+-- building generators for GADTs.+class GArbitraryK (a :: Type) (f :: LoT Type -> Type) where+  garbitraryk :: [Gen (f x)]++instance GArbitraryK a U1 where+  garbitraryk = pure $ pure U1++instance (GArbitraryK1 (f :*: g)) => GArbitraryK a (f :*: g) where+  garbitraryk = garbitraryk1++instance (GArbitraryK1 (Field b)) => GArbitraryK a (Field b) where+  garbitraryk = garbitraryk1++instance (GArbitraryK a f, GArbitraryK a g) => GArbitraryK a (f :+: g) where+  garbitraryk = fmap (fmap L1) (garbitraryk @a @f)+             <> fmap (fmap R1) (garbitraryk @a @g)++instance GArbitraryK1 f => GArbitraryK a ('Kon (a ~~ a) :=>: f) where+  garbitraryk = fmap SuchThat <$> garbitraryk1++instance {-# INCOHERENT #-} GArbitraryK a ('Kon (a ~~ b) :=>: f) where+  garbitraryk = []++instance {-# INCOHERENT #-} GArbitraryK a ('Kon (b ~~ c) :=>: f) where+  garbitraryk = []++instance (GArbitraryK a f) => GArbitraryK a (M1 _1 _2 f) where+  garbitraryk = fmap M1 <$> garbitraryk @a+++------------------------------------------------------------------------------+-- | @genEff \@e \@a \@m@ gets a generator capable of producing every+-- well-typed GADT constructor of @e m a@.+genEff :: forall e a m. (GArbitraryK a (RepK (e m a)), GenericK (e m a)) => Gen (e m a)+genEff = fmap toK $ oneof $ garbitraryk @a @(RepK (e m a))+++------------------------------------------------------------------------------+-- | Like @GArbitraryK@, but gets run after we've already discharged the @a+-- ~ T@ GADT constraint.+class GArbitraryK1 (f :: LoT Type -> Type) where+  garbitraryk1 :: [Gen (f x)]++instance (GArbitraryK1 f, GArbitraryK1 g) => GArbitraryK1 (f :*: g) where+  garbitraryk1 = liftA2 (liftA2 (:*:)) garbitraryk1 garbitraryk1++instance GArbitraryKTerm t => GArbitraryK1 (Field ('Kon t)) where+  garbitraryk1 = pure $ fmap Field garbitrarykterm++instance (GArbitraryK1 f) => GArbitraryK1 (M1 _1 _2 f) where+  garbitraryk1 = fmap M1 <$> garbitraryk1++instance GArbitraryK1 U1 where+  garbitraryk1 = pure $ pure U1+++class GArbitraryKTerm (t :: Type) where+  garbitrarykterm :: Gen t++instance {-# OVERLAPPING #-} ArbitraryEffOfType a r r => GArbitraryKTerm (Sem r a) where+  garbitrarykterm = do+    SomeEffOfType act <- oneof $ genSomeEffOfType @a @r @r+    pure $ send act++instance {-# OVERLAPPING #-} (CoArbitrary a, GArbitraryKTerm b) => GArbitraryKTerm (a -> b) where+  garbitrarykterm = liftArbitrary garbitrarykterm++instance Arbitrary a => GArbitraryKTerm a where+  garbitrarykterm = arbitrary++
+ src/Polysemy/Check/Arbitrary/Generic.hs-boot view
@@ -0,0 +1,19 @@+module Polysemy.Check.Arbitrary.Generic where++import Data.Kind (Type)+import Generics.Kind+import Test.QuickCheck+++------------------------------------------------------------------------------+-- | Given @'GArbitraryK' a ('RepK' (e m a))@, this typeclass computes+-- generators for every well-typed constructor of @e m a@. It is capable of+-- building generators for GADTs.+class GArbitraryK (a :: Type) (f :: LoT Type -> Type) where+  garbitraryk :: [Gen (f x)]++------------------------------------------------------------------------------+-- | @genEff \@e \@a \@m@ gets a generator capable of producing every+-- well-typed GADT constructor of @e m a@.+genEff :: forall e a m. (GArbitraryK a (RepK (e m a)), GenericK (e m a)) => Gen (e m a)+
+ src/Polysemy/Check/Orphans.hs view
@@ -0,0 +1,54 @@+{-# OPTIONS_GHC -Wno-orphans #-}++module Polysemy.Check.Orphans () where++import Generics.Kind.TH+import Polysemy+import Polysemy.Error+import Polysemy.Fail+import Polysemy.Fixpoint+import Polysemy.Input+import Polysemy.NonDet+import Polysemy.Output+import Polysemy.Reader+import Polysemy.Resource+import Polysemy.State+import Polysemy.Tagged+import Polysemy.Trace+import Polysemy.View+import Polysemy.Writer++deriveGenericK ''Embed+deriveGenericK ''Error+deriveGenericK ''Fail+deriveGenericK ''Fixpoint+deriveGenericK ''Input+deriveGenericK ''NonDet+deriveGenericK ''Output+deriveGenericK ''Reader+deriveGenericK ''Resource+deriveGenericK ''State+deriveGenericK ''Tagged+deriveGenericK ''Trace+deriveGenericK ''View+deriveGenericK ''Writer++deriving instance Show s => Show (State s (Sem r) a)+deriving instance Show o => Show (Output o (Sem r) a)+deriving instance Show (Input i (Sem r) a)+deriving instance Show (Fail (Sem r) a)+deriving instance Show (Trace (Sem r) a)++instance Show e => Show (Error e (Sem r) a) where+  show (Throw e2) = "Throw " <> show e2+  show (Catch _ _) = "<Catch>"++instance Show (Reader e (Sem r) a) where+  show Ask = "Ask"+  show (Local _ _) = "<Local>"++instance Show e => Show (Writer e (Sem r) a) where+  show (Tell e) = "Tell " <> show e+  show (Listen _) = "<Listen>"+  show (Pass _) = "<Pass>"+
+ src/Polysemy/Internal/Union/Inject.hs view
@@ -0,0 +1,36 @@+module Polysemy.Internal.Union.Inject+  ( inject+  , Inject+  ) where++import Polysemy.Internal+import Polysemy.Internal.Union+++------------------------------------------------------------------------------+-- | Morally:+--+-- @+-- 'inject' :: 'Members' effs r => 'Sem' effs a -> 'Sem' r a+-- @+inject :: Inject effs r => Sem effs a -> Sem r a+inject (Sem a) = a $ liftSem . deject . hoist inject+++------------------------------------------------------------------------------+-- | Helper class for munging the 'Union' so that we can implement 'inject'.+class Inject effs r where+  deject :: Union effs (Sem r) a -> Union r (Sem r) a++instance Inject '[] r where+  deject = absurdU++instance {-# INCOHERENT #-} Inject r r where+  deject = id++instance (Member eff r, Inject effs r) => Inject (eff ': effs) r where+  deject u =+    case decomp u of+      Left  u' -> deject u'+      Right w  -> Union membership w+
+ test/CommutativeSpec.hs view
@@ -0,0 +1,34 @@+module CommutativeSpec where++import Data.Functor.Compose+import Polysemy+import Polysemy.Check+import Polysemy.Error (Error, runError)+import Polysemy.State+import Polysemy.Trace+import Test.Hspec+import Test.Hspec.QuickCheck+import Test.QuickCheck+++spec :: Spec+spec = do+  prop "State commutes with Trace" $+    prepropCommutative @(State Int) @Trace @TestEffs $+      runTestEffs++  prop "State does not commute with itself" $ expectFailure $+    prepropCommutative @(State Int) @(State Int) @TestEffs $+      runTestEffs++  prop "Error does not commute with State (really: we can do Arbitrary stuff on Error)" $ expectFailure $+    prepropCommutative @(Error Int) @(State Int) @[Error Int, State Int] $+      pure . Compose . run . runState 0 . runError+++type TestEffs = '[State Int, Trace, State Int]++runTestEffs :: Sem TestEffs a -> IO (Compose ((,) Int) ((,) [String]) a)+runTestEffs =+  pure . Compose . run . runState 0 . runTraceList . subsume+
+ test/EquivSpec.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE PartialTypeSignatures #-}++{-# OPTIONS_GHC -Wno-orphans             #-}+{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}++module EquivSpec where++import Polysemy+import Polysemy.Check+import Test.Hspec+import Test.QuickCheck+import Test.Hspec.QuickCheck+import Polysemy.State+import Data.IORef (newIORef)+import Unsafe.Coerce (unsafeCoerce)+++spec :: Spec+spec = do+  prop "Pure state is equivalent to IO state" $ do+    s0 <- arbitrary+    pure $+      prepropEquivalent @'[State Int] @Int+        (runPureState s0)+        (runIOState s0)+        $ ((do+            SomeAction e1 <- arbitraryAction @(State Int) @r+            SomeAction e2 <- arbitraryAction @(State Int) @r+            SomeAction e3 <- arbitraryAction @(State Int) @r+            -- TODO(sandy): e3 has an existential type! GHC doesn't care, but+            -- AFAIK, thereis no syntax to return this type, since it doesn't+            -- exist when we bind 'a' below.+            pure $ send e1 >> send e2 >> unsafeCoerce (send e3)+           ) :: forall r a. Member (State Int) r => Gen (Sem r a))+++runPureState :: Int -> Sem '[State Int] a -> IO a+runPureState s = pure . run . evalState s+++runIOState :: Int -> Sem '[State Int, Embed IO] a -> IO (a)+runIOState s sem = do+  ref <- newIORef s+  runM . runStateIORef ref $ sem+
+ test/LawSpec.hs view
@@ -0,0 +1,94 @@+{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}++module LawSpec where++import Polysemy+import Polysemy.Check+import Test.Hspec+import Test.QuickCheck+import Test.Hspec.QuickCheck+import Polysemy.State+import Data.IORef (newIORef, readIORef)+++spec :: Spec+spec = do+  describe "pure state" $ do+    prop "put >> put = put" $ do+      s <- arbitrary+      pure $ putPutLaw $ runPureState s+    prop "get >>= put = pure ()" $ do+      s <- arbitrary+      pure $ getPutLaw $ runPureState s+    prop "put >> get = put >> pure" $ do+      s <- arbitrary+      pure $ putGetLaw $ runPureState s++  describe "io state" $ do+    prop "put >> put = put" $ do+      s <- arbitrary+      pure $ putPutLaw $ runIOState s+    prop "get >>= put = pure ()" $ do+      s <- arbitrary+      pure $ getPutLaw $ runIOState s+    prop "put >> get = put >> pure" $ do+      s <- arbitrary+      pure $ putGetLaw $ runIOState s+++putPutLaw+    :: (Arbitrary s, Member (State s) r, Eq x, Show x)+    => (Sem r s -> IO x)+    -> Property+putPutLaw = prepropLaw $ do+  s1 <- arbitrary+  s2 <- arbitrary+  pure+    ( do+        put s1+        put s2+        get+    , do+        put s2+        get+    )+++getPutLaw+    :: (Arbitrary s, Member (State s) r, Eq x, Show x)+    => (Sem r () -> IO x)+    -> Property+getPutLaw = prepropLaw $ do+  pure+    ( get >>= put+    , pure ()+    )+++putGetLaw+    :: (Arbitrary s, Member (State s) r, Eq x, Show x)+    => (Sem r s -> IO x)+    -> Property+putGetLaw = prepropLaw $ do+  s <- arbitrary+  pure+    ( do+        put s+        get+    , do+        put s+        pure s+    )+++runPureState :: Int -> Sem '[State Int] a -> IO (Int, a)+runPureState s = pure . run . runState s+++runIOState :: Int -> Sem '[State Int, Embed IO] a -> IO (Int, a)+runIOState s sem = do+  ref <- newIORef s+  a <- runM . runStateIORef ref $ sem+  r <- readIORef ref+  pure (r, a)+
+ test/Main.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}