Direct encoding of laws as tests

Author: sjoerdvisscher

proarrow.cabal

@@ -107,7 +107,6 @@ library
         Proarrow.Core
         Proarrow.Functor
         Proarrow.Tools.CCC
-        Proarrow.Tools.Laws
         Proarrow.Monoid
         Proarrow.Object
         Proarrow.Object.BinaryProduct
@@ -168,6 +167,7 @@ test-suite test
     other-modules:
         Props
         Props.Bool
+        Props.Free
         Props.Hask
         Props.Kleisli
         Props.Linear

src/Proarrow/Category/Monoidal.hs

@@ -3,7 +3,7 @@
 module Proarrow.Category.Monoidal where
 
 import Data.Kind (Constraint)
-import Prelude (Eq, Show, ($), (++))
+import Prelude (Eq, Show, ($))
 
 import Proarrow.Category.Instance.Free
   ( Elem
@@ -14,13 +14,11 @@ import Proarrow.Category.Instance.Free
   , Ok
   , WithEq
   , WithShow
-  , emb
   )
 import Proarrow.Category.Instance.Product ((:**:) (..))
 import Proarrow.Category.Instance.Unit qualified as U
 import Proarrow.Core (CAT, CategoryOf (..), Kind, Obj, Profunctor (..), Promonad (..), obj, src, tgt, type (+->))
 import Proarrow.Functor (FunctorForRep (..))
-import Proarrow.Tools.Laws (AssertEq (..), Laws (..), Var, iso)
 
 -- This is equal to a monoidal functor for representable profunctors
 -- and to an oplax monoidal functor for corepresentable profunctors.
@@ -209,62 +207,6 @@ deriving instance (WithShow a) => Show (Struct SymMonoidal a b)
 instance (Ok cs p, SymMonoidal `Elem` cs, Monoidal `Elem` cs) => SymMonoidal (FREE cs p) where
   swap = Str Swap Id
 
-data instance Var '[Monoidal] a b where
-  F :: Var '[Monoidal] "A" "B"
-  G :: Var '[Monoidal] "B" "C"
-  H :: Var '[Monoidal] "C" "D"
-deriving instance Show (Var '[Monoidal] a b)
-instance Laws '[Monoidal] where
-  type
-    EqTypes '[Monoidal] =
-      '[ EMB "A"
-       , EMB "B"
-       , UnitF **! EMB "A"
-       , UnitF **! EMB "B"
-       , EMB "A" **! UnitF
-       , EMB "B" **! UnitF
-       , EMB "A" **! EMB "B"
-       , (EMB "A" **! UnitF) **! EMB "B"
-       , (EMB "A" **! EMB "B") **! EMB "C"
-       , EMB "A" **! (EMB "B" **! EMB "C")
-       , (EMB "B" **! EMB "C") **! EMB "D"
-       , EMB "B" **! (EMB "C" **! EMB "D")
-       , EMB "A" **! (EMB "B" **! (EMB "C" **! EMB "D"))
-       , ((EMB "A" **! EMB "B") **! EMB "C") **! EMB "D"
-       ]
-  laws =
-    let f = emb F; g = emb G; h = emb H
-    in iso @((EMB "A" **! EMB "B") **! EMB "C") @(EMB "A" **! (EMB "B" **! EMB "C")) associator associatorInv
-         ++ iso @(UnitF **! EMB "A") @(EMB "A") leftUnitor leftUnitorInv
-         ++ iso @(EMB "A" **! UnitF) @(EMB "A") rightUnitor rightUnitorInv
-         ++ [ associator . ((f `par` g) `par` h) :=: (f `par` (g `par` h)) . associator
-            , associatorInv . (f `par` (g `par` h)) :=: ((f `par` g) `par` h) . associatorInv
-            , leftUnitor . (par0 `par` f) :=: f . leftUnitor
-            , leftUnitorInv . f :=: (par0 `par` f) . leftUnitorInv
-            , rightUnitor . (f `par` par0) :=: f . rightUnitor
-            , rightUnitorInv . f :=: (f `par` par0) . rightUnitorInv
-            , (id `par` leftUnitor) . associator @_ @(EMB "A") @_ @(EMB "B") :=: rightUnitor `par` id
-            , (id `par` associator @_ @(EMB "B") @(EMB "C") @(EMB "D"))
-                . associator
-                . (associator @_ @(EMB "A") @(EMB "B") @(EMB "C") `par` id)
-                :=: associator . associator
-            ]
-
-data instance Var '[Monoidal, SymMonoidal] a b
-deriving instance Show (Var '[Monoidal, SymMonoidal] a b)
-instance Laws '[Monoidal, SymMonoidal] where
-  type
-    EqTypes '[Monoidal, SymMonoidal] =
-      '[ EMB "A" **! EMB "B"
-       , (EMB "A" **! EMB "B") **! EMB "C"
-       , EMB "B" **! (EMB "C" **! EMB "A")
-       ]
-  laws =
-    [ swap @_ @(EMB "B") @(EMB "A") . swap :=: id
-    , (id `par` swap) . associator . (swap `par` id)
-        :=: associator . swap . associator @_ @(EMB "A") @(EMB "B") @(EMB "C")
-    ]
-
 data UnitFtor :: () +-> k
 instance (Monoidal k) => FunctorForRep (UnitFtor :: () +-> k) where
   type UnitFtor @ '() = Unit

src/Proarrow/Object/BinaryCoproduct.hs

@@ -16,7 +16,6 @@ import Proarrow.Category.Instance.Free
   , Ok
   , WithEq
   , WithShow
-  , emb
   )
 import Proarrow.Category.Instance.Free qualified as F
 import Proarrow.Category.Instance.Prof (Prof (..))
@@ -33,7 +32,6 @@ import Proarrow.Profunctor.Corepresentable (Corepresentable (..), withCorepOb)
 import Proarrow.Profunctor.Identity (Id (..))
 import Proarrow.Profunctor.Product ((:*:) (..))
 import Proarrow.Profunctor.Terminal (TerminalProfunctor (..))
-import Proarrow.Tools.Laws (AssertEq (..), Laws (..), Var)
 
 infixl 4 ||
 infixl 4 |||
@@ -230,17 +228,3 @@ instance (Ok cs p, HasBinaryCoproducts `Elem` cs) => HasBinaryCoproducts (FREE c
   lft = Str Lft F.Id
   rgt = Str Rgt F.Id
   f ||| g = Str (Sum f g) F.Id \\ f \\ g
-
-data instance Var '[HasBinaryCoproducts] a b where
-  F :: Var '[HasBinaryCoproducts] "A" "C"
-  G :: Var '[HasBinaryCoproducts] "B" "C"
-  H :: Var '[HasBinaryCoproducts] "C" "Z"
-deriving instance Show (Var '[HasBinaryCoproducts] a b)
-instance Laws '[HasBinaryCoproducts] where
-  type EqTypes '[HasBinaryCoproducts] = '[EMB "A", EMB "B", EMB "C", EMB "Z", EMB "A" + EMB "B"]
-  laws =
-    let f = emb F; g = emb G; h = emb H
-    in [ (f ||| g) . lft :=: f
-       , (f ||| g) . rgt :=: g
-       , (h . f) ||| (h . g) :=: h . (f ||| g)
-       ]

src/Proarrow/Object/BinaryProduct.hs

@@ -16,7 +16,6 @@ import Proarrow.Category.Instance.Free
   , Ok
   , WithEq
   , WithShow
-  , emb
   )
 import Proarrow.Category.Instance.Product (Fst, Snd, (:**:) (..))
 import Proarrow.Category.Instance.Prof (Prof (..))
@@ -31,7 +30,6 @@ import Proarrow.Object.Terminal (HasTerminalObject (..), Semicartesian)
 import Proarrow.Profunctor.Identity qualified as Id
 import Proarrow.Profunctor.Product (prod, (:*:) (..))
 import Proarrow.Profunctor.Representable (Representable (..), withRepOb)
-import Proarrow.Tools.Laws (AssertEq (..), Laws (..), Var)
 
 infixl 5 &&
 infixl 5 &&&
@@ -268,17 +266,3 @@ instance (Ok cs p, HasBinaryProducts `Elem` cs) => HasBinaryProducts (FREE cs p)
   fst = Str Fst Id
   snd = Str Snd Id
   f &&& g = Str (Prd f g) Id \\ f \\ g
-
-data instance Var '[HasBinaryProducts] a b where
-  F :: Var '[HasBinaryProducts] "A" "B"
-  G :: Var '[HasBinaryProducts] "A" "C"
-  H :: Var '[HasBinaryProducts] "Z" "A"
-deriving instance Show (Var '[HasBinaryProducts] a b)
-instance Laws '[HasBinaryProducts] where
-  type EqTypes '[HasBinaryProducts] = '[EMB "A", EMB "B", EMB "C", EMB "Z", EMB "B" *! EMB "C"]
-  laws =
-    let f = emb F; g = emb G; h = emb H
-    in [ fst . (f &&& g) :=: f
-       , snd . (f &&& g) :=: g
-       , (f . h) &&& (g . h) :=: (f &&& g) . h
-       ]

src/Proarrow/Object/Initial.hs

@@ -4,14 +4,13 @@ import Data.Kind (Type)
 import Data.Void (Void, absurd)
 import Prelude (Eq, Show, type (~))
 
-import Proarrow.Category.Instance.Free (Elem, FREE (..), Free (..), HasStructure (..), IsFreeOb (..), Ok, emb)
+import Proarrow.Category.Instance.Free (Elem, FREE (..), Free (..), HasStructure (..), IsFreeOb (..), Ok)
 import Proarrow.Category.Instance.Product ((:**:) (..))
 import Proarrow.Category.Instance.Prof (Prof (..))
 import Proarrow.Category.Instance.Unit (Unit (..))
 import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
 import Proarrow.Object.Terminal (HasTerminalObject (..))
 import Proarrow.Profunctor.Initial (InitialProfunctor)
-import Proarrow.Tools.Laws (AssertEq (..), Laws (..), Var)
 
 class (CategoryOf k, Ob (InitialObject :: k)) => HasInitialObject k where
   type InitialObject :: k
@@ -54,10 +53,3 @@ deriving instance Show (Struct HasInitialObject a b)
 instance (Ok cs p, HasInitialObject `Elem` cs) => HasInitialObject (FREE cs p) where
   type InitialObject = InitF
   initiate = Str Initial Id
-
-data instance Var '[HasInitialObject] a b where
-  F :: Var '[HasInitialObject] "A" "B"
-deriving instance Show (Var '[HasInitialObject] a b)
-instance Laws '[HasInitialObject] where
-  type EqTypes '[HasInitialObject] = '[EMB "B", InitF]
-  laws = [emb F . initiate :=: initiate]

src/Proarrow/Object/Terminal.hs

@@ -3,14 +3,13 @@ module Proarrow.Object.Terminal where
 import Data.Kind (Type)
 import Prelude (Eq, Show, type (~))
 
-import Proarrow.Category.Instance.Free (Elem, FREE (..), Free (..), HasStructure (..), IsFreeOb (..), Ok, emb)
+import Proarrow.Category.Instance.Free (Elem, FREE (..), Free (..), HasStructure (..), IsFreeOb (..), Ok)
 import Proarrow.Category.Instance.Product ((:**:) (..))
 import Proarrow.Category.Instance.Prof (Prof (..))
 import Proarrow.Category.Instance.Unit qualified as U
 import Proarrow.Category.Monoidal (Monoidal (..))
 import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
 import Proarrow.Profunctor.Terminal (TerminalProfunctor (..))
-import Proarrow.Tools.Laws (AssertEq (..), Laws (..), Var)
 
 class (CategoryOf k, Ob (TerminalObject :: k)) => HasTerminalObject k where
   type TerminalObject :: k
@@ -54,10 +53,3 @@ deriving instance Show (Struct HasTerminalObject a b)
 instance (Ok cs p, HasTerminalObject `Elem` cs) => HasTerminalObject (FREE cs p) where
   type TerminalObject = TermF
   terminate = Str Terminate Id
-
-data instance Var '[HasTerminalObject] a b where
-  F :: Var '[HasTerminalObject] "A" "B"
-deriving instance Show (Var '[HasTerminalObject] a b)
-instance Laws '[HasTerminalObject] where
-  type EqTypes '[HasTerminalObject] = '[EMB "A", TermF]
-  laws = [terminate . emb F :=: terminate]

src/Proarrow/Squares/Limit.hs

@@ -22,12 +22,6 @@ import Proarrow.Squares
   , hId
   , hSplitAll
   , toRight
-  , vArr
-  , vCombine
-  , vId
-  , vSplit
-  , vUnitor
-  , vUnitorInv
   , (===)
   , (|||)
   )

src/Proarrow/Tools/Laws.hs

@@ -6,6 +6,7 @@ import Test.Tasty (defaultMain, testGroup)
 import Prelude
 
 import Props.Bool qualified as Bool
+import Props.Free qualified as Free
 import Props.Hask qualified as Hask
 import Props.Kleisli qualified as Kleisli
 import Props.Linear qualified as Linear
@@ -20,6 +21,7 @@ main =
     testGroup
       "Proarrow"
       [ Bool.test
+      , Free.test
       , Hask.test
       , Linear.test
       , Kleisli.test