Copyright	Guillaume Sabbagh 2021
License	GPL-3
Maintainer	guillaumesabbagh@protonmail.com
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Set.FinSet

Description

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

Synopsis

data FinSet a
- = Elem a
- | Collection [FinSet a]
emptyFinSet :: FinSet a
singleton :: a -> FinSet a
toList :: FinSet a -> [FinSet a]
fromList :: Eq a => [FinSet a] -> FinSet a
(|||) :: Eq a => FinSet a -> FinSet a -> FinSet a
union :: Eq a => [FinSet a] -> FinSet a
(&&&) :: Eq a => FinSet a -> FinSet a -> FinSet a
intersection :: Eq a => [FinSet a] -> FinSet a
isIn :: Eq a => FinSet a -> FinSet a -> Bool
includedIn :: Eq a => FinSet a -> FinSet a -> Bool
card :: FinSet a -> Int
generalizeType :: FinSet a -> FinSet (Either a b)
data FinMap a = FinMap {
- finMap :: AssociationList (FinSet a) (FinSet a)
- codomain :: FinSet a
}
data FinSetCat a = FinSetCat [FinSet a]
powerFinSet :: FinSet a -> FinSet a
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)
generalizeTypeSetCat :: FinSetCat a -> FinSetCat (Either a b)

Documentation

data FinSet a Source #

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.

Constructors

Elem a
Collection [FinSet a]

Instances

Instances details

Functor FinSet Source #
Instance details Defined in Set.FinSet Methods fmap :: (a -> b) -> FinSet a -> FinSet b # (<$) :: a -> FinSet b -> FinSet a #
Eq a => Eq (FinSet a) Source #
Instance details Defined in Set.FinSet Methods (==) :: FinSet a -> FinSet a -> Bool (/=) :: FinSet a -> FinSet a -> Bool
Show a => Show (FinSet a) Source #
Instance details Defined in Set.FinSet Methods showsPrec :: Int -> FinSet a -> ShowS show :: FinSet a -> String showList :: [FinSet a] -> ShowS
PrettyPrintable a => PrettyPrintable (FinSet a) Source #
Instance details Defined in Set.FinSet Methods pprint :: FinSet a -> String Source #
Eq a => Morphism (FinMap a) (FinSet a) Source #
Instance details Defined in Set.FinSet Methods (@) :: FinMap a -> FinMap a -> FinMap a Source # source :: FinMap a -> FinSet a Source # target :: FinMap a -> FinSet a Source #
Eq a => GeneratedFiniteCategory (FinSetCat a) (FinMap a) (FinSet a) Source #
Instance details Defined in Set.FinSet Methods genAr :: FinSetCat a -> FinSet a -> FinSet a -> [FinMap a] Source # decompose :: FinSetCat a -> FinMap a -> [FinMap a] Source # genArrows :: FinSetCat a -> [FinMap a] Source #
Eq a => FiniteCategory (FinSetCat a) (FinMap a) (FinSet a) Source #
Instance details Defined in Set.FinSet Methods ob :: FinSetCat a -> [FinSet a] Source # identity :: FinSetCat a -> FinSet a -> FinMap a Source # ar :: FinSetCat a -> FinSet a -> FinSet a -> [FinMap a] Source # arrows :: FinSetCat a -> [FinMap a] Source #

emptyFinSet :: FinSet a Source #

Constructs the empty set.

singleton :: a -> FinSet a Source #

Constructs a singleton set.

toList :: FinSet a -> [FinSet a] Source #

Extract a list from a set.

fromList :: Eq a => [FinSet a] -> FinSet a Source #

Transforms a list of sets into a set.

(|||) :: Eq a => FinSet a -> FinSet a -> FinSet a Source #

Union of two sets.

union :: Eq a => [FinSet a] -> FinSet a Source #

Union of a list of sets.

(&&&) :: Eq a => FinSet a -> FinSet a -> FinSet a Source #

Intersection of two sets.

intersection :: Eq a => [FinSet a] -> FinSet a Source #

Intersection of a list of sets.

isIn :: Eq a => FinSet a -> FinSet a -> Bool Source #

Returns wether a set is in another one.

includedIn :: Eq a => FinSet a -> FinSet a -> Bool Source #

Returns wether a set is included in another one.

card :: FinSet a -> Int Source #

Returns the size of a set.

generalizeType :: FinSet a -> FinSet (Either a b) Source #

Generalizes a set of a so that it can contain elements of type a or b.

data FinMap a Source #

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.

Constructors

FinMap
Fields finMap :: AssociationList (FinSet a) (FinSet a) codomain :: FinSet a

Instances

Instances details

Eq a => Eq (FinMap a) Source #
Instance details Defined in Set.FinSet Methods (==) :: FinMap a -> FinMap a -> Bool (/=) :: FinMap a -> FinMap a -> Bool
Show a => Show (FinMap a) Source #
Instance details Defined in Set.FinSet Methods showsPrec :: Int -> FinMap a -> ShowS show :: FinMap a -> String showList :: [FinMap a] -> ShowS
(PrettyPrintable a, Eq a) => PrettyPrintable (FinMap a) Source #
Instance details Defined in Set.FinSet Methods pprint :: FinMap a -> String Source #
Eq a => Morphism (FinMap a) (FinSet a) Source #
Instance details Defined in Set.FinSet Methods (@) :: FinMap a -> FinMap a -> FinMap a Source # source :: FinMap a -> FinSet a Source # target :: FinMap a -> FinSet a Source #
Eq a => GeneratedFiniteCategory (FinSetCat a) (FinMap a) (FinSet a) Source #
Instance details Defined in Set.FinSet Methods genAr :: FinSetCat a -> FinSet a -> FinSet a -> [FinMap a] Source # decompose :: FinSetCat a -> FinMap a -> [FinMap a] Source # genArrows :: FinSetCat a -> [FinMap a] Source #
Eq a => FiniteCategory (FinSetCat a) (FinMap a) (FinSet a) Source #
Instance details Defined in Set.FinSet Methods ob :: FinSetCat a -> [FinSet a] Source # identity :: FinSetCat a -> FinSet a -> FinMap a Source # ar :: FinSetCat a -> FinSet a -> FinSet a -> [FinMap a] Source # arrows :: FinSetCat a -> [FinMap a] Source #

data FinSetCat a Source #

FinSetCat is the type for the category of FinSet. Its elements are the sets considered in the Set category.

Constructors

FinSetCat [FinSet a]

Instances

Instances details

Eq a => Eq (FinSetCat a) Source #
Instance details Defined in Set.FinSet Methods (==) :: FinSetCat a -> FinSetCat a -> Bool (/=) :: FinSetCat a -> FinSetCat a -> Bool
Show a => Show (FinSetCat a) Source #
Instance details Defined in Set.FinSet Methods showsPrec :: Int -> FinSetCat a -> ShowS show :: FinSetCat a -> String showList :: [FinSetCat a] -> ShowS
PrettyPrintable a => PrettyPrintable (FinSetCat a) Source #
Instance details Defined in Set.FinSet Methods pprint :: FinSetCat a -> String Source #
Eq a => GeneratedFiniteCategory (FinSetCat a) (FinMap a) (FinSet a) Source #
Instance details Defined in Set.FinSet Methods genAr :: FinSetCat a -> FinSet a -> FinSet a -> [FinMap a] Source # decompose :: FinSetCat a -> FinMap a -> [FinMap a] Source # genArrows :: FinSetCat a -> [FinMap a] Source #
Eq a => FiniteCategory (FinSetCat a) (FinMap a) (FinSet a) Source #
Instance details Defined in Set.FinSet Methods ob :: FinSetCat a -> [FinSet a] Source # identity :: FinSetCat a -> FinSet a -> FinMap a Source # ar :: FinSetCat a -> FinSet a -> FinSet a -> [FinMap a] Source # arrows :: FinSetCat a -> [FinMap a] Source #

powerFinSet :: FinSet a -> FinSet a Source #

Returns the FinSet category such that every subset of the set given is an object of the category.

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) Source #

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.

generalizeTypeSetCat :: FinSetCat a -> FinSetCat (Either a b) Source #

Generalizes a set category of a so that it can contain elements of type a or b.