Add MFunctor test cases

lib/Function.hs

@@ -7,6 +7,8 @@ module Function
     , law_MCategory_comp_id_right
     , law_MCategory_comp_assoc
     , MFunctor(..)
+    , law_MFunctor_id
+    , law_MFunctor_assoc
     , type (-.>)(..)
     , NList(..)
     ) where
@@ -18,6 +20,7 @@ import Data.Constraint
 import Data.Kind
 import qualified Data.Vector.Unboxed as U ()
 import GHC.Generics
+import qualified Test.QuickCheck as QC
 
 
 
@@ -86,8 +89,6 @@ class MCategory (k :: CatKind) where
     type Obj k :: ObjKind
     type Obj k = k
 
-
-
 -- id . f = f
 law_MCategory_comp_id_left :: Ok m a b => a `m` b -> FnEqual a b
 law_MCategory_comp_id_left f = (MId .:. f) `fnEqual` f
@@ -116,6 +117,24 @@ class ( MCategory (Dom f), MCategory (Cod f)
             , n ~ Mor f
             ) => a `m` b -> f a `n` f b
 
+-- fmap id = id
+law_MFunctor_id :: forall f a. (MFunctor f, Obj (Dom f) a)
+                   => FnEqual (f a) (f a)
+law_MFunctor_id =
+    fmap (MId :: MId (Dom f) a a) `fnEqual` (MId :: MId (Cod f) (f a) (f a))
+       \\ (proveCod :: Obj (Dom f) a :- Obj (Cod f) (f a))
+
+-- fmap (f . g) = fmap f . fmap g
+law_MFunctor_assoc :: forall f m n a b c.
+                     ( MFunctor f
+                     , Cat m ~ Dom f, Cat n ~ Dom f
+                     , Ok m a b, Ok n b c
+                     ) => b `n` c -> a `m` b -> FnEqual (f a) (f c)
+law_MFunctor_assoc g f = fmap (g .:. f) `fnEqual` (fmap g .:. fmap f)
+                         \\ (proveCod :: Obj (Dom f) a :- Obj (Cod f) (f a))
+                         \\ (proveCod :: Obj (Dom f) b :- Obj (Cod f) (f b))
+                         \\ (proveCod :: Obj (Dom f) c :- Obj (Cod f) (f c))
+
 
 
 -- | Hask
@@ -164,7 +183,7 @@ instance Discretization (-.>) where
     discretize = NFun
 
 newtype NList a = NList { getNList :: [a] }
-    deriving (Eq, Ord, Read, Show, Generic)
+    deriving (Eq, Ord, Read, Show, Generic, QC.Arbitrary, QC.CoArbitrary)
 
 instance MFunctor NList where
     type Dom NList = Num

lib/Functor.hs

@@ -44,7 +44,7 @@ law_Functor_id = fmap id `fnEqual` (id @(Cod f))
 law_Functor_assoc :: forall f a b c.
                      (Functor f, Obj (Dom f) a, Obj (Dom f) b, Obj (Dom f) c)
                      => Dom f b c -> Dom f a b -> FnEqual (f a) (f c)
-law_Functor_assoc g f = (fmap (g . f) `fnEqual` (fmap g . fmap f))
+law_Functor_assoc g f = fmap (g . f) `fnEqual` (fmap g . fmap f)
                         \\ (proveCod :: Obj (Dom f) a :- Obj (Cod f) (f a))
                         \\ (proveCod :: Obj (Dom f) b :- Obj (Cod f) (f b))
                         \\ (proveCod :: Obj (Dom f) c :- Obj (Cod f) (f c))

test/FunctionSpec.hs

@@ -23,6 +23,29 @@ prop_Hask_MCategory_comp_assoc (Fn h) (Fn g) (Fn f) x =
 
 
 
+prop_List_MFunctor_id :: [A] -> Property
+prop_List_MFunctor_id xs =
+    uncurry (===) (getFnEqual law_MFunctor_id xs)
+
+prop_List_MFunctor_assoc :: Fun B C -> Fun A B -> [A] -> Property
+prop_List_MFunctor_assoc (Fn g) (Fn f) xs =
+    uncurry (===) (getFnEqual (law_MFunctor_assoc g f) xs)
+
+
+
+prop_Function_MFunctor_id :: Fun B A -> NonEmptyList B -> Property
+prop_Function_MFunctor_id (Fn xs) (NonEmpty bs) =
+    let (u, v) = getFnEqual law_MFunctor_id xs
+    in conjoin [u b === v b | b <- bs]
+
+prop_Function_MFunctor_assoc ::
+    Fun B C -> Fun A B -> Fun B A -> NonEmptyList B -> Property
+prop_Function_MFunctor_assoc (Fn g) (Fn f) (Fn xs) (NonEmpty bs) =
+    let (u, v) = getFnEqual (law_MFunctor_assoc g f) xs
+    in conjoin [u b === v b | b <- bs]
+
+
+
 newtype NA = NA Integer
     deriving (Eq, Ord, Read, Show, Num, Arbitrary, CoArbitrary)
 instance Function NA where
@@ -51,3 +74,26 @@ prop_Num_MCategory_comp_assoc ::
 prop_Num_MCategory_comp_assoc (Fn h) (Fn g) (Fn f) x =
     uncurry (===) (getFnEqual (law_MCategory_comp_assoc
                                       (NFun h) (NFun g) (NFun f)) x)
+
+
+
+prop_NList_MFunctor_id :: NList NA -> Property
+prop_NList_MFunctor_id xs =
+    uncurry (===) (getFnEqual law_MFunctor_id xs)
+
+prop_NList_MFunctor_assoc :: Fun NB NC -> Fun NA NB -> NList NA -> Property
+prop_NList_MFunctor_assoc (Fn g) (Fn f) xs =
+    uncurry (===) (getFnEqual (law_MFunctor_assoc (NFun g) (NFun f)) xs)
+
+
+
+prop_NFun_MFunctor_id :: Fun NB NA -> NonEmptyList NB -> Property
+prop_NFun_MFunctor_id (Fn xs) (NonEmpty bs) =
+    let (u, v) = getFnEqual law_MFunctor_id (NFun xs)
+    in conjoin [chase u b === chase v b | b <- bs]
+
+prop_NFun_MFunctor_assoc ::
+    Fun NB NC -> Fun NA NB -> Fun NB NA -> NonEmptyList NB -> Property
+prop_NFun_MFunctor_assoc (Fn g) (Fn f) (Fn xs) (NonEmpty bs) =
+    let (u, v) = getFnEqual (law_MFunctor_assoc (NFun g) (NFun f)) (NFun xs)
+    in conjoin [chase u b === chase v b | b <- bs]