Check more laws

lib/Applicative.hs

@@ -6,6 +6,10 @@ module Applicative
     , law_Applicative_comp
     , law_Applicative_homo
     , law_Applicative_inter
+    , law_Applicative_id'
+    , law_Applicative_id_left'
+    , law_Applicative_id_right'
+    , law_Applicative_assoc'
     , (<$>)
     , ZipList(..)
     ) where
@@ -96,6 +100,109 @@ law_Applicative_inter :: (Applicative f, Dom f ~ Cod f, Cod f ~ (->))
                          => f (Dom f a b) -> a -> Equal (f b)
 law_Applicative_inter fs x = (fs <*> pure x) `equal` (pure ($ x) <*> fs)
 
+-- f :: a -> b
+-- x :: a
+-- liftA2' (\((), x) -> f x) (pure (), xs) = fmap f xs
+law_Applicative_id' :: forall f a b k p u l q.
+                       ( Applicative f
+                       , Cartesian (Dom f), Cartesian (Cod f)
+                       , Obj (Dom f) a, Obj (Dom f) b
+                       , Cod f ~ (->)
+                       , k ~ Dom f, p ~ Prod k, u ~ Unit p
+                       , l ~ Cod f, q ~ Prod l
+                       ) => a `k` b -> f a -> Equal (f b)
+law_Applicative_id' f xs =
+    liftA2' f' xs' `equal` fmap f xs
+    where
+      f' :: p u a `k` b
+      f' = unapply (\p -> let (_, x) = unprod p in f `apply` x)
+           \\ (proveCartesian @k :: (Obj k u, Obj k a) :- Obj k (p u a))
+      xs' :: q (f u) (f a)
+      xs' = prod (pure (punit @p), xs)
+
+-- f :: (a, b) -> c
+-- x :: a
+-- ys :: f b
+-- liftA2' f (pure x, ys) = fmap (\x -> f (x, y)) ys
+law_Applicative_id_left' ::
+    forall f a b c k p.
+       ( Applicative f, Cartesian (Dom f), Cartesian (Cod f)
+       , Obj (Dom f) a, Obj (Dom f) b, Obj (Dom f) c
+       , Cod f ~ (->)
+       , k ~ Dom f, p ~ Prod k
+       ) => p a b `k` c -> a -> f b -> Equal (f c)
+law_Applicative_id_left' f x ys =
+    liftA2' f (prod (pure x, ys)) `equal`
+    fmap (unapply (\y -> f `apply` prod (x, y))) ys
+       \\ (proveCartesian @k :: (Obj k a, Obj k b) :- Obj k (p a b))
+
+-- liftA2' f (xs, pure y) = fmap (\y -> f (x, y)) xs
+-- f :: (a, b) -> c
+-- xs :: f a
+-- y :: b
+law_Applicative_id_right' ::
+    forall f a b c k p.
+       ( Applicative f, Cartesian (Dom f), Cartesian (Cod f)
+       , Obj (Dom f) a, Obj (Dom f) b, Obj (Dom f) c
+       , Cod f ~ (->)
+       , k ~ Dom f, p ~ Prod k
+       ) => p a b `k` c -> f a -> b -> Equal (f c)
+law_Applicative_id_right' f xs y =
+    liftA2' f (prod (xs, pure y)) `equal`
+    fmap (unapply (\x -> f `apply` prod (x, y))) xs
+       \\ (proveCartesian @k :: (Obj k a, Obj k b) :- Obj k (p a b))
+
+-- f :: a -> a'
+-- g :: b -> b'
+-- h :: c -> c'
+-- i :: (a', (b', c')) -> d
+-- liftA2' hi (liftA2' fg (xs, ys), zs) = liftA2' fi (xs, liftA2' gh (ys, zs))
+law_Applicative_assoc' ::
+    forall f a a' b b' c c' d k p.
+       ( Applicative f, Cartesian (Dom f), Cartesian (Cod f)
+       , Obj (Dom f) a, Obj (Dom f) b, Obj (Dom f) c, Obj (Dom f) d
+       , Obj (Dom f) a', Obj (Dom f) b', Obj (Dom f) c'
+       , Cod f ~ (->)
+       , k ~ Dom f, p ~ Prod k
+       ) => a `k` a' -> b `k` b' -> c `k` c' -> (p a' (p b' c')) `k` d ->
+            f a -> f b -> f c -> Equal (f d)
+law_Applicative_assoc' f g h i xs ys zs =
+    liftA2' hi (liftA2' fg (xs, ys), zs) `equal`
+    liftA2' fi (xs, liftA2' gh (ys, zs))
+       \\ (proveCartesian @k :: (Obj k a', Obj k b') :- Obj k (p a' b'))
+       \\ (proveCartesian @k :: (Obj k b', Obj k c') :- Obj k (p b' c'))
+    where fg :: p a b `k` p a' b'
+          fg = unapply (\p -> let (x, y) = unprod p
+                              in prod (f `apply` x, g `apply` y))
+               \\ (proveCartesian @k :: (Obj k a, Obj k b) :- Obj k (p a b))
+               \\ (proveCartesian @k :: (Obj k a', Obj k b') :- Obj k (p a' b'))
+          hi :: p (p a' b') c `k` d
+          hi = unapply (\p -> let (q', z) = unprod p
+                                  (x', y') = unprod q'
+                                  r' = prod (x', prod (y', h `apply` z))
+                              in i `apply` r')
+               \\ (proveCartesian @k ::
+                       (Obj k (p a' b'), Obj k c) :- Obj k (p (p a' b') c))
+               \\ (proveCartesian @k :: (Obj k a', Obj k b') :- Obj k (p a' b'))
+               \\ (proveCartesian @k ::
+                       (Obj k a', Obj k (p b' c')) :- Obj k (p a' (p b' c')))
+               \\ (proveCartesian @k :: (Obj k b', Obj k c') :- Obj k (p b' c'))
+          gh :: p b c `k` p b' c'
+          gh = unapply (\p -> let (y, z) = unprod p
+                              in prod (g `apply` y, h `apply` z))
+               \\ (proveCartesian @k :: (Obj k b, Obj k c) :- Obj k (p b c))
+               \\ (proveCartesian @k :: (Obj k b', Obj k c') :- Obj k (p b' c'))
+          fi :: p a (p b' c') `k` d
+          fi = unapply (\p -> let (x, q') = unprod p
+                                  (y', z') = unprod q'
+                                  r' = prod (f `apply` x, prod (y', z'))
+                              in i `apply` r')
+               \\ (proveCartesian @k ::
+                       (Obj k a, Obj k (p b' c')) :- Obj k (p a (p b' c')))
+               \\ (proveCartesian @k ::
+                       (Obj k a', Obj k (p b' c')) :- Obj k (p a' (p b' c')))
+               \\ (proveCartesian @k :: (Obj k b', Obj k c') :- Obj k (p b' c'))
+
 
 
 infixl 4 <$>
@@ -175,3 +282,9 @@ instance Applicative ZipList where
         in ZipList (f x y : rs)
     liftA2 _ _ _ = ZipList []
     -- liftA2 f (ZipList xs) (ZipList ys) = ZipList (zipWith f xs ys)
+
+instance Applicative NList where
+    pure x = NList [x]
+    (<*>) = undefined
+    liftA2' f (NList xs, NList ys) =
+        NList [f `apply` NProd x y | x <- xs, y <- ys]

lib/Category.hs

@@ -1,3 +1,6 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
 module Category
     ( Equal(..)
     , equal
@@ -17,6 +20,8 @@ module Category
     , Closed(..)
     , Hask
     , type (-#>)(..)
+    , type (*#*)(..), NUnit(..)
+    -- , type (+#+)(..), NCounit()
     ) where
 
 import Prelude hiding (id, (.), curry, uncurry)
@@ -25,6 +30,8 @@ import qualified Prelude
 import Data.Constraint
 import Data.Kind
 import Data.Void
+import GHC.Generics
+import qualified Test.QuickCheck as QC
 
 
 
@@ -99,7 +106,8 @@ class CatProd (p :: ProdKind) where
     -- preassoc p = let (q, z) = unprod p
     --                  (x, y) = unprod q
     --              in prod (x, prod (y, z))
-class (Category k, CatProd (Prod k)) => Cartesian k where
+class (Category k, CatProd (Prod k), Obj k (Unit (Prod k)))
+        => Cartesian k where
     type Prod k :: ProdKind
     proveCartesian :: (Obj k a, Obj k b) :- Obj k (Prod k a b)
 
@@ -114,7 +122,8 @@ class CatCoprod (p :: CoprodKind) where
     --            => p a (p b c) -> p (p a b) c
     -- recoassoc :: (Obj k a, Obj k b, Obj k c, p ~ Coprod k)
     --              => p (p a b) c -> p a (p b c)
-class (Category k, CatCoprod (Coprod k)) => Cocartesian k where
+class (Category k, CatCoprod (Coprod k), Obj k (Counit (Coprod k)))
+        => Cocartesian k where
     type Coprod k :: Type -> Type -> Type
     proveCocartesian :: (Obj k a, Obj k b) :- Obj k (Coprod k a b)
 
@@ -174,9 +183,85 @@ instance Closed (->) where
 -- | Num is a category
 newtype (-#>) a b = NFun { unNFun :: (Num a, Num b) => a -> b }
 
+data (*#*) a b = NProd a b
+                 deriving (Eq, Ord, Read, Show, Generic)
+instance QC.Arbitrary (a, b) => QC.Arbitrary (a *#* b) where
+    arbitrary = prod Prelude.<$> QC.arbitrary
+    shrink p = prod Prelude.<$> QC.shrink (unprod p)
+instance (QC.CoArbitrary a, QC.CoArbitrary b) => QC.CoArbitrary (a *#* b)
+instance QC.Function (a, b) => QC.Function (a *#* b) where
+    function = QC.functionMap unprod prod
+
+instance (Num a, Num b) => Num (a *#* b) where
+    NProd x1 x2 + NProd y1 y2 = NProd (x1 + y1) (x2 + y2)
+    NProd x1 x2 * NProd y1 y2 = NProd (x1 * y1) (x2 * y2)
+    negate (NProd x y) = NProd (negate x) (negate y)
+    abs (NProd x y) = NProd (abs x) (abs y)
+    signum (NProd x y) = NProd (signum x) (signum y)
+    fromInteger n = NProd (fromInteger n) (fromInteger n)
+
+data NUnit = NUnit
+             deriving (Eq, Ord, Read, Show, Generic)
+
+instance QC.Arbitrary NUnit where
+    arbitrary = return NUnit
+    shrink NUnit = []
+instance QC.CoArbitrary NUnit
+instance QC.Function NUnit where
+    function = QC.functionMap (const ()) (const NUnit)
+
+instance Num NUnit where
+    NUnit + NUnit = NUnit
+    NUnit * NUnit = NUnit
+    negate NUnit = NUnit
+    abs NUnit = NUnit
+    signum NUnit = NUnit
+    fromInteger _ = NUnit
+
 instance Category (-#>) where
     type Obj (-#>) = Num
     id = NFun id
     NFun g . NFun f = NFun (g . f)
     apply = unNFun
     unapply = NFun
+
+instance CatProd (*#*) where
+    type Unit (*#*) = NUnit
+    punit = NUnit
+    prod (a, b) = NProd a b
+    unprod (NProd a b) = (a, b)
+
+instance Cartesian (-#>) where
+    type Prod (-#>) = (*#*)
+    proveCartesian = Sub Dict
+
+-- data (+#+) a b = NLeft a | NRight b
+--                  deriving (Eq, Ord, Read, Show)
+-- instance (Num a, Num b) => Num (a +#+ b) where
+--     NLeft x + NLeft y = NLeft (x + y)
+--     NRight x + NRight y = NRight (x + y)
+--     NLeft x + _ = NLeft x
+--     _ + NLeft y = NLeft y
+--     NLeft x * NLeft y = NLeft (x * y)
+--     NRight x * NRight y = NRight (x * y)
+--     NLeft x * _ = NLeft x
+--     _ * NLeft y = NLeft y
+--     negate (NLeft x) = NLeft (negate x)
+--     negate (NRight x) = NRight (negate x)
+--     abs (NLeft x) = NLeft (abs x)
+--     abs (NRight x) = NRight (abs x)
+--     signum (NLeft x) = NLeft (signum x)
+--     signum (NRight x) = NRight (signum x)
+--     fromInteger n = NLeft (fromInteger n)
+-- 
+-- data NCounit
+-- instance CatCoprod (+#+) where
+--     type Counit (+#+) = NCounit
+--     coprod (Left a) = NLeft a
+--     coprod (Right b) = NRight b
+--     uncoprod (NLeft a) = Left a
+--     uncoprod (NRight b) = Right b
+-- 
+-- instance Cocartesian (-#>) where
+--     type Coprod (-#>) = (+#+)
+--     proveCocartesian = Sub Dict

lib/Comonad.hs

@@ -8,6 +8,7 @@ module Comonad
 import Prelude hiding ( id, (.), curry, uncurry
                       , Functor(..)
                       )
+
 import Data.Functor.Identity
 import Data.Functor.Product as F
 import Data.Functor.Sum as F

lib/Functor.hs

@@ -4,6 +4,7 @@ module Functor
     ( Functor(..)
     , law_Functor_id
     , law_Functor_assoc
+    , NList(..)
     ) where
 
 import Prelude hiding ( id, (.), curry, uncurry
@@ -19,6 +20,7 @@ import Data.Functor.Product as F
 import Data.Functor.Sum as F
 import Data.List.NonEmpty
 import Data.Proxy
+import qualified Test.QuickCheck as QC
 
 import Category
 
@@ -136,3 +138,14 @@ instance Functor ZipList where
     type Cod ZipList = Cod []
     proveCod = Sub Dict
     fmap f (ZipList xs) = ZipList (fmap f xs)
+
+
+
+newtype NList a = NList [a]
+    deriving (Eq, Ord, Read, Show, QC.Arbitrary, QC.Arbitrary1)
+
+instance Functor NList where
+    type Dom NList = (-#>)
+    type Cod NList = (->)
+    proveCod = Sub Dict
+    fmap f (NList xs) = NList (fmap (apply f) xs)