WeakSets-0.1.0.0: src/PureSet.hs
{-| Module : WeakSets
Description : Pure sets are nested sets which only contain other sets all the way down. They allow to explore basic set theory.
Copyright : Guillaume Sabbagh 2021
License : GPL-3
Maintainer : guillaumesabbagh@protonmail.com
Stability : experimental
Portability : portable
Pure sets are nested sets which only contain other sets all the way down. They allow to explore basic set theory.
Every mathematical object is a set, usual constructions such as Von Neumann numbers and Kuratowski pairs are implemented.
It is a tree where the order of the branches does not matter.
Functions with the same name as homogeneous set functions are suffixed with the letter 'P' for pure to avoid name collision.
-}
module PureSet
(
-- * `PureSet` datatype
PureSet(..),
pureSet,
-- * Mathematical constructions using sets
emptySet,
singleton,
pair,
cartesianProduct,
numberToSet,
(||||),
(&&&&),
isInP,
isIncludedInP,
card,
powerSetP,
-- * Formatting functions
prettify,
formatPureSet,
)
where
import HomogeneousSet
import Data.List (intersect, nub, intercalate, subsequences)
import Data.Maybe (fromJust, catMaybes)
-- | A `PureSet` is a `Set` of other pure sets.
data PureSet = PureSet (Set PureSet) deriving (Eq)
instance Show PureSet where
show (PureSet xs) = "(pureSet "++ show (setToList xs) ++")"
-- | Constructs a `PureSet` from a list of pure sets.
pureSet :: [PureSet] -> PureSet
pureSet = (PureSet).set
-- | Peels a `PureSet` into a `Set`.
pureSetToSet :: PureSet -> Set PureSet
pureSetToSet (PureSet xs) = xs
-- | Constructs the empty set.
emptySet :: PureSet
emptySet = pureSet []
-- | Constructs the singleton containing a given set.
singleton :: PureSet -> PureSet
singleton x = pureSet $ [x]
-- | Constructs an ordered pair from two sets according to Kuratowski's definition of a tuple.
pair :: PureSet -> PureSet -> PureSet
pair x y = PureSet $ set [singleton x, pureSet $ [x,y]]
-- | Constructs the cartesian product of two sets.
cartesianProduct :: PureSet -> PureSet -> PureSet
cartesianProduct (PureSet xs) (PureSet ys) = pureSet $ [pair x y | x <- setToList xs, y <- setToList ys]
-- | Union of two pure sets.
(||||) :: PureSet -> PureSet -> PureSet
(||||) (PureSet xs) (PureSet ys) = PureSet $ xs ||| ys
-- | Intersection of two pure sets.
(&&&&) :: PureSet -> PureSet -> PureSet
(&&&&) (PureSet xs) (PureSet ys) = PureSet $ xs |&| ys
-- | Difference of two pure sets.
(\\\\) :: PureSet -> PureSet -> PureSet
(\\\\) (PureSet xs) (PureSet ys) = PureSet $ xs |-| ys
-- | Transforms a number into its Von Neumann construction
numberToSet :: (Num a, Eq a) => a -> PureSet
numberToSet 0 = emptySet
numberToSet n = (numberToSet (n-1)) |||| (singleton (numberToSet (n-1)))
-- | Returns wether a pure set is in another one.
isInP :: PureSet -> PureSet -> Bool
isInP x (PureSet xs) = x `isIn` xs
-- | Returns wether a pure set is included in another one.
isIncludedInP :: PureSet -> PureSet -> Bool
isIncludedInP (PureSet xs) (PureSet ys) = xs `isIncludedIn` ys
-- | Returns the size of a pure set.
card :: PureSet -> Int
card (PureSet xs) = cardinal xs
-- | Returns the set of subsets of a given set.
powerSetP :: PureSet -> PureSet
powerSetP (PureSet xs) = PureSet $ PureSet |<$>| powerSet xs
-- | Prettiffies a pure set according to usual mathematical notation.
prettify :: PureSet -> String
prettify (PureSet xs)
| cardinal xs == 0 = "{}"
| otherwise = "{" ++ (intercalate ", " $ prettify <$> setToList xs) ++ "}"
-- | Format pure sets such that if numbers are recognized, they are transformed into integer and if pairs are recognized, they are transformed into pairs.
formatPureSet :: PureSet -> String
formatPureSet x
| (not.null) $ toNumber x = show.fromJust $ toNumber x
| (not.null) $ toPair x = fromJust.toPair $ x
| otherwise = "{"++intercalate "," (formatPureSet <$> (setToList.pureSetToSet $ x))++"}"
where
toNumber s@(PureSet xs)
| s == emptySet = Just 0
| otherwise = let
numbers = setToList $ toNumber |<$>| xs
anyMissing = null $ foldr1 (>>) numbers
maxNb = maximum $ catMaybes numbers
in
if (not anyMissing) && (set (Just <$> [0..maxNb])) == (set numbers) then Just (maxNb + 1) else Nothing
toPair (PureSet xs)
| cardinal xs == 2 =
case () of
() | ((card $ (setToList xs) !! 0) == 1 && (card $ (setToList xs) !! 1) == 2) && ((setToList xs) !! 0) `isInP` ((setToList xs) !! 1) -> Just $ "(" ++ (formatPureSet.head.setToList.pureSetToSet $ ((setToList xs) !! 0)) ++ "," ++ (formatPureSet.head.setToList.pureSetToSet $ (((setToList xs) !! 1) \\\\ ((setToList xs) !! 0))) ++ ")"
| ((card $ (setToList xs) !! 1) == 1 && (card $ (setToList xs) !! 0) == 2) && ((setToList xs) !! 1) `isInP` ((setToList xs) !! 0) -> Just $ "(" ++ (formatPureSet.head.setToList.pureSetToSet $ ((setToList xs) !! 1)) ++ "," ++ (formatPureSet.head.setToList.pureSetToSet $ (((setToList xs) !! 0) \\\\ ((setToList xs) !! 1))) ++ ")"
| otherwise -> Nothing
| otherwise = Nothing