{-# LANGUAGE MultiParamTypeClasses #-}
{-| Module : FiniteCategories
Description : The category of finite sets.
Copyright : Guillaume Sabbagh 2021
License : GPL-3
Maintainer : guillaumesabbagh@protonmail.com
Stability : experimental
Portability : portable
The __FinSet__ category has as objects finite sets and as morphisms maps between them.
It is a full subcategory of the __Set__ category.
It is itself a large category (therefore not a finite one),
we only construct finite subcategories of the mathematical infinite __FinSet__ category.
`FinSet` is the type of full finite subcategories of __FinSet__.
To instantiate it, use the `FinSet` constructor on a list of sets.
For example, see Example.ExampleSet
-}
module Set.FinSet where
import Data.List (intersect, nub, intercalate, subsequences)
import Utils.SetList
import Utils.AssociationList
import FiniteCategory.FiniteCategory
import Utils.CartesianProduct ((|^|))
import IO.PrettyPrint
import Diagram.Diagram
import ConeCategory.ConeCategory
import UsualCategories.One
-- | When constructing a set, the following rules should be respected :
--
-- - An elem is always a leaf construct.
--
-- - There should be no duplicate in a Collection.
--
-- - The root construct is always a Collection.
--
-- This set construction does not require the ord constraint.
data FinSet a = Elem a
| Collection [FinSet a]
deriving (Show)
instance (Eq a) => Eq (FinSet a) where
(Elem a) == (Elem b) = a == b
(Collection s1) == (Collection s2) = doubleInclusion s1 s2
_ == _ = False
instance Functor FinSet where
fmap f (Elem a) = Elem (f a)
fmap f (Collection xs) = Collection (fmap f <$> xs)
-- | Constructs the empty set.
emptyFinSet :: FinSet a
emptyFinSet = Collection []
-- | Constructs a singleton set.
singleton :: a -> FinSet a
singleton x = Collection [Elem x]
-- | Extract a list from a set.
toList :: FinSet a -> [FinSet a]
toList (Collection list) = list
-- | Transforms a list of sets into a set.
fromList :: (Eq a) => [FinSet a] -> FinSet a
fromList xs = Collection $ nub xs
-- | Union of two sets.
(|||) :: (Eq a) => FinSet a -> FinSet a -> FinSet a
(|||) (Collection l1) (Collection l2) = Collection $ nub (l1++l2)
-- | Union of a list of sets.
union :: (Eq a) => [FinSet a] -> FinSet a
union sets = foldr (|||) emptyFinSet sets
-- | Intersection of two sets.
(&&&) :: (Eq a) => FinSet a -> FinSet a -> FinSet a
(&&&) (Collection l1) (Collection l2) = Collection $ intersect l1 l2
-- | Intersection of a list of sets.
intersection :: (Eq a) => [FinSet a] -> FinSet a
intersection [] = error "Cannot make an intersection of no set."
intersection sets = foldr1 (&&&) sets
-- | Returns wether a set is in another one.
isIn :: (Eq a) => FinSet a -> FinSet a -> Bool
isIn e (Collection es) = elem e es
-- | Returns wether a set is included in another one.
includedIn :: (Eq a) => FinSet a -> FinSet a -> Bool
includedIn (Collection l1) (Collection l2) = isIncludedIn l1 l2
-- | Returns the size of a set.
card :: FinSet a -> Int
card (Collection xs) = length xs
-- | Generalizes a set of @a@ so that it can contain elements of type @a@ or @b@.
generalizeType :: FinSet a -> FinSet (Either a b)
generalizeType = fmap Left
instance (PrettyPrintable a) => PrettyPrintable (FinSet a) where
pprint (Elem a) = pprint a
pprint (Collection elems) = "{"++ (intercalate "," (pprint <$> elems)) ++ "}"
-- | `FinMap` is the morphism of the `FinSetCat` category.
--
-- We need to keep the codomain because it would not be present in a non-surjective map.
--
-- It is represented by an association list and a codomain.
data FinMap a = FinMap { finMap :: (AssociationList (FinSet a) (FinSet a))
, codomain :: (FinSet a)
}
deriving (Eq, Show)
instance (Eq a) => Morphism (FinMap a) (FinSet a) where
(@) g f = FinMap { finMap = [(k,((finMap g) !-! v)) | (k,v) <- (finMap f)]
, codomain = (codomain g)
}
source m = Collection $ nub (keys (finMap m))
target = codomain
instance (PrettyPrintable a, Eq a) => PrettyPrintable (FinMap a) where
pprint f = pprint (source f) ++ " -> " ++ pprint (target f) ++ "\n" ++ pprint (finMap f)
-- | `FinSetCat` is the type for the category of `FinSet`.
-- Its elements are the sets considered in the Set category.
data FinSetCat a = FinSetCat [FinSet a] deriving (Eq, Show)
instance (Eq a) => FiniteCategory (FinSetCat a) (FinMap a) (FinSet a) where
ob (FinSetCat xs) = xs
identity c s
| elem s (ob c) = FinMap{ finMap = [(e,e) | e <- toList s]
, codomain = s
}
| otherwise = error("Trying to get identity of an object not in the Set category.")
ar _ s t
| s == emptyFinSet = [FinMap{finMap=[],codomain=t}]
| t == emptyFinSet = []
| otherwise = (\x -> FinMap {codomain=t, finMap=x}) <$> [zip domain i | i <- images] where
domain = toList s
codomain = toList t
images = (codomain |^| (length domain))
instance (Eq a) => GeneratedFiniteCategory (FinSetCat a) (FinMap a) (FinSet a) where
genAr _ s t
| s == emptyFinSet = [FinMap{finMap=[],codomain=t}]
| t == emptyFinSet = []
| card s == 1 = [FinMap {codomain=t, finMap=injectiv}]
| card t == 1 = [FinMap {codomain=t, finMap=surjectiv}]
| s == t = nub $ (\m -> FinMap {codomain=t, finMap=m}) <$> [transpose,rotate,project]
| card s < card t = [FinMap {codomain=t, finMap=injectiv}]
| otherwise = [FinMap {codomain=t, finMap=surjectiv}]
where
domain = toList s
codomain = toList t
transpose = [(domain !! 0, domain !! 1),(domain !! 1, domain !! 0)]++[(o,o) | o <- drop 2 domain]
rotatedDomain = (tail domain) ++ [(head domain)]
rotate = zip domain rotatedDomain
project = (domain !! 0, domain !! 1):[(o,o) | o <- tail domain]
injectiv = zip domain codomain
surjectiv = zip domain ((replicate ((card s)-(card t)+1) (head codomain))++codomain)
decompose = bruteForceDecompose
instance (PrettyPrintable a) => PrettyPrintable (FinSetCat a) where
pprint (FinSetCat xs) = "FinSetCat "++(pprint xs)
-- | Returns the `FinSet` category such that every subset of the set given is an object of the category.
powerFinSet :: FinSet a -> FinSet a
powerFinSet (Collection xs) = Collection (Collection <$> subsequences xs)
-- | Add a set to the target FinSetCat such that the given diagram has a limit. The diagram must not be the empty diagram from @0@ to @0@.
--
-- Returns an insertion functor from the previous set category to the new one, an updated diagram which has a limit, and the new limit object.
constructLimit :: (FiniteCategory c m o, Morphism m o, Eq a, Eq c, Eq m, Eq o) => Diagram c m o (FinSetCat a) (FinMap a) (FinSet a) -> (Diagram (FinSetCat a) (FinMap a) (FinSet a) (FinSetCat a) (FinMap a) (FinSet a), Diagram c m o (FinSetCat a) (FinMap a) (FinSet a), (FinSet a))
constructLimit diag = (insertionFunctor, newDiagram, newLimitObject)
where
cat@(FinSetCat sets) = tgt diag
singletonAlreadyHere = or $ (\s -> card s == 1) <$> sets
singleton2 = if singletonAlreadyHere
then
head [s | s <- sets, card s == 1]
else
Collection [head sets] -- we make a singleton out of the first set
newSetCat = if singletonAlreadyHere
then
cat
else
FinSetCat (singleton2:sets)
newDiag = Diagram {src = src diag, tgt = newSetCat, omap = omap diag, mmap = mmap diag}
newLimitObject = Collection $ [(iterate (\x -> Collection [x]) singleton2) !! i | i <- [1..(length (conesOfApex newDiag singleton2))]]
newTargetCat = FinSetCat (newLimitObject:sets)
insertionFunctor = Diagram {src = cat, tgt = newTargetCat, omap = functToAssocList id (ob cat)
, mmap = functToAssocList id (arrows cat)}
newDiagram = insertionFunctor `composeDiag` diag
-- | Generalizes a set category of @a@ so that it can contain elements of type @a@ or @b@.
generalizeTypeSetCat :: FinSetCat a -> FinSetCat (Either a b)
generalizeTypeSetCat (FinSetCat xs) = FinSetCat $ (fmap Left) <$> xs