{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}

-- |
-- Module      : OAlg.Category.Definition
-- Description : definition of categories
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- categories of morphisms. We adapted the concept of categories form 'Control.Category.Category' to
-- better cover our needs.
module OAlg.Category.Definition
  ( 
    -- * Category
    Category(..), cOne'

    -- | __Some basic definitions in the category @('->')@__
  , id
  , const
  , curry, uncurry, fst, snd
  , curry3, uncurry3

    -- * Cayleyan
  , Cayleyan2(..)
  
    -- * Morphism
  , Morphism(..)
  , Homomorphous(..), tauHom, tau1Hom
  , eqlDomain, eqlRange
  , eqlMorphism
  -- , toOp2Struct

    -- * Applicative
  , Applicative(..), ($)
  , Applicative1(..)
  
    -- * Functorial
  , Functorial

    -- * Forget
  , Forget(..)
    
    -- * Embeddable
  , EmbeddableMorphism
  , EmbeddableMorphismTyp
  )
  where

import Data.Type.Equality
import Data.Typeable
import Data.Kind
import Data.Maybe
import Data.List ((++))

import OAlg.Data.Show
import OAlg.Data.Equal

import OAlg.Data.Opposite
import OAlg.Data.Either

import OAlg.Category.Applicative

import OAlg.Structure.Definition

--------------------------------------------------------------------------------
-- Defs -

-- | the identity map.
id :: x -> x
id :: forall x. x -> x
id = \x
x -> x
x

-- | the constant map given by a value in @__b__@.
--
-- __Property__ Let @y@ be in @__b__@ then for all @x@ in @__a__@ holds: @'const' y x@ is identical
-- to @y@.
const :: b -> a -> b
const :: forall b a. b -> a -> b
const b
b a
_ = b
b

-- | the first component of the pair.
fst :: (a,b) -> a
fst :: forall a b. (a, b) -> a
fst (a
a,b
_) = a
a

-- | the second component of the pair. 
snd :: (a,b) -> b
snd :: forall a b. (a, b) -> b
snd (a
_,b
b) = b
b

-- | currying a map.
curry :: ((a,b) -> c) -> a -> b -> c
curry :: forall a b c. ((a, b) -> c) -> a -> b -> c
curry (a, b) -> c
f a
a b
b = (a, b) -> c
f (a
a,b
b)

-- | uncurrying a map.
uncurry :: (a -> b -> c) -> (a,b) -> c
uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> b -> c
f (a
a,b
b) = a -> b -> c
f a
a b
b

-- | currying a map.
curry3 :: ((a,b,c) -> d) -> a -> b -> c -> d
curry3 :: forall a b c d. ((a, b, c) -> d) -> a -> b -> c -> d
curry3 (a, b, c) -> d
f a
a b
b c
c = (a, b, c) -> d
f (a
a,b
b,c
c)

-- | uncurrying a map.
uncurry3 :: (a -> b -> c -> d) -> (a,b,c) -> d
uncurry3 :: forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 a -> b -> c -> d
f (a
a,b
b,c
c) = a -> b -> c -> d
f a
a b
b c
c

--------------------------------------------------------------------------------
-- eqlDomain -

-- | gets for two 'Typeable' types @__x__@ and @__x'__@ and for two parameterized types maybe an
-- attest that the domain types are equal.
eqlDomain :: Struct Typ x -> Struct Typ x'
  -> m x y -> m x' y -> Maybe (x :~: x')
eqlDomain :: forall x x' (m :: * -> * -> *) y.
Struct Typ x
-> Struct Typ x' -> m x y -> m x' y -> Maybe (x :~: x')
eqlDomain Struct Typ x
Struct Struct Typ x'
Struct m x y
_ m x' y
_ = forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

--------------------------------------------------------------------------------
-- eqlRange -

-- | gets for two 'Typeable' types @__y__@ and @__y'__@ and for two parameterized types maybe an
-- attest that the range types are equal.
eqlRange :: Struct Typ y -> Struct Typ y'
  -> m x y -> m x y' -> Maybe (y :~: y')
eqlRange :: forall y y' (m :: * -> * -> *) x.
Struct Typ y
-> Struct Typ y' -> m x y -> m x y' -> Maybe (y :~: y')
eqlRange Struct Typ y
Struct Struct Typ y'
Struct m x y
_ m x y'
_ = forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

--------------------------------------------------------------------------------
-- eqlMorphism -

-- | gets maybe an attest that the two given morphisms types are equal. 
eqlMorphism :: Typeable m
  => Struct Typ x -> Struct Typ x'
  -> Struct Typ y -> Struct Typ y'
  -> m x y -> m x' y' -> Maybe (m x y :~: m x' y')
eqlMorphism :: forall (m :: * -> * -> *) x x' y y'.
Typeable m =>
Struct Typ x
-> Struct Typ x'
-> Struct Typ y
-> Struct Typ y'
-> m x y
-> m x' y'
-> Maybe (m x y :~: m x' y')
eqlMorphism Struct Typ x
Struct Struct Typ x'
Struct Struct Typ y
Struct Struct Typ y'
Struct m x y
_ m x' y'
_ = forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

--------------------------------------------------------------------------------
-- Homomorphous -

infix 5 :>:

-- | attest that both @__x__@ and @__y__@ have homomorphous structures, i.e.
--   both admit the same constraints given by the parameter @s@.
data Homomorphous s x y = Struct s x :>: Struct s y deriving (Int -> Homomorphous s x y -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s x y. Int -> Homomorphous s x y -> ShowS
forall s x y. [Homomorphous s x y] -> ShowS
forall s x y. Homomorphous s x y -> String
showList :: [Homomorphous s x y] -> ShowS
$cshowList :: forall s x y. [Homomorphous s x y] -> ShowS
show :: Homomorphous s x y -> String
$cshow :: forall s x y. Homomorphous s x y -> String
showsPrec :: Int -> Homomorphous s x y -> ShowS
$cshowsPrec :: forall s x y. Int -> Homomorphous s x y -> ShowS
Show,Homomorphous s x y -> Homomorphous s x y -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s x y. Homomorphous s x y -> Homomorphous s x y -> Bool
/= :: Homomorphous s x y -> Homomorphous s x y -> Bool
$c/= :: forall s x y. Homomorphous s x y -> Homomorphous s x y -> Bool
== :: Homomorphous s x y -> Homomorphous s x y -> Bool
$c== :: forall s x y. Homomorphous s x y -> Homomorphous s x y -> Bool
Eq)

instance Show2 (Homomorphous m)
instance Eq2 (Homomorphous m)

--------------------------------------------------------------------------------
-- tauHom -

-- | transforming homomorphous structural attests. 
tauHom :: Transformable s t => Homomorphous s x y -> Homomorphous t x y
tauHom :: forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (Struct s x
d :>: Struct s y
r) = forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s x
d forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s y
r

--------------------------------------------------------------------------------
-- tau1Hom -

-- | transforming homomorphous structural attests. 
tau1Hom :: Transformable1 f s => Homomorphous s x y -> Homomorphous s (f x) (f y)
tau1Hom :: forall (f :: * -> *) s x y.
Transformable1 f s =>
Homomorphous s x y -> Homomorphous s (f x) (f y)
tau1Hom (Struct s x
sx:>:Struct s y
sy) = forall (f :: * -> *) s x.
Transformable1 f s =>
Struct s x -> Struct s (f x)
tau1 Struct s x
sx forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall (f :: * -> *) s x.
Transformable1 f s =>
Struct s x -> Struct s (f x)
tau1 Struct s y
sy

--------------------------------------------------------------------------------
-- Morphism -

-- | morphism.
class Morphism m where
  {-# MINIMAL homomorphous | (domain,range) #-}

  -- | the object class.
  type ObjectClass m

  -- | attests, that the types @__x__@ and @__y__@ fulfill the constraints given
  -- by @'Homomorphous' ('ObjectClass' __m__) __x__ __y__@, i.e both fulfill the constraints
  -- given by @'Structure' ('ObjectClass' __m__) __x__@ and @'Structure' ('ObjectClass' __m__) __y__@
  -- respectively.
  homomorphous :: m x y -> Homomorphous (ObjectClass m) x y
  homomorphous m x y
m = forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain m x y
m forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range m x y
m

  -- | attests that the domain type @__x__@ fulfills the constraints given
  -- by @'Structure' ('ObjectClass' __m__) __x__@.
  domain :: m x y -> Struct (ObjectClass m) x
  domain m x y
m = Struct (ObjectClass m) x
d where Struct (ObjectClass m) x
d :>: Struct (ObjectClass m) y
_ = forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous m x y
m

  -- | attests that the range type @__y__@ fulfills the constraints given
  -- by @'Structure' ('ObjectClass' __m__) __y__@.
  range  :: m x y -> Struct (ObjectClass m) y
  range m x y
m = Struct (ObjectClass m) y
r where Struct (ObjectClass m) x
_ :>: Struct (ObjectClass m) y
r = forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous m x y
m

--------------------------------------------------------------------------------
-- toOp2Struct -

-- | transforming a 'Struct' where __@p@__ serves only as a proxy for __@m@__ and will not
--   be evaluated.
toOp2Struct :: p m -> Struct (ObjectClass m) x -> Struct (ObjectClass (Op2 m)) x
toOp2Struct :: forall (p :: (* -> * -> *) -> *) (m :: * -> * -> *) x.
p m -> Struct (ObjectClass m) x -> Struct (ObjectClass (Op2 m)) x
toOp2Struct p m
_ = forall x. x -> x
id

--------------------------------------------------------------------------------
-- Morphism - Instance -

instance Morphism (Homomorphous s) where
  type ObjectClass (Homomorphous s) = s
  homomorphous :: forall x y.
Homomorphous s x y
-> Homomorphous (ObjectClass (Homomorphous s)) x y
homomorphous = forall x. x -> x
id

instance Morphism (->) where
  type ObjectClass (->) = Type
  homomorphous :: forall x y. (x -> y) -> Homomorphous (ObjectClass (->)) x y
homomorphous x -> y
_ = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct

instance Morphism h => Morphism (Op2 h) where
  type ObjectClass (Op2 h) = ObjectClass h
  domain :: forall x y. Op2 h x y -> Struct (ObjectClass (Op2 h)) x
domain (Op2 h y x
h) = forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h y x
h
  range :: forall x y. Op2 h x y -> Struct (ObjectClass (Op2 h)) y
range (Op2 h y x
h) = forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h y x
h
  
--------------------------------------------------------------------------------
-- Category -
infixr 9 .
-- | category of morphisms.
--
--   __Properties__ Let __@c@__ be a type instance of the class 'Category', then
--   holds:
--
--  (1) #Cat1#For all types __@x@__, __@y@__ and @f@ in __@c@__ __@x@__ __@y@__ holds:
--      @'cOne' ('range' f) '.' f = f@ and @f '.' 'cOne' ('domain' f) = f@.
--
--  (1) #Cat2#For all types __@w@__, __@x@__, __@y@__, __@z@__
--      and @f@ in __@c@__ __@x@__ __@w@__, @g@ in __@c@__ __@y@__ __@x@__,
--      @h@ in __@c@__ __@z@__ __@y@__ holds: @f '.' (g '.' h) = (f '.' g) '.' h@. 
class Morphism c => Category c where
  -- | the identity morphism for an eligible __@x@__.
  cOne :: Struct (ObjectClass c) x -> c x x
  (.) :: c y z -> c x y -> c x z

--------------------------------------------------------------------------------
-- cOne' -

-- | the 'cOne' to a given @'Struct' ('ObjectClass' __c__)@. The type @__p c__@ serves only as
--   proxy and 'cOne'' is lazy in it.
--
--   __Note__ As 'ObjectClass' may be a non-injective type family,
--   the type checker needs some times a little bit more information
--   to pic the right 'cOne'.
cOne' :: Category c => p c -> Struct (ObjectClass c) x -> c x x
cOne' :: forall (c :: * -> * -> *) (p :: (* -> * -> *) -> *) x.
Category c =>
p c -> Struct (ObjectClass c) x -> c x x
cOne' p c
_ = forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne

--------------------------------------------------------------------------------
-- Category - Instance -

instance Category (Homomorphous s) where
  cOne :: forall x.
Struct (ObjectClass (Homomorphous s)) x -> Homomorphous s x x
cOne Struct (ObjectClass (Homomorphous s)) x
s = Struct (ObjectClass (Homomorphous s)) x
s forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct (ObjectClass (Homomorphous s)) x
s
  (Struct s y
Struct :>: Struct s z
c) . :: forall y z x.
Homomorphous s y z -> Homomorphous s x y -> Homomorphous s x z
. (Struct s x
a :>: Struct s y
Struct) = Struct s x
aforall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>:Struct s z
c

instance Category (->) where
  cOne :: forall x. Struct (ObjectClass (->)) x -> x -> x
cOne Struct (ObjectClass (->)) x
Struct = \x
x -> x
x
  y -> z
f . :: forall y z x. (y -> z) -> (x -> y) -> x -> z
. x -> y
g = \x
x -> y -> z
f (x -> y
g x
x)

instance Category c => Category (Op2 c) where
  cOne :: forall x. Struct (ObjectClass (Op2 c)) x -> Op2 c x x
cOne Struct (ObjectClass (Op2 c)) x
s = forall (h :: * -> * -> *) x y. h y x -> Op2 h x y
Op2 (forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne Struct (ObjectClass (Op2 c)) x
s)
  Op2 c z y
f . :: forall y z x. Op2 c y z -> Op2 c x y -> Op2 c x z
. Op2 c y x
g = forall (h :: * -> * -> *) x y. h y x -> Op2 h x y
Op2 (c y x
g forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c z y
f)
  
--------------------------------------------------------------------------------
-- Functorial -

-- | representable categories, i.e. covariant functors from an 'Applicative' category
--   __c__ to @('->')@.
--
--   __Properties__ Let __@c@__ be a type instance of the class 'Functorial' then holds:
--
--   (1) #Fnc1#For all types __@x@__ and @d@ in @'Struct' ('ObjectClass' __c__) __x__@ holds:
--   @'amap' ('cOne' d) = 'id'@.
--
--   (1) #Fnc2#For all types __@x@__, __@y@__, __@z@__ and @f@ in __@c@__ __@y@__ __@z@__,
--   @g@ in __@c@__ __@x@__ __@y@__ holds: @'amap' (f '.' g) = 'amap' f '.' 'amap' g@. 
class (Applicative c, Category c) => Functorial c

--------------------------------------------------------------------------------
-- Cayleyan2 -

-- | category of isomorphisms.
--
--  __Property__ Let __@c@__ be a type instance of 'Cayleyan2', then holds:
--  For all types __@x@__, __@y@__ and @f@ in __@c@__ __@x@__ __@y@__ holds:
--  @('invert2' f '.' f) == 'cOne' ('domain' f)@ and
--  @(f '.' 'invert2' f) == 'cOne' ('range' f)@ where @(==) = 'eq2'@.
class (Category c, Eq2 c) => Cayleyan2 c where
  invert2 :: c x y -> c y x

--------------------------------------------------------------------------------
-- Cayleyan2 - Instance -

instance Cayleyan2 (Homomorphous m) where
  invert2 :: forall x y. Homomorphous m x y -> Homomorphous m y x
invert2 (Struct m x
d :>: Struct m y
r) = Struct m y
r forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct m x
d  

instance Cayleyan2 c => Cayleyan2 (Op2 c) where
  invert2 :: forall x y. Op2 c x y -> Op2 c y x
invert2 (Op2 c y x
f) = forall (h :: * -> * -> *) x y. h y x -> Op2 h x y
Op2 (forall (c :: * -> * -> *) x y. Cayleyan2 c => c x y -> c y x
invert2 c y x
f)
  
--------------------------------------------------------------------------------
-- Either2 - Morphism -

instance (Morphism f, Morphism g, ObjectClass f ~ ObjectClass g)
  => Morphism (Either2 f g) where
  
  type ObjectClass (Either2 f g) = ObjectClass f
  
  domain :: forall x y. Either2 f g x y -> Struct (ObjectClass (Either2 f g)) x
domain (Left2 f x y
f) = forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain f x y
f
  domain (Right2 g x y
g) = forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain g x y
g

  range :: forall x y. Either2 f g x y -> Struct (ObjectClass (Either2 f g)) y
range (Left2 f x y
f) = forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range f x y
f
  range (Right2 g x y
g) = forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range g x y
g

--------------------------------------------------------------------------------
-- Forget -

-- | forgets the 'ObjectClass' of __@m@__ and sets it to __@t@__, under the condition
--   that the 'ObjectClass' of __@m@__ is 'Transformable' to __@t@__.
data Forget t m x y where
  Forget :: Transformable (ObjectClass m) t => m x y -> Forget t m x y

instance Show2 m => Show2 (Forget t m) where
  show2 :: forall a b. Forget t m a b -> String
show2 (Forget m a b
m) = String
"Forget[" forall a. [a] -> [a] -> [a]
++ forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 m a b
m forall a. [a] -> [a] -> [a]
++ String
"]"
  
instance Show2 m => Show (Forget t m x y) where
  show :: Forget t m x y -> String
show = forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2

instance Eq2 m => Eq2 (Forget t m) where
  eq2 :: forall x y. Forget t m x y -> Forget t m x y -> Bool
eq2 (Forget m x y
f) (Forget m x y
g) = forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2 m x y
f m x y
g

instance Eq2 m => Eq (Forget t m x y) where
  == :: Forget t m x y -> Forget t m x y -> Bool
(==) = forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2
  
instance Morphism m => Morphism (Forget t m) where
  type ObjectClass (Forget t m) = t

  homomorphous :: forall x y.
Forget t m x y -> Homomorphous (ObjectClass (Forget t m)) x y
homomorphous (Forget m x y
m) = forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous m x y
m)

instance Applicative m => Applicative (Forget t m) where
  amap :: forall a b. Forget t m a b -> a -> b
amap (Forget m a b
h) = forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap m a b
h

--------------------------------------------------------------------------------
-- EmbeddableMorphism -

-- | morphism for which its object class can be embedded into the given structure.
class (Morphism m, Transformable (ObjectClass m) t) => EmbeddableMorphism m t

instance (Morphism m, Transformable s t) => EmbeddableMorphism (Forget s m) t

instance EmbeddableMorphism m t => EmbeddableMorphism (Op2 m) t

--------------------------------------------------------------------------------
-- EmbeddableMorphismType -

-- | helper class to avoid undecidable instances.
class EmbeddableMorphism m Typ => EmbeddableMorphismTyp m

instance (Morphism m, ForgetfulTyp t) => EmbeddableMorphismTyp (Forget t m)

instance EmbeddableMorphismTyp m => EmbeddableMorphismTyp (Op2 m)