WeakSets-1.3.3.0: src/Math/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 2022
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 pure set functions are suffixed with the letter 'P' for pure to avoid name collision.
-}
module Math.PureSet
(
-- * `PureSet` datatype
PureSet(..),
pureSet,
-- * Mathematical constructions using sets
emptySet,
singleton,
pair,
first,
second,
maybeFirst,
maybeSecond,
cartesianProduct,
numberToSet,
(||||),
(&&&&),
isInP,
isIncludedInP,
card,
powerSetP,
-- * Formatting functions
prettify,
formatPureSet,
)
where
import Data.WeakSet (Set)
import Data.WeakSet.Safe
import qualified Data.WeakSet as S
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, Show)
-- | Construct a `PureSet` from a list of pure sets.
pureSet :: [PureSet] -> PureSet
pureSet = (PureSet).set
-- | Peel a `PureSet` into a `Set`.
pureSetToSet :: PureSet -> Set PureSet
pureSetToSet (PureSet xs) = xs
-- | Construct the empty set.
emptySet :: PureSet
emptySet = pureSet []
-- | Construct the singleton containing a given set.
singleton :: PureSet -> PureSet
singleton x = pureSet $ [x]
-- | Construct 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]]
-- | Return the first element of a pair according to Kuratowski's definition of a tuple.
first :: PureSet -> PureSet
first (PureSet s)
| length l == 2 = anElement f
| length l == 1 = if card (anElement s) == 1 then (anElement.pureSetToSet.anElement $ s) else (error $ "Math.PureSet.first : malformed pair " ++ (show s))
| otherwise = error $ "Math.PureSet.first : malformed pair " ++ (show s)
where
l = setToList s
a = l !! 0
b = l !! 1
PureSet f = if card a == 1 then a else b
-- | Return the second element of a pair according to Kuratowski's definition of a tuple.
second :: PureSet -> PureSet
second i@(PureSet s)
| length l == 1 = if card (anElement s) == 1 then (anElement.pureSetToSet.anElement $ s) else (error $ "Math.PureSet.second : malformed pair " ++ (show s))
| length l == 2 = if r2 !! 0 == first i then r2 !! 1 else (if r2 !! 1 == first i then r2 !! 0 else (error $ "Math.PureSet.second : malformed pair " ++ (show s)))
| otherwise = error $ "Math.PureSet.second : malformed pair " ++ (show s)
where
l = setToList s
a = l !! 0
b = l !! 1
PureSet r = if card a == 2 then a else b
r2 = setToList r
-- | Return the first element of a pair if possible.
maybeFirst :: PureSet -> Maybe PureSet
maybeFirst (PureSet s)
| length l == 2 = Just $ anElement f
| length l == 1 = if card (anElement s) == 1 then Just (anElement.pureSetToSet.anElement $ s) else Nothing
| otherwise = Nothing
where
l = setToList s
a = l !! 0
b = l !! 1
PureSet f = if card a == 1 then a else b
-- | Return the second element of a pair if possible.
maybeSecond :: PureSet -> Maybe PureSet
maybeSecond i@(PureSet s)
| length l == 1 = if card (anElement s) == 1 then Just (anElement.pureSetToSet.anElement $ s) else Nothing
| length l == 2 = if r2 !! 0 == first i then Just (r2 !! 1) else (if r2 !! 1 == first i then Just (r2 !! 0) else Nothing)
| otherwise = Nothing
where
l = setToList s
a = l !! 0
b = l !! 1
PureSet r = if card a == 2 then a else b
r2 = setToList r
-- | Construct 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
-- | Transform 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)))
-- | Return wether a pure set is in another one.
isInP :: PureSet -> PureSet -> Bool
isInP x (PureSet xs) = x `isIn` xs
-- | Return wether a pure set is included in another one.
isIncludedInP :: PureSet -> PureSet -> Bool
isIncludedInP (PureSet xs) (PureSet ys) = xs `isIncludedIn` ys
-- | Return the size of a pure set.
card :: PureSet -> Int
card (PureSet xs) = cardinal xs
-- | Return the set of subsets of a given set.
powerSetP :: PureSet -> PureSet
powerSetP (PureSet xs) = PureSet $ PureSet <$> S.powerSet xs
-- | Prettify 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 x
| null (maybeSecond x) = Nothing
| otherwise = Just $ "(" ++ (formatPureSet.first $ x) ++ "," ++ (formatPureSet.second $ x) ++ ")"