FinSet.hs

{-# LANGUAGE OverloadedLists #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Props.FinSet where

import Data.Fin (Fin, absurd, universe)
import Data.Proxy (Proxy (..))
import Data.Type.Equality (TestEquality (..), type (:~:) (..))
import Data.Type.Nat (Nat0, Nat1, Nat2, Nat3, Nat4, SNat (..), SNatI, reflect, snat)
import Data.Vec.Lazy (Vec (..), repeat)
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.Falsify (testProperty)
import Prelude qualified as P

import Proarrow.Category.Instance.FinSet (FINSET (..), FinSet (..))
import Proarrow.Category.Topos (closedTopology, doubleNegation, openTopology)
import Proarrow.Core (CategoryOf (..), Promonad (..), UN)

import Proarrow.Testing
  ( GenTotal (..)
  , Testable (..)
  , TestableProfunctor
  , TestableType (..)
  , TestingEqShow (..)
  , genSomeDef
  , invmap
  , oneElem
  , optGen
  , testEq
  , pattern GenNonEmpty
  )
import Proarrow.Testing.Laws

test :: TestTree
test =
  testGroup
    "FinSet"
    [ testCategory @FINSET
    , testTerminalObject @FINSET
    , testInitialObject @FINSET
    , testBinaryProducts_ @FINSET
    , testCartesian_ @FINSET
    , testMonoidal_ @FINSET
    , testSymMonoidal_ @FINSET
    , testCopyDiscard_ @FINSET
    , testBinaryCoproducts_ @FINSET
    , testDistributive_ @FINSET
    , testClosed_ @FINSET
    , testEqualizers_ @FINSET
    , testCoequalizers_ @FINSET
    , testEpiMonoFactorization_ @FINSET
    , testSubobjectClassifier_ @FINSET
    , -- FINSET is Boolean, so its only topologies are the two extremes, and ¬¬ is the identity
      testGroup
        "Lawvere-Tierney topologies"
        [ testLawvereTierney_ @FINSET doubleNegation
        , testLawvereTierneyFamily_ @FINSET "open" openTopology
        , testLawvereTierneyFamily_ @FINSET "closed" closedTopology
        , testProperty "double negation is the identity" P.$
            testEq "¬¬" "doubleNegation" (doubleNegation @FINSET) "id" id
        , testNegation @FINSET
        ]
    , testPullbacks_ @FINSET
    , testPushouts_ @FINSET
    , testComonoid_ @(FS Nat0)
    , testComonoid_ @(FS Nat1)
    , testComonoid_ @(FS Nat2)
    , testComonoid_ @(FS Nat3)
    , testMonoid_ @(FS Nat1)
    , -- The product category, whose tensor, products and coproducts all go through the
      -- projections, so that 'Cartesian' can see the tensor as the product at all. We use
      -- FINSET, not a thin category: there parallel arrows are equal, so these laws could only
      -- check that the arrows evaluate. Both factors are the same, so mixing up the components
      -- still type-checks and has to be caught here.
      testGroup
        "FINSET x FINSET"
        [ testCategory @(FINSET, FINSET)
        , testTerminalObject @(FINSET, FINSET)
        , testInitialObject @(FINSET, FINSET)
        , testBinaryProducts_ @(FINSET, FINSET)
        , testBinaryCoproducts_ @(FINSET, FINSET)
        , testMonoidal_ @(FINSET, FINSET)
        , testSymMonoidal_ @(FINSET, FINSET)
        , testCopyDiscard_ @(FINSET, FINSET)
        , testCartesian_ @(FINSET, FINSET)
        , testDistributive_ @(FINSET, FINSET)
        ]
    ]

-- | Two finite sets are the same object when they have the same cardinality. Not a method of
-- 'Testable': no law needs to compare objects (see "Props.Span"\'s 'eqP' for why the ones that do
-- are comparing something existential).
eqFinSet :: forall (a :: FINSET) (b :: FINSET). (Ob a, Ob b) => P.Maybe (a :~: b)
eqFinSet = (\Refl -> Refl) P.<$> testEquality (snat @(UN FS a)) (snat @(UN FS b))

instance Testable FINSET where
  type TestOb a = Ob a
  showOb @(FS a) = P.show (reflect (Proxy @a))
  genSome = genSomeDef @'[FS Nat0, FS Nat1, FS Nat2, FS Nat3, FS Nat4]

instance (Ob a, Ob b) => TestingEqShow (FinSet a b)
instance (Ob a, Ob b) => TestableType (FinSet a b) where
  gen = invmap FinSet unFinSet gen
instance TestableProfunctor FinSet

instance (P.Eq a, P.Show a) => TestingEqShow (Vec n a)
instance (P.Eq a, P.Show a, TestableType a, SNatI n) => TestableType (Vec n a) where
  gen = case gen of
    GenEmpty absrd -> case snat @n of
      SZ -> oneElem VNil
      SS -> GenEmpty \(a ::: _) -> absrd a
    GenNonEmpty g -> GenNonEmpty (P.sequence (repeat @n g))

instance (SNatI n) => TestingEqShow (Fin n)
instance (SNatI n) => TestableType (Fin n) where
  gen = case snat @n of
    SZ -> GenEmpty absurd
    SS -> optGen universe