Opposite.hs

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}

{-| Module  : FiniteCategories
Description : Each 'Category' has an opposite one where morphisms are reversed.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Each 'Category' has an opposite one where morphisms are reversed.
-}

module Math.Categories.Opposite
(
    OpMorphism(..),
    opOpMorphism,
    Op(..),
    opOp,
)
where
    import          Math.Category
    import          Math.FiniteCategory
    import          Math.IO.PrettyPrint
    
    import          Data.WeakSet.Safe
    import          Data.Simplifiable
    
    import          GHC.Generics
    
    -- | An 'OpMorphism' is a morphism where source and target are reversed.
    data OpMorphism m = OpMorphism m deriving (Eq, Show, Generic, Simplifiable)
    
    -- | Return the original morphism given an 'OpMorphism'.
    opOpMorphism :: OpMorphism m -> m
    opOpMorphism (OpMorphism m) = m
    
    instance (Morphism m o) => Morphism (OpMorphism m) o where
        source (OpMorphism m) = target m
        target (OpMorphism m) = source m
        (@) (OpMorphism m2) (OpMorphism m1) = OpMorphism $ m1 @ m2
    
    -- | The 'Op' operator gives the opposite of a 'Category'.
    data Op c = Op c deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
    
    -- | Return the original category given an 'Op' category.
    opOp :: Op c -> c
    opOp (Op c) = c
    
    instance (Category c m o, Morphism m o) => Category (Op c) (OpMorphism m) o where
        identity (Op c) o = OpMorphism $ identity c o
        ar (Op c) x y = OpMorphism <$> ar c y x
        genAr (Op c) x y = OpMorphism <$> genAr c y x
        decompose (Op c) (OpMorphism m) = OpMorphism <$> reverse (decompose c m)
    
    instance (FiniteCategory c m o, Morphism m o) => FiniteCategory (Op c) (OpMorphism m) o where
        ob (Op c) = ob c
    
    instance (PrettyPrint m) => PrettyPrint (OpMorphism m) where
        pprint 0 _ = "..."
        pprint v (OpMorphism m) = "Op("++ pprint (v-1) m ++ ")"
        
        -- pprintWithIndentations 0 ov indent _ = indentation ov indent ++ "...\n"
        -- pprintWithIndentations cv ov indent (OpMorphism x) = indentation (ov - cv) indent ++ "Op\n" ++ pprintWithIndentations (cv - 1) ov indent x