{-# 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 (..)

    -- * Support for Existential Types
  , ExistentialFor

    -- * Constraints for Generators of Effects
  , GArbitraryK
  , ArbitraryAction
  , ArbitraryEff
  , ArbitraryEffOfType
  , TypesOf

    -- * Re-exports
  , send
  , deriveGenericK
  , GenericK
  ) where

import Control.Monad (void)
import Generics.Kind (GenericK)
import Generics.Kind.TH (deriveGenericK)
import Polysemy
import Polysemy.Check.Arbitrary
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 :: (forall a. Sem r a -> IO (f a)) -> Property
prepropCommutative lower :: forall a. Sem r a -> IO (f a)
lower = Testable (Gen Property) => Gen Property -> Property
forall prop. Testable prop => prop -> Property
property @(Gen Property) (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ do
  SomeEff m1 :: e (Sem r) a
m1 <- ArbitraryEff r r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @r @r
  SomeEff e1 :: e (Sem r) a
e1 <- ArbitraryEff '[e1] r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @'[e1] @r
  SomeEff e2 :: e (Sem r) a
e2 <- ArbitraryEff '[e2] r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @'[e2] @r
  SomeEff m2 :: e (Sem r) a
m2 <- ArbitraryEff r r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @r @r
  Property -> Gen Property
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample "Effects are not commutative!" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample "" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ("k1  = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
m1) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ("e1 = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
e1) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ("e2 = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
e2) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ("k2  = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
m2) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample "" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample "(e1 >> e2 >> k) /= (e2 >> e1 >> k)" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
        f a
r1 <- Sem r a -> IO (f a)
forall a. Sem r a -> IO (f a)
lower (Sem r a -> IO (f a)) -> Sem r a -> IO (f a)
forall a b. (a -> b) -> a -> b
$ e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
m1 Sem r a -> Sem r a -> Sem r a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
e1 Sem r a -> Sem r a -> Sem r a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
e2 Sem r a -> Sem r a -> Sem r a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
m2
        f a
r2 <- Sem r a -> IO (f a)
forall a. Sem r a -> IO (f a)
lower (Sem r a -> IO (f a)) -> Sem r a -> IO (f a)
forall a b. (a -> b) -> a -> b
$ e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
m1 Sem r a -> Sem r a -> Sem r a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
e2 Sem r a -> Sem r a -> Sem r a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
e1 Sem r a -> Sem r a -> Sem r a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
m2
        Property -> IO Property
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ f a
r1 f a -> f a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== f a
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
    :: 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
prepropLaw :: Gen (Sem r a, Sem r a)
-> (forall z. Sem r (a, z) -> IO (f (a, z))) -> Property
prepropLaw g :: Gen (Sem r a, Sem r a)
g lower :: forall z. Sem r (a, z) -> IO (f (a, z))
lower = Testable (Gen Property) => Gen Property -> Property
forall prop. Testable prop => prop -> Property
property @(Gen Property) (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ do
  SomeEff pre :: e (Sem r) a
pre <- ArbitraryEff effs r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @effs @r
  (m1 :: Sem r a
m1, m2 :: Sem r a
m2) <- Gen (Sem r a, Sem r a)
g
  SomeEff post :: e (Sem r) a
post <- ArbitraryEff effs r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @effs @r
  Property -> Gen Property
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ("before = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
pre) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ("after  = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
post) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
        f (a, a)
a1 <-
          Sem r (a, a) -> IO (f (a, a))
forall z. Sem r (a, z) -> IO (f (a, z))
lower (Sem r (a, a) -> IO (f (a, a))) -> Sem r (a, a) -> IO (f (a, a))
forall a b. (a -> b) -> a -> b
$ do
            Sem r a -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Sem r a -> Sem r ()) -> Sem r a -> Sem r ()
forall a b. (a -> b) -> a -> b
$ e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
pre
            a
a1 <- Sem r a
m1
            a
r <- e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
post
            (a, a) -> Sem r (a, a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a1, a
r)
        f (a, a)
a2 <-
          Sem r (a, a) -> IO (f (a, a))
forall z. Sem r (a, z) -> IO (f (a, z))
lower (Sem r (a, a) -> IO (f (a, a))) -> Sem r (a, a) -> IO (f (a, a))
forall a b. (a -> b) -> a -> b
$ do
            Sem r a -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Sem r a -> Sem r ()) -> Sem r a -> Sem r ()
forall a b. (a -> b) -> a -> b
$ e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
pre
            a
a2 <- Sem r a
m2
            a
r <- e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
post
            (a, a) -> Sem r (a, a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a2, a
r)
        Property -> IO Property
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ f (a, a)
a1 f (a, a) -> f (a, a) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== f (a, a)
a2


------------------------------------------------------------------------------
-- | Prove that two interpreters are equivalent. This property ensures that the
-- two interpreters give the same result for every arbitrary program.
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))
       -- ^ 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.
    -> Property
prepropEquivalent :: (forall a. Sem r1 a -> IO (f a))
-> (forall a. Sem r2 a -> IO (f a)) -> Property
prepropEquivalent int1 :: forall a. Sem r1 a -> IO (f a)
int1 int2 :: forall a. Sem r2 a -> IO (f a)
int2 = Gen Property -> Property
forall prop. Testable prop => prop -> Property
property (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ do
  SomeSem sem :: forall (r :: EffectRow). Inject effs r => Sem r Int
sem <- Arbitrary (Sem effs Int) => Gen (SomeSem effs Int)
forall (effs :: EffectRow) a.
Arbitrary (Sem effs a) =>
Gen (SomeSem effs a)
liftGen @effs @Int
  Property -> Gen Property
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    f Int
a1 <- Sem r1 Int -> IO (f Int)
forall a. Sem r1 a -> IO (f a)
int1 Sem r1 Int
forall (r :: EffectRow). Inject effs r => Sem r Int
sem
    f Int
a2 <- Sem r2 Int -> IO (f Int)
forall a. Sem r2 a -> IO (f a)
int2 Sem r2 Int
forall (r :: EffectRow). Inject effs r => Sem r Int
sem
    Property -> IO Property
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ f Int
a1 f Int -> f Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== f Int
a2


newtype SomeSem effs a = SomeSem
  { SomeSem effs a -> forall (r :: EffectRow). Inject effs r => Sem r a
_getSomeSem :: forall r. (Inject effs r) => Sem r a
  }


liftGen
    :: forall effs a
     . Arbitrary (Sem effs a)
    => Gen (SomeSem effs a)
liftGen :: Gen (SomeSem effs a)
liftGen = do
  Sem effs a
a <- Arbitrary (Sem effs a) => Gen (Sem effs a)
forall a. Arbitrary a => Gen a
arbitrary @(Sem effs a)
  SomeSem effs a -> Gen (SomeSem effs a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeSem effs a -> Gen (SomeSem effs a))
-> SomeSem effs a -> Gen (SomeSem effs a)
forall a b. (a -> b) -> a -> b
$ (forall (r :: EffectRow). Inject effs r => Sem r a)
-> SomeSem effs a
forall (effs :: EffectRow) a.
(forall (r :: EffectRow). Inject effs r => Sem r a)
-> SomeSem effs a
SomeSem ((forall (r :: EffectRow). Inject effs r => Sem r a)
 -> SomeSem effs a)
-> (forall (r :: EffectRow). Inject effs r => Sem r a)
-> SomeSem effs a
forall a b. (a -> b) -> a -> b
$ Sem effs a -> Sem r a
forall (effs :: EffectRow) (r :: EffectRow) a.
Inject effs r =>
Sem effs a -> Sem r a
inject Sem effs a
a