{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

{-| Module  : FiniteCategories
Description : The __'FinSet'__ category has finite sets as objects and functions as morphisms.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __'FinSet'__ category has finite sets as objects and functions as morphisms.

Finite sets are represented by weak sets from Data.WeakSet and functions by enriched weak maps from Data.WeakMap.

These structures are homogeneous, meaning you can only have sets containing one type of objects in a given 'FinSet' category.

See the category __'PureSet'__ for the category of sets which can be arbitrarily nested.
-}

module Math.Categories.FinSet
(
    -- * Function

    Function(..),
    (||!||),
    -- * __FinSet__

    FinSet(..),
)
where
    import              Math.Category
    import              Math.Categories.ConeCategory
    import              Math.Categories.FunctorCategory
    import              Math.FiniteCategories.DiscreteCategory
    import              Math.IO.PrettyPrint
    
    import              Data.WeakSet        (Set)
    import qualified    Data.WeakSet    as  Set
    import              Data.WeakSet.Safe
    import              Data.WeakMap        (Map)
    import qualified    Data.WeakMap    as  Map
    import              Data.WeakMap.Safe
    import              Data.List           (nub)
    import              Data.Maybe          (fromJust)

    
    -- | A 'Function' (finite function) is a weak map enriched with a codomain.

    --

    -- We have to store the codomain to retrieve the target set of a morphism in __'FinSet'__.

    data Function a = Function 
                            {
                                forall a. Function a -> Map a a
function :: Map a a,
                                forall a. Function a -> Set a
codomain :: Set a
                            }
                        deriving
                            (Function a -> Function a -> Bool
(Function a -> Function a -> Bool)
-> (Function a -> Function a -> Bool) -> Eq (Function a)
forall a. Eq a => Function a -> Function a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Function a -> Function a -> Bool
== :: Function a -> Function a -> Bool
$c/= :: forall a. Eq a => Function a -> Function a -> Bool
/= :: Function a -> Function a -> Bool
Eq, Int -> Function a -> ShowS
[Function a] -> ShowS
Function a -> String
(Int -> Function a -> ShowS)
-> (Function a -> String)
-> ([Function a] -> ShowS)
-> Show (Function a)
forall a. Show a => Int -> Function a -> ShowS
forall a. Show a => [Function a] -> ShowS
forall a. Show a => Function a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Function a -> ShowS
showsPrec :: Int -> Function a -> ShowS
$cshow :: forall a. Show a => Function a -> String
show :: Function a -> String
$cshowList :: forall a. Show a => [Function a] -> ShowS
showList :: [Function a] -> ShowS
Show)
    
    instance (Eq a) => Morphism (Function a) (Set a) where
        source :: Function a -> Set a
source = Map a a -> Set a
forall k a. Map k a -> Set k
domain(Map a a -> Set a)
-> (Function a -> Map a a) -> Function a -> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Function a -> Map a a
forall a. Function a -> Map a a
function
        target :: Function a -> Set a
target = Function a -> Set a
forall a. Function a -> Set a
codomain
        @? :: Function a -> Function a -> Maybe (Function a)
(@?) Function a
f2 Function a
f1
            | Function a -> Set a
forall m o. Morphism m o => m -> o
target Function a
f1 Set a -> Set a -> Bool
forall a. Eq a => a -> a -> Bool
== Function a -> Set a
forall m o. Morphism m o => m -> o
source Function a
f2 = Function a -> Maybe (Function a)
forall a. a -> Maybe a
Just Function{function :: Map a a
function = (Function a -> Map a a
forall a. Function a -> Map a a
function Function a
f2) Map a a -> Map a a -> Map a a
forall b c a. Eq b => Map b c -> Map a b -> Map a c
|.| (Function a -> Map a a
forall a. Function a -> Map a a
function Function a
f1), codomain :: Set a
codomain = Function a -> Set a
forall a. Function a -> Set a
codomain Function a
f2}
            | Bool
otherwise = Maybe (Function a)
forall a. Maybe a
Nothing
            
    -- | A function to apply a 'Function' to an object in the domain of the 'Function'.

    (||!||) :: (Eq a) => Function a -> a -> a
    ||!|| :: forall a. Eq a => Function a -> a -> a
(||!||) Function a
f a
x = (Function a -> Map a a
forall a. Function a -> Map a a
function Function a
f) Map a a -> a -> a
forall k v. Eq k => Map k v -> k -> v
|!| a
x
    
    -- | __'FinSet'__ is the category of finite sets.

    data FinSet a = FinSet deriving (FinSet a -> FinSet a -> Bool
(FinSet a -> FinSet a -> Bool)
-> (FinSet a -> FinSet a -> Bool) -> Eq (FinSet a)
forall a. FinSet a -> FinSet a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. FinSet a -> FinSet a -> Bool
== :: FinSet a -> FinSet a -> Bool
$c/= :: forall a. FinSet a -> FinSet a -> Bool
/= :: FinSet a -> FinSet a -> Bool
Eq, Int -> FinSet a -> ShowS
[FinSet a] -> ShowS
FinSet a -> String
(Int -> FinSet a -> ShowS)
-> (FinSet a -> String) -> ([FinSet a] -> ShowS) -> Show (FinSet a)
forall a. Int -> FinSet a -> ShowS
forall a. [FinSet a] -> ShowS
forall a. FinSet a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Int -> FinSet a -> ShowS
showsPrec :: Int -> FinSet a -> ShowS
$cshow :: forall a. FinSet a -> String
show :: FinSet a -> String
$cshowList :: forall a. [FinSet a] -> ShowS
showList :: [FinSet a] -> ShowS
Show)
    
    instance (Eq a) => Category (FinSet a) (Function a) (Set a) where
        identity :: Morphism (Function a) (Set a) => FinSet a -> Set a -> Function a
identity FinSet a
_ Set a
s = Function {function :: Map a a
function = Set a -> Map a a
forall a. Set a -> Map a a
idFromSet Set a
s, codomain :: Set a
codomain = Set a
s}
        
        ar :: Morphism (Function a) (Set a) =>
FinSet a -> Set a -> Set a -> Set (Function a)
ar FinSet a
_ Set a
s Set a
t
            | Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
s = [Function a] -> Set (Function a)
forall a. [a] -> Set a
set [Function{function :: Map a a
function = AssociationList a a -> Map a a
forall k v. AssociationList k v -> Map k v
weakMap [], codomain :: Set a
codomain = Set a
t}]
            | Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
t = [Function a] -> Set (Function a)
forall a. [a] -> Set a
set []
            | Bool
otherwise = (\Map a a
x -> Function{function :: Map a a
function = Map a a
x, codomain :: Set a
codomain = Set a
t}) (Map a a -> Function a) -> Set (Map a a) -> Set (Function a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (Map a a)
functions where
                domain :: [a]
domain = Set a -> [a]
forall a. Eq a => Set a -> [a]
setToList Set a
s
                images :: Set [a]
images = (Set a
t Set a -> Int -> Set [a]
forall a. Eq a => Set a -> Int -> Set [a]
|^| ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
domain))
                functions :: Set (Map a a)
functions = AssociationList a a -> Map a a
forall k v. AssociationList k v -> Map k v
weakMap (AssociationList a a -> Map a a)
-> ([a] -> AssociationList a a) -> [a] -> Map a a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> [a] -> AssociationList a a
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
domain ([a] -> Map a a) -> Set [a] -> Set (Map a a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set [a]
images
                
    -- instance (Eq a) => HasFiniteProducts (FinSet a) (Set a) (Function [a]) (Set [a]) where

        -- product _ diag2 = result

            -- where

                -- prod = cartesianProductOfSets (elems (omap diag2))

                -- diag1 = constantDiagram (source diag2) FinSet prod

                -- mapping i = memorizeFunction (\_ -> (!! i) <$> prod) prod

                -- Just result = naturalTransformationToCone $ unsafeNaturalTransformation diag1 diag2 (weakMap [(i,Function {function=mapping i, codomain = image (mapping i)}) | i <- [0..((Map.size (omap diag2))-1)]])

       
    instance (PrettyPrint a, Eq a) => PrettyPrint (Function a) where
        pprint :: Function a -> String
pprint = Map a a -> String
forall a. PrettyPrint a => a -> String
pprint(Map a a -> String)
-> (Function a -> Map a a) -> Function a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Function a -> Map a a
forall a. Function a -> Map a a
function
        
    instance (PrettyPrint a, Eq a) => PrettyPrint (FinSet a) where
        pprint :: FinSet a -> String
pprint = FinSet a -> String
forall a. Show a => a -> String
show