Law Machinery (#269)

This PR adds machinery for writing easy laws that should hold for an effect. It gives an example of what they'd look like for State s.

package.yaml

@@ -30,6 +30,7 @@ dependencies:
 - async >= 2.2 && < 3
 - type-errors >= 0.2.0.0
 - type-errors-pretty >= 0.0.0.0 && < 0.1
+- QuickCheck >= 2.11.3 && < 3
 
 custom-setup:
   dependencies:

polysemy.cabal

@@ -4,7 +4,7 @@ cabal-version: 1.24
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 522ece75c59adca1fc23637f8f0f6a2a5185fc52a0eb4c003c3a9dd76d1a94f6
+-- hash: 9c9c8b8561c30bd1736e7de233dd3ffd9bf260977d78704950e3d0b48be7f291
 
 name:           polysemy
 version:        1.2.3.0
@@ -71,11 +71,13 @@ library
       Polysemy.Internal.Union
       Polysemy.Internal.Writer
       Polysemy.IO
+      Polysemy.Law
       Polysemy.NonDet
       Polysemy.Output
       Polysemy.Reader
       Polysemy.Resource
       Polysemy.State
+      Polysemy.State.Law
       Polysemy.Tagged
       Polysemy.Trace
       Polysemy.View
@@ -87,7 +89,8 @@ library
   default-extensions: DataKinds DeriveFunctor FlexibleContexts GADTs LambdaCase PolyKinds RankNTypes ScopedTypeVariables StandaloneDeriving TypeApplications TypeOperators TypeFamilies UnicodeSyntax
   ghc-options: -Wall
   build-depends:
-      async >=2.2 && <3
+      QuickCheck >=2.11.3 && <3
+    , async >=2.2 && <3
     , base >=4.9 && <5
     , containers >=0.5 && <0.7
     , first-class-families >=0.5.0.0 && <0.7
@@ -136,6 +139,7 @@ test-suite polysemy-test
       HigherOrderSpec
       InspectorSpec
       InterceptSpec
+      LawsSpec
       OutputSpec
       ThEffectSpec
       TypeErrors
@@ -149,7 +153,8 @@ test-suite polysemy-test
   build-tool-depends:
       hspec-discover:hspec-discover >=2.0
   build-depends:
-      async >=2.2 && <3
+      QuickCheck >=2.11.3 && <3
+    , async >=2.2 && <3
     , base >=4.9 && <5
     , containers >=0.5 && <0.7
     , doctest >=0.16.0.1 && <0.17
@@ -183,7 +188,8 @@ benchmark polysemy-bench
       bench
   default-extensions: DataKinds DeriveFunctor FlexibleContexts GADTs LambdaCase PolyKinds RankNTypes ScopedTypeVariables StandaloneDeriving TypeApplications TypeOperators TypeFamilies UnicodeSyntax
   build-depends:
-      async >=2.2 && <3
+      QuickCheck >=2.11.3 && <3
+    , async >=2.2 && <3
     , base >=4.9 && <5
     , containers >=0.5 && <0.7
     , criterion

src/Polysemy/Law.hs

@@ -0,0 +1,197 @@
+{-# LANGUAGE CPP                    #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+#if __GLASGOW_HASKELL__ < 806
+-- There is a bug in older versions of Haddock that don't allow documentation
+-- on GADT arguments.
+#define HADDOCK --
+#else
+#define HADDOCK -- ^
+#endif
+
+module Polysemy.Law
+  ( Law (..)
+  , runLaw
+  , MakeLaw (..)
+  , Citizen (..)
+  , printf
+  , module Test.QuickCheck
+  ) where
+
+import Control.Arrow (first)
+import Data.Char
+import Polysemy
+import Test.QuickCheck
+
+
+------------------------------------------------------------------------------
+-- | Associates the name @r@ with the eventual type @a@. For example,
+-- @'Citizen' (String -> Bool) Bool@ can produce arbitrary @Bool@s by calling
+-- the given function with arbitrary @String@s.
+class Citizen r a | r -> a where
+  -- | Generate two @a@s via two @r@s. Additionally, produce a list of strings
+  -- corresponding to any arbitrary arguments we needed to build.
+  getCitizen :: r -> r -> Gen ([String], (a, a))
+
+instance {-# OVERLAPPING #-} Citizen (Sem r a -> b) (Sem r a -> b) where
+  getCitizen r1 r2 = pure ([], (r1, r2))
+
+instance Citizen (Sem r a) (Sem r a) where
+  getCitizen r1 r2 = pure ([], (r1, r2))
+
+instance (Arbitrary a, Show a, Citizen b r) => Citizen (a -> b) r where
+  getCitizen f1 f2 = do
+    a <- arbitrary
+    first (show a :) <$> getCitizen (f1 a) (f2 a)
+
+
+------------------------------------------------------------------------------
+-- | A law that effect @e@ must satisfy whenever it is in environment @r@. You
+-- can use 'runLaw' to transform these 'Law's into QuickCheck-able 'Property's.
+data Law e r where
+  -- | A pure 'Law', that doesn't require any access to 'IO'.
+  Law
+      :: ( Eq a
+         , Show a
+         , Citizen i12n (Sem r x -> a)
+         , Citizen res (Sem (e ': r) x)
+         )
+      => i12n
+         HADDOCK An interpretation from @'Sem' r x@ down to a pure value. This is
+         -- likely 'run'.
+      -> String
+         HADDOCK A string representation of the left-hand of the rule. This is
+         -- a formatted string, for more details, refer to 'printf'.
+      -> res
+         HADDOCK The left-hand rule. This thing may be of type @'Sem' (e ': r) x@,
+         -- or be a function type that reproduces a @'Sem' (e ': r) x@. If this
+         -- is a function type, it's guaranteed to be called with the same
+         -- arguments that the right-handed side was called with.
+      -> String
+         HADDOCK A string representation of the right-hand of the rule. This is
+         -- a formatted string, for more details, refer to 'printf'.
+      -> res
+         HADDOCK The right-hand rule. This thing may be of type @'Sem' (e ': r) x@,
+         -- or be a function type that reproduces a @'Sem' (e ': r) x@. If this
+         -- is a function type, it's guaranteed to be called with the same
+         -- arguments that the left-handed side was called with.
+      -> Law e r
+  -- | Like 'Law', but for 'IO'-accessing effects.
+  LawIO
+      :: ( Eq a
+         , Show a
+         , Citizen i12n (Sem r x -> IO a)
+         , Citizen res (Sem (e ': r) x)
+         )
+      => i12n
+         HADDOCK An interpretation from @'Sem' r x@ down to an 'IO' value. This is
+         -- likely 'runM'.
+      -> String
+         HADDOCK A string representation of the left-hand of the rule. This is
+         -- a formatted string, for more details, refer to 'printf'.
+      -> res
+         HADDOCK The left-hand rule. This thing may be of type @'Sem' (e ': r) x@,
+         -- or be a function type that reproduces a @'Sem' (e ': r) x@. If this
+         -- is a function type, it's guaranteed to be called with the same
+         -- arguments that the right-handed side was called with.
+      -> String
+         HADDOCK A string representation of the right-hand of the rule. This is
+         -- a formatted string, for more details, refer to 'printf'.
+      -> res
+         HADDOCK The right-hand rule. This thing may be of type @'Sem' (e ': r) x@,
+         -- or be a function type that reproduces a @'Sem' (e ': r) x@. If this
+         -- is a function type, it's guaranteed to be called with the same
+         -- arguments that the left-handed side was called with.
+      -> Law e r
+
+
+------------------------------------------------------------------------------
+-- | A typeclass that provides the smart constructor 'mkLaw'.
+class MakeLaw e r where
+  -- | A smart constructor for building 'Law's.
+  mkLaw
+      :: (Eq a, Show a, Citizen res (Sem (e ': r) a))
+      => String
+      -> res
+      -> String
+      -> res
+      -> Law e r
+
+instance MakeLaw e '[] where
+  mkLaw = Law run
+
+instance MakeLaw e '[Embed IO] where
+  mkLaw = LawIO runM
+
+
+------------------------------------------------------------------------------
+-- | Produces a QuickCheck-able 'Property' corresponding to whether the given
+-- interpreter satisfies the 'Law'.
+runLaw :: InterpreterFor e r -> Law e r -> Property
+runLaw i12n (Law finish str1 a str2 b) = property $ do
+  (_, (lower, _)) <- getCitizen finish finish
+  (args, (ma, mb)) <- getCitizen a b
+  let run_it = lower . i12n
+      a' = run_it ma
+      b' = run_it mb
+  pure $
+    counterexample
+      (mkCounterexampleString str1 a' str2 b' args)
+      (a' == b')
+runLaw i12n (LawIO finish str1 a str2 b) = property $ do
+  (_, (lower, _)) <- getCitizen finish finish
+  (args, (ma, mb)) <- getCitizen a b
+  let run_it = lower . i12n
+  pure $ ioProperty $ do
+    a' <- run_it ma
+    b' <- run_it mb
+    pure $
+      counterexample
+        (mkCounterexampleString str1 a' str2 b' args)
+        (a' == b')
+
+
+------------------------------------------------------------------------------
+-- | Make a string representation for a failing 'runLaw' property.
+mkCounterexampleString
+    :: Show a
+    => String
+    -> a
+    -> String
+    -> a
+    -> [String]
+    -> String
+mkCounterexampleString str1 a str2 b args =
+  mconcat
+    [ printf str1 args , " (result: " , show a , ")\n /= \n"
+    , printf str2 args , " (result: " , show b , ")"
+    ]
+
+
+------------------------------------------------------------------------------
+-- | A bare-boned implementation of printf. This function will replace tokens
+-- of the form @"%n"@ in the first string with @args !! n@.
+--
+-- This will only work for indexes up to 9.
+--
+-- For example:
+--
+-- >>> printf "hello %1 %2% %3 %1" ["world", "50"]
+-- "hello world 50% %3 world"
+printf :: String -> [String] -> String
+printf str args = splitArgs str
+  where
+    splitArgs :: String -> String
+    splitArgs s =
+      case break (== '%') s of
+        (as, "") -> as
+        (as, _ : b : bs)
+          | isDigit b
+          , let d = read [b] - 1
+          , d < length args
+            -> as ++ (args !! d) ++ splitArgs bs
+        (as, _ : bs) ->  as ++ "%" ++ splitArgs bs
+

src/Polysemy/State/Law.hs

@@ -0,0 +1,59 @@
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module Polysemy.State.Law where
+
+import Polysemy
+import Polysemy.Law
+import Polysemy.State
+import Control.Applicative
+import Control.Arrow
+
+
+------------------------------------------------------------------------------
+-- | A collection of laws that show a `State` interpreter is correct.
+prop_lawfulState
+    :: forall r s
+     . (Eq s, Show s, Arbitrary s, MakeLaw (State s) r)
+    => InterpreterFor (State s) r
+    -> Property
+prop_lawfulState i12n = conjoin
+  [ runLaw i12n law_putTwice
+  , runLaw i12n law_getTwice
+  , runLaw i12n law_getPutGet
+  ]
+
+
+law_putTwice
+    :: forall s r
+     . (Eq s, Arbitrary s, Show s, MakeLaw (State s) r)
+    => Law (State s) r
+law_putTwice =
+  mkLaw
+    "put %1 >> put %2 >> get"
+    (\s s' -> put @s s >> put @s s' >> get @s)
+    "put %2 >> get"
+    (\_ s' ->             put @s s' >> get @s)
+
+law_getTwice
+    :: forall s r
+     . (Eq s, Arbitrary s, Show s, MakeLaw (State s) r)
+    => Law (State s) r
+law_getTwice =
+  mkLaw
+    "liftA2 (,) get get"
+    (liftA2 (,) (get @s) (get @s))
+    "(id &&& id) <$> get"
+    ((id &&& id) <$> get @s)
+
+law_getPutGet
+    :: forall s r
+     . (Eq s, Arbitrary s, Show s, MakeLaw (State s) r)
+    => Law (State s) r
+law_getPutGet =
+  mkLaw
+    "get >>= put >> get"
+    (get @s >>= put @s >> get @s)
+    "get"
+    (get @s)
+

test/LawsSpec.hs

@@ -0,0 +1,20 @@
+module LawsSpec where
+
+import Polysemy
+import Polysemy.Law
+import Polysemy.State
+import Polysemy.State.Law
+import Test.Hspec
+
+spec :: Spec
+spec = parallel $ do
+  describe "State effects" $ do
+    it "runState should pass the laws" $
+      property $ prop_lawfulState @'[] $ fmap snd . runState @Int 0
+
+    it "runLazyState should pass the laws" $
+      property $ prop_lawfulState @'[] $ fmap snd . runLazyState @Int 0
+
+    it "stateToIO should pass the laws" $
+      property $ prop_lawfulState @'[Embed IO] $ fmap snd . stateToIO @Int 0
+