{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}

{-| Module  : FiniteCategories
Description : Typeclasses for 'Category' which are cartesian complete.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Typeclasses for 'Category' which are cartesian complete.

A 'TwoBase' specifies an internal domain and an internal codomain.

A 'Tripod' is the data necessary to specify an exponential object.

An exponential object is a terminal object in the category of candidate exponential objects.
-}

module Math.CartesianClosedCategory
(
    -- * 2-base
    TwoBase(..),
    -- * Tripod
    Tripod,
    -- ** Getters
    twoCone,
    evalMap,
    internalDomain,
    internalCodomain,
    powerObject,
    universeCategoryTripod,
    -- ** Smart constructors
    tripod,
    unsafeTripod,
    -- * Cartesian closed category
    CartesianClosedCategory(..),
    TwoProduct(..),
    Exponential(..),
    unexproject,
    Cartesian(..),
    -- * Exponential object
    -- ** Candidate exponential object
    isCandidateExponentialObject,
    CandidateExponentialObject(..),
    -- ** Candidate exponential object morphism
    CandidateExponentialObjectMorphism,
    -- *** Getters
    transpose,
    -- *** Smart constructors
    candidateExponentialObjectMorphism,
    unsafeCandidateExponentialObjectMorphism,
    -- ** Candidate exponential object category,
    CandidateExponentialObjectCategory(..),
    -- ** Exponential object function
    exponentialObjects,
)
where
    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               (intercalate)
    import              Data.Simplifiable
    
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.CompleteCategory
    import              Math.FiniteCategories.DiscreteTwo
    import              Math.FiniteCategories.ConeCategory
    import              Math.FiniteCategories.FunctorCategory
    import              Math.IO.PrettyPrint
    
    import              GHC.Generics
    
    -- | A 'TwoBase' is the specification of an internal domain and an internal codomain.
    --
    -- The object 'A' selects the internal domain, the object 'B' selects the internal codomain.
    --
    -- Don't confuse the 2-base of an exponential object with the base of its 2-cone. The 2-base selects the internal domain and internal codomain of the exponential object. The base of the 2-cone selects the power object and the internal domain.
    type TwoBase c m o = Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o
    
    -- | A 'Tripod' is a 2-cone on the power object and the internal domain, and an evaluation map from the apex of the 2-cone to the internal codomain.
    --
    -- 'Tripod' is private, use smart constructor 'tripod' which checks the structure of the 'Tripod' or use 'unsafeTripod' if you know that the 'evalMap' has the apex of the 'twoCone' as a source.
    data Tripod c m o = Tripod {
        twoCone :: (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o), -- ^ In the base of the cone, the power object should be the image of 'A' and the internal domain should be the image of 'B'.
        evalMap :: m -- ^ The evaluation map should go from the apex of the 2-cone to the internal codomain
        } deriving (Eq, Show, Generic, Simplifiable, PrettyPrint)
        
    -- | Smart constructor of 'Tripod', checks that the apex of the 'twoCone' is the source of the 'evalMap'.
    tripod :: (Morphism m o, Eq o) => Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o -> m -> Maybe (Tripod c m o)
    tripod cone em
        | source em /= apex cone = Nothing
        | otherwise = Just Tripod{twoCone = cone, evalMap = em}
        
    -- | Construct a 'Tripod' without checking the sructure of the 'Tripod', use with caution.
    unsafeTripod :: Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o -> m -> Tripod c m o
    unsafeTripod cone em = Tripod{twoCone = cone, evalMap = em}    
    
    -- | Return the internal domain of a 'Tripod'.
    internalDomain :: (Morphism m o) => Tripod c m o -> o
    internalDomain t = target $ (legsCone (twoCone t)) =>$ B
    
    -- | Return the internal codomain of a 'Tripod'.
    internalCodomain :: (Morphism m o) => Tripod c m o -> o
    internalCodomain t = target $ evalMap t
    
    -- | Return the power object of a 'Tripod'.
    powerObject :: (Morphism m o) => Tripod c m o -> o
    powerObject t = target $ (legsCone (twoCone t)) =>$ A
    
    -- | Return the category in which a 'Tripod' lives.
    universeCategoryTripod :: (Category c m o, Morphism m o, Eq c, Eq m, Eq o) => 
        Tripod c m o -> c
    universeCategoryTripod = universeCategoryCone.twoCone
    
    -- | For a 'Category' parametrized over a type t, the power object of an exponential object of a 2-base will contain 'ExponentialElement' constructions (an exponential element is a mapping). A given mapping has as domain and codomain values 'Exprojection's.
    --
    -- For example, in 'FinSet', let's consider the 2-base selecting {1,2} and {3,4} as internal domain and codomain. The power object of the 2-base is {{1->3,2->3},{1->3,2->4},{1->4,2->3},{1->4,2->4}}, note that it is not an object of ('Finset' Int) but an object of ('FinSet' (Set (Map Int))). The 'Exponential' type allows to construct type ('FinSet' ('Exponential' Int)) in which we can consider the original objects with 'Exprojection' and the new mappings with 'ExponentialElement'. Here, instead of mappings, we can construct the type ('FinSet' (Set (Exponential Int))), a mapping is then ('ExponentialElement' (weakMap [(1,3),(2,3)])). We can construct exprojections in the same category, for example along 'A' which will map ('ExponentialElement' (weakMap [(1,3),(2,3)])) to (set ['Exprojection' 1, 'Exprojection' 2]).
    data Exponential t = Exprojection t -- ^A 'ExponentialElement' can be applied to an 'Exprojection' yielding another 'Exprojection'.  
                       | ExponentialElement (Map t t) -- ^ An 'ExponentialElement' is an element in an exponential object, it is a mapping between objects of type t.
        deriving (Eq, Show, Generic, Simplifiable, PrettyPrint)
        
    -- | Remove the constructor 'Exprojection' from an original object t, throws an error if an 'ExponentialElement' is given.
    unexproject :: Exponential t -> t
    unexproject (Exprojection t) = t
    unexproject (ExponentialElement _) = error "Unexproject an exponential element."
        
    -- | For a category to be cartesian closed, we need to construct 2-products.
    type TwoProduct t = Limit DiscreteTwoOb t
    
    -- | For a category to be cartesian closed, we need to construct 2-products of exponential objects with exprojected objects.
    type Cartesian t = TwoProduct (Exponential t)
    
    
    class CartesianClosedCategory c m o cLim mLim oLim cLimExp mLimExp oLimExp | 
        c -> m, m -> o, cLim -> mLim, mLim -> oLim, cLimExp -> mLimExp, mLimExp -> oLimExp, c m o -> cLimExp where
        
        internalHom :: (CompleteCategory c m o cLim mLim oLim DiscreteTwo DiscreteTwoAr DiscreteTwoOb) => TwoBase c m o -> Tripod cLimExp mLimExp oLimExp

    -- | Return wether a 'Tripod' is a candidate exponential object or not. A 'Tripod' is a candidate exponential object if its 'twoCone' is a limit. Tests if the 2-cone is a 2-product by computing the limits in the universe category with the function 'limits' : it is slow.
    isCandidateExponentialObject :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Tripod c m o -> Bool
    isCandidateExponentialObject t = (twoCone t) `Set.elem` (limits.baseCone.twoCone $ t)
    
    -- | A 'CandidateExponentialObject' is a 'Tripod' such that its 'twoCone' is a limit.
    type CandidateExponentialObject c m o = Tripod c m o
    
    -- | A 'CandidateExponentialObjectMorphism' is a morphism between two 'CandidateExponentialObject's. It is private, use smart constructors 'candidateExponentialObjectMorphism' and 'unsafeCandidateExponentialObjectMorphism' to instantiate.
    data CandidateExponentialObjectMorphism c m o = CandidateExponentialObjectMorphism {
                                                        sourceCandidateExponentialObject :: CandidateExponentialObject c m o,
                                                        targetCandidateExponentialObject :: CandidateExponentialObject c m o,
                                                        transpose :: m
                                                    }
                                                    deriving (Eq, Show, Generic, Simplifiable, PrettyPrint)
    
    
    -- | Smart constructor for 'CandidateExponentialObjectMorphism'. Checks wether the transpose has valid domain and valid codomain.
    candidateExponentialObjectMorphism :: (Morphism m o, Eq m, Eq o) => CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> m -> Maybe (CandidateExponentialObjectMorphism c m o)
    candidateExponentialObjectMorphism s t transp
        | source transp == target ((legsCone $ twoCone s) =>$ A) && target transp == target ((legsCone $ twoCone t) =>$ A) = Just CandidateExponentialObjectMorphism {sourceCandidateExponentialObject = s, targetCandidateExponentialObject = t, transpose = transp}
        | otherwise = Nothing
        
    -- | Unsafe version of 'candidateExponentialObjectMorphism', use with caution as it does not check wether the transpose has valid domain and valid codomain.
    unsafeCandidateExponentialObjectMorphism :: CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> m -> CandidateExponentialObjectMorphism c m o
    unsafeCandidateExponentialObjectMorphism s t transp = CandidateExponentialObjectMorphism {sourceCandidateExponentialObject = s, targetCandidateExponentialObject = t, transpose = transp}
    
    instance (Morphism m o) => Morphism (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o) where
        source = sourceCandidateExponentialObject
        target = targetCandidateExponentialObject
        ceom2 @ ceom1 = CandidateExponentialObjectMorphism {sourceCandidateExponentialObject = sourceCandidateExponentialObject ceom1, targetCandidateExponentialObject = targetCandidateExponentialObject ceom2, transpose = (transpose ceom2) @ (transpose ceom1)}
    
    data CandidateExponentialObjectCategory c m o = CandidateExponentialObjectCategory (TwoBase c m o)
        deriving (Eq, Show, Generic, Simplifiable, PrettyPrint)
        
    instance (Category c m o, Morphism m o, Eq c, Eq m ,Eq o) => Category (CandidateExponentialObjectCategory c m o) (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o) where
        
        identity (CandidateExponentialObjectCategory base) tripod
            | differentInternalDomain = error "identity in a CandidateExponentialObjectCategory of a tripod with a different internal domain."
            | differentInternalCodomain = error "identity in a CandidateExponentialObjectCategory of a tripod with a different internal codomain."
            | differentUniverseCategory = error "identity in a CandidateExponentialObjectCategory of a tripod with a different universe category."
            | otherwise = CandidateExponentialObjectMorphism {sourceCandidateExponentialObject = tripod, targetCandidateExponentialObject = tripod, transpose = identity (universeCategoryTripod tripod) (powerObject tripod)}
            where
                differentInternalDomain = internalDomain tripod /= base ->$ A
                differentInternalCodomain = internalCodomain tripod /= base ->$ B
                differentUniverseCategory = universeCategoryTripod tripod /= tgt base
            
        
        ar (CandidateExponentialObjectCategory base) tripod1 tripod2
            | differentInternalDomain1 = error "ar in a CandidateExponentialObjectCategory where the source has different internal domain."
            | differentInternalCodomain1 = error "ar in a CandidateExponentialObjectCategory where the source has different internal codomain."
            | differentUniverseCategory1 = error "ar in a CandidateExponentialObjectCategory where the source has different universe Category."
            | differentInternalDomain2 = error "ar in a CandidateExponentialObjectCategory where the target has different internal domain."
            | differentInternalCodomain2 = error "ar in a CandidateExponentialObjectCategory where the target has different internal codomain."
            | differentUniverseCategory2 = error "ar in a CandidateExponentialObjectCategory where the target has different universe Category."
            | otherwise = (\m -> CandidateExponentialObjectMorphism{sourceCandidateExponentialObject = tripod1, targetCandidateExponentialObject = tripod2, transpose = m}) <$> ar (universeCategoryTripod tripod1) (powerObject tripod1) (powerObject tripod2)
            where
                differentInternalDomain1 = internalDomain tripod1 /= base ->$ A
                differentInternalCodomain1 = internalCodomain tripod1 /= base ->$ B
                differentUniverseCategory1 = universeCategoryTripod tripod1 /= tgt base
                differentInternalDomain2 = internalDomain tripod2 /= base ->$ A
                differentInternalCodomain2 = internalCodomain tripod2 /= base ->$ B
                differentUniverseCategory2 = universeCategoryTripod tripod2 /= tgt base
    
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m ,Eq o) => FiniteCategory (CandidateExponentialObjectCategory c m o) (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o) where
        
        ob (CandidateExponentialObjectCategory base) = [Tripod{twoCone = c, evalMap = m} | powerObj <- ob (tgt base), c <- limits (twoDiagram (tgt base) powerObj (base ->$ A)), m <- ar (tgt base) (apex c) (base ->$ B), isCandidateExponentialObject Tripod{twoCone = c, evalMap = m}]
        
    -- | Return the exponential objects of a given 2-base.
    exponentialObjects :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m ,Eq o) => TwoBase c m o -> Set (CandidateExponentialObject c m o)
    exponentialObjects base = terminalObjects (CandidateExponentialObjectCategory base)