From c5d626e3a5bf425e254496fd8bfb9a8b9fcf8126 Mon Sep 17 00:00:00 2001 From: Marcin Szamotulski Date: Mon, 7 Oct 2019 06:42:44 +0100 Subject: [PATCH] Removed Cat type It's not performing as good as 'Queue' or 'ListTr'. --- README.md | 3 +- bench/Main.hs | 43 +--- bench/report-O0.md | 33 ---- bench/report-O1.md | 35 ---- bench/report-O2.md | 34 ---- examples/src/LoginStateMachine.hs | 12 +- src/Control/Category/Free.hs | 271 +------------------------- src/Control/Category/Free/Internal.hs | 2 + test/Test/Cat.hs | 72 ++----- 9 files changed, 30 insertions(+), 475 deletions(-) diff --git a/README.md b/README.md index 33515fb..f811798 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,8 @@ [![Maintainer: coot](https://img.shields.io/badge/maintainer-coot-lightgrey.svg)](http://github.com/coot) [![CircleCI](https://circleci.com/gh/coot/free-category/tree/master.svg?style=svg)](https://circleci.com/gh/coot/free-category/tree/master) -This package contains efficient free categories. There are a few presentations based on: +This package contains efficient implementation of free categories. There are +various resentations available: * real-time queues (C. Okasaki 'Pure Functional Data Structures') * type aligned lists diff --git a/bench/Main.hs b/bench/Main.hs index 799ca93..1acf496 100644 --- a/bench/Main.hs +++ b/bench/Main.hs @@ -66,30 +66,7 @@ setupEnv500 = replicate 500 [1..500] main :: IO () main = defaultMain [ env (pure setupEnv100) $ \ints -> bgroup "main" - [ bgroup "Cat 100" $ - [ bench "right right" $ - whnf - (\c -> foldNatCat interpret c 0) - (fromListR (liftCat . Add) ints) - , bench "right left" $ - whnf - (\c -> foldNatCat interpret c 0) - (fromListRL (liftCat . Add) ints) - , bench "left left" $ - whnf - (\c -> foldNatCat interpret c 0) - (fromListL (liftCat . Add) ints) - , bench "left right" $ - whnf - (\c -> foldNatCat interpret c 0) - (fromListLR (liftCat . Add) ints) - , bench "alternate" $ - whnf - (\c -> foldNatCat interpret c 0) - (fromListM (liftCat . Add) ints) - ] - - , bgroup "Queue 100" + [ bgroup "Queue 100" [ bench "right right" $ whnf (\c -> foldNatQ interpret c 0) @@ -159,15 +136,6 @@ main = defaultMain ] ] , env (pure setupEnv250) $ \ints -> bgroup "main" - {-- - - [ bgroup "Cat 250" $ - - [ bench "right right" $ - - whnf - - (\c -> foldNatCat interpret c 0) - - (fromListR (liftCat . Add) ints) - - ] - --} - [ bgroup "Queue 250" [ bench "right right" $ whnf @@ -192,15 +160,6 @@ main = defaultMain --} ] , env (pure setupEnv500) $ \ints -> bgroup "main" - {-- - - [ bgroup "Cat 500" $ - - [ bench "right right" $ - - whnf - - (\c -> foldNatCat interpret c 0) - - (fromListR (liftCat . Add) ints) - - ] - --} - [ bgroup "Queue 500" [ bench "right right" $ whnf diff --git a/bench/report-O0.md b/bench/report-O0.md index 54d8739..44cebeb 100644 --- a/bench/report-O0.md +++ b/bench/report-O0.md @@ -1,38 +1,5 @@ ``` cabal run -O0 bench-cats -benchmarking main/Cat 100/right right -time 2.311 ms (2.243 ms .. 2.442 ms) - 0.953 R² (0.875 R² .. 0.999 R²) -mean 2.300 ms (2.241 ms .. 2.496 ms) -std dev 310.7 μs (47.01 μs .. 629.1 μs) -variance introduced by outliers: 79% (severely inflated) - -benchmarking main/Cat 100/right left -time 3.525 ms (3.291 ms .. 3.908 ms) - 0.930 R² (0.839 R² .. 0.999 R²) -mean 3.693 ms (3.503 ms .. 4.401 ms) -std dev 982.7 μs (162.3 μs .. 1.995 ms) -variance introduced by outliers: 93% (severely inflated) - -benchmarking main/Cat 100/left left -time 3.454 ms (3.439 ms .. 3.470 ms) - 1.000 R² (0.999 R² .. 1.000 R²) -mean 3.422 ms (3.401 ms .. 3.439 ms) -std dev 60.69 μs (42.00 μs .. 89.06 μs) - -benchmarking main/Cat 100/left right -time 3.397 ms (3.376 ms .. 3.415 ms) - 1.000 R² (0.999 R² .. 1.000 R²) -mean 3.370 ms (3.355 ms .. 3.384 ms) -std dev 48.28 μs (38.10 μs .. 63.13 μs) - -benchmarking main/Cat 100/alternate -time 2.649 ms (2.600 ms .. 2.713 ms) - 0.998 R² (0.997 R² .. 0.999 R²) -mean 2.715 ms (2.692 ms .. 2.737 ms) -std dev 76.81 μs (63.80 μs .. 95.94 μs) -variance introduced by outliers: 14% (moderately inflated) - benchmarking main/Queue 100/right right time 1.141 ms (1.138 ms .. 1.143 ms) 1.000 R² (1.000 R² .. 1.000 R²) diff --git a/bench/report-O1.md b/bench/report-O1.md index 08994a5..d992d56 100644 --- a/bench/report-O1.md +++ b/bench/report-O1.md @@ -1,40 +1,5 @@ ``` cabal run -O1 bench-cats -benchmarking main/Cat 100/right right -time 383.4 μs (370.0 μs .. 412.2 μs) - 0.928 R² (0.846 R² .. 0.996 R²) -mean 408.5 μs (381.2 μs .. 466.5 μs) -std dev 131.4 μs (59.97 μs .. 250.7 μs) -variance introduced by outliers: 98% (severely inflated) - -benchmarking main/Cat 100/right left -time 665.2 μs (647.0 μs .. 681.1 μs) - 0.996 R² (0.994 R² .. 0.997 R²) -mean 651.8 μs (643.7 μs .. 660.0 μs) -std dev 27.99 μs (23.84 μs .. 32.75 μs) -variance introduced by outliers: 35% (moderately inflated) - -benchmarking main/Cat 100/left left -time 682.9 μs (671.9 μs .. 692.8 μs) - 0.997 R² (0.995 R² .. 0.998 R²) -mean 694.2 μs (683.5 μs .. 713.7 μs) -std dev 46.27 μs (26.75 μs .. 75.32 μs) -variance introduced by outliers: 56% (severely inflated) - -benchmarking main/Cat 100/left right -time 682.0 μs (664.8 μs .. 698.9 μs) - 0.997 R² (0.995 R² .. 0.998 R²) -mean 673.7 μs (666.1 μs .. 682.2 μs) -std dev 28.44 μs (24.53 μs .. 33.41 μs) -variance introduced by outliers: 34% (moderately inflated) - -benchmarking main/Cat 100/alternate -ktime 582.0 μs (576.1 μs .. 587.5 μs) - 0.997 R² (0.995 R² .. 0.999 R²) -mean 581.2 μs (573.0 μs .. 597.4 μs) -std dev 37.40 μs (21.44 μs .. 68.12 μs) -variance introduced by outliers: 56% (severely inflated) - benchmarking main/Queue 100/right right time 344.2 μs (337.1 μs .. 362.0 μs) 0.974 R² (0.923 R² .. 1.000 R²) diff --git a/bench/report-O2.md b/bench/report-O2.md index 740883a..63292a5 100644 --- a/bench/report-O2.md +++ b/bench/report-O2.md @@ -1,39 +1,5 @@ ``` cabal run -O2 bench-cats -benchmarking main/Cat 100/right right -time 387.7 μs (382.0 μs .. 396.1 μs) - 0.997 R² (0.992 R² .. 1.000 R²) -mean 382.3 μs (378.8 μs .. 389.3 μs) -std dev 15.61 μs (9.528 μs .. 27.64 μs) -variance introduced by outliers: 35% (moderately inflated) - -benchmarking main/Cat 100/right left -time 1.902 ms (1.885 ms .. 1.919 ms) - 0.999 R² (0.999 R² .. 1.000 R²) -mean 1.926 ms (1.911 ms .. 1.943 ms) -std dev 55.12 μs (41.26 μs .. 90.08 μs) -variance introduced by outliers: 15% (moderately inflated) - -benchmarking main/Cat 100/left left -time 1.941 ms (1.924 ms .. 1.958 ms) - 0.999 R² (0.999 R² .. 1.000 R²) -mean 1.937 ms (1.929 ms .. 1.947 ms) -std dev 30.60 μs (23.82 μs .. 41.19 μs) - -benchmarking main/Cat 100/left right -time 1.946 ms (1.895 ms .. 2.034 ms) - 0.994 R² (0.988 R² .. 0.999 R²) -mean 1.982 ms (1.957 ms .. 2.009 ms) -std dev 86.70 μs (66.65 μs .. 112.2 μs) -variance introduced by outliers: 30% (moderately inflated) - -benchmarking main/Cat 100/alternate -time 1.700 ms (1.605 ms .. 1.902 ms) - 0.954 R² (0.904 R² .. 1.000 R²) -mean 1.641 ms (1.614 ms .. 1.740 ms) -std dev 159.2 μs (28.75 μs .. 334.0 μs) -variance introduced by outliers: 69% (severely inflated) - benchmarking main/Queue 100/right right time 341.9 μs (341.2 μs .. 342.8 μs) 1.000 R² (1.000 R² .. 1.000 R²) diff --git a/examples/src/LoginStateMachine.hs b/examples/src/LoginStateMachine.hs index 13485a3..5735e8b 100644 --- a/examples/src/LoginStateMachine.hs +++ b/examples/src/LoginStateMachine.hs @@ -23,7 +23,7 @@ import qualified Data.List.NonEmpty as NE import Test.QuickCheck -import Control.Category.Free (Cat) +import Control.Category.Free (ListTr) -- Import classes and combintators used in this example import Control.Category.FreeEffect @@ -77,16 +77,16 @@ data Tr a (from :: StateType) (to :: StateType) where login :: Monad m => SStateType st - -> EffCat m (Cat (Tr a)) 'LoggedOutType st + -> EffCat m (ListTr (Tr a)) 'LoggedOutType st login = liftEffect . Login logout :: Monad m => Maybe a - -> EffCat m (Cat (Tr a)) 'LoggedInType 'LoggedOutType + -> EffCat m (ListTr (Tr a)) 'LoggedInType 'LoggedOutType logout = liftEffect . Logout access :: Monad m - => EffCat m (Cat (Tr a)) 'LoggedInType 'LoggedInType + => EffCat m (ListTr (Tr a)) 'LoggedInType 'LoggedInType access = liftEffect Access -- @@ -168,7 +168,7 @@ accessSecret -- @'HandleLogin'@ (with a small modifications) but this way we are able to -- test it with a pure @'HandleLogin'@ (see @'handleLoginPure'@). -> HandleLogin m String a - -> EffCat m (Cat (Tr a)) 'LoggedOutType 'LoggedOutType + -> EffCat m (ListTr (Tr a)) 'LoggedOutType 'LoggedOutType accessSecret 0 HandleLogin{handleAccessDenied} = effect $ handleAccessDenied $> id @@ -183,7 +183,7 @@ accessSecret n HandleLogin{handleLogin} where handle :: HandleAccess m a -> Maybe a - -> EffCat m (Cat (Tr a)) 'LoggedInType 'LoggedOutType + -> EffCat m (ListTr (Tr a)) 'LoggedInType 'LoggedOutType handle LogoutHandler ma = logout ma handle (AccessHandler accessHandler dataHandler) _ = effect $ do a <- accessHandler diff --git a/src/Control/Category/Free.hs b/src/Control/Category/Free.hs index 672999a..25b633f 100644 --- a/src/Control/Category/Free.hs +++ b/src/Control/Category/Free.hs @@ -45,12 +45,6 @@ module Control.Category.Free , foldrL , zipWithL - -- * Free Category based on Queue - , Cat (Id) - , liftCat - , consCat - , foldNatCat - -- * Free category (CPS style) , C (..) , liftC @@ -95,269 +89,6 @@ import Data.Semigroup (Semigroup (..)) #endif import Control.Category.Free.Internal -import Unsafe.Coerce (unsafeCoerce) - - --- | A version of a free category based on realtime queues. This is an --- optimised version (for right associations) of E.Kemett's free category from --- 'guanxi' project. --- --- @('.')@ has @O\(1\)@ complexity, folding is @O\(n\)@ where @n@ is the number --- of transitions. --- --- It is optimised for building a morphism from left to right (e.g. with 'foldr' and --- @('.')@). The performance benefits were only seen with @-O1@ or @-O2@, --- though the @-O2@ performance might not be what you expect: morphisms build --- with right fold are fast, but when left folding is used the performance --- drastically decrease (this was not observed with @-O1@). --- --- The internal representation is using type aligned 'Queue', a morphism --- `a → c` is represented as a tuple: --- --- @ --- a → c = ( a → b --- , b ← b₁ : b₂ ← b₃ : ⋯ : bₙ₋₁ ← c : NilQ :: Queue (Cat (Op f) c b) --- ) --- @ --- --- where ← arrows represent arrows in `Cat (Op f)` --- thus we can think of this representation as (though this would not type --- check) --- --- @ --- a → c ~ ( a → b --- , b → b₁ : b₂ → b₃ : ⋯ : bₙ₋₁ → c : NilQ --- ) --- @ --- --- Type aligned 'Queue's have efficient 'snocQ' and 'unconsQ' operations which --- allow to implement efficient composition and folding for 'Cat'. --- --- /Performence/: it does not perform as reliably as 'Queue', which are not --- frigile to left right associations, and it is also more frigile to @-O@ --- flags (behaves purly without any optimisations, e.g. @-O0@; and in some --- cases performence degrades with @-O2@ flag). --- -data Cat (f :: k -> k -> *) a b where - Id :: Cat f a a - Cat :: Queue (Cat (Op f)) c b - -> f a b - -> Cat f a c - -compose :: forall (f :: k -> k -> *) x y z. - Cat f y z - -> Cat f x y - -> Cat f x z -compose f (Cat q g) = Cat (q `snocQ` op f) g -compose Id f = f -compose f Id = f -{-# INLINE [1] compose #-} - -liftCat :: forall (f :: k -> k -> *) a b. - f a b - -> Cat f a b -liftCat ab = Cat nilQ ab -{-# INLINE [1] liftCat #-} - -consCat :: forall (f :: k -> k -> *) a b c. - f b c - -> Cat f a b - -> Cat f a c -consCat bc ab = liftCat bc . ab -{-# INLINE [1] consCat #-} - -foldNatCat :: forall (f :: k -> k -> *)c a b. - Category c - => (forall x y. f x y -> c x y) - -> Cat f a b - -> c a b -foldNatCat _nat Id = id -foldNatCat nat (Cat q0 tr0) = - case q0 of - NilQ -> nat tr0 - ConsQ Id q' -> go q' . nat tr0 - ConsQ c q' -> go q' . foldNatCat nat (unOp c) . nat tr0 - where - -- like foldNatQ - go :: Queue (Cat (Op f)) x y -> c y x - go q = case q of - NilQ -> id - ConsQ zy q' -> go q' . foldNatCat nat (unOp zy) -{-# INLINE [1] foldNatCat #-} - -{-# RULES - -"foldNatCat/consCat" - forall (f :: f (v :: k) (w :: k)) - (q :: Cat f (u :: k) (v :: k)) - (nat :: forall (x :: k) (y :: k). f x y -> c x y). - foldNatCat nat (consCat f q) = nat f . foldNatCat nat q - -"foldNatCat/liftCat" - forall (nat :: forall (x :: k) (y :: k). f x y -> c x y) - (g :: f v w) - (h :: Cat f u v). - foldNatCat nat (liftCat g `compose` h) = nat g . foldNatCat nat h - --- TODO: These two rules may never fire due to `Class op` rule. --- --- "foldNatCat/foldMap" --- forall (nat :: forall (x :: k) (y :: k). f x y -> c x y) --- (fs :: Monoid (c a a) => [f (a :: k) a]). --- foldNatCat nat (foldMap liftCat fs) = foldMap nat fs - --- "foldNatCat/foldr" --- forall (nat :: forall (x :: k) (y :: k). f x y -> c x y) --- (fs :: Monoid (c a a) => [f (a :: k) a]) --- (nil :: Cat f a a). --- foldNatCat nat (foldr consCat nil fs) = foldMap nat fs . foldNatCat nat nil - -#-} - --- | 'op' can be defined as --- --- @ --- op :: Cat f x y -> Cat (Op f) y x --- op Id = Id --- op (Cat q tr) = Cat nilQ (Op tr) . foldNatQ unDual q --- @ --- --- where --- --- @ --- unDual :: forall (f :: k -> k -> *) x y. --- Cat (Op (Op f)) x y --- -> Cat f x y --- unDual Id = Id --- unDual (Cat q (Op (Op tr))) = Cat (hoistQ unDual q) tr --- @ --- --- But instead we use `unsafeCoerce`, which is safe by the following argument. --- We use `l ~ r` to say that the left and right hand side have the same --- representation. We want to show that `op g ~ g` for any `g :: Cat f x y` --- --- It is easy to observe that `unDual g ~ g` for any `x :: Cat (Op (Op f)) x y`. --- --- > op Id = Id --- > ~ Id --- > op (Cat q tr) --- > = c₀@(Cat nilQ (Op tr)) . foldNatQ unDual q --- > Note that `.` here denotes composition in `Cat (Op f)`. --- > Let us assume that `q = c₁ : c₂ : ⋯ : cₙ : NilQ`, --- > where each `cᵢ :: Cat (Op (Op tr)) aᵢ aᵢ₊₁` --- > unfolding 'foldNatQ' gives us --- > = c₀ . unDual c₁ . ⋯ . unDual cₙ --- > `unDual cᵢ :: Cat tr aᵢ aᵢ₊₁` has the same representation as cᵢ, --- > at this step we also need to rewrite `.` composition in --- > `Cat (Op f)` using composition in `Cat f`, this reverses the order --- > ~ cₙ . ⋯ . c₁ . Cat nilQ tr --- > By definition of composition in `Cat f` --- > = Cat q tr --- --- This proves that `op` does not change the representation and thus it is safe --- to use `unsafeCoerce` instead. --- -op :: forall (f :: k -> k -> *) x y. - Cat f x y - -> Cat (Op f) y x -op = unsafeCoerce -{-# INLINE [1] op #-} - --- | Since `op` is an identity, it inverse `unOp` must be too. Thus we can --- also use `unsafeCoerce`. --- -unOp :: forall (f :: k -> k -> *) x y. - Cat (Op f) x y - -> Cat f y x -unOp = unsafeCoerce --- unOp Id = Id --- unOp (Cat q (Op tr)) = Cat nilQ tr . foldNatQ unDual q -{-# INLINE [1] unOp #-} - -{-# RULES - -"op/unOp" - forall (x :: Cat (Op f) (x :: k) (y :: k)). - op (unOp x) = x - -"unOp/op" - forall (x :: Cat f (x :: k) (y :: k)). - unOp (op x) = x - -#-} - -instance Category (Cat f) where - id = Id - (.) = compose - -instance Semigroup (Cat f a a) where - f <> g = f `compose` g - -instance Monoid (Cat f o o) where - mempty = id -#if __GLASGOW_HASKELL__ < 804 - mappend = (<>) -#endif - -#if __GLASGOW_HASKELL__ >= 806 --- | Show instance via 'ListTr' --- -instance (forall x y. Show (f x y)) => Show (Cat f a b) where - show c = show (hoistFreeH2 c :: ListTr f a b) -#else --- | Blind show instance via 'ListTr' --- -instance Show (Cat f a b) where - show c = show (hoistFreeH2 c :: ListTr f a b) -#endif - -instance Arrow f => Arrow (Cat f) where - arr = liftCat . arr - {-# INLINE arr #-} - - Cat q tr *** Cat q' tr' = - Cat (zipWithQ (\x y -> op (unOp x *** unOp y)) q q') - (tr *** tr') - Cat q tr *** Id = - Cat (zipWithQ (\x y -> op (unOp x *** unOp y)) q NilQ) - (tr *** arr id) - Id *** Cat q' tr' = - Cat (zipWithQ (\x y -> op (unOp x *** unOp y)) NilQ q') - (arr id *** tr') - Id *** Id = - Cat NilQ (arr id *** arr id) - {-# INLINE (***) #-} - -instance ArrowZero f => ArrowZero (Cat f) where - zeroArrow = liftCat zeroArrow - -instance ArrowChoice f => ArrowChoice (Cat f) where - Cat xb ax +++ Cat yb ay = - Cat (zipWithQ (\x y -> op (unOp x +++ unOp y)) xb yb) - (ax +++ ay) - Cat xb ax +++ Id = - Cat (zipWithQ (\x y -> op (unOp x +++ unOp y)) xb NilQ) - (ax +++ arr id) - Id +++ (Cat xb ax) = - Cat (zipWithQ (\x y -> op (unOp x +++ unOp y)) NilQ xb) - (arr id +++ ax) - Id +++ Id = Id - {-# INLINE (+++) #-} - -type instance AlgebraType0 Cat f = () -type instance AlgebraType Cat c = Category c - --- | /complexity/ of 'foldNatFree2': @O\(n\)@ where @n@ is number of --- transitions embedded in 'Cat'. --- -instance FreeAlgebra2 Cat where - liftFree2 = liftCat - {-# INLINE liftFree2 #-} - foldNatFree2 = foldNatCat - {-# INLINE foldNatFree2 #-} - - codom2 = Proof - forget2 = Proof -- @@ -384,7 +115,7 @@ composeC (C g) (C f) = C $ \k -> g k . f k {-# INLINE [1] composeC #-} -- | --- Isomorphism from @'Cat'@ to @'C'@, which is a specialisation of +-- Isomorphism from @'ListTr'@ to @'C'@, which is a specialisation of -- @'hoistFreeH2'@. toC :: ListTr f a b -> C f a b toC = hoistFreeH2 diff --git a/src/Control/Category/Free/Internal.hs b/src/Control/Category/Free/Internal.hs index 93b4a69..3ba0533 100644 --- a/src/Control/Category/Free/Internal.hs +++ b/src/Control/Category/Free/Internal.hs @@ -29,6 +29,7 @@ module Control.Category.Free.Internal ( Op (..) , hoistOp + , ListTr (..) , liftL , foldNatL @@ -36,6 +37,7 @@ module Control.Category.Free.Internal , foldrL , foldlL , zipWithL + , Queue (NilQ, ConsQ) , liftQ , nilQ diff --git a/test/Test/Cat.hs b/test/Test/Cat.hs index 548dbf1..b996b99 100644 --- a/test/Test/Cat.hs +++ b/test/Test/Cat.hs @@ -36,23 +36,20 @@ import Test.Tasty.QuickCheck (testProperty) tests :: TestTree tests = testGroup "Control.Category.Free" - [ testProperty "Cat" prop_Cat + [ testProperty "Queue" prop_Queue , testProperty "C" prop_C , testGroup "Category laws" - [ testProperty "Cat id" prop_id_Cat - , testProperty "Cat associativity" prop_associativity_Cat + [ testProperty "ListTr id" prop_id_ListTr + , testProperty "ListTr associativity" prop_associativity_ListTr + , testProperty "Queue id" prop_id_Queue + , testProperty "Queue associativity" prop_associativity_Queue , testProperty "C id" prop_id_C , testProperty "C associativity" prop_associativity_C - , testProperty "ListTr id" prop_id_Queue - , testProperty "ListTr associativity" prop_associativity_Queue - , testProperty "ListTr id" prop_id_ListTr - , testProperty "ListTr associativity" prop_associativity_ListTr ] , testGroup "foldFree2 and foldMap" - [ testProperty "foldFree Cat" prop_foldCat - , testProperty "foldFree C" prop_foldC + [ testProperty "foldFree ListTr" prop_foldListTr , testProperty "foldFree Queue" prop_foldQueue - , testProperty "foldFree ListTr" prop_foldListTr + , testProperty "foldFree C" prop_foldC ] ] @@ -210,20 +207,20 @@ instance Arbitrary ArbListTr where -- -- test 'Cat' and 'C' treating 'ListTr' as a model to compare to. -- -prop_Cat, prop_C +prop_Queue, prop_C :: Blind ArbListTr -> Bool -prop_Cat (Blind (ArbListTr listTr SInt _)) = - foldNatFree2 interpretTr (hoistFreeH2 @_ @Cat listTr) 0 +prop_Queue (Blind (ArbListTr listTr SInt _)) = + foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0 == foldNatFree2 interpretTr listTr 0 -prop_Cat (Blind (ArbListTr listTr SInteger _)) = - foldNatFree2 interpretTr (hoistFreeH2 @_ @Cat listTr) 0 +prop_Queue (Blind (ArbListTr listTr SInteger _)) = + foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0 == foldNatFree2 interpretTr listTr 0 -prop_Cat (Blind (ArbListTr listTr SNatural _)) = - foldNatFree2 interpretTr (hoistFreeH2 @_ @Cat listTr) 0 +prop_Queue (Blind (ArbListTr listTr SNatural _)) = + foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0 == foldNatFree2 interpretTr listTr 0 @@ -311,35 +308,6 @@ toList c = go (hoistFreeH2 c) go NilTr = [] go (ConsTr tr@IntCat{} xs) = tr : go xs - --- --- 'Cat' cateogry laws --- - -newtype ArbIntCat = ArbIntCat (Cat IntCat '() '()) - -instance Show ArbIntCat where - show (ArbIntCat c) = show c - -instance Arbitrary ArbIntCat where - arbitrary = ArbIntCat . fromList <$> arbitrary - shrink (ArbIntCat c) = - map (ArbIntCat . fromList) - $ shrinkList (const []) - $ toList c - -prop_id_Cat :: ArbIntCat -> Bool -prop_id_Cat (ArbIntCat f) = - prop_id (on (==) toList) f - -prop_associativity_Cat - :: ArbIntCat -> ArbIntCat -> ArbIntCat - -> Bool -prop_associativity_Cat (ArbIntCat f0) - (ArbIntCat f1) - (ArbIntCat f2) = - prop_associativity (on (==) toList) f0 f1 f2 - -- -- 'C' category laws -- @@ -429,18 +397,14 @@ prop_associativity_ListTr (ArbIntListTr f0) -- Compatibility between 'foldFree2' and 'foldMap' for 'IntCat' -- -prop_foldCat :: ArbIntCat -> Bool -prop_foldCat (ArbIntCat f) - = foldFree2 f == foldMap id (toList f) - -prop_foldC :: (Blind ArbIntC) -> Bool -prop_foldC (Blind (ArbIntC f)) +prop_foldListTr :: ArbIntListTr -> Bool +prop_foldListTr (ArbIntListTr f) = foldFree2 f == foldMap id (toList f) prop_foldQueue :: ArbIntQueue -> Bool prop_foldQueue (ArbIntQueue f) = foldFree2 f == foldMap id (toList f) -prop_foldListTr :: ArbIntListTr -> Bool -prop_foldListTr (ArbIntListTr f) +prop_foldC :: (Blind ArbIntC) -> Bool +prop_foldC (Blind (ArbIntC f)) = foldFree2 f == foldMap id (toList f)