mirror of
https://github.com/coot/free-category.git
synced 2024-09-11 14:17:30 +03:00
396 lines
11 KiB
Haskell
396 lines
11 KiB
Haskell
{-# LANGUAGE CPP #-}
|
|
{-# LANGUAGE DataKinds #-}
|
|
{-# LANGUAGE FlexibleInstances #-}
|
|
#if __GLASGOW_HASKELL__ >= 902
|
|
{-# LANGUAGE FlexibleContexts #-}
|
|
#endif
|
|
{-# LANGUAGE GADTs #-}
|
|
{-# LANGUAGE KindSignatures #-}
|
|
{-# LANGUAGE PolyKinds #-}
|
|
{-# LANGUAGE ScopedTypeVariables #-}
|
|
{-# LANGUAGE TypeApplications #-}
|
|
{-# LANGUAGE TupleSections #-}
|
|
{-# LANGUAGE UndecidableInstances #-}
|
|
{-# LANGUAGE QuantifiedConstraints #-}
|
|
|
|
{-# OPTIONS_GHC -Wno-orphans #-}
|
|
|
|
module Test.Cat (tests) where
|
|
|
|
import Prelude hiding ((.), id)
|
|
import Control.Category
|
|
import Data.Function (on)
|
|
import Text.Show.Functions ()
|
|
import Numeric.Natural (Natural)
|
|
|
|
import Control.Algebra.Free2
|
|
import Control.Category.Free
|
|
|
|
import Test.QuickCheck
|
|
import Test.Tasty (TestTree, testGroup)
|
|
import Test.Tasty.QuickCheck (testProperty)
|
|
|
|
tests :: TestTree
|
|
tests =
|
|
testGroup "Control.Category.Free"
|
|
[ testProperty "Queue" prop_Queue
|
|
, testProperty "C" prop_C
|
|
, testGroup "Category laws"
|
|
[ 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
|
|
]
|
|
, testGroup "foldFree2 and foldMap"
|
|
[ testProperty "foldFree ListTr" prop_foldListTr
|
|
, testProperty "foldFree Queue" prop_foldQueue
|
|
, testProperty "foldFree C" prop_foldC
|
|
]
|
|
]
|
|
|
|
|
|
data Tr a b where
|
|
-- Num transition
|
|
NumTr :: Num a => (a -> a) -> Tr a a
|
|
FromInteger :: Num b => Tr Integer b
|
|
|
|
-- Integral transition
|
|
ToInteger :: Integral a => Tr a Integer
|
|
|
|
|
|
interpretTr :: Tr a b -> a -> b
|
|
interpretTr (NumTr f) = f
|
|
interpretTr FromInteger = fromInteger
|
|
interpretTr ToInteger = toInteger
|
|
|
|
|
|
instance (Show a, Show b) => Show (Tr a b) where
|
|
show (NumTr f) = "NumTr " ++ show f
|
|
show FromInteger = "FromInteger"
|
|
show ToInteger = "ToInteger"
|
|
|
|
|
|
data SomeNumTr f a where
|
|
SomeNumTr :: Num a
|
|
=> f Tr a a
|
|
-> SomeNumTr f a
|
|
|
|
instance Show (f Tr a a) => Show (SomeNumTr f a) where
|
|
show (SomeNumTr f) = "SomeNumTr " ++ show f
|
|
|
|
|
|
data SomeIntegralTr f a where
|
|
SomeIntegralTr :: Integral a
|
|
=> f Tr a a
|
|
-> SomeIntegralTr f a
|
|
|
|
instance Show (f Tr a a) => Show (SomeIntegralTr f a) where
|
|
show (SomeIntegralTr f) = "SomeIntegralTr " ++ show f
|
|
|
|
|
|
-- A 'fromIntegral' transition in any free category @f@.
|
|
fromIntegralTr :: ( Integral a
|
|
, Num b
|
|
, Category (f Tr)
|
|
, AlgebraType0 f Tr
|
|
, FreeAlgebra2 f
|
|
) => f Tr a b
|
|
fromIntegralTr = liftFree2 FromInteger . liftFree2 ToInteger
|
|
|
|
|
|
data Sing a where
|
|
SInt :: Sing Int
|
|
SInteger :: Sing Integer
|
|
SNatural :: Sing Natural
|
|
|
|
instance Show (Sing a) where
|
|
show SInt = "SInt"
|
|
show SInteger = "SInteger"
|
|
show SNatural = "SNatural"
|
|
|
|
data AnySing where
|
|
AnySing :: Eq a => Sing a -> AnySing
|
|
|
|
instance Eq AnySing where
|
|
AnySing SInt == AnySing SInt = True
|
|
AnySing SInteger == AnySing SInteger = True
|
|
AnySing SNatural == AnySing SNatural = True
|
|
_ == _ = False
|
|
|
|
instance Show AnySing where
|
|
show (AnySing sing) = show sing
|
|
|
|
instance Arbitrary AnySing where
|
|
arbitrary = oneof
|
|
[ pure $ AnySing SInt
|
|
, pure $ AnySing SInteger
|
|
, pure $ AnySing SNatural
|
|
]
|
|
|
|
|
|
instance Arbitrary Natural where
|
|
arbitrary =
|
|
fromIntegral . getPositive <$> (arbitrary :: Gen (Positive Integer))
|
|
|
|
instance CoArbitrary Natural where
|
|
coarbitrary a = variant (fromIntegral a :: Int)
|
|
|
|
data AnyListTr b where
|
|
AnyListTr :: Eq c => ListTr Tr b c -> Sing c -> AnyListTr b
|
|
|
|
|
|
genNextTr :: Sing b
|
|
-> Gen (AnyListTr b)
|
|
genNextTr b = do
|
|
AnySing c <- arbitrary
|
|
case (b, c) of
|
|
(SInt, SInt) ->
|
|
(\f -> AnyListTr (ConsTr (NumTr f) NilTr) c) <$> arbitrary
|
|
(SInteger, SInteger) ->
|
|
(\f -> AnyListTr (ConsTr (NumTr f) NilTr) c) <$> arbitrary
|
|
(SNatural, SNatural) ->
|
|
(\f -> AnyListTr (ConsTr (NumTr f) NilTr) c) <$> arbitrary
|
|
|
|
(SInt, SInteger) ->
|
|
pure $ AnyListTr fromIntegralTr c
|
|
(SInt, SNatural) ->
|
|
pure $ AnyListTr (fromIntegralTr . liftFree2 (NumTr abs)) c
|
|
(SInteger, SInt) ->
|
|
pure $ AnyListTr fromIntegralTr c
|
|
(SNatural, SInt) ->
|
|
pure $ AnyListTr fromIntegralTr c
|
|
(SNatural, SInteger) ->
|
|
pure $ AnyListTr fromIntegralTr c
|
|
(SInteger, SNatural) ->
|
|
pure $ AnyListTr (fromIntegralTr . liftFree2 (NumTr abs)) c
|
|
|
|
|
|
data ArbListTr where
|
|
ArbListTr :: Eq b => ListTr Tr a b -> Sing a -> Sing b -> ArbListTr
|
|
|
|
instance (forall x y. Show (Tr x y)) => Show ArbListTr where
|
|
show (ArbListTr listTr a b) =
|
|
"ArbListTr "
|
|
++ show a
|
|
++ " -> "
|
|
++ show b
|
|
++ " "
|
|
++ show listTr
|
|
|
|
instance Arbitrary ArbListTr where
|
|
arbitrary = sized $ \n -> do
|
|
k <- choose (0, n)
|
|
AnySing a <- arbitrary
|
|
go k a (AnyListTr NilTr a)
|
|
where
|
|
go 0 a (AnyListTr ab b) = pure $ ArbListTr ab a b
|
|
go n a (AnyListTr ab b) = do
|
|
AnyListTr bc c <- genNextTr b
|
|
-- (.) can be used as (++) for ListTr
|
|
go (n - 1) a $ AnyListTr (bc . ab) c
|
|
|
|
|
|
--
|
|
-- test 'Cat' and 'C' treating 'ListTr' as a model to compare to.
|
|
--
|
|
prop_Queue, prop_C
|
|
:: Blind ArbListTr -> Bool
|
|
|
|
|
|
prop_Queue (Blind (ArbListTr listTr SInt _)) =
|
|
foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0
|
|
==
|
|
foldNatFree2 interpretTr listTr 0
|
|
prop_Queue (Blind (ArbListTr listTr SInteger _)) =
|
|
foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0
|
|
==
|
|
foldNatFree2 interpretTr listTr 0
|
|
prop_Queue (Blind (ArbListTr listTr SNatural _)) =
|
|
foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0
|
|
==
|
|
foldNatFree2 interpretTr listTr 0
|
|
|
|
|
|
prop_C (Blind (ArbListTr listTr SInt _)) =
|
|
foldNatFree2 interpretTr (hoistFreeH2 @_ @C listTr) 0
|
|
==
|
|
foldNatFree2 interpretTr listTr 0
|
|
prop_C (Blind (ArbListTr listTr SInteger _)) =
|
|
foldNatFree2 interpretTr (hoistFreeH2 @_ @C listTr) 0
|
|
==
|
|
foldNatFree2 interpretTr listTr 0
|
|
prop_C (Blind (ArbListTr listTr SNatural _)) =
|
|
foldNatFree2 interpretTr (hoistFreeH2 @_ @C listTr) 0
|
|
==
|
|
foldNatFree2 interpretTr listTr 0
|
|
|
|
--
|
|
-- Test Category Laws
|
|
-- @
|
|
-- f . id == f == id . f
|
|
-- f . g . h == (f . g) . h
|
|
-- @
|
|
--
|
|
|
|
prop_id :: Category c
|
|
=> (c a b -> c a b -> Bool)
|
|
-> c a b
|
|
-> Bool
|
|
prop_id eqCat f = eqCat (f . id) f && eqCat (id . f) f
|
|
|
|
prop_associativity :: Category c
|
|
=> (c x w -> c x w -> Bool)
|
|
-> c z w -> c y z -> c x y
|
|
-> Bool
|
|
prop_associativity eqCat f g h =
|
|
(f . g . h) `eqCat` ((f . g) . h)
|
|
|
|
|
|
-- | Integers form commutative monoid, and thus a category (a groupoid to be
|
|
-- precise) with a single object.
|
|
--
|
|
data IntCat (a :: ()) (b :: ()) where
|
|
IntCat :: Int -> IntCat a a
|
|
|
|
instance Show (IntCat a b) where
|
|
show (IntCat i) = "IntCat " ++ show i
|
|
|
|
instance Eq (IntCat a b) where
|
|
IntCat i == IntCat j = i == j
|
|
|
|
instance Category IntCat where
|
|
id = IntCat 0
|
|
IntCat a . IntCat b = IntCat (a + b)
|
|
|
|
instance Semigroup (IntCat '() '()) where
|
|
IntCat a <> IntCat b = IntCat (a + b)
|
|
|
|
instance Monoid (IntCat '() '()) where
|
|
mempty = IntCat 0
|
|
|
|
instance Arbitrary (IntCat '() '()) where
|
|
arbitrary = IntCat <$> arbitrary
|
|
|
|
fromList :: forall k (a :: k) m f.
|
|
( FreeAlgebra2 m
|
|
, AlgebraType0 m f
|
|
, Category (m f)
|
|
) => [f a a] -> m f a a
|
|
fromList [] = id
|
|
fromList (f : fs) = liftFree2 f . fromList fs
|
|
|
|
toList :: ( FreeAlgebra2 m
|
|
, AlgebraType0 m IntCat
|
|
, AlgebraType m (ListTr IntCat)
|
|
)
|
|
=> m IntCat '() '()
|
|
-> [IntCat '() '()]
|
|
toList c = go (hoistFreeH2 c)
|
|
where
|
|
go :: ListTr IntCat '() '() -> [IntCat '() '()]
|
|
go NilTr = []
|
|
go (ConsTr tr@IntCat{} xs) = tr : go xs
|
|
|
|
--
|
|
-- 'C' category laws
|
|
--
|
|
|
|
newtype ArbIntC = ArbIntC (C IntCat '() '())
|
|
|
|
instance Show ArbIntC where
|
|
show (ArbIntC c) = show c
|
|
|
|
instance Arbitrary ArbIntC where
|
|
arbitrary = ArbIntC . fromList <$> arbitrary
|
|
shrink (ArbIntC c) =
|
|
map (ArbIntC . fromList)
|
|
$ shrinkList (const [])
|
|
$ toList c
|
|
|
|
prop_id_C :: ArbIntC -> Bool
|
|
prop_id_C (ArbIntC f) =
|
|
prop_id (on (==) toList) f
|
|
|
|
prop_associativity_C
|
|
:: ArbIntC -> ArbIntC -> ArbIntC
|
|
-> Bool
|
|
prop_associativity_C (ArbIntC f0)
|
|
(ArbIntC f1)
|
|
(ArbIntC f2) =
|
|
prop_associativity (on (==) toList) f0 f1 f2
|
|
|
|
--
|
|
-- 'Queue' category laws
|
|
--
|
|
|
|
newtype ArbIntQueue = ArbIntQueue (Queue IntCat '() '())
|
|
|
|
instance Show ArbIntQueue where
|
|
show (ArbIntQueue f) = show (toList f)
|
|
|
|
instance Arbitrary ArbIntQueue where
|
|
arbitrary = ArbIntQueue . fromList <$> arbitrary
|
|
shrink (ArbIntQueue c) =
|
|
map (ArbIntQueue . fromList)
|
|
$ shrinkList (const [])
|
|
$ toList c
|
|
|
|
prop_id_Queue :: ArbIntQueue -> Bool
|
|
prop_id_Queue (ArbIntQueue f) =
|
|
prop_id (on (==) toList) f
|
|
|
|
prop_associativity_Queue
|
|
:: ArbIntQueue -> ArbIntQueue -> ArbIntQueue
|
|
-> Bool
|
|
prop_associativity_Queue (ArbIntQueue f0)
|
|
(ArbIntQueue f1)
|
|
(ArbIntQueue f2) =
|
|
prop_associativity (on (==) toList) f0 f1 f2
|
|
|
|
--
|
|
-- 'ListTr' category laws
|
|
--
|
|
|
|
newtype ArbIntListTr = ArbIntListTr (ListTr IntCat '() '())
|
|
|
|
instance Show ArbIntListTr where
|
|
show (ArbIntListTr f) = show (toList f)
|
|
|
|
instance Arbitrary ArbIntListTr where
|
|
arbitrary = ArbIntListTr . fromList <$> arbitrary
|
|
shrink (ArbIntListTr c) =
|
|
map (ArbIntListTr . fromList)
|
|
$ shrinkList (const [])
|
|
$ toList c
|
|
|
|
prop_id_ListTr :: ArbIntListTr -> Bool
|
|
prop_id_ListTr (ArbIntListTr f) =
|
|
prop_id (on (==) toList) f
|
|
|
|
prop_associativity_ListTr
|
|
:: ArbIntListTr -> ArbIntListTr -> ArbIntListTr
|
|
-> Bool
|
|
prop_associativity_ListTr (ArbIntListTr f0)
|
|
(ArbIntListTr f1)
|
|
(ArbIntListTr f2) =
|
|
prop_associativity (on (==) toList) f0 f1 f2
|
|
|
|
|
|
--
|
|
-- Compatibility between 'foldFree2' and 'foldMap' for 'IntCat'
|
|
--
|
|
|
|
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_foldC :: (Blind ArbIntC) -> Bool
|
|
prop_foldC (Blind (ArbIntC f))
|
|
= foldFree2 f == foldMap id (toList f)
|